author | wenzelm |
Sat, 07 Apr 2012 16:41:59 +0200 | |
changeset 47389 | e8552cba702d |
parent 44902 | 9ba11d41cd1f |
child 50526 | 899c9c4e4a4c |
permissions | -rw-r--r-- |
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 {* Finite-Dimensional 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 |