author | haftmann |
Sat, 28 Jun 2014 09:16:42 +0200 | |
changeset 57418 | 6ab1c7cb0b8d |
parent 54781 | fe462aa28c3d |
child 58877 | 262572d90bc6 |
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 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
26 |
abbreviation dimension :: "('a::euclidean_space) itself \<Rightarrow> nat" where |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
27 |
"dimension TYPE('a) \<equiv> card (Basis :: 'a set)" |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
28 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
29 |
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
|
30 |
|
37646 | 31 |
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
|
32 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
33 |
lemma (in euclidean_space) norm_Basis[simp]: "u \<in> Basis \<Longrightarrow> norm u = 1" |
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
34 |
unfolding norm_eq_sqrt_inner by (simp add: inner_Basis) |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
35 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
36 |
lemma (in euclidean_space) inner_same_Basis[simp]: "u \<in> Basis \<Longrightarrow> inner u u = 1" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
37 |
by (simp add: inner_Basis) |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
38 |
|
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
39 |
lemma (in euclidean_space) inner_not_same_Basis: "u \<in> Basis \<Longrightarrow> v \<in> Basis \<Longrightarrow> u \<noteq> v \<Longrightarrow> inner u v = 0" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
40 |
by (simp add: inner_Basis) |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
41 |
|
44166
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" |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
43 |
unfolding sgn_div_norm by (simp add: scaleR_one) |
44166
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 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
54 |
lemma (in euclidean_space) SOME_Basis: "(SOME i. i \<in> Basis) \<in> Basis" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
55 |
by (metis ex_in_conv nonempty_Basis someI_ex) |
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
56 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
57 |
lemma (in euclidean_space) inner_setsum_left_Basis[simp]: |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
58 |
"b \<in> Basis \<Longrightarrow> inner (\<Sum>i\<in>Basis. f i *\<^sub>R i) b = f b" |
57418 | 59 |
by (simp add: inner_setsum_left inner_Basis if_distrib comm_monoid_add_class.setsum.If_cases) |
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
60 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
61 |
lemma (in euclidean_space) euclidean_eqI: |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
62 |
assumes b: "\<And>b. b \<in> Basis \<Longrightarrow> inner x b = inner y b" shows "x = y" |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
63 |
proof - |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
64 |
from b have "\<forall>b\<in>Basis. inner (x - y) b = 0" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
65 |
by (simp add: inner_diff_left) |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
66 |
then show "x = y" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
67 |
by (simp add: euclidean_all_zero_iff) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
68 |
qed |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
69 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
70 |
lemma (in euclidean_space) euclidean_eq_iff: |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
71 |
"x = y \<longleftrightarrow> (\<forall>b\<in>Basis. inner x b = inner y b)" |
44129 | 72 |
by (auto intro: euclidean_eqI) |
73 |
||
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
74 |
lemma (in euclidean_space) euclidean_representation_setsum: |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
75 |
"(\<Sum>i\<in>Basis. f i *\<^sub>R i) = b \<longleftrightarrow> (\<forall>i\<in>Basis. f i = inner b i)" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
76 |
by (subst euclidean_eq_iff) 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
|
77 |
|
54776
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
53939
diff
changeset
|
78 |
lemma (in euclidean_space) euclidean_representation_setsum': |
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
53939
diff
changeset
|
79 |
"b = (\<Sum>i\<in>Basis. f i *\<^sub>R i) \<longleftrightarrow> (\<forall>i\<in>Basis. f i = inner b i)" |
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
53939
diff
changeset
|
80 |
by (auto simp add: euclidean_representation_setsum[symmetric]) |
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
53939
diff
changeset
|
81 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
82 |
lemma (in euclidean_space) euclidean_representation: "(\<Sum>b\<in>Basis. inner x b *\<^sub>R b) = x" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
83 |
unfolding euclidean_representation_setsum by simp |
44129 | 84 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
85 |
lemma (in euclidean_space) choice_Basis_iff: |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
86 |
fixes P :: "'a \<Rightarrow> real \<Rightarrow> bool" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
87 |
shows "(\<forall>i\<in>Basis. \<exists>x. P i x) \<longleftrightarrow> (\<exists>x. \<forall>i\<in>Basis. P i (inner x i))" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
88 |
unfolding bchoice_iff |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
89 |
proof safe |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
90 |
fix f assume "\<forall>i\<in>Basis. P i (f i)" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
91 |
then show "\<exists>x. \<forall>i\<in>Basis. P i (inner x i)" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
92 |
by (auto intro!: exI[of _ "\<Sum>i\<in>Basis. f i *\<^sub>R i"]) |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
93 |
qed 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
|
94 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
95 |
lemma DIM_positive: "0 < DIM('a::euclidean_space)" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
96 |
by (simp add: card_gt_0_iff) |
44628
bd17b7543af1
move lemmas from Topology_Euclidean_Space to Euclidean_Space
huffman
parents:
44571
diff
changeset
|
97 |
|
44571 | 98 |
subsection {* Subclass relationships *} |
99 |
||
100 |
instance euclidean_space \<subseteq> perfect_space |
|
101 |
proof |
|
102 |
fix x :: 'a show "\<not> open {x}" |
|
103 |
proof |
|
104 |
assume "open {x}" |
|
105 |
then obtain e where "0 < e" and e: "\<forall>y. dist y x < e \<longrightarrow> y = x" |
|
106 |
unfolding open_dist by fast |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
107 |
def y \<equiv> "x + scaleR (e/2) (SOME b. b \<in> Basis)" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
108 |
have [simp]: "(SOME b. b \<in> Basis) \<in> Basis" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
109 |
by (rule someI_ex) (auto simp: ex_in_conv) |
44571 | 110 |
from `0 < e` have "y \<noteq> x" |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
111 |
unfolding y_def by (auto intro!: nonzero_Basis) |
44571 | 112 |
from `0 < e` have "dist y x < e" |
53939 | 113 |
unfolding y_def by (simp add: dist_norm) |
44571 | 114 |
from `y \<noteq> x` and `dist y x < e` show "False" |
115 |
using e by simp |
|
116 |
qed |
|
117 |
qed |
|
118 |
||
44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
119 |
subsection {* Class instances *} |
33175 | 120 |
|
44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
121 |
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
|
122 |
|
44129 | 123 |
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
|
124 |
begin |
44129 | 125 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
126 |
definition |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
127 |
[simp]: "Basis = {1::real}" |
44129 | 128 |
|
129 |
instance |
|
53939 | 130 |
by default auto |
44129 | 131 |
|
132 |
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
|
133 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
134 |
lemma DIM_real[simp]: "DIM(real) = 1" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
135 |
by simp |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
136 |
|
44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
137 |
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
|
138 |
|
44129 | 139 |
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
|
140 |
begin |
44129 | 141 |
|
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
142 |
definition Basis_complex_def: |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
143 |
"Basis = {1, ii}" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
144 |
|
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
145 |
instance |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
146 |
by default (auto simp add: Basis_complex_def intro: complex_eqI split: split_if_asm) |
44129 | 147 |
|
148 |
end |
|
149 |
||
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
150 |
lemma DIM_complex[simp]: "DIM(complex) = 2" |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
151 |
unfolding Basis_complex_def 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
|
152 |
|
44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
153 |
subsubsection {* Type @{typ "'a \<times> 'b"} *} |
38656 | 154 |
|
44129 | 155 |
instantiation prod :: (euclidean_space, euclidean_space) euclidean_space |
38656 | 156 |
begin |
157 |
||
44129 | 158 |
definition |
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
159 |
"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
|
160 |
|
54781 | 161 |
lemma setsum_Basis_prod_eq: |
162 |
fixes f::"('a*'b)\<Rightarrow>('a*'b)" |
|
163 |
shows "setsum f Basis = setsum (\<lambda>i. f (i, 0)) Basis + setsum (\<lambda>i. f (0, i)) Basis" |
|
164 |
proof - |
|
165 |
have "inj_on (\<lambda>u. (u::'a, 0::'b)) Basis" "inj_on (\<lambda>u. (0::'a, u::'b)) Basis" |
|
166 |
by (auto intro!: inj_onI Pair_inject) |
|
167 |
thus ?thesis |
|
168 |
unfolding Basis_prod_def |
|
57418 | 169 |
by (subst setsum.union_disjoint) (auto simp: Basis_prod_def setsum.reindex) |
54781 | 170 |
qed |
171 |
||
44129 | 172 |
instance proof |
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
173 |
show "(Basis :: ('a \<times> 'b) set) \<noteq> {}" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
174 |
unfolding Basis_prod_def by simp |
44129 | 175 |
next |
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
176 |
show "finite (Basis :: ('a \<times> 'b) set)" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
177 |
unfolding Basis_prod_def by simp |
44129 | 178 |
next |
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
179 |
fix u v :: "'a \<times> 'b" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
180 |
assume "u \<in> Basis" and "v \<in> Basis" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
181 |
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
|
182 |
unfolding Basis_prod_def inner_prod_def |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
183 |
by (auto simp add: inner_Basis split: split_if_asm) |
44129 | 184 |
next |
185 |
fix x :: "'a \<times> 'b" |
|
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
186 |
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
|
187 |
unfolding Basis_prod_def ball_Un ball_simps |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
188 |
by (simp add: inner_prod_def prod_eq_iff euclidean_all_zero_iff) |
38656 | 189 |
qed |
44129 | 190 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
191 |
lemma DIM_prod[simp]: "DIM('a \<times> 'b) = DIM('a) + DIM('b)" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
192 |
unfolding Basis_prod_def |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
193 |
by (subst card_Un_disjoint) (auto intro!: card_image arg_cong2[where f="op +"] inj_onI) |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
194 |
|
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 |
end |
38656 | 196 |
|
197 |
end |