Skip to content

Commit ba79ddf

Browse files
lowasserlowasser
authored
Hilbert spaces (#1713)
Uses the Cauchy-Schwarz inequality to prove the triangle inequality for inner product spaces, and that inner product spaces are normed.
1 parent 7b80669 commit ba79ddf

File tree

6 files changed

+348
-9
lines changed

6 files changed

+348
-9
lines changed

‎src/linear-algebra.lagda.md‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,9 @@ open import linear-algebra.orthogonality-real-inner-product-spaces public
4141
open import linear-algebra.preimages-of-left-module-structures-along-homomorphisms-of-rings public
4242
open import linear-algebra.rational-modules public
4343
open import linear-algebra.real-banach-spaces public
44+
open import linear-algebra.real-hilbert-spaces public
4445
open import linear-algebra.real-inner-product-spaces public
46+
open import linear-algebra.real-inner-product-spaces-are-normed public
4547
open import linear-algebra.real-vector-spaces public
4648
open import linear-algebra.right-modules-rings public
4749
open import linear-algebra.scalar-multiplication-matrices public

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

Lines changed: 111 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,111 @@
1+
# Real Hilbert spaces
2+
3+
```agda
4+
{-# OPTIONS --lossy-unification #-}
5+
6+
module linear-algebra.real-hilbert-spaces where
7+
```
8+
9+
<details><summary>Imports</summary>
10+
11+
```agda
12+
open import foundation.dependent-pair-types
13+
open import foundation.propositions
14+
open import foundation.subtypes
15+
open import foundation.transport-along-identifications
16+
open import foundation.universe-levels
17+
18+
open import linear-algebra.normed-real-vector-spaces
19+
open import linear-algebra.real-banach-spaces
20+
open import linear-algebra.real-inner-product-spaces
21+
open import linear-algebra.real-inner-product-spaces-are-normed
22+
23+
open import metric-spaces.complete-metric-spaces
24+
open import metric-spaces.metric-spaces
25+
26+
open import real-numbers.cauchy-completeness-dedekind-real-numbers
27+
```
28+
29+
</details>
30+
31+
## Idea
32+
33+
A
34+
{{#concept "real Hilbert space" WDID=Q190056 WD="Hilbert space" Agda=ℝ-Hilbert-Space}}
35+
is a [real inner product space](linear-algebra.real-inner-product-spaces.md) for
36+
which the [metric space](metric-spaces.metric-spaces.md)
37+
[induced](linear-algebra.real-inner-product-spaces-are-normed.md) by the inner
38+
product is [complete](metric-spaces.complete-metric-spaces.md).
39+
40+
## Definition
41+
42+
```agda
43+
module _
44+
{l1 l2 : Level}
45+
(V : ℝ-Inner-Product-Space l1 l2)
46+
where
47+
48+
is-complete-prop-ℝ-Inner-Product-Space : Prop (l1 ⊔ l2)
49+
is-complete-prop-ℝ-Inner-Product-Space =
50+
is-complete-prop-Metric-Space
51+
( metric-space-ℝ-Inner-Product-Space V)
52+
53+
is-complete-ℝ-Inner-Product-Space : UU (l1 ⊔ l2)
54+
is-complete-ℝ-Inner-Product-Space =
55+
type-Prop is-complete-prop-ℝ-Inner-Product-Space
56+
57+
ℝ-Hilbert-Space : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
58+
ℝ-Hilbert-Space l1 l2 =
59+
type-subtype (is-complete-prop-ℝ-Inner-Product-Space {l1} {l2})
60+
```
61+
62+
## Properties
63+
64+
### Every real Hilbert space is a real Banach space
65+
66+
```agda
67+
module _
68+
{l1 l2 : Level}
69+
(V : ℝ-Hilbert-Space l1 l2)
70+
where
71+
72+
inner-product-space-ℝ-Hilbert-Space : ℝ-Inner-Product-Space l1 l2
73+
inner-product-space-ℝ-Hilbert-Space = pr1 V
74+
75+
normed-vector-space-ℝ-Hilbert-Space : Normed-ℝ-Vector-Space l1 l2
76+
normed-vector-space-ℝ-Hilbert-Space =
77+
normed-vector-space-ℝ-Inner-Product-Space
78+
( inner-product-space-ℝ-Hilbert-Space)
79+
80+
banach-space-ℝ-Hilbert-Space : ℝ-Banach-Space l1 l2
81+
banach-space-ℝ-Hilbert-Space =
82+
( normed-vector-space-ℝ-Hilbert-Space , pr2 V)
83+
```
84+
85+
### The real numbers are a real Hilbert space with multiplication as the inner product
86+
87+
```agda
88+
abstract
89+
is-complete-real-inner-product-space-ℝ :
90+
(l : Level) →
91+
is-complete-ℝ-Inner-Product-Space (real-inner-product-space-ℝ l)
92+
is-complete-real-inner-product-space-ℝ l =
93+
inv-tr
94+
( is-complete-Metric-Space)
95+
( eq-metric-space-real-inner-product-space-ℝ l)
96+
( is-complete-metric-space-ℝ l)
97+
98+
real-hilbert-space-ℝ : (l : Level) → ℝ-Hilbert-Space l (lsuc l)
99+
real-hilbert-space-ℝ l =
100+
( real-inner-product-space-ℝ l ,
101+
is-complete-real-inner-product-space-ℝ l)
102+
```
103+
104+
## See also
105+
106+
- [Real Banach spaces](linear-algebra.real-banach-spaces.md)
107+
108+
## External links
109+
110+
- [Hilbert space](https://en.wikipedia.org/wiki/Hilbert_space) on Wikipedia
111+
- [Hilbert space](https://ncatlab.org/nlab/show/Hilbert+space) on $n$Lab

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

Lines changed: 219 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,219 @@
1+
# Real inner product spaces are normed
2+
3+
```agda
4+
{-# OPTIONS --lossy-unification #-}
5+
6+
module linear-algebra.real-inner-product-spaces-are-normed where
7+
```
8+
9+
<details><summary>Imports</summary>
10+
11+
```agda
12+
open import elementary-number-theory.nonzero-natural-numbers
13+
14+
open import foundation.action-on-identifications-functions
15+
open import foundation.dependent-pair-types
16+
open import foundation.identity-types
17+
open import foundation.logical-equivalences
18+
open import foundation.transport-along-identifications
19+
open import foundation.universe-levels
20+
21+
open import linear-algebra.cauchy-schwarz-inequality-real-inner-product-spaces
22+
open import linear-algebra.normed-real-vector-spaces
23+
open import linear-algebra.real-inner-product-spaces
24+
open import linear-algebra.seminormed-real-vector-spaces
25+
26+
open import metric-spaces.equality-of-metric-spaces
27+
open import metric-spaces.metric-spaces
28+
29+
open import order-theory.large-posets
30+
31+
open import real-numbers.absolute-value-real-numbers
32+
open import real-numbers.addition-nonnegative-real-numbers
33+
open import real-numbers.addition-real-numbers
34+
open import real-numbers.inequalities-addition-and-subtraction-real-numbers
35+
open import real-numbers.inequality-real-numbers
36+
open import real-numbers.metric-space-of-real-numbers
37+
open import real-numbers.multiplication-positive-real-numbers
38+
open import real-numbers.multiplication-real-numbers
39+
open import real-numbers.positive-real-numbers
40+
open import real-numbers.raising-universe-levels-real-numbers
41+
open import real-numbers.rational-real-numbers
42+
open import real-numbers.similarity-real-numbers
43+
open import real-numbers.square-roots-nonnegative-real-numbers
44+
open import real-numbers.squares-real-numbers
45+
```
46+
47+
</details>
48+
49+
## Idea
50+
51+
Given a [real inner product space](linear-algebra.real-inner-product-spaces.md)
52+
`V`, defining the norm of `v` as the
53+
[square root](real-numbers.square-roots-nonnegative-real-numbers.md) of the
54+
inner product of `v` with itself satisfies the conditions of a
55+
[normed real vector space](linear-algebra.normed-real-vector-spaces.md).
56+
57+
## Definition
58+
59+
```agda
60+
module _
61+
{l1 l2 : Level}
62+
(V : ℝ-Inner-Product-Space l1 l2)
63+
where
64+
65+
abstract
66+
is-triangular-squared-norm-ℝ-Inner-Product-Space :
67+
(u v : type-ℝ-Inner-Product-Space V) →
68+
leq-ℝ
69+
( squared-norm-ℝ-Inner-Product-Space V
70+
( add-ℝ-Inner-Product-Space V u v))
71+
( square-ℝ
72+
( ( norm-ℝ-Inner-Product-Space V u) +ℝ
73+
( norm-ℝ-Inner-Product-Space V v)))
74+
is-triangular-squared-norm-ℝ-Inner-Product-Space u v =
75+
let
76+
open inequality-reasoning-Large-Poset ℝ-Large-Poset
77+
in
78+
chain-of-inequalities
79+
squared-norm-ℝ-Inner-Product-Space V (add-ℝ-Inner-Product-Space V u v)
80+
≤ ( squared-norm-ℝ-Inner-Product-Space V u) +ℝ
81+
( real-ℕ 2 *ℝ inner-product-ℝ-Inner-Product-Space V u v) +ℝ
82+
( squared-norm-ℝ-Inner-Product-Space V v)
83+
by leq-eq-ℝ (squared-norm-add-ℝ-Inner-Product-Space V u v)
84+
≤ ( squared-norm-ℝ-Inner-Product-Space V u) +ℝ
85+
( ( real-ℕ 2) *ℝ
86+
( ( norm-ℝ-Inner-Product-Space V u) *ℝ
87+
norm-ℝ-Inner-Product-Space V v)) +ℝ
88+
( squared-norm-ℝ-Inner-Product-Space V v)
89+
by
90+
preserves-leq-right-add-ℝ _ _ _
91+
( preserves-leq-left-add-ℝ _ _ _
92+
( preserves-leq-left-mul-ℝ⁺
93+
( positive-real-ℕ⁺ two-ℕ⁺)
94+
( transitive-leq-ℝ _ _ _
95+
( cauchy-schwarz-inequality-ℝ-Inner-Product-Space V u v)
96+
( leq-abs-ℝ _))))
97+
≤ ( square-ℝ (norm-ℝ-Inner-Product-Space V u)) +ℝ
98+
( ( real-ℕ 2) *ℝ
99+
( ( norm-ℝ-Inner-Product-Space V u) *ℝ
100+
norm-ℝ-Inner-Product-Space V v)) +ℝ
101+
( square-ℝ (norm-ℝ-Inner-Product-Space V v))
102+
by
103+
leq-eq-ℝ
104+
( ap-add-ℝ
105+
( ap-add-ℝ
106+
( inv
107+
( eq-real-square-sqrt-ℝ⁰⁺
108+
( nonnegative-squared-norm-ℝ-Inner-Product-Space V u)))
109+
( refl))
110+
( inv
111+
( eq-real-square-sqrt-ℝ⁰⁺
112+
( nonnegative-squared-norm-ℝ-Inner-Product-Space V v))))
113+
≤ square-ℝ
114+
( ( norm-ℝ-Inner-Product-Space V u) +ℝ
115+
( norm-ℝ-Inner-Product-Space V v))
116+
by leq-eq-ℝ (inv (square-add-ℝ _ _))
117+
118+
is-triangular-norm-ℝ-Inner-Product-Space :
119+
(u v : type-ℝ-Inner-Product-Space V) →
120+
leq-ℝ
121+
( norm-ℝ-Inner-Product-Space V (add-ℝ-Inner-Product-Space V u v))
122+
( norm-ℝ-Inner-Product-Space V u +ℝ norm-ℝ-Inner-Product-Space V v)
123+
is-triangular-norm-ℝ-Inner-Product-Space u v =
124+
tr
125+
( leq-ℝ _)
126+
( ( inv (eq-abs-sqrt-square-ℝ _)) ∙
127+
( abs-real-ℝ⁰⁺
128+
( ( nonnegative-norm-ℝ-Inner-Product-Space V u) +ℝ⁰⁺
129+
( nonnegative-norm-ℝ-Inner-Product-Space V v))))
130+
( preserves-leq-sqrt-ℝ⁰⁺
131+
( nonnegative-squared-norm-ℝ-Inner-Product-Space V
132+
( add-ℝ-Inner-Product-Space V u v))
133+
( nonnegative-square-ℝ
134+
( norm-ℝ-Inner-Product-Space V u +ℝ norm-ℝ-Inner-Product-Space V v))
135+
( is-triangular-squared-norm-ℝ-Inner-Product-Space u v))
136+
137+
is-seminorm-norm-ℝ-Inner-Product-Space :
138+
is-seminorm-ℝ-Vector-Space
139+
( vector-space-ℝ-Inner-Product-Space V)
140+
( norm-ℝ-Inner-Product-Space V)
141+
is-seminorm-norm-ℝ-Inner-Product-Space =
142+
( is-triangular-norm-ℝ-Inner-Product-Space ,
143+
is-absolutely-homogeneous-norm-ℝ-Inner-Product-Space V)
144+
145+
abstract
146+
is-extensional-norm-ℝ-Inner-Product-Space :
147+
(v : type-ℝ-Inner-Product-Space V) →
148+
(norm-ℝ-Inner-Product-Space V v ＝ raise-ℝ l1 zero-ℝ) →
149+
is-zero-ℝ-Inner-Product-Space V v
150+
is-extensional-norm-ℝ-Inner-Product-Space v ∥v∥=0 =
151+
is-extensional-diagonal-inner-product-ℝ-Inner-Product-Space
152+
( V)
153+
( v)
154+
( equational-reasoning
155+
squared-norm-ℝ-Inner-Product-Space V v
156+
＝ square-ℝ (norm-ℝ-Inner-Product-Space V v)
157+
by
158+
inv
159+
( eq-real-square-sqrt-ℝ⁰⁺
160+
( nonnegative-squared-norm-ℝ-Inner-Product-Space V v))
161+
＝ square-ℝ (raise-ℝ l1 zero-ℝ)
162+
by ap square-ℝ ∥v∥=0
163+
＝ raise-ℝ l1 zero-ℝ
164+
by square-raise-zero-ℝ l1)
165+
166+
norm-normed-vector-space-ℝ-Inner-Product-Space :
167+
norm-ℝ-Vector-Space (vector-space-ℝ-Inner-Product-Space V)
168+
norm-normed-vector-space-ℝ-Inner-Product-Space =
169+
( ( norm-ℝ-Inner-Product-Space V ,
170+
is-seminorm-norm-ℝ-Inner-Product-Space) ,
171+
is-extensional-norm-ℝ-Inner-Product-Space)
172+
173+
normed-vector-space-ℝ-Inner-Product-Space : Normed-ℝ-Vector-Space l1 l2
174+
normed-vector-space-ℝ-Inner-Product-Space =
175+
( vector-space-ℝ-Inner-Product-Space V ,
176+
norm-normed-vector-space-ℝ-Inner-Product-Space)
177+
178+
metric-space-ℝ-Inner-Product-Space : Metric-Space l2 l1
179+
metric-space-ℝ-Inner-Product-Space =
180+
metric-space-Normed-ℝ-Vector-Space normed-vector-space-ℝ-Inner-Product-Space
181+
```
182+
183+
## Properties
184+
185+
### The metric space of the inner product space of `ℝ` over itself is the standard metric space of `ℝ`
186+
187+
```agda
188+
abstract
189+
isometric-eq-metric-space-real-inner-product-space-normed-real-vector-space-ℝ :
190+
(l : Level) →
191+
isometric-eq-Metric-Space
192+
( metric-space-ℝ-Inner-Product-Space (real-inner-product-space-ℝ l))
193+
( metric-space-Normed-ℝ-Vector-Space (normed-real-vector-space-ℝ l))
194+
isometric-eq-metric-space-real-inner-product-space-normed-real-vector-space-ℝ
195+
l =
196+
( refl ,
197+
λ d x y →
198+
iff-eq
199+
( ap
200+
( λ m → leq-prop-ℝ m (real-ℚ⁺ d))
201+
( inv (eq-abs-sqrt-square-ℝ _))))
202+
203+
eq-metric-space-real-inner-product-space-normed-real-vector-space-ℝ :
204+
(l : Level) →
205+
metric-space-ℝ-Inner-Product-Space (real-inner-product-space-ℝ l) ＝
206+
metric-space-Normed-ℝ-Vector-Space (normed-real-vector-space-ℝ l)
207+
eq-metric-space-real-inner-product-space-normed-real-vector-space-ℝ l =
208+
eq-isometric-eq-Metric-Space _ _
209+
( isometric-eq-metric-space-real-inner-product-space-normed-real-vector-space-ℝ
210+
( l))
211+
212+
eq-metric-space-real-inner-product-space-ℝ :
213+
(l : Level) →
214+
metric-space-ℝ-Inner-Product-Space (real-inner-product-space-ℝ l) ＝
215+
metric-space-ℝ l
216+
eq-metric-space-real-inner-product-space-ℝ l =
217+
( eq-metric-space-real-inner-product-space-normed-real-vector-space-ℝ l) ∙
218+
( eq-metric-space-normed-real-vector-space-metric-space-ℝ l)
219+
```

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ open import foundation.transport-along-identifications
2020
open import foundation.universe-levels
2121
2222
open import linear-algebra.bilinear-forms-real-vector-spaces
23+
open import linear-algebra.normed-real-vector-spaces
2324
open import linear-algebra.real-vector-spaces
2425
open import linear-algebra.symmetric-bilinear-forms-real-vector-spaces
2526

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

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -702,15 +702,6 @@ is-positive-sqrt-iff-is-positive-ℝ⁰⁺ x =
702702
is-positive-sqrt-is-positive-ℝ⁰⁺ x)
703703
```
704704

705-
### The square root of zero is zero
706-
707-
```agda
708-
abstract
709-
real-sqrt-zero-ℝ⁰⁺ : real-sqrt-ℝ⁰⁺ zero-ℝ⁰⁺ ＝ zero-ℝ
710-
real-sqrt-zero-ℝ⁰⁺ =
711-
inv (eq-sim-ℝ (unique-sqrt-ℝ⁰⁺ zero-ℝ⁰⁺ zero-ℝ⁰⁺ (left-zero-law-mul-ℝ _)))
712-
```
713-
714705
### The square root of a nonnegative real number preserves inequality
715706

716707
```agda
@@ -729,6 +720,15 @@ abstract
729720
( x≤y))
730721
```
731722

723+
### The square root of zero is zero
724+
725+
```agda
726+
abstract
727+
real-sqrt-zero-ℝ⁰⁺ : real-sqrt-ℝ⁰⁺ zero-ℝ⁰⁺ ＝ zero-ℝ
728+
real-sqrt-zero-ℝ⁰⁺ =
729+
inv (eq-sim-ℝ (unique-sqrt-ℝ⁰⁺ zero-ℝ⁰⁺ zero-ℝ⁰⁺ (left-zero-law-mul-ℝ _)))
730+
```
731+
732732
### If `√x ≤ 1`, `x ≤ 1`
733733

734734
```agda

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

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@ open import elementary-number-theory.square-roots-positive-rational-numbers
2424
open import elementary-number-theory.squares-rational-numbers
2525
open import elementary-number-theory.strict-inequality-rational-numbers
2626
27+
open import foundation.action-on-identifications-functions
2728
open import foundation.dependent-pair-types
2829
open import foundation.disjunction
2930
open import foundation.existential-quantification
@@ -407,4 +408,9 @@ abstract
407408
abstract
408409
square-zero-ℝ : square-ℝ zero-ℝ ＝ zero-ℝ
409410
square-zero-ℝ = eq-sim-ℝ (left-zero-law-mul-ℝ zero-ℝ)
411+
412+
square-raise-zero-ℝ :
413+
(l : Level) → square-ℝ (raise-zero-ℝ l) ＝ raise-zero-ℝ l
414+
square-raise-zero-ℝ l =
415+
square-raise-ℝ l _ ∙ ap (raise-ℝ l) square-zero-ℝ
410416
```

0 commit comments

Comments
 (0)