1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
|
Require Import
MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders.
(** Scalar multiplication function class *)
Class ScalarMult K V := scalar_mult: K → V → V.
#[global]
Instance: Params (@scalar_mult) 3 := {}.
Infix "·" := scalar_mult (at level 50) : mc_scope.
Notation "(·)" := scalar_mult (only parsing) : mc_scope.
Notation "( x ·)" := (scalar_mult x) (only parsing) : mc_scope.
Notation "(· x )" := (λ y, y · x) (only parsing) : mc_scope.
(** The inproduct function class *)
Class Inproduct K V := inprod : V → V → K.
#[global]
Instance: Params (@inprod) 3 := {}.
Notation "(⟨⟩)" := (inprod) (only parsing) : mc_scope.
Notation "⟨ u , v ⟩" := (inprod u v) (at level 51) : mc_scope.
Notation "⟨ u , ⟩" := (λ v, ⟨u,v⟩) (at level 50, only parsing) : mc_scope.
Notation "⟨ , v ⟩" := (λ u, ⟨u,v⟩) (at level 50, only parsing) : mc_scope.
Notation "x ⊥ y" := (⟨x,y⟩ = 0) (at level 70) : mc_scope.
(** The norm function class *)
Class Norm K V := norm : V → K.
#[global]
Instance: Params (@norm) 2 := {}.
Notation "∥ L ∥" := (norm L) (at level 50) : mc_scope.
Notation "∥·∥" := norm (only parsing) : mc_scope.
(** Let [M] be an R-Module. *)
Class Module (R M : Type)
{Re Rplus Rmult Rzero Rone Rnegate}
{Me Mop Munit Mnegate}
{sm : ScalarMult R M}
:=
{ lm_ring :: @Ring R Re Rplus Rmult Rzero Rone Rnegate
; lm_group :: @AbGroup M Me Mop Munit Mnegate
; lm_distr_l :: LeftHeteroDistribute (·) (&) (&)
; lm_distr_r :: RightHeteroDistribute (·) (+) (&)
; lm_assoc :: HeteroAssociative (·) (·) (·) (.*.)
; lm_identity :: LeftIdentity (·) 1
; scalar_mult_proper :: Proper ((=) ==> (=) ==> (=)) sm
}.
(* TODO K is commutative, so derive right module laws? *)
(** A module with a seminorm. *)
Class Seminormed
{R Re Rplus Rmult Rzero Rone Rnegate Rle Rlt Rapart}
{M Me Mop Munit Mnegate Smult}
`{!Abs R} (n : Norm R M)
:=
(* We have a module *)
{ snm_module :: @Module R M Re Rplus Rmult Rzero Rone Rnegate
Me Mop Munit Mnegate Smult
; snm_order :: @FullPseudoSemiRingOrder R Re Rapart Rplus Rmult Rzero Rone Rle Rlt
(* With respect to which our norm preserves the following: *)
; snm_scale : ∀ a v, ∥a · v∥ = (abs a) * ∥v∥ (* positive homgeneity *)
; snm_triangle : ∀ u v, ∥u & v∥ ≤ ∥u∥ + ∥v∥ (* triangle inequality *)
}.
(** [K] is the field of scalars, [V] the abelian group of vectors,
and together with a scalar multiplication operation, they satisfy
the Module laws.
*)
Class VectorSpace (K V : Type)
{Ke Kplus Kmult Kzero Kone Knegate Krecip} (* scalar operations *)
{Ve Vop Vunit Vnegate} (* vector operations *)
{sm : ScalarMult K V}
:=
{ vs_field :: @DecField K Ke Kplus Kmult Kzero Kone Knegate Krecip
; vs_abgroup :: @AbGroup V Ve Vop Vunit Vnegate
; vs_module :: @Module K V Ke Kplus Kmult Kzero Kone Knegate
Ve Vop Vunit Vnegate sm
}.
(** Given some vector space V over a ordered field K,
we define the inner product space
*)
Class InnerProductSpace (K V : Type)
{Ke Kplus Kmult Kzero Kone Knegate Krecip} (* scalar operations *)
{Ve Vop Vunit Vnegate} (* vector operations *)
{sm : ScalarMult K V} {inp: Inproduct K V} {Kle: Le K}
:=
{ in_vectorspace :: @VectorSpace K V Ke Kplus Kmult Kzero Kone Knegate
Krecip Ve Vop Vunit Vnegate sm
; in_srorder :: SemiRingOrder Kle
; in_comm :: Commutative inprod
; in_linear_l : ∀ a u v, ⟨a·u,v⟩ = a*⟨u,v⟩
; in_nonneg :: ∀ v, PropHolds (0 ≤ ⟨v,v⟩) (* TODO Le to strong? *)
; in_mon_unit_zero :: ∀ v, 0 = ⟨v,v⟩ <-> v = mon_unit
; inprod_proper :: Proper ((=) ==> (=) ==> (=)) (⟨⟩)
}.
(* TODO complex conjugate?
Section proof_in_linear_r.
Context `{InnerProductSpace}.
Lemma in_linear_r a u v : ⟨u,a·v⟩ = a*⟨u,v⟩.
Proof. rewrite !(commutativity u). apply in_linear_l. Qed.
End proof_in_linear_r.
*)
(* This is probably a bad idea? (because ∣ ≠ |)
Notation "∣ a ∣" := (abs a).
*)
Class SemiNormedSpace (K V : Type)
`{a:Abs K} `{n : @Norm K V} (* scalar and vector norms *)
{Ke Kplus Kmult Kzero Kone Knegate Krecip} (* scalar operations *)
{Ve Vop Vunit Vnegate} (* vector operations *)
{sm : ScalarMult K V}
:=
{ sn_vectorspace :: @VectorSpace K V Ke Kplus Kmult Kzero Kone Knegate
Krecip Ve Vop Vunit Vnegate sm
; sn_nonneg : ∀ v, 0 ≤ ∥v∥ (* non-negativity *)
; sn_scale : ∀ a v, ∥a · v∥ = (abs a) * ∥v∥ (* positive homgeneity *)
; sn_triangle : ∀ u v, ∥u & v∥ ≤ ∥u∥ + ∥v∥ (* triangle inequality *)
}.
(* For normed spaces:
n_separates : ∀ (v:V), ∥v∥ = 0 ↔ v = unit
*)
(* - Induced metric: d x y := ∥ x - y ∥
- Induced norm. If the metric is
1). translation invariant: d x y = d (x + a) (y + a)
2). and homogeneous: d (α * x) (α * y) = ∣α∣ * (d x y)
then we can define the norm as:
∥ x ∥ := d 0 x
- Same for seminorm
*)
|
