src/HOL/Analysis/Euclidean_Space.thy
 author wenzelm Sun Sep 18 20:33:48 2016 +0200 (2016-09-18) changeset 63915 bab633745c7f parent 63627 6ddb43c6b711 child 63938 f6ce08859d4c permissions -rw-r--r--
tuned proofs;
1 (*  Title:      HOL/Analysis/Euclidean_Space.thy
2     Author:     Johannes Hölzl, TU München
3     Author:     Brian Huffman, Portland State University
4 *)
6 section \<open>Finite-Dimensional Inner Product Spaces\<close>
8 theory Euclidean_Space
9 imports
10   L2_Norm
11   "~~/src/HOL/Library/Inner_Product"
12   "~~/src/HOL/Library/Product_Vector"
13 begin
15 subsection \<open>Type class of Euclidean spaces\<close>
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"
21   assumes inner_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 syntax "_type_dimension" :: "type \<Rightarrow> nat"  ("(1DIM/(1'(_')))")
27 translations "DIM('a)" \<rightharpoonup> "CONST card (CONST Basis :: 'a set)"
28 typed_print_translation \<open>
29   [(@{const_syntax card},
30     fn ctxt => fn _ => fn [Const (@{const_syntax Basis}, Type (@{type_name set}, [T]))] =>
31       Syntax.const @{syntax_const "_type_dimension"} \$ Syntax_Phases.term_of_typ ctxt T)]
32 \<close>
34 lemma (in euclidean_space) norm_Basis[simp]: "u \<in> Basis \<Longrightarrow> norm u = 1"
35   unfolding norm_eq_sqrt_inner by (simp add: inner_Basis)
37 lemma (in euclidean_space) inner_same_Basis[simp]: "u \<in> Basis \<Longrightarrow> inner u u = 1"
40 lemma (in euclidean_space) inner_not_same_Basis: "u \<in> Basis \<Longrightarrow> v \<in> Basis \<Longrightarrow> u \<noteq> v \<Longrightarrow> inner u v = 0"
43 lemma (in euclidean_space) sgn_Basis: "u \<in> Basis \<Longrightarrow> sgn u = u"
44   unfolding sgn_div_norm by (simp add: scaleR_one)
46 lemma (in euclidean_space) Basis_zero [simp]: "0 \<notin> Basis"
47 proof
48   assume "0 \<in> Basis" thus "False"
49     using inner_Basis [of 0 0] by simp
50 qed
52 lemma (in euclidean_space) nonzero_Basis: "u \<in> Basis \<Longrightarrow> u \<noteq> 0"
53   by clarsimp
55 lemma (in euclidean_space) SOME_Basis: "(SOME i. i \<in> Basis) \<in> Basis"
56   by (metis ex_in_conv nonempty_Basis someI_ex)
58 lemma (in euclidean_space) inner_setsum_left_Basis[simp]:
59     "b \<in> Basis \<Longrightarrow> inner (\<Sum>i\<in>Basis. f i *\<^sub>R i) b = f b"
62 lemma (in euclidean_space) euclidean_eqI:
63   assumes b: "\<And>b. b \<in> Basis \<Longrightarrow> inner x b = inner y b" shows "x = y"
64 proof -
65   from b have "\<forall>b\<in>Basis. inner (x - y) b = 0"
67   then show "x = y"
69 qed
71 lemma (in euclidean_space) euclidean_eq_iff:
72   "x = y \<longleftrightarrow> (\<forall>b\<in>Basis. inner x b = inner y b)"
73   by (auto intro: euclidean_eqI)
75 lemma (in euclidean_space) euclidean_representation_setsum:
76   "(\<Sum>i\<in>Basis. f i *\<^sub>R i) = b \<longleftrightarrow> (\<forall>i\<in>Basis. f i = inner b i)"
77   by (subst euclidean_eq_iff) simp
79 lemma (in euclidean_space) euclidean_representation_setsum':
80   "b = (\<Sum>i\<in>Basis. f i *\<^sub>R i) \<longleftrightarrow> (\<forall>i\<in>Basis. f i = inner b i)"
81   by (auto simp add: euclidean_representation_setsum[symmetric])
83 lemma (in euclidean_space) euclidean_representation: "(\<Sum>b\<in>Basis. inner x b *\<^sub>R b) = x"
84   unfolding euclidean_representation_setsum by simp
86 lemma (in euclidean_space) choice_Basis_iff:
87   fixes P :: "'a \<Rightarrow> real \<Rightarrow> bool"
88   shows "(\<forall>i\<in>Basis. \<exists>x. P i x) \<longleftrightarrow> (\<exists>x. \<forall>i\<in>Basis. P i (inner x i))"
89   unfolding bchoice_iff
90 proof safe
91   fix f assume "\<forall>i\<in>Basis. P i (f i)"
92   then show "\<exists>x. \<forall>i\<in>Basis. P i (inner x i)"
93     by (auto intro!: exI[of _ "\<Sum>i\<in>Basis. f i *\<^sub>R i"])
94 qed auto
96 lemma (in euclidean_space) euclidean_representation_setsum_fun:
97     "(\<lambda>x. \<Sum>b\<in>Basis. inner (f x) b *\<^sub>R b) = f"
98   by (rule ext) (simp add: euclidean_representation_setsum)
100 lemma euclidean_isCont:
101   assumes "\<And>b. b \<in> Basis \<Longrightarrow> isCont (\<lambda>x. (inner (f x) b) *\<^sub>R b) x"
102     shows "isCont f x"
103   apply (subst euclidean_representation_setsum_fun [symmetric])
104   apply (rule isCont_setsum)
105   apply (blast intro: assms)
106   done
108 lemma DIM_positive: "0 < DIM('a::euclidean_space)"
111 lemma DIM_ge_Suc0 [iff]: "Suc 0 \<le> card Basis"
112   by (meson DIM_positive Suc_leI)
115 lemma setsum_inner_Basis_scaleR [simp]:
116   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_vector"
117   assumes "b \<in> Basis" shows "(\<Sum>i\<in>Basis. (inner i b) *\<^sub>R f i) = f b"
121 lemma setsum_inner_Basis_eq [simp]:
122   assumes "b \<in> Basis" shows "(\<Sum>i\<in>Basis. (inner i b) * f i) = f b"
126 subsection \<open>Subclass relationships\<close>
128 instance euclidean_space \<subseteq> perfect_space
129 proof
130   fix x :: 'a show "\<not> open {x}"
131   proof
132     assume "open {x}"
133     then obtain e where "0 < e" and e: "\<forall>y. dist y x < e \<longrightarrow> y = x"
134       unfolding open_dist by fast
135     define y where "y = x + scaleR (e/2) (SOME b. b \<in> Basis)"
136     have [simp]: "(SOME b. b \<in> Basis) \<in> Basis"
137       by (rule someI_ex) (auto simp: ex_in_conv)
138     from \<open>0 < e\<close> have "y \<noteq> x"
139       unfolding y_def by (auto intro!: nonzero_Basis)
140     from \<open>0 < e\<close> have "dist y x < e"
141       unfolding y_def by (simp add: dist_norm)
142     from \<open>y \<noteq> x\<close> and \<open>dist y x < e\<close> show "False"
143       using e by simp
144   qed
145 qed
147 subsection \<open>Class instances\<close>
149 subsubsection \<open>Type @{typ real}\<close>
151 instantiation real :: euclidean_space
152 begin
154 definition
155   [simp]: "Basis = {1::real}"
157 instance
158   by standard auto
160 end
162 lemma DIM_real[simp]: "DIM(real) = 1"
163   by simp
165 subsubsection \<open>Type @{typ complex}\<close>
167 instantiation complex :: euclidean_space
168 begin
170 definition Basis_complex_def: "Basis = {1, \<i>}"
172 instance
173   by standard (auto simp add: Basis_complex_def intro: complex_eqI split: if_split_asm)
175 end
177 lemma DIM_complex[simp]: "DIM(complex) = 2"
178   unfolding Basis_complex_def by simp
180 subsubsection \<open>Type @{typ "'a \<times> 'b"}\<close>
182 instantiation prod :: (euclidean_space, euclidean_space) euclidean_space
183 begin
185 definition
186   "Basis = (\<lambda>u. (u, 0)) ` Basis \<union> (\<lambda>v. (0, v)) ` Basis"
188 lemma setsum_Basis_prod_eq:
189   fixes f::"('a*'b)\<Rightarrow>('a*'b)"
190   shows "setsum f Basis = setsum (\<lambda>i. f (i, 0)) Basis + setsum (\<lambda>i. f (0, i)) Basis"
191 proof -
192   have "inj_on (\<lambda>u. (u::'a, 0::'b)) Basis" "inj_on (\<lambda>u. (0::'a, u::'b)) Basis"
193     by (auto intro!: inj_onI Pair_inject)
194   thus ?thesis
195     unfolding Basis_prod_def
196     by (subst setsum.union_disjoint) (auto simp: Basis_prod_def setsum.reindex)
197 qed
199 instance proof
200   show "(Basis :: ('a \<times> 'b) set) \<noteq> {}"
201     unfolding Basis_prod_def by simp
202 next
203   show "finite (Basis :: ('a \<times> 'b) set)"
204     unfolding Basis_prod_def by simp
205 next
206   fix u v :: "'a \<times> 'b"
207   assume "u \<in> Basis" and "v \<in> Basis"
208   thus "inner u v = (if u = v then 1 else 0)"
209     unfolding Basis_prod_def inner_prod_def
210     by (auto simp add: inner_Basis split: if_split_asm)
211 next
212   fix x :: "'a \<times> 'b"
213   show "(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> x = 0"
214     unfolding Basis_prod_def ball_Un ball_simps
215     by (simp add: inner_prod_def prod_eq_iff euclidean_all_zero_iff)
216 qed
218 lemma DIM_prod[simp]: "DIM('a \<times> 'b) = DIM('a) + DIM('b)"
219   unfolding Basis_prod_def
220   by (subst card_Un_disjoint) (auto intro!: card_image arg_cong2[where f="op +"] inj_onI)
222 end
224 end