author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 44902  9ba11d41cd1f 
child 50526  899c9c4e4a4c 
permissions  rwrr 
41959  1 
(* Title: HOL/Multivariate_Analysis/Euclidean_Space.thy 
44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset

2 
Author: Johannes Hölzl, TU München 
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset

3 
Author: Brian Huffman, Portland State University 
33175  4 
*) 
5 

44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset

6 
header {* FiniteDimensional Inner Product Spaces *} 
33175  7 

8 
theory Euclidean_Space 

9 
imports 

44628
bd17b7543af1
move lemmas from Topology_Euclidean_Space to Euclidean_Space
huffman
parents:
44571
diff
changeset

10 
L2_Norm 
41413
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
40786
diff
changeset

11 
"~~/src/HOL/Library/Inner_Product" 
44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset

12 
"~~/src/HOL/Library/Product_Vector" 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

13 
begin 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

14 

44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset

15 
subsection {* Type class of Euclidean spaces *} 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

16 

44129  17 
class euclidean_space = real_inner + 
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

18 
fixes Basis :: "'a set" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

19 
assumes nonempty_Basis [simp]: "Basis \<noteq> {}" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

20 
assumes finite_Basis [simp]: "finite Basis" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

21 
assumes inner_Basis: 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

22 
"\<lbrakk>u \<in> Basis; v \<in> Basis\<rbrakk> \<Longrightarrow> inner u v = (if u = v then 1 else 0)" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

23 
assumes euclidean_all_zero_iff: 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

24 
"(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> (x = 0)" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

25 

d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

26 
 "FIXME: make this a separate definition" 
44129  27 
fixes dimension :: "'a itself \<Rightarrow> nat" 
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

28 
assumes dimension_def: "dimension TYPE('a) = card Basis" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

29 

d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

30 
 "FIXME: eventually basis function can be removed" 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

31 
fixes basis :: "nat \<Rightarrow> 'a" 
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

32 
assumes image_basis: "basis ` {..<dimension TYPE('a)} = Basis" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

33 
assumes basis_finite: "basis ` {dimension TYPE('a)..} = {0}" 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

34 

44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

35 
syntax "_type_dimension" :: "type => nat" ("(1DIM/(1'(_')))") 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

36 

37646  37 
translations "DIM('t)" == "CONST dimension (TYPE('t))" 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

38 

44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

39 
lemma (in euclidean_space) norm_Basis: "u \<in> Basis \<Longrightarrow> norm u = 1" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

40 
unfolding norm_eq_sqrt_inner by (simp add: inner_Basis) 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

41 

d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

42 
lemma (in euclidean_space) sgn_Basis: "u \<in> Basis \<Longrightarrow> sgn u = u" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

43 
unfolding sgn_div_norm by (simp add: norm_Basis scaleR_one) 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

44 

d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

45 
lemma (in euclidean_space) Basis_zero [simp]: "0 \<notin> Basis" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

46 
proof 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

47 
assume "0 \<in> Basis" thus "False" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

48 
using inner_Basis [of 0 0] by simp 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

49 
qed 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

50 

d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

51 
lemma (in euclidean_space) nonzero_Basis: "u \<in> Basis \<Longrightarrow> u \<noteq> 0" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

52 
by clarsimp 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

53 

d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

54 
text {* Lemmas related to @{text basis} function. *} 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

55 

d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

56 
lemma (in euclidean_space) euclidean_all_zero: 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

57 
"(\<forall>i<DIM('a). inner (basis i) x = 0) \<longleftrightarrow> (x = 0)" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

58 
using euclidean_all_zero_iff [of x, folded image_basis] 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

59 
unfolding ball_simps by (simp add: Ball_def inner_commute) 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

60 

d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

61 
lemma (in euclidean_space) basis_zero [simp]: 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

62 
"DIM('a) \<le> i \<Longrightarrow> basis i = 0" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

63 
using basis_finite by auto 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

64 

d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

65 
lemma (in euclidean_space) DIM_positive [intro]: "0 < DIM('a)" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

66 
unfolding dimension_def by (simp add: card_gt_0_iff) 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

67 

d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

68 
lemma (in euclidean_space) basis_inj [simp, intro]: "inj_on basis {..<DIM('a)}" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

69 
by (simp add: inj_on_iff_eq_card image_basis dimension_def [symmetric]) 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

70 

d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

71 
lemma (in euclidean_space) basis_in_Basis [simp]: 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

72 
"basis i \<in> Basis \<longleftrightarrow> i < DIM('a)" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

73 
by (cases "i < DIM('a)", simp add: image_basis [symmetric], simp) 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

74 

d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

75 
lemma (in euclidean_space) Basis_elim: 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

76 
assumes "u \<in> Basis" obtains i where "i < DIM('a)" and "u = basis i" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

77 
using assms unfolding image_basis [symmetric] by fast 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

78 

d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

79 
lemma (in euclidean_space) basis_orthonormal: 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

80 
"\<forall>i<DIM('a). \<forall>j<DIM('a). 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

81 
inner (basis i) (basis j) = (if i = j then 1 else 0)" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

82 
apply clarify 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

83 
apply (simp add: inner_Basis) 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

84 
apply (simp add: basis_inj [unfolded inj_on_def]) 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

85 
done 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

86 

44129  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))") 

90 
case False 

91 
hence "inner (basis i) (basis j) = 0" by auto 

92 
thus ?thesis using False by auto 

93 
next 

94 
case True thus ?thesis using basis_orthonormal by auto 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

95 
qed 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

96 

44129  97 
lemma (in euclidean_space) basis_eq_0_iff [simp]: 
98 
"basis i = 0 \<longleftrightarrow> DIM('a) \<le> i" 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

99 
proof  
44129  100 
have "inner (basis i) (basis i) = 0 \<longleftrightarrow> DIM('a) \<le> i" 
101 
by (simp add: dot_basis) 

102 
thus ?thesis by simp 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

103 
qed 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

104 

44129  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 

108 

109 
lemma (in euclidean_space) basis_neq_0 [intro]: 

110 
assumes "i<DIM('a)" shows "(basis i) \<noteq> 0" 

111 
using assms by simp 

112 

113 
subsubsection {* Projecting components *} 

114 

115 
definition (in euclidean_space) euclidean_component (infixl "$$" 90) 

116 
where "x $$ i = inner (basis i) x" 

117 

118 
lemma bounded_linear_euclidean_component: 

119 
"bounded_linear (\<lambda>x. euclidean_component x i)" 

120 
unfolding euclidean_component_def 

44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44233
diff
changeset

121 
by (rule bounded_linear_inner_right) 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44233
diff
changeset

122 

f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44233
diff
changeset

123 
lemmas tendsto_euclidean_component [tendsto_intros] = 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44233
diff
changeset

124 
bounded_linear.tendsto [OF bounded_linear_euclidean_component] 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44233
diff
changeset

125 

f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44233
diff
changeset

126 
lemmas isCont_euclidean_component [simp] = 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44233
diff
changeset

127 
bounded_linear.isCont [OF bounded_linear_euclidean_component] 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44233
diff
changeset

128 

44286
8766839efb1b
declare euclidean_component_zero[simp] at the point it is proved
huffman
parents:
44282
diff
changeset

129 
lemma euclidean_component_zero [simp]: "0 $$ i = 0" 
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44233
diff
changeset

130 
unfolding euclidean_component_def by (rule inner_zero_right) 
44129  131 

44457
d366fa5551ef
declare euclidean_simps [simp] at the point they are proved;
huffman
parents:
44286
diff
changeset

132 
lemma euclidean_component_add [simp]: "(x + y) $$ i = x $$ i + y $$ i" 
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44233
diff
changeset

133 
unfolding euclidean_component_def by (rule inner_add_right) 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44233
diff
changeset

134 

44457
d366fa5551ef
declare euclidean_simps [simp] at the point they are proved;
huffman
parents:
44286
diff
changeset

135 
lemma euclidean_component_diff [simp]: "(x  y) $$ i = x $$ i  y $$ i" 
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44233
diff
changeset

136 
unfolding euclidean_component_def by (rule inner_diff_right) 
44129  137 

44457
d366fa5551ef
declare euclidean_simps [simp] at the point they are proved;
huffman
parents:
44286
diff
changeset

138 
lemma euclidean_component_minus [simp]: "( x) $$ i =  (x $$ i)" 
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44233
diff
changeset

139 
unfolding euclidean_component_def by (rule inner_minus_right) 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44233
diff
changeset

140 

44457
d366fa5551ef
declare euclidean_simps [simp] at the point they are proved;
huffman
parents:
44286
diff
changeset

141 
lemma euclidean_component_scaleR [simp]: "(scaleR a x) $$ i = a * (x $$ i)" 
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44233
diff
changeset

142 
unfolding euclidean_component_def by (rule inner_scaleR_right) 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44233
diff
changeset

143 

44457
d366fa5551ef
declare euclidean_simps [simp] at the point they are proved;
huffman
parents:
44286
diff
changeset

144 
lemma euclidean_component_setsum [simp]: "(\<Sum>x\<in>A. f x) $$ i = (\<Sum>x\<in>A. f x $$ i)" 
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44233
diff
changeset

145 
unfolding euclidean_component_def by (rule inner_setsum_right) 
44233  146 

44129  147 
lemma euclidean_eqI: 
148 
fixes x y :: "'a::euclidean_space" 

149 
assumes "\<And>i. i < DIM('a) \<Longrightarrow> x $$ i = y $$ i" shows "x = y" 

150 
proof  

151 
from assms have "\<forall>i<DIM('a). (x  y) $$ i = 0" 

44531
1d477a2b1572
replace some continuous_on lemmas with more general versions
huffman
parents:
44457
diff
changeset

152 
by simp 
44129  153 
then show "x = y" 
154 
unfolding euclidean_component_def euclidean_all_zero by simp 

155 
qed 

156 

157 
lemma euclidean_eq: 

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) 

161 

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 

165 

166 
lemma (in euclidean_space) basis_at_neq_0 [intro]: 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

167 
"i < DIM('a) \<Longrightarrow> basis i $$ i \<noteq> 0" 
44129  168 
by simp 
169 

170 
lemma (in euclidean_space) euclidean_component_ge [simp]: 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

171 
assumes "i \<ge> DIM('a)" shows "x $$ i = 0" 
44129  172 
unfolding euclidean_component_def basis_zero[OF assms] by simp 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

173 

44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

174 
lemmas euclidean_simps = 
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44233
diff
changeset

175 
euclidean_component_add 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44233
diff
changeset

176 
euclidean_component_diff 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44233
diff
changeset

177 
euclidean_component_scaleR 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44233
diff
changeset

178 
euclidean_component_minus 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44233
diff
changeset

179 
euclidean_component_setsum 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

180 
basis_component 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

181 

44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

182 
lemma euclidean_representation: 
44129  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: if_distrib setsum_delta cong: if_cong) 

187 
done 

188 

189 
subsubsection {* Binder notation for vectors *} 

190 

191 
definition (in euclidean_space) Chi (binder "\<chi>\<chi> " 10) where 

192 
"(\<chi>\<chi> i. f i) = (\<Sum>i<DIM('a). f i *\<^sub>R basis i)" 

193 

194 
lemma euclidean_lambda_beta [simp]: 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

195 
"((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ j = (if j < DIM('a) then f j else 0)" 
44457
d366fa5551ef
declare euclidean_simps [simp] at the point they are proved;
huffman
parents:
44286
diff
changeset

196 
by (auto simp: Chi_def if_distrib setsum_cases intro!: setsum_cong) 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

197 

44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

198 
lemma euclidean_lambda_beta': 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

199 
"j < DIM('a) \<Longrightarrow> ((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ j = f j" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

200 
by simp 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

201 

44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

202 
lemma euclidean_lambda_beta'':"(\<forall>j < DIM('a::euclidean_space). P j (((\<chi>\<chi> i. f i)::'a) $$ j)) \<longleftrightarrow> 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

203 
(\<forall>j < DIM('a::euclidean_space). P j (f j))" by auto 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

204 

44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

205 
lemma euclidean_beta_reduce[simp]: 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

206 
"(\<chi>\<chi> i. x $$ i) = (x::'a::euclidean_space)" 
44129  207 
by (simp add: euclidean_eq) 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

208 

44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

209 
lemma euclidean_lambda_beta_0[simp]: 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

210 
"((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ 0 = f 0" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

211 
by (simp add: DIM_positive) 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

212 

44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

213 
lemma euclidean_inner: 
44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset

214 
"inner x (y::'a) = (\<Sum>i<DIM('a::euclidean_space). (x $$ i) * (y $$ i))" 
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset

215 
by (subst (1 2) euclidean_representation, 
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44233
diff
changeset

216 
simp add: inner_setsum_left inner_setsum_right 
44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset

217 
dot_basis if_distrib setsum_cases mult_commute) 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

218 

44628
bd17b7543af1
move lemmas from Topology_Euclidean_Space to Euclidean_Space
huffman
parents:
44571
diff
changeset

219 
lemma euclidean_dist_l2: 
bd17b7543af1
move lemmas from Topology_Euclidean_Space to Euclidean_Space
huffman
parents:
44571
diff
changeset

220 
fixes x y :: "'a::euclidean_space" 
bd17b7543af1
move lemmas from Topology_Euclidean_Space to Euclidean_Space
huffman
parents:
44571
diff
changeset

221 
shows "dist x y = setL2 (\<lambda>i. dist (x $$ i) (y $$ i)) {..<DIM('a)}" 
bd17b7543af1
move lemmas from Topology_Euclidean_Space to Euclidean_Space
huffman
parents:
44571
diff
changeset

222 
unfolding dist_norm norm_eq_sqrt_inner setL2_def 
bd17b7543af1
move lemmas from Topology_Euclidean_Space to Euclidean_Space
huffman
parents:
44571
diff
changeset

223 
by (simp add: euclidean_inner power2_eq_square) 
bd17b7543af1
move lemmas from Topology_Euclidean_Space to Euclidean_Space
huffman
parents:
44571
diff
changeset

224 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

225 
lemma component_le_norm: "\<bar>x$$i\<bar> \<le> norm (x::'a::euclidean_space)" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

226 
unfolding euclidean_component_def 
44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset

227 
by (rule order_trans [OF Cauchy_Schwarz_ineq2]) simp 
33175  228 

44628
bd17b7543af1
move lemmas from Topology_Euclidean_Space to Euclidean_Space
huffman
parents:
44571
diff
changeset

229 
lemma dist_nth_le: "dist (x $$ i) (y $$ i) \<le> dist x (y::'a::euclidean_space)" 
bd17b7543af1
move lemmas from Topology_Euclidean_Space to Euclidean_Space
huffman
parents:
44571
diff
changeset

230 
unfolding euclidean_dist_l2 [where 'a='a] 
bd17b7543af1
move lemmas from Topology_Euclidean_Space to Euclidean_Space
huffman
parents:
44571
diff
changeset

231 
by (cases "i < DIM('a)", rule member_le_setL2, auto) 
bd17b7543af1
move lemmas from Topology_Euclidean_Space to Euclidean_Space
huffman
parents:
44571
diff
changeset

232 

44571  233 
subsection {* Subclass relationships *} 
234 

235 
instance euclidean_space \<subseteq> perfect_space 

236 
proof 

237 
fix x :: 'a show "\<not> open {x}" 

238 
proof 

239 
assume "open {x}" 

240 
then obtain e where "0 < e" and e: "\<forall>y. dist y x < e \<longrightarrow> y = x" 

241 
unfolding open_dist by fast 

242 
def y \<equiv> "x + scaleR (e/2) (sgn (basis 0))" 

243 
from `0 < e` have "y \<noteq> x" 

244 
unfolding y_def by (simp add: sgn_zero_iff DIM_positive) 

245 
from `0 < e` have "dist y x < e" 

246 
unfolding y_def by (simp add: dist_norm norm_sgn) 

247 
from `y \<noteq> x` and `dist y x < e` show "False" 

248 
using e by simp 

249 
qed 

250 
qed 

251 

44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset

252 
subsection {* Class instances *} 
33175  253 

44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset

254 
subsubsection {* Type @{typ real} *} 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

255 

44129  256 
instantiation real :: euclidean_space 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

257 
begin 
44129  258 

259 
definition 

44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

260 
"Basis = {1::real}" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

261 

d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

262 
definition 
44129  263 
"dimension (t::real itself) = 1" 
264 

265 
definition [simp]: 

266 
"basis i = (if i = 0 then 1 else (0::real))" 

267 

268 
lemma DIM_real [simp]: "DIM(real) = 1" 

269 
by (rule dimension_real_def) 

270 

271 
instance 

44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

272 
by default (auto simp add: Basis_real_def) 
44129  273 

274 
end 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

275 

44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset

276 
subsubsection {* Type @{typ complex} *} 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

277 

44129  278 
instantiation complex :: euclidean_space 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

279 
begin 
44129  280 

44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

281 
definition Basis_complex_def: 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

282 
"Basis = {1, ii}" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

283 

44129  284 
definition 
285 
"dimension (t::complex itself) = 2" 

286 

287 
definition 

288 
"basis i = (if i = 0 then 1 else if i = 1 then ii else 0)" 

289 

44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

290 
instance 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

291 
by default (auto simp add: Basis_complex_def dimension_complex_def 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

292 
basis_complex_def intro: complex_eqI split: split_if_asm) 
44129  293 

294 
end 

295 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

296 
lemma DIM_complex[simp]: "DIM(complex) = 2" 
44129  297 
by (rule dimension_complex_def) 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

298 

44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset

299 
subsubsection {* Type @{typ "'a \<times> 'b"} *} 
38656  300 

44129  301 
instantiation prod :: (euclidean_space, euclidean_space) euclidean_space 
38656  302 
begin 
303 

44129  304 
definition 
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

305 
"Basis = (\<lambda>u. (u, 0)) ` Basis \<union> (\<lambda>v. (0, v)) ` Basis" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

306 

d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

307 
definition 
44129  308 
"dimension (t::('a \<times> 'b) itself) = DIM('a) + DIM('b)" 
309 

310 
definition 

311 
"basis i = (if i < DIM('a) then (basis i, 0) else (0, basis (i  DIM('a))))" 

312 

313 
instance proof 

44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

314 
show "(Basis :: ('a \<times> 'b) set) \<noteq> {}" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

315 
unfolding Basis_prod_def by simp 
44129  316 
next 
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

317 
show "finite (Basis :: ('a \<times> 'b) set)" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

318 
unfolding Basis_prod_def by simp 
44129  319 
next 
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

320 
fix u v :: "'a \<times> 'b" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

321 
assume "u \<in> Basis" and "v \<in> Basis" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

322 
thus "inner u v = (if u = v then 1 else 0)" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

323 
unfolding Basis_prod_def inner_prod_def 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

324 
by (auto simp add: inner_Basis split: split_if_asm) 
44129  325 
next 
326 
fix x :: "'a \<times> 'b" 

44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

327 
show "(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> x = 0" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

328 
unfolding Basis_prod_def ball_Un ball_simps 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

329 
by (simp add: inner_prod_def prod_eq_iff euclidean_all_zero_iff) 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

330 
next 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

331 
show "DIM('a \<times> 'b) = card (Basis :: ('a \<times> 'b) set)" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

332 
unfolding dimension_prod_def Basis_prod_def 
44215  333 
by (simp add: card_Un_disjoint disjoint_iff_not_equal 
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

334 
card_image inj_on_def dimension_def) 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

335 
next 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

336 
show "basis ` {..<DIM('a \<times> 'b)} = (Basis :: ('a \<times> 'b) set)" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

337 
by (auto simp add: Basis_prod_def dimension_prod_def basis_prod_def 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

338 
image_def elim!: Basis_elim) 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

339 
next 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

340 
show "basis ` {DIM('a \<times> 'b)..} = {0::('a \<times> 'b)}" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset

341 
by (auto simp add: dimension_prod_def basis_prod_def prod_eq_iff image_def) 
38656  342 
qed 
44129  343 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset

344 
end 
38656  345 

346 
end 