Up to index of Isabelle/HOL/HOL-Multivariate_Analysis/Gauss-Jordan
theory Elementary_Operationstheory Elementary_Operations
imports Main
"~~/src/HOL/Multivariate_Analysis/Linear_Algebra"
"~~/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space"
"Dim_Formula"
"Numeral_Type_Addenda"
begin
(*
Title: Elementary_Operations.thy
Author: Jose Divasón <jose.divasonm at unirioja.es>
Author: Jesús Aransay <jesus-maria.aransay at unirioja.es>
*)
section{*Previous definitions*}
definition nrows :: "'a^'columns^'rows => nat"
where "nrows A = CARD('rows)"
definition ncols :: "'a^'columns^'rows => nat"
where "ncols A = CARD('columns)"
lemma nrows_not_0[simp]:
shows "0 ≠ nrows A" unfolding nrows_def by simp
lemma ncols_not_0[simp]:
shows "0 ≠ ncols A" unfolding ncols_def by simp
section{*Code Generation for matrices*}
lemma [code abstype]: "vec_lambda (vec_nth v) = (v::('a::{type}, 'b::{finite}) vec)"
using vec_lambda_eta by fast
lemma [code abstract]: "vec_nth 0 = (%x. 0)" by (metis zero_index)
lemma [code abstract]: "vec_nth (a + b) = (%i. a$i + b$i)" by (metis vector_add_component)
definition mat_mult_row
where "mat_mult_row m m' f = vec_lambda (%c. setsum (%k. ((m$f)$k) * ((m'$k)$c)) (UNIV :: 'n::finite set))"
lemma mat_mult_row_code [code abstract]:
"vec_nth (mat_mult_row m m' f) = (%c. setsum (%k. ((m$f)$k) * ((m'$k)$c)) (UNIV :: 'n::finite set))"
by(simp add: mat_mult_row_def fun_eq_iff)
lemma mat_mult [code abstract]: "vec_nth (m ** m') = mat_mult_row m m'"
unfolding matrix_matrix_mult_def mat_mult_row_def[abs_def]
using vec_lambda_beta by auto
lemma [code abstract]: "vec_nth (a + b) = (%i. a $ i + b $ i)" by (metis vector_add_component)
section{*Elementary Operations*}
text{*Some previous results:*}
lemma invertible_mult:
assumes inv_A: "invertible A"
and inv_B: "invertible B"
shows "invertible (A**B)"
proof -
obtain A' where AA': "A ** A' = mat 1" and A'A: "A' ** A = mat 1" using inv_A unfolding invertible_def by blast
obtain B' where BB': "B ** B' = mat 1" and B'B: "B' ** B = mat 1" using inv_B unfolding invertible_def by blast
show ?thesis
proof (unfold invertible_def, rule exI[of _ "B'**A'"], rule conjI)
have "A ** B ** (B' ** A') = A ** (B ** (B' ** A'))" using matrix_mul_assoc[of A B "(B' ** A')", symmetric] .
also have "... = A ** (B ** B' ** A')" unfolding matrix_mul_assoc[of B "B'" "A'"] ..
also have "... = A ** (mat 1 ** A')" unfolding BB' ..
also have "... = A ** A'" unfolding matrix_mul_lid ..
also have "... = mat 1" unfolding AA' ..
finally show "A ** B ** (B' ** A') = mat (1::'a)" .
have "B' ** A' ** (A ** B) = B' ** (A' ** (A ** B))" using matrix_mul_assoc[of B' A' "(A ** B)", symmetric] .
also have "... = B' ** (A' ** A ** B)" unfolding matrix_mul_assoc[of A' A B] ..
also have "... = B' ** (mat 1 ** B)" unfolding A'A ..
also have "... = B' ** B" unfolding matrix_mul_lid ..
also have "... = mat 1" unfolding B'B ..
finally show "B' ** A' ** (A ** B) = mat 1" .
qed
qed
text{*In the library, @{thm "matrix_inv_def"} allows the use of non squary matrices.
The following lemma can be also proved fixing @{term "A::'a::{semiring_1}^'n^'m"}*}
lemma matrix_inv_unique:
fixes A::"'a::{semiring_1}^'n^'n"
assumes AB: "A**B=mat 1" and BA: "B**A=mat 1"
shows "matrix_inv A = B"
proof (unfold matrix_inv_def, rule some_equality)
show "A ** B = mat (1::'a) ∧ B ** A = mat (1::'a)" using AB BA by simp
fix C assume "A ** C = mat (1::'a) ∧ C ** A = mat (1::'a)"
hence AC: "A ** C = mat (1::'a)" and CA: "C ** A = mat (1::'a)" by auto
have "B = B ** (mat 1)" unfolding matrix_mul_rid ..
also have "... = B ** (A**C)" unfolding AC ..
also have "... = B ** A ** C" unfolding matrix_mul_assoc ..
also have "... = C" unfolding BA matrix_mul_lid ..
finally show "C = B" ..
qed
lemma mat_1_fun: "mat 1 $ a $ b = (λi j. if i=j then 1 else 0) a b" unfolding mat_def by auto
lemma mat1_sum_eq:
shows "(∑k∈UNIV. mat (1::'a::{semiring_1}) $ s $ k * mat 1 $ k $ t) = mat 1 $ s $ t"
proof (unfold mat_def, auto)
let ?f="λk. (if t = k then 1::'a else (0::'a)) * (if k = t then 1::'a else (0::'a))"
have univ_eq: "UNIV = (UNIV - {t}) ∪ {t}" by fast
have "setsum ?f UNIV = setsum ?f ((UNIV - {t}) ∪ {t}) " using univ_eq by simp
also have "... = setsum ?f (UNIV - {t}) + setsum ?f {t}" by (rule setsum_Un_disjoint, auto)
also have "... = 0 + setsum ?f {t}" by auto
also have "... = setsum ?f {t}" by simp
also have "... = 1" by simp
finally show "setsum ?f UNIV = 1" .
next
assume s_not_t: "s ≠ t"
let ?g="λk. (if s = k then 1::'a else 0) * (if k = t then 1 else 0)"
have "setsum ?g UNIV = setsum (λk. 0::'a) (UNIV::'b set)" by (rule setsum_cong2, simp add: s_not_t)
also have "... = 0" by simp
finally show "setsum ?g UNIV = 0" .
qed
lemma finite_rows: "finite (rows A)"
proof -
def f≡"λi. row i A"
show ?thesis unfolding rows_def using finite_Atleast_Atmost_nat[of f] unfolding f_def by simp
qed
lemma finite_columns: "finite (columns A)"
proof -
def f≡"λi. column i A"
show ?thesis unfolding columns_def using finite_Atleast_Atmost_nat[of f] unfolding f_def by simp
qed
lemma invertible_mat_n:
fixes n::"'a::{field}"
assumes n: "n ≠ 0"
shows "invertible ((mat n)::'a^'n^'n)"
proof (unfold invertible_def, rule exI[of _ "mat (inverse n)"], rule conjI)
show "mat n ** mat (inverse n) = (mat 1::'a^'n^'n)"
proof (unfold matrix_matrix_mult_def mat_def, vector, auto)
fix ia::'n
let ?f="(λk. (if ia = k then n else 0) * (if k = ia then inverse n else 0))"
have UNIV_rw: "(UNIV::'n set) = insert ia (UNIV-{ia})" by auto
have "(∑k∈(UNIV::'n set). (if ia = k then n else 0) * (if k = ia then inverse n else 0)) =
(∑k∈insert ia (UNIV-{ia}). (if ia = k then n else 0) * (if k = ia then inverse n else 0))" using UNIV_rw by simp
also have "... = ?f ia + setsum ?f (UNIV-{ia})"
proof (rule setsum.insert)
show "finite (UNIV - {ia})" using finite_UNIV by fastforce
show "ia ∉ UNIV - {ia}" by fast
qed
also have "... = 1" using right_inverse[OF n] by simp
finally show " (∑k∈(UNIV::'n set). (if ia = k then n else 0) * (if k = ia then inverse n else 0)) = (1::'a)" .
fix i::'n
assume i_not_ia: "i ≠ ia"
show "(∑k∈(UNIV::'n set). (if i = k then n else 0) * (if k = ia then inverse n else 0)) = 0" by (rule setsum_0', simp add: i_not_ia)
qed
next
show "mat (inverse n) ** mat n = ((mat 1)::'a^'n^'n)"
proof (unfold matrix_matrix_mult_def mat_def, vector, auto)
fix ia::'n
let ?f=" (λk. (if ia = k then inverse n else 0) * (if k = ia then n else 0))"
have UNIV_rw: "(UNIV::'n set) = insert ia (UNIV-{ia})" by auto
have "(∑k∈(UNIV::'n set). (if ia = k then inverse n else 0) * (if k = ia then n else 0)) =
(∑k∈insert ia (UNIV-{ia}). (if ia = k then inverse n else 0) * (if k = ia then n else 0))" using UNIV_rw by simp
also have "... = ?f ia + setsum ?f (UNIV-{ia})"
proof (rule setsum.insert)
show "finite (UNIV - {ia})" using finite_UNIV by fastforce
show "ia ∉ UNIV - {ia}" by fast
qed
also have "... = 1" using left_inverse[OF n] by simp
finally show " (∑k∈(UNIV::'n set). (if ia = k then inverse n else 0) * (if k = ia then n else 0)) = (1::'a)" .
fix i::'n
assume i_not_ia: "i ≠ ia"
show "(∑k∈(UNIV::'n set). (if i = k then inverse n else 0) * (if k = ia then n else 0)) = 0" by (rule setsum_0', simp add: i_not_ia)
qed
qed
corollary invertible_mat_1:
shows "invertible (mat (1::'a::{field}))" by (metis invertible_mat_n zero_neq_one)
text{*Functions between two real vector spaces form a real vector*}
instantiation "fun" :: (real_vector, real_vector) real_vector
begin
definition "plus_fun f g = (λi. f i + g i)"
definition "zero_fun = (λi. 0)"
definition "scaleR_fun a f = (λi. a *⇩R f i )"
instance proof
fix a::"'a => 'b" and b::"'a => 'b" and c::"'a => 'b"
show "a + b + c = a + (b + c)" unfolding fun_eq_iff unfolding plus_fun_def by auto
show "a + b = b + a" unfolding fun_eq_iff unfolding plus_fun_def by auto
show " (0::'a => 'b) + a = a" unfolding fun_eq_iff unfolding plus_fun_def zero_fun_def by auto
show "- a + a = (0::'a => 'b)" unfolding fun_eq_iff unfolding plus_fun_def zero_fun_def by auto
show "a - b = a + - b" unfolding fun_eq_iff unfolding plus_fun_def zero_fun_def by auto
next
fix a::real and x::"('a => 'b)" and y::"'a => 'b"
show "a *⇩R (x + y) = a *⇩R x + a *⇩R y"
unfolding fun_eq_iff plus_fun_def scaleR_fun_def scaleR_right.add by auto
next
fix a::real and b::real and x::"'a => 'b"
show "(a + b) *⇩R x = a *⇩R x + b *⇩R x"
unfolding fun_eq_iff unfolding plus_fun_def scaleR_fun_def unfolding scaleR_left.add by auto
show " a *⇩R b *⇩R x = (a * b) *⇩R x" unfolding fun_eq_iff unfolding scaleR_fun_def by auto
show "(1::real) *⇩R x = x" unfolding fun_eq_iff unfolding scaleR_fun_def by auto
qed
end
text{*Definitions of elementary row operations*}
definition interchange_rows :: "('a::semiring_1) ^'n^'m => 'm => 'm => 'a ^'n^'m"
where "interchange_rows A a b = (χ i j. if i=a then A $ b $ j else if i=b then A $ a $ j else A $ i $ j)"
definition mult_row :: "('a::semiring_1) ^'n^'m => 'm => 'a => 'a ^'n^'m"
where "mult_row A a q = (χ i j. if i=a then q*(A $ a $ j) else A $ i $ j)"
definition row_add :: "('a::semiring_1) ^'n^'m => 'm => 'm => 'a => 'a ^'n^'m"
where "row_add A a b q = (χ i j. if i=a then (A $ a $ j) + q*(A $ b $ j) else A $ i $ j)"
text{*Definitions of elementary column operations*}
definition interchange_columns :: "('a::semiring_1) ^'n^'m => 'n => 'n => 'a ^'n^'m"
where "interchange_columns A n m = (χ i j. if j=n then A $ i $ m else if j=m then A $ i $ n else A $ i $ j)"
definition mult_column :: "('a::semiring_1) ^'n^'m => 'n => 'a => 'a ^'n^'m"
where " mult_column A n q = (χ i j. if j=n then (A $ i $ j)*q else A $ i $ j)"
definition column_add :: "('a::semiring_1) ^'n^'m => 'n => 'n => 'a => 'a ^'n^'m"
where "column_add A n m q = (χ i j. if j=n then ((A $ i $ n) + (A $ i $ m)*q) else A $ i $ j)"
text{*Properties about @{term "interchange_rows"}*}
lemma interchange_same_rows: "interchange_rows A a a = A"
unfolding interchange_rows_def by vector
lemma interchange_rows_i[simp]: "interchange_rows A i j $ i = A $ j"
unfolding interchange_rows_def by vector
lemma interchange_rows_j[simp]: "interchange_rows A i j $ j = A $ i"
unfolding interchange_rows_def by vector
lemma interchange_rows_preserves:
assumes "i ≠ a" and "j ≠ a"
shows "interchange_rows A i j $ a = A $ a"
using assms unfolding interchange_rows_def by vector
lemma interchange_rows_mat_1:
shows "interchange_rows (mat 1) a b ** A = interchange_rows A a b"
proof (unfold matrix_matrix_mult_def interchange_rows_def, vector, auto)
fix ia
let ?f="(λk. mat (1::'a) $ a $ k * A $ k $ ia)"
have univ_rw:"UNIV = (UNIV-{a}) ∪ {a}" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV-{a}) ∪ {a})" using univ_rw by auto
also have "... = setsum ?f (UNIV-{a}) + setsum ?f {a}"
proof (rule setsum_Un_disjoint)
show "finite (UNIV - {a})" by (metis finite_code)
show "finite {a}" by simp
show "(UNIV - {a}) ∩ {a} = {}" by simp
qed
also have "... = setsum ?f {a}" unfolding mat_def by auto
also have "... = ?f a" by auto
also have "... = A $ a $ ia" unfolding mat_def by auto
finally show "(∑k∈UNIV. mat (1::'a) $ a $ k * A $ k $ ia) = A $ a $ ia" .
assume i: " a ≠ b"
let ?g= "λk. mat (1::'a) $ b $ k * A $ k $ ia"
have univ_rw':"UNIV = (UNIV-{b}) ∪ {b}" by auto
have "setsum ?g UNIV = setsum ?g ((UNIV-{b}) ∪ {b})" using univ_rw' by auto
also have "... = setsum ?g (UNIV-{b}) + setsum ?g {b}" by (rule setsum_Un_disjoint, auto)
also have "... = setsum ?g {b}" unfolding mat_def by auto
also have "... = ?g b" by simp
finally show "(∑k∈UNIV. mat (1::'a) $ b $ k * A $ k $ ia) = A $ b $ ia" unfolding mat_def by simp
next
fix i j
assume ib: "i ≠ b" and ia:"i ≠ a"
let ?h="λk. mat (1::'a) $ i $ k * A $ k $ j"
have univ_rw'':"UNIV = (UNIV-{i}) ∪ {i}" by auto
have "setsum ?h UNIV = setsum ?h ((UNIV-{i}) ∪ {i})" using univ_rw'' by auto
also have "... = setsum ?h (UNIV-{i}) + setsum ?h {i}" by (rule setsum_Un_disjoint, auto)
also have "... = setsum ?h {i}" unfolding mat_def by auto
also have "... = ?h i" by simp
finally show " (∑k∈UNIV. mat (1::'a) $ i $ k * A $ k $ j) = A $ i $ j" unfolding mat_def by auto
qed
lemma invertible_interchange_rows: "invertible (interchange_rows (mat 1) a b)"
proof (unfold invertible_def, rule exI[of _ "interchange_rows (mat 1) a b"], simp, unfold matrix_matrix_mult_def, vector, clarify,
unfold interchange_rows_def, vector, unfold mat_1_fun, auto+)
fix s t::"'b"
assume s_not_t: "s ≠ t"
show " (∑k::'b∈UNIV. (if s = k then 1::'a else (0::'a)) * (if k = t then 1::'a else if k = t then 1::'a else if k = t then 1::'a else (0::'a))) = (0::'a)"
by (rule setsum_0', simp add: s_not_t)
assume b_not_t: "b ≠ t"
show "(∑k∈UNIV. (if s = b then if t = k then 1::'a else (0::'a) else if s = k then 1::'a else (0::'a)) *
(if k = t then 0::'a else if k = b then 1::'a else if k = t then 1::'a else (0::'a))) =
(0::'a)" by (rule setsum_0', simp)
assume a_not_t: "a ≠ t"
show "(∑k∈UNIV. (if s = a then if b = k then 1::'a else (0::'a) else if s = b then if a = k then 1::'a else (0::'a) else if s = k then 1::'a else (0::'a)) *
(if k = a then 0::'a else if k = b then 0::'a else if k = t then 1::'a else (0::'a))) =
(0::'a)" by (rule setsum_0', auto simp add: s_not_t)
next
fix s t::"'b"
assume a_noteq_t: "a≠t" and s_noteq_t: "s ≠ t"
show " (∑k∈UNIV. (if s = a then if t = k then 1::'a else (0::'a) else if s = t then if a = k then 1::'a else (0::'a) else if s = k then 1::'a else (0::'a)) *
(if k = a then 1::'a else if k = t then 0::'a else if k = t then 1::'a else (0::'a))) =
(0::'a)" apply (rule setsum_0') using s_noteq_t by fastforce
next
fix s t::"'b"
show "(∑k∈UNIV. (if t = k then 1::'a else (0::'a)) * (if k = t then 1::'a else if k = t then 1::'a else if k = t then 1::'a else (0::'a))) = (1::'a)"
proof -
let ?f="(λk. (if t = k then 1::'a else (0::'a)) * (if k = t then 1::'a else if k = t then 1::'a else if k = t then 1::'a else (0::'a)))"
have univ_eq: "UNIV = ((UNIV - {t}) ∪ {t})" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV - {t}) ∪ {t}) " using univ_eq by simp
also have "... = setsum ?f (UNIV - {t}) + setsum ?f {t}" by (rule setsum_Un_disjoint, auto)
also have "... = 0 + setsum ?f {t}" by auto
also have "... = setsum ?f {t}" by simp
also have "... = 1" by simp
finally show ?thesis .
qed
next
fix s t::"'b"
assume b_noteq_t: "b ≠ t"
show " (∑k∈UNIV. (if b = k then 1::'a else (0::'a)) * (if k = t then 0::'a else if k = b then 1::'a else if k = t then 1::'a else (0::'a))) = (1::'a)"
proof -
let ?f="(λk. (if b = k then 1::'a else (0::'a)) * (if k = t then 0::'a else if k = b then 1::'a else if k = t then 1::'a else (0::'a)))"
have univ_eq: "UNIV = ((UNIV - {b}) ∪ {b})" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV - {b}) ∪ {b}) " using univ_eq by simp
also have "... = setsum ?f (UNIV - {b}) + setsum ?f {b}" by (rule setsum_Un_disjoint, auto)
also have "... = 0 + setsum ?f {b}" by auto
also have "... = setsum ?f {b}" by simp
also have "... = 1" using b_noteq_t by simp
finally show ?thesis .
qed
assume a_noteq_t: "a≠t"
show " (∑k∈UNIV. (if t = k then 1::'a else (0::'a)) * (if k = a then 0::'a else if k = b then 0::'a else if k = t then 1::'a else (0::'a))) = (1::'a)"
proof -
let ?f="(λk. (if t = k then 1::'a else (0::'a)) * (if k = a then 0::'a else if k = b then 0::'a else if k = t then 1::'a else (0::'a)))"
have univ_eq: "UNIV = ((UNIV - {t}) ∪ {t})" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV - {t}) ∪ {t}) " using univ_eq by simp
also have "... = setsum ?f (UNIV - {t}) + setsum ?f {t}" by (rule setsum_Un_disjoint, auto)
also have "... = 0 + setsum ?f {t}" by auto
also have "... = setsum ?f {t}" by simp
also have "... = 1" using b_noteq_t a_noteq_t by simp
finally show ?thesis .
qed
next
fix s t::"'b"
assume a_noteq_t: "a≠t"
show "(∑k∈UNIV. (if a = k then 1::'a else (0::'a)) * (if k = a then 1::'a else if k = t then 0::'a else if k = t then 1::'a else (0::'a))) = (1::'a)"
proof -
let ?f="λk. (if a = k then 1::'a else (0::'a)) * (if k = a then 1::'a else if k = t then 0::'a else if k = t then 1::'a else (0::'a))"
have univ_eq: "UNIV = ((UNIV - {a}) ∪ {a})" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV - {a}) ∪ {a}) " using univ_eq by simp
also have "... = setsum ?f (UNIV - {a}) + setsum ?f {a}" by (rule setsum_Un_disjoint, auto)
also have "... = 0 + setsum ?f {a}" by auto
also have "... = setsum ?f {a}" by simp
also have "... = 1" using a_noteq_t by simp
finally show ?thesis .
qed
qed
text{*Properties about @{term "mult_row"}*}
lemma mult_row_mat_1: "mult_row (mat 1) a q ** A = mult_row A a q"
proof (unfold matrix_matrix_mult_def mult_row_def, vector, auto)
fix ia
let ?f="λk. q * mat (1::'a) $ a $ k * A $ k $ ia"
have univ_rw:"UNIV = (UNIV-{a}) ∪ {a}" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV-{a}) ∪ {a})" using univ_rw by auto
also have "... = setsum ?f (UNIV-{a}) + setsum ?f {a}" by (rule setsum_Un_disjoint, auto)
also have "... = setsum ?f {a}" unfolding mat_def by auto
also have "... = ?f a" by auto
also have "... = q * A $ a $ ia" unfolding mat_def by auto
finally show "(∑k∈UNIV. q * mat (1::'a) $ a $ k * A $ k $ ia) = q * A $ a $ ia" .
fix i
assume i: "i ≠ a"
let ?g="λk. mat (1::'a) $ i $ k * A $ k $ ia"
have univ_rw'':"UNIV = (UNIV-{i}) ∪ {i}" by auto
have "setsum ?g UNIV = setsum ?g ((UNIV-{i}) ∪ {i})" using univ_rw'' by auto
also have "... = setsum ?g (UNIV-{i}) + setsum ?g {i}" by (rule setsum_Un_disjoint, auto)
also have "... = setsum ?g {i}" unfolding mat_def by auto
also have "... = ?g i" by simp
finally show "(∑k∈UNIV. mat (1::'a) $ i $ k * A $ k $ ia) = A $ i $ ia" unfolding mat_def by simp
qed
lemma invertible_mult_row:
assumes qk: "q*k=1" and kq: "k*q=1"
shows "invertible (mult_row (mat 1) a q)"
proof (unfold invertible_def, rule exI[of _ "mult_row (mat 1) a k"],rule conjI)
show "mult_row (mat (1::'a)) a q ** mult_row (mat (1::'a)) a k = mat (1::'a)"
proof (unfold matrix_matrix_mult_def, vector, clarify, unfold mult_row_def, vector, unfold mat_1_fun, auto)
show "(∑ka∈UNIV. q * (if a = ka then 1::'a else (0::'a)) * (if ka = a then k * (1::'a) else if ka = a then 1::'a else (0::'a))) = (1::'a)"
proof -
let ?f="λka. q * (if a = ka then 1::'a else (0::'a)) * (if ka = a then k * (1::'a) else if ka = a then 1::'a else (0::'a)) "
have univ_eq: "UNIV = ((UNIV - {a}) ∪ {a})" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV - {a}) ∪ {a}) " using univ_eq by simp
also have "... = setsum ?f (UNIV - {a}) + setsum ?f {a}" by (rule setsum_Un_disjoint, auto)
also have "... = 0 + setsum ?f {a}" by auto
also have "... = setsum ?f {a}" by simp
also have "... = 1" using qk by simp
finally show ?thesis .
qed
next
fix s
assume s_noteq_a: "s≠a"
show "(∑ka∈UNIV. (if s = ka then 1::'a else (0::'a)) * (if ka = a then k * (1::'a) else if ka = a then 1::'a else 0)) = 0"
by (rule setsum_0', simp add: s_noteq_a)
next
fix t
assume a_noteq_t: "a≠t"
show "(∑ka∈UNIV. (if t = ka then 1::'a else (0::'a)) * (if ka = a then k * (0::'a) else if ka = t then 1::'a else (0::'a))) = (1::'a)"
proof -
let ?f="λka. (if t = ka then 1::'a else (0::'a)) * (if ka = a then k * (0::'a) else if ka = t then 1::'a else (0::'a)) "
have univ_eq: "UNIV = ((UNIV - {t}) ∪ {t})" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV - {t}) ∪ {t}) " using univ_eq by simp
also have "... = setsum ?f (UNIV - {t}) + setsum ?f {t}" by (rule setsum_Un_disjoint, auto)
also have "... = setsum ?f {t}" by simp
also have "... = 1" using a_noteq_t by auto
finally show ?thesis .
qed
fix s
assume s_not_t: "s≠t"
show "(∑ka∈UNIV. (if s = a then q * (if a = ka then 1::'a else (0::'a)) else if s = ka then 1::'a else (0::'a)) *
(if ka = a then k * (0::'a) else if ka = t then 1::'a else (0::'a))) = (0::'a)"
by (rule setsum_0', simp add: s_not_t a_noteq_t)
qed
show "mult_row (mat (1::'a)) a k ** mult_row (mat (1::'a)) a q = mat (1::'a)"
proof (unfold matrix_matrix_mult_def, vector, clarify, unfold mult_row_def, vector, unfold mat_1_fun, auto)
show "(∑ka∈UNIV. k * (if a = ka then 1::'a else (0::'a)) * (if ka = a then q * (1::'a) else if ka = a then 1::'a else (0::'a))) = (1::'a)"
proof -
let ?f="λka. k * (if a = ka then 1::'a else (0::'a)) * (if ka = a then q * (1::'a) else if ka = a then 1::'a else (0::'a)) "
have univ_eq: "UNIV = ((UNIV - {a}) ∪ {a})" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV - {a}) ∪ {a}) " using univ_eq by simp
also have "... = setsum ?f (UNIV - {a}) + setsum ?f {a}" by (rule setsum_Un_disjoint, auto)
also have "... = 0 + setsum ?f {a}" by auto
also have "... = setsum ?f {a}" by simp
also have "... = 1" using kq by simp
finally show ?thesis .
qed
next
fix s
assume s_not_a: "s≠a"
show "(∑k∈UNIV. (if s = k then 1::'a else (0::'a)) * (if k = a then q * (1::'a) else if k = a then 1::'a else (0::'a))) = (0::'a)"
by (rule setsum_0', simp add: s_not_a)
next
fix t
assume a_not_t: "a≠t"
show "(∑k∈UNIV. (if t = k then 1::'a else (0::'a)) * (if k = a then q * (0::'a) else if k = t then 1::'a else (0::'a))) = (1::'a)"
proof -
let ?f="λk. (if t = k then 1::'a else (0::'a)) * (if k = a then q * (0::'a) else if k = t then 1::'a else (0::'a))"
have univ_eq: "UNIV = ((UNIV - {t}) ∪ {t})" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV - {t}) ∪ {t}) " using univ_eq by simp
also have "... = setsum ?f (UNIV - {t}) + setsum ?f {t}" by (rule setsum_Un_disjoint, auto)
also have "... = setsum ?f {t}" by simp
also have "... = 1" using a_not_t by simp
finally show ?thesis .
qed
fix s
assume s_not_t: "s≠t"
show " (∑ka∈UNIV. (if s = a then k * (if a = ka then 1::'a else (0::'a)) else if s = ka then 1::'a else (0::'a)) *
(if ka = a then q * (0::'a) else if ka = t then 1::'a else (0::'a))) = (0::'a)"
by (rule setsum_0', simp add: s_not_t)
qed
qed
corollary invertible_mult_row':
assumes q_not_zero: "q ≠ 0"
shows "invertible (mult_row (mat (1::'a::{field})) a q)"
by (simp add: invertible_mult_row[of q "inverse q"] q_not_zero)
text{*Properties about @{term "row_add"}*}
lemma row_add_mat_1: "row_add (mat 1) a b q ** A = row_add A a b q"
proof (unfold matrix_matrix_mult_def row_add_def, vector, auto)
fix j
let ?f=" (λk. (mat (1::'a) $ a $ k + q * mat (1::'a) $ b $ k) * A $ k $ j)"
show "setsum ?f UNIV = A $ a $ j + q * A $ b $ j"
proof (cases "a=b")
case False
have univ_rw: "UNIV = {a} ∪ ({b} ∪ (UNIV - {a} - {b}))" by auto
have setsum_rw: "setsum ?f ({b} ∪ (UNIV - {a} - {b})) = setsum ?f {b} + setsum ?f (UNIV - {a} - {b})" by (rule setsum_Un_disjoint, auto simp add: False)
have "setsum ?f UNIV = setsum ?f ({a} ∪ ({b} ∪ (UNIV - {a} - {b})))" using univ_rw by simp
also have "... = setsum ?f {a} + setsum ?f ({b} ∪ (UNIV - {a} - {b}))" by (rule setsum_Un_disjoint, auto simp add: False)
also have "... = setsum ?f {a} + setsum ?f {b} + setsum ?f (UNIV - {a} - {b})" unfolding setsum_rw ab_semigroup_add_class.add_ac(1)[symmetric] ..
also have "... = setsum ?f {a} + setsum ?f {b}"
proof -
have "setsum ?f (UNIV - {a} - {b}) = setsum (λk. 0) (UNIV - {a} - {b})" unfolding mat_def by (rule setsum_cong2, auto)
also have "... = 0" unfolding setsum_0 ..
finally show ?thesis by simp
qed
also have "... = A $ a $ j + q * A $ b $ j" using False unfolding mat_def by simp
finally show ?thesis .
next
case True
have univ_rw: "UNIV = {b} ∪ (UNIV - {b})" by auto
have "setsum ?f UNIV = setsum ?f ({b} ∪ (UNIV - {b}))" using univ_rw by simp
also have "... = setsum ?f {b} + setsum ?f (UNIV - {b})" by (rule setsum_Un_disjoint, auto)
also have "... = setsum ?f {b}"
proof -
have "setsum ?f (UNIV - {b}) = setsum (λk. 0) (UNIV - {b})" using True unfolding mat_def by auto
also have "... = 0" unfolding setsum_0 ..
finally show ?thesis by simp
qed
also have "... = A $ a $ j + q * A $ b $ j"
by (unfold True mat_def, simp, metis (hide_lams, no_types) vector_add_component vector_sadd_rdistrib vector_smult_component vector_smult_lid)
finally show ?thesis .
qed
fix i assume i: "i≠a"
let ?g="λk. mat (1::'a) $ i $ k * A $ k $ j"
have univ_rw: "UNIV = {i} ∪ (UNIV - {i})" by auto
have "setsum ?g UNIV = setsum ?g ({i} ∪ (UNIV - {i}))" using univ_rw by simp
also have "... = setsum ?g {i} + setsum ?g (UNIV - {i})" by (rule setsum_Un_disjoint, auto)
also have "... = setsum ?g {i}"
proof -
have "setsum ?g (UNIV - {i}) = setsum (λk. 0) (UNIV - {i})" unfolding mat_def by auto
also have "... = 0" unfolding setsum_0 ..
finally show ?thesis by simp
qed
also have "... = A $ i $ j" unfolding mat_def by simp
finally show "(∑k∈UNIV. mat (1::'a) $ i $ k * A $ k $ j) = A $ i $ j" .
qed
lemma invertible_row_add:
assumes a_noteq_b: "a≠b"
shows "invertible (row_add (mat (1::'a::{ring_1})) a b q)"
proof (unfold invertible_def, rule exI[of _ "(row_add (mat 1) a b (-q))"], rule conjI)
show "row_add (mat (1::'a)) a b q ** row_add (mat (1::'a)) a b (- q) = mat (1::'a)" using a_noteq_b
proof (unfold matrix_matrix_mult_def, vector, clarify, unfold row_add_def, vector, unfold mat_1_fun, auto)
show " (∑k::'b∈UNIV. (if b = k then 1::'a else (0::'a)) * (if k = a then (0::'a) + - q * (1::'a) else if k = b then 1::'a else (0::'a))) = (1::'a)"
proof -
let ?f="λk. (if b = k then 1::'a else (0::'a)) * (if k = a then (0::'a) + - q * (1::'a) else if k = b then 1::'a else (0::'a))"
have univ_eq: "UNIV = ((UNIV - {b}) ∪ {b})" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV - {b}) ∪ {b}) " using univ_eq by simp
also have "... = setsum ?f (UNIV - {b}) + setsum ?f {b}" by (rule setsum_Un_disjoint, auto)
also have "... = 0 + setsum ?f {b}" by auto
also have "... = setsum ?f {b}" by simp
also have "... = 1" using a_noteq_b by simp
finally show ?thesis .
qed
show "(∑k::'b∈UNIV. ((if a = k then 1::'a else (0::'a)) + q * (if b = k then 1::'a else (0::'a))) * (if k = a then (1::'a) + -
q * (0::'a) else if k = a then 1::'a else (0::'a))) = (1::'a)"
proof -
let ?f="λk. ((if a = k then 1::'a else (0::'a)) + q * (if b = k then 1::'a else (0::'a))) * (if k = a then (1::'a) + -
q * (0::'a) else if k = a then 1::'a else (0::'a))"
have univ_eq: "UNIV = ((UNIV - {a}) ∪ {a})" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV - {a}) ∪ {a}) " using univ_eq by simp
also have "... = setsum ?f (UNIV - {a}) + setsum ?f {a}" by (rule setsum_Un_disjoint, auto)
also have "... = 0 + setsum ?f {a}" by auto
also have "... = setsum ?f {a}" by simp
also have "... = 1" using a_noteq_b by simp
finally show ?thesis .
qed
next
fix s
assume s_not_a: "s ≠ a"
show "(∑k::'b∈UNIV. (if s = k then 1::'a else (0::'a)) * (if k = a then (1::'a) + - q * (0::'a) else if k = a then 1::'a else (0::'a))) = (0::'a)"
by (rule setsum_0', auto simp add: s_not_a)
next
fix t
assume b_not_t: "b ≠ t" and a_not_t: "a ≠ t"
show "(∑k∈UNIV. (if t = k then 1::'a else (0::'a)) * (if k = a then (0::'a) + - q * (0::'a) else if k = t then 1::'a else (0::'a))) = (1::'a)"
proof -
let ?f="λk. (if t = k then 1::'a else (0::'a)) * (if k = a then (0::'a) + - q * (0::'a) else if k = t then 1::'a else (0::'a)) "
have univ_eq: "UNIV = ((UNIV - {t}) ∪ {t})" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV - {t}) ∪ {t}) " using univ_eq by simp
also have "... = setsum ?f (UNIV - {t}) + setsum ?f {t}" by (rule setsum_Un_disjoint, auto)
also have "... = 0 + setsum ?f {t}" by auto
also have "... = setsum ?f {t}" by simp
also have "... = 1" using b_not_t a_not_t by simp
finally show ?thesis .
qed
next
fix s t
assume b_not_t: "b ≠ t" and a_not_t: "a ≠ t" and s_not_t: "s ≠ t"
show " (∑k∈UNIV. (if s = a then (if a = k then 1::'a else (0::'a)) + q * (if b = k then 1::'a else (0::'a)) else if s = k then 1::'a else (0::'a)) *
(if k = a then (0::'a) + - q * (0::'a) else if k = t then 1::'a else (0::'a))) = (0::'a)" by (rule setsum_0', auto simp add: b_not_t a_not_t s_not_t)
next
fix s
assume s_not_b: "s≠b"
let ?f="λk. (if s = a then (if a = k then 1::'a else (0::'a)) + q * (if b = k then 1::'a else (0::'a)) else if s = k then 1::'a else (0::'a)) *
(if k = a then (0::'a) + - q * (1::'a) else if k = b then 1::'a else (0::'a))"
show "setsum ?f UNIV = (0::'a)"
proof (cases "s=a")
case False
show ?thesis by (rule setsum_0', auto simp add: False s_not_b a_noteq_b)
next
case True --"This case is different from the other cases"
have univ_eq: "UNIV = ((UNIV - {a}- {b}) ∪ ({b} ∪ {a}))" by auto
have setsum_a: "setsum ?f {a} = -q" unfolding True using s_not_b using a_noteq_b by auto
have setsum_b: "setsum ?f {b} = q" unfolding True using s_not_b using a_noteq_b by auto
have setsum_rest: "setsum ?f (UNIV - {a} - {b}) = 0" by (rule setsum_0', auto simp add: True s_not_b a_noteq_b)
have "setsum ?f UNIV = setsum ?f ((UNIV - {a}- {b}) ∪ ({b} ∪ {a}))" using univ_eq by simp
also have "... = setsum ?f (UNIV - {a} - {b}) + setsum ?f ({b} ∪ {a})" by (rule setsum_Un_disjoint, auto)
also have "... = setsum ?f (UNIV - {a} - {b}) + setsum ?f {b} + setsum ?f {a}" by (auto simp add: setsum_Un_disjoint a_noteq_b)
also have "... = 0" unfolding setsum_a setsum_b setsum_rest by simp
finally show ?thesis .
qed
qed
next
show "row_add (mat (1::'a)) a b (- q) ** row_add (mat (1::'a)) a b q = mat (1::'a)" using a_noteq_b
proof (unfold matrix_matrix_mult_def, vector, clarify, unfold row_add_def, vector, unfold mat_1_fun, auto)
show "(∑k∈UNIV. (if b = k then 1::'a else (0::'a)) * (if k = a then (0::'a) + q * (1::'a) else if k = b then 1::'a else (0::'a))) = (1::'a)"
proof -
let ?f="λk. (if b = k then 1::'a else (0::'a)) * (if k = a then (0::'a) + q * (1::'a) else if k = b then 1::'a else (0::'a))"
have univ_eq: "UNIV = ((UNIV - {b}) ∪ {b})" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV - {b}) ∪ {b}) " using univ_eq by simp
also have "... = setsum ?f (UNIV - {b}) + setsum ?f {b}" by (rule setsum_Un_disjoint, auto)
also have "... = 0 + setsum ?f {b}" by auto
also have "... = setsum ?f {b}" by simp
also have "... = 1" using a_noteq_b by simp
finally show ?thesis .
qed
next
show "(∑k∈UNIV. ((if a = k then 1::'a else (0::'a)) + - (q * (if b = k then 1::'a else (0::'a)))) * (if k = a then (1::'a)
+ q * (0::'a) else if k = a then 1::'a else (0::'a))) = (1::'a)"
proof -
let ?f="λk. ((if a = k then 1::'a else (0::'a)) + - (q * (if b = k then 1::'a else (0::'a)))) * (if k = a then (1::'a) + q * (0::'a) else if k = a then 1::'a else (0::'a))"
have univ_eq: "UNIV = ((UNIV - {a}) ∪ {a})" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV - {a}) ∪ {a}) " using univ_eq by simp
also have "... = setsum ?f (UNIV - {a}) + setsum ?f {a}" by (rule setsum_Un_disjoint, auto)
also have "... = 0 + setsum ?f {a}" by auto
also have "... = setsum ?f {a}" by simp
also have "... = 1" using a_noteq_b by simp
finally show ?thesis .
qed
next
fix s
assume s_not_a: "s≠a"
show "(∑k∈UNIV. (if s = k then 1::'a else (0::'a)) * (if k = a then (1::'a) + q * (0::'a) else if k = a then 1::'a else (0::'a))) = (0::'a)"
by (rule setsum_0', auto simp add: s_not_a)
next
fix t
assume b_not_t: "b ≠ t" and a_not_t: "a ≠ t"
show "(∑k∈UNIV. (if t = k then 1::'a else (0::'a)) * (if k = a then (0::'a) + q * (0::'a) else if k = t then 1::'a else (0::'a))) = (1::'a)"
proof -
let ?f="λk. (if t = k then 1::'a else (0::'a)) * (if k = a then (0::'a) + q * (0::'a) else if k = t then 1::'a else (0::'a))"
have univ_eq: "UNIV = ((UNIV - {t}) ∪ {t})" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV - {t}) ∪ {t}) " using univ_eq by simp
also have "... = setsum ?f (UNIV - {t}) + setsum ?f {t}" by (rule setsum_Un_disjoint, auto)
also have "... = 0 + setsum ?f {t}" by auto
also have "... = setsum ?f {t}" by simp
also have "... = 1" using b_not_t a_not_t by simp
finally show ?thesis .
qed
next
fix s t
assume b_not_t: "b ≠ t" and a_not_t: "a ≠ t" and s_not_t: "s ≠ t"
show "(∑k∈UNIV. (if s = a then (if a = k then 1::'a else (0::'a)) + - q * (if b = k then 1::'a else (0::'a)) else if s = k then 1::'a else (0::'a)) *
(if k = a then (0::'a) + q * (0::'a) else if k = t then 1::'a else (0::'a))) = (0::'a)"
by (rule setsum_0', auto simp add: b_not_t a_not_t s_not_t)
next
fix s
assume s_not_b: "s≠b"
let ?f="λk.(if s = a then (if a = k then 1::'a else (0::'a)) + - q * (if b = k then 1::'a else (0::'a)) else if s = k then 1::'a else (0::'a))
* (if k = a then (0::'a) + q * (1::'a) else if k = b then 1::'a else (0::'a))"
show "setsum ?f UNIV = 0"
proof (cases "s=a")
case False
show ?thesis by (rule setsum_0', auto simp add: False s_not_b a_noteq_b)
next
case True --"This case is different from the other cases"
have univ_eq: "UNIV = ((UNIV - {a}- {b}) ∪ ({b} ∪ {a}))" by auto
have setsum_a: "setsum ?f {a} = q" unfolding True using s_not_b using a_noteq_b by auto
have setsum_b: "setsum ?f {b} = -q" unfolding True using s_not_b using a_noteq_b by auto
have setsum_rest: "setsum ?f (UNIV - {a} - {b}) = 0" by (rule setsum_0', auto simp add: True s_not_b a_noteq_b)
have "setsum ?f UNIV = setsum ?f ((UNIV - {a}- {b}) ∪ ({b} ∪ {a}))" using univ_eq by simp
also have "... = setsum ?f (UNIV - {a} - {b}) + setsum ?f ({b} ∪ {a})" by (rule setsum_Un_disjoint, auto)
also have "... = setsum ?f (UNIV - {a} - {b}) + setsum ?f {b} + setsum ?f {a}" by (auto simp add: setsum_Un_disjoint a_noteq_b)
also have "... = 0" unfolding setsum_a setsum_b setsum_rest by simp
finally show ?thesis .
qed
qed
qed
text{*Properties about @{term "interchange_columns"}*}
lemma interchange_columns_mat_1: "A ** interchange_columns (mat 1) a b = interchange_columns A a b"
proof (unfold matrix_matrix_mult_def, unfold interchange_columns_def, vector, auto)
fix i
show "(∑k∈UNIV. A $ i $ k * mat (1::'a) $ k $ a) = A $ i $ a"
proof -
let ?f="(λk. A $ i $ k * mat (1::'a) $ k $ a)"
have univ_rw:"UNIV = (UNIV-{a}) ∪ {a}" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV-{a}) ∪ {a})" using univ_rw by auto
also have "... = setsum ?f (UNIV-{a}) + setsum ?f {a}" by (rule setsum_Un_disjoint, auto)
also have "... = setsum ?f {a}" unfolding mat_def by auto
finally show ?thesis unfolding mat_def by simp
qed
assume a_not_b: "a≠b"
show " (∑k∈UNIV. A $ i $ k * mat (1::'a) $ k $ b) = A $ i $ b"
proof -
let ?f="(λk. A $ i $ k * mat (1::'a) $ k $ b)"
have univ_rw:"UNIV = (UNIV-{b}) ∪ {b}" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV-{b}) ∪ {b})" using univ_rw by auto
also have "... = setsum ?f (UNIV-{b}) + setsum ?f {b}" by (rule setsum_Un_disjoint, auto)
also have "... = setsum ?f {b}" unfolding mat_def by auto
finally show ?thesis unfolding mat_def by simp
qed
next
fix i j
assume j_not_b: "j ≠ b" and j_not_a: "j ≠ a"
show "(∑k∈UNIV. A $ i $ k * mat (1::'a) $ k $ j) = A $ i $ j"
proof -
let ?f="(λk. A $ i $ k * mat (1::'a) $ k $ j)"
have univ_rw:"UNIV = (UNIV-{j}) ∪ {j}" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV-{j}) ∪ {j})" using univ_rw by auto
also have "... = setsum ?f (UNIV-{j}) + setsum ?f {j}" by (rule setsum_Un_disjoint, auto)
also have "... = setsum ?f {j}" unfolding mat_def using j_not_b j_not_a by auto
finally show ?thesis unfolding mat_def by simp
qed
qed
lemma invertible_interchange_columns: "invertible (interchange_columns (mat 1) a b)"
proof (unfold invertible_def, rule exI[of _ "interchange_columns (mat 1) a b"], simp, unfold matrix_matrix_mult_def, vector, clarify,
unfold interchange_columns_def, vector, unfold mat_1_fun, auto+)
show "(∑k∈UNIV. (if k = b then 1::'a else if k = b then 1::'a else if b = k then 1::'a else (0::'a)) * (if k = b then 1::'a else (0::'a))) = (1::'a)"
proof -
let ?f="(λk. (if k = b then 1::'a else if k = b then 1::'a else if b = k then 1::'a else (0::'a)) * (if k = b then 1::'a else (0::'a)))"
have univ_rw:"UNIV = (UNIV-{b}) ∪ {b}" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV-{b}) ∪ {b})" using univ_rw by auto
also have "... = setsum ?f (UNIV-{b}) + setsum ?f {b}" by (rule setsum_Un_disjoint, auto)
also have "... = setsum ?f {b}" by auto
finally show ?thesis by simp
qed
assume a_not_b: "a ≠ b"
show "(∑k∈UNIV. (if k = a then 0::'a else if k = b then 1::'a else if a = k then 1::'a else (0::'a)) * (if k = b then 1::'a else (0::'a))) = (1::'a)"
proof -
let ?f="λk. (if k = a then 0::'a else if k = b then 1::'a else if a = k then 1::'a else (0::'a)) * (if k = b then 1::'a else (0::'a))"
have univ_rw:"UNIV = (UNIV-{b}) ∪ {b}" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV-{b}) ∪ {b})" using univ_rw by auto
also have "... = setsum ?f (UNIV-{b}) + setsum ?f {b}" by (rule setsum_Un_disjoint, auto)
also have "... = setsum ?f {b}" using a_not_b by simp
finally show ?thesis using a_not_b by auto
qed
next
fix t
assume b_not_t: "b ≠ t"
show " (∑k∈UNIV. (if k = b then 1::'a else if k = b then 1::'a else if b = k then 1::'a else (0::'a)) * (if k = t then 1::'a else (0::'a))) = (0::'a)"
apply (rule setsum_0') using b_not_t by auto
assume b_not_a: "b ≠ a"
show "(∑k∈UNIV. (if k = a then 1::'a else if k = b then 0::'a else if b = k then 1::'a else (0::'a)) *
(if t = a then if k = b then 1::'a else (0::'a) else if t = b then if k = a then 1::'a else (0::'a) else if k = t then 1::'a else (0::'a))) =
(0::'a)" apply (rule setsum_0') using b_not_t by auto
next
fix t
assume a_not_b: "a ≠ b" and a_not_t: "a ≠ t"
show "(∑k∈UNIV. (if k = a then 0::'a else if k = b then 1::'a else if a = k then 1::'a else (0::'a)) *
(if t = b then if k = a then 1::'a else (0::'a) else if k = t then 1::'a else (0::'a))) = (0::'a)"
by (rule setsum_0', auto simp add: a_not_b a_not_t)
next
assume b_not_a: "b ≠ a"
show "(∑k∈UNIV. (if k = a then 1::'a else if k = b then 0::'a else if b = k then 1::'a else (0::'a)) * (if k = a then 1::'a else (0::'a))) = (1::'a)"
proof -
let ?f="λk. (if k = a then 1::'a else if k = b then 0::'a else if b = k then 1::'a else (0::'a)) * (if k = a then 1::'a else (0::'a))"
have univ_rw:"UNIV = (UNIV-{a}) ∪ {a}" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV-{a}) ∪ {a})" using univ_rw by auto
also have "... = setsum ?f (UNIV-{a}) + setsum ?f {a}" by (rule setsum_Un_disjoint, auto)
also have "... = setsum ?f {a}" using b_not_a by simp
finally show ?thesis using b_not_a by auto
qed
next
fix t
assume t_not_a: "t ≠ a" and t_not_b: "t ≠ b"
show "(∑k∈UNIV. (if k = a then 0::'a else if k = b then 0::'a else if t = k then 1::'a else (0::'a)) * (if k = t then 1::'a else (0::'a))) = (1::'a)"
proof -
let ?f="λk. (if k = a then 0::'a else if k = b then 0::'a else if t = k then 1::'a else (0::'a)) * (if k = t then 1::'a else (0::'a))"
have univ_rw:"UNIV = (UNIV-{t}) ∪ {t}" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV-{t}) ∪ {t})" using univ_rw by auto
also have "... = setsum ?f (UNIV-{t}) + setsum ?f {t}" by (rule setsum_Un_disjoint, auto)
also have "... = setsum ?f {t}" using t_not_a t_not_b by simp
also have "... = 1" using t_not_a t_not_b by simp
finally show ?thesis .
qed
next
fix s t
assume s_not_a: "s ≠ a" and s_not_b: "s ≠ b" and s_not_t: "s ≠ t"
show "(∑k∈UNIV. (if k = a then 0::'a else if k = b then 0::'a else if s = k then 1::'a else (0::'a)) *
(if t = a then if k = b then 1::'a else (0::'a) else if t = b then if k = a then 1::'a else (0::'a) else if k = t then 1::'a else (0::'a))) =
(0::'a)"
by (rule setsum_0', auto simp add: s_not_a s_not_b s_not_t)
qed
text{*Properties about @{term "mult_column"}*}
lemma mult_column_mat_1: "A ** mult_column (mat 1) a q = mult_column A a q"
proof (unfold matrix_matrix_mult_def, unfold mult_column_def, vector, auto)
fix i
show "(∑k∈UNIV. A $ i $ k * (mat (1::'a) $ k $ a * q)) = A $ i $ a * q"
proof -
let ?f="λk. A $ i $ k * (mat (1::'a) $ k $ a * q)"
have univ_rw:"UNIV = (UNIV-{a}) ∪ {a}" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV-{a}) ∪ {a})" using univ_rw by auto
also have "... = setsum ?f (UNIV-{a}) + setsum ?f {a}" by (rule setsum_Un_disjoint, auto)
also have "... = setsum ?f {a}" unfolding mat_def by auto
also have "... = A $ i $ a * q" unfolding mat_def by auto
finally show ?thesis .
qed
fix j
show "(∑k∈UNIV. A $ i $ k * mat (1::'a) $ k $ j) = A $ i $ j"
proof -
let ?f="λk. A $ i $ k * mat (1::'a) $ k $ j"
have univ_rw:"UNIV = (UNIV-{j}) ∪ {j}" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV-{j}) ∪ {j})" using univ_rw by auto
also have "... = setsum ?f (UNIV-{j}) + setsum ?f {j}" by (rule setsum_Un_disjoint, auto)
also have "... = setsum ?f {j}" unfolding mat_def by auto
also have "... = A $ i $ j" unfolding mat_def by auto
finally show ?thesis .
qed
qed
lemma invertible_mult_column:
assumes qk: "q*k=1" and kq: "k*q=1"
shows "invertible (mult_column (mat 1) a q)"
proof (unfold invertible_def, rule exI[of _ "mult_column (mat 1) a k"], rule conjI)
show "mult_column (mat 1) a q ** mult_column (mat 1) a k = mat 1"
proof (unfold matrix_matrix_mult_def, vector, clarify, unfold mult_column_def, vector, unfold mat_1_fun, auto)
fix t
show "(∑ka∈UNIV. (if ka = a then (if t = ka then 1::'a else (0::'a)) * q else if t = ka then 1::'a else (0::'a)) *
(if t = a then (if ka = t then 1::'a else (0::'a)) * k else if ka = t then 1::'a else (0::'a))) =
(1::'a)"
proof -
let ?f=" λka. (if ka = a then (if t = ka then 1::'a else (0::'a)) * q else if t = ka then 1::'a else (0::'a)) *
(if t = a then (if ka = t then 1::'a else (0::'a)) * k else if ka = t then 1::'a else (0::'a))"
have univ_rw:"UNIV = (UNIV-{t}) ∪ {t}" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV-{t}) ∪ {t})" using univ_rw by auto
also have "... = setsum ?f (UNIV-{t}) + setsum ?f {t}" by (rule setsum_Un_disjoint, auto)
also have "... = setsum ?f {t}" by auto
also have "... = 1" using qk by auto
finally show ?thesis .
qed
fix s
assume s_not_t: "s ≠ t"
show "(∑ka∈UNIV. (if ka = a then (if s = ka then 1::'a else (0::'a)) * q else if s = ka then 1::'a else (0::'a)) *
(if t = a then (if ka = t then 1::'a else (0::'a)) * k else if ka = t then 1::'a else (0::'a))) =
(0::'a)"
apply (rule setsum_0') using s_not_t by auto
qed
show "mult_column (mat (1::'a)) a k ** mult_column (mat (1::'a)) a q = mat (1::'a)"
proof (unfold matrix_matrix_mult_def, vector, clarify, unfold mult_column_def, vector, unfold mat_1_fun, auto)
fix t
show "(∑ka∈UNIV. (if ka = a then (if t = ka then 1::'a else (0::'a)) * k else if t = ka then 1::'a else (0::'a)) *
(if t = a then (if ka = t then 1::'a else (0::'a)) * q else if ka = t then 1::'a else (0::'a))) = (1::'a)"
proof -
let ?f=" λka. (if ka = a then (if t = ka then 1::'a else (0::'a)) * k else if t = ka then 1::'a else (0::'a)) *
(if t = a then (if ka = t then 1::'a else (0::'a)) * q else if ka = t then 1::'a else (0::'a))"
have univ_rw:"UNIV = (UNIV-{t}) ∪ {t}" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV-{t}) ∪ {t})" using univ_rw by auto
also have "... = setsum ?f (UNIV-{t}) + setsum ?f {t}" by (rule setsum_Un_disjoint, auto)
also have "... = setsum ?f {t}" by auto
also have "... = 1" using kq by auto
finally show ?thesis .
qed
fix s assume s_not_t: "s ≠ t"
show "(∑ka∈UNIV. (if ka = a then (if s = ka then 1::'a else (0::'a)) * k else if s = ka then 1::'a else (0::'a)) *
(if t = a then (if ka = t then 1::'a else (0::'a)) * q else if ka = t then 1::'a else (0::'a))) = 0"
apply (rule setsum_0') using s_not_t by auto
qed
qed
corollary invertible_mult_column':
assumes q_not_zero: "q ≠ 0"
shows "invertible (mult_column (mat (1::'a::{field})) a q)"
by (simp add: invertible_mult_column[of q "inverse q"] q_not_zero)
text{*Properties about @{term "column_add"}*}
lemma column_add_mat_1: "A ** column_add (mat 1) a b q = column_add A a b q"
proof (unfold matrix_matrix_mult_def,
unfold column_add_def, vector, auto)
fix i
let ?f="λk. A $ i $ k * (mat (1::'a) $ k $ a + mat (1::'a) $ k $ b * q)"
show "setsum ?f UNIV = A $ i $ a + A $ i $ b * q"
proof (cases "a=b")
case True
have univ_rw:"UNIV = (UNIV-{a}) ∪ {a}" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV-{a}) ∪ {a})" using univ_rw by auto
also have "... = setsum ?f (UNIV-{a}) + setsum ?f {a}" by (rule setsum_Un_disjoint, auto)
also have "... = setsum ?f {a}" unfolding mat_def True by auto
also have "... = ?f a" by auto
also have "... = A $ i $ a + A $ i $ b * q" using True unfolding mat_1_fun using distrib_left[of "A $ i $ b" 1 q] by auto
finally show ?thesis .
next
case False
have univ_rw: "UNIV = {a} ∪ ({b} ∪ (UNIV - {a} - {b}))" by auto
have setsum_rw: "setsum ?f ({b} ∪ (UNIV - {a} - {b})) = setsum ?f {b} + setsum ?f (UNIV - {a} - {b})" by (rule setsum_Un_disjoint, auto simp add: False)
have "setsum ?f UNIV = setsum ?f ({a} ∪ ({b} ∪ (UNIV - {a} - {b})))" using univ_rw by simp
also have "... = setsum ?f {a} + setsum ?f ({b} ∪ (UNIV - {a} - {b}))" by (rule setsum_Un_disjoint, auto simp add: False)
also have "... = setsum ?f {a} + setsum ?f {b} + setsum ?f (UNIV - {a} - {b})" unfolding setsum_rw ab_semigroup_add_class.add_ac(1)[symmetric] ..
also have "... = setsum ?f {a} + setsum ?f {b}" unfolding mat_def by auto
also have "... = A $ i $ a + A $ i $ b * q" using False unfolding mat_def by simp
finally show ?thesis .
qed
fix j
assume j_noteq_a: "j≠a"
show "(∑k∈UNIV. A $ i $ k * mat (1::'a) $ k $ j) = A $ i $ j"
proof -
let ?f="λk. A $ i $ k * mat (1::'a) $ k $ j"
have univ_rw:"UNIV = (UNIV-{j}) ∪ {j}" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV-{j}) ∪ {j})" using univ_rw by auto
also have "... = setsum ?f (UNIV-{j}) + setsum ?f {j}" by (rule setsum_Un_disjoint, auto)
also have "... = setsum ?f {j}" unfolding mat_def by auto
also have "... = A $ i $ j" unfolding mat_def by simp
finally show ?thesis .
qed
qed
lemma invertible_column_add:
assumes a_noteq_b: "a≠b"
shows "invertible (column_add (mat (1::'a::{ring_1})) a b q)"
proof (unfold invertible_def, rule exI[of _ "(column_add (mat 1) a b (-q))"], rule conjI)
show " column_add (mat (1::'a)) a b q ** column_add (mat (1::'a)) a b (- q) = mat (1::'a)" using a_noteq_b
proof (unfold matrix_matrix_mult_def, vector, clarify, unfold column_add_def, vector, unfold mat_1_fun, auto)
show " (∑k∈UNIV. (if k = a then (0::'a) + (1::'a) * q else if b = k then 1::'a else (0::'a)) * (if k = b then 1::'a else (0::'a))) = (1::'a)"
proof -
let ?f="λk. (if k = a then (0::'a) + (1::'a) * q else if b = k then 1::'a else (0::'a)) * (if k = b then 1::'a else (0::'a))"
have univ_rw:"UNIV = (UNIV-{b}) ∪ {b}" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV-{b}) ∪ {b})" using univ_rw by auto
also have "... = setsum ?f (UNIV-{b}) + setsum ?f {b}" by (rule setsum_Un_disjoint, auto)
also have "... = setsum ?f {b}" by auto
also have "... = 1" using a_noteq_b by simp
finally show ?thesis .
qed
show "(∑k∈UNIV. (if k = a then (1::'a) + (0::'a) * q else if a = k then 1::'a else (0::'a)) * ((if k = a then 1::'a else (0::'a)) + - ((if k = b then 1::'a else (0::'a)) * q))) =
(1::'a)"
proof -
let ?f="λk. (if k = a then (1::'a) + (0::'a) * q else if a = k then 1::'a else (0::'a)) * ((if k = a then 1::'a else (0::'a)) + - ((if k = b then 1::'a else (0::'a)) * q))"
have univ_rw:"UNIV = (UNIV-{a}) ∪ {a}" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV-{a}) ∪ {a})" using univ_rw by auto
also have "... = setsum ?f (UNIV-{a}) + setsum ?f {a}" by (rule setsum_Un_disjoint, auto)
also have "... = setsum ?f {a}" by auto
also have "... = 1" using a_noteq_b by simp
finally show ?thesis .
qed
fix i j
assume i_not_b: "i ≠ b" and i_not_a: "i ≠ a" and i_not_j: "i ≠ j"
show "(∑k∈UNIV. (if k = a then (0::'a) + (0::'a) * q else if i = k then 1::'a else (0::'a)) *
(if j = a then (if k = a then 1::'a else (0::'a)) + (if k = b then 1::'a else (0::'a)) * - q else if k = j then 1::'a else (0::'a))) = (0::'a)"
by (rule setsum_0', auto simp add: i_not_b i_not_a i_not_j)
next
fix j
assume a_not_j: "a≠j"
show " (∑k∈UNIV. (if k = a then (1::'a) + (0::'a) * q else if a = k then 1::'a else (0::'a)) * (if k = j then 1::'a else (0::'a))) = (0::'a)"
apply (rule setsum_0') using a_not_j a_noteq_b by auto
next
fix j
assume j_not_b: "j ≠ b" and j_not_a: "j ≠ a"
show " (∑k∈UNIV. (if k = a then (0::'a) + (0::'a) * q else if j = k then 1::'a else (0::'a)) * (if k = j then 1::'a else (0::'a))) = (1::'a)"
proof -
let ?f="λk. (if k = a then (0::'a) + (0::'a) * q else if j = k then 1::'a else (0::'a)) * (if k = j then 1::'a else (0::'a))"
have univ_rw:"UNIV = (UNIV-{j}) ∪ {j}" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV-{j}) ∪ {j})" using univ_rw by auto
also have "... = setsum ?f (UNIV-{j}) + setsum ?f {j}" by (rule setsum_Un_disjoint, auto)
also have "... = setsum ?f {j}" using j_not_b j_not_a by auto
also have "... = 1" using j_not_b j_not_a by auto
finally show ?thesis .
qed
next
fix j
assume b_not_j: "b ≠ j"
show "(∑k∈UNIV. (if k = a then 0 + 1 * q else if b = k then 1 else 0) *
(if j = a then (if k = a then 1 else 0) + (if k = b then 1 else 0) * - q else if k = j then 1 else 0)) = 0"
proof (cases "j=a")
case False
show ?thesis by (rule setsum_0', auto simp add: False b_not_j)
next
case True --"This case is different from the other cases"
let ?f="λk. (if k = a then 0 + 1 * q else if b = k then 1 else 0) *
(if j = a then (if k = a then 1 else 0) + (if k = b then 1 else 0) * - q else if k = j then 1 else 0)"
have univ_eq: "UNIV = ((UNIV - {a}- {b}) ∪ ({b} ∪ {a}))" by auto
have setsum_a: "setsum ?f {a} = q" unfolding True using b_not_j using a_noteq_b by auto
have setsum_b: "setsum ?f {b} = -q" unfolding True using b_not_j using a_noteq_b by auto
have setsum_rest: "setsum ?f (UNIV - {a} - {b}) = 0" by (rule setsum_0', auto simp add: True b_not_j a_noteq_b)
have "setsum ?f UNIV = setsum ?f ((UNIV - {a}- {b}) ∪ ({b} ∪ {a}))" using univ_eq by simp
also have "... = setsum ?f (UNIV - {a} - {b}) + setsum ?f ({b} ∪ {a})" by (rule setsum_Un_disjoint, auto)
also have "... = setsum ?f (UNIV - {a} - {b}) + setsum ?f {b} + setsum ?f {a}" by (auto simp add: setsum_Un_disjoint a_noteq_b)
also have "... = 0" unfolding setsum_a setsum_b setsum_rest by simp
finally show ?thesis .
qed
qed
next
show " column_add (mat (1::'a)) a b (- q) ** column_add (mat (1::'a)) a b q = mat (1::'a)" using a_noteq_b
proof (unfold matrix_matrix_mult_def, vector, clarify, unfold column_add_def, vector, unfold mat_1_fun, auto)
show "(∑k∈UNIV. (if k = a then (0::'a) + (1::'a) * - q else if b = k then 1::'a else (0::'a)) * (if k = b then 1::'a else (0::'a))) = (1::'a)"
proof -
let ?f="λk. (if k = a then (0::'a) + (1::'a) * - q else if b = k then 1::'a else (0::'a)) * (if k = b then 1::'a else (0::'a))"
have univ_rw:"UNIV = (UNIV-{b}) ∪ {b}" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV-{b}) ∪ {b})" using univ_rw by auto
also have "... = setsum ?f (UNIV-{b}) + setsum ?f {b}" by (rule setsum_Un_disjoint, auto)
also have "... = setsum ?f {b}" by auto
also have "... = 1" using a_noteq_b by auto
finally show ?thesis .
qed
next
show "(∑k∈UNIV. (if k = a then (1::'a) + (0::'a) * - q else if a = k then 1::'a else (0::'a)) * ((if k = a then 1::'a else (0::'a)) + (if k = b then 1::'a else (0::'a)) * q)) =
(1::'a)"
proof -
let ?f="λk. (if k = a then (1::'a) + (0::'a) * - q else if a = k then 1::'a else (0::'a)) * ((if k = a then 1::'a else (0::'a)) + (if k = b then 1::'a else (0::'a)) * q) "
have univ_rw:"UNIV = (UNIV-{a}) ∪ {a}" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV-{a}) ∪ {a})" using univ_rw by auto
also have "... = setsum ?f (UNIV-{a}) + setsum ?f {a}" by (rule setsum_Un_disjoint, auto)
also have "... = setsum ?f {a}" by auto
also have "... = 1" using a_noteq_b by auto
finally show ?thesis .
qed
next
fix j
assume a_not_j: "a ≠ j" show "(∑k∈UNIV. (if k = a then (1::'a) + (0::'a) * - q else if a = k then 1::'a else (0::'a)) * (if k = j then 1::'a else (0::'a))) = (0::'a)"
apply (rule setsum_0') using a_not_j by auto
next
fix j
assume j_not_b: "j ≠ b" and j_not_a: "j ≠ a"
show "(∑k∈UNIV. (if k = a then (0::'a) + (0::'a) * - q else if j = k then 1::'a else (0::'a)) * (if k = j then 1::'a else (0::'a))) = (1::'a)"
proof -
let ?f="λk.(if k = a then (0::'a) + (0::'a) * - q else if j = k then 1::'a else (0::'a)) * (if k = j then 1::'a else (0::'a))"
have univ_rw:"UNIV = (UNIV-{j}) ∪ {j}" by auto
have "setsum ?f UNIV = setsum ?f ((UNIV-{j}) ∪ {j})" using univ_rw by auto
also have "... = setsum ?f (UNIV-{j}) + setsum ?f {j}" by (rule setsum_Un_disjoint, auto)
also have "... = setsum ?f {j}" by auto
also have "... = 1" using a_noteq_b j_not_b j_not_a by auto
finally show ?thesis .
qed
next
fix i j
assume i_not_b: "i ≠ b" and i_not_a: "i ≠ a" and i_not_j: "i ≠ j"
show "(∑k∈UNIV. (if k = a then (0::'a) + (0::'a) * - q else if i = k then 1::'a else (0::'a)) *
(if j = a then (if k = a then 1::'a else (0::'a)) + (if k = b then 1::'a else (0::'a)) * q else if k = j then 1::'a else (0::'a))) = (0::'a)"
by (rule setsum_0', auto simp add: i_not_b i_not_a i_not_j)
next
fix j
assume b_not_j: "b ≠ j"
show "(∑k∈UNIV. (if k = a then (0::'a) + (1::'a) * - q else if b = k then 1::'a else (0::'a)) *
(if j = a then (if k = a then 1::'a else (0::'a)) + (if k = b then 1::'a else (0::'a)) * q else if k = j then 1::'a else (0::'a))) = 0"
proof (cases "j=a")
case False
show ?thesis by (rule setsum_0', auto simp add: False b_not_j)
next
case True --"This case is different from the other cases"
let ?f="λk. (if k = a then (0::'a) + (1::'a) * - q else if b = k then 1::'a else (0::'a)) *
(if j = a then (if k = a then 1::'a else (0::'a)) + (if k = b then 1::'a else (0::'a)) * q else if k = j then 1::'a else (0::'a))"
have univ_eq: "UNIV = ((UNIV - {a}- {b}) ∪ ({b} ∪ {a}))" by auto
have setsum_a: "setsum ?f {a} = -q" unfolding True using b_not_j using a_noteq_b by auto
have setsum_b: "setsum ?f {b} = q" unfolding True using b_not_j using a_noteq_b by auto
have setsum_rest: "setsum ?f (UNIV - {a} - {b}) = 0" by (rule setsum_0', auto simp add: True b_not_j a_noteq_b)
have "setsum ?f UNIV = setsum ?f ((UNIV - {a}- {b}) ∪ ({b} ∪ {a}))" using univ_eq by simp
also have "... = setsum ?f (UNIV - {a} - {b}) + setsum ?f ({b} ∪ {a})" by (rule setsum_Un_disjoint, auto)
also have "... = setsum ?f (UNIV - {a} - {b}) + setsum ?f {b} + setsum ?f {a}" by (auto simp add: setsum_Un_disjoint a_noteq_b)
also have "... = 0" unfolding setsum_a setsum_b setsum_rest by simp
finally show ?thesis .
qed
qed
qed
text{*Relationships between @{term "interchange_rows"} and @{term "interchange_columns"}*}
lemma interchange_rows_transpose:
shows "interchange_rows (transpose A) a b = transpose (interchange_columns A a b)"
unfolding interchange_rows_def interchange_columns_def transpose_def by vector
lemma interchange_rows_transpose':
shows "interchange_rows A a b = transpose (interchange_columns (transpose A) a b)"
unfolding interchange_rows_def interchange_columns_def transpose_def by vector
lemma interchange_columns_transpose:
shows "interchange_columns (transpose A) a b = transpose (interchange_rows A a b)"
unfolding interchange_rows_def interchange_columns_def transpose_def by vector
lemma interchange_columns_transpose':
shows "interchange_columns A a b = transpose (interchange_rows (transpose A) a b)"
unfolding interchange_rows_def interchange_columns_def transpose_def by vector
text{*Code equations for @{thm interchange_rows_def}, @{thm interchange_columns_def}, @{thm row_add_def}, @{thm column_add_def},
@{thm mult_row_def} and @{thm mult_column_def}:*}
definition interchange_rows_row
where "interchange_rows_row A a b i = vec_lambda (%j. if i = a then A $ b $ j else if i = b then A $ a $ j else A $ i $ j)"
lemma interchange_rows_code [code abstract]:
"vec_nth (interchange_rows_row A a b i) = (%j. if i = a then A $ b $ j else if i = b then A $ a $ j else A $ i $ j)"
unfolding interchange_rows_row_def by auto
lemma interchange_rows_code_nth [code abstract]: "vec_nth (interchange_rows A a b) = interchange_rows_row A a b"
unfolding interchange_rows_def unfolding interchange_rows_row_def[abs_def]
by auto
definition interchange_columns_row
where "interchange_columns_row A n m i = vec_lambda (%j. if j = n then A $ i $ m else if j = m then A $ i $ n else A $ i $ j)"
lemma interchange_columns_code [code abstract]:
"vec_nth (interchange_columns_row A n m i) = (%j. if j = n then A $ i $ m else if j = m then A $ i $ n else A $ i $ j)"
unfolding interchange_columns_row_def by auto
lemma interchange_columns_code_nth [code abstract]: "vec_nth (interchange_columns A a b) = interchange_columns_row A a b"
unfolding interchange_columns_def unfolding interchange_columns_row_def[abs_def]
by auto
definition row_add_row
where "row_add_row A a b q i = vec_lambda (%j. if i = a then A $ a $ j + q * A $ b $ j else A $ i $ j)"
lemma row_add_code [code abstract]:
"vec_nth (row_add_row A a b q i) = (%j. if i = a then A $ a $ j + q * A $ b $ j else A $ i $ j)"
unfolding row_add_row_def by auto
lemma row_add_code_nth [code abstract]: "vec_nth (row_add A a b q) = row_add_row A a b q"
unfolding row_add_def unfolding row_add_row_def[abs_def]
by auto
definition column_add_row
where "column_add_row A n m q i = vec_lambda (%j. if j = n then A $ i $ n + A $ i $ m * q else A $ i $ j)"
lemma column_add_code [code abstract]:
"vec_nth (column_add_row A n m q i) = (%j. if j = n then A $ i $ n + A $ i $ m * q else A $ i $ j)"
unfolding column_add_row_def by auto
lemma column_add_code_nth [code abstract]: "vec_nth (column_add A a b q) = column_add_row A a b q"
unfolding column_add_def unfolding column_add_row_def[abs_def]
by auto
definition mult_row_row
where "mult_row_row A a q i = vec_lambda (%j. if i = a then q * A $ a $ j else A $ i $ j)"
lemma mult_row_code [code abstract]:
"vec_nth (mult_row_row A a q i) = (%j. if i = a then q * A $ a $ j else A $ i $ j)"
unfolding mult_row_row_def by auto
lemma mult_row_code_nth [code abstract]: "vec_nth (mult_row A a q) = mult_row_row A a q"
unfolding mult_row_def unfolding mult_row_row_def[abs_def]
by auto
definition mult_column_row
where "mult_column_row A n q i = vec_lambda (%j. if j = n then A $ i $ j * q else A $ i $ j)"
lemma mult_column_code [code abstract]:
"vec_nth (mult_column_row A n q i) = (%j. if j = n then A $ i $ j * q else A $ i $ j)"
unfolding mult_column_row_def by auto
lemma mult_column_code_nth [code abstract]: "vec_nth (mult_column A a q) = mult_column_row A a q"
unfolding mult_column_def unfolding mult_column_row_def[abs_def]
by auto
text{*Definitions of row space, column space and rank*}
definition col_space :: "'a::{real_vector}^'n^'m=>('a^'m) set"
where "col_space A = span (columns A)"
definition row_space :: "'a::{real_vector}^'n^'m=>('a^'n) set"
where "row_space A = span (rows A)"
definition row_rank :: "'a::{real_vector}^'n^'m=>nat"
where "row_rank A = dim (row_space A)"
definition col_rank :: "'a::{real_vector}^'n^'m=>nat"
where "col_rank A = dim (col_space A)"
definition rank :: "real^'n^'m=>nat"
where "rank A = row_rank A"
lemma matrix_vmult_column_sum:
fixes A::"real^'n^'m"
shows "∃f. A *v x = setsum (λy. f y *⇩R y) (columns A)"
proof (rule exI[of _ "λy. setsum (λi. x $ i) {i. y = column i A}"])
let ?f="λy. setsum (λi. x $ i) {i. y = column i A}"
let ?g="(λy. {i. y=column i (A)})"
have inj: "inj_on ?g (columns (A))" unfolding inj_on_def unfolding columns_def by auto
have union_univ: "\<Union> (?g`(columns (A))) = UNIV" unfolding columns_def by auto
have " A *v x = (∑i∈UNIV. x $ i *s column i A)" unfolding matrix_mult_vsum ..
also have "... = setsum (λi. x $ i *s column i A) (\<Union>(?g`(columns A)))" unfolding union_univ ..
also have "... = setsum (setsum ((λi. x $ i *s column i A))) (?g`(columns A))" by (rule setsum_Union_disjoint, auto)
also have "... = setsum ((setsum ((λi. x $ i *s column i A))) o ?g) (columns A)" by (rule setsum_reindex, simp add: inj)
also have "... = setsum (λy. ?f y *⇩R y) (columns A)"
proof (rule setsum_cong2, unfold o_def)
fix xa
have "setsum (λi. x $ i *s column i A) {i. xa = column i A} = setsum (λi. x $ i *s xa) {i. xa = column i A}" by simp
also have "... = setsum (λi. x $ i *⇩R xa) {i. xa = column i A}" unfolding scalar_mult_eq_scaleR ..
also have "... = setsum (λi. x $ i) {i. xa = column i A} *⇩R xa" using scaleR_setsum_left[of "(λi. x $ i)" "{i. xa = column i A}" xa] ..
finally show "(∑i | xa = column i A. x $ i *s column i A) = (∑i | xa = column i A. x $ i) *⇩R xa" .
qed
finally show "A *v x = (∑y∈columns A. (∑i | y = column i A. x $ i) *⇩R y)" .
qed
lemma row_space_eq_col_space_transpose:
fixes A::"'a::{real_vector, semiring_1}^'columns^'rows"
shows "row_space A = col_space (transpose A)"
unfolding col_space_def row_space_def columns_transpose[of A] ..
lemma col_space_eq:
fixes A::"real^'m^'n"
shows "col_space A = Dim_Formula.col_space A"
proof (unfold col_space_def col_space_eq span_explicit, rule)
show "{y. ∃x. A *v x = y} ⊆ {y. ∃S u. finite S ∧ S ⊆ columns A ∧ (∑v∈S. u v *⇩R v) = y}"
proof (rule)
fix y assume y: "y ∈ {y. ∃x. A *v x = y}"
obtain x where x:"A *v x = y" using y by blast
obtain f where setsum: "A *v x = setsum (λy. f y *⇩R y) (columns A)" using matrix_vmult_column_sum by auto
have finite_cols: "finite (columns A)"
proof -
def f=="λi. column i A"
show ?thesis unfolding columns_def using finite_Atleast_Atmost_nat[of f] unfolding f_def by simp
qed
show "y ∈ {y. ∃S u. finite S ∧ S ⊆ columns A ∧ (∑v∈S. u v *⇩R v) = y}"
by (rule, rule exI[of _ "columns A"], auto, rule finite_cols, rule exI[of _ "f"], metis x setsum)
qed
next
show "{y. ∃S u. finite S ∧ S ⊆ columns A ∧ (∑v∈S. u v *⇩R v) = y} ⊆ {y. ∃x. A *v x = y}"
proof (rule, auto)
fix S and u::"(real, 'n) vec => real"
assume finite_S: "finite S" and S_in_cols: "S ⊆ columns A"
let ?f="λx. if x ∈ S then u x else 0"
let ?x ="(χ i. if column i A ∈ S then (inverse (real (card {a. column i A=column a A}))) * u (column i A) else 0)"
show "∃x. A *v x = (∑v∈S. u v *⇩R v)"
proof (unfold matrix_mult_vsum, rule exI[of _ "?x"], simp)
let ?g="λy. {i. y=column i A}"
have inj: "inj_on ?g (columns A)" unfolding inj_on_def unfolding columns_def by auto
have union_univ: "\<Union>(?g`(columns A)) = UNIV" unfolding columns_def by auto
have "setsum (λi.(if column i A ∈ S then inverse (real (card {a. column i A = column a A})) * u (column i A) else 0) *s column i A) UNIV
= setsum (λi.(if column i A ∈ S then inverse (real (card {a. column i A = column a A})) * u (column i A) else 0) *s column i A) (\<Union>(?g`(columns A)))"
unfolding union_univ ..
also have "... = setsum (setsum (λi.(if column i A ∈ S then inverse (real (card {a. column i A = column a A})) * u (column i A) else 0) *s column i A)) (?g`(columns A))"
by (rule setsum_Union_disjoint, auto)
also have "... = setsum ((setsum (λi.(if column i A ∈ S then inverse (real (card {a. column i A = column a A})) * u (column i A) else 0) *s column i A)) o ?g)
(columns A)" by (rule setsum_reindex, simp add: inj)
also have "... = setsum (λy. ?f y *⇩R y) (columns A)"
proof (rule setsum_cong2, auto)
fix x
assume x_in_cols: "x ∈ columns A" and x_notin_S: "x ∉ S"
show "(∑i | x = column i A. (if column i A ∈ S then (inverse (real (card {a. column i A = column a A}))) * u (column i A) else 0) *s column i A) = 0"
apply (rule setsum_0') using x_notin_S by auto
next
fix x
assume x_in_cols: "x ∈ columns A" and x_in_S: "x ∈ S"
have "setsum (λi. (if column i A ∈ S then (inverse (real (card {a. column i A = column a A}))) * u (column i A) else 0) *s column i A) {i. x = column i A} =
setsum (λi. (inverse (real (card {a. column i A = column a A}))) * u (column i A) *s column i A) {i. x = column i A}" apply (rule setsum_cong2) using x_in_S by simp
also have "... = setsum (λi. (inverse (real (card {a. x = column a A}))) * u x *s x) {i. x = column i A}" by auto
also have "... = of_nat (card {i. x = column i A}) * (inverse (real (card {a. x = column a A})) * u x *s x)" unfolding setsum_constant ..
also have "... = of_nat (card {i. x = column i A}) * (inverse (real (card {a. x = column a A})) *s (u x *s x))"
unfolding vector_smult_assoc [of "inverse (real (card {a. x = column a A}))" " u x" x , symmetric] ..
also have "... = real (card {i. x = column i A}) *⇩R (inverse (real (card {a. x = column a A})) *s (u x *s x))"
by (auto, metis real_of_nat_def setsum_constant setsum_constant_scaleR)
also have "... = real (card {i. x = column i A}) *s (inverse (real (card {a. x = column a A})) *s (u x *s x))" unfolding scalar_mult_eq_scaleR ..
also have "... = (real (card {i. x = column i A}) * inverse (real (card {a. x = column a A}))) *s (u x *s x)" unfolding vector_smult_assoc by auto
also have "... = 1 *s (u x *s x)" apply (auto, rule right_inverse) using x_in_cols unfolding columns_def by auto
also have "... = u x *s x" by auto
also have "... = u x *⇩R x" unfolding scalar_mult_eq_scaleR ..
finally show " (∑i | x = column i A. (if column i A ∈ S then inverse (real (card {a. column i A = column a A})) * u (column i A) else 0) *s column i A) = u x *⇩R x" .
qed
also have "... = setsum (λy. ?f y *⇩R y) (S ∪ ((columns A) - S))" apply (rule setsum_cong) using S_in_cols by auto
also have "... = setsum (λy. ?f y *⇩R y) S + setsum (λy. ?f y *⇩R y) ((columns A) - S)" apply (rule setsum_Un_disjoint) using S_in_cols finite_S finite_columns by auto
also have "... = setsum (λy. ?f y *⇩R y) S" by simp
finally show "(∑i∈UNIV. (if column i A ∈ S then inverse (real (card {a. column i A = column a A})) * u (column i A) else 0) *s column i A) = (∑v∈S. u v *⇩R v)" by auto
qed
qed
qed
lemma matrix_vector_zero: "A *v 0 = 0"
unfolding matrix_vector_mult_def by (simp add: zero_vec_def)
lemma vector_matrix_zero: "0 v* A = 0"
unfolding vector_matrix_mult_def by (simp add: zero_vec_def)
lemma vector_matrix_zero': "x v* 0 = 0"
unfolding vector_matrix_mult_def by (simp add: zero_vec_def)
lemma transpose_vector: "x v* A = transpose A *v x"
by (unfold matrix_vector_mult_def vector_matrix_mult_def transpose_def, auto)
lemma norm_mult_vec:
fixes a::"(real,'b::finite) vec"
shows "norm (x • x)=norm x * norm x"
by (metis inner_real_def norm_cauchy_schwarz_eq norm_mult)
lemma norm_equivalence:
fixes A::"real^'n^'m"
shows "((transpose A) *v (A *v x) = 0) <-> (A *v x = 0)"
proof (auto)
show "transpose A *v 0 = 0" unfolding matrix_vector_zero ..
next
assume a: "transpose A *v (A *v x) = 0"
have eq: "(x v* (transpose A)) = (A *v x)"
by (metis Cartesian_Euclidean_Space.transpose_transpose transpose_vector)
have eq_0: "0 = (x v* (transpose A)) * (A *v x)"
by (metis a comm_semiring_1_class.normalizing_semiring_rules(7) dot_lmul_matrix inner_eq_zero_iff inner_zero_left mult_zero_left transpose_vector)
hence "0 = norm ((x v* (transpose A)) * (A *v x))" by auto
also have "... = norm ((A *v x)*(A *v x))" unfolding eq ..
also have "... = norm ((A *v x) • (A *v x))"
by (metis eq_0 a dot_lmul_matrix eq inner_zero_right norm_zero)
also have "... = norm (A *v x)^2" unfolding norm_mult_vec[of "(A *v x)"] power2_eq_square ..
finally show "A *v x = 0"
by (metis (lifting) field_power_not_zero norm_eq_0_imp)
qed
lemma combination_columns:
fixes A::"real^'n^'m"
assumes x: "x ∈ columns (transpose A ** A)"
shows "∃f. (∑y∈columns(transpose A). f y *⇩R y) = x"
proof -
obtain j where j: "x= column j (transpose A ** A)" using x unfolding columns_def by auto
let ?g="(λy. {i. y=column i (transpose A)})"
have inj: "inj_on ?g (columns (transpose A))" unfolding inj_on_def unfolding columns_def by auto
have union_univ: "\<Union> (?g`(columns (transpose A))) = UNIV" unfolding columns_def by auto
let ?f="(λy. card {a. y = column a (transpose A)} * A $ (SOME a. y = column a (transpose A)) $ j)"
have "column j (transpose A ** A) = (∑i∈UNIV. (A$i$j) *⇩R (column i (transpose A)))"
unfolding matrix_matrix_mult_def unfolding column_def by (vector, auto, rule setsum_cong2, auto)
also have "... = setsum (λi. (A$i$j) *⇩R (column i (transpose A))) (\<Union>(?g`(columns (transpose A))))" unfolding union_univ ..
also have "... = setsum (setsum (λi. (A$i$j) *⇩R (column i (transpose A)))) (?g`(columns (transpose A)))" by (rule setsum_Union_disjoint, auto)
also have "... = setsum ((setsum (λi. (A$i$j) *⇩R (column i (transpose A)))) o ?g) (columns (transpose A))" apply (rule setsum_reindex) using inj by auto
also have "... = setsum (λy. ?f y *⇩R y) (columns (transpose A))"
proof (rule setsum_cong2, unfold o_def)
fix x assume x: "x ∈ columns (transpose A)"
obtain b where xb: "x = column b (transpose A)" using x unfolding columns_def by auto
have "∀a c. a∈ {i. x = column i (transpose A)} ∧ c∈ {i. x = column i (transpose A)} --> A $ a $ j = A $ c $ j"
by (unfold column_def transpose_def, auto, metis vec_lambda_inverse vec_nth)
hence rw_b: "∀a. a∈ {i. x = column i (transpose A)} --> A $ a $ j = A $ b $ j" using xb by fast
have Abj: "A $ b $ j = A $ (SOME a. x = column a (Cartesian_Euclidean_Space.transpose A)) $ j"
by (metis (lifting, mono_tags) xb mem_Collect_eq rw_b some_eq_ex)
have "(∑i | x = column i (Cartesian_Euclidean_Space.transpose A). A $ i $ j *⇩R column i (Cartesian_Euclidean_Space.transpose A))
= setsum (λi. A $ i $ j *⇩R x) {i. x = column i (transpose A)}" by auto
also have "... = (∑i∈{i. x = column i (transpose A)}. A $ b $ j *⇩R x)" using rw_b by auto
also have "... = of_nat (card {i. x = column i (transpose A)}) * (A $ b $ j *⇩R x)" unfolding setsum_constant by auto
also have "... = (real (card {i. x = column i (transpose A)})) *⇩R (A $ b $ j *⇩R x)"
by (metis (no_types) real_of_nat_def setsum_constant setsum_constant_scaleR)
also have "... = (real (card {a. x = column a (transpose A)}) * A $ b $ j) *⇩R x" by auto
also have "... = (real (card {a. x = column a (transpose A)}) * A $ (SOME a. x = column a (Cartesian_Euclidean_Space.transpose A)) $ j) *⇩R x"
unfolding Abj ..
finally show "(∑i | x = column i (Cartesian_Euclidean_Space.transpose A). A $ i $ j *⇩R column i (Cartesian_Euclidean_Space.transpose A)) =
(real (card {a. x = column a (Cartesian_Euclidean_Space.transpose A)}) * A $ (SOME a. x = column a (Cartesian_Euclidean_Space.transpose A)) $ j) *⇩R x" .
qed
finally show ?thesis unfolding j by auto
qed
lemma rrk_crk:
fixes A::"real^'n^'m"
shows "col_rank A ≤ row_rank A"
proof -
have null_space_eq: "null_space A = null_space (transpose A ** A)" using norm_equivalence unfolding matrix_vector_mul_assoc unfolding null_space_def by fastforce
have col_rank_transpose: "col_rank A = col_rank (transpose A ** A)"
using rank_nullity_theorem_matrices[of A] rank_nullity_theorem_matrices[of "(transpose A ** A)"]
unfolding col_space_eq[symmetric]
unfolding null_space_eq by (metis col_rank_def nat_add_left_cancel)
have "col_rank (transpose A ** A) ≤ col_rank (transpose A)"
proof (unfold col_rank_def, rule subset_le_dim, unfold col_space_def, unfold span_span, clarify)
fix x assume x_in: "x ∈ span (columns (transpose A ** A))"
show "x ∈ span (columns (transpose A))"
proof (rule span_induct)
show "x ∈ span (columns (transpose A ** A))" using x_in .
show "subspace (span (columns (transpose A)))" using subspace_span .
fix y assume y: "y ∈ columns (transpose A ** A)"
show "y ∈ span (columns (transpose A))"
proof (unfold span_explicit, simp, rule exI[of _ "columns (transpose A)"], auto intro: combination_columns[OF y])
show "finite (columns (transpose A))" unfolding columns_def using finite_Atleast_Atmost_nat by auto
qed
qed
qed
thus ?thesis
unfolding col_rank_transpose[symmetric]
unfolding col_rank_def col_space_def columns_transpose row_rank_def row_space_def .
qed
corollary row_rank_eq_col_rank:
fixes A::"real^'n^'m"
shows "row_rank A = col_rank A"
using rrk_crk[of A] using rrk_crk[of "transpose A"]
unfolding col_rank_def row_rank_def row_space_def col_space_def
unfolding rows_transpose columns_transpose by simp
theorem rank_col_rank:
shows "rank A = col_rank A" unfolding rank_def row_rank_eq_col_rank ..
theorem rank_eq_dim_image:
"rank A = dim (range (λx. A *v (x::real^'n)))"
by (metis Dim_Formula.col_space_def col_rank_def col_space_eq rank_col_rank)
theorem rank_eq_dim_col_space:
"rank A = dim (col_space A)" using rank_col_rank unfolding col_rank_def .
text{*Following definition and lemmas are obtained from AFP: \url{http://afp.sourceforge.net/browser_info/current/HOL/Tarskis_Geometry/Linear_Algebra2.html}*}
definition
is_basis :: "(real^('n::finite)) set => bool" where
"is_basis S ≡ independent S ∧ span S = UNIV"
lemma card_finite:
assumes "card S = CARD('n::finite)"
shows "finite S"
proof -
from `card S = CARD('n)` have "card S ≠ 0" by simp
with card_eq_0_iff [of S] show "finite S" by simp
qed
lemma independent_is_basis:
fixes B :: "(real^('n::finite)) set"
shows "independent B ∧ card B = CARD('n) <-> is_basis B"
proof
assume "independent B ∧ card B = CARD('n)"
hence "independent B" and "card B = CARD('n)" by simp+
from card_finite [of B, where 'n = 'n] and `card B = CARD('n)`
have "finite B" by simp
from `card B = CARD('n)`
have "card B = dim (UNIV :: ((real^'n) set))"
by (simp add: dim_UNIV)
with card_eq_dim [of B UNIV] and `finite B` and `independent B`
have "span B = UNIV" by auto
with `independent B` show "is_basis B" unfolding is_basis_def ..
next
assume "is_basis B"
hence "independent B" unfolding is_basis_def ..
moreover have "card B = CARD('n)"
proof -
have "B ⊆ UNIV" by simp
moreover
{ from `is_basis B` have "UNIV ⊆ span B" and "independent B"
unfolding is_basis_def
by simp+ }
ultimately have "card B = dim (UNIV::((real^'n) set))"
using basis_card_eq_dim [of B UNIV]
by simp
then show "card B = CARD('n)" by (simp add: dim_UNIV)
qed
ultimately show "independent B ∧ card B = CARD('n)" ..
qed
lemma basis_finite:
fixes B :: "(real^('n::finite)) set"
assumes "is_basis B"
shows "finite B"
proof -
from independent_is_basis [of B] and `is_basis B` have "card B = CARD('n)"
by simp
with card_finite [of B, where 'n = 'n] show "finite B" by simp
qed
text{*Here ends the facts obtained from AFP: \url{http://afp.sourceforge.net/browser_info/current/HOL/Tarskis_Geometry/Linear_Algebra2.html}*}
text{*Invertible linear maps*}
text{*We could dispense the property @{term "linear g"} using @{thm "left_inverse_linear"}*}
definition invertible_lf ::"('a::euclidean_space => 'a::euclidean_space) => bool"
where "invertible_lf f = (linear f ∧ (∃g. linear g ∧ (g o f = id) ∧ (f o g = id)))"
lemma invertible_lf_intro[intro]:
assumes "linear f" and "(g o f = id)" and "(f o g = id)"
shows "invertible_lf f"
by (metis assms(1) assms(2) invertible_lf_def left_inverse_linear linear_inverse_left)
lemma invertible_imp_bijective:
assumes "invertible_lf f"
shows "bij f"
by (metis assms bij_betw_comp_iff bij_betw_imp_surj invertible_lf_def inj_on_imageI2 inj_on_imp_bij_betw inv_id surj_id surj_imp_inj_inv)
lemma invertible_matrix_imp_invertible_lf:
fixes A::"real^'n^'n"
assumes invertible_A: "invertible A"
shows "invertible_lf (λx. A *v x)"
proof -
obtain B where AB: "A**B=mat 1" and BA: "B**A=mat 1" using invertible_A unfolding invertible_def by blast
show ?thesis
proof (rule invertible_lf_intro [of _ "(λx. B *v x)"])
show l: "linear (op *v A)" using matrix_vector_mul_linear .
show id1: "op *v B o op *v A = id" by (metis (lifting) AB BA isomorphism_expand matrix_vector_mul_assoc matrix_vector_mul_lid)
show "op *v A o op *v B = id" by (metis l id1 left_inverse_linear linear_inverse_left)
qed
qed
lemma invertible_lf_imp_invertible_matrix:
fixes f::"real^'n=>real^'n"
assumes invertible_f: "invertible_lf f"
shows "invertible (matrix f)"
proof -
obtain g where linear_g: "linear g" and gf: "(g o f = id)" and fg: "(f o g = id)" using invertible_f unfolding invertible_lf_def by auto
show ?thesis proof (unfold invertible_def, rule exI[of _ "matrix g"], rule conjI)
show " matrix f ** matrix g = mat 1"
by (metis (no_types) fg id_def left_inverse_linear linear_g linear_id matrix_compose matrix_eq matrix_mul_rid matrix_vector_mul matrix_vector_mul_assoc)
show "matrix g ** matrix f = mat 1"
by (metis `matrix f ** matrix g = mat 1` matrix_left_right_inverse)
qed
qed
lemma invertible_matrix_iff_invertible_lf:
fixes A::"real^'n^'n"
shows "invertible A <-> invertible_lf (λx. A *v x)"
by (metis invertible_lf_imp_invertible_matrix invertible_matrix_imp_invertible_lf matrix_of_matrix_vector_mul)
lemma invertible_matrix_iff_invertible_lf':
fixes f::"real^'n=>real^'n"
assumes linear_f: "linear f"
shows "invertible (matrix f) <-> invertible_lf f"
by (metis (lifting) assms invertible_matrix_iff_invertible_lf matrix_vector_mul)
lemma invertible_matrix_mult_right_rank:
fixes A::"real^'n^'m" and Q::"real^'n^'n"
assumes invertible_Q: "invertible Q"
shows "rank (A**Q) = rank A"
proof -
def TQ=="(λx. Q *v x)"
def TA≡"(λx. A *v x)"
def TAQ=="(λx. (A**Q) *v x)"
have "invertible_lf TQ" using invertible_matrix_imp_invertible_lf[OF invertible_Q] unfolding TQ_def .
hence bij_TQ: "bij TQ" using invertible_imp_bijective by auto
have "range TAQ = range (TA o TQ)" unfolding TQ_def TA_def TAQ_def o_def matrix_vector_mul_assoc ..
also have "... = TA `(range TQ)" unfolding image_compose ..
also have "... = TA ` (UNIV)" using bij_is_surj[OF bij_TQ] by simp
finally have "range TAQ = range TA" .
thus ?thesis unfolding rank_eq_dim_image TAQ_def TA_def by simp
qed
lemma subspace_image_invertible_mat:
fixes P::"real^'m^'m"
assumes inv_P: "invertible P"
and sub_W: "subspace W"
shows "subspace ((λx. P *v x)` W)"
by (metis (lifting) matrix_vector_mul_linear sub_W subspace_linear_image)
lemma dim_image_invertible_mat:
fixes P::"real^'m^'m"
assumes inv_P: "invertible P"
and sub_W: "subspace W"
shows "dim ((λx. P *v x)` W) = dim W"
proof -
obtain B where B_in_W: "B⊆W" and ind_B: "independent B" and W_in_span_B: " W ⊆ span B" and card_B_eq_dim_W: "card B = dim W"
using basis_exists by blast
def L≡"(λx. P *v x)"
def C≡"L`B"
have finite_B: "finite B" using indep_card_eq_dim_span[OF ind_B] by simp
have linear_L: "linear L" using matrix_vector_mul_linear unfolding L_def .
have finite_C: "finite C" using indep_card_eq_dim_span[OF ind_B] unfolding C_def by simp
have inv_TP: "invertible_lf (λx. P *v x)" using invertible_matrix_imp_invertible_lf[OF inv_P] .
have inj_on_LW: "inj_on L W" using invertible_imp_bijective[OF inv_TP] unfolding bij_def L_def unfolding inj_on_def
by blast
hence inj_on_LB: "inj_on L B" unfolding inj_on_def using B_in_W by auto
have ind_D: "independent C"
proof (rule independent_if_scalars_zero[OF finite_C], clarify)
fix f x
assume setsum: "(∑x∈C. f x *⇩R x) = 0" and x: "x ∈ C"
obtain y where Ly_eq_x: "L y = x" and y: "y ∈ B" using x unfolding C_def L_def by auto
have "(∑x∈C. f x *⇩R x) = setsum ((λx. f x *⇩R x) o L) B" unfolding C_def by (rule setsum_reindex[OF inj_on_LB])
also have "... = setsum (λx. f (L x) *⇩R L x) B" unfolding o_def ..
also have "... = setsum (λx. ((f o L) x) *⇩R L x) B" using o_def by auto
also have "... = L (setsum (λx. ((f o L) x) *⇩R x) B)" by (rule linear_setsum_mul[OF linear_L finite_B,symmetric])
finally have rw: " (∑x∈C. f x *⇩R x) = L (∑x∈B. (f o L) x *⇩R x)" .
have "(∑x∈B. (f o L) x *⇩R x) ∈ W" by (rule subspace_setsum[OF sub_W finite_B], auto simp add: B_in_W set_rev_mp sub_W subspace_mul)
hence "(∑x∈B. (f o L) x *⇩R x)=0" using setsum rw using linear_injective_on_subspace_0[OF linear_L sub_W] using inj_on_LW by auto
hence "(f o L) y = 0" using scalars_zero_if_independent[OF finite_B ind_B, of "(f o L)"] using y by auto
thus "f x = 0" unfolding o_def Ly_eq_x .
qed
have "L` W ⊆ span C"
proof (unfold span_finite[OF finite_C], clarify)
fix xa assume xa_in_W: "xa ∈ W"
obtain g where setsum_g: "setsum (λx. g x *⇩R x) B = xa" using span_finite[OF finite_B] W_in_span_B xa_in_W by blast
show "∃u. (∑v∈C. u v *⇩R v) = L xa"
proof (rule exI[of _ "λx. g (THE y. y ∈ B ∧ x=L y)"])
have "L xa = L (setsum (λx. g x *⇩R x) B)" using setsum_g by simp
also have "... = setsum (λx. g x *⇩R L x) B" using linear_setsum_mul[OF linear_L finite_B] .
also have "... = setsum (λx. g (THE y. y ∈ B ∧ x=L y) *⇩R x) (L`B)"
proof (unfold setsum_reindex[OF inj_on_LB], unfold o_def, rule setsum_cong2)
fix x assume x_in_B: "x∈B"
have x_eq_the:"x = (THE y. y ∈ B ∧ L x = L y)"
proof (rule the_equality[symmetric])
show "x ∈ B ∧ L x = L x" using x_in_B by auto
show "!!y. y ∈ B ∧ L x = L y ==> y = x" using inj_on_LB x_in_B unfolding inj_on_def by fast
qed
show "g x *⇩R L x = g (THE y. y ∈ B ∧ L x = L y) *⇩R L x" using x_eq_the by simp
qed
finally show "(∑v∈C. g (THE y. y ∈ B ∧ v = L y) *⇩R v) = L xa" unfolding C_def ..
qed
qed
have "card C = card B" using card_image[OF inj_on_LB] unfolding C_def .
thus ?thesis
by (metis Convex_Euclidean_Space.span_eq L_def dim_image_eq inj_on_LW linear_L sub_W)
qed
lemma invertible_matrix_mult_left_rank:
fixes A::"real^'n^'m" and P::"real^'m^'m"
assumes invertible_P: "invertible P"
shows "rank (P**A) = rank A"
proof -
def TP=="(λx. P *v x)"
def TA≡"(λx. A *v x)"
def TPA=="(λx. (P**A) *v x)"
have sub: "subspace (range (op *v A))" by (metis matrix_vector_mul_linear subspace_UNIV subspace_linear_image)
have "dim (range TPA) = dim (range (TP o TA))" unfolding TP_def TA_def TPA_def o_def matrix_vector_mul_assoc ..
also have "... = dim (range TA)" using dim_image_invertible_mat[OF invertible_P sub] unfolding TP_def TA_def o_def image_compose[symmetric] .
finally show ?thesis unfolding rank_eq_dim_image TPA_def TA_def .
qed
corollary invertible_matrices_mult_rank:
fixes A::"real^'n^'m" and P::"real^'m^'m" and Q::"real^'n^'n"
assumes invertible_P: "invertible P"
and invertible_Q: "invertible Q"
shows "rank (P**A**Q) = rank A"
using invertible_matrix_mult_right_rank[OF invertible_Q] using invertible_matrix_mult_left_rank[OF invertible_P] by metis
lemma invertible_matrix_mult_left_rank':
fixes A::"real^'n^'m" and P::"real^'m^'m"
assumes invertible_P: "invertible P" and B_eq_PA: "B=P**A"
shows "rank B = rank A"
proof -
have "rank B = rank (P**A)" using B_eq_PA by auto
also have "... = rank A" using invertible_matrix_mult_left_rank[OF invertible_P] by auto
finally show ?thesis .
qed
lemma invertible_matrix_mult_right_rank':
fixes A::"real^'n^'m" and Q::"real^'n^'n"
assumes invertible_Q: "invertible Q" and B_eq_PA: "B=A**Q"
shows "rank B = rank A" by (metis B_eq_PA invertible_Q invertible_matrix_mult_right_rank)
lemma invertible_matrices_rank':
fixes A::"real^'n^'m" and P::"real^'m^'m" and Q::"real^'n^'n"
assumes invertible_P: "invertible P" and invertible_Q: "invertible Q" and B_eq_PA: "B=P**A**Q"
shows "rank B = rank A" by (metis B_eq_PA invertible_P invertible_Q invertible_matrices_mult_rank)
text{*Some definitions:*}
definition set_of_vector :: "'a^'n => 'a set"
where "set_of_vector A = {A$i |i. i ∈ UNIV}"
lemma basis_image_linear:
assumes invertible_lf: "invertible_lf f"
and basis_X: "is_basis (set_of_vector X)"
shows "is_basis (f` (set_of_vector X))"
proof (rule iffD1[OF independent_is_basis], rule conjI)
have "card (f ` set_of_vector X) = card (set_of_vector X)"
by (rule card_image[of f "set_of_vector X"], metis invertible_imp_bijective[OF invertible_lf] bij_def inj_eq inj_on_def)
also have "... = card (UNIV::'a set)" using independent_is_basis basis_X by auto
finally show "card (f ` set_of_vector X) = card (UNIV::'a set)" .
show "independent (f ` set_of_vector X)"
proof (rule independent_injective_image)
show "independent (set_of_vector X)" using basis_X unfolding is_basis_def by simp
show "linear f" using invertible_lf unfolding invertible_lf_def by simp
show "inj f" using invertible_imp_bijective[OF invertible_lf] unfolding bij_def by simp
qed
qed
definition cart_basis' :: " real^'n^'n"
where "cart_basis' = (χ i. axis i 1)"
text{*Properties about @{thm "cart_basis'_def"}*}
lemma set_of_vector_cart_basis':
shows "(set_of_vector cart_basis') = {axis i 1 :: real^'n | i. i ∈ (UNIV :: 'n set)}"
unfolding set_of_vector_def cart_basis'_def by auto
lemma cart_basis'_i: "cart_basis' $ i = axis i 1" unfolding cart_basis'_def by simp
lemma finite_cart_basis':
shows "finite (set_of_vector cart_basis')"
proof-
def f=="λi. (cart_basis'::real^'a^'a) $ i"
show ?thesis unfolding set_of_vector_def using finite_Atleast_Atmost_nat[of f] unfolding f_def .
qed
lemma axis_Basis:"{axis i (1::real) |i. i ∈ (UNIV::('a::finite set))} = Basis"
proof (auto)
fix i::"'n::finite" show "axis i (1::real) ∈ Basis" proof (rule axis_in_Basis)
show "(1::real) ∈ Basis" using Basis_real_def by simp
qed
next
fix x::"real^'n" assume x: "x ∈ Basis" show "∃i. x = axis i 1" using x unfolding Basis_vec_def by auto
qed
lemma span_stdbasis:"span {axis i 1 :: real^'n | i. i ∈ (UNIV :: 'n set)} = UNIV"
unfolding span_Basis[symmetric] unfolding axis_Basis by auto
lemma independent_stdbasis: "independent {axis i 1 ::real^'n |i. i∈ (UNIV :: 'n set)}"
by (rule independent_substdbasis, auto, rule axis_in_Basis, auto)
lemma span_cart_basis':
shows "span (set_of_vector cart_basis') = UNIV"
unfolding set_of_vector_def unfolding cart_basis'_def using span_stdbasis by auto
lemma is_basis_cart_basis': "is_basis (set_of_vector (cart_basis'))"
by (metis (lifting) independent_stdbasis is_basis_def set_of_vector_cart_basis' span_stdbasis)
lemma basis_expansion_cart_basis':"setsum (λi. x$i *⇩R cart_basis' $ i) UNIV = x" unfolding cart_basis'_def using basis_expansion apply auto
proof -
assume ass:"(!!x::(real, 'a) vec. (∑i∈UNIV. x $ i *s axis i 1) = x)"
have "(∑i∈UNIV. x $ i *s axis i 1) = x" using ass[of x] .
thus "(∑i∈UNIV. x $ i *⇩R axis i 1) = x" unfolding scalar_mult_eq_scaleR .
qed
lemma basis_expansion_unique:
"setsum (λi. f i *s axis (i::'n::finite) 1) UNIV = (x::('a::comm_ring_1) ^'n) <-> (∀i. f i = x$i)"
proof (auto simp add: basis_expansion)
fix i::"'n"
have univ_rw: "UNIV = (UNIV - {i}) ∪ {i}" by fastforce
have "(∑x∈UNIV. f x * axis x 1 $ i) = setsum (λx. f x * axis x 1 $ i) (UNIV - {i} ∪ {i})" using univ_rw by simp
also have "... = setsum (λx. f x * axis x 1 $ i) (UNIV - {i}) + setsum (λx. f x * axis x 1 $ i) {i}" by (rule setsum_Un_disjoint, auto)
also have "... = f i" unfolding axis_def by auto
finally show "f i = (∑x∈UNIV. f x * axis x 1 $ i)" ..
qed
lemma basis_expansion_cart_basis'_unique: "setsum (λi. f (cart_basis' $ i) *⇩R cart_basis' $ i) UNIV = x <-> (∀i. f (cart_basis' $ i) = x$i)"
using basis_expansion_unique unfolding cart_basis'_def
by (simp add: vec_eq_iff setsum_delta if_distrib cong del: if_weak_cong)
lemma basis_expansion_cart_basis'_unique': "setsum (λi. f i *⇩R cart_basis' $ i) UNIV = x <-> (∀i. f i = x$i)"
using basis_expansion_unique unfolding cart_basis'_def
by (simp add: vec_eq_iff setsum_delta if_distrib cong del: if_weak_cong)
text{*Properties of @{thm "is_basis_def"}*}
lemma setsum_basis_eq:
fixes X::"real^'n^'n"
assumes is_basis:"is_basis (set_of_vector X)"
shows "setsum (λx. f x *⇩R x) (set_of_vector X) = setsum (λi. f (X$i) *⇩R (X$i)) UNIV"
proof (rule setsum_reindex_cong[of "λi. X$i"])
show fact_1: "set_of_vector X = range (op $ X)" unfolding set_of_vector_def by auto
have card_set_of_vector:"card(set_of_vector X) = CARD('n)" using independent_is_basis[of "set_of_vector X"] using is_basis by auto
show "inj (op $ X)"
proof (rule eq_card_imp_inj_on)
show "finite (UNIV::'n set)" using finite_class.finite_UNIV .
show "card (range (op $ X)) = card (UNIV::'n set)" using card_set_of_vector using fact_1 unfolding set_of_vector_def by simp
qed
show "!!a. a ∈ UNIV ==> f (X $ a) *⇩R X $ a = f (X $ a) *⇩R X $ a" by simp
qed
corollary setsum_basis_eq2:
fixes X::"real^'n^'n"
assumes is_basis:"is_basis (set_of_vector X)"
shows "setsum (λx. f x *⇩R x) (set_of_vector X) = setsum (λi. (f o op $ X) i *⇩R (X$i)) UNIV" using setsum_basis_eq[OF is_basis] by simp
lemma inj_op_nth:
fixes X::"real^'n^'n"
assumes is_basis: "is_basis (set_of_vector X)"
shows "inj (op $ X)"
proof -
have fact_1: "set_of_vector X = range (op $ X)" unfolding set_of_vector_def by auto
have card_set_of_vector:"card(set_of_vector X) = CARD('n)" using independent_is_basis[of "set_of_vector X"] using is_basis by auto
show "inj (op $ X)"
proof (rule eq_card_imp_inj_on)
show "finite (UNIV::'n set)" using finite_class.finite_UNIV .
show "card (range (op $ X)) = card (UNIV::'n set)" using card_set_of_vector using fact_1 unfolding set_of_vector_def by simp
qed
qed
lemma basis_UNIV:
fixes X::"real^'n^'n"
assumes is_basis: "is_basis (set_of_vector X)"
shows "UNIV = {x. ∃g. (∑i∈UNIV. g i *⇩R X$i) = x}"
proof -
have "UNIV = {x. ∃g. (∑i∈(set_of_vector X). g i *⇩R i) = x}" using is_basis unfolding is_basis_def using span_finite[OF basis_finite[OF is_basis]] by simp
also have "... ⊆ {x. ∃g. (∑i∈UNIV. g i *⇩R X$i) = x}"
proof (clarify)
fix f
show "∃g. (∑i∈UNIV. g i *⇩R X $ i) = (∑i∈set_of_vector X. f i *⇩R i)"
proof (rule exI[of _ "(λi. (f o op $ X) i)"], unfold o_def, rule setsum_reindex_cong[symmetric, of "op $ X"])
show fact_1: "set_of_vector X = range (op $ X)" unfolding set_of_vector_def by auto
have card_set_of_vector:"card(set_of_vector X) = CARD('n)" using independent_is_basis[of "set_of_vector X"] using is_basis by auto
show "inj (op $ X)" using inj_op_nth[OF is_basis] .
show "!!a. a ∈ UNIV ==> f (X $ a) *⇩R X $ a = f (X $ a) *⇩R X $ a" by simp
qed
qed
finally show ?thesis by auto
qed
lemma scalars_zero_if_basis:
fixes X::"real^'n^'n"
assumes is_basis: "is_basis (set_of_vector X)" and setsum: "(∑i∈(UNIV::'n set). f i *⇩R X$i) = 0"
shows "∀i∈(UNIV::'n set). f i = 0"
proof -
have ind_X: "independent (set_of_vector X)" using is_basis unfolding is_basis_def by simp
have finite_X:"finite (set_of_vector X)" using basis_finite[OF is_basis] .
have 1: "(∀g. (∑v∈(set_of_vector X). g v *⇩R v) = 0 --> (∀v∈(set_of_vector X). g v = 0))" using ind_X unfolding independent_explicit using finite_X by auto
def g≡"λv. f (THE i. X $ i = v)"
have "(∑v∈(set_of_vector X). g v *⇩R v) = 0"
proof -
have "(∑v∈(set_of_vector X). g v *⇩R v) = (∑i∈(UNIV::'n set). f i *⇩R X$i)"
proof (rule setsum_reindex_cong)
show "inj (op $ X)" using inj_op_nth[OF is_basis] .
show "set_of_vector X = range (op $ X)" unfolding set_of_vector_def by auto
show "!!a. a ∈ (UNIV::'n set) ==> f a *⇩R X $ a = g (X $ a) *⇩R X $ a"
proof (auto)
fix a
assume "X $ a ≠ 0"
show "f a = g (X $ a)"
unfolding g_def using inj_op_nth[OF is_basis]
by (metis (lifting, mono_tags) injD the_equality)
qed
qed
thus ?thesis unfolding setsum .
qed
hence 2: "∀v∈(set_of_vector X). g v = 0" using 1 by auto
show ?thesis
proof (clarify)
fix a
have "g (X$a) = 0" using 2 unfolding set_of_vector_def by auto
thus "f a = 0" unfolding g_def using inj_op_nth[OF is_basis]
by (metis (lifting, mono_tags) injD the_equality)
qed
qed
lemma basis_combination_unique:
fixes X::"real^'n^'n"
assumes basis_X: "is_basis (set_of_vector X)" and setsum_eq: "(∑i∈UNIV. g i *⇩R X$i) = (∑i∈UNIV. f i *⇩R X$i)"
shows "f=g"
proof (rule ccontr)
assume "f≠g"
from this obtain x where fx_gx: "f x ≠ g x" by fast
have "0=(∑i∈UNIV. g i *⇩R X$i) - (∑i∈UNIV. f i *⇩R X$i)" using setsum_eq by simp
also have "... = (∑i∈UNIV. g i *⇩R X$i - f i *⇩R X$i)" unfolding setsum_subtractf[symmetric] ..
also have "... = (∑i∈UNIV. (g i - f i) *⇩R X$i)" by (rule setsum_cong2, simp add: scaleR_diff_left)
also have "... = (∑i∈UNIV. (g - f) i *⇩R X$i)" by simp
finally have setsum_eq_1: "0 = (∑i∈UNIV. (g - f) i *⇩R X$i)" by simp
have " ∀i∈UNIV. (g - f) i = 0" by (rule scalars_zero_if_basis[OF basis_X setsum_eq_1[symmetric]])
hence "(g - f) x = 0" by simp
hence "f x = g x" by simp
thus False using fx_gx by contradiction
qed
text{*Definition and properties of the coordinates of a vector (in terms of a particular ordered basis).*}
definition coord :: "real^'n^'n=>real^'n=>real^'n"
where "coord X v = (χ i. (THE f. v = setsum (λx. f x *⇩R X$x) UNIV) i)"
text{*@{term "coord X v"} is the coordinates of vector @{term "v"} with respect to the basis @{term "X"}*}
lemma bij_coord:
fixes X::"real^'n^'n"
assumes basis_X: "is_basis (set_of_vector X)"
shows "bij (coord X)"
proof (unfold bij_def, auto)
show inj: "inj (coord X)"
proof (unfold inj_on_def, auto)
fix x y assume coord_eq: "coord X x = coord X y"
obtain f where f: "(∑x∈UNIV. f x *⇩R X $ x) = x" using basis_UNIV[OF basis_X] by blast
obtain g where g: "(∑x∈UNIV. g x *⇩R X $ x) = y" using basis_UNIV[OF basis_X] by blast
have the_f: "(THE f. x = (∑x∈UNIV. f x *⇩R X $ x)) = f"
proof (rule the_equality)
show "x = (∑x∈UNIV. f x *⇩R X $ x)" using f by simp
show "!!fa. x = (∑x∈UNIV. fa x *⇩R X $ x) ==> fa = f" using basis_combination_unique[OF basis_X] f by simp
qed
have the_g: "(THE g. y = (∑x∈UNIV. g x *⇩R X $ x)) = g"
proof (rule the_equality)
show "y = (∑x∈UNIV. g x *⇩R X $ x)" using g by simp
show "!!ga. y = (∑x∈UNIV. ga x *⇩R X $ x) ==> ga = g" using basis_combination_unique[OF basis_X] g by simp
qed
have "(THE f. x = (∑x∈UNIV. f x *⇩R X $ x)) = (THE g. y = (∑x∈UNIV. g x *⇩R X $ x))"
using coord_eq unfolding coord_def
using vec_lambda_inject[of "(THE f. x = (∑x∈UNIV. f x *⇩R X $ x)) " "(THE f. y = (∑x∈UNIV. f x *⇩R X $ x))"]
by auto
hence "f = g" unfolding the_f the_g .
thus "x=y" using f g by simp
qed
next
fix x::"(real, 'n) vec"
show "x ∈ range (coord X)"
proof (unfold image_def, auto, rule exI[of _ "setsum (λi. x$i *⇩R X$i) UNIV"], unfold coord_def)
def f≡"λi. x$i"
have the_f: " (THE f. (∑i∈UNIV. x $ i *⇩R X $ i) = (∑x∈UNIV. f x *⇩R X $ x)) = f"
proof (rule the_equality)
show "(∑i∈UNIV. x $ i *⇩R X $ i) = (∑x∈UNIV. f x *⇩R X $ x)" unfolding f_def ..
fix g assume setsum_eq:"(∑i∈UNIV. x $ i *⇩R X $ i) = (∑x∈UNIV. g x *⇩R X $ x)"
show "g = f" using basis_combination_unique[OF basis_X] using setsum_eq unfolding f_def by simp
qed
show " x = vec_lambda (THE f. (∑i∈UNIV. x $ i *⇩R X $ i) = (∑x∈UNIV. f x *⇩R X $ x))" unfolding the_f unfolding f_def using vec_lambda_eta[of x] by simp
qed
qed
lemma linear_coord:
fixes X::"real^'n^'n"
assumes basis_X: "is_basis (set_of_vector X)"
shows "linear (coord X)"
proof (unfold linear_def coord_def, auto)
fix x y::"(real, 'n) vec"
show "vec_lambda (THE f. x + y = (∑x∈UNIV. f x *⇩R X $ x)) = vec_lambda (THE f. x = (∑x∈UNIV. f x *⇩R X $ x)) + vec_lambda (THE f. y = (∑x∈UNIV. f x *⇩R X $ x))"
proof -
obtain f where f: "(∑a∈(UNIV::'n set). f a *⇩R X $ a) = x + y" using basis_UNIV[OF basis_X] by blast
obtain g where g: " (∑x∈UNIV. g x *⇩R X $ x) = x" using basis_UNIV[OF basis_X] by blast
obtain h where h: "(∑x∈UNIV. h x *⇩R X $ x) = y" using basis_UNIV[OF basis_X] by blast
def t≡"λi. g i + h i"
have the_f: "(THE f. x + y = (∑x∈UNIV. f x *⇩R X $ x)) = f"
proof (rule the_equality)
show " x + y = (∑x∈UNIV. f x *⇩R X $ x)" using f by simp
show "!!fa. x + y = (∑x∈UNIV. fa x *⇩R X $ x) ==> fa = f" using basis_combination_unique[OF basis_X] f by simp
qed
have the_g: "(THE g. x = (∑x∈UNIV. g x *⇩R X $ x)) = g"
proof (rule the_equality)
show "x = (∑x∈UNIV. g x *⇩R X $ x)" using g by simp
show "!!ga. x = (∑x∈UNIV. ga x *⇩R X $ x) ==> ga = g" using basis_combination_unique[OF basis_X] g by simp
qed
have the_h: "(THE h. y = (∑x∈UNIV. h x *⇩R X $ x)) = h"
proof (rule the_equality)
show "y = (∑x∈UNIV. h x *⇩R X $ x)" using h ..
show "!!ha. y = (∑x∈UNIV. ha x *⇩R X $ x) ==> ha = h" using basis_combination_unique[OF basis_X] h by simp
qed
have "(∑a∈(UNIV::'n set). f a *⇩R X $ a) = (∑x∈UNIV. g x *⇩R X $ x) + (∑x∈UNIV. h x *⇩R X $ x)" using f g h by simp
also have "... = (∑x∈UNIV. g x *⇩R X $ x + h x *⇩R X $ x)" unfolding setsum_addf[symmetric] ..
also have "... = (∑x∈UNIV. (g x + h x) *⇩R X $ x)" by (rule setsum_cong2, simp add: scaleR_left_distrib)
also have "... = (∑x∈UNIV. t x *⇩R X $ x)" unfolding t_def ..
finally have "(∑a∈UNIV. f a *⇩R X $ a) = (∑x∈UNIV. t x *⇩R X $ x)" .
hence "f=t" using basis_combination_unique[OF basis_X] by auto
thus ?thesis
by (unfold the_f the_g the_h, vector, auto, unfold f g h t_def, simp)
qed
next
fix c x
show " vec_lambda (THE f. c *⇩R x = (∑x∈UNIV. f x *⇩R X $ x)) = c *⇩R vec_lambda (THE f. x = (∑x∈UNIV. f x *⇩R X $ x))"
proof -
obtain f where f: "(∑x∈UNIV. f x *⇩R X $ x) = c *⇩R x" using basis_UNIV[OF basis_X] by blast
obtain g where g: "(∑x∈UNIV. g x *⇩R X $ x) = x" using basis_UNIV[OF basis_X] by blast
def t≡"λi. c *⇩R g i"
have the_f: "(THE f. c *⇩R x = (∑x∈UNIV. f x *⇩R X $ x)) = f"
proof (rule the_equality)
show " c *⇩R x = (∑x∈UNIV. f x *⇩R X $ x)" using f ..
show "!!fa. c *⇩R x = (∑x∈UNIV. fa x *⇩R X $ x) ==> fa = f" using basis_combination_unique[OF basis_X] f by simp
qed
have the_g: "(THE g. x = (∑x∈UNIV. g x *⇩R X $ x)) = g"proof (rule the_equality)
show " x = (∑x∈UNIV. g x *⇩R X $ x)" using g ..
show "!!ga. x = (∑x∈UNIV. ga x *⇩R X $ x) ==> ga = g" using basis_combination_unique[OF basis_X] g by simp
qed
have "(∑x∈UNIV. f x *⇩R X $ x) = c *⇩R (∑x∈UNIV. g x *⇩R X $ x)" using f g by simp
also have "... = (∑x∈UNIV. c *⇩R g x *⇩R X $ x)" by (rule scaleR_setsum_right)
also have "... = (∑x∈UNIV. t x *⇩R X $ x)" unfolding t_def by simp
finally have " (∑x∈UNIV. f x *⇩R X $ x) = (∑x∈UNIV. t x *⇩R X $ x)" .
hence "f=t" using basis_combination_unique[OF basis_X] by auto
thus ?thesis
by (unfold the_f the_g, vector, auto, unfold t_def, auto)
qed
qed
lemma coord_eq:
assumes basis_X:"is_basis (set_of_vector X)"
and coord_eq: "coord X v = coord X w"
shows "v = w"
proof -
have "∀i. (THE f. ∀i. v $ i = (∑x∈UNIV. f x * X $ x $ i)) i = (THE f. ∀i. w $ i = (∑x∈UNIV. f x * X $ x $ i)) i" using coord_eq
unfolding coord_eq coord_def vec_eq_iff by simp
hence the_eq: "(THE f. ∀i. v $ i = (∑x∈UNIV. f x * X $ x $ i)) = (THE f. ∀i. w $ i = (∑x∈UNIV. f x * X $ x $ i))" by auto
obtain f where f: "(∑x∈UNIV. f x *⇩R X $ x)= v" using basis_UNIV[OF basis_X] by blast
obtain g where g: "(∑x∈UNIV. g x *⇩R X $ x)= w" using basis_UNIV[OF basis_X] by blast
have the_f: "(THE f. ∀i. v $ i = (∑x∈UNIV. f x * X $ x $ i)) = f"
proof (rule the_equality)
show " ∀i. v $ i = (∑x∈UNIV. f x * X $ x $ i)" using f by auto
fix fa assume "∀i. v $ i = (∑x∈UNIV. fa x * X $ x $ i)"
hence "∀i. v $ i = (∑x∈UNIV. fa x *⇩R X $ x) $ i" unfolding setsum_component by simp
hence fa:" v = (∑x∈UNIV. fa x *⇩R X $ x)" unfolding vec_eq_iff .
show "fa = f" using basis_combination_unique[OF basis_X] f fa by simp
qed
have the_g: "(THE g. ∀i. w $ i = (∑x∈UNIV. g x * X $ x $ i)) = g"
proof (rule the_equality)
show " ∀i. w $ i = (∑x∈UNIV. g x * X $ x $ i)" using g by auto
fix fa assume "∀i. w $ i = (∑x∈UNIV. fa x * X $ x $ i)"
hence "∀i. w $ i = (∑x∈UNIV. fa x *⇩R X $ x) $ i" unfolding setsum_component by simp
hence fa:" w = (∑x∈UNIV. fa x *⇩R X $ x)" unfolding vec_eq_iff .
show "fa = g" using basis_combination_unique[OF basis_X] g fa by simp
qed
have "f=g" using the_eq unfolding the_f the_g .
thus "v=w" using f g by blast
qed
text{*Definitions of matrix of change of basis and matrix of a linear transformation with respect to two bases:*}
definition matrix_change_of_basis :: "real^'n^'n =>real^'n^'n=>real^'n^'n"
where "matrix_change_of_basis X Y = (χ i j. (coord Y (X$j)) $ i)"
definition matrix' :: "real^'n^'n => real^'m^'m => (real^'n => real^'m) => real^'n^'m"
where "matrix' X Y f= (χ i j. (coord Y (f(X$j))) $ i)"
text{*Properties of @{thm "matrix'_def"}*}
lemma matrix'_eq_matrix:
defines cart_basis_Rn: "cart_basis_Rn == (cart_basis')::real^'n^'n" and cart_basis_Rm:"cart_basis_Rm == (cart_basis')::real^'m^'m"
assumes lf: "linear f"
shows "matrix' (cart_basis_Rn) (cart_basis_Rm) f = matrix f"
proof (unfold matrix_def matrix'_def coord_def, vector, auto)
fix i j
have basis_Rn:"is_basis (set_of_vector cart_basis_Rn)" using is_basis_cart_basis' unfolding cart_basis_Rn .
have basis_Rm:"is_basis (set_of_vector cart_basis_Rm)" using is_basis_cart_basis' unfolding cart_basis_Rm .
obtain g where setsum_g: "(∑x∈UNIV. g x *⇩R (cart_basis_Rm $ x)) = f (cart_basis_Rn $ j)" using basis_UNIV[OF basis_Rm] by blast
have the_g: "(THE g. ∀a. f (cart_basis_Rn $ j) $ a = (∑x∈UNIV. g x * cart_basis_Rm $ x $ a)) = g"
proof (rule the_equality, clarify)
fix a
have "f (cart_basis_Rn $ j) $ a = (∑i∈UNIV. g i *⇩R (cart_basis_Rm $ i)) $ a" using setsum_g by simp
also have "... = (∑x∈UNIV. g x * cart_basis_Rm $ x $ a)" unfolding setsum_component by simp
finally show "f (cart_basis_Rn $ j) $ a = (∑x∈UNIV. g x * cart_basis_Rm $ x $ a)" .
fix ga assume "∀a. f (cart_basis_Rn $ j) $ a = (∑x∈UNIV. ga x * cart_basis_Rm $ x $ a)"
hence setsum_ga: "f (cart_basis_Rn $ j) = (∑i∈UNIV. ga i *⇩R cart_basis_Rm $ i)" by (vector, auto)
show "ga = g"
proof (rule basis_combination_unique)
show "is_basis (set_of_vector (cart_basis_Rm))" using basis_Rm .
show " (∑i∈UNIV. g i *⇩R cart_basis_Rm $ i) = (∑i∈UNIV. ga i *⇩R cart_basis_Rm $ i)" using setsum_g setsum_ga by simp
qed
qed
show " (THE fa. ∀i. f (cart_basis_Rn $ j) $ i = (∑x∈UNIV. fa x * cart_basis_Rm $ x $ i)) i = f (axis j 1) $ i"
unfolding the_g using setsum_g unfolding cart_basis_Rm cart_basis_Rn cart_basis'_def using basis_expansion_unique[of g "f (axis j 1)"]
unfolding scalar_mult_eq_scaleR by auto
qed
lemma matrix':
assumes linear_f: "linear f" and basis_X: "is_basis (set_of_vector X)" and basis_Y: "is_basis (set_of_vector Y)"
shows "f (X$i) = setsum (λj. (matrix' X Y f) $ j $ i *⇩R (Y$j)) UNIV"
proof (unfold matrix'_def coord_def matrix_mult_vsum column_def, vector, auto)
fix j
obtain g where g: "(∑x∈UNIV. g x *⇩R Y $ x) = f (X $ i)" using basis_UNIV[OF basis_Y] by blast
have the_g: "(THE fa. ∀ia. f (X $ i) $ ia = (∑x∈UNIV. fa x * Y $ x $ ia)) = g"
proof (rule the_equality, clarify)
fix a
have "f (X $ i) $ a = (∑x∈UNIV. g x *⇩R Y $ x) $ a" using g by simp
also have "... = (∑x∈UNIV. g x * Y $ x $ a)" unfolding setsum_component by auto
finally show "f (X $ i) $ a = (∑x∈UNIV. g x * Y $ x $ a)" .
fix fa
assume "∀ia. f (X $ i) $ ia = (∑x∈UNIV. fa x * Y $ x $ ia)"
hence " ∀ia. f (X $ i) $ ia = (∑x∈UNIV. fa x *⇩R Y $ x) $ ia" unfolding setsum_component by simp
hence fa:"f (X $ i) = (∑x∈UNIV. fa x *⇩R Y $ x)" unfolding vec_eq_iff .
show "fa = g" by (rule basis_combination_unique[OF basis_Y], simp add: fa g)
qed
show " f (X $ i) $ j = (∑x∈UNIV. (THE fa. ∀j. f (X $ i) $ j = (∑x∈UNIV. fa x * Y $ x $ j)) x * Y $ x $ j)"
unfolding the_g unfolding g[symmetric] setsum_component by simp
qed
corollary matrix'2:
assumes linear_f: "linear f" and basis_X: "is_basis (set_of_vector X)" and basis_Y: "is_basis (set_of_vector Y)"
and eq_f: "∀i. f (X$i) = setsum (λj. A $ j $ i *⇩R (Y$j)) UNIV"
shows "matrix' X Y f = A"
proof -
have eq_f': "∀i. f (X$i) = setsum (λj. (matrix' X Y f) $ j $ i *⇩R (Y$j)) UNIV" using matrix'[OF linear_f basis_X basis_Y] by auto
show ?thesis
proof (vector, auto)
fix i j
def a≡"λx. (matrix' X Y f) $ x $ i"
def b≡"λx. A $ x $ i"
have fxi_1:"f (X$i) = setsum (λj. a j *⇩R (Y$j)) UNIV" using eq_f' unfolding a_def by simp
have fxi_2: "f (X$i) = setsum (λj. b j *⇩R (Y$j)) UNIV" using eq_f unfolding b_def by simp
have "a=b" using basis_combination_unique[OF basis_Y] fxi_1 fxi_2 by auto
thus "(matrix' X Y f) $ j $ i = A $ j $ i" unfolding a_def b_def by metis
qed
qed
lemma coord_matrix':
fixes X::"real^'n^'n" and Y::"real^'m^'m"
assumes basis_X: "is_basis (set_of_vector X)" and basis_Y: "is_basis (set_of_vector Y)" and linear_f: "linear f"
shows "coord Y (f v) = (matrix' X Y f) *v (coord X v)"
proof (unfold matrix_mult_vsum matrix'_def column_def coord_def, vector, auto)
fix i
obtain g where g: "(∑x∈UNIV. g x *⇩R Y $ x) = f v" using basis_UNIV[OF basis_Y] by auto
obtain s where s: "(∑x∈UNIV. s x *⇩R X $ x) = v" using basis_UNIV[OF basis_X] by auto
have the_g: "(THE fa. ∀a. f v $ a = (∑x∈UNIV. fa x * Y $ x $ a)) = g"
proof (rule the_equality)
have "∀a. f v $ a = (∑x∈UNIV. g x *⇩R Y $ x) $ a" using g by simp
thus " ∀a. f v $ a = (∑x∈UNIV. g x * Y $ x $ a)" unfolding setsum_component by simp
fix fa assume " ∀a. f v $ a = (∑x∈UNIV. fa x * Y $ x $ a)"
hence fa: "f v = (∑x∈UNIV. fa x *⇩R Y $ x)" by (vector, auto)
show "fa=g" by (rule basis_combination_unique[OF basis_Y], simp add: fa g)
qed
have the_s: "(THE f. ∀i. v $ i = (∑x∈UNIV. f x * X $ x $ i))=s"
proof (rule the_equality)
have " ∀i. v $ i = (∑x∈UNIV. s x *⇩R X $ x) $ i" using s by simp
thus " ∀i. v $ i = (∑x∈UNIV. s x * X $ x $ i)"unfolding setsum_component by simp
fix fa assume "∀i. v $ i = (∑x∈UNIV. fa x * X $ x $ i)"
hence fa: "v=(∑x∈UNIV. fa x *⇩R X $ x)" by (vector, auto)
show "fa=s"by (rule basis_combination_unique[OF basis_X], simp add: fa s)
qed
def t≡"λx. (∑i∈UNIV. (s i * (THE fa. f (X $ i) = (∑x∈UNIV. fa x *⇩R Y $ x)) x))"
have "(∑x∈UNIV. g x *⇩R Y $ x) = f v" using g by simp
also have "... = f (∑x∈UNIV. s x *⇩R X $ x)" using s by simp
also have "... = (∑x∈UNIV. s x *⇩R f (X $ x))" by (rule linear_setsum_mul[OF linear_f], simp)
also have "... = (∑i∈UNIV. s i *⇩R setsum (λj. (matrix' X Y f)$j$i *⇩R (Y$j)) UNIV)" using matrix'[OF linear_f basis_X basis_Y] by auto
also have "... = (∑i∈UNIV. ∑x∈UNIV. s i *⇩R matrix' X Y f $ x $ i *⇩R Y $ x)" unfolding scaleR_setsum_right ..
also have "... = (∑i∈UNIV. ∑x∈UNIV. (s i * (THE fa. f (X $ i) = (∑x∈UNIV. fa x *⇩R Y $ x)) x) *⇩R Y $ x)" unfolding matrix'_def unfolding coord_def by auto
also have "... = (∑x∈UNIV. (∑i∈UNIV. (s i * (THE fa. f (X $ i) = (∑x∈UNIV. fa x *⇩R Y $ x)) x) *⇩R Y $ x))" by (rule setsum_commute)
also have "... = (∑x∈UNIV. (∑i∈UNIV. (s i * (THE fa. f (X $ i) = (∑x∈UNIV. fa x *⇩R Y $ x)) x)) *⇩R Y $ x)" unfolding scaleR_setsum_left ..
also have "... = (∑x∈UNIV. t x *⇩R Y $ x)" unfolding t_def ..
finally have "(∑x∈UNIV. g x *⇩R Y $ x) = (∑x∈UNIV. t x *⇩R Y $ x)" .
hence "g=t" using basis_combination_unique[OF basis_Y] by simp
thus "(THE fa. ∀i. f v $ i = (∑x∈UNIV. fa x * Y $ x $ i)) i =
(∑x∈UNIV. (THE f. ∀i. v $ i = (∑x∈UNIV. f x * X $ x $ i)) x * (THE fa. ∀i. f (X $ x) $ i = (∑x∈UNIV. fa x * Y $ x $ i)) i)"
proof (unfold the_g the_s t_def, auto)
have " (∑x∈UNIV. s x * (THE fa. ∀i. f (X $ x) $ i = (∑x∈UNIV. fa x * Y $ x $ i)) i) =
(∑x∈UNIV. s x * (THE fa. ∀i. f (X $ x) $ i = (∑x∈UNIV. fa x *⇩R Y $ x) $ i) i)" unfolding setsum_component by simp
also have "... = (∑x∈UNIV. s x * (THE fa. f (X $ x) = (∑x∈UNIV. fa x *⇩R Y $ x)) i)" by (rule setsum_cong2, simp add: vec_eq_iff)
finally show " (∑ia∈UNIV. s ia * (THE fa. f (X $ ia) = (∑x∈UNIV. fa x *⇩R Y $ x)) i) = (∑x∈UNIV. s x * (THE fa. ∀i. f (X $ x) $ i = (∑x∈UNIV. fa x * Y $ x $ i)) i)"
by auto
qed
qed
lemma matrix'_compose:
fixes X::"real^'n^'n" and Y::"real^'m^'m" and Z::"real^'p^'p"
assumes basis_X: "is_basis (set_of_vector X)" and basis_Y: "is_basis (set_of_vector Y)" and basis_Z: "is_basis (set_of_vector Z)"
and linear_f: "linear f" and linear_g: "linear g"
shows "matrix' X Z (g o f) = (matrix' Y Z g) ** (matrix' X Y f)"
proof (unfold matrix_eq, clarify)
fix a::"(real, 'n) vec"
obtain v where v: "a = coord X v" using bij_coord[OF basis_X] unfolding bij_iff by metis
have linear_gf: "linear (g o f)" using linear_compose[OF linear_f linear_g] .
have "matrix' X Z (g o f) *v a = matrix' X Z (g o f) *v (coord X v)" unfolding v ..
also have "... = coord Z ((g o f) v)" unfolding coord_matrix'[OF basis_X basis_Z linear_gf, symmetric] ..
also have "... = coord Z (g (f v))" unfolding o_def ..
also have "... = (matrix' Y Z g) *v (coord Y (f v))" unfolding coord_matrix'[OF basis_Y basis_Z linear_g] ..
also have "... = (matrix' Y Z g) *v ((matrix' X Y f) *v (coord X v))" unfolding coord_matrix'[OF basis_X basis_Y linear_f] ..
also have "... = ((matrix' Y Z g) ** (matrix' X Y f)) *v (coord X v)" unfolding matrix_vector_mul_assoc ..
finally show "matrix' X Z (g o f) *v a = matrix' Y Z g ** matrix' X Y f *v a" unfolding v .
qed
lemma exists_linear_eq_matrix':
fixes A::"real^'m^'n" and X::"real^'m^'m" and Y::"real^'n^'n"
assumes basis_X: "is_basis (set_of_vector X)" and basis_Y: "is_basis (set_of_vector Y)"
shows "∃f. matrix' X Y f = A ∧ linear f"
proof -
def f == "λv. setsum (λj. A $ j $ (THE k. v = X $ k) *⇩R Y $ j) UNIV"
obtain g where linear_g: "linear g" and f_eq_g: "(∀x ∈ (set_of_vector X). g x = f x)" using linear_independent_extend using basis_X unfolding is_basis_def by blast
show ?thesis
proof (rule exI[of _ g], rule conjI)
show "matrix' X Y g = A"
proof (rule matrix'2)
show "linear g" using linear_g .
show "is_basis (set_of_vector X)" using basis_X .
show "is_basis (set_of_vector Y)" using basis_Y .
show "∀i. g (X $ i) = (∑j∈UNIV. A $ j $ i *⇩R Y $ j)"
proof (clarify)
fix i
have the_k_eq_i: "(THE k. X $ i = X $ k) = i"
proof (rule the_equality)
show "X $ i = X $ i" ..
fix k assume Xi_Xk: "X $ i = X $ k" show "k = i" using Xi_Xk basis_X inj_eq inj_op_nth by metis
qed
have Xi_in_X:"X$i ∈ (set_of_vector X)" unfolding set_of_vector_def by auto
have "g (X$i) = f (X$i)" using f_eq_g Xi_in_X by simp
also have "... = (∑j∈UNIV. A $ j $ (THE k. X $ i = X $ k) *⇩R Y $ j)" unfolding f_def ..
also have "... = (∑j∈UNIV. A $ j $ i *⇩R Y $ j)" unfolding the_k_eq_i ..
finally show "g (X $ i) = (∑j∈UNIV. A $ j $ i *⇩R Y $ j)" .
qed
qed
show "linear g" using linear_g .
qed
qed
lemma linear_matrix':
assumes basis_Y: "is_basis (set_of_vector Y)"
shows "linear (matrix' X Y)"
proof (unfold linear_def, auto)
fix f g
show "matrix' X Y (f + g) = matrix' X Y f + matrix' X Y g"
proof (unfold matrix'_def coord_def, vector, auto)
fix i j
obtain a where a:"(∑x∈UNIV. a x *⇩R Y $ x) = f (X $ j)" using basis_UNIV[OF basis_Y] by blast
obtain b where b:"(∑x∈UNIV. b x *⇩R Y $ x) = g (X $ j)" using basis_UNIV[OF basis_Y] by blast
obtain c where c: "(∑x∈UNIV. c x *⇩R Y $ x) = (f + g) (X $ j)" using basis_UNIV[OF basis_Y] by blast
def d≡"λi. a i + b i"
have "(∑x∈UNIV. c x *⇩R Y $ x) = (f + g) (X $ j)" using c by simp
also have "... = f (X $ j) + g (X $ j)" unfolding plus_fun_def ..
also have "... = (∑x∈UNIV. a x *⇩R Y $ x) + (∑x∈UNIV. b x *⇩R Y $ x)" unfolding a b ..
also have "... = (∑x∈UNIV. (a x *⇩R Y $ x) + b x *⇩R Y $ x)" unfolding setsum_addf ..
also have "... = (∑x∈UNIV. (a x + b x) *⇩R Y $ x)" unfolding scaleR_add_left ..
also have "... = (∑x∈UNIV. (d x) *⇩R Y $ x)" unfolding d_def by simp
finally have "(∑x∈UNIV. c x *⇩R Y $ x) = (∑x∈UNIV. d x *⇩R Y $ x)" .
hence c_eq_d: "c=d" using basis_combination_unique[OF basis_Y] by simp
have the_a: "(THE fa. ∀i. f (X $ j) $ i = (∑x∈UNIV. fa x * Y $ x $ i)) = a"
proof (rule the_equality)
have " ∀i. f (X $ j) $ i = (∑x∈UNIV. a x *⇩R Y $ x) $ i" using a unfolding vec_eq_iff by simp
thus " ∀i. f (X $ j) $ i = (∑x∈UNIV. a x * Y $ x $ i)" unfolding setsum_component by simp
fix fa assume "∀i. f (X $ j) $ i = (∑x∈UNIV. fa x * Y $ x $ i)"
hence "f (X $ j) = (∑x∈UNIV. fa x *⇩R Y $ x)" unfolding vec_eq_iff setsum_component by simp
thus "fa = a" using basis_combination_unique[OF basis_Y] a by simp
qed
have the_b:"(THE f. ∀i. g (X $ j) $ i = (∑x∈UNIV. f x * Y $ x $ i)) = b"
proof (rule the_equality)
have "∀i. g (X $ j) $ i = (∑x∈UNIV. b x *⇩R Y $ x) $ i" using b unfolding vec_eq_iff by simp
thus " ∀i. g (X $ j) $ i = (∑x∈UNIV. b x * Y $ x $ i)" unfolding setsum_component by simp
fix fa assume "∀i. g (X $ j) $ i = (∑x∈UNIV. fa x * Y $ x $ i)"
hence "g (X $ j) = (∑x∈UNIV. fa x *⇩R Y $ x)" unfolding vec_eq_iff setsum_component by simp
thus "fa = b" using basis_combination_unique[OF basis_Y] b by simp
qed
have the_c: "(THE fa. ∀i. (f + g) (X $ j) $ i = (∑x∈UNIV. fa x * Y $ x $ i)) = c"
proof (rule the_equality)
have "∀i. (f + g) (X $ j) $ i = (∑x∈UNIV. c x *⇩R Y $ x) $ i" using c unfolding vec_eq_iff by simp
thus " ∀i. (f + g) (X $ j) $ i = (∑x∈UNIV. c x * Y $ x $ i)" unfolding setsum_component by simp
fix fa assume "∀i. (f + g) (X $ j) $ i = (∑x∈UNIV. fa x * Y $ x $ i)"
hence "(f + g) (X $ j) = (∑x∈UNIV. fa x *⇩R Y $ x)" unfolding vec_eq_iff setsum_component by simp
thus "fa = c" using basis_combination_unique[OF basis_Y] c by simp
qed
show "(THE fa. ∀i. (f + g) (X $ j) $ i = (∑x∈UNIV. fa x * Y $ x $ i)) i =
(THE fa. ∀i. f (X $ j) $ i = (∑x∈UNIV. fa x * Y $ x $ i)) i + (THE f. ∀i. g (X $ j) $ i = (∑x∈UNIV. f x * Y $ x $ i)) i"
unfolding the_a the_b the_c unfolding a b c using c_eq_d unfolding d_def by fast
qed
fix c
show "matrix' X Y (c *⇩R f) = c *⇩R matrix' X Y f"
proof (unfold matrix'_def coord_def, vector, auto)
fix i j
obtain a where a:"(∑x∈UNIV. a x *⇩R Y $ x) = f (X $ j)" using basis_UNIV[OF basis_Y] by blast
obtain b where b: "(∑x∈UNIV. b x *⇩R Y $ x) = (c *⇩R f) (X $ j)" using basis_UNIV[OF basis_Y] by blast
def d≡"λi. c *⇩R a i"
have the_a: "(THE fa. ∀i. f (X $ j) $ i = (∑x∈UNIV. fa x * Y $ x $ i)) = a"
proof (rule the_equality)
have "∀i. f (X $ j) $ i = (∑x∈UNIV. a x *⇩R Y $ x) $ i" using a unfolding vec_eq_iff by simp
thus "∀i. f (X $ j) $ i = (∑x∈UNIV. a x * Y $ x $ i)" unfolding setsum_component by simp
fix fa assume "∀i. f (X $ j) $ i = (∑x∈UNIV. fa x * Y $ x $ i)"
hence "f (X $ j) = (∑x∈UNIV. fa x *⇩R Y $ x)" unfolding vec_eq_iff setsum_component by simp
thus "fa = a" using basis_combination_unique[OF basis_Y] a by simp
qed
have the_b: "(THE fa. ∀i. (c *⇩R f) (X $ j) $ i = (∑x∈UNIV. fa x * Y $ x $ i)) = b"
proof (rule the_equality)
have "∀i. (c *⇩R f) (X $ j) $ i = (∑x∈UNIV. b x *⇩R Y $ x) $ i" using b unfolding vec_eq_iff by simp
thus "∀i. (c *⇩R f) (X $ j) $ i = (∑x∈UNIV. b x * Y $ x $ i)" unfolding setsum_component by simp
fix fa assume "∀i. (c *⇩R f) (X $ j) $ i = (∑x∈UNIV. fa x * Y $ x $ i)"
hence "(c *⇩R f) (X $ j) = (∑x∈UNIV. fa x *⇩R Y $ x)" unfolding vec_eq_iff setsum_component by simp
thus "fa = b" using basis_combination_unique[OF basis_Y] b by simp
qed
have "(∑x∈UNIV. b x *⇩R Y $ x) = (c *⇩R f) (X $ j)" using b .
also have "... = c *⇩R f (X $ j)" unfolding scaleR_fun_def ..
also have "... = c *⇩R (∑x∈UNIV. a x *⇩R Y $ x)" unfolding a ..
also have "... = (∑x∈UNIV. c *⇩R (a x *⇩R Y $ x))" unfolding scaleR_setsum_right ..
also have "... = (∑x∈UNIV. (c *⇩R a x) *⇩R Y $ x)" by auto
also have "... = (∑x∈UNIV. d x *⇩R Y $ x)" unfolding d_def ..
finally have "(∑x∈UNIV. b x *⇩R Y $ x) = (∑x∈UNIV. d x *⇩R Y $ x)" .
hence "b=d" using basis_combination_unique[OF basis_Y] b by simp
thus "(THE fa. ∀i. (c *⇩R f) (X $ j) $ i = (∑x∈UNIV. fa x * Y $ x $ i)) i = c * (THE fa. ∀i. f (X $ j) $ i = (∑x∈UNIV. fa x * Y $ x $ i)) i"
unfolding the_a the_b d_def
by simp
qed
qed
lemma matrix'_surj:
assumes basis_X: "is_basis (set_of_vector X)" and basis_Y: "is_basis (set_of_vector Y)"
shows "surj (matrix' X Y)"
proof (unfold surj_def, clarify)
fix A
show "∃f. A = matrix' X Y f"
using exists_linear_eq_matrix'[OF basis_X basis_Y, of A] unfolding matrix'_def by auto
qed
text{*Properties of @{thm "matrix_change_of_basis_def"}.*}
lemma matrix_change_of_basis_works:
fixes X::"real^'n^'n" and Y::"real^'n^'n"
assumes basis_X: "is_basis (set_of_vector X)"
and basis_Y: "is_basis (set_of_vector Y)"
shows "(matrix_change_of_basis X Y) *v (coord X v) = (coord Y v)"
proof (unfold matrix_mult_vsum matrix_change_of_basis_def column_def coord_def, vector, auto)
fix i
obtain f where f: "(∑x∈UNIV. f x *⇩R Y $ x) = v" using basis_UNIV[OF basis_Y] by blast
obtain g where g: "(∑x∈UNIV. g x *⇩R X $ x) = v" using basis_UNIV[OF basis_X] by blast
def t≡"λx. (THE f. X $ x= (∑a∈UNIV. f a *⇩R Y $ a))"
def w≡"λi. (∑x∈UNIV. g x *⇩R t x i)"
have the_f:"(THE f. ∀i. v $ i = (∑x∈UNIV. f x * Y $ x $ i)) = f"
proof (rule the_equality)
show "∀i. v $ i = (∑x∈UNIV. f x * Y $ x $ i)" using f by auto
fix fa assume "∀i. v $ i = (∑x∈UNIV. fa x * Y $ x $ i)"
hence "∀i. v $ i = (∑x∈UNIV. fa x *⇩R Y $ x) $ i" unfolding setsum_component by simp
hence fa: " v = (∑x∈UNIV. fa x *⇩R Y $ x)" unfolding vec_eq_iff .
show "fa = f"
using basis_combination_unique[OF basis_Y] fa f by simp
qed
have the_g: "(THE f. ∀i. v $ i = (∑x∈UNIV. f x * X $ x $ i)) = g"
proof (rule the_equality)
show "∀i. v $ i = (∑x∈UNIV. g x * X $ x $ i)" using g by auto
fix fa assume "∀i. v $ i = (∑x∈UNIV. fa x * X $ x $ i)"
hence "∀i. v $ i = (∑x∈UNIV. fa x *⇩R X $ x) $ i" unfolding setsum_component by simp
hence fa: " v = (∑x∈UNIV. fa x *⇩R X $ x)" unfolding vec_eq_iff .
show "fa = g"
using basis_combination_unique[OF basis_X] fa g by simp
qed
have "(∑x∈UNIV. f x *⇩R Y $ x) = (∑x∈UNIV. g x *⇩R X $ x)" unfolding f g ..
also have "... = (∑x∈UNIV. g x *⇩R (setsum (λi. (t x i) *⇩R Y $ i) UNIV))" unfolding t_def
proof (rule setsum_cong2)
fix x
obtain h where h: "(∑a∈UNIV. h a *⇩R Y $ a) = X$x" using basis_UNIV[OF basis_Y] by blast
have the_h: "(THE f. X $ x = (∑a∈UNIV. f a *⇩R Y $ a))=h"
proof (rule the_equality)
show " X $ x = (∑a∈UNIV. h a *⇩R Y $ a)" using h by simp
fix f assume f: "X $ x = (∑a∈UNIV. f a *⇩R Y $ a)"
show "f = h" using basis_combination_unique[OF basis_Y] f h by simp
qed
show " g x *⇩R X $ x = g x *⇩R (∑i∈UNIV. (THE f. X $ x = (∑a∈UNIV. f a *⇩R Y $ a)) i *⇩R Y $ i)" unfolding the_h h ..
qed
also have "... = (∑x∈UNIV. (setsum (λi. g x *⇩R (t x i) *⇩R Y $ i) UNIV))" unfolding scaleR_setsum_right ..
also have "... = (∑i∈UNIV. ∑x∈UNIV. g x *⇩R t x i *⇩R Y $ i)" by (rule setsum_commute)
also have "... = (∑i∈UNIV. (∑x∈UNIV. g x *⇩R t x i) *⇩R Y $ i)" unfolding scaleR_setsum_left by auto
finally have "(∑x∈UNIV. f x *⇩R Y $ x) = (∑i∈UNIV. (∑x∈UNIV. g x *⇩R t x i) *⇩R Y $ i) " .
hence "f=w" using basis_combination_unique[OF basis_Y] unfolding w_def by auto
thus "(∑x∈UNIV. (THE f. ∀i. v $ i = (∑x∈UNIV. f x * X $ x $ i)) x * (THE f. ∀i. X $ x $ i = (∑x∈UNIV. f x * Y $ x $ i)) i) =
(THE f. ∀i. v $ i = (∑x∈UNIV. f x * Y $ x $ i)) i" unfolding the_f the_g unfolding w_def t_def unfolding vec_eq_iff by auto
qed
lemma matrix_change_of_basis_mat_1:
fixes X::"real^'n^'n"
assumes basis_X: "is_basis (set_of_vector X)"
shows "matrix_change_of_basis X X = mat 1"
proof (unfold matrix_change_of_basis_def coord_def mat_def, vector, auto)
fix j::"'n"
def f≡"λi. if i=j then 1::real else 0"
have UNIV_rw: "UNIV = insert j (UNIV-{j})" by auto
have "(∑x∈UNIV. f x *⇩R X $ x) = (∑x∈(insert j (UNIV-{j})). f x *⇩R X $ x)" using UNIV_rw by simp
also have "... = (λx. f x *⇩R X $ x) j + (∑x∈(UNIV-{j}). f x *⇩R X $ x)" by (rule setsum_insert, simp+)
also have "... = X$j + (∑x∈(UNIV-{j}). f x *⇩R X $ x)" unfolding f_def by simp
also have "... = X$j + 0" unfolding add_left_cancel f_def by (rule setsum_0', simp)
finally have f: "(∑x∈UNIV. f x *⇩R X $ x) = X$j" by simp
have the_f: "(THE f. ∀i. X $ j $ i = (∑x∈UNIV. f x * X $ x $ i)) = f"
proof (rule the_equality)
show "∀i. X $ j $ i = (∑x∈UNIV. f x * X $ x $ i)" using f unfolding vec_eq_iff unfolding setsum_component by simp
fix fa assume "∀i. X $ j $ i = (∑x∈UNIV. fa x * X $ x $ i)"
hence "∀i. X $ j $ i = (∑x∈UNIV. fa x *⇩R X $ x) $ i" unfolding setsum_component by simp
hence fa: "X $ j = (∑x∈UNIV. fa x *⇩R X $ x)" unfolding vec_eq_iff .
show "fa = f" using basis_combination_unique[OF basis_X] fa f by simp
qed
show "(THE f. ∀i. X $ j $ i = (∑x∈UNIV. f x * X $ x $ i)) j = 1" unfolding the_f f_def by simp
fix i assume i_not_j: "i ≠ j"
show "(THE f. ∀i. X $ j $ i = (∑x∈UNIV. f x * X $ x $ i)) i = 0" unfolding the_f f_def using i_not_j by simp
qed
text{*Relationships between @{thm "matrix'_def"} and @{thm "matrix_change_of_basis_def"}*}
lemma matrix'_matrix_change_of_basis:
fixes B::"real^'n^'n" and B'::"real^'n^'n" and C::"real^'m^'m" and C'::"real^'m^'m"
assumes basis_B: "is_basis (set_of_vector B)" and basis_B': "is_basis (set_of_vector B')"
and basis_C: "is_basis (set_of_vector C)" and basis_C': "is_basis (set_of_vector C')"
and linear_f: "linear f"
shows "matrix' B' C' f = matrix_change_of_basis C C' ** matrix' B C f ** matrix_change_of_basis B' B"
proof (unfold matrix_eq, clarify)
fix x
obtain v where v: "x=coord B' v" using bij_coord[OF basis_B'] unfolding bij_iff by metis
have "matrix_change_of_basis C C' ** matrix' B C f** matrix_change_of_basis B' B *v (coord B' v)
= matrix_change_of_basis C C' ** matrix' B C f *v (matrix_change_of_basis B' B *v (coord B' v)) " unfolding matrix_vector_mul_assoc ..
also have "... = matrix_change_of_basis C C' ** matrix' B C f *v (coord B v)" unfolding matrix_change_of_basis_works[OF basis_B' basis_B] ..
also have "... = matrix_change_of_basis C C' *v (matrix' B C f *v (coord B v))" unfolding matrix_vector_mul_assoc ..
also have "... = matrix_change_of_basis C C' *v (coord C (f v))" unfolding coord_matrix'[OF basis_B basis_C linear_f] ..
also have "... = coord C' (f v)" unfolding matrix_change_of_basis_works[OF basis_C basis_C'] ..
also have "... = matrix' B' C' f *v coord B' v" unfolding coord_matrix'[OF basis_B' basis_C' linear_f] ..
finally show " matrix' B' C' f *v x = matrix_change_of_basis C C' ** matrix' B C f ** matrix_change_of_basis B' B *v x" unfolding v ..
qed
lemma matrix'_id_eq_matrix_change_of_basis:
fixes X::"real^'n^'n" and Y::"real^'n^'n"
assumes basis_X: "is_basis (set_of_vector X)" and basis_Y: "is_basis (set_of_vector Y)"
shows "matrix' X Y (id) = matrix_change_of_basis X Y"
unfolding matrix'_def matrix_change_of_basis_def unfolding id_def ..
text{*Relationships among @{thm "invertible_lf_def"}, @{thm "matrix_change_of_basis_def"}, @{thm "matrix'_def"} and @{thm "invertible_def"}.*}
lemma matrix_inv_matrix_change_of_basis:
fixes X::"real^'n^'n" and Y::"real^'n^'n"
assumes basis_X: "is_basis (set_of_vector X)" and basis_Y: "is_basis (set_of_vector Y)"
shows"matrix_change_of_basis Y X = matrix_inv (matrix_change_of_basis X Y)"
proof (rule matrix_inv_unique[symmetric])
have linear_id: "linear id" by (metis linear_id)
have "(matrix_change_of_basis Y X) ** (matrix_change_of_basis X Y) = (matrix' Y X id) ** (matrix' X Y id)"
unfolding matrix'_id_eq_matrix_change_of_basis[OF basis_X basis_Y]
unfolding matrix'_id_eq_matrix_change_of_basis[OF basis_Y basis_X] ..
also have "... = matrix' X X (id o id)" using matrix'_compose[OF basis_X basis_Y basis_X linear_id linear_id] ..
also have "... = matrix_change_of_basis X X" using matrix'_id_eq_matrix_change_of_basis[OF basis_X basis_X] unfolding o_def id_def .
also have "... = mat 1" using matrix_change_of_basis_mat_1[OF basis_X] .
finally show "matrix_change_of_basis Y X ** matrix_change_of_basis X Y = mat 1" .
have "(matrix_change_of_basis X Y) ** (matrix_change_of_basis Y X) = (matrix' X Y id) ** (matrix' Y X id)"
unfolding matrix'_id_eq_matrix_change_of_basis[OF basis_X basis_Y]
unfolding matrix'_id_eq_matrix_change_of_basis[OF basis_Y basis_X] ..
also have "... = matrix' Y Y (id o id)" using matrix'_compose[OF basis_Y basis_X basis_Y linear_id linear_id] ..
also have "... = matrix_change_of_basis Y Y" using matrix'_id_eq_matrix_change_of_basis[OF basis_Y basis_Y] unfolding o_def id_def .
also have "... = mat 1" using matrix_change_of_basis_mat_1[OF basis_Y] .
finally show "matrix_change_of_basis X Y ** matrix_change_of_basis Y X = mat 1" .
qed
corollary invertible_matrix_change_of_basis:
fixes X::"real^'n^'n" and Y::"real^'n^'n"
assumes basis_X: "is_basis (set_of_vector X)" and basis_Y: "is_basis (set_of_vector Y)"
shows "invertible (matrix_change_of_basis X Y)"
by (metis basis_X basis_Y invertible_left_inverse linear_id matrix'_id_eq_matrix_change_of_basis matrix'_matrix_change_of_basis matrix_change_of_basis_mat_1)
lemma invertible_lf_imp_invertible_matrix':
assumes "invertible_lf f" and basis_X: "is_basis (set_of_vector X)" and basis_Y: "is_basis (set_of_vector Y)"
shows "invertible (matrix' X Y f)"
by (metis (lifting) assms(1) basis_X basis_Y invertible_lf_def invertible_lf_imp_invertible_matrix
invertible_matrix_change_of_basis invertible_mult is_basis_cart_basis' matrix'_eq_matrix matrix'_matrix_change_of_basis)
lemma invertible_matrix'_imp_invertible_lf:
assumes "invertible (matrix' X Y f)" and basis_X: "is_basis (set_of_vector X)"
and linear_f: "linear f" and basis_Y: "is_basis (set_of_vector Y)"
shows "invertible_lf f"
by (metis assms(1) basis_X basis_Y id_o invertible_matrix_change_of_basis
invertible_matrix_iff_invertible_lf' invertible_mult is_basis_cart_basis' linear_f linear_id
matrix'_compose matrix'_eq_matrix matrix'_id_eq_matrix_change_of_basis o_id)
lemma invertible_matrix_is_change_of_basis:
assumes invertible_P: "invertible P" and basis_X: "is_basis (set_of_vector X)"
shows "∃!Y. matrix_change_of_basis Y X = P ∧ is_basis (set_of_vector Y)"
proof (auto)
show "∃Y. matrix_change_of_basis Y X = P ∧ is_basis (set_of_vector Y)"
proof -
fix i j
obtain f where P: "P = matrix' X X f" and linear_f: "linear f" using exists_linear_eq_matrix'[OF basis_X basis_X, of P] by blast
show ?thesis
proof (rule exI[of _ "χ j. f (X$j)"], rule conjI)
show "matrix_change_of_basis (χ j. f (X $ j)) X = P" unfolding matrix_change_of_basis_def P matrix'_def by vector
have invertible_f: "invertible_lf f" using invertible_matrix'_imp_invertible_lf[OF _ basis_X linear_f basis_X] using invertible_P unfolding P by simp
have rw: "set_of_vector (χ j. f (X $ j)) = f`(set_of_vector X)" unfolding set_of_vector_def by auto
show "is_basis (set_of_vector (χ j. f (X $ j)))" unfolding rw using basis_image_linear[OF invertible_f basis_X] .
qed
qed
fix Y Z
assume basis_Y:"is_basis (set_of_vector Y)" and eq: "matrix_change_of_basis Z X = matrix_change_of_basis Y X" and basis_Z: "is_basis (set_of_vector Z)"
have ZY_coord: "∀i. coord X (Z$i) = coord X (Y$i)" using eq unfolding matrix_change_of_basis_def unfolding vec_eq_iff by vector
show "Y=Z" by (vector, metis ZY_coord coord_eq[OF basis_X])
qed
text{*Equivalent Matrices*}
text{*Next definition follows the one presented in Modern Algebra by Seth Warner.*}
definition "equivalent_matrices A B = (∃P Q. invertible P ∧ invertible Q ∧ B = (matrix_inv P)**A**Q)"
lemma exists_basis: "∃X::real^'n^'n. is_basis (set_of_vector X)" using is_basis_cart_basis' by auto
lemma equivalent_implies_exist_matrix':
assumes equivalent: "equivalent_matrices A B"
shows "∃X Y X' Y' f::real^'n=>real^'m.
linear f ∧ matrix' X Y f = A ∧ matrix' X' Y' f = B ∧ is_basis (set_of_vector X) ∧ is_basis (set_of_vector Y) ∧ is_basis (set_of_vector X') ∧ is_basis (set_of_vector Y')"
proof -
obtain X::"real^'n^'n" where X: "is_basis (set_of_vector X)" using exists_basis by blast
obtain Y::"real^'m^'m" where Y: "is_basis (set_of_vector Y)" using exists_basis by blast
obtain P Q where B_PAQ: "B=(matrix_inv P)**A**Q" and inv_P: "invertible P" and inv_Q: "invertible Q" using equivalent unfolding equivalent_matrices_def by auto
obtain f where f_A: "matrix' X Y f = A" and linear_f: "linear f" using exists_linear_eq_matrix'[OF X Y] by auto
obtain X'::"real^'n^'n" where X': "is_basis (set_of_vector X')" and Q:"matrix_change_of_basis X' X = Q" using invertible_matrix_is_change_of_basis[OF inv_Q X] by fast
obtain Y'::"real^'m^'m" where Y': "is_basis (set_of_vector Y')" and P: "matrix_change_of_basis Y' Y = P" using invertible_matrix_is_change_of_basis[OF inv_P Y] by fast
have matrix_inv_P: "matrix_change_of_basis Y Y' = matrix_inv P" using matrix_inv_matrix_change_of_basis[OF Y' Y] P by simp
have "matrix' X' Y' f = matrix_change_of_basis Y Y' ** matrix' X Y f ** matrix_change_of_basis X' X" using matrix'_matrix_change_of_basis[OF X X' Y Y' linear_f] .
also have "... = (matrix_inv P) ** A ** Q" unfolding matrix_inv_P f_A Q ..
also have "... = B" using B_PAQ ..
finally show ?thesis using f_A X X' Y Y' linear_f by fast
qed
lemma exist_matrix'_implies_equivalent:
assumes A: "matrix' X Y f = A"
and B: "matrix' X' Y' f = B"
and X: "is_basis (set_of_vector X)"
and Y: "is_basis (set_of_vector Y)"
and X': "is_basis (set_of_vector X')"
and Y': "is_basis (set_of_vector Y')"
and linear_f: "linear f"
shows "equivalent_matrices A B"
proof (unfold equivalent_matrices_def, rule exI[of _ "matrix_change_of_basis Y' Y"], rule exI[of _ "matrix_change_of_basis X' X"], auto)
have inv: "matrix_change_of_basis Y Y' = matrix_inv (matrix_change_of_basis Y' Y)" using matrix_inv_matrix_change_of_basis[OF Y' Y] .
show "invertible (matrix_change_of_basis Y' Y)" using invertible_matrix_change_of_basis[OF Y' Y] .
show "invertible (matrix_change_of_basis X' X)" using invertible_matrix_change_of_basis[OF X' X] .
have "B = matrix' X' Y' f" using B ..
also have "... = matrix_change_of_basis Y Y' ** matrix' X Y f ** matrix_change_of_basis X' X" using matrix'_matrix_change_of_basis[OF X X' Y Y' linear_f] .
finally show "B = matrix_inv (matrix_change_of_basis Y' Y) ** A ** matrix_change_of_basis X' X" unfolding inv unfolding A .
qed
corollary equivalent_iff_exist_matrix':
shows "equivalent_matrices A B <-> (∃X Y X' Y' f::real^'n=>real^'m.
linear f ∧ matrix' X Y f = A ∧ matrix' X' Y' f = B ∧ is_basis (set_of_vector X) ∧ is_basis (set_of_vector Y) ∧ is_basis (set_of_vector X') ∧ is_basis (set_of_vector Y'))"
by (rule, auto simp add: exist_matrix'_implies_equivalent equivalent_implies_exist_matrix')
text{*Similar matrices*}
definition similar_matrices :: "'a::{semiring_1}^'n^'n => 'a::{semiring_1}^'n^'n => bool"
where "similar_matrices A B = (∃P. invertible P ∧ B=(matrix_inv P)**A**P)"
lemma similar_implies_exist_matrix':
fixes A B::"real^'n^'n"
assumes similar: "similar_matrices A B"
shows "∃X Y f. linear f ∧ matrix' X X f = A ∧ matrix' Y Y f = B ∧ is_basis (set_of_vector X) ∧ is_basis (set_of_vector Y)"
proof -
obtain P where inv_P: "invertible P" and B_PAP: "B=(matrix_inv P)**A**P" using similar unfolding similar_matrices_def by blast
obtain X::"real^'n^'n" where X: "is_basis (set_of_vector X)" using exists_basis by blast
obtain f where linear_f: "linear f" and A: "matrix' X X f = A" using exists_linear_eq_matrix'[OF X X] by blast
obtain Y::"real^'n^'n" where Y: "is_basis (set_of_vector Y)" and P: "P = matrix_change_of_basis Y X" using invertible_matrix_is_change_of_basis[OF inv_P X] by fast
have P': "matrix_inv P = matrix_change_of_basis X Y" by (metis (lifting) P X Y matrix_inv_matrix_change_of_basis)
have "B = (matrix_inv P)**A**P" using B_PAP .
also have "... = matrix_change_of_basis X Y ** matrix' X X f ** P " unfolding P' A ..
also have "... = matrix_change_of_basis X Y ** matrix' X X f ** matrix_change_of_basis Y X" unfolding P ..
also have "... = matrix' Y Y f" using matrix'_matrix_change_of_basis[OF X Y X Y linear_f] by simp
finally show ?thesis using X Y A linear_f by fast
qed
lemma exist_matrix'_implies_similar:
fixes A B::"real^'n^'n"
assumes linear_f: "linear f" and A: "matrix' X X f = A" and B: "matrix' Y Y f = B" and X: "is_basis (set_of_vector X)" and Y: "is_basis (set_of_vector Y)"
shows "similar_matrices A B"
proof (unfold similar_matrices_def, rule exI[of _ "matrix_change_of_basis Y X"], rule conjI)
have "B=matrix' Y Y f" using B ..
also have "... = matrix_change_of_basis X Y ** matrix' X X f ** matrix_change_of_basis Y X" using matrix'_matrix_change_of_basis[OF X Y X Y linear_f] by simp
also have "... = matrix_inv (matrix_change_of_basis Y X) ** A ** matrix_change_of_basis Y X" unfolding A matrix_inv_matrix_change_of_basis[OF Y X] ..
finally show "B = matrix_inv (matrix_change_of_basis Y X) ** A ** matrix_change_of_basis Y X" .
show "invertible (matrix_change_of_basis Y X)" using invertible_matrix_change_of_basis[OF Y X] .
qed
corollary similar_iff_exist_matrix':
fixes A B::"real^'n^'n"
shows "similar_matrices A B <-> (∃X Y f. linear f ∧ matrix' X X f = A ∧ matrix' Y Y f = B ∧ is_basis (set_of_vector X) ∧ is_basis (set_of_vector Y))"
by (rule, auto simp add: exist_matrix'_implies_similar similar_implies_exist_matrix')
end