1 (* Title: HOL/Multivariate_Analysis/Euclidean_Space.thy
2 Author: Johannes Hölzl, TU München
3 Author: Brian Huffman, Portland State University
6 header {* Finite-Dimensional Inner Product Spaces *}
11 "~~/src/HOL/Library/Inner_Product"
12 "~~/src/HOL/Library/Product_Vector"
15 subsection {* Type class of Euclidean spaces *}
17 class euclidean_space = real_inner +
18 fixes Basis :: "'a set"
19 assumes nonempty_Basis [simp]: "Basis \<noteq> {}"
20 assumes finite_Basis [simp]: "finite Basis"
22 "\<lbrakk>u \<in> Basis; v \<in> Basis\<rbrakk> \<Longrightarrow> inner u v = (if u = v then 1 else 0)"
23 assumes euclidean_all_zero_iff:
24 "(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> (x = 0)"
26 -- "FIXME: make this a separate definition"
27 fixes dimension :: "'a itself \<Rightarrow> nat"
28 assumes dimension_def: "dimension TYPE('a) = card Basis"
30 -- "FIXME: eventually basis function can be removed"
31 fixes basis :: "nat \<Rightarrow> 'a"
32 assumes image_basis: "basis ` {..<dimension TYPE('a)} = Basis"
33 assumes basis_finite: "basis ` {dimension TYPE('a)..} = {0}"
35 syntax "_type_dimension" :: "type => nat" ("(1DIM/(1'(_')))")
37 translations "DIM('t)" == "CONST dimension (TYPE('t))"
39 lemma (in euclidean_space) norm_Basis: "u \<in> Basis \<Longrightarrow> norm u = 1"
40 unfolding norm_eq_sqrt_inner by (simp add: inner_Basis)
42 lemma (in euclidean_space) sgn_Basis: "u \<in> Basis \<Longrightarrow> sgn u = u"
43 unfolding sgn_div_norm by (simp add: norm_Basis scaleR_one)
45 lemma (in euclidean_space) Basis_zero [simp]: "0 \<notin> Basis"
47 assume "0 \<in> Basis" thus "False"
48 using inner_Basis [of 0 0] by simp
51 lemma (in euclidean_space) nonzero_Basis: "u \<in> Basis \<Longrightarrow> u \<noteq> 0"
54 text {* Lemmas related to @{text basis} function. *}
56 lemma (in euclidean_space) euclidean_all_zero:
57 "(\<forall>i<DIM('a). inner (basis i) x = 0) \<longleftrightarrow> (x = 0)"
58 using euclidean_all_zero_iff [of x, folded image_basis]
59 unfolding ball_simps by (simp add: Ball_def inner_commute)
61 lemma (in euclidean_space) basis_zero [simp]:
62 "DIM('a) \<le> i \<Longrightarrow> basis i = 0"
63 using basis_finite by auto
65 lemma (in euclidean_space) DIM_positive [intro]: "0 < DIM('a)"
66 unfolding dimension_def by (simp add: card_gt_0_iff)
68 lemma (in euclidean_space) basis_inj [simp, intro]: "inj_on basis {..<DIM('a)}"
69 by (simp add: inj_on_iff_eq_card image_basis dimension_def [symmetric])
71 lemma (in euclidean_space) basis_in_Basis [simp]:
72 "basis i \<in> Basis \<longleftrightarrow> i < DIM('a)"
73 by (cases "i < DIM('a)", simp add: image_basis [symmetric], simp)
75 lemma (in euclidean_space) Basis_elim:
76 assumes "u \<in> Basis" obtains i where "i < DIM('a)" and "u = basis i"
77 using assms unfolding image_basis [symmetric] by fast
79 lemma (in euclidean_space) basis_orthonormal:
80 "\<forall>i<DIM('a). \<forall>j<DIM('a).
81 inner (basis i) (basis j) = (if i = j then 1 else 0)"
83 apply (simp add: inner_Basis)
84 apply (simp add: basis_inj [unfolded inj_on_def])
87 lemma (in euclidean_space) dot_basis:
88 "inner (basis i) (basis j) = (if i = j \<and> i < DIM('a) then 1 else 0)"
89 proof (cases "(i < DIM('a) \<and> j < DIM('a))")
91 hence "inner (basis i) (basis j) = 0" by auto
92 thus ?thesis using False by auto
94 case True thus ?thesis using basis_orthonormal by auto
97 lemma (in euclidean_space) basis_eq_0_iff [simp]:
98 "basis i = 0 \<longleftrightarrow> DIM('a) \<le> i"
100 have "inner (basis i) (basis i) = 0 \<longleftrightarrow> DIM('a) \<le> i"
101 by (simp add: dot_basis)
105 lemma (in euclidean_space) norm_basis [simp]:
106 "norm (basis i) = (if i < DIM('a) then 1 else 0)"
107 unfolding norm_eq_sqrt_inner dot_basis by simp
109 lemma (in euclidean_space) basis_neq_0 [intro]:
110 assumes "i<DIM('a)" shows "(basis i) \<noteq> 0"
113 subsubsection {* Projecting components *}
115 definition (in euclidean_space) euclidean_component (infixl "$$" 90)
116 where "x $$ i = inner (basis i) x"
118 lemma bounded_linear_euclidean_component:
119 "bounded_linear (\<lambda>x. euclidean_component x i)"
120 unfolding euclidean_component_def
121 by (rule bounded_linear_inner_right)
123 lemmas tendsto_euclidean_component [tendsto_intros] =
124 bounded_linear.tendsto [OF bounded_linear_euclidean_component]
126 lemmas isCont_euclidean_component [simp] =
127 bounded_linear.isCont [OF bounded_linear_euclidean_component]
129 lemma euclidean_component_zero [simp]: "0 $$ i = 0"
130 unfolding euclidean_component_def by (rule inner_zero_right)
132 lemma euclidean_component_add: "(x + y) $$ i = x $$ i + y $$ i"
133 unfolding euclidean_component_def by (rule inner_add_right)
135 lemma euclidean_component_diff: "(x - y) $$ i = x $$ i - y $$ i"
136 unfolding euclidean_component_def by (rule inner_diff_right)
138 lemma euclidean_component_minus: "(- x) $$ i = - (x $$ i)"
139 unfolding euclidean_component_def by (rule inner_minus_right)
141 lemma euclidean_component_scaleR: "(scaleR a x) $$ i = a * (x $$ i)"
142 unfolding euclidean_component_def by (rule inner_scaleR_right)
144 lemma euclidean_component_setsum: "(\<Sum>x\<in>A. f x) $$ i = (\<Sum>x\<in>A. f x $$ i)"
145 unfolding euclidean_component_def by (rule inner_setsum_right)
148 fixes x y :: "'a::euclidean_space"
149 assumes "\<And>i. i < DIM('a) \<Longrightarrow> x $$ i = y $$ i" shows "x = y"
151 from assms have "\<forall>i<DIM('a). (x - y) $$ i = 0"
152 by (simp add: euclidean_component_diff)
154 unfolding euclidean_component_def euclidean_all_zero by simp
158 fixes x y :: "'a::euclidean_space"
159 shows "x = y \<longleftrightarrow> (\<forall>i<DIM('a). x $$ i = y $$ i)"
160 by (auto intro: euclidean_eqI)
162 lemma (in euclidean_space) basis_component [simp]:
163 "basis i $$ j = (if i = j \<and> i < DIM('a) then 1 else 0)"
164 unfolding euclidean_component_def dot_basis by auto
166 lemma (in euclidean_space) basis_at_neq_0 [intro]:
167 "i < DIM('a) \<Longrightarrow> basis i $$ i \<noteq> 0"
170 lemma (in euclidean_space) euclidean_component_ge [simp]:
171 assumes "i \<ge> DIM('a)" shows "x $$ i = 0"
172 unfolding euclidean_component_def basis_zero[OF assms] by simp
174 lemmas euclidean_simps =
175 euclidean_component_add
176 euclidean_component_diff
177 euclidean_component_scaleR
178 euclidean_component_minus
179 euclidean_component_setsum
182 lemma euclidean_representation:
183 fixes x :: "'a::euclidean_space"
184 shows "x = (\<Sum>i<DIM('a). (x$$i) *\<^sub>R basis i)"
185 apply (rule euclidean_eqI)
186 apply (simp add: euclidean_component_setsum euclidean_component_scaleR)
187 apply (simp add: if_distrib setsum_delta cong: if_cong)
190 subsubsection {* Binder notation for vectors *}
192 definition (in euclidean_space) Chi (binder "\<chi>\<chi> " 10) where
193 "(\<chi>\<chi> i. f i) = (\<Sum>i<DIM('a). f i *\<^sub>R basis i)"
195 lemma euclidean_lambda_beta [simp]:
196 "((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ j = (if j < DIM('a) then f j else 0)"
197 by (auto simp: euclidean_component_setsum euclidean_component_scaleR
198 Chi_def if_distrib setsum_cases intro!: setsum_cong)
200 lemma euclidean_lambda_beta':
201 "j < DIM('a) \<Longrightarrow> ((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ j = f j"
204 lemma euclidean_lambda_beta'':"(\<forall>j < DIM('a::euclidean_space). P j (((\<chi>\<chi> i. f i)::'a) $$ j)) \<longleftrightarrow>
205 (\<forall>j < DIM('a::euclidean_space). P j (f j))" by auto
207 lemma euclidean_beta_reduce[simp]:
208 "(\<chi>\<chi> i. x $$ i) = (x::'a::euclidean_space)"
209 by (simp add: euclidean_eq)
211 lemma euclidean_lambda_beta_0[simp]:
212 "((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ 0 = f 0"
213 by (simp add: DIM_positive)
215 lemma euclidean_inner:
216 "inner x (y::'a) = (\<Sum>i<DIM('a::euclidean_space). (x $$ i) * (y $$ i))"
217 by (subst (1 2) euclidean_representation,
218 simp add: inner_setsum_left inner_setsum_right
219 dot_basis if_distrib setsum_cases mult_commute)
221 lemma component_le_norm: "\<bar>x$$i\<bar> \<le> norm (x::'a::euclidean_space)"
222 unfolding euclidean_component_def
223 by (rule order_trans [OF Cauchy_Schwarz_ineq2]) simp
225 subsection {* Class instances *}
227 subsubsection {* Type @{typ real} *}
229 instantiation real :: euclidean_space
236 "dimension (t::real itself) = 1"
239 "basis i = (if i = 0 then 1 else (0::real))"
241 lemma DIM_real [simp]: "DIM(real) = 1"
242 by (rule dimension_real_def)
245 by default (auto simp add: Basis_real_def)
249 subsubsection {* Type @{typ complex} *}
251 (* TODO: move these to Complex.thy/Inner_Product.thy *)
253 lemma norm_ii [simp]: "norm ii = 1"
254 unfolding i_def by simp
256 lemma complex_inner_1 [simp]: "inner 1 x = Re x"
257 unfolding inner_complex_def by simp
259 lemma complex_inner_1_right [simp]: "inner x 1 = Re x"
260 unfolding inner_complex_def by simp
262 lemma complex_inner_ii_left [simp]: "inner ii x = Im x"
263 unfolding inner_complex_def by simp
265 lemma complex_inner_ii_right [simp]: "inner x ii = Im x"
266 unfolding inner_complex_def by simp
268 instantiation complex :: euclidean_space
271 definition Basis_complex_def:
275 "dimension (t::complex itself) = 2"
278 "basis i = (if i = 0 then 1 else if i = 1 then ii else 0)"
281 by default (auto simp add: Basis_complex_def dimension_complex_def
282 basis_complex_def intro: complex_eqI split: split_if_asm)
286 lemma DIM_complex[simp]: "DIM(complex) = 2"
287 by (rule dimension_complex_def)
289 subsubsection {* Type @{typ "'a \<times> 'b"} *}
291 instantiation prod :: (euclidean_space, euclidean_space) euclidean_space
295 "Basis = (\<lambda>u. (u, 0)) ` Basis \<union> (\<lambda>v. (0, v)) ` Basis"
298 "dimension (t::('a \<times> 'b) itself) = DIM('a) + DIM('b)"
301 "basis i = (if i < DIM('a) then (basis i, 0) else (0, basis (i - DIM('a))))"
304 show "(Basis :: ('a \<times> 'b) set) \<noteq> {}"
305 unfolding Basis_prod_def by simp
307 show "finite (Basis :: ('a \<times> 'b) set)"
308 unfolding Basis_prod_def by simp
310 fix u v :: "'a \<times> 'b"
311 assume "u \<in> Basis" and "v \<in> Basis"
312 thus "inner u v = (if u = v then 1 else 0)"
313 unfolding Basis_prod_def inner_prod_def
314 by (auto simp add: inner_Basis split: split_if_asm)
316 fix x :: "'a \<times> 'b"
317 show "(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> x = 0"
318 unfolding Basis_prod_def ball_Un ball_simps
319 by (simp add: inner_prod_def prod_eq_iff euclidean_all_zero_iff)
321 show "DIM('a \<times> 'b) = card (Basis :: ('a \<times> 'b) set)"
322 unfolding dimension_prod_def Basis_prod_def
323 by (simp add: card_Un_disjoint disjoint_iff_not_equal
324 card_image inj_on_def dimension_def)
326 show "basis ` {..<DIM('a \<times> 'b)} = (Basis :: ('a \<times> 'b) set)"
327 by (auto simp add: Basis_prod_def dimension_prod_def basis_prod_def
328 image_def elim!: Basis_elim)
330 show "basis ` {DIM('a \<times> 'b)..} = {0::('a \<times> 'b)}"
331 by (auto simp add: dimension_prod_def basis_prod_def prod_eq_iff image_def)