subsubsection\<^marker>\<open>tag important\<close> \<open>Definition of determinant\<close>
definition\<^marker>\<open>tag important\<close> det:: "'a::comm_ring_1^'n^'n \<Rightarrow> 'a" where "det A =
sum (\<lambda>p. of_int (sign p) * prod (\<lambda>i. A$i$p i) (UNIV :: 'n set))
{p. p permutes (UNIV :: 'n set)}"
text\<open>Basic determinant properties\<close>
lemma det_transpose [simp]: "det (transpose A) = det (A::'a::comm_ring_1 ^'n^'n)" proof - let ?di = "\A i j. A$i$j" let ?U = "(UNIV :: 'n set)" have fU: "finite ?U"by simp
{ fix p assume p: "p \ {p. p permutes ?U}" from p have pU: "p permutes ?U" by blast have sth: "sign (inv p) = sign p" by (metis sign_inverse fU p mem_Collect_eq permutation_permutes) from permutes_inj[OF pU] have pi: "inj_on p ?U" by (blast intro: inj_on_subset) from permutes_image[OF pU] have"prod (\i. ?di (transpose A) i (inv p i)) ?U =
prod (\<lambda>i. ?di (transpose A) i (inv p i)) (p ` ?U)" by simp alsohave"\ = prod ((\i. ?di (transpose A) i (inv p i)) \ p) ?U" unfolding prod.reindex[OF pi] .. alsohave"\ = prod (\i. ?di A i (p i)) ?U" proof - have"((\i. ?di (transpose A) i (inv p i)) \ p) i = ?di A i (p i)" if "i \ ?U" for i using that permutes_inv_o[OF pU] permutes_in_image[OF pU] unfolding transpose_def by (simp add: fun_eq_iff) thenshow"prod ((\i. ?di (transpose A) i (inv p i)) \ p) ?U = prod (\i. ?di A i (p i)) ?U" by (auto intro: prod.cong) qed finallyhave"of_int (sign (inv p)) * (prod (\i. ?di (transpose A) i (inv p i)) ?U) =
of_int (sign p) * (prod (\<lambda>i. ?di A i (p i)) ?U)" using sth by simp
} thenshow ?thesis unfolding det_def by (subst sum_permutations_inverse) (blast intro: sum.cong) qed
lemma det_lowerdiagonal: fixes A :: "'a::comm_ring_1^('n::{finite,wellorder})^('n::{finite,wellorder})" assumes ld: "\i j. i < j \ A$i$j = 0" shows"det A = prod (\i. A$i$i) (UNIV:: 'n set)" proof - let ?U = "UNIV:: 'n set" let ?PU = "{p. p permutes ?U}" let ?pp = "\p. of_int (sign p) * prod (\i. A$i$p i) (UNIV :: 'n set)" have fU: "finite ?U" by simp have id0: "{id} \ ?PU" by (auto simp: permutes_id) have p0: "\p \ ?PU - {id}. ?pp p = 0" proof fix p assume"p \ ?PU - {id}" thenobtain i where i: "p i > i" by clarify (meson leI permutes_natset_le) from ld[OF i] have"\i \ ?U. A$i$p i = 0" by blast with prod_zero[OF fU] show"?pp p = 0" by force qed from sum.mono_neutral_cong_left[OF finite_permutations[OF fU] id0 p0] show ?thesis unfolding det_def by (simp add: sign_id) qed
lemma det_upperdiagonal: fixes A :: "'a::comm_ring_1^'n::{finite,wellorder}^'n::{finite,wellorder}" assumes ld: "\i j. i > j \ A$i$j = 0" shows"det A = prod (\i. A$i$i) (UNIV:: 'n set)" proof - let ?U = "UNIV:: 'n set" let ?PU = "{p. p permutes ?U}" let ?pp = "(\p. of_int (sign p) * prod (\i. A$i$p i) (UNIV :: 'n set))" have fU: "finite ?U" by simp have id0: "{id} \ ?PU" by (auto simp: permutes_id) have p0: "\p \ ?PU -{id}. ?pp p = 0" proof fix p assume p: "p \ ?PU - {id}" thenobtain i where i: "p i < i" by clarify (meson leI permutes_natset_ge) from ld[OF i] have"\i \ ?U. A$i$p i = 0" by blast with prod_zero[OF fU] show"?pp p = 0" by force qed from sum.mono_neutral_cong_left[OF finite_permutations[OF fU] id0 p0] show ?thesis unfolding det_def by (simp add: sign_id) qed
proposition det_diagonal: fixes A :: "'a::comm_ring_1^'n^'n" assumes ld: "\i j. i \ j \ A$i$j = 0" shows"det A = prod (\i. A$i$i) (UNIV::'n set)" proof - let ?U = "UNIV:: 'n set" let ?PU = "{p. p permutes ?U}" let ?pp = "\p. of_int (sign p) * prod (\i. A$i$p i) (UNIV :: 'n set)" have fU: "finite ?U"by simp from finite_permutations[OF fU] have fPU: "finite ?PU" . have id0: "{id} \ ?PU" by (auto simp: permutes_id) have p0: "\p \ ?PU - {id}. ?pp p = 0" proof fix p assume p: "p \ ?PU - {id}" thenobtain i where i: "p i \ i" by fastforce with ld have"\i \ ?U. A$i$p i = 0" by (metis UNIV_I) with prod_zero [OF fU] show"?pp p = 0" by force qed from sum.mono_neutral_cong_left[OF fPU id0 p0] show ?thesis unfolding det_def by (simp add: sign_id) qed
lemma det_permute_rows: fixes A :: "'a::comm_ring_1^'n^'n" assumes p: "p permutes (UNIV :: 'n::finite set)" shows"det (\ i. A$p i :: 'a^'n^'n) = of_int (sign p) * det A" proof - let ?U = "UNIV :: 'n set" let ?PU = "{p. p permutes ?U}" have *: "(\q\?PU. of_int (sign (q \ p)) * (\i\?U. A $ p i $ (q \ p) i)) =
(\<Sum>n\<in>?PU. of_int (sign p) * of_int (sign n) * (\<Prod>i\<in>?U. A $ i $ n i))" proof (rule sum.cong) fix q assume qPU: "q \ ?PU" have fU: "finite ?U" by simp from qPU have q: "q permutes ?U" by blast have"prod (\i. A$p i$ (q \ p) i) ?U = prod ((\i. A$p i$(q \ p) i) \ inv p) ?U" by (simp only: prod.permute[OF permutes_inv[OF p], symmetric]) alsohave"\ = prod (\i. A $ (p \ inv p) i $ (q \ (p \ inv p)) i) ?U" by (simp only: o_def) alsohave"\ = prod (\i. A$i$q i) ?U" by (simp only: o_def permutes_inverses[OF p]) finallyhave thp: "prod (\i. A$p i$ (q \ p) i) ?U = prod (\i. A$i$q i) ?U" by blast from p q have pp: "permutation p"and qp: "permutation q" by (metis fU permutation_permutes)+ show"of_int (sign (q \ p)) * prod (\i. A$ p i$ (q \ p) i) ?U =
of_int (sign p) * of_int (sign q) * prod (\<lambda>i. A$i$q i) ?U" by (simp only: thp sign_compose[OF qp pp] mult.commute of_int_mult) qed auto show ?thesis apply (simp add: det_def sum_distrib_left mult.assoc[symmetric]) apply (subst sum_permutations_compose_right[OF p]) apply (rule *) done qed
lemma det_permute_columns: fixes A :: "'a::comm_ring_1^'n^'n" assumes p: "p permutes (UNIV :: 'n set)" shows"det(\ i j. A$i$ p j :: 'a^'n^'n) = of_int (sign p) * det A" proof - let ?Ap = "\ i j. A$i$ p j :: 'a^'n^'n" let ?At = "transpose A" have"of_int (sign p) * det A = det (transpose (\ i. transpose A $ p i))" unfolding det_permute_rows[OF p, of ?At] det_transpose .. moreover have"?Ap = transpose (\ i. transpose A $ p i)" by (simp add: transpose_def vec_eq_iff) ultimatelyshow ?thesis by simp qed
lemma det_identical_columns: fixes A :: "'a::comm_ring_1^'n^'n" assumes jk: "j \ k" and r: "column j A = column k A" shows"det A = 0" proof - let ?U="UNIV::'n set" let ?t_jk="Transposition.transpose j k" let ?PU="{p. p permutes ?U}" let ?S1="{p. p\?PU \ evenperm p}" let ?S2="{(?t_jk \ p) |p. p \?S1}" let ?f="\p. of_int (sign p) * (\i\UNIV. A $ i $ p i)" let ?g="\p. ?t_jk \ p" have g_S1: "?S2 = ?g` ?S1"by auto have inj_g: "inj_on ?g ?S1" proof (unfold inj_on_def, auto) fix x y assume x: "x permutes ?U"and even_x: "evenperm x" and y: "y permutes ?U"and even_y: "evenperm y"and eq: "?t_jk \ x = ?t_jk \ y" show"x = y"by (metis (opaque_lifting, no_types) comp_assoc eq id_comp swap_id_idempotent) qed have tjk_permutes: "?t_jk permutes ?U" by (auto simp add: permutes_def dest: transpose_eq_imp_eq) (meson transpose_involutory) have tjk_eq: "\i l. A $ i $ ?t_jk l = A $ i $ l" using r jk unfolding column_def vec_eq_iff by (simp add: Transposition.transpose_def) have sign_tjk: "sign ?t_jk = -1"using sign_swap_id[of j k] jk by auto
{fix x assume x: "x\ ?S1" have"sign (?t_jk \ x) = sign (?t_jk) * sign x" by (metis (lifting) finite_class.finite_UNIV mem_Collect_eq
permutation_permutes permutation_swap_id sign_compose x) alsohave"\ = - sign x" using sign_tjk by simp alsohave"\ \ sign x" unfolding sign_def by simp finallyhave"sign (?t_jk \ x) \ sign x" and "(?t_jk \ x) \ ?S2" using x by force+
} hence disjoint: "?S1 \ ?S2 = {}" by (force simp: sign_def) have PU_decomposition: "?PU = ?S1 \ ?S2" proof (auto) fix x assume x: "x permutes ?U"and"\p. p permutes ?U \ x = Transposition.transpose j k \ p \ \ evenperm p" thenobtain p where p: "p permutes UNIV"and x_eq: "x = Transposition.transpose j k \ p" and odd_p: "\ evenperm p" by (metis (mono_tags) id_o o_assoc permutes_compose swap_id_idempotent tjk_permutes) thus"evenperm x" by (meson evenperm_comp evenperm_swap finite_class.finite_UNIV
jk permutation_permutes permutation_swap_id) next fix p assume p: "p permutes ?U" show"Transposition.transpose j k \ p permutes UNIV" by (metis p permutes_compose tjk_permutes) qed have"sum ?f ?S2 = sum ((\p. of_int (sign p) * (\i\UNIV. A $ i $ p i)) \<circ> (\<circ>) (Transposition.transpose j k)) {p \<in> {p. p permutes UNIV}. evenperm p}" unfolding g_S1 by (rule sum.reindex[OF inj_g]) alsohave"\ = sum (\p. of_int (sign (?t_jk \ p)) * (\i\UNIV. A $ i $ p i)) ?S1" unfolding o_def by (rule sum.cong, auto simp: tjk_eq) alsohave"\ = sum (\p. - ?f p) ?S1" proof (rule sum.cong, auto) fix x assume x: "x permutes ?U" and even_x: "evenperm x" hence perm_x: "permutation x"and perm_tjk: "permutation ?t_jk" using permutation_permutes[of x] permutation_permutes[of ?t_jk] permutation_swap_id by (metis finite_code)+ have"(sign (?t_jk \ x)) = - (sign x)" unfolding sign_compose[OF perm_tjk perm_x] sign_tjk by auto thus"of_int (sign (?t_jk \ x)) * (\i\UNIV. A $ i $ x i)
= - (of_int (sign x) * (\<Prod>i\<in>UNIV. A $ i $ x i))" by auto qed alsohave"\= - sum ?f ?S1" unfolding sum_negf .. finallyhave *: "sum ?f ?S2 = - sum ?f ?S1" . have"det A = (\p | p permutes UNIV. of_int (sign p) * (\i\UNIV. A $ i $ p i))" unfolding det_def .. alsohave"\= sum ?f ?S1 + sum ?f ?S2" by (subst PU_decomposition, rule sum.union_disjoint[OF _ _ disjoint], auto) alsohave"\= sum ?f ?S1 - sum ?f ?S1 " unfolding * by auto alsohave"\= 0" by simp finallyshow"det A = 0"by simp qed
lemma det_identical_rows: fixes A :: "'a::comm_ring_1^'n^'n" assumes ij: "i \ j" and r: "row i A = row j A" shows"det A = 0" by (metis column_transpose det_identical_columns det_transpose ij r)
lemma det_zero_row: fixes A :: "'a::{idom, ring_char_0}^'n^'n"and F :: "'b::{field}^'m^'m" shows"row i A = 0 \ det A = 0" and "row j F = 0 \ det F = 0" by (force simp: row_def det_def vec_eq_iff sign_nz intro!: sum.neutral)+
lemma det_zero_column: fixes A :: "'a::{idom, ring_char_0}^'n^'n"and F :: "'b::{field}^'m^'m" shows"column i A = 0 \ det A = 0" and "column j F = 0 \ det F = 0" unfolding atomize_conj atomize_imp by (metis det_transpose det_zero_row row_transpose)
lemma det_row_add: fixes a b c :: "'n::finite \ _ ^ 'n" shows"det((\ i. if i = k then a i + b i else c i)::'a::comm_ring_1^'n^'n) =
det((\<chi> i. if i = k then a i else c i)::'a::comm_ring_1^'n^'n) +
det((\<chi> i. if i = k then b i else c i)::'a::comm_ring_1^'n^'n)" unfolding det_def vec_lambda_beta sum.distrib[symmetric] proof (rule sum.cong) let ?U = "UNIV :: 'n set" let ?pU = "{p. p permutes ?U}" let ?f = "(\i. if i = k then a i + b i else c i)::'n \ 'a::comm_ring_1^'n" let ?g = "(\ i. if i = k then a i else c i)::'n \ 'a::comm_ring_1^'n" let ?h = "(\ i. if i = k then b i else c i)::'n \ 'a::comm_ring_1^'n" fix p assume p: "p \ ?pU" let ?Uk = "?U - {k}" from p have pU: "p permutes ?U" by blast have kU: "?U = insert k ?Uk" by blast have eq: "prod (\i. ?f i $ p i) ?Uk = prod (\i. ?g i $ p i) ?Uk" "prod (\i. ?f i $ p i) ?Uk = prod (\i. ?h i $ p i) ?Uk" by auto have Uk: "finite ?Uk""k \ ?Uk" by auto have"prod (\i. ?f i $ p i) ?U = prod (\i. ?f i $ p i) (insert k ?Uk)" unfolding kU[symmetric] .. alsohave"\ = ?f k $ p k * prod (\i. ?f i $ p i) ?Uk" by (rule prod.insert) auto alsohave"\ = (a k $ p k * prod (\i. ?f i $ p i) ?Uk) + (b k$ p k * prod (\i. ?f i $ p i) ?Uk)" by (simp add: field_simps) alsohave"\ = (a k $ p k * prod (\i. ?g i $ p i) ?Uk) + (b k$ p k * prod (\i. ?h i $ p i) ?Uk)" by (metis eq) alsohave"\ = prod (\i. ?g i $ p i) (insert k ?Uk) + prod (\i. ?h i $ p i) (insert k ?Uk)" unfolding prod.insert[OF Uk] by simp finallyhave"prod (\i. ?f i $ p i) ?U = prod (\i. ?g i $ p i) ?U + prod (\i. ?h i $ p i) ?U" unfolding kU[symmetric] . thenshow"of_int (sign p) * prod (\i. ?f i $ p i) ?U =
of_int (sign p) * prod (\<lambda>i. ?g i $ p i) ?U + of_int (sign p) * prod (\<lambda>i. ?h i $ p i) ?U" by (simp add: field_simps) qed auto
lemma det_row_mul: fixes a b :: "'n::finite \ _ ^ 'n" shows"det((\ i. if i = k then c *s a i else b i)::'a::comm_ring_1^'n^'n) =
c * det((\<chi> i. if i = k then a i else b i)::'a::comm_ring_1^'n^'n)" unfolding det_def vec_lambda_beta sum_distrib_left proof (rule sum.cong) let ?U = "UNIV :: 'n set" let ?pU = "{p. p permutes ?U}" let ?f = "(\i. if i = k then c*s a i else b i)::'n \ 'a::comm_ring_1^'n" let ?g = "(\ i. if i = k then a i else b i)::'n \ 'a::comm_ring_1^'n" fix p assume p: "p \ ?pU" let ?Uk = "?U - {k}" from p have pU: "p permutes ?U" by blast have kU: "?U = insert k ?Uk" by blast have eq: "prod (\i. ?f i $ p i) ?Uk = prod (\i. ?g i $ p i) ?Uk" by auto have Uk: "finite ?Uk""k \ ?Uk" by auto have"prod (\i. ?f i $ p i) ?U = prod (\i. ?f i $ p i) (insert k ?Uk)" unfolding kU[symmetric] .. alsohave"\ = ?f k $ p k * prod (\i. ?f i $ p i) ?Uk" by (rule prod.insert) auto alsohave"\ = (c*s a k) $ p k * prod (\i. ?f i $ p i) ?Uk" by (simp add: field_simps) alsohave"\ = c* (a k $ p k * prod (\i. ?g i $ p i) ?Uk)" unfolding eq by (simp add: ac_simps) alsohave"\ = c* (prod (\i. ?g i $ p i) (insert k ?Uk))" unfolding prod.insert[OF Uk] by simp finallyhave"prod (\i. ?f i $ p i) ?U = c* (prod (\i. ?g i $ p i) ?U)" unfolding kU[symmetric] . thenshow"of_int (sign p) * prod (\i. ?f i $ p i) ?U = c * (of_int (sign p) * prod (\i. ?g i $ p i) ?U)" by (simp add: field_simps) qed auto
lemma det_row_0: fixes b :: "'n::finite \ _ ^ 'n" shows"det((\ i. if i = k then 0 else b i)::'a::comm_ring_1^'n^'n) = 0" using det_row_mul[of k 0 "\i. 1" b] apply simp apply (simp only: vector_smult_lzero) done
lemma det_row_operation: fixes A :: "'a::{comm_ring_1}^'n^'n" assumes ij: "i \ j" shows"det (\ k. if k = i then row i A + c *s row j A else row k A) = det A" proof - let ?Z = "(\ k. if k = i then row j A else row k A) :: 'a ^'n^'n" have th: "row i ?Z = row j ?Z"by (vector row_def) have th2: "((\ k. if k = i then row i A else row k A) :: 'a^'n^'n) = A" by (vector row_def) show ?thesis unfolding det_row_add [of i] det_row_mul[of i] det_identical_rows[OF ij th] th2 by simp qed
lemma det_row_span: fixes A :: "'a::{field}^'n^'n" assumes x: "x \ vec.span {row j A |j. j \ i}" shows"det (\ k. if k = i then row i A + x else row k A) = det A" using x proof (induction rule: vec.span_induct_alt) case base have"(if k = i then row i A + 0 else row k A) = row k A"for k by simp thenshow ?case by (simp add: row_def) next case (step c z y) thenobtain j where j: "z = row j A""i \ j" by blast let ?w = "row i A + y" have th0: "row i A + (c*s z + y) = ?w + c*s z" by vector let ?d = "\x. det (\ k. if k = i then x else row k A)" have thz: "?d z = 0" apply (rule det_identical_rows[OF j(2)]) using j apply (vector row_def) done have"?d (row i A + (c*s z + y)) = ?d (?w + c*s z)" unfolding th0 .. thenhave"?d (row i A + (c*s z + y)) = det A" unfolding thz step.IH det_row_mul[of i] det_row_add[of i] by simp thenshow ?case unfolding scalar_mult_eq_scaleR . qed
text\<open>
May as well do this, though it's a bit unsatisfactory since it ignores
exact duplicates by considering the rows/columns as a set. \<close>
lemma det_dependent_rows: fixes A:: "'a::{field}^'n^'n" assumes d: "vec.dependent (rows A)" shows"det A = 0" proof - let ?U = "UNIV :: 'n set" from d obtain i where i: "row i A \ vec.span (rows A - {row i A})" unfolding vec.dependent_def rows_def by blast show ?thesis proof (cases "\i j. i \ j \ row i A \ row j A") case True with i have"vec.span (rows A - {row i A}) \ vec.span {row j A |j. j \ i}" by (auto simp: rows_def intro!: vec.span_mono) thenhave"- row i A \ vec.span {row j A|j. j \ i}" by (meson i subsetCE vec.span_neg) from det_row_span[OF this] have"det A = det (\ k. if k = i then 0 *s 1 else row k A)" unfolding right_minus vector_smult_lzero .. with det_row_mul[of i 0 "\i. 1"] show ?thesis by simp next case False thenobtain j k where jk: "j \ k" "row j A = row k A" by auto from det_identical_rows[OF jk] show ?thesis . qed qed
lemma det_dependent_columns: assumes d: "vec.dependent (columns (A::real^'n^'n))" shows"det A = 0" by (metis d det_dependent_rows rows_transpose det_transpose)
text\<open>Multilinearity and the multiplication formula\<close>
lemma Cart_lambda_cong: "(\x. f x = g x) \ (vec_lambda f::'a^'n) = (vec_lambda g :: 'a^'n)" by auto
lemma det_linear_row_sum: assumes fS: "finite S" shows"det ((\ i. if i = k then sum (a i) S else c i)::'a::comm_ring_1^'n^'n) =
sum (\<lambda>j. det ((\<chi> i. if i = k then a i j else c i)::'a^'n^'n)) S" using fS by (induct rule: finite_induct; simp add: det_row_0 det_row_add cong: if_cong)
lemma finite_bounded_functions: assumes fS: "finite S" shows"finite {f. (\i \ {1.. (k::nat)}. f i \ S) \ (\i. i \ {1 .. k} \ f i = i)}" proof (induct k) case 0 have *: "{f. \i. f i = i} = {id}" by auto show ?case by (auto simp: *) next case (Suc k) let ?f = "\(y::nat,g) i. if i = Suc k then y else g i" let ?S = "?f ` (S \ {f. (\i\{1..k}. f i \ S) \ (\i. i \ {1..k} \ f i = i)})" have"?S = {f. (\i\{1.. Suc k}. f i \ S) \ (\i. i \ {1.. Suc k} \ f i = i)}" apply (auto simp: image_iff) apply (rename_tac f) apply (rule_tac x="f (Suc k)"in bexI) apply (rule_tac x = "\i. if i = Suc k then i else f i" in exI, auto) done with finite_imageI[OF finite_cartesian_product[OF fS Suc.hyps(1)], of ?f] show ?case by metis qed
lemma det_linear_rows_sum_lemma: assumes fS: "finite S" and fT: "finite T" shows"det ((\ i. if i \ T then sum (a i) S else c i):: 'a::comm_ring_1^'n^'n) =
sum (\<lambda>f. det((\<chi> i. if i \<in> T then a i (f i) else c i)::'a^'n^'n))
{f. (\<forall>i \<in> T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = i)}" using fT proof (induct T arbitrary: a c set: finite) case empty have th0: "\x y. (\ i. if i \ {} then x i else y i) = (\ i. y i)" by vector from empty.prems show ?case unfolding th0 by (simp add: eq_id_iff) next case (insert z T a c) let ?F = "\T. {f. (\i \ T. f i \ S) \ (\i. i \ T \ f i = i)}" let ?h = "\(y,g) i. if i = z then y else g i" let ?k = "\h. (h(z),(\i. if i = z then i else h i))" let ?s = "\ k a c f. det((\ i. if i \ T then a i (f i) else c i)::'a^'n^'n)" let ?c = "\j i. if i = z then a i j else c i" have thif: "\a b c d. (if a \ b then c else d) = (if a then c else if b then c else d)" by simp have thif2: "\a b c d e. (if a then b else if c then d else e) =
(if c then (if a then b else d) else (if a then b else e))" by simp from\<open>z \<notin> T\<close> have nz: "\<And>i. i \<in> T \<Longrightarrow> i \<noteq> z" by auto have"det (\ i. if i \ insert z T then sum (a i) S else c i) =
det (\<chi> i. if i = z then sum (a i) S else if i \<in> T then sum (a i) S else c i)" unfolding insert_iff thif .. alsohave"\ = (\j\S. det (\ i. if i \ T then sum (a i) S else if i = z then a i j else c i))" unfolding det_linear_row_sum[OF fS] by (subst thif2) (simp add: nz cong: if_cong) finallyhave tha: "det (\ i. if i \ insert z T then sum (a i) S else c i) =
(\<Sum>(j, f)\<in>S \<times> ?F T. det (\<chi> i. if i \<in> T then a i (f i)
else if i = z then a i j
else c i))" unfolding insert.hyps unfolding sum.cartesian_product by blast show ?caseunfolding tha using\<open>z \<notin> T\<close> by (intro sum.reindex_bij_witness[where i="?k"and j="?h"])
(auto intro!: cong[OF refl[of det]] simp: vec_eq_iff) qed
lemma det_linear_rows_sum: fixes S :: "'n::finite set" assumes fS: "finite S" shows"det (\ i. sum (a i) S) =
sum (\<lambda>f. det (\<chi> i. a i (f i) :: 'a::comm_ring_1 ^ 'n^'n)) {f. \<forall>i. f i \<in> S}" proof - have th0: "\x y. ((\ i. if i \ (UNIV:: 'n set) then x i else y i) :: 'a^'n^'n) = (\ i. x i)" by vector from det_linear_rows_sum_lemma[OF fS, of "UNIV :: 'n set" a, unfolded th0, OF finite] show ?thesis by simp qed
lemma matrix_mul_sum_alt: fixes A B :: "'a::comm_ring_1^'n^'n" shows"A ** B = (\ i. sum (\k. A$i$k *s B $ k) (UNIV :: 'n set))" by (vector matrix_matrix_mult_def sum_component)
lemma det_rows_mul: "det((\ i. c i *s a i)::'a::comm_ring_1^'n^'n) =
prod (\<lambda>i. c i) (UNIV:: 'n set) * det((\<chi> i. a i)::'a^'n^'n)" proof (simp add: det_def sum_distrib_left cong add: prod.cong, rule sum.cong) let ?U = "UNIV :: 'n set" let ?PU = "{p. p permutes ?U}" fix p assume pU: "p \ ?PU" let ?s = "of_int (sign p)" from pU have p: "p permutes ?U" by blast have"prod (\i. c i * a i $ p i) ?U = prod c ?U * prod (\i. a i $ p i) ?U" unfolding prod.distrib .. thenshow"?s * (\xa\?U. c xa * a xa $ p xa) =
prod c ?U * (?s* (\<Prod>xa\<in>?U. a xa $ p xa))" by (simp add: field_simps) qed rule
proposition det_mul: fixes A B :: "'a::comm_ring_1^'n^'n" shows"det (A ** B) = det A * det B" proof - let ?U = "UNIV :: 'n set" let ?F = "{f. (\i \ ?U. f i \ ?U) \ (\i. i \ ?U \ f i = i)}" let ?PU = "{p. p permutes ?U}" have"p \ ?F" if "p permutes ?U" for p by simp thenhave PUF: "?PU \ ?F" by blast
{ fix f assume fPU: "f \ ?F - ?PU" have fUU: "f ` ?U \ ?U" using fPU by auto from fPU have f: "\i \ ?U. f i \ ?U" "\i. i \ ?U \ f i = i" "\(\y. \!x. f x = y)" unfolding permutes_def by auto
let ?A = "(\ i. A$i$f i *s B$f i) :: 'a^'n^'n" let ?B = "(\ i. B$f i) :: 'a^'n^'n"
{ assume fni: "\ inj_on f ?U" thenobtain i j where ij: "f i = f j""i \ j" unfolding inj_on_def by blast thenhave"row i ?B = row j ?B" by (vector row_def) with det_identical_rows[OF ij(2)] have"det (\ i. A$i$f i *s B$f i) = 0" unfolding det_rows_mul by force
} moreover
{ assume fi: "inj_on f ?U" from f fi have fith: "\i j. f i = f j \ i = j" unfolding inj_on_def by metis note fs = fi[unfolded surjective_iff_injective_gen[OF finite finite refl fUU, symmetric]] have"\!x. f x = y" for y using fith fs by blast with f(3) have"det (\ i. A$i$f i *s B$f i) = 0" by blast
} ultimatelyhave"det (\ i. A$i$f i *s B$f i) = 0" by blast
} thenhave zth: "\ f\ ?F - ?PU. det (\ i. A$i$f i *s B$f i) = 0" by simp
{ fix p assume pU: "p \ ?PU" from pU have p: "p permutes ?U" by blast let ?s = "\p. of_int (sign p)" let ?f = "\q. ?s p * (\i\ ?U. A $ i $ p i) * (?s q * (\i\ ?U. B $ i $ q i))" have"(sum (\q. ?s q *
(\<Prod>i\<in> ?U. (\<chi> i. A $ i $ p i *s B $ p i :: 'a^'n^'n) $ i $ q i)) ?PU) =
(sum (\<lambda>q. ?s p * (\<Prod>i\<in> ?U. A $ i $ p i) * (?s q * (\<Prod>i\<in> ?U. B $ i $ q i))) ?PU)" unfolding sum_permutations_compose_right[OF permutes_inv[OF p], of ?f] proof (rule sum.cong) fix q assume qU: "q \ ?PU" thenhave q: "q permutes ?U" by blast from p q have pp: "permutation p"and pq: "permutation q" unfolding permutation_permutes by auto have th00: "of_int (sign p) * of_int (sign p) = (1::'a)" "\a. of_int (sign p) * (of_int (sign p) * a) = a" unfolding mult.assoc[symmetric] unfolding of_int_mult[symmetric] by (simp_all add: sign_idempotent) have ths: "?s q = ?s p * ?s (q \ inv p)" using pp pq permutation_inverse[OF pp] sign_inverse[OF pp] by (simp add: th00 ac_simps sign_idempotent sign_compose) have th001: "prod (\i. B$i$ q (inv p i)) ?U = prod ((\i. B$i$ q (inv p i)) \ p) ?U" by (rule prod.permute[OF p]) have thp: "prod (\i. (\ i. A$i$p i *s B$p i :: 'a^'n^'n) $i $ q i) ?U =
prod (\<lambda>i. A$i$p i) ?U * prod (\<lambda>i. B$i$ q (inv p i)) ?U" unfolding th001 prod.distrib[symmetric] o_def permutes_inverses[OF p] apply (rule prod.cong[OF refl]) using permutes_in_image[OF q] apply vector done show"?s q * prod (\i. (((\ i. A$i$p i *s B$p i) :: 'a^'n^'n)$i$q i)) ?U =
?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)" using ths thp pp pq permutation_inverse[OF pp] sign_inverse[OF pp] by (simp add: sign_nz th00 field_simps sign_idempotent sign_compose) qed rule
} thenhave th2: "sum (\f. det (\ i. A$i$f i *s B$f i)) ?PU = det A * det B" unfolding det_def sum_product by (rule sum.cong [OF refl]) have"det (A**B) = sum (\f. det (\ i. A $ i $ f i *s B $ f i)) ?F" unfolding matrix_mul_sum_alt det_linear_rows_sum[OF finite] by simp alsohave"\ = sum (\f. det (\ i. A$i$f i *s B$f i)) ?PU" using sum.mono_neutral_cong_left[OF finite PUF zth, symmetric] unfolding det_rows_mul by auto finallyshow ?thesis unfolding th2 . qed
subsection \<open>Relation to invertibility\<close>
proposition invertible_det_nz: fixes A::"'a::{field}^'n^'n" shows"invertible A \ det A \ 0" proof (cases "invertible A") case True thenobtain B :: "'a^'n^'n"where B: "A ** B = mat 1" unfolding invertible_right_inverse by blast thenhave"det (A ** B) = det (mat 1 :: 'a^'n^'n)" by simp thenshow ?thesis by (metis True det_I det_mul mult_zero_left one_neq_zero) next case False let ?U = "UNIV :: 'n set" have fU: "finite ?U" by simp from False obtain c i where c: "sum (\i. c i *s row i A) ?U = 0" and iU: "i \ ?U" and ci: "c i \ 0" unfolding invertible_right_inverse matrix_right_invertible_independent_rows by blast have thr0: "- row i A = sum (\j. (1/ c i) *s (c j *s row j A)) (?U - {i})" unfolding sum_cmul using c ci by (auto simp: sum.remove[OF fU iU] eq_vector_fraction_iff add_eq_0_iff) have thr: "- row i A \ vec.span {row j A| j. j \ i}" unfolding thr0 by (auto intro: vec.span_base vec.span_scale vec.span_sum) let ?B = "(\ k. if k = i then 0 else row k A) :: 'a^'n^'n" have thrb: "row i ?B = 0"using iU by (vector row_def) have"det A = 0" unfolding det_row_span[OF thr, symmetric] right_minus unfolding det_zero_row(2)[OF thrb] .. thenshow ?thesis by (simp add: False) qed
lemma det_nz_iff_inj_gen: fixes f :: "'a::field^'n \ 'a::field^'n" assumes"Vector_Spaces.linear (*s) (*s) f" shows"det (matrix f) \ 0 \ inj f" proof assume"det (matrix f) \ 0" thenshow"inj f" using assms invertible_det_nz inj_matrix_vector_mult by force next assume"inj f" show"det (matrix f) \ 0" using vec.linear_injective_left_inverse [OF assms \<open>inj f\<close>] by (metis assms invertible_det_nz invertible_left_inverse matrix_compose_gen matrix_id_mat_1) qed
lemma det_eq_0_rank: fixes A :: "real^'n^'n" shows"det A = 0 \ rank A < CARD('n)" using invertible_det_nz [of A] by (auto simp: matrix_left_invertible_injective invertible_left_inverse less_rank_noninjective)
subsubsection\<^marker>\<open>tag important\<close> \<open>Invertibility of matrices and corresponding linear functions\<close>
lemma matrix_left_invertible_gen: fixes f :: "'a::field^'m \ 'a::field^'n" assumes"Vector_Spaces.linear (*s) (*s) f" shows"((\B. B ** matrix f = mat 1) \ (\g. Vector_Spaces.linear (*s) (*s) g \ g \ f = id))" proof safe fix B assume 1: "B ** matrix f = mat 1" show"\g. Vector_Spaces.linear (*s) (*s) g \ g \ f = id" proof (intro exI conjI) show"Vector_Spaces.linear (*s) (*s) (\y. B *v y)" by simp show"((*v) B) \ f = id" unfolding o_def by (metis assms 1 eq_id_iff matrix_vector_mul(1) matrix_vector_mul_assoc matrix_vector_mul_lid) qed next fix g assume"Vector_Spaces.linear (*s) (*s) g" "g \ f = id" thenhave"matrix g ** matrix f = mat 1" by (metis assms matrix_compose_gen matrix_id_mat_1) thenshow"\B. B ** matrix f = mat 1" .. qed
lemma matrix_left_invertible: "linear f \ ((\B. B ** matrix f = mat 1) \ (\g. linear g \ g \ f = id))" for f::"real^'m \ real^'n" using matrix_left_invertible_gen[of f] by (auto simp: linear_matrix_vector_mul_eq)
lemma matrix_right_invertible_gen: fixes f :: "'a::field^'m \ 'a^'n" assumes"Vector_Spaces.linear (*s) (*s) f" shows"((\B. matrix f ** B = mat 1) \ (\g. Vector_Spaces.linear (*s) (*s) g \ f \ g = id))" proof safe fix B assume 1: "matrix f ** B = mat 1" show"\g. Vector_Spaces.linear (*s) (*s) g \ f \ g = id" proof (intro exI conjI) show"Vector_Spaces.linear (*s) (*s) ((*v) B)" by simp show"f \ (*v) B = id" using 1 assms comp_apply eq_id_iff vec.linear_id matrix_id_mat_1 matrix_vector_mul_assoc matrix_works by (metis (no_types, opaque_lifting)) qed next fix g assume"Vector_Spaces.linear (*s) (*s) g" and "f \ g = id" thenhave"matrix f ** matrix g = mat 1" by (metis assms matrix_compose_gen matrix_id_mat_1) thenshow"\B. matrix f ** B = mat 1" .. qed
lemma matrix_right_invertible: "linear f \ ((\B. matrix f ** B = mat 1) \ (\g. linear g \ f \ g = id))" for f::"real^'m \ real^'n" using matrix_right_invertible_gen[of f] by (auto simp: linear_matrix_vector_mul_eq)
lemma matrix_invertible_gen: fixes f :: "'a::field^'m \ 'a::field^'n" assumes"Vector_Spaces.linear (*s) (*s) f" shows"invertible (matrix f) \ (\g. Vector_Spaces.linear (*s) (*s) g \ f \ g = id \ g \ f = id)"
(is"?lhs = ?rhs") proof assume ?lhs thenshow ?rhs by (metis assms invertible_def left_right_inverse_eq matrix_left_invertible_gen matrix_right_invertible_gen) next assume ?rhs thenshow ?lhs by (metis assms invertible_def matrix_compose_gen matrix_id_mat_1) qed
lemma matrix_invertible: "linear f \ invertible (matrix f) \ (\g. linear g \ f \ g = id \ g \ f = id)" for f::"real^'m \ real^'n" using matrix_invertible_gen[of f] by (auto simp: linear_matrix_vector_mul_eq)
lemma invertible_eq_bij: fixes m :: "'a::field^'m^'n" shows"invertible m \ bij ((*v) m)" using matrix_invertible_gen[OF matrix_vector_mul_linear_gen, of m, simplified matrix_of_matrix_vector_mul] by (metis bij_betw_def left_right_inverse_eq matrix_vector_mul_linear_gen o_bij
vec.linear_injective_left_inverse vec.linear_surjective_right_inverse)
subsection \<open>Cramer's rule\<close>
lemma cramer_lemma_transpose: fixes A:: "'a::{field}^'n^'n" and x :: "'a::{field}^'n" shows"det ((\ i. if i = k then sum (\i. x$i *s row i A) (UNIV::'n set)
else row i A)::'a::{field}^'n^'n) = x$k * det A"
(is"?lhs = ?rhs") proof - let ?U = "UNIV :: 'n set" let ?Uk = "?U - {k}" have U: "?U = insert k ?Uk" by blast have kUk: "k \ ?Uk" by simp have th00: "\k s. x$k *s row k A + s = (x$k - 1) *s row k A + row k A + s" by (vector field_simps) have th001: "\f k . (\x. if x = k then f k else f x) = f" by auto have"(\ i. row i A) = A" by (vector row_def) thenhave thd1: "det (\ i. row i A) = det A" by simp have thd0: "det (\ i. if i = k then row k A + (\i \ ?Uk. x $ i *s row i A) else row i A) = det A" by (force intro: det_row_span vec.span_sum vec.span_scale vec.span_base) show"?lhs = x$k * det A" apply (subst U) unfolding sum.insert[OF finite kUk] apply (subst th00) unfolding add.assoc apply (subst det_row_add) unfolding thd0 unfolding det_row_mul unfolding th001[of k "\i. row i A"] unfolding thd1 apply (simp add: field_simps) done qed
proposition cramer_lemma: fixes A :: "'a::{field}^'n^'n" shows"det((\ i j. if j = k then (A *v x)$i else A$i$j):: 'a::{field}^'n^'n) = x$k * det A" proof - let ?U = "UNIV :: 'n set" have *: "\c. sum (\i. c i *s row i (transpose A)) ?U = sum (\i. c i *s column i A) ?U" by (auto intro: sum.cong) show ?thesis unfolding matrix_mult_sum unfolding cramer_lemma_transpose[of k x "transpose A", unfolded det_transpose, symmetric] unfolding *[of "\i. x$i"] apply (subst det_transpose[symmetric]) apply (rule cong[OF refl[of det]]) apply (vector transpose_def column_def row_def) done qed
proposition cramer: fixes A ::"'a::{field}^'n^'n" assumes d0: "det A \ 0" shows"A *v x = b \ x = (\ k. det(\ i j. if j=k then b$i else A$i$j) / det A)" proof - from d0 obtain B where B: "A ** B = mat 1""B ** A = mat 1" unfolding invertible_det_nz[symmetric] invertible_def by blast have"(A ** B) *v b = b" by (simp add: B) thenhave"A *v (B *v b) = b" by (simp add: matrix_vector_mul_assoc) thenhave xe: "\x. A *v x = b" by blast
{ fix x assume x: "A *v x = b" have"x = (\ k. det(\ i j. if j=k then b$i else A$i$j) / det A)" unfolding x[symmetric] using d0 by (simp add: vec_eq_iff cramer_lemma field_simps)
} with xe show ?thesis by auto qed
text\<open> Slightly stronger results giving rotation, but only in two or more dimensions\<close>
lemma rotation_matrix_exists_basis: fixes a :: "real^'n" assumes 2: "2 \ CARD('n)" and "norm a = 1" obtains A where"rotation_matrix A""A *v (axis k 1) = a" proof - obtain A where"orthogonal_matrix A"and A: "A *v (axis k 1) = a" using orthogonal_matrix_exists_basis assms by metis with orthogonal_rotation_or_rotoinversion
consider "rotation_matrix A" | "rotoinversion_matrix A" by metis thenshow thesis proof cases assume"rotation_matrix A" thenshow ?thesis using\<open>A *v axis k 1 = a\<close> that by auto next from obtain_subset_with_card_n[OF 2] obtain h i::'n where "h \ i" by (fastforce simp add: eval_nat_numeral card_Suc_eq) thenobtain j where"j \ k" by (metis (full_types)) let ?TA = "transpose A" let ?A = "\ i. if i = j then - 1 *\<^sub>R (?TA $ i) else ?TA $i" assume"rotoinversion_matrix A" thenhave [simp]: "det A = -1" by (simp add: rotoinversion_matrix_def) show ?thesis proof have [simp]: "row i (\ 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 by (auto simp: row_def) have"orthogonal_matrix ?A" unfolding orthogonal_matrix_orthonormal_rows using\<open>orthogonal_matrix A\<close> by (auto simp: orthogonal_matrix_orthonormal_columns orthogonal_clauses) thenshow"rotation_matrix (transpose ?A)" unfolding rotation_matrix_def by (simp add: det_row_mul[of j _ "\i. ?TA $ i", unfolded scalar_mult_eq_scaleR]) show"transpose ?A *v axis k 1 = a" 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) qed qed qed
lemma rotation_exists_1: fixes a :: "real^'n" assumes"2 \ CARD('n)" "norm a = 1" "norm b = 1" obtains f where"orthogonal_transformation f""det(matrix f) = 1""f a = b" proof - obtain k::'n where True by simp obtain A B where AB: "rotation_matrix A""rotation_matrix B" and eq: "A *v (axis k 1) = a""B *v (axis k 1) = b" using rotation_matrix_exists_basis assms by metis let ?f = "\x. (B ** transpose A) *v x" show thesis proof show"orthogonal_transformation ?f" using AB orthogonal_matrix_mul orthogonal_transformation_matrix rotation_matrix_def matrix_vector_mul_linear by force show"det (matrix ?f) = 1" using AB by (auto simp: det_mul rotation_matrix_def) show"?f a = b" using AB unfolding orthogonal_matrix_def rotation_matrix_def by (metis eq matrix_mul_rid matrix_vector_mul_assoc) qed qed
lemma rotation_exists: fixes a :: "real^'n" assumes 2: "2 \ CARD('n)" and eq: "norm a = norm b" obtains f where"orthogonal_transformation f""det(matrix f) = 1""f a = b" proof (cases "a = 0 \ b = 0") case True with assms have"a = 0""b = 0" by auto thenshow ?thesis by (metis eq_id_iff matrix_id orthogonal_transformation_id that) next case False thenobtain f where f: "orthogonal_transformation f""det (matrix f) = 1" and f': "f (a /\<^sub>R norm a) = b /\<^sub>R norm b" using rotation_exists_1 [of "a /\<^sub>R norm a" "b /\<^sub>R norm b", OF 2] by auto theninterpret linear f by (simp add: orthogonal_transformation) have"f a = b" using f' False by (simp add: eq scale) with f show thesis .. qed
lemma rotation_rightward_line: fixes a :: "real^'n" obtains f where"orthogonal_transformation f""2 \ CARD('n) \ det(matrix f) = 1" "f(norm a *\<^sub>R axis k 1) = a" proof (cases "CARD('n) = 1") case True obtain f where"orthogonal_transformation f""f (norm a *\<^sub>R axis k (1::real)) = a" proof (rule orthogonal_transformation_exists) show"norm (norm a *\<^sub>R axis k (1::real)) = norm a" by simp qed auto thenshow thesis using True that by auto next case False obtain f where"orthogonal_transformation f""det(matrix f) = 1""f (norm a *\<^sub>R axis k 1) = a" proof (rule rotation_exists) show"2 \ CARD('n)" using False one_le_card_finite [where'a='n] by linarith show"norm (norm a *\<^sub>R axis k (1::real)) = norm a" by simp qed auto thenshow thesis using that by blast qed
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
