Skip to content

Commit 6f37f04

Browse files
lowasserlowasser
authored
Inner product spaces (#1705)
Includes the Pythagorean theorem. Completes #1691. Builds on #1704 , but doesn't actually connect yet -- that'll require a proof of Cauchy-Schwarz, which I am trying to figure out; Wikipedia's proofs lean on excluded middle and I haven't yet figured out how to sidestep that.
1 parent abcdc62 commit 6f37f04

14 files changed

+1101
-8
lines changed

‎src/linear-algebra.lagda.md‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@
55
```agda
66
module linear-algebra where
77
8+
open import linear-algebra.bilinear-forms-real-vector-spaces public
89
open import linear-algebra.complex-vector-spaces public
910
open import linear-algebra.constant-matrices public
1011
open import linear-algebra.constant-tuples public
@@ -33,14 +34,18 @@ open import linear-algebra.linear-spans-left-modules-rings public
3334
open import linear-algebra.matrices public
3435
open import linear-algebra.matrices-on-rings public
3536
open import linear-algebra.multiplication-matrices public
37+
open import linear-algebra.orthogonality-bilinear-forms-real-vector-spaces public
38+
open import linear-algebra.orthogonality-real-inner-product-spaces public
3639
open import linear-algebra.preimages-of-left-module-structures-along-homomorphisms-of-rings public
3740
open import linear-algebra.rational-modules public
41+
open import linear-algebra.real-inner-product-spaces public
3842
open import linear-algebra.real-vector-spaces public
3943
open import linear-algebra.right-modules-rings public
4044
open import linear-algebra.scalar-multiplication-matrices public
4145
open import linear-algebra.scalar-multiplication-tuples public
4246
open import linear-algebra.scalar-multiplication-tuples-on-rings public
4347
open import linear-algebra.subsets-left-modules-rings public
48+
open import linear-algebra.symmetric-bilinear-forms-real-vector-spaces public
4449
open import linear-algebra.transposition-matrices public
4550
open import linear-algebra.tuples-on-commutative-monoids public
4651
open import linear-algebra.tuples-on-commutative-rings public

‎src/linear-algebra/bilinear-forms-real-vector-spaces.lagda.md‎

Lines changed: 178 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,178 @@
1+
# Bilinear forms in real vector spaces
2+
3+
```agda
4+
{-# OPTIONS --lossy-unification #-}
5+
6+
module linear-algebra.bilinear-forms-real-vector-spaces where
7+
```
8+
9+
<details><summary>Imports</summary>
10+
11+
```agda
12+
open import foundation.conjunction
13+
open import foundation.dependent-pair-types
14+
open import foundation.propositions
15+
open import foundation.sets
16+
open import foundation.subtypes
17+
open import foundation.universe-levels
18+
19+
open import linear-algebra.real-vector-spaces
20+
21+
open import real-numbers.addition-real-numbers
22+
open import real-numbers.dedekind-real-numbers
23+
open import real-numbers.multiplication-real-numbers
24+
```
25+
26+
</details>
27+
28+
## Idea
29+
30+
A
31+
{{#concept "bilinear form" WDID=Q837924 WD="bilinear form" Disambiguation="on a real vector space" Agda=bilinear-form-ℝ-Vector-Space}}
32+
on a [real vector space](linear-algebra.real-vector-spaces.md) `V` is a map
33+
`B : V → V → ℝ` that is linear in each argument:
34+
`B (a * x + b * y) z = a * B x z + b * B y z` and
35+
`B x (a * y + b * z) = a * B x y + b * B x z`.
36+
37+
## Definition
38+
39+
```agda
40+
module _
41+
{l1 l2 : Level}
42+
(V : ℝ-Vector-Space l1 l2)
43+
(B : type-ℝ-Vector-Space V → type-ℝ-Vector-Space V → ℝ l1)
44+
where
45+
46+
is-left-additive-prop-form-ℝ-Vector-Space : Prop (lsuc l1 ⊔ l2)
47+
is-left-additive-prop-form-ℝ-Vector-Space =
48+
Π-Prop
49+
( type-ℝ-Vector-Space V)
50+
( λ x →
51+
Π-Prop
52+
( type-ℝ-Vector-Space V)
53+
( λ y →
54+
Π-Prop
55+
( type-ℝ-Vector-Space V)
56+
( λ z →
57+
Id-Prop
58+
( ℝ-Set l1)
59+
( B (add-ℝ-Vector-Space V x y) z)
60+
( B x z +ℝ B y z))))
61+
62+
is-left-additive-form-ℝ-Vector-Space : UU (lsuc l1 ⊔ l2)
63+
is-left-additive-form-ℝ-Vector-Space =
64+
type-Prop is-left-additive-prop-form-ℝ-Vector-Space
65+
66+
preserves-scalar-mul-left-prop-form-ℝ-Vector-Space : Prop (lsuc l1 ⊔ l2)
67+
preserves-scalar-mul-left-prop-form-ℝ-Vector-Space =
68+
Π-Prop
69+
( ℝ l1)
70+
( λ a →
71+
Π-Prop
72+
( type-ℝ-Vector-Space V)
73+
( λ x →
74+
Π-Prop
75+
( type-ℝ-Vector-Space V)
76+
( λ y →
77+
Id-Prop
78+
( ℝ-Set l1)
79+
( B (mul-ℝ-Vector-Space V a x) y)
80+
( a *ℝ B x y))))
81+
82+
preserves-scalar-mul-left-form-ℝ-Vector-Space : UU (lsuc l1 ⊔ l2)
83+
preserves-scalar-mul-left-form-ℝ-Vector-Space =
84+
type-Prop preserves-scalar-mul-left-prop-form-ℝ-Vector-Space
85+
86+
is-right-additive-prop-form-ℝ-Vector-Space : Prop (lsuc l1 ⊔ l2)
87+
is-right-additive-prop-form-ℝ-Vector-Space =
88+
Π-Prop
89+
( type-ℝ-Vector-Space V)
90+
( λ x →
91+
Π-Prop
92+
( type-ℝ-Vector-Space V)
93+
( λ y →
94+
Π-Prop
95+
( type-ℝ-Vector-Space V)
96+
( λ z →
97+
Id-Prop
98+
( ℝ-Set l1)
99+
( B x (add-ℝ-Vector-Space V y z))
100+
( B x y +ℝ B x z))))
101+
102+
is-right-additive-form-ℝ-Vector-Space : UU (lsuc l1 ⊔ l2)
103+
is-right-additive-form-ℝ-Vector-Space =
104+
type-Prop is-right-additive-prop-form-ℝ-Vector-Space
105+
106+
preserves-scalar-mul-right-prop-form-ℝ-Vector-Space : Prop (lsuc l1 ⊔ l2)
107+
preserves-scalar-mul-right-prop-form-ℝ-Vector-Space =
108+
Π-Prop
109+
( ℝ l1)
110+
( λ a →
111+
Π-Prop
112+
( type-ℝ-Vector-Space V)
113+
( λ x →
114+
Π-Prop
115+
( type-ℝ-Vector-Space V)
116+
( λ y →
117+
Id-Prop
118+
( ℝ-Set l1)
119+
( B x (mul-ℝ-Vector-Space V a y))
120+
( a *ℝ B x y))))
121+
122+
preserves-scalar-mul-right-form-ℝ-Vector-Space : UU (lsuc l1 ⊔ l2)
123+
preserves-scalar-mul-right-form-ℝ-Vector-Space =
124+
type-Prop preserves-scalar-mul-right-prop-form-ℝ-Vector-Space
125+
126+
is-bilinear-prop-form-ℝ-Vector-Space : Prop (lsuc l1 ⊔ l2)
127+
is-bilinear-prop-form-ℝ-Vector-Space =
128+
is-left-additive-prop-form-ℝ-Vector-Space ∧
129+
preserves-scalar-mul-left-prop-form-ℝ-Vector-Space ∧
130+
is-right-additive-prop-form-ℝ-Vector-Space ∧
131+
preserves-scalar-mul-right-prop-form-ℝ-Vector-Space
132+
133+
is-bilinear-form-ℝ-Vector-Space : UU (lsuc l1 ⊔ l2)
134+
is-bilinear-form-ℝ-Vector-Space =
135+
type-Prop is-bilinear-prop-form-ℝ-Vector-Space
136+
137+
bilinear-form-ℝ-Vector-Space :
138+
{l1 l2 : Level} (V : ℝ-Vector-Space l1 l2) → UU (lsuc l1 ⊔ l2)
139+
bilinear-form-ℝ-Vector-Space V =
140+
type-subtype (is-bilinear-prop-form-ℝ-Vector-Space V)
141+
142+
module _
143+
{l1 l2 : Level}
144+
(V : ℝ-Vector-Space l1 l2)
145+
(B : bilinear-form-ℝ-Vector-Space V)
146+
where
147+
148+
map-bilinear-form-ℝ-Vector-Space :
149+
type-ℝ-Vector-Space V → type-ℝ-Vector-Space V → ℝ l1
150+
map-bilinear-form-ℝ-Vector-Space = pr1 B
151+
152+
is-left-additive-map-bilinear-form-ℝ-Vector-Space :
153+
is-left-additive-form-ℝ-Vector-Space V map-bilinear-form-ℝ-Vector-Space
154+
is-left-additive-map-bilinear-form-ℝ-Vector-Space = pr1 (pr2 B)
155+
156+
preserves-scalar-mul-left-map-bilinear-form-ℝ-Vector-Space :
157+
preserves-scalar-mul-left-form-ℝ-Vector-Space
158+
( V)
159+
( map-bilinear-form-ℝ-Vector-Space)
160+
preserves-scalar-mul-left-map-bilinear-form-ℝ-Vector-Space = pr1 (pr2 (pr2 B))
161+
162+
is-right-additive-map-bilinear-form-ℝ-Vector-Space :
163+
is-right-additive-form-ℝ-Vector-Space
164+
( V)
165+
( map-bilinear-form-ℝ-Vector-Space)
166+
is-right-additive-map-bilinear-form-ℝ-Vector-Space = pr1 (pr2 (pr2 (pr2 B)))
167+
168+
preserves-scalar-mul-right-map-bilinear-form-ℝ-Vector-Space :
169+
preserves-scalar-mul-right-form-ℝ-Vector-Space
170+
( V)
171+
( map-bilinear-form-ℝ-Vector-Space)
172+
preserves-scalar-mul-right-map-bilinear-form-ℝ-Vector-Space =
173+
pr2 (pr2 (pr2 (pr2 B)))
174+
```
175+
176+
## External links
177+
178+
- [Bilinear form](https://en.wikipedia.org/wiki/Bilinear_form) on Wikipedia

‎src/linear-algebra/orthogonality-bilinear-forms-real-vector-spaces.lagda.md‎

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
# Orthogonality relative to a bilinear form in a real vector space
2+
3+
```agda
4+
module linear-algebra.orthogonality-bilinear-forms-real-vector-spaces where
5+
```
6+
7+
<details><summary>Imports</summary>
8+
9+
```agda
10+
open import foundation.binary-relations
11+
open import foundation.identity-types
12+
open import foundation.sets
13+
open import foundation.universe-levels
14+
15+
open import linear-algebra.bilinear-forms-real-vector-spaces
16+
open import linear-algebra.real-vector-spaces
17+
18+
open import real-numbers.dedekind-real-numbers
19+
open import real-numbers.rational-real-numbers
20+
```
21+
22+
</details>
23+
24+
## Idea
25+
26+
Two elements `u` and `v` of a
27+
[real vector space](linear-algebra.real-vector-spaces.md) `V` are
28+
{{#concept "orthogonal" Disambiguation="relative to a bilinear form over a real vector space" Agda=is-orthogonal-bilinear-form-ℝ-Vector-Space}}
29+
relative to a
30+
[bilinear form](linear-algebra.bilinear-forms-real-vector-spaces.md)
31+
`B : V → V → ℝ` if `B u v = 0`.
32+
33+
## Definition
34+
35+
```agda
36+
module _
37+
{l1 l2 : Level}
38+
(V : ℝ-Vector-Space l1 l2)
39+
(B : bilinear-form-ℝ-Vector-Space V)
40+
where
41+
42+
is-orthogonal-prop-bilinear-form-ℝ-Vector-Space :
43+
Relation-Prop (lsuc l1) (type-ℝ-Vector-Space V)
44+
is-orthogonal-prop-bilinear-form-ℝ-Vector-Space v w =
45+
Id-Prop
46+
( ℝ-Set l1)
47+
( map-bilinear-form-ℝ-Vector-Space V B v w)
48+
( raise-zero-ℝ l1)
49+
50+
is-orthogonal-bilinear-form-ℝ-Vector-Space :
51+
Relation (lsuc l1) (type-ℝ-Vector-Space V)
52+
is-orthogonal-bilinear-form-ℝ-Vector-Space =
53+
type-Relation-Prop is-orthogonal-prop-bilinear-form-ℝ-Vector-Space
54+
```

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

Lines changed: 132 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,132 @@
1+
# Orthogonality in real inner product spaces
2+
3+
```agda
4+
module linear-algebra.orthogonality-real-inner-product-spaces where
5+
```
6+
7+
<details><summary>Imports</summary>
8+
9+
```agda
10+
open import foundation.action-on-identifications-functions
11+
open import foundation.binary-relations
12+
open import foundation.identity-types
13+
open import foundation.universe-levels
14+
15+
open import linear-algebra.orthogonality-bilinear-forms-real-vector-spaces
16+
open import linear-algebra.real-inner-product-spaces
17+
18+
open import real-numbers.addition-nonnegative-real-numbers
19+
open import real-numbers.addition-real-numbers
20+
open import real-numbers.multiplication-real-numbers
21+
open import real-numbers.nonnegative-real-numbers
22+
open import real-numbers.raising-universe-levels-real-numbers
23+
open import real-numbers.rational-real-numbers
24+
open import real-numbers.similarity-real-numbers
25+
open import real-numbers.square-roots-nonnegative-real-numbers
26+
```
27+
28+
</details>
29+
30+
## Idea
31+
32+
Two vectors are
33+
{{#concept "orthogonal" WDID=Q215067 WD="orthogonality" Agda=is-orthogonal-ℝ-Inner-Product-Space Disambiguation="in a real inner product space"}}
34+
in a [real inner product space](linear-algebra.real-inner-product-spaces.md) if
35+
they are
36+
[orthogonal](linear-algebra.orthogonality-bilinear-forms-real-vector-spaces.md)
37+
relative to the inner product as a
38+
[bilinear form](linear-algebra.bilinear-forms-real-vector-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-orthogonal-prop-ℝ-Inner-Product-Space :
49+
Relation-Prop (lsuc l1) (type-ℝ-Inner-Product-Space V)
50+
is-orthogonal-prop-ℝ-Inner-Product-Space =
51+
is-orthogonal-prop-bilinear-form-ℝ-Vector-Space
52+
( vector-space-ℝ-Inner-Product-Space V)
53+
( bilinear-form-inner-product-ℝ-Inner-Product-Space V)
54+
55+
is-orthogonal-ℝ-Inner-Product-Space :
56+
Relation (lsuc l1) (type-ℝ-Inner-Product-Space V)
57+
is-orthogonal-ℝ-Inner-Product-Space =
58+
type-Relation-Prop is-orthogonal-prop-ℝ-Inner-Product-Space
59+
```
60+
61+
## Properties
62+
63+
### The Pythagorean Theorem
64+
65+
The Pythagorean theorem for real inner product spaces asserts that for
66+
orthogonal `v` and `w`, the squared norm of `v + w` is the sum of the squared
67+
norm of `v` and the squared norm of `w`.
68+
69+
The Pythagorean theorem is the [4th](literature.100-theorems.md#4) theorem on
70+
[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
71+
[100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
72+
73+
## Proof
74+
75+
```agda
76+
module _
77+
{l1 l2 : Level}
78+
(V : ℝ-Inner-Product-Space l1 l2)
79+
where
80+
81+
abstract
82+
pythagorean-theorem-ℝ-Inner-Product-Space :
83+
(v w : type-ℝ-Inner-Product-Space V) →
84+
is-orthogonal-ℝ-Inner-Product-Space V v w →
85+
squared-norm-ℝ-Inner-Product-Space V (add-ℝ-Inner-Product-Space V v w) ＝
86+
squared-norm-ℝ-Inner-Product-Space V v +ℝ
87+
squared-norm-ℝ-Inner-Product-Space V w
88+
pythagorean-theorem-ℝ-Inner-Product-Space v w v∙w=0 =
89+
let
90+
⟨_,V_⟩ = inner-product-ℝ-Inner-Product-Space V
91+
_+V_ = add-ℝ-Inner-Product-Space V
92+
in
93+
equational-reasoning
94+
⟨ v +V w ,V v +V w ⟩
95+
＝ ⟨ v ,V v ⟩ +ℝ real-ℕ 2 *ℝ ⟨ v ,V w ⟩ +ℝ ⟨ w ,V w ⟩
96+
by squared-norm-add-ℝ-Inner-Product-Space V v w
97+
＝ ⟨ v ,V v ⟩ +ℝ real-ℕ 2 *ℝ raise-ℝ l1 zero-ℝ +ℝ ⟨ w ,V w ⟩
98+
by ap-add-ℝ (ap-add-ℝ refl (ap-mul-ℝ refl v∙w=0)) refl
99+
＝ ⟨ v ,V v ⟩ +ℝ zero-ℝ +ℝ ⟨ w ,V w ⟩
100+
by
101+
ap-add-ℝ
102+
( eq-sim-ℝ
103+
( preserves-sim-left-add-ℝ _ _ _
104+
( similarity-reasoning-ℝ
105+
real-ℕ 2 *ℝ raise-ℝ l1 zero-ℝ
106+
~ℝ real-ℕ 2 *ℝ zero-ℝ
107+
by
108+
preserves-sim-left-mul-ℝ _ _ _
109+
( sim-raise-ℝ' l1 zero-ℝ)
110+
~ℝ zero-ℝ
111+
by right-zero-law-mul-ℝ _)))
112+
( refl)
113+
＝ ⟨ v ,V v ⟩ +ℝ ⟨ w ,V w ⟩
114+
by ap-add-ℝ (right-unit-law-add-ℝ _) refl
115+
116+
norm-add-orthogonal-ℝ-Inner-Product-Space :
117+
(v w : type-ℝ-Inner-Product-Space V) →
118+
is-orthogonal-ℝ-Inner-Product-Space V v w →
119+
norm-ℝ-Inner-Product-Space V (add-ℝ-Inner-Product-Space V v w) ＝
120+
real-sqrt-ℝ⁰⁺
121+
( nonnegative-squared-norm-ℝ-Inner-Product-Space V v +ℝ⁰⁺
122+
nonnegative-squared-norm-ℝ-Inner-Product-Space V w)
123+
norm-add-orthogonal-ℝ-Inner-Product-Space v w v∙w=0 =
124+
ap
125+
( real-sqrt-ℝ⁰⁺)
126+
( eq-ℝ⁰⁺ _ _
127+
( pythagorean-theorem-ℝ-Inner-Product-Space v w v∙w=0))
128+
```
129+
130+
## References
131+
132+
{{#bibliography}}

0 commit comments

Comments
 (0)