author | Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk> |
Tue, 28 Aug 2018 13:28:39 +0100 | |
changeset 68833 | fde093888c16 |
parent 68263 | e4e536a71e3d |
child 69064 | 5840724b1d71 |
permissions | -rw-r--r-- |
63627 | 1 |
(* Title: HOL/Analysis/Determinants.thy |
68143 | 2 |
Author: Amine Chaieb, University of Cambridge; proofs reworked by LCP |
33175 | 3 |
*) |
4 |
||
60420 | 5 |
section \<open>Traces, Determinant of square matrices and some properties\<close> |
33175 | 6 |
|
7 |
theory Determinants |
|
44228
5f974bead436
get Multivariate_Analysis/Determinants.thy compiled and working again
huffman
parents:
41959
diff
changeset
|
8 |
imports |
5f974bead436
get Multivariate_Analysis/Determinants.thy compiled and working again
huffman
parents:
41959
diff
changeset
|
9 |
Cartesian_Euclidean_Space |
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
64272
diff
changeset
|
10 |
"HOL-Library.Permutations" |
33175 | 11 |
begin |
12 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
13 |
subsection%important \<open>Trace\<close> |
33175 | 14 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
15 |
definition%important trace :: "'a::semiring_1^'n^'n \<Rightarrow> 'a" |
64267 | 16 |
where "trace A = sum (\<lambda>i. ((A$i)$i)) (UNIV::'n set)" |
33175 | 17 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
18 |
lemma%unimportant trace_0: "trace (mat 0) = 0" |
33175 | 19 |
by (simp add: trace_def mat_def) |
20 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
21 |
lemma%unimportant trace_I: "trace (mat 1 :: 'a::semiring_1^'n^'n) = of_nat(CARD('n))" |
33175 | 22 |
by (simp add: trace_def mat_def) |
23 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
24 |
lemma%unimportant trace_add: "trace ((A::'a::comm_semiring_1^'n^'n) + B) = trace A + trace B" |
64267 | 25 |
by (simp add: trace_def sum.distrib) |
33175 | 26 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
27 |
lemma%unimportant trace_sub: "trace ((A::'a::comm_ring_1^'n^'n) - B) = trace A - trace B" |
64267 | 28 |
by (simp add: trace_def sum_subtractf) |
33175 | 29 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
30 |
lemma%important trace_mul_sym: "trace ((A::'a::comm_semiring_1^'n^'m) ** B) = trace (B**A)" |
33175 | 31 |
apply (simp add: trace_def matrix_matrix_mult_def) |
66804
3f9bb52082c4
avoid name clashes on interpretation of abstract locales
haftmann
parents:
66453
diff
changeset
|
32 |
apply (subst sum.swap) |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
33 |
apply (simp add: mult.commute) |
53253 | 34 |
done |
33175 | 35 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
36 |
subsubsection%important \<open>Definition of determinant\<close> |
33175 | 37 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
38 |
definition%important det:: "'a::comm_ring_1^'n^'n \<Rightarrow> 'a" where |
53253 | 39 |
"det A = |
64272 | 40 |
sum (\<lambda>p. of_int (sign p) * prod (\<lambda>i. A$i$p i) (UNIV :: 'n set)) |
53253 | 41 |
{p. p permutes (UNIV :: 'n set)}" |
33175 | 42 |
|
68134 | 43 |
text \<open>Basic determinant properties\<close> |
33175 | 44 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
45 |
lemma%important det_transpose [simp]: "det (transpose A) = det (A::'a::comm_ring_1 ^'n^'n)" |
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
46 |
proof%unimportant - |
33175 | 47 |
let ?di = "\<lambda>A i j. A$i$j" |
48 |
let ?U = "(UNIV :: 'n set)" |
|
49 |
have fU: "finite ?U" by simp |
|
53253 | 50 |
{ |
51 |
fix p |
|
52 |
assume p: "p \<in> {p. p permutes ?U}" |
|
53854 | 53 |
from p have pU: "p permutes ?U" |
54 |
by blast |
|
33175 | 55 |
have sth: "sign (inv p) = sign p" |
44260
7784fa3232ce
Determinants.thy: avoid using mem_def/Collect_def
huffman
parents:
44228
diff
changeset
|
56 |
by (metis sign_inverse fU p mem_Collect_eq permutation_permutes) |
33175 | 57 |
from permutes_inj[OF pU] |
53854 | 58 |
have pi: "inj_on p ?U" |
59 |
by (blast intro: subset_inj_on) |
|
33175 | 60 |
from permutes_image[OF pU] |
64272 | 61 |
have "prod (\<lambda>i. ?di (transpose A) i (inv p i)) ?U = |
62 |
prod (\<lambda>i. ?di (transpose A) i (inv p i)) (p ` ?U)" |
|
53854 | 63 |
by simp |
64272 | 64 |
also have "\<dots> = prod ((\<lambda>i. ?di (transpose A) i (inv p i)) \<circ> p) ?U" |
65 |
unfolding prod.reindex[OF pi] .. |
|
66 |
also have "\<dots> = prod (\<lambda>i. ?di A i (p i)) ?U" |
|
53253 | 67 |
proof - |
68134 | 68 |
have "((\<lambda>i. ?di (transpose A) i (inv p i)) \<circ> p) i = ?di A i (p i)" if "i \<in> ?U" for i |
69 |
using that permutes_inv_o[OF pU] permutes_in_image[OF pU] |
|
70 |
unfolding transpose_def by (simp add: fun_eq_iff) |
|
71 |
then show "prod ((\<lambda>i. ?di (transpose A) i (inv p i)) \<circ> p) ?U = prod (\<lambda>i. ?di A i (p i)) ?U" |
|
64272 | 72 |
by (auto intro: prod.cong) |
33175 | 73 |
qed |
64272 | 74 |
finally have "of_int (sign (inv p)) * (prod (\<lambda>i. ?di (transpose A) i (inv p i)) ?U) = |
75 |
of_int (sign p) * (prod (\<lambda>i. ?di A i (p i)) ?U)" |
|
53854 | 76 |
using sth by simp |
53253 | 77 |
} |
78 |
then show ?thesis |
|
79 |
unfolding det_def |
|
68138 | 80 |
by (subst sum_permutations_inverse) (blast intro: sum.cong) |
33175 | 81 |
qed |
82 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
83 |
lemma%unimportant det_lowerdiagonal: |
34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34289
diff
changeset
|
84 |
fixes A :: "'a::comm_ring_1^('n::{finite,wellorder})^('n::{finite,wellorder})" |
33175 | 85 |
assumes ld: "\<And>i j. i < j \<Longrightarrow> A$i$j = 0" |
64272 | 86 |
shows "det A = prod (\<lambda>i. A$i$i) (UNIV:: 'n set)" |
53253 | 87 |
proof - |
33175 | 88 |
let ?U = "UNIV:: 'n set" |
89 |
let ?PU = "{p. p permutes ?U}" |
|
64272 | 90 |
let ?pp = "\<lambda>p. of_int (sign p) * prod (\<lambda>i. A$i$p i) (UNIV :: 'n set)" |
53854 | 91 |
have fU: "finite ?U" |
92 |
by simp |
|
93 |
have id0: "{id} \<subseteq> ?PU" |
|
68138 | 94 |
by (auto simp: permutes_id) |
68134 | 95 |
have p0: "\<forall>p \<in> ?PU - {id}. ?pp p = 0" |
96 |
proof |
|
53253 | 97 |
fix p |
68134 | 98 |
assume "p \<in> ?PU - {id}" |
99 |
then obtain i where i: "p i > i" |
|
100 |
by clarify (meson leI permutes_natset_le) |
|
101 |
from ld[OF i] have "\<exists>i \<in> ?U. A$i$p i = 0" |
|
53253 | 102 |
by blast |
68134 | 103 |
with prod_zero[OF fU] show "?pp p = 0" |
104 |
by force |
|
105 |
qed |
|
106 |
from sum.mono_neutral_cong_left[OF finite_permutations[OF fU] id0 p0] show ?thesis |
|
33175 | 107 |
unfolding det_def by (simp add: sign_id) |
108 |
qed |
|
109 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
110 |
lemma%important det_upperdiagonal: |
34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34289
diff
changeset
|
111 |
fixes A :: "'a::comm_ring_1^'n::{finite,wellorder}^'n::{finite,wellorder}" |
33175 | 112 |
assumes ld: "\<And>i j. i > j \<Longrightarrow> A$i$j = 0" |
64272 | 113 |
shows "det A = prod (\<lambda>i. A$i$i) (UNIV:: 'n set)" |
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
114 |
proof%unimportant - |
33175 | 115 |
let ?U = "UNIV:: 'n set" |
116 |
let ?PU = "{p. p permutes ?U}" |
|
64272 | 117 |
let ?pp = "(\<lambda>p. of_int (sign p) * prod (\<lambda>i. A$i$p i) (UNIV :: 'n set))" |
53854 | 118 |
have fU: "finite ?U" |
119 |
by simp |
|
120 |
have id0: "{id} \<subseteq> ?PU" |
|
68138 | 121 |
by (auto simp: permutes_id) |
68134 | 122 |
have p0: "\<forall>p \<in> ?PU -{id}. ?pp p = 0" |
123 |
proof |
|
53253 | 124 |
fix p |
53854 | 125 |
assume p: "p \<in> ?PU - {id}" |
68134 | 126 |
then obtain i where i: "p i < i" |
127 |
by clarify (meson leI permutes_natset_ge) |
|
128 |
from ld[OF i] have "\<exists>i \<in> ?U. A$i$p i = 0" |
|
53854 | 129 |
by blast |
68134 | 130 |
with prod_zero[OF fU] show "?pp p = 0" |
131 |
by force |
|
132 |
qed |
|
133 |
from sum.mono_neutral_cong_left[OF finite_permutations[OF fU] id0 p0] show ?thesis |
|
33175 | 134 |
unfolding det_def by (simp add: sign_id) |
135 |
qed |
|
136 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
137 |
lemma%important det_diagonal: |
34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34289
diff
changeset
|
138 |
fixes A :: "'a::comm_ring_1^'n^'n" |
33175 | 139 |
assumes ld: "\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0" |
64272 | 140 |
shows "det A = prod (\<lambda>i. A$i$i) (UNIV::'n set)" |
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
141 |
proof%unimportant - |
33175 | 142 |
let ?U = "UNIV:: 'n set" |
143 |
let ?PU = "{p. p permutes ?U}" |
|
64272 | 144 |
let ?pp = "\<lambda>p. of_int (sign p) * prod (\<lambda>i. A$i$p i) (UNIV :: 'n set)" |
33175 | 145 |
have fU: "finite ?U" by simp |
146 |
from finite_permutations[OF fU] have fPU: "finite ?PU" . |
|
53854 | 147 |
have id0: "{id} \<subseteq> ?PU" |
68138 | 148 |
by (auto simp: permutes_id) |
68134 | 149 |
have p0: "\<forall>p \<in> ?PU - {id}. ?pp p = 0" |
150 |
proof |
|
53253 | 151 |
fix p |
152 |
assume p: "p \<in> ?PU - {id}" |
|
53854 | 153 |
then obtain i where i: "p i \<noteq> i" |
68134 | 154 |
by fastforce |
155 |
with ld have "\<exists>i \<in> ?U. A$i$p i = 0" |
|
156 |
by (metis UNIV_I) |
|
157 |
with prod_zero [OF fU] show "?pp p = 0" |
|
158 |
by force |
|
159 |
qed |
|
64267 | 160 |
from sum.mono_neutral_cong_left[OF fPU id0 p0] show ?thesis |
33175 | 161 |
unfolding det_def by (simp add: sign_id) |
162 |
qed |
|
163 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
164 |
lemma%unimportant det_I [simp]: "det (mat 1 :: 'a::comm_ring_1^'n^'n) = 1" |
67673
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset
|
165 |
by (simp add: det_diagonal mat_def) |
33175 | 166 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
167 |
lemma%unimportant det_0 [simp]: "det (mat 0 :: 'a::comm_ring_1^'n^'n) = 0" |
67970 | 168 |
by (simp add: det_def prod_zero power_0_left) |
33175 | 169 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
170 |
lemma%unimportant det_permute_rows: |
34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34289
diff
changeset
|
171 |
fixes A :: "'a::comm_ring_1^'n^'n" |
33175 | 172 |
assumes p: "p permutes (UNIV :: 'n::finite set)" |
53854 | 173 |
shows "det (\<chi> i. A$p i :: 'a^'n^'n) = of_int (sign p) * det A" |
68134 | 174 |
proof - |
33175 | 175 |
let ?U = "UNIV :: 'n set" |
176 |
let ?PU = "{p. p permutes ?U}" |
|
68134 | 177 |
have *: "(\<Sum>q\<in>?PU. of_int (sign (q \<circ> p)) * (\<Prod>i\<in>?U. A $ p i $ (q \<circ> p) i)) = |
178 |
(\<Sum>n\<in>?PU. of_int (sign p) * of_int (sign n) * (\<Prod>i\<in>?U. A $ i $ n i))" |
|
179 |
proof (rule sum.cong) |
|
180 |
fix q |
|
181 |
assume qPU: "q \<in> ?PU" |
|
182 |
have fU: "finite ?U" |
|
183 |
by simp |
|
184 |
from qPU have q: "q permutes ?U" |
|
185 |
by blast |
|
186 |
have "prod (\<lambda>i. A$p i$ (q \<circ> p) i) ?U = prod ((\<lambda>i. A$p i$(q \<circ> p) i) \<circ> inv p) ?U" |
|
187 |
by (simp only: prod.permute[OF permutes_inv[OF p], symmetric]) |
|
188 |
also have "\<dots> = prod (\<lambda>i. A $ (p \<circ> inv p) i $ (q \<circ> (p \<circ> inv p)) i) ?U" |
|
189 |
by (simp only: o_def) |
|
190 |
also have "\<dots> = prod (\<lambda>i. A$i$q i) ?U" |
|
191 |
by (simp only: o_def permutes_inverses[OF p]) |
|
192 |
finally have thp: "prod (\<lambda>i. A$p i$ (q \<circ> p) i) ?U = prod (\<lambda>i. A$i$q i) ?U" |
|
193 |
by blast |
|
194 |
from p q have pp: "permutation p" and qp: "permutation q" |
|
195 |
by (metis fU permutation_permutes)+ |
|
196 |
show "of_int (sign (q \<circ> p)) * prod (\<lambda>i. A$ p i$ (q \<circ> p) i) ?U = |
|
197 |
of_int (sign p) * of_int (sign q) * prod (\<lambda>i. A$i$q i) ?U" |
|
198 |
by (simp only: thp sign_compose[OF qp pp] mult.commute of_int_mult) |
|
199 |
qed auto |
|
200 |
show ?thesis |
|
201 |
apply (simp add: det_def sum_distrib_left mult.assoc[symmetric]) |
|
202 |
apply (subst sum_permutations_compose_right[OF p]) |
|
203 |
apply (rule *) |
|
204 |
done |
|
68143 | 205 |
qed |
33175 | 206 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
207 |
lemma%important det_permute_columns: |
34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34289
diff
changeset
|
208 |
fixes A :: "'a::comm_ring_1^'n^'n" |
33175 | 209 |
assumes p: "p permutes (UNIV :: 'n set)" |
210 |
shows "det(\<chi> i j. A$i$ p j :: 'a^'n^'n) = of_int (sign p) * det A" |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
211 |
proof%unimportant - |
33175 | 212 |
let ?Ap = "\<chi> i j. A$i$ p j :: 'a^'n^'n" |
35150
082fa4bd403d
Rename transp to transpose in HOL-Multivariate_Analysis. (by himmelma)
hoelzl
parents:
35028
diff
changeset
|
213 |
let ?At = "transpose A" |
082fa4bd403d
Rename transp to transpose in HOL-Multivariate_Analysis. (by himmelma)
hoelzl
parents:
35028
diff
changeset
|
214 |
have "of_int (sign p) * det A = det (transpose (\<chi> i. transpose A $ p i))" |
082fa4bd403d
Rename transp to transpose in HOL-Multivariate_Analysis. (by himmelma)
hoelzl
parents:
35028
diff
changeset
|
215 |
unfolding det_permute_rows[OF p, of ?At] det_transpose .. |
33175 | 216 |
moreover |
35150
082fa4bd403d
Rename transp to transpose in HOL-Multivariate_Analysis. (by himmelma)
hoelzl
parents:
35028
diff
changeset
|
217 |
have "?Ap = transpose (\<chi> i. transpose A $ p i)" |
44228
5f974bead436
get Multivariate_Analysis/Determinants.thy compiled and working again
huffman
parents:
41959
diff
changeset
|
218 |
by (simp add: transpose_def vec_eq_iff) |
53854 | 219 |
ultimately show ?thesis |
220 |
by simp |
|
33175 | 221 |
qed |
222 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
223 |
lemma%unimportant det_identical_columns: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
224 |
fixes A :: "'a::comm_ring_1^'n^'n" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
225 |
assumes jk: "j \<noteq> k" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
226 |
and r: "column j A = column k A" |
33175 | 227 |
shows "det A = 0" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
228 |
proof - |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
229 |
let ?U="UNIV::'n set" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
230 |
let ?t_jk="Fun.swap j k id" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
231 |
let ?PU="{p. p permutes ?U}" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
232 |
let ?S1="{p. p\<in>?PU \<and> evenperm p}" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
233 |
let ?S2="{(?t_jk \<circ> p) |p. p \<in>?S1}" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
234 |
let ?f="\<lambda>p. of_int (sign p) * (\<Prod>i\<in>UNIV. A $ i $ p i)" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
235 |
let ?g="\<lambda>p. ?t_jk \<circ> p" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
236 |
have g_S1: "?S2 = ?g` ?S1" by auto |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
237 |
have inj_g: "inj_on ?g ?S1" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
238 |
proof (unfold inj_on_def, auto) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
239 |
fix x y assume x: "x permutes ?U" and even_x: "evenperm x" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
240 |
and y: "y permutes ?U" and even_y: "evenperm y" and eq: "?t_jk \<circ> x = ?t_jk \<circ> y" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
241 |
show "x = y" by (metis (hide_lams, no_types) comp_assoc eq id_comp swap_id_idempotent) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
242 |
qed |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
243 |
have tjk_permutes: "?t_jk permutes ?U" unfolding permutes_def swap_id_eq by (auto,metis) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
244 |
have tjk_eq: "\<forall>i l. A $ i $ ?t_jk l = A $ i $ l" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
245 |
using r jk |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
246 |
unfolding column_def vec_eq_iff swap_id_eq by fastforce |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
247 |
have sign_tjk: "sign ?t_jk = -1" using sign_swap_id[of j k] jk by auto |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
248 |
{fix x |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
249 |
assume x: "x\<in> ?S1" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
250 |
have "sign (?t_jk \<circ> x) = sign (?t_jk) * sign x" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
251 |
by (metis (lifting) finite_class.finite_UNIV mem_Collect_eq |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
252 |
permutation_permutes permutation_swap_id sign_compose x) |
68138 | 253 |
also have "\<dots> = - sign x" using sign_tjk by simp |
254 |
also have "\<dots> \<noteq> sign x" unfolding sign_def by simp |
|
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
255 |
finally have "sign (?t_jk \<circ> x) \<noteq> sign x" and "(?t_jk \<circ> x) \<in> ?S2" |
68134 | 256 |
using x by force+ |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
257 |
} |
68134 | 258 |
hence disjoint: "?S1 \<inter> ?S2 = {}" |
259 |
by (force simp: sign_def) |
|
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
260 |
have PU_decomposition: "?PU = ?S1 \<union> ?S2" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
261 |
proof (auto) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
262 |
fix x |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
263 |
assume x: "x permutes ?U" and "\<forall>p. p permutes ?U \<longrightarrow> x = Fun.swap j k id \<circ> p \<longrightarrow> \<not> evenperm p" |
68134 | 264 |
then obtain p where p: "p permutes UNIV" and x_eq: "x = Fun.swap j k id \<circ> p" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
265 |
and odd_p: "\<not> evenperm p" |
68134 | 266 |
by (metis (mono_tags) id_o o_assoc permutes_compose swap_id_idempotent tjk_permutes) |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
267 |
thus "evenperm x" |
68134 | 268 |
by (meson evenperm_comp evenperm_swap finite_class.finite_UNIV |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
269 |
jk permutation_permutes permutation_swap_id) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
270 |
next |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
271 |
fix p assume p: "p permutes ?U" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
272 |
show "Fun.swap j k id \<circ> p permutes UNIV" by (metis p permutes_compose tjk_permutes) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
273 |
qed |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
274 |
have "sum ?f ?S2 = sum ((\<lambda>p. of_int (sign p) * (\<Prod>i\<in>UNIV. A $ i $ p i)) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
275 |
\<circ> (\<circ>) (Fun.swap j k id)) {p \<in> {p. p permutes UNIV}. evenperm p}" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
276 |
unfolding g_S1 by (rule sum.reindex[OF inj_g]) |
68138 | 277 |
also have "\<dots> = sum (\<lambda>p. of_int (sign (?t_jk \<circ> p)) * (\<Prod>i\<in>UNIV. A $ i $ p i)) ?S1" |
278 |
unfolding o_def by (rule sum.cong, auto simp: tjk_eq) |
|
279 |
also have "\<dots> = sum (\<lambda>p. - ?f p) ?S1" |
|
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
280 |
proof (rule sum.cong, auto) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
281 |
fix x assume x: "x permutes ?U" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
282 |
and even_x: "evenperm x" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
283 |
hence perm_x: "permutation x" and perm_tjk: "permutation ?t_jk" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
284 |
using permutation_permutes[of x] permutation_permutes[of ?t_jk] permutation_swap_id |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
285 |
by (metis finite_code)+ |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
286 |
have "(sign (?t_jk \<circ> x)) = - (sign x)" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
287 |
unfolding sign_compose[OF perm_tjk perm_x] sign_tjk by auto |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
288 |
thus "of_int (sign (?t_jk \<circ> x)) * (\<Prod>i\<in>UNIV. A $ i $ x i) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
289 |
= - (of_int (sign x) * (\<Prod>i\<in>UNIV. A $ i $ x i))" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
290 |
by auto |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
291 |
qed |
68138 | 292 |
also have "\<dots>= - sum ?f ?S1" unfolding sum_negf .. |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
293 |
finally have *: "sum ?f ?S2 = - sum ?f ?S1" . |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
294 |
have "det A = (\<Sum>p | p permutes UNIV. of_int (sign p) * (\<Prod>i\<in>UNIV. A $ i $ p i))" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
295 |
unfolding det_def .. |
68138 | 296 |
also have "\<dots>= sum ?f ?S1 + sum ?f ?S2" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
297 |
by (subst PU_decomposition, rule sum.union_disjoint[OF _ _ disjoint], auto) |
68138 | 298 |
also have "\<dots>= sum ?f ?S1 - sum ?f ?S1 " unfolding * by auto |
299 |
also have "\<dots>= 0" by simp |
|
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
300 |
finally show "det A = 0" by simp |
33175 | 301 |
qed |
302 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
303 |
lemma%unimportant det_identical_rows: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
304 |
fixes A :: "'a::comm_ring_1^'n^'n" |
68134 | 305 |
assumes ij: "i \<noteq> j" and r: "row i A = row j A" |
33175 | 306 |
shows "det A = 0" |
68134 | 307 |
by (metis column_transpose det_identical_columns det_transpose ij r) |
33175 | 308 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
309 |
lemma%unimportant det_zero_row: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
310 |
fixes A :: "'a::{idom, ring_char_0}^'n^'n" and F :: "'b::{field}^'m^'m" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
311 |
shows "row i A = 0 \<Longrightarrow> det A = 0" and "row j F = 0 \<Longrightarrow> det F = 0" |
68138 | 312 |
by (force simp: row_def det_def vec_eq_iff sign_nz intro!: sum.neutral)+ |
33175 | 313 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
314 |
lemma%unimportant det_zero_column: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
315 |
fixes A :: "'a::{idom, ring_char_0}^'n^'n" and F :: "'b::{field}^'m^'m" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
316 |
shows "column i A = 0 \<Longrightarrow> det A = 0" and "column j F = 0 \<Longrightarrow> det F = 0" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
317 |
unfolding atomize_conj atomize_imp |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
318 |
by (metis det_transpose det_zero_row row_transpose) |
33175 | 319 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
320 |
lemma%unimportant det_row_add: |
33175 | 321 |
fixes a b c :: "'n::finite \<Rightarrow> _ ^ 'n" |
322 |
shows "det((\<chi> i. if i = k then a i + b i else c i)::'a::comm_ring_1^'n^'n) = |
|
53253 | 323 |
det((\<chi> i. if i = k then a i else c i)::'a::comm_ring_1^'n^'n) + |
324 |
det((\<chi> i. if i = k then b i else c i)::'a::comm_ring_1^'n^'n)" |
|
64267 | 325 |
unfolding det_def vec_lambda_beta sum.distrib[symmetric] |
326 |
proof (rule sum.cong) |
|
33175 | 327 |
let ?U = "UNIV :: 'n set" |
328 |
let ?pU = "{p. p permutes ?U}" |
|
329 |
let ?f = "(\<lambda>i. if i = k then a i + b i else c i)::'n \<Rightarrow> 'a::comm_ring_1^'n" |
|
330 |
let ?g = "(\<lambda> i. if i = k then a i else c i)::'n \<Rightarrow> 'a::comm_ring_1^'n" |
|
331 |
let ?h = "(\<lambda> i. if i = k then b i else c i)::'n \<Rightarrow> 'a::comm_ring_1^'n" |
|
53253 | 332 |
fix p |
333 |
assume p: "p \<in> ?pU" |
|
33175 | 334 |
let ?Uk = "?U - {k}" |
53854 | 335 |
from p have pU: "p permutes ?U" |
336 |
by blast |
|
337 |
have kU: "?U = insert k ?Uk" |
|
338 |
by blast |
|
68134 | 339 |
have eq: "prod (\<lambda>i. ?f i $ p i) ?Uk = prod (\<lambda>i. ?g i $ p i) ?Uk" |
340 |
"prod (\<lambda>i. ?f i $ p i) ?Uk = prod (\<lambda>i. ?h i $ p i) ?Uk" |
|
341 |
by auto |
|
342 |
have Uk: "finite ?Uk" "k \<notin> ?Uk" |
|
53854 | 343 |
by auto |
64272 | 344 |
have "prod (\<lambda>i. ?f i $ p i) ?U = prod (\<lambda>i. ?f i $ p i) (insert k ?Uk)" |
33175 | 345 |
unfolding kU[symmetric] .. |
64272 | 346 |
also have "\<dots> = ?f k $ p k * prod (\<lambda>i. ?f i $ p i) ?Uk" |
68134 | 347 |
by (rule prod.insert) auto |
64272 | 348 |
also have "\<dots> = (a k $ p k * prod (\<lambda>i. ?f i $ p i) ?Uk) + (b k$ p k * prod (\<lambda>i. ?f i $ p i) ?Uk)" |
53253 | 349 |
by (simp add: field_simps) |
64272 | 350 |
also have "\<dots> = (a k $ p k * prod (\<lambda>i. ?g i $ p i) ?Uk) + (b k$ p k * prod (\<lambda>i. ?h i $ p i) ?Uk)" |
68134 | 351 |
by (metis eq) |
64272 | 352 |
also have "\<dots> = prod (\<lambda>i. ?g i $ p i) (insert k ?Uk) + prod (\<lambda>i. ?h i $ p i) (insert k ?Uk)" |
68134 | 353 |
unfolding prod.insert[OF Uk] by simp |
64272 | 354 |
finally have "prod (\<lambda>i. ?f i $ p i) ?U = prod (\<lambda>i. ?g i $ p i) ?U + prod (\<lambda>i. ?h i $ p i) ?U" |
53854 | 355 |
unfolding kU[symmetric] . |
64272 | 356 |
then show "of_int (sign p) * prod (\<lambda>i. ?f i $ p i) ?U = |
357 |
of_int (sign p) * prod (\<lambda>i. ?g i $ p i) ?U + of_int (sign p) * prod (\<lambda>i. ?h i $ p i) ?U" |
|
36350 | 358 |
by (simp add: field_simps) |
68134 | 359 |
qed auto |
33175 | 360 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
361 |
lemma%unimportant det_row_mul: |
33175 | 362 |
fixes a b :: "'n::finite \<Rightarrow> _ ^ 'n" |
363 |
shows "det((\<chi> i. if i = k then c *s a i else b i)::'a::comm_ring_1^'n^'n) = |
|
53253 | 364 |
c * det((\<chi> i. if i = k then a i else b i)::'a::comm_ring_1^'n^'n)" |
64267 | 365 |
unfolding det_def vec_lambda_beta sum_distrib_left |
366 |
proof (rule sum.cong) |
|
33175 | 367 |
let ?U = "UNIV :: 'n set" |
368 |
let ?pU = "{p. p permutes ?U}" |
|
369 |
let ?f = "(\<lambda>i. if i = k then c*s a i else b i)::'n \<Rightarrow> 'a::comm_ring_1^'n" |
|
370 |
let ?g = "(\<lambda> i. if i = k then a i else b i)::'n \<Rightarrow> 'a::comm_ring_1^'n" |
|
53253 | 371 |
fix p |
372 |
assume p: "p \<in> ?pU" |
|
33175 | 373 |
let ?Uk = "?U - {k}" |
53854 | 374 |
from p have pU: "p permutes ?U" |
375 |
by blast |
|
376 |
have kU: "?U = insert k ?Uk" |
|
377 |
by blast |
|
68134 | 378 |
have eq: "prod (\<lambda>i. ?f i $ p i) ?Uk = prod (\<lambda>i. ?g i $ p i) ?Uk" |
68138 | 379 |
by auto |
68134 | 380 |
have Uk: "finite ?Uk" "k \<notin> ?Uk" |
53854 | 381 |
by auto |
64272 | 382 |
have "prod (\<lambda>i. ?f i $ p i) ?U = prod (\<lambda>i. ?f i $ p i) (insert k ?Uk)" |
33175 | 383 |
unfolding kU[symmetric] .. |
64272 | 384 |
also have "\<dots> = ?f k $ p k * prod (\<lambda>i. ?f i $ p i) ?Uk" |
68134 | 385 |
by (rule prod.insert) auto |
64272 | 386 |
also have "\<dots> = (c*s a k) $ p k * prod (\<lambda>i. ?f i $ p i) ?Uk" |
53253 | 387 |
by (simp add: field_simps) |
64272 | 388 |
also have "\<dots> = c* (a k $ p k * prod (\<lambda>i. ?g i $ p i) ?Uk)" |
68134 | 389 |
unfolding eq by (simp add: ac_simps) |
64272 | 390 |
also have "\<dots> = c* (prod (\<lambda>i. ?g i $ p i) (insert k ?Uk))" |
68134 | 391 |
unfolding prod.insert[OF Uk] by simp |
64272 | 392 |
finally have "prod (\<lambda>i. ?f i $ p i) ?U = c* (prod (\<lambda>i. ?g i $ p i) ?U)" |
53253 | 393 |
unfolding kU[symmetric] . |
68134 | 394 |
then show "of_int (sign p) * prod (\<lambda>i. ?f i $ p i) ?U = c * (of_int (sign p) * prod (\<lambda>i. ?g i $ p i) ?U)" |
36350 | 395 |
by (simp add: field_simps) |
68134 | 396 |
qed auto |
33175 | 397 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
398 |
lemma%unimportant det_row_0: |
33175 | 399 |
fixes b :: "'n::finite \<Rightarrow> _ ^ 'n" |
400 |
shows "det((\<chi> i. if i = k then 0 else b i)::'a::comm_ring_1^'n^'n) = 0" |
|
53253 | 401 |
using det_row_mul[of k 0 "\<lambda>i. 1" b] |
402 |
apply simp |
|
403 |
apply (simp only: vector_smult_lzero) |
|
404 |
done |
|
33175 | 405 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
406 |
lemma%important det_row_operation: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
407 |
fixes A :: "'a::{comm_ring_1}^'n^'n" |
33175 | 408 |
assumes ij: "i \<noteq> j" |
409 |
shows "det (\<chi> k. if k = i then row i A + c *s row j A else row k A) = det A" |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
410 |
proof%unimportant - |
33175 | 411 |
let ?Z = "(\<chi> k. if k = i then row j A else row k A) :: 'a ^'n^'n" |
412 |
have th: "row i ?Z = row j ?Z" by (vector row_def) |
|
413 |
have th2: "((\<chi> k. if k = i then row i A else row k A) :: 'a^'n^'n) = A" |
|
414 |
by (vector row_def) |
|
415 |
show ?thesis |
|
416 |
unfolding det_row_add [of i] det_row_mul[of i] det_identical_rows[OF ij th] th2 |
|
417 |
by simp |
|
418 |
qed |
|
419 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
420 |
lemma%unimportant det_row_span: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
421 |
fixes A :: "'a::{field}^'n^'n" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
422 |
assumes x: "x \<in> vec.span {row j A |j. j \<noteq> i}" |
33175 | 423 |
shows "det (\<chi> k. if k = i then row i A + x else row k A) = det A" |
68069
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
424 |
using x |
68074 | 425 |
proof (induction rule: vec.span_induct_alt) |
68069
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
426 |
case base |
68134 | 427 |
have "(if k = i then row i A + 0 else row k A) = row k A" for k |
428 |
by simp |
|
68069
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
429 |
then show ?case |
68134 | 430 |
by (simp add: row_def) |
68069
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
431 |
next |
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
432 |
case (step c z y) |
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
433 |
then obtain j where j: "z = row j A" "i \<noteq> j" |
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
434 |
by blast |
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
435 |
let ?w = "row i A + y" |
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
436 |
have th0: "row i A + (c*s z + y) = ?w + c*s z" |
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
437 |
by vector |
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
438 |
let ?d = "\<lambda>x. det (\<chi> k. if k = i then x else row k A)" |
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
439 |
have thz: "?d z = 0" |
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
440 |
apply (rule det_identical_rows[OF j(2)]) |
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
441 |
using j |
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
442 |
apply (vector row_def) |
33175 | 443 |
done |
68069
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
444 |
have "?d (row i A + (c*s z + y)) = ?d (?w + c*s z)" |
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
445 |
unfolding th0 .. |
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
446 |
then have "?d (row i A + (c*s z + y)) = det A" |
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
447 |
unfolding thz step.IH det_row_mul[of i] det_row_add[of i] by simp |
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
448 |
then show ?case |
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
449 |
unfolding scalar_mult_eq_scaleR . |
68143 | 450 |
qed |
33175 | 451 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
452 |
lemma%unimportant matrix_id [simp]: "det (matrix id) = 1" |
67673
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset
|
453 |
by (simp add: matrix_id_mat_1) |
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset
|
454 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
455 |
lemma%important det_matrix_scaleR [simp]: "det (matrix ((( *\<^sub>R) r)) :: real^'n^'n) = r ^ CARD('n::finite)" |
67673
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset
|
456 |
apply (subst det_diagonal) |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
457 |
apply (auto simp: matrix_def mat_def) |
67673
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset
|
458 |
apply (simp add: cart_eq_inner_axis inner_axis_axis) |
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset
|
459 |
done |
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset
|
460 |
|
60420 | 461 |
text \<open> |
53854 | 462 |
May as well do this, though it's a bit unsatisfactory since it ignores |
463 |
exact duplicates by considering the rows/columns as a set. |
|
60420 | 464 |
\<close> |
33175 | 465 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
466 |
lemma%unimportant det_dependent_rows: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
467 |
fixes A:: "'a::{field}^'n^'n" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
468 |
assumes d: "vec.dependent (rows A)" |
33175 | 469 |
shows "det A = 0" |
53253 | 470 |
proof - |
33175 | 471 |
let ?U = "UNIV :: 'n set" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
472 |
from d obtain i where i: "row i A \<in> vec.span (rows A - {row i A})" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
473 |
unfolding vec.dependent_def rows_def by blast |
68134 | 474 |
show ?thesis |
475 |
proof (cases "\<forall>i j. i \<noteq> j \<longrightarrow> row i A \<noteq> row j A") |
|
476 |
case True |
|
477 |
with i have "vec.span (rows A - {row i A}) \<subseteq> vec.span {row j A |j. j \<noteq> i}" |
|
68138 | 478 |
by (auto simp: rows_def intro!: vec.span_mono) |
68134 | 479 |
then have "- row i A \<in> vec.span {row j A|j. j \<noteq> i}" |
480 |
by (meson i subsetCE vec.span_neg) |
|
481 |
from det_row_span[OF this] |
|
33175 | 482 |
have "det A = det (\<chi> k. if k = i then 0 *s 1 else row k A)" |
483 |
unfolding right_minus vector_smult_lzero .. |
|
68134 | 484 |
with det_row_mul[of i 0 "\<lambda>i. 1"] |
485 |
show ?thesis by simp |
|
486 |
next |
|
487 |
case False |
|
488 |
then obtain j k where jk: "j \<noteq> k" "row j A = row k A" |
|
489 |
by auto |
|
490 |
from det_identical_rows[OF jk] show ?thesis . |
|
491 |
qed |
|
33175 | 492 |
qed |
493 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
494 |
lemma%unimportant det_dependent_columns: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
495 |
assumes d: "vec.dependent (columns (A::real^'n^'n))" |
53253 | 496 |
shows "det A = 0" |
497 |
by (metis d det_dependent_rows rows_transpose det_transpose) |
|
33175 | 498 |
|
68134 | 499 |
text \<open>Multilinearity and the multiplication formula\<close> |
33175 | 500 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
501 |
lemma%unimportant Cart_lambda_cong: "(\<And>x. f x = g x) \<Longrightarrow> (vec_lambda f::'a^'n) = (vec_lambda g :: 'a^'n)" |
68134 | 502 |
by auto |
33175 | 503 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
504 |
lemma%unimportant det_linear_row_sum: |
33175 | 505 |
assumes fS: "finite S" |
64267 | 506 |
shows "det ((\<chi> i. if i = k then sum (a i) S else c i)::'a::comm_ring_1^'n^'n) = |
507 |
sum (\<lambda>j. det ((\<chi> i. if i = k then a i j else c i)::'a^'n^'n)) S" |
|
68134 | 508 |
using fS by (induct rule: finite_induct; simp add: det_row_0 det_row_add cong: if_cong) |
33175 | 509 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
510 |
lemma%unimportant finite_bounded_functions: |
33175 | 511 |
assumes fS: "finite S" |
512 |
shows "finite {f. (\<forall>i \<in> {1.. (k::nat)}. f i \<in> S) \<and> (\<forall>i. i \<notin> {1 .. k} \<longrightarrow> f i = i)}" |
|
53253 | 513 |
proof (induct k) |
33175 | 514 |
case 0 |
68134 | 515 |
have *: "{f. \<forall>i. f i = i} = {id}" |
53854 | 516 |
by auto |
517 |
show ?case |
|
68138 | 518 |
by (auto simp: *) |
33175 | 519 |
next |
520 |
case (Suc k) |
|
521 |
let ?f = "\<lambda>(y::nat,g) i. if i = Suc k then y else g i" |
|
522 |
let ?S = "?f ` (S \<times> {f. (\<forall>i\<in>{1..k}. f i \<in> S) \<and> (\<forall>i. i \<notin> {1..k} \<longrightarrow> f i = i)})" |
|
523 |
have "?S = {f. (\<forall>i\<in>{1.. Suc k}. f i \<in> S) \<and> (\<forall>i. i \<notin> {1.. Suc k} \<longrightarrow> f i = i)}" |
|
68138 | 524 |
apply (auto simp: image_iff) |
68134 | 525 |
apply (rename_tac f) |
526 |
apply (rule_tac x="f (Suc k)" in bexI) |
|
68138 | 527 |
apply (rule_tac x = "\<lambda>i. if i = Suc k then i else f i" in exI, auto) |
33175 | 528 |
done |
529 |
with finite_imageI[OF finite_cartesian_product[OF fS Suc.hyps(1)], of ?f] |
|
53854 | 530 |
show ?case |
531 |
by metis |
|
33175 | 532 |
qed |
533 |
||
534 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
535 |
lemma%important det_linear_rows_sum_lemma: |
53854 | 536 |
assumes fS: "finite S" |
537 |
and fT: "finite T" |
|
64267 | 538 |
shows "det ((\<chi> i. if i \<in> T then sum (a i) S else c i):: 'a::comm_ring_1^'n^'n) = |
539 |
sum (\<lambda>f. det((\<chi> i. if i \<in> T then a i (f i) else c i)::'a^'n^'n)) |
|
53253 | 540 |
{f. (\<forall>i \<in> T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = i)}" |
541 |
using fT |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
542 |
proof%unimportant (induct T arbitrary: a c set: finite) |
33175 | 543 |
case empty |
53253 | 544 |
have th0: "\<And>x y. (\<chi> i. if i \<in> {} then x i else y i) = (\<chi> i. y i)" |
545 |
by vector |
|
53854 | 546 |
from empty.prems show ?case |
62408
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
61286
diff
changeset
|
547 |
unfolding th0 by (simp add: eq_id_iff) |
33175 | 548 |
next |
549 |
case (insert z T a c) |
|
550 |
let ?F = "\<lambda>T. {f. (\<forall>i \<in> T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = i)}" |
|
551 |
let ?h = "\<lambda>(y,g) i. if i = z then y else g i" |
|
552 |
let ?k = "\<lambda>h. (h(z),(\<lambda>i. if i = z then i else h i))" |
|
553 |
let ?s = "\<lambda> k a c f. det((\<chi> i. if i \<in> T then a i (f i) else c i)::'a^'n^'n)" |
|
57129
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56545
diff
changeset
|
554 |
let ?c = "\<lambda>j i. if i = z then a i j else c i" |
53253 | 555 |
have thif: "\<And>a b c d. (if a \<or> b then c else d) = (if a then c else if b then c else d)" |
556 |
by simp |
|
33175 | 557 |
have thif2: "\<And>a b c d e. (if a then b else if c then d else e) = |
53253 | 558 |
(if c then (if a then b else d) else (if a then b else e))" |
559 |
by simp |
|
68134 | 560 |
from \<open>z \<notin> T\<close> have nz: "\<And>i. i \<in> T \<Longrightarrow> i \<noteq> z" |
53253 | 561 |
by auto |
64267 | 562 |
have "det (\<chi> i. if i \<in> insert z T then sum (a i) S else c i) = |
563 |
det (\<chi> i. if i = z then sum (a i) S else if i \<in> T then sum (a i) S else c i)" |
|
33175 | 564 |
unfolding insert_iff thif .. |
64267 | 565 |
also have "\<dots> = (\<Sum>j\<in>S. det (\<chi> i. if i \<in> T then sum (a i) S else if i = z then a i j else c i))" |
566 |
unfolding det_linear_row_sum[OF fS] |
|
68134 | 567 |
by (subst thif2) (simp add: nz cong: if_cong) |
33175 | 568 |
finally have tha: |
64267 | 569 |
"det (\<chi> i. if i \<in> insert z T then sum (a i) S else c i) = |
33175 | 570 |
(\<Sum>(j, f)\<in>S \<times> ?F T. det (\<chi> i. if i \<in> T then a i (f i) |
571 |
else if i = z then a i j |
|
572 |
else c i))" |
|
64267 | 573 |
unfolding insert.hyps unfolding sum.cartesian_product by blast |
33175 | 574 |
show ?case unfolding tha |
60420 | 575 |
using \<open>z \<notin> T\<close> |
64267 | 576 |
by (intro sum.reindex_bij_witness[where i="?k" and j="?h"]) |
57129
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56545
diff
changeset
|
577 |
(auto intro!: cong[OF refl[of det]] simp: vec_eq_iff) |
33175 | 578 |
qed |
579 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
580 |
lemma%unimportant det_linear_rows_sum: |
53854 | 581 |
fixes S :: "'n::finite set" |
582 |
assumes fS: "finite S" |
|
64267 | 583 |
shows "det (\<chi> i. sum (a i) S) = |
584 |
sum (\<lambda>f. det (\<chi> i. a i (f i) :: 'a::comm_ring_1 ^ 'n^'n)) {f. \<forall>i. f i \<in> S}" |
|
53253 | 585 |
proof - |
586 |
have th0: "\<And>x y. ((\<chi> i. if i \<in> (UNIV:: 'n set) then x i else y i) :: 'a^'n^'n) = (\<chi> i. x i)" |
|
587 |
by vector |
|
64267 | 588 |
from det_linear_rows_sum_lemma[OF fS, of "UNIV :: 'n set" a, unfolded th0, OF finite] |
53253 | 589 |
show ?thesis by simp |
33175 | 590 |
qed |
591 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
592 |
lemma%unimportant matrix_mul_sum_alt: |
34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34289
diff
changeset
|
593 |
fixes A B :: "'a::comm_ring_1^'n^'n" |
64267 | 594 |
shows "A ** B = (\<chi> i. sum (\<lambda>k. A$i$k *s B $ k) (UNIV :: 'n set))" |
595 |
by (vector matrix_matrix_mult_def sum_component) |
|
33175 | 596 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
597 |
lemma%unimportant det_rows_mul: |
34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34289
diff
changeset
|
598 |
"det((\<chi> i. c i *s a i)::'a::comm_ring_1^'n^'n) = |
64272 | 599 |
prod (\<lambda>i. c i) (UNIV:: 'n set) * det((\<chi> i. a i)::'a^'n^'n)" |
600 |
proof (simp add: det_def sum_distrib_left cong add: prod.cong, rule sum.cong) |
|
33175 | 601 |
let ?U = "UNIV :: 'n set" |
602 |
let ?PU = "{p. p permutes ?U}" |
|
53253 | 603 |
fix p |
604 |
assume pU: "p \<in> ?PU" |
|
33175 | 605 |
let ?s = "of_int (sign p)" |
53253 | 606 |
from pU have p: "p permutes ?U" |
607 |
by blast |
|
64272 | 608 |
have "prod (\<lambda>i. c i * a i $ p i) ?U = prod c ?U * prod (\<lambda>i. a i $ p i) ?U" |
609 |
unfolding prod.distrib .. |
|
33175 | 610 |
then show "?s * (\<Prod>xa\<in>?U. c xa * a xa $ p xa) = |
64272 | 611 |
prod c ?U * (?s* (\<Prod>xa\<in>?U. a xa $ p xa))" |
53854 | 612 |
by (simp add: field_simps) |
57418 | 613 |
qed rule |
33175 | 614 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
615 |
lemma%important det_mul: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
616 |
fixes A B :: "'a::comm_ring_1^'n^'n" |
33175 | 617 |
shows "det (A ** B) = det A * det B" |
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
618 |
proof%unimportant - |
33175 | 619 |
let ?U = "UNIV :: 'n set" |
68134 | 620 |
let ?F = "{f. (\<forall>i \<in> ?U. f i \<in> ?U) \<and> (\<forall>i. i \<notin> ?U \<longrightarrow> f i = i)}" |
33175 | 621 |
let ?PU = "{p. p permutes ?U}" |
68134 | 622 |
have "p \<in> ?F" if "p permutes ?U" for p |
53854 | 623 |
by simp |
624 |
then have PUF: "?PU \<subseteq> ?F" by blast |
|
53253 | 625 |
{ |
626 |
fix f |
|
627 |
assume fPU: "f \<in> ?F - ?PU" |
|
53854 | 628 |
have fUU: "f ` ?U \<subseteq> ?U" |
629 |
using fPU by auto |
|
53253 | 630 |
from fPU have f: "\<forall>i \<in> ?U. f i \<in> ?U" "\<forall>i. i \<notin> ?U \<longrightarrow> f i = i" "\<not>(\<forall>y. \<exists>!x. f x = y)" |
631 |
unfolding permutes_def by auto |
|
33175 | 632 |
|
633 |
let ?A = "(\<chi> i. A$i$f i *s B$f i) :: 'a^'n^'n" |
|
634 |
let ?B = "(\<chi> i. B$f i) :: 'a^'n^'n" |
|
53253 | 635 |
{ |
636 |
assume fni: "\<not> inj_on f ?U" |
|
33175 | 637 |
then obtain i j where ij: "f i = f j" "i \<noteq> j" |
638 |
unfolding inj_on_def by blast |
|
68134 | 639 |
then have "row i ?B = row j ?B" |
53854 | 640 |
by (vector row_def) |
68134 | 641 |
with det_identical_rows[OF ij(2)] |
33175 | 642 |
have "det (\<chi> i. A$i$f i *s B$f i) = 0" |
68134 | 643 |
unfolding det_rows_mul by force |
53253 | 644 |
} |
33175 | 645 |
moreover |
53253 | 646 |
{ |
647 |
assume fi: "inj_on f ?U" |
|
33175 | 648 |
from f fi have fith: "\<And>i j. f i = f j \<Longrightarrow> i = j" |
649 |
unfolding inj_on_def by metis |
|
68134 | 650 |
note fs = fi[unfolded surjective_iff_injective_gen[OF finite finite refl fUU, symmetric]] |
651 |
have "\<exists>!x. f x = y" for y |
|
652 |
using fith fs by blast |
|
53854 | 653 |
with f(3) have "det (\<chi> i. A$i$f i *s B$f i) = 0" |
654 |
by blast |
|
53253 | 655 |
} |
53854 | 656 |
ultimately have "det (\<chi> i. A$i$f i *s B$f i) = 0" |
657 |
by blast |
|
53253 | 658 |
} |
53854 | 659 |
then have zth: "\<forall> f\<in> ?F - ?PU. det (\<chi> i. A$i$f i *s B$f i) = 0" |
53253 | 660 |
by simp |
661 |
{ |
|
662 |
fix p |
|
663 |
assume pU: "p \<in> ?PU" |
|
53854 | 664 |
from pU have p: "p permutes ?U" |
665 |
by blast |
|
33175 | 666 |
let ?s = "\<lambda>p. of_int (sign p)" |
53253 | 667 |
let ?f = "\<lambda>q. ?s p * (\<Prod>i\<in> ?U. A $ i $ p i) * (?s q * (\<Prod>i\<in> ?U. B $ i $ q i))" |
64267 | 668 |
have "(sum (\<lambda>q. ?s q * |
53253 | 669 |
(\<Prod>i\<in> ?U. (\<chi> i. A $ i $ p i *s B $ p i :: 'a^'n^'n) $ i $ q i)) ?PU) = |
64267 | 670 |
(sum (\<lambda>q. ?s p * (\<Prod>i\<in> ?U. A $ i $ p i) * (?s q * (\<Prod>i\<in> ?U. B $ i $ q i))) ?PU)" |
33175 | 671 |
unfolding sum_permutations_compose_right[OF permutes_inv[OF p], of ?f] |
64267 | 672 |
proof (rule sum.cong) |
53253 | 673 |
fix q |
674 |
assume qU: "q \<in> ?PU" |
|
53854 | 675 |
then have q: "q permutes ?U" |
676 |
by blast |
|
33175 | 677 |
from p q have pp: "permutation p" and pq: "permutation q" |
678 |
unfolding permutation_permutes by auto |
|
679 |
have th00: "of_int (sign p) * of_int (sign p) = (1::'a)" |
|
680 |
"\<And>a. of_int (sign p) * (of_int (sign p) * a) = a" |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
681 |
unfolding mult.assoc[symmetric] |
53854 | 682 |
unfolding of_int_mult[symmetric] |
33175 | 683 |
by (simp_all add: sign_idempotent) |
53854 | 684 |
have ths: "?s q = ?s p * ?s (q \<circ> inv p)" |
33175 | 685 |
using pp pq permutation_inverse[OF pp] sign_inverse[OF pp] |
68134 | 686 |
by (simp add: th00 ac_simps sign_idempotent sign_compose) |
64272 | 687 |
have th001: "prod (\<lambda>i. B$i$ q (inv p i)) ?U = prod ((\<lambda>i. B$i$ q (inv p i)) \<circ> p) ?U" |
68134 | 688 |
by (rule prod.permute[OF p]) |
64272 | 689 |
have thp: "prod (\<lambda>i. (\<chi> i. A$i$p i *s B$p i :: 'a^'n^'n) $i $ q i) ?U = |
690 |
prod (\<lambda>i. A$i$p i) ?U * prod (\<lambda>i. B$i$ q (inv p i)) ?U" |
|
691 |
unfolding th001 prod.distrib[symmetric] o_def permutes_inverses[OF p] |
|
692 |
apply (rule prod.cong[OF refl]) |
|
53253 | 693 |
using permutes_in_image[OF q] |
694 |
apply vector |
|
695 |
done |
|
64272 | 696 |
show "?s q * prod (\<lambda>i. (((\<chi> i. A$i$p i *s B$p i) :: 'a^'n^'n)$i$q i)) ?U = |
697 |
?s p * (prod (\<lambda>i. A$i$p i) ?U) * (?s (q \<circ> inv p) * prod (\<lambda>i. B$i$(q \<circ> inv p) i) ?U)" |
|
33175 | 698 |
using ths thp pp pq permutation_inverse[OF pp] sign_inverse[OF pp] |
36350 | 699 |
by (simp add: sign_nz th00 field_simps sign_idempotent sign_compose) |
57418 | 700 |
qed rule |
33175 | 701 |
} |
64267 | 702 |
then have th2: "sum (\<lambda>f. det (\<chi> i. A$i$f i *s B$f i)) ?PU = det A * det B" |
703 |
unfolding det_def sum_product |
|
704 |
by (rule sum.cong [OF refl]) |
|
705 |
have "det (A**B) = sum (\<lambda>f. det (\<chi> i. A $ i $ f i *s B $ f i)) ?F" |
|
68134 | 706 |
unfolding matrix_mul_sum_alt det_linear_rows_sum[OF finite] |
53854 | 707 |
by simp |
64267 | 708 |
also have "\<dots> = sum (\<lambda>f. det (\<chi> i. A$i$f i *s B$f i)) ?PU" |
68134 | 709 |
using sum.mono_neutral_cong_left[OF finite PUF zth, symmetric] |
33175 | 710 |
unfolding det_rows_mul by auto |
711 |
finally show ?thesis unfolding th2 . |
|
712 |
qed |
|
713 |
||
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
714 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
715 |
subsection%important \<open>Relation to invertibility\<close> |
33175 | 716 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
717 |
lemma%important invertible_det_nz: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
718 |
fixes A::"'a::{field}^'n^'n" |
33175 | 719 |
shows "invertible A \<longleftrightarrow> det A \<noteq> 0" |
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
720 |
proof%unimportant (cases "invertible A") |
68134 | 721 |
case True |
722 |
then obtain B :: "'a^'n^'n" where B: "A ** B = mat 1" |
|
723 |
unfolding invertible_right_inverse by blast |
|
724 |
then have "det (A ** B) = det (mat 1 :: 'a^'n^'n)" |
|
725 |
by simp |
|
726 |
then show ?thesis |
|
727 |
by (metis True det_I det_mul mult_zero_left one_neq_zero) |
|
728 |
next |
|
729 |
case False |
|
730 |
let ?U = "UNIV :: 'n set" |
|
731 |
have fU: "finite ?U" |
|
732 |
by simp |
|
733 |
from False obtain c i where c: "sum (\<lambda>i. c i *s row i A) ?U = 0" and iU: "i \<in> ?U" and ci: "c i \<noteq> 0" |
|
734 |
unfolding invertible_right_inverse matrix_right_invertible_independent_rows |
|
53854 | 735 |
by blast |
68134 | 736 |
have thr0: "- row i A = sum (\<lambda>j. (1/ c i) *s (c j *s row j A)) (?U - {i})" |
68143 | 737 |
unfolding sum_cmul using c ci |
68138 | 738 |
by (auto simp: sum.remove[OF fU iU] eq_vector_fraction_iff add_eq_0_iff) |
68134 | 739 |
have thr: "- row i A \<in> vec.span {row j A| j. j \<noteq> i}" |
740 |
unfolding thr0 by (auto intro: vec.span_base vec.span_scale vec.span_sum) |
|
741 |
let ?B = "(\<chi> k. if k = i then 0 else row k A) :: 'a^'n^'n" |
|
742 |
have thrb: "row i ?B = 0" using iU by (vector row_def) |
|
743 |
have "det A = 0" |
|
744 |
unfolding det_row_span[OF thr, symmetric] right_minus |
|
745 |
unfolding det_zero_row(2)[OF thrb] .. |
|
746 |
then show ?thesis |
|
747 |
by (simp add: False) |
|
33175 | 748 |
qed |
749 |
||
68134 | 750 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
751 |
lemma%unimportant det_nz_iff_inj_gen: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
752 |
fixes f :: "'a::field^'n \<Rightarrow> 'a::field^'n" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
753 |
assumes "Vector_Spaces.linear ( *s) ( *s) f" |
67990 | 754 |
shows "det (matrix f) \<noteq> 0 \<longleftrightarrow> inj f" |
755 |
proof |
|
756 |
assume "det (matrix f) \<noteq> 0" |
|
757 |
then show "inj f" |
|
758 |
using assms invertible_det_nz inj_matrix_vector_mult by force |
|
759 |
next |
|
760 |
assume "inj f" |
|
761 |
show "det (matrix f) \<noteq> 0" |
|
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
762 |
using vec.linear_injective_left_inverse [OF assms \<open>inj f\<close>] |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
763 |
by (metis assms invertible_det_nz invertible_left_inverse matrix_compose_gen matrix_id_mat_1) |
67990 | 764 |
qed |
765 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
766 |
lemma%unimportant det_nz_iff_inj: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
767 |
fixes f :: "real^'n \<Rightarrow> real^'n" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
768 |
assumes "linear f" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
769 |
shows "det (matrix f) \<noteq> 0 \<longleftrightarrow> inj f" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
770 |
using det_nz_iff_inj_gen[of f] assms |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
771 |
unfolding linear_matrix_vector_mul_eq . |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
772 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
773 |
lemma%unimportant det_eq_0_rank: |
67990 | 774 |
fixes A :: "real^'n^'n" |
775 |
shows "det A = 0 \<longleftrightarrow> rank A < CARD('n)" |
|
776 |
using invertible_det_nz [of A] |
|
777 |
by (auto simp: matrix_left_invertible_injective invertible_left_inverse less_rank_noninjective) |
|
778 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
779 |
subsubsection%important \<open>Invertibility of matrices and corresponding linear functions\<close> |
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
780 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
781 |
lemma%important matrix_left_invertible_gen: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
782 |
fixes f :: "'a::field^'m \<Rightarrow> 'a::field^'n" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
783 |
assumes "Vector_Spaces.linear ( *s) ( *s) f" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
784 |
shows "((\<exists>B. B ** matrix f = mat 1) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> g \<circ> f = id))" |
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
785 |
proof%unimportant safe |
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
786 |
fix B |
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
787 |
assume 1: "B ** matrix f = mat 1" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
788 |
show "\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> g \<circ> f = id" |
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
789 |
proof (intro exI conjI) |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
790 |
show "Vector_Spaces.linear ( *s) ( *s) (\<lambda>y. B *v y)" |
68138 | 791 |
by simp |
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
792 |
show "(( *v) B) \<circ> f = id" |
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
793 |
unfolding o_def |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
794 |
by (metis assms 1 eq_id_iff matrix_vector_mul(1) matrix_vector_mul_assoc matrix_vector_mul_lid) |
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
795 |
qed |
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
796 |
next |
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
797 |
fix g |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
798 |
assume "Vector_Spaces.linear ( *s) ( *s) g" "g \<circ> f = id" |
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
799 |
then have "matrix g ** matrix f = mat 1" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
800 |
by (metis assms matrix_compose_gen matrix_id_mat_1) |
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
801 |
then show "\<exists>B. B ** matrix f = mat 1" .. |
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
802 |
qed |
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
803 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
804 |
lemma%unimportant matrix_left_invertible: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
805 |
"linear f \<Longrightarrow> ((\<exists>B. B ** matrix f = mat 1) \<longleftrightarrow> (\<exists>g. linear g \<and> g \<circ> f = id))" for f::"real^'m \<Rightarrow> real^'n" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
806 |
using matrix_left_invertible_gen[of f] |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
807 |
by (auto simp: linear_matrix_vector_mul_eq) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
808 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
809 |
lemma%unimportant matrix_right_invertible_gen: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
810 |
fixes f :: "'a::field^'m \<Rightarrow> 'a^'n" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
811 |
assumes "Vector_Spaces.linear ( *s) ( *s) f" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
812 |
shows "((\<exists>B. matrix f ** B = mat 1) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> f \<circ> g = id))" |
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
813 |
proof safe |
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
814 |
fix B |
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
815 |
assume 1: "matrix f ** B = mat 1" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
816 |
show "\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> f \<circ> g = id" |
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
817 |
proof (intro exI conjI) |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
818 |
show "Vector_Spaces.linear ( *s) ( *s) (( *v) B)" |
68138 | 819 |
by simp |
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
820 |
show "f \<circ> ( *v) B = id" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
821 |
using 1 assms comp_apply eq_id_iff vec.linear_id matrix_id_mat_1 matrix_vector_mul_assoc matrix_works |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
822 |
by (metis (no_types, hide_lams)) |
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
823 |
qed |
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
824 |
next |
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
825 |
fix g |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
826 |
assume "Vector_Spaces.linear ( *s) ( *s) g" and "f \<circ> g = id" |
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
827 |
then have "matrix f ** matrix g = mat 1" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
828 |
by (metis assms matrix_compose_gen matrix_id_mat_1) |
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
829 |
then show "\<exists>B. matrix f ** B = mat 1" .. |
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
830 |
qed |
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
831 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
832 |
lemma%unimportant matrix_right_invertible: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
833 |
"linear f \<Longrightarrow> ((\<exists>B. matrix f ** B = mat 1) \<longleftrightarrow> (\<exists>g. linear g \<and> f \<circ> g = id))" for f::"real^'m \<Rightarrow> real^'n" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
834 |
using matrix_right_invertible_gen[of f] |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
835 |
by (auto simp: linear_matrix_vector_mul_eq) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
836 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
837 |
lemma%unimportant matrix_invertible_gen: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
838 |
fixes f :: "'a::field^'m \<Rightarrow> 'a::field^'n" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
839 |
assumes "Vector_Spaces.linear ( *s) ( *s) f" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
840 |
shows "invertible (matrix f) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> f \<circ> g = id \<and> g \<circ> f = id)" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
841 |
(is "?lhs = ?rhs") |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
842 |
proof |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
843 |
assume ?lhs then show ?rhs |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
844 |
by (metis assms invertible_def left_right_inverse_eq matrix_left_invertible_gen matrix_right_invertible_gen) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
845 |
next |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
846 |
assume ?rhs then show ?lhs |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
847 |
by (metis assms invertible_def matrix_compose_gen matrix_id_mat_1) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
848 |
qed |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
849 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
850 |
lemma%unimportant matrix_invertible: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
851 |
"linear f \<Longrightarrow> invertible (matrix f) \<longleftrightarrow> (\<exists>g. linear g \<and> f \<circ> g = id \<and> g \<circ> f = id)" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
852 |
for f::"real^'m \<Rightarrow> real^'n" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
853 |
using matrix_invertible_gen[of f] |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
854 |
by (auto simp: linear_matrix_vector_mul_eq) |
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
855 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
856 |
lemma%unimportant invertible_eq_bij: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
857 |
fixes m :: "'a::field^'m^'n" |
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
858 |
shows "invertible m \<longleftrightarrow> bij (( *v) m)" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
859 |
using matrix_invertible_gen[OF matrix_vector_mul_linear_gen, of m, simplified matrix_of_matrix_vector_mul] |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
860 |
by (metis bij_betw_def left_right_inverse_eq matrix_vector_mul_linear_gen o_bij |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
861 |
vec.linear_injective_left_inverse vec.linear_surjective_right_inverse) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
862 |
|
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
863 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
864 |
subsection%important \<open>Cramer's rule\<close> |
33175 | 865 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
866 |
lemma%important cramer_lemma_transpose: |
68263 | 867 |
fixes A:: "'a::{field}^'n^'n" |
868 |
and x :: "'a::{field}^'n" |
|
64267 | 869 |
shows "det ((\<chi> i. if i = k then sum (\<lambda>i. x$i *s row i A) (UNIV::'n set) |
68263 | 870 |
else row i A)::'a::{field}^'n^'n) = x$k * det A" |
33175 | 871 |
(is "?lhs = ?rhs") |
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
872 |
proof%unimportant - |
33175 | 873 |
let ?U = "UNIV :: 'n set" |
874 |
let ?Uk = "?U - {k}" |
|
53854 | 875 |
have U: "?U = insert k ?Uk" |
876 |
by blast |
|
877 |
have kUk: "k \<notin> ?Uk" |
|
878 |
by simp |
|
33175 | 879 |
have th00: "\<And>k s. x$k *s row k A + s = (x$k - 1) *s row k A + row k A + s" |
36350 | 880 |
by (vector field_simps) |
53854 | 881 |
have th001: "\<And>f k . (\<lambda>x. if x = k then f k else f x) = f" |
882 |
by auto |
|
33175 | 883 |
have "(\<chi> i. row i A) = A" by (vector row_def) |
53253 | 884 |
then have thd1: "det (\<chi> i. row i A) = det A" |
885 |
by simp |
|
33175 | 886 |
have thd0: "det (\<chi> i. if i = k then row k A + (\<Sum>i \<in> ?Uk. x $ i *s row i A) else row i A) = det A" |
68134 | 887 |
by (force intro: det_row_span vec.span_sum vec.span_scale vec.span_base) |
33175 | 888 |
show "?lhs = x$k * det A" |
889 |
apply (subst U) |
|
68134 | 890 |
unfolding sum.insert[OF finite kUk] |
33175 | 891 |
apply (subst th00) |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
892 |
unfolding add.assoc |
33175 | 893 |
apply (subst det_row_add) |
894 |
unfolding thd0 |
|
895 |
unfolding det_row_mul |
|
896 |
unfolding th001[of k "\<lambda>i. row i A"] |
|
53253 | 897 |
unfolding thd1 |
898 |
apply (simp add: field_simps) |
|
899 |
done |
|
33175 | 900 |
qed |
901 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
902 |
lemma%important cramer_lemma: |
68263 | 903 |
fixes A :: "'a::{field}^'n^'n" |
904 |
shows "det((\<chi> i j. if j = k then (A *v x)$i else A$i$j):: 'a::{field}^'n^'n) = x$k * det A" |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
905 |
proof%unimportant - |
33175 | 906 |
let ?U = "UNIV :: 'n set" |
64267 | 907 |
have *: "\<And>c. sum (\<lambda>i. c i *s row i (transpose A)) ?U = sum (\<lambda>i. c i *s column i A) ?U" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
908 |
by (auto intro: sum.cong) |
53854 | 909 |
show ?thesis |
67673
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset
|
910 |
unfolding matrix_mult_sum |
53253 | 911 |
unfolding cramer_lemma_transpose[of k x "transpose A", unfolded det_transpose, symmetric] |
912 |
unfolding *[of "\<lambda>i. x$i"] |
|
913 |
apply (subst det_transpose[symmetric]) |
|
914 |
apply (rule cong[OF refl[of det]]) |
|
915 |
apply (vector transpose_def column_def row_def) |
|
916 |
done |
|
33175 | 917 |
qed |
918 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
919 |
lemma%important cramer: |
68263 | 920 |
fixes A ::"'a::{field}^'n^'n" |
33175 | 921 |
assumes d0: "det A \<noteq> 0" |
36362
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
35542
diff
changeset
|
922 |
shows "A *v x = b \<longleftrightarrow> x = (\<chi> k. det(\<chi> i j. if j=k then b$i else A$i$j) / det A)" |
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
923 |
proof%unimportant - |
33175 | 924 |
from d0 obtain B where B: "A ** B = mat 1" "B ** A = mat 1" |
53854 | 925 |
unfolding invertible_det_nz[symmetric] invertible_def |
926 |
by blast |
|
927 |
have "(A ** B) *v b = b" |
|
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
928 |
by (simp add: B) |
53854 | 929 |
then have "A *v (B *v b) = b" |
930 |
by (simp add: matrix_vector_mul_assoc) |
|
931 |
then have xe: "\<exists>x. A *v x = b" |
|
932 |
by blast |
|
53253 | 933 |
{ |
934 |
fix x |
|
935 |
assume x: "A *v x = b" |
|
936 |
have "x = (\<chi> k. det(\<chi> i j. if j=k then b$i else A$i$j) / det A)" |
|
937 |
unfolding x[symmetric] |
|
938 |
using d0 by (simp add: vec_eq_iff cramer_lemma field_simps) |
|
939 |
} |
|
53854 | 940 |
with xe show ?thesis |
941 |
by auto |
|
33175 | 942 |
qed |
943 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
944 |
subsection%important \<open>Orthogonality of a transformation and matrix\<close> |
33175 | 945 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
946 |
definition%important "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v w. f v \<bullet> f w = v \<bullet> w)" |
33175 | 947 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
948 |
definition%important "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow> |
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
949 |
transpose Q ** Q = mat 1 \<and> Q ** transpose Q = mat 1" |
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
950 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
951 |
lemma%unimportant orthogonal_transformation: |
67733
346cb74e79f6
generalized lemmas about orthogonal transformation
immler
parents:
67683
diff
changeset
|
952 |
"orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v. norm (f v) = norm v)" |
33175 | 953 |
unfolding orthogonal_transformation_def |
954 |
apply auto |
|
955 |
apply (erule_tac x=v in allE)+ |
|
35542 | 956 |
apply (simp add: norm_eq_sqrt_inner) |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
957 |
apply (simp add: dot_norm linear_add[symmetric]) |
53253 | 958 |
done |
33175 | 959 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
960 |
lemma%unimportant orthogonal_transformation_id [simp]: "orthogonal_transformation (\<lambda>x. x)" |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
961 |
by (simp add: linear_iff orthogonal_transformation_def) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
962 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
963 |
lemma%unimportant orthogonal_orthogonal_transformation: |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
964 |
"orthogonal_transformation f \<Longrightarrow> orthogonal (f x) (f y) \<longleftrightarrow> orthogonal x y" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
965 |
by (simp add: orthogonal_def orthogonal_transformation_def) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
966 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
967 |
lemma%unimportant orthogonal_transformation_compose: |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
968 |
"\<lbrakk>orthogonal_transformation f; orthogonal_transformation g\<rbrakk> \<Longrightarrow> orthogonal_transformation(f \<circ> g)" |
68138 | 969 |
by (auto simp: orthogonal_transformation_def linear_compose) |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
970 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
971 |
lemma%unimportant orthogonal_transformation_neg: |
67733
346cb74e79f6
generalized lemmas about orthogonal transformation
immler
parents:
67683
diff
changeset
|
972 |
"orthogonal_transformation(\<lambda>x. -(f x)) \<longleftrightarrow> orthogonal_transformation f" |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
973 |
by (auto simp: orthogonal_transformation_def dest: linear_compose_neg) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
974 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
975 |
lemma%unimportant orthogonal_transformation_scaleR: "orthogonal_transformation f \<Longrightarrow> f (c *\<^sub>R v) = c *\<^sub>R f v" |
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
976 |
by (simp add: linear_iff orthogonal_transformation_def) |
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
977 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
978 |
lemma%unimportant orthogonal_transformation_linear: |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
979 |
"orthogonal_transformation f \<Longrightarrow> linear f" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
980 |
by (simp add: orthogonal_transformation_def) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
981 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
982 |
lemma%unimportant orthogonal_transformation_inj: |
67733
346cb74e79f6
generalized lemmas about orthogonal transformation
immler
parents:
67683
diff
changeset
|
983 |
"orthogonal_transformation f \<Longrightarrow> inj f" |
346cb74e79f6
generalized lemmas about orthogonal transformation
immler
parents:
67683
diff
changeset
|
984 |
unfolding orthogonal_transformation_def inj_on_def |
346cb74e79f6
generalized lemmas about orthogonal transformation
immler
parents:
67683
diff
changeset
|
985 |
by (metis vector_eq) |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
986 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
987 |
lemma%unimportant orthogonal_transformation_surj: |
67733
346cb74e79f6
generalized lemmas about orthogonal transformation
immler
parents:
67683
diff
changeset
|
988 |
"orthogonal_transformation f \<Longrightarrow> surj f" |
346cb74e79f6
generalized lemmas about orthogonal transformation
immler
parents:
67683
diff
changeset
|
989 |
for f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space" |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
990 |
by (simp add: linear_injective_imp_surjective orthogonal_transformation_inj orthogonal_transformation_linear) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
991 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
992 |
lemma%unimportant orthogonal_transformation_bij: |
67733
346cb74e79f6
generalized lemmas about orthogonal transformation
immler
parents:
67683
diff
changeset
|
993 |
"orthogonal_transformation f \<Longrightarrow> bij f" |
346cb74e79f6
generalized lemmas about orthogonal transformation
immler
parents:
67683
diff
changeset
|
994 |
for f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space" |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
995 |
by (simp add: bij_def orthogonal_transformation_inj orthogonal_transformation_surj) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
996 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
997 |
lemma%unimportant orthogonal_transformation_inv: |
67733
346cb74e79f6
generalized lemmas about orthogonal transformation
immler
parents:
67683
diff
changeset
|
998 |
"orthogonal_transformation f \<Longrightarrow> orthogonal_transformation (inv f)" |
346cb74e79f6
generalized lemmas about orthogonal transformation
immler
parents:
67683
diff
changeset
|
999 |
for f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space" |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1000 |
by (metis (no_types, hide_lams) bijection.inv_right bijection_def inj_linear_imp_inv_linear orthogonal_transformation orthogonal_transformation_bij orthogonal_transformation_inj) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1001 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1002 |
lemma%unimportant orthogonal_transformation_norm: |
67733
346cb74e79f6
generalized lemmas about orthogonal transformation
immler
parents:
67683
diff
changeset
|
1003 |
"orthogonal_transformation f \<Longrightarrow> norm (f x) = norm x" |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1004 |
by (metis orthogonal_transformation) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1005 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1006 |
lemma%unimportant orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n) \<longleftrightarrow> transpose Q ** Q = mat 1" |
33175 | 1007 |
by (metis matrix_left_right_inverse orthogonal_matrix_def) |
1008 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1009 |
lemma%unimportant orthogonal_matrix_id: "orthogonal_matrix (mat 1 :: _^'n^'n)" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
1010 |
by (simp add: orthogonal_matrix_def) |
33175 | 1011 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1012 |
lemma%unimportant orthogonal_matrix_mul: |
34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34289
diff
changeset
|
1013 |
fixes A :: "real ^'n^'n" |
68143 | 1014 |
assumes "orthogonal_matrix A" "orthogonal_matrix B" |
33175 | 1015 |
shows "orthogonal_matrix(A ** B)" |
68143 | 1016 |
using assms |
1017 |
by (simp add: orthogonal_matrix matrix_transpose_mul matrix_left_right_inverse matrix_mul_assoc) |
|
33175 | 1018 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1019 |
lemma%important orthogonal_transformation_matrix: |
34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34289
diff
changeset
|
1020 |
fixes f:: "real^'n \<Rightarrow> real^'n" |
33175 | 1021 |
shows "orthogonal_transformation f \<longleftrightarrow> linear f \<and> orthogonal_matrix(matrix f)" |
1022 |
(is "?lhs \<longleftrightarrow> ?rhs") |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1023 |
proof%unimportant - |
33175 | 1024 |
let ?mf = "matrix f" |
1025 |
let ?ot = "orthogonal_transformation f" |
|
1026 |
let ?U = "UNIV :: 'n set" |
|
1027 |
have fU: "finite ?U" by simp |
|
1028 |
let ?m1 = "mat 1 :: real ^'n^'n" |
|
53253 | 1029 |
{ |
1030 |
assume ot: ?ot |
|
68134 | 1031 |
from ot have lf: "Vector_Spaces.linear ( *s) ( *s) f" and fd: "\<And>v w. f v \<bullet> f w = v \<bullet> w" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
1032 |
unfolding orthogonal_transformation_def orthogonal_matrix linear_def scalar_mult_eq_scaleR |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
1033 |
by blast+ |
53253 | 1034 |
{ |
1035 |
fix i j |
|
35150
082fa4bd403d
Rename transp to transpose in HOL-Multivariate_Analysis. (by himmelma)
hoelzl
parents:
35028
diff
changeset
|
1036 |
let ?A = "transpose ?mf ** ?mf" |
33175 | 1037 |
have th0: "\<And>b (x::'a::comm_ring_1). (if b then 1 else 0)*x = (if b then x else 0)" |
1038 |
"\<And>b (x::'a::comm_ring_1). x*(if b then 1 else 0) = (if b then x else 0)" |
|
1039 |
by simp_all |
|
68134 | 1040 |
from fd[of "axis i 1" "axis j 1", |
63170 | 1041 |
simplified matrix_works[OF lf, symmetric] dot_matrix_vector_mul] |
33175 | 1042 |
have "?A$i$j = ?m1 $ i $ j" |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
47108
diff
changeset
|
1043 |
by (simp add: inner_vec_def matrix_matrix_mult_def columnvector_def rowvector_def |
64267 | 1044 |
th0 sum.delta[OF fU] mat_def axis_def) |
53253 | 1045 |
} |
53854 | 1046 |
then have "orthogonal_matrix ?mf" |
1047 |
unfolding orthogonal_matrix |
|
53253 | 1048 |
by vector |
53854 | 1049 |
with lf have ?rhs |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
1050 |
unfolding linear_def scalar_mult_eq_scaleR |
53854 | 1051 |
by blast |
53253 | 1052 |
} |
33175 | 1053 |
moreover |
53253 | 1054 |
{ |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
1055 |
assume lf: "Vector_Spaces.linear ( *s) ( *s) f" and om: "orthogonal_matrix ?mf" |
33175 | 1056 |
from lf om have ?lhs |
68143 | 1057 |
unfolding orthogonal_matrix_def norm_eq orthogonal_transformation |
1058 |
apply (simp only: matrix_works[OF lf, symmetric] dot_matrix_vector_mul) |
|
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
1059 |
apply (simp add: dot_matrix_product linear_def scalar_mult_eq_scaleR) |
53253 | 1060 |
done |
1061 |
} |
|
53854 | 1062 |
ultimately show ?thesis |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
1063 |
by (auto simp: linear_def scalar_mult_eq_scaleR) |
33175 | 1064 |
qed |
1065 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1066 |
lemma%important det_orthogonal_matrix: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34291
diff
changeset
|
1067 |
fixes Q:: "'a::linordered_idom^'n^'n" |
33175 | 1068 |
assumes oQ: "orthogonal_matrix Q" |
1069 |
shows "det Q = 1 \<or> det Q = - 1" |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1070 |
proof%unimportant - |
68143 | 1071 |
have "Q ** transpose Q = mat 1" |
1072 |
by (metis oQ orthogonal_matrix_def) |
|
53253 | 1073 |
then have "det (Q ** transpose Q) = det (mat 1:: 'a^'n^'n)" |
1074 |
by simp |
|
1075 |
then have "det Q * det Q = 1" |
|
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
1076 |
by (simp add: det_mul) |
68143 | 1077 |
then show ?thesis |
1078 |
by (simp add: square_eq_1_iff) |
|
33175 | 1079 |
qed |
1080 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1081 |
lemma%important orthogonal_transformation_det [simp]: |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1082 |
fixes f :: "real^'n \<Rightarrow> real^'n" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1083 |
shows "orthogonal_transformation f \<Longrightarrow> \<bar>det (matrix f)\<bar> = 1" |
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1084 |
using%unimportant det_orthogonal_matrix orthogonal_transformation_matrix by fastforce |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1085 |
|
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1086 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1087 |
subsection%important \<open>Linearity of scaling, and hence isometry, that preserves origin\<close> |
53854 | 1088 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1089 |
lemma%important scaling_linear: |
67733
346cb74e79f6
generalized lemmas about orthogonal transformation
immler
parents:
67683
diff
changeset
|
1090 |
fixes f :: "'a::real_inner \<Rightarrow> 'a::real_inner" |
53253 | 1091 |
assumes f0: "f 0 = 0" |
1092 |
and fd: "\<forall>x y. dist (f x) (f y) = c * dist x y" |
|
33175 | 1093 |
shows "linear f" |
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1094 |
proof%unimportant - |
53253 | 1095 |
{ |
1096 |
fix v w |
|
68134 | 1097 |
have "norm (f x) = c * norm x" for x |
1098 |
by (metis dist_0_norm f0 fd) |
|
1099 |
then have "f v \<bullet> f w = c\<^sup>2 * (v \<bullet> w)" |
|
33175 | 1100 |
unfolding dot_norm_neg dist_norm[symmetric] |
68134 | 1101 |
by (simp add: fd power2_eq_square field_simps) |
1102 |
} |
|
1103 |
then show ?thesis |
|
67733
346cb74e79f6
generalized lemmas about orthogonal transformation
immler
parents:
67683
diff
changeset
|
1104 |
unfolding linear_iff vector_eq[where 'a="'a"] scalar_mult_eq_scaleR |
68134 | 1105 |
by (simp add: inner_add field_simps) |
33175 | 1106 |
qed |
1107 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1108 |
lemma%unimportant isometry_linear: |
67733
346cb74e79f6
generalized lemmas about orthogonal transformation
immler
parents:
67683
diff
changeset
|
1109 |
"f (0::'a::real_inner) = (0::'a) \<Longrightarrow> \<forall>x y. dist(f x) (f y) = dist x y \<Longrightarrow> linear f" |
53253 | 1110 |
by (rule scaling_linear[where c=1]) simp_all |
33175 | 1111 |
|
68134 | 1112 |
text \<open>Hence another formulation of orthogonal transformation\<close> |
33175 | 1113 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1114 |
lemma%important orthogonal_transformation_isometry: |
67733
346cb74e79f6
generalized lemmas about orthogonal transformation
immler
parents:
67683
diff
changeset
|
1115 |
"orthogonal_transformation f \<longleftrightarrow> f(0::'a::real_inner) = (0::'a) \<and> (\<forall>x y. dist(f x) (f y) = dist x y)" |
33175 | 1116 |
unfolding orthogonal_transformation |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1117 |
apply (auto simp: linear_0 isometry_linear) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1118 |
apply (metis (no_types, hide_lams) dist_norm linear_diff) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1119 |
by (metis dist_0_norm) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1120 |
|
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1121 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1122 |
lemma%unimportant image_orthogonal_transformation_ball: |
67733
346cb74e79f6
generalized lemmas about orthogonal transformation
immler
parents:
67683
diff
changeset
|
1123 |
fixes f :: "'a::euclidean_space \<Rightarrow> 'a" |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1124 |
assumes "orthogonal_transformation f" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1125 |
shows "f ` ball x r = ball (f x) r" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1126 |
proof (intro equalityI subsetI) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1127 |
fix y assume "y \<in> f ` ball x r" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1128 |
with assms show "y \<in> ball (f x) r" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1129 |
by (auto simp: orthogonal_transformation_isometry) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1130 |
next |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1131 |
fix y assume y: "y \<in> ball (f x) r" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1132 |
then obtain z where z: "y = f z" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1133 |
using assms orthogonal_transformation_surj by blast |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1134 |
with y assms show "y \<in> f ` ball x r" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1135 |
by (auto simp: orthogonal_transformation_isometry) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1136 |
qed |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1137 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1138 |
lemma%unimportant image_orthogonal_transformation_cball: |
67733
346cb74e79f6
generalized lemmas about orthogonal transformation
immler
parents:
67683
diff
changeset
|
1139 |
fixes f :: "'a::euclidean_space \<Rightarrow> 'a" |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1140 |
assumes "orthogonal_transformation f" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1141 |
shows "f ` cball x r = cball (f x) r" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1142 |
proof (intro equalityI subsetI) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1143 |
fix y assume "y \<in> f ` cball x r" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1144 |
with assms show "y \<in> cball (f x) r" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1145 |
by (auto simp: orthogonal_transformation_isometry) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1146 |
next |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1147 |
fix y assume y: "y \<in> cball (f x) r" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1148 |
then obtain z where z: "y = f z" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1149 |
using assms orthogonal_transformation_surj by blast |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1150 |
with y assms show "y \<in> f ` cball x r" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1151 |
by (auto simp: orthogonal_transformation_isometry) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1152 |
qed |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1153 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1154 |
subsection%important \<open> We can find an orthogonal matrix taking any unit vector to any other\<close> |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1155 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1156 |
lemma%unimportant orthogonal_matrix_transpose [simp]: |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1157 |
"orthogonal_matrix(transpose A) \<longleftrightarrow> orthogonal_matrix A" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1158 |
by (auto simp: orthogonal_matrix_def) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1159 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1160 |
lemma%unimportant orthogonal_matrix_orthonormal_columns: |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1161 |
fixes A :: "real^'n^'n" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1162 |
shows "orthogonal_matrix A \<longleftrightarrow> |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1163 |
(\<forall>i. norm(column i A) = 1) \<and> |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1164 |
(\<forall>i j. i \<noteq> j \<longrightarrow> orthogonal (column i A) (column j A))" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1165 |
by (auto simp: orthogonal_matrix matrix_mult_transpose_dot_column vec_eq_iff mat_def norm_eq_1 orthogonal_def) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1166 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1167 |
lemma%unimportant orthogonal_matrix_orthonormal_rows: |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1168 |
fixes A :: "real^'n^'n" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1169 |
shows "orthogonal_matrix A \<longleftrightarrow> |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1170 |
(\<forall>i. norm(row i A) = 1) \<and> |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1171 |
(\<forall>i j. i \<noteq> j \<longrightarrow> orthogonal (row i A) (row j A))" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1172 |
using orthogonal_matrix_orthonormal_columns [of "transpose A"] by simp |
33175 | 1173 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1174 |
lemma%important orthogonal_matrix_exists_basis: |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1175 |
fixes a :: "real^'n" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1176 |
assumes "norm a = 1" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1177 |
obtains A where "orthogonal_matrix A" "A *v (axis k 1) = a" |
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1178 |
proof%unimportant - |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1179 |
obtain S where "a \<in> S" "pairwise orthogonal S" and noS: "\<And>x. x \<in> S \<Longrightarrow> norm x = 1" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1180 |
and "independent S" "card S = CARD('n)" "span S = UNIV" |
68138 | 1181 |
using vector_in_orthonormal_basis assms by force |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
1182 |
then obtain f0 where "bij_betw f0 (UNIV::'n set) S" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
1183 |
by (metis finite_class.finite_UNIV finite_same_card_bij finiteI_independent) |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1184 |
then obtain f where f: "bij_betw f (UNIV::'n set) S" and a: "a = f k" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1185 |
using bij_swap_iff [of k "inv f0 a" f0] |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1186 |
by (metis UNIV_I \<open>a \<in> S\<close> bij_betw_inv_into_right bij_betw_swap_iff swap_apply1) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1187 |
show thesis |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1188 |
proof |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1189 |
have [simp]: "\<And>i. norm (f i) = 1" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1190 |
using bij_betwE [OF \<open>bij_betw f UNIV S\<close>] by (blast intro: noS) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1191 |
have [simp]: "\<And>i j. i \<noteq> j \<Longrightarrow> orthogonal (f i) (f j)" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1192 |
using \<open>pairwise orthogonal S\<close> \<open>bij_betw f UNIV S\<close> |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1193 |
by (auto simp: pairwise_def bij_betw_def inj_on_def) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1194 |
show "orthogonal_matrix (\<chi> i j. f j $ i)" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1195 |
by (simp add: orthogonal_matrix_orthonormal_columns column_def) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1196 |
show "(\<chi> i j. f j $ i) *v axis k 1 = a" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1197 |
by (simp add: matrix_vector_mult_def axis_def a if_distrib cong: if_cong) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1198 |
qed |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1199 |
qed |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1200 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1201 |
lemma%unimportant orthogonal_transformation_exists_1: |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1202 |
fixes a b :: "real^'n" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1203 |
assumes "norm a = 1" "norm b = 1" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1204 |
obtains f where "orthogonal_transformation f" "f a = b" |
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1205 |
proof%unimportant - |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1206 |
obtain k::'n where True |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1207 |
by simp |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1208 |
obtain A B where AB: "orthogonal_matrix A" "orthogonal_matrix B" and eq: "A *v (axis k 1) = a" "B *v (axis k 1) = b" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1209 |
using orthogonal_matrix_exists_basis assms by metis |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1210 |
let ?f = "\<lambda>x. (B ** transpose A) *v x" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1211 |
show thesis |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1212 |
proof |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1213 |
show "orthogonal_transformation ?f" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
1214 |
by (subst orthogonal_transformation_matrix) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
1215 |
(auto simp: AB orthogonal_matrix_mul) |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1216 |
next |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1217 |
show "?f a = b" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1218 |
using \<open>orthogonal_matrix A\<close> unfolding orthogonal_matrix_def |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1219 |
by (metis eq matrix_mul_rid matrix_vector_mul_assoc) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1220 |
qed |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1221 |
qed |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1222 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1223 |
lemma%important orthogonal_transformation_exists: |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1224 |
fixes a b :: "real^'n" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1225 |
assumes "norm a = norm b" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1226 |
obtains f where "orthogonal_transformation f" "f a = b" |
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1227 |
proof%unimportant (cases "a = 0 \<or> b = 0") |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1228 |
case True |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1229 |
with assms show ?thesis |
67733
346cb74e79f6
generalized lemmas about orthogonal transformation
immler
parents:
67683
diff
changeset
|
1230 |
using that by force |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1231 |
next |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1232 |
case False |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1233 |
then obtain f where f: "orthogonal_transformation f" and eq: "f (a /\<^sub>R norm a) = (b /\<^sub>R norm b)" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1234 |
by (auto intro: orthogonal_transformation_exists_1 [of "a /\<^sub>R norm a" "b /\<^sub>R norm b"]) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1235 |
show ?thesis |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1236 |
proof |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
1237 |
interpret linear f |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1238 |
using f by (simp add: orthogonal_transformation_linear) |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
1239 |
have "f a /\<^sub>R norm a = f (a /\<^sub>R norm a)" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
1240 |
by (simp add: scale) |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1241 |
also have "\<dots> = b /\<^sub>R norm a" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1242 |
by (simp add: eq assms [symmetric]) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1243 |
finally show "f a = b" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1244 |
using False by auto |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1245 |
qed (use f in auto) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1246 |
qed |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1247 |
|
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1248 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1249 |
subsection%important \<open>Can extend an isometry from unit sphere\<close> |
33175 | 1250 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1251 |
lemma%important isometry_sphere_extend: |
67733
346cb74e79f6
generalized lemmas about orthogonal transformation
immler
parents:
67683
diff
changeset
|
1252 |
fixes f:: "'a::real_inner \<Rightarrow> 'a" |
68143 | 1253 |
assumes f1: "\<And>x. norm x = 1 \<Longrightarrow> norm (f x) = 1" |
1254 |
and fd1: "\<And>x y. \<lbrakk>norm x = 1; norm y = 1\<rbrakk> \<Longrightarrow> dist (f x) (f y) = dist x y" |
|
33175 | 1255 |
shows "\<exists>g. orthogonal_transformation g \<and> (\<forall>x. norm x = 1 \<longrightarrow> g x = f x)" |
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1256 |
proof%unimportant - |
53253 | 1257 |
{ |
68143 | 1258 |
fix x y x' y' u v u' v' :: "'a" |
1259 |
assume H: "x = norm x *\<^sub>R u" "y = norm y *\<^sub>R v" |
|
1260 |
"x' = norm x *\<^sub>R u'" "y' = norm y *\<^sub>R v'" |
|
1261 |
and J: "norm u = 1" "norm u' = 1" "norm v = 1" "norm v' = 1" "norm(u' - v') = norm(u - v)" |
|
1262 |
then have *: "u \<bullet> v = u' \<bullet> v' + v' \<bullet> u' - v \<bullet> u " |
|
53253 | 1263 |
by (simp add: norm_eq norm_eq_1 inner_add inner_diff) |
68143 | 1264 |
have "norm (norm x *\<^sub>R u' - norm y *\<^sub>R v') = norm (norm x *\<^sub>R u - norm y *\<^sub>R v)" |
1265 |
using J by (simp add: norm_eq norm_eq_1 inner_diff * field_simps) |
|
1266 |
then have "norm(x' - y') = norm(x - y)" |
|
1267 |
using H by metis |
|
53253 | 1268 |
} |
68143 | 1269 |
note norm_eq = this |
1270 |
let ?g = "\<lambda>x. if x = 0 then 0 else norm x *\<^sub>R f (x /\<^sub>R norm x)" |
|
1271 |
have thfg: "?g x = f x" if "norm x = 1" for x |
|
1272 |
using that by auto |
|
1273 |
have thd: "dist (?g x) (?g y) = dist x y" for x y |
|
1274 |
proof (cases "x=0 \<or> y=0") |
|
1275 |
case False |
|
1276 |
show "dist (?g x) (?g y) = dist x y" |
|
1277 |
unfolding dist_norm |
|
1278 |
proof (rule norm_eq) |
|
1279 |
show "x = norm x *\<^sub>R (x /\<^sub>R norm x)" "y = norm y *\<^sub>R (y /\<^sub>R norm y)" |
|
1280 |
"norm (f (x /\<^sub>R norm x)) = 1" "norm (f (y /\<^sub>R norm y)) = 1" |
|
1281 |
using False f1 by auto |
|
1282 |
qed (use False in \<open>auto simp: field_simps intro: f1 fd1[unfolded dist_norm]\<close>) |
|
1283 |
qed (auto simp: f1) |
|
1284 |
show ?thesis |
|
33175 | 1285 |
unfolding orthogonal_transformation_isometry |
68143 | 1286 |
by (rule exI[where x= ?g]) (metis thfg thd) |
33175 | 1287 |
qed |
1288 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1289 |
subsection%important \<open>Rotation, reflection, rotoinversion\<close> |
33175 | 1290 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1291 |
definition%important "rotation_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = 1" |
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1292 |
definition%important "rotoinversion_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = - 1" |
33175 | 1293 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1294 |
lemma%important orthogonal_rotation_or_rotoinversion: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34291
diff
changeset
|
1295 |
fixes Q :: "'a::linordered_idom^'n^'n" |
33175 | 1296 |
shows " orthogonal_matrix Q \<longleftrightarrow> rotation_matrix Q \<or> rotoinversion_matrix Q" |
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1297 |
by%unimportant (metis rotoinversion_matrix_def rotation_matrix_def det_orthogonal_matrix) |
53253 | 1298 |
|
68134 | 1299 |
text \<open>Explicit formulas for low dimensions\<close> |
33175 | 1300 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1301 |
lemma%unimportant prod_neutral_const: "prod f {(1::nat)..1} = f 1" |
61286 | 1302 |
by simp |
33175 | 1303 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1304 |
lemma%unimportant prod_2: "prod f {(1::nat)..2} = f 1 * f 2" |
61286 | 1305 |
by (simp add: eval_nat_numeral atLeastAtMostSuc_conv mult.commute) |
53253 | 1306 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1307 |
lemma%unimportant prod_3: "prod f {(1::nat)..3} = f 1 * f 2 * f 3" |
61286 | 1308 |
by (simp add: eval_nat_numeral atLeastAtMostSuc_conv mult.commute) |
33175 | 1309 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1310 |
lemma%unimportant det_1: "det (A::'a::comm_ring_1^1^1) = A$1$1" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
1311 |
by (simp add: det_def sign_id) |
33175 | 1312 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1313 |
lemma%unimportant det_2: "det (A::'a::comm_ring_1^2^2) = A$1$1 * A$2$2 - A$1$2 * A$2$1" |
53253 | 1314 |
proof - |
33175 | 1315 |
have f12: "finite {2::2}" "1 \<notin> {2::2}" by auto |
1316 |
show ?thesis |
|
53253 | 1317 |
unfolding det_def UNIV_2 |
64267 | 1318 |
unfolding sum_over_permutations_insert[OF f12] |
53253 | 1319 |
unfolding permutes_sing |
1320 |
by (simp add: sign_swap_id sign_id swap_id_eq) |
|
33175 | 1321 |
qed |
1322 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1323 |
lemma%unimportant det_3: |
53253 | 1324 |
"det (A::'a::comm_ring_1^3^3) = |
1325 |
A$1$1 * A$2$2 * A$3$3 + |
|
1326 |
A$1$2 * A$2$3 * A$3$1 + |
|
1327 |
A$1$3 * A$2$1 * A$3$2 - |
|
1328 |
A$1$1 * A$2$3 * A$3$2 - |
|
1329 |
A$1$2 * A$2$1 * A$3$3 - |
|
1330 |
A$1$3 * A$2$2 * A$3$1" |
|
1331 |
proof - |
|
53854 | 1332 |
have f123: "finite {2::3, 3}" "1 \<notin> {2::3, 3}" |
1333 |
by auto |
|
1334 |
have f23: "finite {3::3}" "2 \<notin> {3::3}" |
|
1335 |
by auto |
|
33175 | 1336 |
|
1337 |
show ?thesis |
|
53253 | 1338 |
unfolding det_def UNIV_3 |
64267 | 1339 |
unfolding sum_over_permutations_insert[OF f123] |
1340 |
unfolding sum_over_permutations_insert[OF f23] |
|
53253 | 1341 |
unfolding permutes_sing |
1342 |
by (simp add: sign_swap_id permutation_swap_id sign_compose sign_id swap_id_eq) |
|
33175 | 1343 |
qed |
1344 |
||
68134 | 1345 |
text\<open> Slightly stronger results giving rotation, but only in two or more dimensions\<close> |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1346 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1347 |
lemma%unimportant rotation_matrix_exists_basis: |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1348 |
fixes a :: "real^'n" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1349 |
assumes 2: "2 \<le> CARD('n)" and "norm a = 1" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1350 |
obtains A where "rotation_matrix A" "A *v (axis k 1) = a" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1351 |
proof - |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1352 |
obtain A where "orthogonal_matrix A" and A: "A *v (axis k 1) = a" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1353 |
using orthogonal_matrix_exists_basis assms by metis |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1354 |
with orthogonal_rotation_or_rotoinversion |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1355 |
consider "rotation_matrix A" | "rotoinversion_matrix A" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1356 |
by metis |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1357 |
then show thesis |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1358 |
proof cases |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1359 |
assume "rotation_matrix A" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1360 |
then show ?thesis |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1361 |
using \<open>A *v axis k 1 = a\<close> that by auto |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1362 |
next |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1363 |
obtain j where "j \<noteq> k" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1364 |
by (metis (full_types) 2 card_2_exists ex_card) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1365 |
let ?TA = "transpose A" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1366 |
let ?A = "\<chi> i. if i = j then - 1 *\<^sub>R (?TA $ i) else ?TA $i" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1367 |
assume "rotoinversion_matrix A" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1368 |
then have [simp]: "det A = -1" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1369 |
by (simp add: rotoinversion_matrix_def) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1370 |
show ?thesis |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1371 |
proof |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1372 |
have [simp]: "row i (\<chi> i. if i = j then - 1 *\<^sub>R ?TA $ i else ?TA $ i) = (if i = j then - row i ?TA else row i ?TA)" for i |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1373 |
by (auto simp: row_def) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1374 |
have "orthogonal_matrix ?A" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1375 |
unfolding orthogonal_matrix_orthonormal_rows |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1376 |
using \<open>orthogonal_matrix A\<close> by (auto simp: orthogonal_matrix_orthonormal_columns orthogonal_clauses) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1377 |
then show "rotation_matrix (transpose ?A)" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1378 |
unfolding rotation_matrix_def |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1379 |
by (simp add: det_row_mul[of j _ "\<lambda>i. ?TA $ i", unfolded scalar_mult_eq_scaleR]) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1380 |
show "transpose ?A *v axis k 1 = a" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1381 |
using \<open>j \<noteq> k\<close> A by (simp add: matrix_vector_column axis_def scalar_mult_eq_scaleR if_distrib [of "\<lambda>z. z *\<^sub>R c" for c] cong: if_cong) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1382 |
qed |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1383 |
qed |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1384 |
qed |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1385 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1386 |
lemma%unimportant rotation_exists_1: |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1387 |
fixes a :: "real^'n" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1388 |
assumes "2 \<le> CARD('n)" "norm a = 1" "norm b = 1" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1389 |
obtains f where "orthogonal_transformation f" "det(matrix f) = 1" "f a = b" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1390 |
proof - |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1391 |
obtain k::'n where True |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1392 |
by simp |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1393 |
obtain A B where AB: "rotation_matrix A" "rotation_matrix B" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1394 |
and eq: "A *v (axis k 1) = a" "B *v (axis k 1) = b" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1395 |
using rotation_matrix_exists_basis assms by metis |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1396 |
let ?f = "\<lambda>x. (B ** transpose A) *v x" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1397 |
show thesis |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1398 |
proof |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1399 |
show "orthogonal_transformation ?f" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1400 |
using AB orthogonal_matrix_mul orthogonal_transformation_matrix rotation_matrix_def matrix_vector_mul_linear by force |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1401 |
show "det (matrix ?f) = 1" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1402 |
using AB by (auto simp: det_mul rotation_matrix_def) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1403 |
show "?f a = b" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1404 |
using AB unfolding orthogonal_matrix_def rotation_matrix_def |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1405 |
by (metis eq matrix_mul_rid matrix_vector_mul_assoc) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1406 |
qed |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1407 |
qed |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1408 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1409 |
lemma%unimportant rotation_exists: |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1410 |
fixes a :: "real^'n" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1411 |
assumes 2: "2 \<le> CARD('n)" and eq: "norm a = norm b" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1412 |
obtains f where "orthogonal_transformation f" "det(matrix f) = 1" "f a = b" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1413 |
proof (cases "a = 0 \<or> b = 0") |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1414 |
case True |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1415 |
with assms have "a = 0" "b = 0" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1416 |
by auto |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1417 |
then show ?thesis |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1418 |
by (metis eq_id_iff matrix_id orthogonal_transformation_id that) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1419 |
next |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1420 |
case False |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
1421 |
then obtain f where f: "orthogonal_transformation f" "det (matrix f) = 1" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
1422 |
and f': "f (a /\<^sub>R norm a) = b /\<^sub>R norm b" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
1423 |
using rotation_exists_1 [of "a /\<^sub>R norm a" "b /\<^sub>R norm b", OF 2] by auto |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
1424 |
then interpret linear f by (simp add: orthogonal_transformation) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
1425 |
have "f a = b" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
1426 |
using f' False |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
1427 |
by (simp add: eq scale) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
1428 |
with f show thesis .. |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1429 |
qed |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1430 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68263
diff
changeset
|
1431 |
lemma%unimportant rotation_rightward_line: |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1432 |
fixes a :: "real^'n" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1433 |
obtains f where "orthogonal_transformation f" "2 \<le> CARD('n) \<Longrightarrow> det(matrix f) = 1" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1434 |
"f(norm a *\<^sub>R axis k 1) = a" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1435 |
proof (cases "CARD('n) = 1") |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1436 |
case True |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1437 |
obtain f where "orthogonal_transformation f" "f (norm a *\<^sub>R axis k (1::real)) = a" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1438 |
proof (rule orthogonal_transformation_exists) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1439 |
show "norm (norm a *\<^sub>R axis k (1::real)) = norm a" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1440 |
by simp |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1441 |
qed auto |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1442 |
then show thesis |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1443 |
using True that by auto |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1444 |
next |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1445 |
case False |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1446 |
obtain f where "orthogonal_transformation f" "det(matrix f) = 1" "f (norm a *\<^sub>R axis k 1) = a" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1447 |
proof (rule rotation_exists) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1448 |
show "2 \<le> CARD('n)" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1449 |
using False one_le_card_finite [where 'a='n] by linarith |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1450 |
show "norm (norm a *\<^sub>R axis k (1::real)) = norm a" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1451 |
by simp |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1452 |
qed auto |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1453 |
then show thesis |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1454 |
using that by blast |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1455 |
qed |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1456 |
|
33175 | 1457 |
end |