The standard Euclidean Hilbert spaces

Content created by Louis Wasserman.

Created on 2026-01-09.
Last modified on 2026-01-09.

module functional-analysis.standard-euclidean-hilbert-spaces where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.dependent-pair-types
open import foundation.universe-levels

open import functional-analysis.real-banach-spaces
open import functional-analysis.real-hilbert-spaces

open import linear-algebra.standard-euclidean-inner-product-spaces

open import metric-spaces.complete-metric-spaces
open import metric-spaces.uniform-homeomorphisms-metric-spaces

open import real-numbers.metric-space-of-functions-into-real-numbers

open import univalent-combinatorics.standard-finite-types

Idea

The standard Euclidean inner product space ℝⁿ is a Hilbert space (and therefore a Banach space).

Definition

abstract
  is-complete-euclidean-metric-space-ℝ-Fin :
    (n : ℕ) (l : Level) →
    is-complete-Metric-Space (euclidean-metric-space-ℝ-Fin n l)
  is-complete-euclidean-metric-space-ℝ-Fin n l =
    is-complete-metric-space-uniform-homeo-Metric-Space
      ( function-into-ℝ-Metric-Space (Fin n) l)
      ( euclidean-metric-space-ℝ-Fin n l)
      ( uniform-homeo-id-product-euclidean-metric-space-ℝ-Fin
        ( n)
        ( l))
      ( is-complete-function-into-ℝ-Metric-Space (Fin n) l)

euclidean-hilbert-space-ℝ-Fin : (n : ℕ) (l : Level) → ℝ-Hilbert-Space l (lsuc l)
euclidean-hilbert-space-ℝ-Fin n l =
  ( inner-product-space-ℝ-Fin n l ,
    is-complete-euclidean-metric-space-ℝ-Fin n l)

euclidean-banach-space-ℝ-Fin : (n : ℕ) (l : Level) → ℝ-Banach-Space l (lsuc l)
euclidean-banach-space-ℝ-Fin n l =
  banach-space-ℝ-Hilbert-Space (euclidean-hilbert-space-ℝ-Fin n l)

Recent changes