Hilbert spaces

src/linear-algebra.lagda.md

@@ -41,7 +41,9 @@ open import linear-algebra.orthogonality-real-inner-product-spaces public
 open import linear-algebra.preimages-of-left-module-structures-along-homomorphisms-of-rings public
 open import linear-algebra.rational-modules public
 open import linear-algebra.real-banach-spaces public
+open import linear-algebra.real-hilbert-spaces public
 open import linear-algebra.real-inner-product-spaces public
+open import linear-algebra.real-inner-product-spaces-are-normed public
 open import linear-algebra.real-vector-spaces public
 open import linear-algebra.right-modules-rings public
 open import linear-algebra.scalar-multiplication-matrices public

src/linear-algebra/real-hilbert-spaces.lagda.md

@@ -0,0 +1,111 @@
+# Real Hilbert spaces
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module linear-algebra.real-hilbert-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.propositions
+open import foundation.subtypes
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import linear-algebra.normed-real-vector-spaces
+open import linear-algebra.real-banach-spaces
+open import linear-algebra.real-inner-product-spaces
+open import linear-algebra.real-inner-product-spaces-are-normed
+
+open import metric-spaces.complete-metric-spaces
+open import metric-spaces.metric-spaces
+
+open import real-numbers.cauchy-completeness-dedekind-real-numbers
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "real Hilbert space" WDID=Q190056 WD="Hilbert space" Agda=ℝ-Hilbert-Space}}
+is a [real inner product space](linear-algebra.real-inner-product-spaces.md) for
+which the [metric space](metric-spaces.metric-spaces.md)
+[induced](linear-algebra.real-inner-product-spaces-are-normed.md) by the inner
+product is [complete](metric-spaces.complete-metric-spaces.md).
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : ℝ-Inner-Product-Space l1 l2)
+  where
+
+  is-complete-prop-ℝ-Inner-Product-Space : Prop (l1 ⊔ l2)
+  is-complete-prop-ℝ-Inner-Product-Space =
+    is-complete-prop-Metric-Space
+      ( metric-space-ℝ-Inner-Product-Space V)
+
+  is-complete-ℝ-Inner-Product-Space : UU (l1 ⊔ l2)
+  is-complete-ℝ-Inner-Product-Space =
+    type-Prop is-complete-prop-ℝ-Inner-Product-Space
+
+ℝ-Hilbert-Space : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+ℝ-Hilbert-Space l1 l2 =
+  type-subtype (is-complete-prop-ℝ-Inner-Product-Space {l1} {l2})
+```
+
+## Properties
+
+### Every real Hilbert space is a real Banach space
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : ℝ-Hilbert-Space l1 l2)
+  where
+
+  inner-product-space-ℝ-Hilbert-Space : ℝ-Inner-Product-Space l1 l2
+  inner-product-space-ℝ-Hilbert-Space = pr1 V
+
+  normed-vector-space-ℝ-Hilbert-Space : Normed-ℝ-Vector-Space l1 l2
+  normed-vector-space-ℝ-Hilbert-Space =
+    normed-vector-space-ℝ-Inner-Product-Space
+      ( inner-product-space-ℝ-Hilbert-Space)
+
+  banach-space-ℝ-Hilbert-Space : ℝ-Banach-Space l1 l2
+  banach-space-ℝ-Hilbert-Space =
+    ( normed-vector-space-ℝ-Hilbert-Space , pr2 V)
+```
+
+### The real numbers are a real Hilbert space with multiplication as the inner product
+
+```agda
+abstract
+  is-complete-real-inner-product-space-ℝ :
+    (l : Level) →
+    is-complete-ℝ-Inner-Product-Space (real-inner-product-space-ℝ l)
+  is-complete-real-inner-product-space-ℝ l =
+    inv-tr
+      ( is-complete-Metric-Space)
+      ( eq-metric-space-real-inner-product-space-ℝ l)
+      ( is-complete-metric-space-ℝ l)
+
+real-hilbert-space-ℝ : (l : Level) → ℝ-Hilbert-Space l (lsuc l)
+real-hilbert-space-ℝ l =
+  ( real-inner-product-space-ℝ l ,
+    is-complete-real-inner-product-space-ℝ l)
+```
+
+## See also
+
+- [Real Banach spaces](linear-algebra.real-banach-spaces.md)
+
+## External links
+
+- [Hilbert space](https://en.wikipedia.org/wiki/Hilbert_space) on Wikipedia
+- [Hilbert space](https://ncatlab.org/nlab/show/Hilbert+space) on $n$Lab

src/linear-algebra/real-inner-product-spaces-are-normed.lagda.md

@@ -0,0 +1,219 @@
+# Real inner product spaces are normed
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module linear-algebra.real-inner-product-spaces-are-normed where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.nonzero-natural-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.logical-equivalences
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import linear-algebra.cauchy-schwarz-inequality-real-inner-product-spaces
+open import linear-algebra.normed-real-vector-spaces
+open import linear-algebra.real-inner-product-spaces
+open import linear-algebra.seminormed-real-vector-spaces
+
+open import metric-spaces.equality-of-metric-spaces
+open import metric-spaces.metric-spaces
+
+open import order-theory.large-posets
+
+open import real-numbers.absolute-value-real-numbers
+open import real-numbers.addition-nonnegative-real-numbers
+open import real-numbers.addition-real-numbers
+open import real-numbers.inequalities-addition-and-subtraction-real-numbers
+open import real-numbers.inequality-real-numbers
+open import real-numbers.metric-space-of-real-numbers
+open import real-numbers.multiplication-positive-real-numbers
+open import real-numbers.multiplication-real-numbers
+open import real-numbers.positive-real-numbers
+open import real-numbers.raising-universe-levels-real-numbers
+open import real-numbers.rational-real-numbers
+open import real-numbers.similarity-real-numbers
+open import real-numbers.square-roots-nonnegative-real-numbers
+open import real-numbers.squares-real-numbers
+```
+
+</details>
+
+## Idea
+
+Given a [real inner product space](linear-algebra.real-inner-product-spaces.md)
+`V`, defining the norm of `v` as the
+[square root](real-numbers.square-roots-nonnegative-real-numbers.md) of the
+inner product of `v` with itself satisfies the conditions of a
+[normed real vector space](linear-algebra.normed-real-vector-spaces.md).
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : ℝ-Inner-Product-Space l1 l2)
+  where
+
+  abstract
+    is-triangular-squared-norm-ℝ-Inner-Product-Space :
+      (u v : type-ℝ-Inner-Product-Space V) →
+      leq-ℝ
+        ( squared-norm-ℝ-Inner-Product-Space V
+          ( add-ℝ-Inner-Product-Space V u v))
+        ( square-ℝ
+          ( ( norm-ℝ-Inner-Product-Space V u) +ℝ
+            ( norm-ℝ-Inner-Product-Space V v)))
+    is-triangular-squared-norm-ℝ-Inner-Product-Space u v =
+      let
+        open inequality-reasoning-Large-Poset ℝ-Large-Poset
+      in
+        chain-of-inequalities
+          squared-norm-ℝ-Inner-Product-Space V (add-ℝ-Inner-Product-Space V u v)
+          ≤ ( squared-norm-ℝ-Inner-Product-Space V u) +ℝ
+            ( real-ℕ 2 *ℝ inner-product-ℝ-Inner-Product-Space V u v) +ℝ
+            ( squared-norm-ℝ-Inner-Product-Space V v)
+            by leq-eq-ℝ (squared-norm-add-ℝ-Inner-Product-Space V u v)
+          ≤ ( squared-norm-ℝ-Inner-Product-Space V u) +ℝ
+            ( ( real-ℕ 2) *ℝ
+              ( ( norm-ℝ-Inner-Product-Space V u) *ℝ
+                  norm-ℝ-Inner-Product-Space V v)) +ℝ
+            ( squared-norm-ℝ-Inner-Product-Space V v)
+            by
+              preserves-leq-right-add-ℝ _ _ _
+                ( preserves-leq-left-add-ℝ _ _ _
+                  ( preserves-leq-left-mul-ℝ⁺
+                    ( positive-real-ℕ⁺ two-ℕ⁺)
+                    ( transitive-leq-ℝ _ _ _
+                      ( cauchy-schwarz-inequality-ℝ-Inner-Product-Space V u v)
+                      ( leq-abs-ℝ _))))
+          ≤ ( square-ℝ (norm-ℝ-Inner-Product-Space V u)) +ℝ
+            ( ( real-ℕ 2) *ℝ
+              ( ( norm-ℝ-Inner-Product-Space V u) *ℝ
+                  norm-ℝ-Inner-Product-Space V v)) +ℝ
+            ( square-ℝ (norm-ℝ-Inner-Product-Space V v))
+            by
+              leq-eq-ℝ
+                ( ap-add-ℝ
+                  ( ap-add-ℝ
+                    ( inv
+                      ( eq-real-square-sqrt-ℝ⁰⁺
+                        ( nonnegative-squared-norm-ℝ-Inner-Product-Space V u)))
+                    ( refl))
+                  ( inv
+                    ( eq-real-square-sqrt-ℝ⁰⁺
+                      ( nonnegative-squared-norm-ℝ-Inner-Product-Space V v))))
+          ≤ square-ℝ
+              ( ( norm-ℝ-Inner-Product-Space V u) +ℝ
+                ( norm-ℝ-Inner-Product-Space V v))
+            by leq-eq-ℝ (inv (square-add-ℝ _ _))
+
+    is-triangular-norm-ℝ-Inner-Product-Space :
+      (u v : type-ℝ-Inner-Product-Space V) →
+      leq-ℝ
+        ( norm-ℝ-Inner-Product-Space V (add-ℝ-Inner-Product-Space V u v))
+        ( norm-ℝ-Inner-Product-Space V u +ℝ norm-ℝ-Inner-Product-Space V v)
+    is-triangular-norm-ℝ-Inner-Product-Space u v =
+      tr
+        ( leq-ℝ _)
+        ( ( inv (eq-abs-sqrt-square-ℝ _)) ∙
+          ( abs-real-ℝ⁰⁺
+            ( ( nonnegative-norm-ℝ-Inner-Product-Space V u) +ℝ⁰⁺
+              ( nonnegative-norm-ℝ-Inner-Product-Space V v))))
+        ( preserves-leq-sqrt-ℝ⁰⁺
+          ( nonnegative-squared-norm-ℝ-Inner-Product-Space V
+            ( add-ℝ-Inner-Product-Space V u v))
+          ( nonnegative-square-ℝ
+            ( norm-ℝ-Inner-Product-Space V u +ℝ norm-ℝ-Inner-Product-Space V v))
+          ( is-triangular-squared-norm-ℝ-Inner-Product-Space u v))
+
+  is-seminorm-norm-ℝ-Inner-Product-Space :
+    is-seminorm-ℝ-Vector-Space
+      ( vector-space-ℝ-Inner-Product-Space V)
+      ( norm-ℝ-Inner-Product-Space V)
+  is-seminorm-norm-ℝ-Inner-Product-Space =
+    ( is-triangular-norm-ℝ-Inner-Product-Space ,
+      is-absolutely-homogeneous-norm-ℝ-Inner-Product-Space V)
+
+  abstract
+    is-extensional-norm-ℝ-Inner-Product-Space :
+      (v : type-ℝ-Inner-Product-Space V) →
+      (norm-ℝ-Inner-Product-Space V v ＝ raise-ℝ l1 zero-ℝ) →
+      is-zero-ℝ-Inner-Product-Space V v
+    is-extensional-norm-ℝ-Inner-Product-Space v ∥v∥=0 =
+      is-extensional-diagonal-inner-product-ℝ-Inner-Product-Space
+        ( V)
+        ( v)
+        ( equational-reasoning
+          squared-norm-ℝ-Inner-Product-Space V v
+          ＝ square-ℝ (norm-ℝ-Inner-Product-Space V v)
+            by
+              inv
+                ( eq-real-square-sqrt-ℝ⁰⁺
+                  ( nonnegative-squared-norm-ℝ-Inner-Product-Space V v))
+          ＝ square-ℝ (raise-ℝ l1 zero-ℝ)
+            by ap square-ℝ ∥v∥=0
+          ＝ raise-ℝ l1 zero-ℝ
+            by square-raise-zero-ℝ l1)
+
+  norm-normed-vector-space-ℝ-Inner-Product-Space :
+    norm-ℝ-Vector-Space (vector-space-ℝ-Inner-Product-Space V)
+  norm-normed-vector-space-ℝ-Inner-Product-Space =
+    ( ( norm-ℝ-Inner-Product-Space V ,
+        is-seminorm-norm-ℝ-Inner-Product-Space) ,
+      is-extensional-norm-ℝ-Inner-Product-Space)
+
+  normed-vector-space-ℝ-Inner-Product-Space : Normed-ℝ-Vector-Space l1 l2
+  normed-vector-space-ℝ-Inner-Product-Space =
+    ( vector-space-ℝ-Inner-Product-Space V ,
+      norm-normed-vector-space-ℝ-Inner-Product-Space)
+
+  metric-space-ℝ-Inner-Product-Space : Metric-Space l2 l1
+  metric-space-ℝ-Inner-Product-Space =
+    metric-space-Normed-ℝ-Vector-Space normed-vector-space-ℝ-Inner-Product-Space
+```
+
+## Properties
+
+### The metric space of the inner product space of `ℝ` over itself is the standard metric space of `ℝ`
+
+```agda
+abstract
+  isometric-eq-metric-space-real-inner-product-space-normed-real-vector-space-ℝ :
+    (l : Level) →
+    isometric-eq-Metric-Space
+      ( metric-space-ℝ-Inner-Product-Space (real-inner-product-space-ℝ l))
+      ( metric-space-Normed-ℝ-Vector-Space (normed-real-vector-space-ℝ l))
+  isometric-eq-metric-space-real-inner-product-space-normed-real-vector-space-ℝ
+    l =
+    ( refl ,
+      λ d x y →
+        iff-eq
+          ( ap
+            ( λ m → leq-prop-ℝ m (real-ℚ⁺ d))
+            ( inv (eq-abs-sqrt-square-ℝ _))))
+
+  eq-metric-space-real-inner-product-space-normed-real-vector-space-ℝ :
+    (l : Level) →
+    metric-space-ℝ-Inner-Product-Space (real-inner-product-space-ℝ l) ＝
+    metric-space-Normed-ℝ-Vector-Space (normed-real-vector-space-ℝ l)
+  eq-metric-space-real-inner-product-space-normed-real-vector-space-ℝ l =
+    eq-isometric-eq-Metric-Space _ _
+      ( isometric-eq-metric-space-real-inner-product-space-normed-real-vector-space-ℝ
+        ( l))
+
+  eq-metric-space-real-inner-product-space-ℝ :
+    (l : Level) →
+    metric-space-ℝ-Inner-Product-Space (real-inner-product-space-ℝ l) ＝
+    metric-space-ℝ l
+  eq-metric-space-real-inner-product-space-ℝ l =
+    ( eq-metric-space-real-inner-product-space-normed-real-vector-space-ℝ l) ∙
+    ( eq-metric-space-normed-real-vector-space-metric-space-ℝ l)
+```

src/linear-algebra/real-inner-product-spaces.lagda.md

@@ -20,6 +20,7 @@ open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
 open import linear-algebra.bilinear-forms-real-vector-spaces
+open import linear-algebra.normed-real-vector-spaces
 open import linear-algebra.real-vector-spaces
 open import linear-algebra.symmetric-bilinear-forms-real-vector-spaces
 

src/real-numbers/square-roots-nonnegative-real-numbers.lagda.md

@@ -702,15 +702,6 @@ is-positive-sqrt-iff-is-positive-ℝ⁰⁺ x =
     is-positive-sqrt-is-positive-ℝ⁰⁺ x)
 ```
 
-### The square root of zero is zero
-
-```agda
-abstract
-  real-sqrt-zero-ℝ⁰⁺ : real-sqrt-ℝ⁰⁺ zero-ℝ⁰⁺ ＝ zero-ℝ
-  real-sqrt-zero-ℝ⁰⁺ =
-    inv (eq-sim-ℝ (unique-sqrt-ℝ⁰⁺ zero-ℝ⁰⁺ zero-ℝ⁰⁺ (left-zero-law-mul-ℝ _)))
-```
-
 ### The square root of a nonnegative real number preserves inequality
 
 ```agda
@@ -729,6 +720,15 @@ abstract
         ( x≤y))
 ```
 
+### The square root of zero is zero
+
+```agda
+abstract
+  real-sqrt-zero-ℝ⁰⁺ : real-sqrt-ℝ⁰⁺ zero-ℝ⁰⁺ ＝ zero-ℝ
+  real-sqrt-zero-ℝ⁰⁺ =
+    inv (eq-sim-ℝ (unique-sqrt-ℝ⁰⁺ zero-ℝ⁰⁺ zero-ℝ⁰⁺ (left-zero-law-mul-ℝ _)))
+```
+
 ### If `√x ≤ 1`, `x ≤ 1`
 
 ```agda

src/real-numbers/squares-real-numbers.lagda.md

@@ -24,6 +24,7 @@ open import elementary-number-theory.square-roots-positive-rational-numbers
 open import elementary-number-theory.squares-rational-numbers
 open import elementary-number-theory.strict-inequality-rational-numbers
 
+open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.disjunction
 open import foundation.existential-quantification
@@ -407,4 +408,9 @@ abstract
 abstract
   square-zero-ℝ : square-ℝ zero-ℝ ＝ zero-ℝ
   square-zero-ℝ = eq-sim-ℝ (left-zero-law-mul-ℝ zero-ℝ)
+
+  square-raise-zero-ℝ :
+    (l : Level) → square-ℝ (raise-zero-ℝ l) ＝ raise-zero-ℝ l
+  square-raise-zero-ℝ l =
+    square-raise-ℝ l _ ∙ ap (raise-ℝ l) square-zero-ℝ
 ```