1 (* Title: Determinants |
|
2 Author: Amine Chaieb, University of Cambridge |
|
3 *) |
|
4 |
|
5 header {* Traces, Determinant of square matrices and some properties *} |
|
6 |
|
7 theory Determinants |
|
8 imports Euclidean_Space Permutations |
|
9 begin |
|
10 |
|
11 subsection{* First some facts about products*} |
|
12 lemma setprod_insert_eq: "finite A \<Longrightarrow> setprod f (insert a A) = (if a \<in> A then setprod f A else f a * setprod f A)" |
|
13 apply clarsimp |
|
14 by(subgoal_tac "insert a A = A", auto) |
|
15 |
|
16 lemma setprod_add_split: |
|
17 assumes mn: "(m::nat) <= n + 1" |
|
18 shows "setprod f {m.. n+p} = setprod f {m .. n} * setprod f {n+1..n+p}" |
|
19 proof- |
|
20 let ?A = "{m .. n+p}" |
|
21 let ?B = "{m .. n}" |
|
22 let ?C = "{n+1..n+p}" |
|
23 from mn have un: "?B \<union> ?C = ?A" by auto |
|
24 from mn have dj: "?B \<inter> ?C = {}" by auto |
|
25 have f: "finite ?B" "finite ?C" by simp_all |
|
26 from setprod_Un_disjoint[OF f dj, of f, unfolded un] show ?thesis . |
|
27 qed |
|
28 |
|
29 |
|
30 lemma setprod_offset: "setprod f {(m::nat) + p .. n + p} = setprod (\<lambda>i. f (i + p)) {m..n}" |
|
31 apply (rule setprod_reindex_cong[where f="op + p"]) |
|
32 apply (auto simp add: image_iff Bex_def inj_on_def) |
|
33 apply arith |
|
34 apply (rule ext) |
|
35 apply (simp add: add_commute) |
|
36 done |
|
37 |
|
38 lemma setprod_singleton: "setprod f {x} = f x" by simp |
|
39 |
|
40 lemma setprod_singleton_nat_seg: "setprod f {n..n} = f (n::'a::order)" by simp |
|
41 |
|
42 lemma setprod_numseg: "setprod f {m..0} = (if m=0 then f 0 else 1)" |
|
43 "setprod f {m .. Suc n} = (if m \<le> Suc n then f (Suc n) * setprod f {m..n} |
|
44 else setprod f {m..n})" |
|
45 by (auto simp add: atLeastAtMostSuc_conv) |
|
46 |
|
47 lemma setprod_le: assumes fS: "finite S" and fg: "\<forall>x\<in>S. f x \<ge> 0 \<and> f x \<le> (g x :: 'a::ordered_idom)" |
|
48 shows "setprod f S \<le> setprod g S" |
|
49 using fS fg |
|
50 apply(induct S) |
|
51 apply simp |
|
52 apply auto |
|
53 apply (rule mult_mono) |
|
54 apply (auto intro: setprod_nonneg) |
|
55 done |
|
56 |
|
57 (* FIXME: In Finite_Set there is a useless further assumption *) |
|
58 lemma setprod_inversef: "finite A ==> setprod (inverse \<circ> f) A = (inverse (setprod f A) :: 'a:: {division_by_zero, field})" |
|
59 apply (erule finite_induct) |
|
60 apply (simp) |
|
61 apply simp |
|
62 done |
|
63 |
|
64 lemma setprod_le_1: assumes fS: "finite S" and f: "\<forall>x\<in>S. f x \<ge> 0 \<and> f x \<le> (1::'a::ordered_idom)" |
|
65 shows "setprod f S \<le> 1" |
|
66 using setprod_le[OF fS f] unfolding setprod_1 . |
|
67 |
|
68 subsection{* Trace *} |
|
69 |
|
70 definition trace :: "'a::semiring_1^'n^'n \<Rightarrow> 'a" where |
|
71 "trace A = setsum (\<lambda>i. ((A$i)$i)) (UNIV::'n set)" |
|
72 |
|
73 lemma trace_0: "trace(mat 0) = 0" |
|
74 by (simp add: trace_def mat_def) |
|
75 |
|
76 lemma trace_I: "trace(mat 1 :: 'a::semiring_1^'n^'n) = of_nat(CARD('n))" |
|
77 by (simp add: trace_def mat_def) |
|
78 |
|
79 lemma trace_add: "trace ((A::'a::comm_semiring_1^'n^'n) + B) = trace A + trace B" |
|
80 by (simp add: trace_def setsum_addf) |
|
81 |
|
82 lemma trace_sub: "trace ((A::'a::comm_ring_1^'n^'n) - B) = trace A - trace B" |
|
83 by (simp add: trace_def setsum_subtractf) |
|
84 |
|
85 lemma trace_mul_sym:"trace ((A::'a::comm_semiring_1^'n^'n) ** B) = trace (B**A)" |
|
86 apply (simp add: trace_def matrix_matrix_mult_def) |
|
87 apply (subst setsum_commute) |
|
88 by (simp add: mult_commute) |
|
89 |
|
90 (* ------------------------------------------------------------------------- *) |
|
91 (* Definition of determinant. *) |
|
92 (* ------------------------------------------------------------------------- *) |
|
93 |
|
94 definition det:: "'a::comm_ring_1^'n^'n \<Rightarrow> 'a" where |
|
95 "det A = setsum (\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A$i$p i) (UNIV :: 'n set)) {p. p permutes (UNIV :: 'n set)}" |
|
96 |
|
97 (* ------------------------------------------------------------------------- *) |
|
98 (* A few general lemmas we need below. *) |
|
99 (* ------------------------------------------------------------------------- *) |
|
100 |
|
101 lemma setprod_permute: |
|
102 assumes p: "p permutes S" |
|
103 shows "setprod f S = setprod (f o p) S" |
|
104 proof- |
|
105 {assume "\<not> finite S" hence ?thesis by simp} |
|
106 moreover |
|
107 {assume fS: "finite S" |
|
108 then have ?thesis |
|
109 apply (simp add: setprod_def cong del:strong_setprod_cong) |
|
110 apply (rule ab_semigroup_mult.fold_image_permute) |
|
111 apply (auto simp add: p) |
|
112 apply unfold_locales |
|
113 done} |
|
114 ultimately show ?thesis by blast |
|
115 qed |
|
116 |
|
117 lemma setproduct_permute_nat_interval: "p permutes {m::nat .. n} ==> setprod f {m..n} = setprod (f o p) {m..n}" |
|
118 by (blast intro!: setprod_permute) |
|
119 |
|
120 (* ------------------------------------------------------------------------- *) |
|
121 (* Basic determinant properties. *) |
|
122 (* ------------------------------------------------------------------------- *) |
|
123 |
|
124 lemma det_transp: "det (transp A) = det (A::'a::comm_ring_1 ^'n^'n::finite)" |
|
125 proof- |
|
126 let ?di = "\<lambda>A i j. A$i$j" |
|
127 let ?U = "(UNIV :: 'n set)" |
|
128 have fU: "finite ?U" by simp |
|
129 {fix p assume p: "p \<in> {p. p permutes ?U}" |
|
130 from p have pU: "p permutes ?U" by blast |
|
131 have sth: "sign (inv p) = sign p" |
|
132 by (metis sign_inverse fU p mem_def Collect_def permutation_permutes) |
|
133 from permutes_inj[OF pU] |
|
134 have pi: "inj_on p ?U" by (blast intro: subset_inj_on) |
|
135 from permutes_image[OF pU] |
|
136 have "setprod (\<lambda>i. ?di (transp A) i (inv p i)) ?U = setprod (\<lambda>i. ?di (transp A) i (inv p i)) (p ` ?U)" by simp |
|
137 also have "\<dots> = setprod ((\<lambda>i. ?di (transp A) i (inv p i)) o p) ?U" |
|
138 unfolding setprod_reindex[OF pi] .. |
|
139 also have "\<dots> = setprod (\<lambda>i. ?di A i (p i)) ?U" |
|
140 proof- |
|
141 {fix i assume i: "i \<in> ?U" |
|
142 from i permutes_inv_o[OF pU] permutes_in_image[OF pU] |
|
143 have "((\<lambda>i. ?di (transp A) i (inv p i)) o p) i = ?di A i (p i)" |
|
144 unfolding transp_def by (simp add: expand_fun_eq)} |
|
145 then show "setprod ((\<lambda>i. ?di (transp A) i (inv p i)) o p) ?U = setprod (\<lambda>i. ?di A i (p i)) ?U" by (auto intro: setprod_cong) |
|
146 qed |
|
147 finally have "of_int (sign (inv p)) * (setprod (\<lambda>i. ?di (transp A) i (inv p i)) ?U) = of_int (sign p) * (setprod (\<lambda>i. ?di A i (p i)) ?U)" using sth |
|
148 by simp} |
|
149 then show ?thesis unfolding det_def apply (subst setsum_permutations_inverse) |
|
150 apply (rule setsum_cong2) by blast |
|
151 qed |
|
152 |
|
153 lemma det_lowerdiagonal: |
|
154 fixes A :: "'a::comm_ring_1^'n^'n::{finite,wellorder}" |
|
155 assumes ld: "\<And>i j. i < j \<Longrightarrow> A$i$j = 0" |
|
156 shows "det A = setprod (\<lambda>i. A$i$i) (UNIV:: 'n set)" |
|
157 proof- |
|
158 let ?U = "UNIV:: 'n set" |
|
159 let ?PU = "{p. p permutes ?U}" |
|
160 let ?pp = "\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A$i$p i) (UNIV :: 'n set)" |
|
161 have fU: "finite ?U" by simp |
|
162 from finite_permutations[OF fU] have fPU: "finite ?PU" . |
|
163 have id0: "{id} \<subseteq> ?PU" by (auto simp add: permutes_id) |
|
164 {fix p assume p: "p \<in> ?PU -{id}" |
|
165 from p have pU: "p permutes ?U" and pid: "p \<noteq> id" by blast+ |
|
166 from permutes_natset_le[OF pU] pid obtain i where |
|
167 i: "p i > i" by (metis not_le) |
|
168 from ld[OF i] have ex:"\<exists>i \<in> ?U. A$i$p i = 0" by blast |
|
169 from setprod_zero[OF fU ex] have "?pp p = 0" by simp} |
|
170 then have p0: "\<forall>p \<in> ?PU -{id}. ?pp p = 0" by blast |
|
171 from setsum_mono_zero_cong_left[OF fPU id0 p0] show ?thesis |
|
172 unfolding det_def by (simp add: sign_id) |
|
173 qed |
|
174 |
|
175 lemma det_upperdiagonal: |
|
176 fixes A :: "'a::comm_ring_1^'n^'n::{finite,wellorder}" |
|
177 assumes ld: "\<And>i j. i > j \<Longrightarrow> A$i$j = 0" |
|
178 shows "det A = setprod (\<lambda>i. A$i$i) (UNIV:: 'n set)" |
|
179 proof- |
|
180 let ?U = "UNIV:: 'n set" |
|
181 let ?PU = "{p. p permutes ?U}" |
|
182 let ?pp = "(\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A$i$p i) (UNIV :: 'n set))" |
|
183 have fU: "finite ?U" by simp |
|
184 from finite_permutations[OF fU] have fPU: "finite ?PU" . |
|
185 have id0: "{id} \<subseteq> ?PU" by (auto simp add: permutes_id) |
|
186 {fix p assume p: "p \<in> ?PU -{id}" |
|
187 from p have pU: "p permutes ?U" and pid: "p \<noteq> id" by blast+ |
|
188 from permutes_natset_ge[OF pU] pid obtain i where |
|
189 i: "p i < i" by (metis not_le) |
|
190 from ld[OF i] have ex:"\<exists>i \<in> ?U. A$i$p i = 0" by blast |
|
191 from setprod_zero[OF fU ex] have "?pp p = 0" by simp} |
|
192 then have p0: "\<forall>p \<in> ?PU -{id}. ?pp p = 0" by blast |
|
193 from setsum_mono_zero_cong_left[OF fPU id0 p0] show ?thesis |
|
194 unfolding det_def by (simp add: sign_id) |
|
195 qed |
|
196 |
|
197 lemma det_diagonal: |
|
198 fixes A :: "'a::comm_ring_1^'n^'n::finite" |
|
199 assumes ld: "\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0" |
|
200 shows "det A = setprod (\<lambda>i. A$i$i) (UNIV::'n set)" |
|
201 proof- |
|
202 let ?U = "UNIV:: 'n set" |
|
203 let ?PU = "{p. p permutes ?U}" |
|
204 let ?pp = "\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A$i$p i) (UNIV :: 'n set)" |
|
205 have fU: "finite ?U" by simp |
|
206 from finite_permutations[OF fU] have fPU: "finite ?PU" . |
|
207 have id0: "{id} \<subseteq> ?PU" by (auto simp add: permutes_id) |
|
208 {fix p assume p: "p \<in> ?PU - {id}" |
|
209 then have "p \<noteq> id" by simp |
|
210 then obtain i where i: "p i \<noteq> i" unfolding expand_fun_eq by auto |
|
211 from ld [OF i [symmetric]] have ex:"\<exists>i \<in> ?U. A$i$p i = 0" by blast |
|
212 from setprod_zero [OF fU ex] have "?pp p = 0" by simp} |
|
213 then have p0: "\<forall>p \<in> ?PU - {id}. ?pp p = 0" by blast |
|
214 from setsum_mono_zero_cong_left[OF fPU id0 p0] show ?thesis |
|
215 unfolding det_def by (simp add: sign_id) |
|
216 qed |
|
217 |
|
218 lemma det_I: "det (mat 1 :: 'a::comm_ring_1^'n^'n::finite) = 1" |
|
219 proof- |
|
220 let ?A = "mat 1 :: 'a::comm_ring_1^'n^'n" |
|
221 let ?U = "UNIV :: 'n set" |
|
222 let ?f = "\<lambda>i j. ?A$i$j" |
|
223 {fix i assume i: "i \<in> ?U" |
|
224 have "?f i i = 1" using i by (vector mat_def)} |
|
225 hence th: "setprod (\<lambda>i. ?f i i) ?U = setprod (\<lambda>x. 1) ?U" |
|
226 by (auto intro: setprod_cong) |
|
227 {fix i j assume i: "i \<in> ?U" and j: "j \<in> ?U" and ij: "i \<noteq> j" |
|
228 have "?f i j = 0" using i j ij by (vector mat_def) } |
|
229 then have "det ?A = setprod (\<lambda>i. ?f i i) ?U" using det_diagonal |
|
230 by blast |
|
231 also have "\<dots> = 1" unfolding th setprod_1 .. |
|
232 finally show ?thesis . |
|
233 qed |
|
234 |
|
235 lemma det_0: "det (mat 0 :: 'a::comm_ring_1^'n^'n::finite) = 0" |
|
236 by (simp add: det_def setprod_zero) |
|
237 |
|
238 lemma det_permute_rows: |
|
239 fixes A :: "'a::comm_ring_1^'n^'n::finite" |
|
240 assumes p: "p permutes (UNIV :: 'n::finite set)" |
|
241 shows "det(\<chi> i. A$p i :: 'a^'n^'n) = of_int (sign p) * det A" |
|
242 apply (simp add: det_def setsum_right_distrib mult_assoc[symmetric]) |
|
243 apply (subst sum_permutations_compose_right[OF p]) |
|
244 proof(rule setsum_cong2) |
|
245 let ?U = "UNIV :: 'n set" |
|
246 let ?PU = "{p. p permutes ?U}" |
|
247 fix q assume qPU: "q \<in> ?PU" |
|
248 have fU: "finite ?U" by simp |
|
249 from qPU have q: "q permutes ?U" by blast |
|
250 from p q have pp: "permutation p" and qp: "permutation q" |
|
251 by (metis fU permutation_permutes)+ |
|
252 from permutes_inv[OF p] have ip: "inv p permutes ?U" . |
|
253 have "setprod (\<lambda>i. A$p i$ (q o p) i) ?U = setprod ((\<lambda>i. A$p i$(q o p) i) o inv p) ?U" |
|
254 by (simp only: setprod_permute[OF ip, symmetric]) |
|
255 also have "\<dots> = setprod (\<lambda>i. A $ (p o inv p) i $ (q o (p o inv p)) i) ?U" |
|
256 by (simp only: o_def) |
|
257 also have "\<dots> = setprod (\<lambda>i. A$i$q i) ?U" by (simp only: o_def permutes_inverses[OF p]) |
|
258 finally have thp: "setprod (\<lambda>i. A$p i$ (q o p) i) ?U = setprod (\<lambda>i. A$i$q i) ?U" |
|
259 by blast |
|
260 show "of_int (sign (q o p)) * setprod (\<lambda>i. A$ p i$ (q o p) i) ?U = of_int (sign p) * of_int (sign q) * setprod (\<lambda>i. A$i$q i) ?U" |
|
261 by (simp only: thp sign_compose[OF qp pp] mult_commute of_int_mult) |
|
262 qed |
|
263 |
|
264 lemma det_permute_columns: |
|
265 fixes A :: "'a::comm_ring_1^'n^'n::finite" |
|
266 assumes p: "p permutes (UNIV :: 'n set)" |
|
267 shows "det(\<chi> i j. A$i$ p j :: 'a^'n^'n) = of_int (sign p) * det A" |
|
268 proof- |
|
269 let ?Ap = "\<chi> i j. A$i$ p j :: 'a^'n^'n" |
|
270 let ?At = "transp A" |
|
271 have "of_int (sign p) * det A = det (transp (\<chi> i. transp A $ p i))" |
|
272 unfolding det_permute_rows[OF p, of ?At] det_transp .. |
|
273 moreover |
|
274 have "?Ap = transp (\<chi> i. transp A $ p i)" |
|
275 by (simp add: transp_def Cart_eq) |
|
276 ultimately show ?thesis by simp |
|
277 qed |
|
278 |
|
279 lemma det_identical_rows: |
|
280 fixes A :: "'a::ordered_idom^'n^'n::finite" |
|
281 assumes ij: "i \<noteq> j" |
|
282 and r: "row i A = row j A" |
|
283 shows "det A = 0" |
|
284 proof- |
|
285 have tha: "\<And>(a::'a) b. a = b ==> b = - a ==> a = 0" |
|
286 by simp |
|
287 have th1: "of_int (-1) = - 1" by (metis of_int_1 of_int_minus number_of_Min) |
|
288 let ?p = "Fun.swap i j id" |
|
289 let ?A = "\<chi> i. A $ ?p i" |
|
290 from r have "A = ?A" by (simp add: Cart_eq row_def swap_def) |
|
291 hence "det A = det ?A" by simp |
|
292 moreover have "det A = - det ?A" |
|
293 by (simp add: det_permute_rows[OF permutes_swap_id] sign_swap_id ij th1) |
|
294 ultimately show "det A = 0" by (metis tha) |
|
295 qed |
|
296 |
|
297 lemma det_identical_columns: |
|
298 fixes A :: "'a::ordered_idom^'n^'n::finite" |
|
299 assumes ij: "i \<noteq> j" |
|
300 and r: "column i A = column j A" |
|
301 shows "det A = 0" |
|
302 apply (subst det_transp[symmetric]) |
|
303 apply (rule det_identical_rows[OF ij]) |
|
304 by (metis row_transp r) |
|
305 |
|
306 lemma det_zero_row: |
|
307 fixes A :: "'a::{idom, ring_char_0}^'n^'n::finite" |
|
308 assumes r: "row i A = 0" |
|
309 shows "det A = 0" |
|
310 using r |
|
311 apply (simp add: row_def det_def Cart_eq) |
|
312 apply (rule setsum_0') |
|
313 apply (auto simp: sign_nz) |
|
314 done |
|
315 |
|
316 lemma det_zero_column: |
|
317 fixes A :: "'a::{idom,ring_char_0}^'n^'n::finite" |
|
318 assumes r: "column i A = 0" |
|
319 shows "det A = 0" |
|
320 apply (subst det_transp[symmetric]) |
|
321 apply (rule det_zero_row [of i]) |
|
322 by (metis row_transp r) |
|
323 |
|
324 lemma det_row_add: |
|
325 fixes a b c :: "'n::finite \<Rightarrow> _ ^ 'n" |
|
326 shows "det((\<chi> i. if i = k then a i + b i else c i)::'a::comm_ring_1^'n^'n) = |
|
327 det((\<chi> i. if i = k then a i else c i)::'a::comm_ring_1^'n^'n) + |
|
328 det((\<chi> i. if i = k then b i else c i)::'a::comm_ring_1^'n^'n)" |
|
329 unfolding det_def Cart_lambda_beta setsum_addf[symmetric] |
|
330 proof (rule setsum_cong2) |
|
331 let ?U = "UNIV :: 'n set" |
|
332 let ?pU = "{p. p permutes ?U}" |
|
333 let ?f = "(\<lambda>i. if i = k then a i + b i else c i)::'n \<Rightarrow> 'a::comm_ring_1^'n" |
|
334 let ?g = "(\<lambda> i. if i = k then a i else c i)::'n \<Rightarrow> 'a::comm_ring_1^'n" |
|
335 let ?h = "(\<lambda> i. if i = k then b i else c i)::'n \<Rightarrow> 'a::comm_ring_1^'n" |
|
336 fix p assume p: "p \<in> ?pU" |
|
337 let ?Uk = "?U - {k}" |
|
338 from p have pU: "p permutes ?U" by blast |
|
339 have kU: "?U = insert k ?Uk" by blast |
|
340 {fix j assume j: "j \<in> ?Uk" |
|
341 from j have "?f j $ p j = ?g j $ p j" and "?f j $ p j= ?h j $ p j" |
|
342 by simp_all} |
|
343 then have th1: "setprod (\<lambda>i. ?f i $ p i) ?Uk = setprod (\<lambda>i. ?g i $ p i) ?Uk" |
|
344 and th2: "setprod (\<lambda>i. ?f i $ p i) ?Uk = setprod (\<lambda>i. ?h i $ p i) ?Uk" |
|
345 apply - |
|
346 apply (rule setprod_cong, simp_all)+ |
|
347 done |
|
348 have th3: "finite ?Uk" "k \<notin> ?Uk" by auto |
|
349 have "setprod (\<lambda>i. ?f i $ p i) ?U = setprod (\<lambda>i. ?f i $ p i) (insert k ?Uk)" |
|
350 unfolding kU[symmetric] .. |
|
351 also have "\<dots> = ?f k $ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk" |
|
352 apply (rule setprod_insert) |
|
353 apply simp |
|
354 by blast |
|
355 also have "\<dots> = (a k $ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk) + (b k$ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk)" by (simp add: ring_simps) |
|
356 also have "\<dots> = (a k $ p k * setprod (\<lambda>i. ?g i $ p i) ?Uk) + (b k$ p k * setprod (\<lambda>i. ?h i $ p i) ?Uk)" by (metis th1 th2) |
|
357 also have "\<dots> = setprod (\<lambda>i. ?g i $ p i) (insert k ?Uk) + setprod (\<lambda>i. ?h i $ p i) (insert k ?Uk)" |
|
358 unfolding setprod_insert[OF th3] by simp |
|
359 finally have "setprod (\<lambda>i. ?f i $ p i) ?U = setprod (\<lambda>i. ?g i $ p i) ?U + setprod (\<lambda>i. ?h i $ p i) ?U" unfolding kU[symmetric] . |
|
360 then show "of_int (sign p) * setprod (\<lambda>i. ?f i $ p i) ?U = of_int (sign p) * setprod (\<lambda>i. ?g i $ p i) ?U + of_int (sign p) * setprod (\<lambda>i. ?h i $ p i) ?U" |
|
361 by (simp add: ring_simps) |
|
362 qed |
|
363 |
|
364 lemma det_row_mul: |
|
365 fixes a b :: "'n::finite \<Rightarrow> _ ^ 'n" |
|
366 shows "det((\<chi> i. if i = k then c *s a i else b i)::'a::comm_ring_1^'n^'n) = |
|
367 c* det((\<chi> i. if i = k then a i else b i)::'a::comm_ring_1^'n^'n)" |
|
368 |
|
369 unfolding det_def Cart_lambda_beta setsum_right_distrib |
|
370 proof (rule setsum_cong2) |
|
371 let ?U = "UNIV :: 'n set" |
|
372 let ?pU = "{p. p permutes ?U}" |
|
373 let ?f = "(\<lambda>i. if i = k then c*s a i else b i)::'n \<Rightarrow> 'a::comm_ring_1^'n" |
|
374 let ?g = "(\<lambda> i. if i = k then a i else b i)::'n \<Rightarrow> 'a::comm_ring_1^'n" |
|
375 fix p assume p: "p \<in> ?pU" |
|
376 let ?Uk = "?U - {k}" |
|
377 from p have pU: "p permutes ?U" by blast |
|
378 have kU: "?U = insert k ?Uk" by blast |
|
379 {fix j assume j: "j \<in> ?Uk" |
|
380 from j have "?f j $ p j = ?g j $ p j" by simp} |
|
381 then have th1: "setprod (\<lambda>i. ?f i $ p i) ?Uk = setprod (\<lambda>i. ?g i $ p i) ?Uk" |
|
382 apply - |
|
383 apply (rule setprod_cong, simp_all) |
|
384 done |
|
385 have th3: "finite ?Uk" "k \<notin> ?Uk" by auto |
|
386 have "setprod (\<lambda>i. ?f i $ p i) ?U = setprod (\<lambda>i. ?f i $ p i) (insert k ?Uk)" |
|
387 unfolding kU[symmetric] .. |
|
388 also have "\<dots> = ?f k $ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk" |
|
389 apply (rule setprod_insert) |
|
390 apply simp |
|
391 by blast |
|
392 also have "\<dots> = (c*s a k) $ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk" by (simp add: ring_simps) |
|
393 also have "\<dots> = c* (a k $ p k * setprod (\<lambda>i. ?g i $ p i) ?Uk)" |
|
394 unfolding th1 by (simp add: mult_ac) |
|
395 also have "\<dots> = c* (setprod (\<lambda>i. ?g i $ p i) (insert k ?Uk))" |
|
396 unfolding setprod_insert[OF th3] by simp |
|
397 finally have "setprod (\<lambda>i. ?f i $ p i) ?U = c* (setprod (\<lambda>i. ?g i $ p i) ?U)" unfolding kU[symmetric] . |
|
398 then show "of_int (sign p) * setprod (\<lambda>i. ?f i $ p i) ?U = c * (of_int (sign p) * setprod (\<lambda>i. ?g i $ p i) ?U)" |
|
399 by (simp add: ring_simps) |
|
400 qed |
|
401 |
|
402 lemma det_row_0: |
|
403 fixes b :: "'n::finite \<Rightarrow> _ ^ 'n" |
|
404 shows "det((\<chi> i. if i = k then 0 else b i)::'a::comm_ring_1^'n^'n) = 0" |
|
405 using det_row_mul[of k 0 "\<lambda>i. 1" b] |
|
406 apply (simp) |
|
407 unfolding vector_smult_lzero . |
|
408 |
|
409 lemma det_row_operation: |
|
410 fixes A :: "'a::ordered_idom^'n^'n::finite" |
|
411 assumes ij: "i \<noteq> j" |
|
412 shows "det (\<chi> k. if k = i then row i A + c *s row j A else row k A) = det A" |
|
413 proof- |
|
414 let ?Z = "(\<chi> k. if k = i then row j A else row k A) :: 'a ^'n^'n" |
|
415 have th: "row i ?Z = row j ?Z" by (vector row_def) |
|
416 have th2: "((\<chi> k. if k = i then row i A else row k A) :: 'a^'n^'n) = A" |
|
417 by (vector row_def) |
|
418 show ?thesis |
|
419 unfolding det_row_add [of i] det_row_mul[of i] det_identical_rows[OF ij th] th2 |
|
420 by simp |
|
421 qed |
|
422 |
|
423 lemma det_row_span: |
|
424 fixes A :: "'a:: ordered_idom^'n^'n::finite" |
|
425 assumes x: "x \<in> span {row j A |j. j \<noteq> i}" |
|
426 shows "det (\<chi> k. if k = i then row i A + x else row k A) = det A" |
|
427 proof- |
|
428 let ?U = "UNIV :: 'n set" |
|
429 let ?S = "{row j A |j. j \<noteq> i}" |
|
430 let ?d = "\<lambda>x. det (\<chi> k. if k = i then x else row k A)" |
|
431 let ?P = "\<lambda>x. ?d (row i A + x) = det A" |
|
432 {fix k |
|
433 |
|
434 have "(if k = i then row i A + 0 else row k A) = row k A" by simp} |
|
435 then have P0: "?P 0" |
|
436 apply - |
|
437 apply (rule cong[of det, OF refl]) |
|
438 by (vector row_def) |
|
439 moreover |
|
440 {fix c z y assume zS: "z \<in> ?S" and Py: "?P y" |
|
441 from zS obtain j where j: "z = row j A" "i \<noteq> j" by blast |
|
442 let ?w = "row i A + y" |
|
443 have th0: "row i A + (c*s z + y) = ?w + c*s z" by vector |
|
444 have thz: "?d z = 0" |
|
445 apply (rule det_identical_rows[OF j(2)]) |
|
446 using j by (vector row_def) |
|
447 have "?d (row i A + (c*s z + y)) = ?d (?w + c*s z)" unfolding th0 .. |
|
448 then have "?P (c*s z + y)" unfolding thz Py det_row_mul[of i] det_row_add[of i] |
|
449 by simp } |
|
450 |
|
451 ultimately show ?thesis |
|
452 apply - |
|
453 apply (rule span_induct_alt[of ?P ?S, OF P0]) |
|
454 apply blast |
|
455 apply (rule x) |
|
456 done |
|
457 qed |
|
458 |
|
459 (* ------------------------------------------------------------------------- *) |
|
460 (* May as well do this, though it's a bit unsatisfactory since it ignores *) |
|
461 (* exact duplicates by considering the rows/columns as a set. *) |
|
462 (* ------------------------------------------------------------------------- *) |
|
463 |
|
464 lemma det_dependent_rows: |
|
465 fixes A:: "'a::ordered_idom^'n^'n::finite" |
|
466 assumes d: "dependent (rows A)" |
|
467 shows "det A = 0" |
|
468 proof- |
|
469 let ?U = "UNIV :: 'n set" |
|
470 from d obtain i where i: "row i A \<in> span (rows A - {row i A})" |
|
471 unfolding dependent_def rows_def by blast |
|
472 {fix j k assume jk: "j \<noteq> k" |
|
473 and c: "row j A = row k A" |
|
474 from det_identical_rows[OF jk c] have ?thesis .} |
|
475 moreover |
|
476 {assume H: "\<And> i j. i \<noteq> j \<Longrightarrow> row i A \<noteq> row j A" |
|
477 have th0: "- row i A \<in> span {row j A|j. j \<noteq> i}" |
|
478 apply (rule span_neg) |
|
479 apply (rule set_rev_mp) |
|
480 apply (rule i) |
|
481 apply (rule span_mono) |
|
482 using H i by (auto simp add: rows_def) |
|
483 from det_row_span[OF th0] |
|
484 have "det A = det (\<chi> k. if k = i then 0 *s 1 else row k A)" |
|
485 unfolding right_minus vector_smult_lzero .. |
|
486 with det_row_mul[of i "0::'a" "\<lambda>i. 1"] |
|
487 have "det A = 0" by simp} |
|
488 ultimately show ?thesis by blast |
|
489 qed |
|
490 |
|
491 lemma det_dependent_columns: assumes d: "dependent(columns (A::'a::ordered_idom^'n^'n::finite))" shows "det A = 0" |
|
492 by (metis d det_dependent_rows rows_transp det_transp) |
|
493 |
|
494 (* ------------------------------------------------------------------------- *) |
|
495 (* Multilinearity and the multiplication formula. *) |
|
496 (* ------------------------------------------------------------------------- *) |
|
497 |
|
498 lemma Cart_lambda_cong: "(\<And>x. f x = g x) \<Longrightarrow> (Cart_lambda f::'a^'n) = (Cart_lambda g :: 'a^'n)" |
|
499 apply (rule iffD1[OF Cart_lambda_unique]) by vector |
|
500 |
|
501 lemma det_linear_row_setsum: |
|
502 assumes fS: "finite S" |
|
503 shows "det ((\<chi> i. if i = k then setsum (a i) S else c i)::'a::comm_ring_1^'n^'n::finite) = setsum (\<lambda>j. det ((\<chi> i. if i = k then a i j else c i)::'a^'n^'n)) S" |
|
504 proof(induct rule: finite_induct[OF fS]) |
|
505 case 1 thus ?case apply simp unfolding setsum_empty det_row_0[of k] .. |
|
506 next |
|
507 case (2 x F) |
|
508 then show ?case by (simp add: det_row_add cong del: if_weak_cong) |
|
509 qed |
|
510 |
|
511 lemma finite_bounded_functions: |
|
512 assumes fS: "finite S" |
|
513 shows "finite {f. (\<forall>i \<in> {1.. (k::nat)}. f i \<in> S) \<and> (\<forall>i. i \<notin> {1 .. k} \<longrightarrow> f i = i)}" |
|
514 proof(induct k) |
|
515 case 0 |
|
516 have th: "{f. \<forall>i. f i = i} = {id}" by (auto intro: ext) |
|
517 show ?case by (auto simp add: th) |
|
518 next |
|
519 case (Suc k) |
|
520 let ?f = "\<lambda>(y::nat,g) i. if i = Suc k then y else g i" |
|
521 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)})" |
|
522 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)}" |
|
523 apply (auto simp add: image_iff) |
|
524 apply (rule_tac x="x (Suc k)" in bexI) |
|
525 apply (rule_tac x = "\<lambda>i. if i = Suc k then i else x i" in exI) |
|
526 apply (auto intro: ext) |
|
527 done |
|
528 with finite_imageI[OF finite_cartesian_product[OF fS Suc.hyps(1)], of ?f] |
|
529 show ?case by metis |
|
530 qed |
|
531 |
|
532 |
|
533 lemma eq_id_iff[simp]: "(\<forall>x. f x = x) = (f = id)" by (auto intro: ext) |
|
534 |
|
535 lemma det_linear_rows_setsum_lemma: |
|
536 assumes fS: "finite S" and fT: "finite T" |
|
537 shows "det((\<chi> i. if i \<in> T then setsum (a i) S else c i):: 'a::comm_ring_1^'n^'n::finite) = |
|
538 setsum (\<lambda>f. det((\<chi> i. if i \<in> T then a i (f i) else c i)::'a^'n^'n)) |
|
539 {f. (\<forall>i \<in> T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = i)}" |
|
540 using fT |
|
541 proof(induct T arbitrary: a c set: finite) |
|
542 case empty |
|
543 have th0: "\<And>x y. (\<chi> i. if i \<in> {} then x i else y i) = (\<chi> i. y i)" by vector |
|
544 from "empty.prems" show ?case unfolding th0 by simp |
|
545 next |
|
546 case (insert z T a c) |
|
547 let ?F = "\<lambda>T. {f. (\<forall>i \<in> T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = i)}" |
|
548 let ?h = "\<lambda>(y,g) i. if i = z then y else g i" |
|
549 let ?k = "\<lambda>h. (h(z),(\<lambda>i. if i = z then i else h i))" |
|
550 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)" |
|
551 let ?c = "\<lambda>i. if i = z then a i j else c i" |
|
552 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)" by simp |
|
553 have thif2: "\<And>a b c d e. (if a then b else if c then d else e) = |
|
554 (if c then (if a then b else d) else (if a then b else e))" by simp |
|
555 from `z \<notin> T` have nz: "\<And>i. i \<in> T \<Longrightarrow> i = z \<longleftrightarrow> False" by auto |
|
556 have "det (\<chi> i. if i \<in> insert z T then setsum (a i) S else c i) = |
|
557 det (\<chi> i. if i = z then setsum (a i) S |
|
558 else if i \<in> T then setsum (a i) S else c i)" |
|
559 unfolding insert_iff thif .. |
|
560 also have "\<dots> = (\<Sum>j\<in>S. det (\<chi> i. if i \<in> T then setsum (a i) S |
|
561 else if i = z then a i j else c i))" |
|
562 unfolding det_linear_row_setsum[OF fS] |
|
563 apply (subst thif2) |
|
564 using nz by (simp cong del: if_weak_cong cong add: if_cong) |
|
565 finally have tha: |
|
566 "det (\<chi> i. if i \<in> insert z T then setsum (a i) S else c i) = |
|
567 (\<Sum>(j, f)\<in>S \<times> ?F T. det (\<chi> i. if i \<in> T then a i (f i) |
|
568 else if i = z then a i j |
|
569 else c i))" |
|
570 unfolding insert.hyps unfolding setsum_cartesian_product by blast |
|
571 show ?case unfolding tha |
|
572 apply(rule setsum_eq_general_reverses[where h= "?h" and k= "?k"], |
|
573 blast intro: finite_cartesian_product fS finite, |
|
574 blast intro: finite_cartesian_product fS finite) |
|
575 using `z \<notin> T` |
|
576 apply (auto intro: ext) |
|
577 apply (rule cong[OF refl[of det]]) |
|
578 by vector |
|
579 qed |
|
580 |
|
581 lemma det_linear_rows_setsum: |
|
582 assumes fS: "finite (S::'n::finite set)" |
|
583 shows "det (\<chi> i. setsum (a i) S) = setsum (\<lambda>f. det (\<chi> i. a i (f i) :: 'a::comm_ring_1 ^ 'n^'n::finite)) {f. \<forall>i. f i \<in> S}" |
|
584 proof- |
|
585 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)" by vector |
|
586 |
|
587 from det_linear_rows_setsum_lemma[OF fS, of "UNIV :: 'n set" a, unfolded th0, OF finite] show ?thesis by simp |
|
588 qed |
|
589 |
|
590 lemma matrix_mul_setsum_alt: |
|
591 fixes A B :: "'a::comm_ring_1^'n^'n::finite" |
|
592 shows "A ** B = (\<chi> i. setsum (\<lambda>k. A$i$k *s B $ k) (UNIV :: 'n set))" |
|
593 by (vector matrix_matrix_mult_def setsum_component) |
|
594 |
|
595 lemma det_rows_mul: |
|
596 "det((\<chi> i. c i *s a i)::'a::comm_ring_1^'n^'n::finite) = |
|
597 setprod (\<lambda>i. c i) (UNIV:: 'n set) * det((\<chi> i. a i)::'a^'n^'n)" |
|
598 proof (simp add: det_def setsum_right_distrib cong add: setprod_cong, rule setsum_cong2) |
|
599 let ?U = "UNIV :: 'n set" |
|
600 let ?PU = "{p. p permutes ?U}" |
|
601 fix p assume pU: "p \<in> ?PU" |
|
602 let ?s = "of_int (sign p)" |
|
603 from pU have p: "p permutes ?U" by blast |
|
604 have "setprod (\<lambda>i. c i * a i $ p i) ?U = setprod c ?U * setprod (\<lambda>i. a i $ p i) ?U" |
|
605 unfolding setprod_timesf .. |
|
606 then show "?s * (\<Prod>xa\<in>?U. c xa * a xa $ p xa) = |
|
607 setprod c ?U * (?s* (\<Prod>xa\<in>?U. a xa $ p xa))" by (simp add: ring_simps) |
|
608 qed |
|
609 |
|
610 lemma det_mul: |
|
611 fixes A B :: "'a::ordered_idom^'n^'n::finite" |
|
612 shows "det (A ** B) = det A * det B" |
|
613 proof- |
|
614 let ?U = "UNIV :: 'n set" |
|
615 let ?F = "{f. (\<forall>i\<in> ?U. f i \<in> ?U) \<and> (\<forall>i. i \<notin> ?U \<longrightarrow> f i = i)}" |
|
616 let ?PU = "{p. p permutes ?U}" |
|
617 have fU: "finite ?U" by simp |
|
618 have fF: "finite ?F" by (rule finite) |
|
619 {fix p assume p: "p permutes ?U" |
|
620 |
|
621 have "p \<in> ?F" unfolding mem_Collect_eq permutes_in_image[OF p] |
|
622 using p[unfolded permutes_def] by simp} |
|
623 then have PUF: "?PU \<subseteq> ?F" by blast |
|
624 {fix f assume fPU: "f \<in> ?F - ?PU" |
|
625 have fUU: "f ` ?U \<subseteq> ?U" using fPU by auto |
|
626 from fPU have f: "\<forall>i \<in> ?U. f i \<in> ?U" |
|
627 "\<forall>i. i \<notin> ?U \<longrightarrow> f i = i" "\<not>(\<forall>y. \<exists>!x. f x = y)" unfolding permutes_def |
|
628 by auto |
|
629 |
|
630 let ?A = "(\<chi> i. A$i$f i *s B$f i) :: 'a^'n^'n" |
|
631 let ?B = "(\<chi> i. B$f i) :: 'a^'n^'n" |
|
632 {assume fni: "\<not> inj_on f ?U" |
|
633 then obtain i j where ij: "f i = f j" "i \<noteq> j" |
|
634 unfolding inj_on_def by blast |
|
635 from ij |
|
636 have rth: "row i ?B = row j ?B" by (vector row_def) |
|
637 from det_identical_rows[OF ij(2) rth] |
|
638 have "det (\<chi> i. A$i$f i *s B$f i) = 0" |
|
639 unfolding det_rows_mul by simp} |
|
640 moreover |
|
641 {assume fi: "inj_on f ?U" |
|
642 from f fi have fith: "\<And>i j. f i = f j \<Longrightarrow> i = j" |
|
643 unfolding inj_on_def by metis |
|
644 note fs = fi[unfolded surjective_iff_injective_gen[OF fU fU refl fUU, symmetric]] |
|
645 |
|
646 {fix y |
|
647 from fs f have "\<exists>x. f x = y" by blast |
|
648 then obtain x where x: "f x = y" by blast |
|
649 {fix z assume z: "f z = y" from fith x z have "z = x" by metis} |
|
650 with x have "\<exists>!x. f x = y" by blast} |
|
651 with f(3) have "det (\<chi> i. A$i$f i *s B$f i) = 0" by blast} |
|
652 ultimately have "det (\<chi> i. A$i$f i *s B$f i) = 0" by blast} |
|
653 hence zth: "\<forall> f\<in> ?F - ?PU. det (\<chi> i. A$i$f i *s B$f i) = 0" by simp |
|
654 {fix p assume pU: "p \<in> ?PU" |
|
655 from pU have p: "p permutes ?U" by blast |
|
656 let ?s = "\<lambda>p. of_int (sign p)" |
|
657 let ?f = "\<lambda>q. ?s p * (\<Prod>i\<in> ?U. A $ i $ p i) * |
|
658 (?s q * (\<Prod>i\<in> ?U. B $ i $ q i))" |
|
659 have "(setsum (\<lambda>q. ?s q * |
|
660 (\<Prod>i\<in> ?U. (\<chi> i. A $ i $ p i *s B $ p i :: 'a^'n^'n) $ i $ q i)) ?PU) = |
|
661 (setsum (\<lambda>q. ?s p * (\<Prod>i\<in> ?U. A $ i $ p i) * |
|
662 (?s q * (\<Prod>i\<in> ?U. B $ i $ q i))) ?PU)" |
|
663 unfolding sum_permutations_compose_right[OF permutes_inv[OF p], of ?f] |
|
664 proof(rule setsum_cong2) |
|
665 fix q assume qU: "q \<in> ?PU" |
|
666 hence q: "q permutes ?U" by blast |
|
667 from p q have pp: "permutation p" and pq: "permutation q" |
|
668 unfolding permutation_permutes by auto |
|
669 have th00: "of_int (sign p) * of_int (sign p) = (1::'a)" |
|
670 "\<And>a. of_int (sign p) * (of_int (sign p) * a) = a" |
|
671 unfolding mult_assoc[symmetric] unfolding of_int_mult[symmetric] |
|
672 by (simp_all add: sign_idempotent) |
|
673 have ths: "?s q = ?s p * ?s (q o inv p)" |
|
674 using pp pq permutation_inverse[OF pp] sign_inverse[OF pp] |
|
675 by (simp add: th00 mult_ac sign_idempotent sign_compose) |
|
676 have th001: "setprod (\<lambda>i. B$i$ q (inv p i)) ?U = setprod ((\<lambda>i. B$i$ q (inv p i)) o p) ?U" |
|
677 by (rule setprod_permute[OF p]) |
|
678 have thp: "setprod (\<lambda>i. (\<chi> i. A$i$p i *s B$p i :: 'a^'n^'n) $i $ q i) ?U = setprod (\<lambda>i. A$i$p i) ?U * setprod (\<lambda>i. B$i$ q (inv p i)) ?U" |
|
679 unfolding th001 setprod_timesf[symmetric] o_def permutes_inverses[OF p] |
|
680 apply (rule setprod_cong[OF refl]) |
|
681 using permutes_in_image[OF q] by vector |
|
682 show "?s q * setprod (\<lambda>i. (((\<chi> i. A$i$p i *s B$p i) :: 'a^'n^'n)$i$q i)) ?U = ?s p * (setprod (\<lambda>i. A$i$p i) ?U) * (?s (q o inv p) * setprod (\<lambda>i. B$i$(q o inv p) i) ?U)" |
|
683 using ths thp pp pq permutation_inverse[OF pp] sign_inverse[OF pp] |
|
684 by (simp add: sign_nz th00 ring_simps sign_idempotent sign_compose) |
|
685 qed |
|
686 } |
|
687 then have th2: "setsum (\<lambda>f. det (\<chi> i. A$i$f i *s B$f i)) ?PU = det A * det B" |
|
688 unfolding det_def setsum_product |
|
689 by (rule setsum_cong2) |
|
690 have "det (A**B) = setsum (\<lambda>f. det (\<chi> i. A $ i $ f i *s B $ f i)) ?F" |
|
691 unfolding matrix_mul_setsum_alt det_linear_rows_setsum[OF fU] by simp |
|
692 also have "\<dots> = setsum (\<lambda>f. det (\<chi> i. A$i$f i *s B$f i)) ?PU" |
|
693 using setsum_mono_zero_cong_left[OF fF PUF zth, symmetric] |
|
694 unfolding det_rows_mul by auto |
|
695 finally show ?thesis unfolding th2 . |
|
696 qed |
|
697 |
|
698 (* ------------------------------------------------------------------------- *) |
|
699 (* Relation to invertibility. *) |
|
700 (* ------------------------------------------------------------------------- *) |
|
701 |
|
702 lemma invertible_left_inverse: |
|
703 fixes A :: "real^'n^'n::finite" |
|
704 shows "invertible A \<longleftrightarrow> (\<exists>(B::real^'n^'n). B** A = mat 1)" |
|
705 by (metis invertible_def matrix_left_right_inverse) |
|
706 |
|
707 lemma invertible_righ_inverse: |
|
708 fixes A :: "real^'n^'n::finite" |
|
709 shows "invertible A \<longleftrightarrow> (\<exists>(B::real^'n^'n). A** B = mat 1)" |
|
710 by (metis invertible_def matrix_left_right_inverse) |
|
711 |
|
712 lemma invertible_det_nz: |
|
713 fixes A::"real ^'n^'n::finite" |
|
714 shows "invertible A \<longleftrightarrow> det A \<noteq> 0" |
|
715 proof- |
|
716 {assume "invertible A" |
|
717 then obtain B :: "real ^'n^'n" where B: "A ** B = mat 1" |
|
718 unfolding invertible_righ_inverse by blast |
|
719 hence "det (A ** B) = det (mat 1 :: real ^'n^'n)" by simp |
|
720 hence "det A \<noteq> 0" |
|
721 apply (simp add: det_mul det_I) by algebra } |
|
722 moreover |
|
723 {assume H: "\<not> invertible A" |
|
724 let ?U = "UNIV :: 'n set" |
|
725 have fU: "finite ?U" by simp |
|
726 from H obtain c i where c: "setsum (\<lambda>i. c i *s row i A) ?U = 0" |
|
727 and iU: "i \<in> ?U" and ci: "c i \<noteq> 0" |
|
728 unfolding invertible_righ_inverse |
|
729 unfolding matrix_right_invertible_independent_rows by blast |
|
730 have stupid: "\<And>(a::real^'n) b. a + b = 0 \<Longrightarrow> -a = b" |
|
731 apply (drule_tac f="op + (- a)" in cong[OF refl]) |
|
732 apply (simp only: ab_left_minus add_assoc[symmetric]) |
|
733 apply simp |
|
734 done |
|
735 from c ci |
|
736 have thr0: "- row i A = setsum (\<lambda>j. (1/ c i) *s (c j *s row j A)) (?U - {i})" |
|
737 unfolding setsum_diff1'[OF fU iU] setsum_cmul |
|
738 apply - |
|
739 apply (rule vector_mul_lcancel_imp[OF ci]) |
|
740 apply (auto simp add: vector_smult_assoc vector_smult_rneg field_simps) |
|
741 unfolding stupid .. |
|
742 have thr: "- row i A \<in> span {row j A| j. j \<noteq> i}" |
|
743 unfolding thr0 |
|
744 apply (rule span_setsum) |
|
745 apply simp |
|
746 apply (rule ballI) |
|
747 apply (rule span_mul)+ |
|
748 apply (rule span_superset) |
|
749 apply auto |
|
750 done |
|
751 let ?B = "(\<chi> k. if k = i then 0 else row k A) :: real ^'n^'n" |
|
752 have thrb: "row i ?B = 0" using iU by (vector row_def) |
|
753 have "det A = 0" |
|
754 unfolding det_row_span[OF thr, symmetric] right_minus |
|
755 unfolding det_zero_row[OF thrb] ..} |
|
756 ultimately show ?thesis by blast |
|
757 qed |
|
758 |
|
759 (* ------------------------------------------------------------------------- *) |
|
760 (* Cramer's rule. *) |
|
761 (* ------------------------------------------------------------------------- *) |
|
762 |
|
763 lemma cramer_lemma_transp: |
|
764 fixes A:: "'a::ordered_idom^'n^'n::finite" and x :: "'a ^'n::finite" |
|
765 shows "det ((\<chi> i. if i = k then setsum (\<lambda>i. x$i *s row i A) (UNIV::'n set) |
|
766 else row i A)::'a^'n^'n) = x$k * det A" |
|
767 (is "?lhs = ?rhs") |
|
768 proof- |
|
769 let ?U = "UNIV :: 'n set" |
|
770 let ?Uk = "?U - {k}" |
|
771 have U: "?U = insert k ?Uk" by blast |
|
772 have fUk: "finite ?Uk" by simp |
|
773 have kUk: "k \<notin> ?Uk" by simp |
|
774 have th00: "\<And>k s. x$k *s row k A + s = (x$k - 1) *s row k A + row k A + s" |
|
775 by (vector ring_simps) |
|
776 have th001: "\<And>f k . (\<lambda>x. if x = k then f k else f x) = f" by (auto intro: ext) |
|
777 have "(\<chi> i. row i A) = A" by (vector row_def) |
|
778 then have thd1: "det (\<chi> i. row i A) = det A" by simp |
|
779 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" |
|
780 apply (rule det_row_span) |
|
781 apply (rule span_setsum[OF fUk]) |
|
782 apply (rule ballI) |
|
783 apply (rule span_mul) |
|
784 apply (rule span_superset) |
|
785 apply auto |
|
786 done |
|
787 show "?lhs = x$k * det A" |
|
788 apply (subst U) |
|
789 unfolding setsum_insert[OF fUk kUk] |
|
790 apply (subst th00) |
|
791 unfolding add_assoc |
|
792 apply (subst det_row_add) |
|
793 unfolding thd0 |
|
794 unfolding det_row_mul |
|
795 unfolding th001[of k "\<lambda>i. row i A"] |
|
796 unfolding thd1 by (simp add: ring_simps) |
|
797 qed |
|
798 |
|
799 lemma cramer_lemma: |
|
800 fixes A :: "'a::ordered_idom ^'n^'n::finite" |
|
801 shows "det((\<chi> i j. if j = k then (A *v x)$i else A$i$j):: 'a^'n^'n) = x$k * det A" |
|
802 proof- |
|
803 let ?U = "UNIV :: 'n set" |
|
804 have stupid: "\<And>c. setsum (\<lambda>i. c i *s row i (transp A)) ?U = setsum (\<lambda>i. c i *s column i A) ?U" |
|
805 by (auto simp add: row_transp intro: setsum_cong2) |
|
806 show ?thesis unfolding matrix_mult_vsum |
|
807 unfolding cramer_lemma_transp[of k x "transp A", unfolded det_transp, symmetric] |
|
808 unfolding stupid[of "\<lambda>i. x$i"] |
|
809 apply (subst det_transp[symmetric]) |
|
810 apply (rule cong[OF refl[of det]]) by (vector transp_def column_def row_def) |
|
811 qed |
|
812 |
|
813 lemma cramer: |
|
814 fixes A ::"real^'n^'n::finite" |
|
815 assumes d0: "det A \<noteq> 0" |
|
816 shows "A *v x = b \<longleftrightarrow> x = (\<chi> k. det(\<chi> i j. if j=k then b$i else A$i$j :: real^'n^'n) / det A)" |
|
817 proof- |
|
818 from d0 obtain B where B: "A ** B = mat 1" "B ** A = mat 1" |
|
819 unfolding invertible_det_nz[symmetric] invertible_def by blast |
|
820 have "(A ** B) *v b = b" by (simp add: B matrix_vector_mul_lid) |
|
821 hence "A *v (B *v b) = b" by (simp add: matrix_vector_mul_assoc) |
|
822 then have xe: "\<exists>x. A*v x = b" by blast |
|
823 {fix x assume x: "A *v x = b" |
|
824 have "x = (\<chi> k. det(\<chi> i j. if j=k then b$i else A$i$j :: real^'n^'n) / det A)" |
|
825 unfolding x[symmetric] |
|
826 using d0 by (simp add: Cart_eq cramer_lemma field_simps)} |
|
827 with xe show ?thesis by auto |
|
828 qed |
|
829 |
|
830 (* ------------------------------------------------------------------------- *) |
|
831 (* Orthogonality of a transformation and matrix. *) |
|
832 (* ------------------------------------------------------------------------- *) |
|
833 |
|
834 definition "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v w. f v \<bullet> f w = v \<bullet> w)" |
|
835 |
|
836 lemma orthogonal_transformation: "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>(v::real ^_). norm (f v) = norm v)" |
|
837 unfolding orthogonal_transformation_def |
|
838 apply auto |
|
839 apply (erule_tac x=v in allE)+ |
|
840 apply (simp add: real_vector_norm_def) |
|
841 by (simp add: dot_norm linear_add[symmetric]) |
|
842 |
|
843 definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow> transp Q ** Q = mat 1 \<and> Q ** transp Q = mat 1" |
|
844 |
|
845 lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n::finite) \<longleftrightarrow> transp Q ** Q = mat 1" |
|
846 by (metis matrix_left_right_inverse orthogonal_matrix_def) |
|
847 |
|
848 lemma orthogonal_matrix_id: "orthogonal_matrix (mat 1 :: _^'n^'n::finite)" |
|
849 by (simp add: orthogonal_matrix_def transp_mat matrix_mul_lid) |
|
850 |
|
851 lemma orthogonal_matrix_mul: |
|
852 fixes A :: "real ^'n^'n::finite" |
|
853 assumes oA : "orthogonal_matrix A" |
|
854 and oB: "orthogonal_matrix B" |
|
855 shows "orthogonal_matrix(A ** B)" |
|
856 using oA oB |
|
857 unfolding orthogonal_matrix matrix_transp_mul |
|
858 apply (subst matrix_mul_assoc) |
|
859 apply (subst matrix_mul_assoc[symmetric]) |
|
860 by (simp add: matrix_mul_rid) |
|
861 |
|
862 lemma orthogonal_transformation_matrix: |
|
863 fixes f:: "real^'n \<Rightarrow> real^'n::finite" |
|
864 shows "orthogonal_transformation f \<longleftrightarrow> linear f \<and> orthogonal_matrix(matrix f)" |
|
865 (is "?lhs \<longleftrightarrow> ?rhs") |
|
866 proof- |
|
867 let ?mf = "matrix f" |
|
868 let ?ot = "orthogonal_transformation f" |
|
869 let ?U = "UNIV :: 'n set" |
|
870 have fU: "finite ?U" by simp |
|
871 let ?m1 = "mat 1 :: real ^'n^'n" |
|
872 {assume ot: ?ot |
|
873 from ot have lf: "linear f" and fd: "\<forall>v w. f v \<bullet> f w = v \<bullet> w" |
|
874 unfolding orthogonal_transformation_def orthogonal_matrix by blast+ |
|
875 {fix i j |
|
876 let ?A = "transp ?mf ** ?mf" |
|
877 have th0: "\<And>b (x::'a::comm_ring_1). (if b then 1 else 0)*x = (if b then x else 0)" |
|
878 "\<And>b (x::'a::comm_ring_1). x*(if b then 1 else 0) = (if b then x else 0)" |
|
879 by simp_all |
|
880 from fd[rule_format, of "basis i" "basis j", unfolded matrix_works[OF lf, symmetric] dot_matrix_vector_mul] |
|
881 have "?A$i$j = ?m1 $ i $ j" |
|
882 by (simp add: dot_def matrix_matrix_mult_def columnvector_def rowvector_def basis_def th0 setsum_delta[OF fU] mat_def)} |
|
883 hence "orthogonal_matrix ?mf" unfolding orthogonal_matrix by vector |
|
884 with lf have ?rhs by blast} |
|
885 moreover |
|
886 {assume lf: "linear f" and om: "orthogonal_matrix ?mf" |
|
887 from lf om have ?lhs |
|
888 unfolding orthogonal_matrix_def norm_eq orthogonal_transformation |
|
889 unfolding matrix_works[OF lf, symmetric] |
|
890 apply (subst dot_matrix_vector_mul) |
|
891 by (simp add: dot_matrix_product matrix_mul_lid)} |
|
892 ultimately show ?thesis by blast |
|
893 qed |
|
894 |
|
895 lemma det_orthogonal_matrix: |
|
896 fixes Q:: "'a::ordered_idom^'n^'n::finite" |
|
897 assumes oQ: "orthogonal_matrix Q" |
|
898 shows "det Q = 1 \<or> det Q = - 1" |
|
899 proof- |
|
900 |
|
901 have th: "\<And>x::'a. x = 1 \<or> x = - 1 \<longleftrightarrow> x*x = 1" (is "\<And>x::'a. ?ths x") |
|
902 proof- |
|
903 fix x:: 'a |
|
904 have th0: "x*x - 1 = (x - 1)*(x + 1)" by (simp add: ring_simps) |
|
905 have th1: "\<And>(x::'a) y. x = - y \<longleftrightarrow> x + y = 0" |
|
906 apply (subst eq_iff_diff_eq_0) by simp |
|
907 have "x*x = 1 \<longleftrightarrow> x*x - 1 = 0" by simp |
|
908 also have "\<dots> \<longleftrightarrow> x = 1 \<or> x = - 1" unfolding th0 th1 by simp |
|
909 finally show "?ths x" .. |
|
910 qed |
|
911 from oQ have "Q ** transp Q = mat 1" by (metis orthogonal_matrix_def) |
|
912 hence "det (Q ** transp Q) = det (mat 1:: 'a^'n^'n)" by simp |
|
913 hence "det Q * det Q = 1" by (simp add: det_mul det_I det_transp) |
|
914 then show ?thesis unfolding th . |
|
915 qed |
|
916 |
|
917 (* ------------------------------------------------------------------------- *) |
|
918 (* Linearity of scaling, and hence isometry, that preserves origin. *) |
|
919 (* ------------------------------------------------------------------------- *) |
|
920 lemma scaling_linear: |
|
921 fixes f :: "real ^'n \<Rightarrow> real ^'n::finite" |
|
922 assumes f0: "f 0 = 0" and fd: "\<forall>x y. dist (f x) (f y) = c * dist x y" |
|
923 shows "linear f" |
|
924 proof- |
|
925 {fix v w |
|
926 {fix x note fd[rule_format, of x 0, unfolded dist_norm f0 diff_0_right] } |
|
927 note th0 = this |
|
928 have "f v \<bullet> f w = c^2 * (v \<bullet> w)" |
|
929 unfolding dot_norm_neg dist_norm[symmetric] |
|
930 unfolding th0 fd[rule_format] by (simp add: power2_eq_square field_simps)} |
|
931 note fc = this |
|
932 show ?thesis unfolding linear_def vector_eq |
|
933 by (simp add: dot_lmult dot_ladd dot_rmult dot_radd fc ring_simps) |
|
934 qed |
|
935 |
|
936 lemma isometry_linear: |
|
937 "f (0:: real^'n) = (0:: real^'n::finite) \<Longrightarrow> \<forall>x y. dist(f x) (f y) = dist x y |
|
938 \<Longrightarrow> linear f" |
|
939 by (rule scaling_linear[where c=1]) simp_all |
|
940 |
|
941 (* ------------------------------------------------------------------------- *) |
|
942 (* Hence another formulation of orthogonal transformation. *) |
|
943 (* ------------------------------------------------------------------------- *) |
|
944 |
|
945 lemma orthogonal_transformation_isometry: |
|
946 "orthogonal_transformation f \<longleftrightarrow> f(0::real^'n) = (0::real^'n::finite) \<and> (\<forall>x y. dist(f x) (f y) = dist x y)" |
|
947 unfolding orthogonal_transformation |
|
948 apply (rule iffI) |
|
949 apply clarify |
|
950 apply (clarsimp simp add: linear_0 linear_sub[symmetric] dist_norm) |
|
951 apply (rule conjI) |
|
952 apply (rule isometry_linear) |
|
953 apply simp |
|
954 apply simp |
|
955 apply clarify |
|
956 apply (erule_tac x=v in allE) |
|
957 apply (erule_tac x=0 in allE) |
|
958 by (simp add: dist_norm) |
|
959 |
|
960 (* ------------------------------------------------------------------------- *) |
|
961 (* Can extend an isometry from unit sphere. *) |
|
962 (* ------------------------------------------------------------------------- *) |
|
963 |
|
964 lemma isometry_sphere_extend: |
|
965 fixes f:: "real ^'n \<Rightarrow> real ^'n::finite" |
|
966 assumes f1: "\<forall>x. norm x = 1 \<longrightarrow> norm (f x) = 1" |
|
967 and fd1: "\<forall> x y. norm x = 1 \<longrightarrow> norm y = 1 \<longrightarrow> dist (f x) (f y) = dist x y" |
|
968 shows "\<exists>g. orthogonal_transformation g \<and> (\<forall>x. norm x = 1 \<longrightarrow> g x = f x)" |
|
969 proof- |
|
970 {fix x y x' y' x0 y0 x0' y0' :: "real ^'n" |
|
971 assume H: "x = norm x *s x0" "y = norm y *s y0" |
|
972 "x' = norm x *s x0'" "y' = norm y *s y0'" |
|
973 "norm x0 = 1" "norm x0' = 1" "norm y0 = 1" "norm y0' = 1" |
|
974 "norm(x0' - y0') = norm(x0 - y0)" |
|
975 |
|
976 have "norm(x' - y') = norm(x - y)" |
|
977 apply (subst H(1)) |
|
978 apply (subst H(2)) |
|
979 apply (subst H(3)) |
|
980 apply (subst H(4)) |
|
981 using H(5-9) |
|
982 apply (simp add: norm_eq norm_eq_1) |
|
983 apply (simp add: dot_lsub dot_rsub dot_lmult dot_rmult) |
|
984 apply (simp add: ring_simps) |
|
985 by (simp only: right_distrib[symmetric])} |
|
986 note th0 = this |
|
987 let ?g = "\<lambda>x. if x = 0 then 0 else norm x *s f (inverse (norm x) *s x)" |
|
988 {fix x:: "real ^'n" assume nx: "norm x = 1" |
|
989 have "?g x = f x" using nx by auto} |
|
990 hence thfg: "\<forall>x. norm x = 1 \<longrightarrow> ?g x = f x" by blast |
|
991 have g0: "?g 0 = 0" by simp |
|
992 {fix x y :: "real ^'n" |
|
993 {assume "x = 0" "y = 0" |
|
994 then have "dist (?g x) (?g y) = dist x y" by simp } |
|
995 moreover |
|
996 {assume "x = 0" "y \<noteq> 0" |
|
997 then have "dist (?g x) (?g y) = dist x y" |
|
998 apply (simp add: dist_norm norm_mul) |
|
999 apply (rule f1[rule_format]) |
|
1000 by(simp add: norm_mul field_simps)} |
|
1001 moreover |
|
1002 {assume "x \<noteq> 0" "y = 0" |
|
1003 then have "dist (?g x) (?g y) = dist x y" |
|
1004 apply (simp add: dist_norm norm_mul) |
|
1005 apply (rule f1[rule_format]) |
|
1006 by(simp add: norm_mul field_simps)} |
|
1007 moreover |
|
1008 {assume z: "x \<noteq> 0" "y \<noteq> 0" |
|
1009 have th00: "x = norm x *s (inverse (norm x) *s x)" "y = norm y *s (inverse (norm y) *s y)" "norm x *s f ((inverse (norm x) *s x)) = norm x *s f (inverse (norm x) *s x)" |
|
1010 "norm y *s f (inverse (norm y) *s y) = norm y *s f (inverse (norm y) *s y)" |
|
1011 "norm (inverse (norm x) *s x) = 1" |
|
1012 "norm (f (inverse (norm x) *s x)) = 1" |
|
1013 "norm (inverse (norm y) *s y) = 1" |
|
1014 "norm (f (inverse (norm y) *s y)) = 1" |
|
1015 "norm (f (inverse (norm x) *s x) - f (inverse (norm y) *s y)) = |
|
1016 norm (inverse (norm x) *s x - inverse (norm y) *s y)" |
|
1017 using z |
|
1018 by (auto simp add: vector_smult_assoc field_simps norm_mul intro: f1[rule_format] fd1[rule_format, unfolded dist_norm]) |
|
1019 from z th0[OF th00] have "dist (?g x) (?g y) = dist x y" |
|
1020 by (simp add: dist_norm)} |
|
1021 ultimately have "dist (?g x) (?g y) = dist x y" by blast} |
|
1022 note thd = this |
|
1023 show ?thesis |
|
1024 apply (rule exI[where x= ?g]) |
|
1025 unfolding orthogonal_transformation_isometry |
|
1026 using g0 thfg thd by metis |
|
1027 qed |
|
1028 |
|
1029 (* ------------------------------------------------------------------------- *) |
|
1030 (* Rotation, reflection, rotoinversion. *) |
|
1031 (* ------------------------------------------------------------------------- *) |
|
1032 |
|
1033 definition "rotation_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = 1" |
|
1034 definition "rotoinversion_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = - 1" |
|
1035 |
|
1036 lemma orthogonal_rotation_or_rotoinversion: |
|
1037 fixes Q :: "'a::ordered_idom^'n^'n::finite" |
|
1038 shows " orthogonal_matrix Q \<longleftrightarrow> rotation_matrix Q \<or> rotoinversion_matrix Q" |
|
1039 by (metis rotoinversion_matrix_def rotation_matrix_def det_orthogonal_matrix) |
|
1040 (* ------------------------------------------------------------------------- *) |
|
1041 (* Explicit formulas for low dimensions. *) |
|
1042 (* ------------------------------------------------------------------------- *) |
|
1043 |
|
1044 lemma setprod_1: "setprod f {(1::nat)..1} = f 1" by simp |
|
1045 |
|
1046 lemma setprod_2: "setprod f {(1::nat)..2} = f 1 * f 2" |
|
1047 by (simp add: nat_number setprod_numseg mult_commute) |
|
1048 lemma setprod_3: "setprod f {(1::nat)..3} = f 1 * f 2 * f 3" |
|
1049 by (simp add: nat_number setprod_numseg mult_commute) |
|
1050 |
|
1051 lemma det_1: "det (A::'a::comm_ring_1^1^1) = A$1$1" |
|
1052 by (simp add: det_def permutes_sing sign_id UNIV_1) |
|
1053 |
|
1054 lemma det_2: "det (A::'a::comm_ring_1^2^2) = A$1$1 * A$2$2 - A$1$2 * A$2$1" |
|
1055 proof- |
|
1056 have f12: "finite {2::2}" "1 \<notin> {2::2}" by auto |
|
1057 show ?thesis |
|
1058 unfolding det_def UNIV_2 |
|
1059 unfolding setsum_over_permutations_insert[OF f12] |
|
1060 unfolding permutes_sing |
|
1061 apply (simp add: sign_swap_id sign_id swap_id_eq) |
|
1062 by (simp add: arith_simps(31)[symmetric] of_int_minus of_int_1 del: arith_simps(31)) |
|
1063 qed |
|
1064 |
|
1065 lemma det_3: "det (A::'a::comm_ring_1^3^3) = |
|
1066 A$1$1 * A$2$2 * A$3$3 + |
|
1067 A$1$2 * A$2$3 * A$3$1 + |
|
1068 A$1$3 * A$2$1 * A$3$2 - |
|
1069 A$1$1 * A$2$3 * A$3$2 - |
|
1070 A$1$2 * A$2$1 * A$3$3 - |
|
1071 A$1$3 * A$2$2 * A$3$1" |
|
1072 proof- |
|
1073 have f123: "finite {2::3, 3}" "1 \<notin> {2::3, 3}" by auto |
|
1074 have f23: "finite {3::3}" "2 \<notin> {3::3}" by auto |
|
1075 |
|
1076 show ?thesis |
|
1077 unfolding det_def UNIV_3 |
|
1078 unfolding setsum_over_permutations_insert[OF f123] |
|
1079 unfolding setsum_over_permutations_insert[OF f23] |
|
1080 |
|
1081 unfolding permutes_sing |
|
1082 apply (simp add: sign_swap_id permutation_swap_id sign_compose sign_id swap_id_eq) |
|
1083 apply (simp add: arith_simps(31)[symmetric] of_int_minus of_int_1 del: arith_simps(31)) |
|
1084 by (simp add: ring_simps) |
|
1085 qed |
|
1086 |
|
1087 end |
|