Theory Jordan_Normal_Form.Char_Poly
section ‹Characteristic Polynomial›
text ‹We define eigenvalues, eigenvectors, and the characteristic polynomial. We further prove
that the eigenvalues are exactly the roots of the characteristic polynomial.
Finally, we apply the fundamental theorem of algebra to show that the characteristic polynomial
of a complex matrix can always be represented as product of linear factors $x - a$.›
theory Char_Poly
imports
Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
Polynomial_Interpolation.Missing_Polynomial
Polynomial_Interpolation.Ring_Hom_Poly
Determinant
Complex_Main
begin
definition eigenvector :: "'a :: comm_ring_1 mat ⇒ 'a vec ⇒ 'a ⇒ bool" where
"eigenvector A v k = (v ∈ carrier_vec (dim_row A) ∧ v ≠ 0⇩v (dim_row A) ∧ A *⇩v v = k ⋅⇩v v)"
lemma eigenvector_pow: assumes A: "A ∈ carrier_mat n n"
and ev: "eigenvector A v (k :: 'a :: comm_ring_1)"
shows "A ^⇩m i *⇩v v = k^i ⋅⇩v v"
proof -
let ?G = "monoid_vec TYPE ('a) n"
from A have dim: "dim_row A = n" by auto
from ev[unfolded eigenvector_def dim]
have v: "v ∈ carrier_vec n" and Av: "A *⇩v v = k ⋅⇩v v" by auto
interpret v: comm_group ?G by (rule comm_group_vec)
show ?thesis
proof (induct i)
case 0
show ?case using v dim by simp
next
case (Suc i)
define P where "P = A ^⇩m i"
have P: "P ∈ carrier_mat n n" using A unfolding P_def by simp
have "A ^⇩m Suc i = P * A" unfolding P_def by simp
also have "… *⇩v v = P *⇩v (A *⇩v v)" using P A v by simp
also have "A *⇩v v = k ⋅⇩v v" by (rule Av)
also have "P *⇩v (k ⋅⇩v v) = k ⋅⇩v (P *⇩v v)"
by (rule eq_vecI, insert v P, auto)
also have "(P *⇩v v) = (k ^ i) ⋅⇩v v" unfolding P_def by (rule Suc)
also have "k ⋅⇩v ((k ^ i) ⋅⇩v v) = (k * k ^ i) ⋅⇩v v"
by (rule eq_vecI, insert v, auto)
also have "k * k ^ i = k ^ (Suc i)" by auto
finally show ?case .
qed
qed
definition eigenvalue :: "'a :: comm_ring_1 mat ⇒ 'a ⇒ bool" where
"eigenvalue A k = (∃ v. eigenvector A v k)"
definition char_matrix :: "'a :: field mat ⇒ 'a ⇒ 'a mat" where
"char_matrix A e = A + ((-e) ⋅⇩m (1⇩m (dim_row A)))"
lemma char_matrix_closed[simp]: "A ∈ carrier_mat n n ⟹ char_matrix A e ∈ carrier_mat n n"
unfolding char_matrix_def by auto
lemma eigenvector_char_matrix: assumes A: "(A :: 'a :: field mat) ∈ carrier_mat n n"
shows "eigenvector A v e = (v ∈ carrier_vec n ∧ v ≠ 0⇩v n ∧ char_matrix A e *⇩v v = 0⇩v n)"
proof -
from A have dim: "dim_row A = n" "dim_col A = n" by auto
{
assume v: "v ∈ carrier_vec n"
hence dimv: "dim_vec v = n" by auto
have "(A *⇩v v = e ⋅⇩v v) = (A *⇩v v + (-e) ⋅⇩v v = 0⇩v n)" (is "?id1 = ?id2")
proof
assume ?id1
from arg_cong[OF this, of "λ w. w + (-e) ⋅⇩v v"]
show ?id2 using A v by auto
next
assume ?id2
have "A *⇩v v + - e ⋅⇩v v + e ⋅⇩v v = A *⇩v v" using A v by auto
from arg_cong[OF ‹?id2›, of "λ w. w + e ⋅⇩v v", unfolded this]
show ?id1 using A v by simp
qed
also have "(A *⇩v v + (-e) ⋅⇩v v) = char_matrix A e *⇩v v" unfolding char_matrix_def
by (rule eq_vecI, insert v A dim, auto simp: add_scalar_prod_distrib[of _ n])
finally have "(A *⇩v v = e ⋅⇩v v) = (char_matrix A e *⇩v v = 0⇩v n)" .
}
thus ?thesis unfolding eigenvector_def dim by blast
qed
lemma eigenvalue_char_matrix: assumes A: "(A :: 'a :: field mat) ∈ carrier_mat n n"
shows "eigenvalue A e = (∃ v. v ∈ carrier_vec n ∧ v ≠ 0⇩v n ∧ char_matrix A e *⇩v v = 0⇩v n)"
unfolding eigenvalue_def eigenvector_char_matrix[OF A] ..
definition find_eigenvector :: "'a::field mat ⇒ 'a ⇒ 'a vec" where
"find_eigenvector A e =
find_base_vector (fst (gauss_jordan (char_matrix A e) (0⇩m (dim_row A) 0)))"
lemma find_eigenvector: assumes A: "A ∈ carrier_mat n n"
and ev: "eigenvalue A e"
shows "eigenvector A (find_eigenvector A e) e"
proof -
define B where "B = char_matrix A e"
from ev[unfolded eigenvalue_char_matrix[OF A]] obtain v where
v: "v ∈ carrier_vec n" "v ≠ 0⇩v n" and Bv: "B *⇩v v = 0⇩v n" unfolding B_def by auto
have B: "B ∈ carrier_mat n n" using A unfolding B_def by simp
let ?z = "0⇩m (dim_row A) 0"
obtain C D where gauss: "gauss_jordan B ?z = (C,D)" by force
define w where "w = find_base_vector C"
have res: "find_eigenvector A e = w" unfolding w_def find_eigenvector_def Let_def gauss B_def[symmetric]
by simp
have "?z ∈ carrier_mat n 0" using A by auto
note gauss_0 = gauss_jordan[OF B this gauss]
hence C: "C ∈ carrier_mat n n" by auto
from gauss_0(1)[OF v(1)] Bv have Cv: "C *⇩v v = 0⇩v n" by auto
{
assume C: "C = 1⇩m n"
have False using id Cv v unfolding C by auto
}
hence C1: "C ≠ 1⇩m n" by auto
from find_base_vector_not_1[OF gauss_jordan_row_echelon[OF B gauss] C C1]
have w: "w ∈ carrier_vec n" "w ≠ 0⇩v n" and id: "C *⇩v w = 0⇩v n" unfolding w_def by auto
from gauss_0(1)[OF w(1)] id have Bw: "B *⇩v w = 0⇩v n" by simp
from w Bw have "eigenvector A w e"
unfolding eigenvector_char_matrix[OF A] B_def by auto
thus ?thesis unfolding res .
qed
lemma eigenvalue_imp_nonzero_dim: assumes "A ∈ carrier_mat n n"
and "eigenvalue A ev"
shows "n > 0"
proof (cases n)
case 0
from assms obtain v where "eigenvector A v ev" unfolding eigenvalue_def by auto
from this[unfolded eigenvector_def] assms 0
have "v ∈ carrier_vec 0" "v ≠ 0⇩v 0" by auto
hence False by auto
thus ?thesis by auto
qed simp
lemma eigenvalue_det: assumes A: "(A :: 'a :: field mat) ∈ carrier_mat n n" shows
"eigenvalue A e = (det (char_matrix A e) = 0)"
proof -
from A have cA: "char_matrix A e ∈ carrier_mat n n" by auto
show ?thesis
unfolding eigenvalue_char_matrix[OF A]
unfolding id det_0_negate[OF cA] det_0_iff_vec_prod_zero[OF cA]
eigenvalue_def by auto
qed
definition char_poly_matrix :: "'a :: comm_ring_1 mat ⇒ 'a poly mat" where
"char_poly_matrix A = (([:0,1:] ⋅⇩m 1⇩m (dim_row A)) + map_mat (λ a. [: - a :]) A)"
lemma char_poly_matrix_closed[simp]: "A ∈ carrier_mat n n ⟹ char_poly_matrix A ∈ carrier_mat n n"
unfolding char_poly_matrix_def by auto
definition char_poly :: "'a :: comm_ring_1 mat ⇒ 'a poly" where
"char_poly A = (det (char_poly_matrix A))"
lemmas char_poly_defs = char_poly_def char_poly_matrix_def
lemma (in comm_ring_hom) char_poly_matrix_hom: assumes A: "A ∈ carrier_mat n n"
shows "char_poly_matrix (mat⇩h A) = map_mat (map_poly hom) (char_poly_matrix A)"
unfolding char_poly_defs
by (rule eq_matI, insert A, auto simp: smult_mat_def hom_distribs)
lemma (in comm_ring_hom) char_poly_hom: assumes A: "A ∈ carrier_mat n n"
shows "char_poly (map_mat hom A) = map_poly hom (char_poly A)"
proof -
interpret map_poly_hom: map_poly_comm_ring_hom hom..
show ?thesis
unfolding char_poly_def map_poly_hom.hom_det[symmetric] char_poly_matrix_hom[OF A] ..
qed
context inj_comm_ring_hom
begin
lemma eigenvector_hom: assumes A: "A ∈ carrier_mat n n"
and ev: "eigenvector A v ev"
shows "eigenvector (mat⇩h A) (vec⇩h v) (hom ev)"
proof -
let ?A = "mat⇩h A"
let ?v = "vec⇩h v"
let ?ev = "hom ev"
from ev[unfolded eigenvector_def] A
have v: "v ∈ carrier_vec n" "v ≠ 0⇩v n" "A *⇩v v = ev ⋅⇩v v" by auto
from v(1) have v1: "?v ∈ carrier_vec n" by simp
from v(1-2) obtain i where "i < n" and "v $ i ≠ 0" by force
with v(1) have "?v $ i ≠ 0" by auto
hence v2: "?v ≠ 0⇩v n" using ‹i < n› v(1) by force
from arg_cong[OF v(3), of "vec⇩h", unfolded mult_mat_vec_hom[OF A v(1)] vec_hom_smult]
have v3: "?A *⇩v ?v = ?ev ⋅⇩v ?v" .
from v1 v2 v3
show ?thesis unfolding eigenvector_def using A by auto
qed
lemma eigenvalue_hom: assumes A: "A ∈ carrier_mat n n"
and ev: "eigenvalue A ev"
shows "eigenvalue (mat⇩h A) (hom ev)"
using eigenvector_hom[OF A, of _ ev] ev
unfolding eigenvalue_def by auto
lemma eigenvector_hom_rev: assumes A: "A ∈ carrier_mat n n"
and ev: "eigenvector (mat⇩h A) (vec⇩h v) (hom ev)"
shows "eigenvector A v ev"
proof -
let ?A = "mat⇩h A"
let ?v = "vec⇩h v"
let ?ev = "hom ev"
from ev[unfolded eigenvector_def] A
have v: "v ∈ carrier_vec n" "?v ≠ 0⇩v n" "?A *⇩v ?v = ?ev ⋅⇩v ?v" by auto
from v(1-2) obtain i where "i < n" and "v $ i ≠ 0" by force
with v(1) have "v $ i ≠ 0" by auto
hence v2: "v ≠ 0⇩v n" using ‹i < n› v(1) by force
from vec_hom_inj[OF v(3)[folded mult_mat_vec_hom[OF A v(1)] vec_hom_smult]]
have v3: "A *⇩v v = ev ⋅⇩v v" .
from v(1) v2 v3
show ?thesis unfolding eigenvector_def using A by auto
qed
end
lemma poly_det_cong: assumes A: "A ∈ carrier_mat n n"
and B: "B ∈ carrier_mat n n"
and poly: "⋀ i j. i < n ⟹ j < n ⟹ poly (B $$ (i,j)) k = A $$ (i,j)"
shows "poly (det B) k = det A"
proof -
show ?thesis
unfolding det_def'[OF A] det_def'[OF B] poly_sum poly_mult poly_prod
proof (rule sum.cong[OF refl])
fix x
assume x: "x ∈ {p. p permutes {0..<n}}"
let ?l = "∏ka = 0..<n. poly (B $$ (ka, x ka)) k"
let ?r = "∏i = 0..<n. A $$ (i, x i)"
have id: "?l = ?r"
by (rule prod.cong[OF refl poly], insert x, auto)
show "poly (signof x) k * ?l = signof x * ?r"
by (cases x rule: sign_cases) (simp_all add: id)
qed
qed
lemma char_poly_matrix: assumes A: "(A :: 'a :: field mat) ∈ carrier_mat n n"
shows "poly (char_poly A) k = det (- (char_matrix A k))" unfolding char_poly_def
by (rule poly_det_cong[of _ n], insert A, auto simp: char_poly_matrix_def char_matrix_def)
lemma eigenvalue_root_char_poly: assumes A: "(A :: 'a :: field mat) ∈ carrier_mat n n"
shows "eigenvalue A k ⟷ poly (char_poly A) k = 0"
unfolding eigenvalue_det[OF A] char_poly_matrix[OF A]
by (subst det_0_negate[of _ n], insert A, auto)
context
fixes A :: "'a :: comm_ring_1 mat" and n :: nat
assumes A: "A ∈ carrier_mat n n"
and ut: "upper_triangular A"
begin
lemma char_poly_matrix_upper_triangular: "upper_triangular (char_poly_matrix A)"
using A ut unfolding upper_triangular_def char_poly_matrix_def by auto
lemma char_poly_upper_triangular:
"char_poly A = (∏ a ← diag_mat A. [:- a, 1:])"
proof -
from A have cA: "char_poly_matrix A ∈ carrier_mat n n" by simp
show ?thesis
unfolding char_poly_def det_upper_triangular [OF char_poly_matrix_upper_triangular cA]
by (rule arg_cong[where f = prod_list], unfold list_eq_iff_nth_eq, insert cA A, auto simp: diag_mat_def
char_poly_matrix_def)
qed
end
lemma map_poly_mult: assumes A: "A ∈ carrier_mat nr n"
and B: "B ∈ carrier_mat n nc"
shows
"map_mat (λ a. [: a :]) (A * B) = map_mat (λ a. [: a :]) A * map_mat (λ a. [: a :]) B" (is "?id")
"map_mat (λ a. [: a :] * p) (A * B) = map_mat (λ a. [: a :] * p) A * map_mat (λ a. [: a :]) B" (is "?left")
"map_mat (λ a. [: a :] * p) (A * B) = map_mat (λ a. [: a :]) A * map_mat (λ a. [: a :] * p) B" (is "?right")
proof -
from A B have dim: "dim_row A = nr" "dim_col A = n" "dim_row B = n" "dim_col B = nc" by auto
{
fix i j
have "i < nr ⟹ j < nc ⟹
row (map_mat (λa. [:a:]) A) i ∙ col (map_mat (λa. [:a:]) B) j = [:(row A i ∙ col B j):]"
unfolding scalar_prod_def
by (auto simp: dim ac_simps, induct n, auto)
} note id = this
{
fix i j
have "i < nr ⟹ j < nc ⟹
[:(row A i ∙ col B j):] * p = row (map_mat (λ a. [: a :] * p) A) i ∙ col (map_mat (λa. [:a:]) B) j"
unfolding scalar_prod_def
by (auto simp: dim ac_simps smult_sum)
} note left = this
{
fix i j
have "i < nr ⟹ j < nc ⟹
[:(row A i ∙ col B j):] * p = row (map_mat (λ a. [: a :]) A) i ∙ col (map_mat (λa. [:a:] * p) B) j"
unfolding scalar_prod_def
by (auto simp: dim ac_simps smult_sum)
} note right = this
show ?id
by (rule eq_matI, insert id, auto simp: dim)
show ?left
by (rule eq_matI, insert left, auto simp: dim)
show ?right
by (rule eq_matI, insert right, auto simp: dim)
qed
lemma char_poly_similar: assumes "similar_mat A (B :: 'a :: comm_ring_1 mat)"
shows "char_poly A = char_poly B"
proof -
from similar_matD[OF assms] obtain n P Q where
carr: "{A, B, P, Q} ⊆ carrier_mat n n" (is "_ ⊆ ?C")
and PQ: "P * Q = 1⇩m n"
and AB: "A = P * B * Q" by auto
hence A: "A ∈ ?C" and B: "B ∈ ?C" and P: "P ∈ ?C" and Q: "Q ∈ ?C" by auto
let ?m = "λ a. [: -a :]"
let ?P = "map_mat (λ a. [: a :]) P"
let ?Q = "map_mat (λ a. [: a :]) Q"
let ?B = "map_mat ?m B"
let ?I = "map_mat (λ a. [: a :]) (1⇩m n)"
let ?XI = "[:0, 1:] ⋅⇩m 1⇩m n"
from A B have dim: "dim_row A = n" "dim_row B = n" by auto
have cong: "⋀ x y z. x = y ⟹ x * z = y * z" by auto
have id: "?m = (λ a :: 'a. [: a :] * [: -1 :])" by (intro ext, auto)
have "char_poly A = det (?XI + map_mat (λa. [:- a:]) (P * B * Q))" unfolding
char_poly_defs dim
by (simp add: AB)
also have "?XI = ?P * ?XI * ?Q" (is "_ = ?left")
proof -
have "?P * ?XI = [:0, 1:] ⋅⇩m (?P * 1⇩m n)"
by (rule mult_smult_distrib[of _ n n _ n], insert P, auto)
also have "?P * 1⇩m n = ?P" using P by simp
also have "([: 0, 1:] ⋅⇩m ?P) * ?Q = [: 0, 1:] ⋅⇩m (?P * ?Q)"
by (rule mult_smult_assoc_mat, insert P Q, auto)
also have "?P * ?Q = ?I" unfolding PQ[symmetric]
by (rule map_poly_mult[symmetric, OF P Q])
also have "[: 0, 1:] ⋅⇩m ?I = ?XI"
by rule auto
finally show ?thesis ..
qed
also have "map_mat ?m (P * B * Q) = ?P * ?B * ?Q" (is "_ = ?right")
unfolding id
by (subst map_poly_mult[OF mult_carrier_mat[OF P B] Q],
subst map_poly_mult(3)[OF P B], simp)
also have "?left + ?right = (?P * ?XI + ?P * ?B) * ?Q"
by (rule add_mult_distrib_mat[symmetric, of _ n n], insert B P Q, auto)
also have "?P * ?XI + ?P * ?B = ?P * (?XI + ?B)"
by (rule mult_add_distrib_mat[symmetric, of _ n n], insert B P Q, auto)
also have "det (?P * (?XI + ?B) * ?Q) = det ?P * det (?XI + ?B) * det ?Q"
by (rule trans[OF det_mult[of _ n] cong[OF det_mult]], insert P Q B, auto)
also have "… = (det ?P * det ?Q) * det (?XI + ?B)" by (simp add: ac_simps)
also have "det (?XI + ?B) = char_poly B" unfolding char_poly_defs dim by simp
also have "det ?P * det ?Q = det (?P * ?Q)"
by (rule det_mult[symmetric], insert P Q, auto)
also have "?P * ?Q = ?I" unfolding PQ[symmetric]
by (rule map_poly_mult[symmetric, OF P Q])
also have "det … = prod_list (diag_mat ?I)"
by (rule det_upper_triangular[of _ n], auto)
also have "… = 1" unfolding prod_list_diag_prod
by (rule prod.neutral) simp
finally show ?thesis by simp
qed
lemma degree_signof_mult[simp]: "degree (signof p * q) = degree q"
by (cases p rule: sign_cases) simp_all
lemma degree_monic_char_poly: assumes A: "A ∈ carrier_mat n n"
shows "degree (char_poly A) = n ∧ coeff (char_poly A) n = 1"
proof -
from A have A': "[:0, 1:] ⋅⇩m 1⇩m (dim_row A) + map_mat (λa. [:- a:]) A ∈ carrier_mat n n" by auto
from A have dA: "dim_row A = n" by simp
show ?thesis
unfolding char_poly_defs det_def'[OF A']
proof (rule degree_lcoeff_sum[of _ id], auto simp: finite_permutations permutes_id dA)
have both: "degree (∏i = 0..<n. ([:0, 1:] ⋅⇩m 1⇩m n + map_mat (λa. [:- a:]) A) $$ (i, i)) = n ∧
coeff (∏i = 0..<n. ([:0, 1:] ⋅⇩m 1⇩m n + map_mat (λa. [:- a:]) A) $$ (i, i)) n = 1"
by (rule degree_prod_monic, insert A, auto)
from both show "degree (∏i = 0..<n. ([:0, 1:] ⋅⇩m 1⇩m n + map_mat (λa. [:- a:]) A) $$ (i, i)) = n" ..
from both show "coeff (∏i = 0..<n. ([:0, 1:] ⋅⇩m 1⇩m n + map_mat (λa. [:- a:]) A) $$ (i, i)) n = 1" ..
next
fix p
assume p: "p permutes {0..<n}"
and "p ≠ id"
then obtain i where i: "i < n" and pi: "p i ≠ i"
by (metis atLeastLessThan_iff order_refl permutes_natset_le)
show "degree (∏i = 0..<n. ([:0, 1:] ⋅⇩m 1⇩m n + map_mat (λa. [:- a:]) A) $$ (i, p i)) < n"
by (rule degree_prod_sum_lt_n[OF _ i], insert p i pi A, auto)
qed
qed
lemma char_poly_factorized: fixes A :: "complex mat"
assumes A: "A ∈ carrier_mat n n"
shows "∃ as. char_poly A = (∏ a ← as. [:- a, 1:]) ∧ length as = n"
proof -
let ?p = "char_poly A"
from fundamental_theorem_algebra_factorized[of ?p] obtain as
where "Polynomial.smult (coeff ?p (degree ?p)) (∏a←as. [:- a, 1:]) = ?p" by blast
also have "coeff ?p (degree ?p) = 1" using degree_monic_char_poly[OF A] by simp
finally have cA: "?p = (∏a←as. [:- a, 1:])" by simp
from degree_monic_char_poly[OF A] have "degree ?p = n" ..
with degree_linear_factors[of uminus as, folded cA] have "length as = n" by auto
with cA show ?thesis by blast
qed
lemma char_poly_four_block_zeros_col: assumes A1: "A1 ∈ carrier_mat 1 1"
and A2: "A2 ∈ carrier_mat 1 n" and A3: "A3 ∈ carrier_mat n n"
shows "char_poly (four_block_mat A1 A2 (0⇩m n 1) A3) = char_poly A1 * char_poly A3"
(is "char_poly ?A = ?cp1 * ?cp3")
proof -
let ?cm = "λ A. [:0, 1:] ⋅⇩m 1⇩m (dim_row A) +
map_mat (λa. [:- a:]) A"
let ?B2 = "map_mat (λa. [:- a:]) A2"
have "char_poly ?A = det (?cm ?A)"
unfolding char_poly_defs using A1 A3 by simp
also have "?cm ?A = four_block_mat (?cm A1) ?B2 (0⇩m n 1) (?cm A3)"
by (rule eq_matI, insert A1 A2 A3, auto simp: one_poly_def)
also have "det … = det (?cm A1) * det (?cm A3)"
by (rule det_four_block_mat_lower_left_zero_col[OF _ _ refl], insert A1 A2 A3, auto)
also have "… = ?cp1 * ?cp3" unfolding char_poly_defs ..
finally show ?thesis .
qed
lemma char_poly_transpose_mat[simp]: assumes A: "A ∈ carrier_mat n n"
shows "char_poly (transpose_mat A) = char_poly A"
proof -
let ?A = "[:0, 1:] ⋅⇩m 1⇩m (dim_row A) + map_mat (λa. [:- a:]) A"
have A': "?A ∈ carrier_mat n n" using A by auto
show ?thesis unfolding char_poly_defs
by (subst det_transpose[symmetric, OF A'], rule arg_cong[of _ _ det],
insert A, auto)
qed
lemma pderiv_char_poly: fixes A :: "'a :: idom mat"
assumes A: "A ∈ carrier_mat n n"
shows "pderiv (char_poly A) = (∑i < n. char_poly (mat_delete A i i))"
proof -
let ?det = Determinant.det
let ?m = "map_mat (λa. [:- a:])"
let ?lam = "[:0, 1:] ⋅⇩m 1⇩m n :: 'a poly mat"
from A have id: "dim_row A = n" by auto
define mA where "mA = ?m A"
define lam where "lam = ?lam"
let ?sum = "lam + mA"
define Sum where "Sum = ?sum"
have mA: "mA ∈ carrier_mat n n" and
lam: "lam ∈ carrier_mat n n" and
Sum: "Sum ∈ carrier_mat n n"
using A unfolding mA_def Sum_def lam_def by auto
let ?P = "{p. p permutes {0..<n}}"
let ?e = "λ p. (∏i = 0..<n. Sum $$ (i, p i))"
let ?f = "λ p a. signof p * (∏i∈{0..<n} - {a}. Sum $$ (i, p i)) * pderiv (Sum $$ (a, p a))"
let ?g = "λ p a. signof p * (∏i∈{0..<n} - {a}. Sum $$ (i, p i))"
define f where "f = ?f"
define g where "g = ?g"
{
fix p
assume p: "p permutes {0 ..< n}"
have "pderiv (signof p :: 'a poly) = 0"
by (cases p rule: sign_cases) (simp_all add: pderiv_minus)
hence "pderiv (signof p * ?e p) = signof p * pderiv (∏i = 0..<n. Sum $$ (i, p i))"
unfolding pderiv_mult by auto
also have "signof p * pderiv (∏i = 0..<n. Sum $$ (i, p i)) =
(∑a = 0..<n. f p a)"
unfolding pderiv_prod sum_distrib_left f_def by (simp add: ac_simps)
also note calculation
} note to_f = this
{
fix a
assume a: "a < n"
have Psplit: "?P = {p. p permutes {0..<n} ∧ p a = a} ∪ (?P - {p. p a = a})" (is "_ = ?Pa ∪ ?Pz") by auto
{
fix p
assume p: "p permutes {0 ..< n}" "p a ≠ a"
hence "pderiv (Sum $$ (a, p a)) = 0" unfolding Sum_def lam_def mA_def using a p A by auto
hence "f p a = 0" unfolding f_def by auto
} note 0 = this
{
fix p
assume p: "p permutes {0 ..< n}" "p a = a"
hence "pderiv (Sum $$ (a, p a)) = 1" unfolding Sum_def lam_def mA_def using a p A
by (auto simp: pderiv_pCons)
hence "f p a = g p a" unfolding f_def g_def by auto
} note fg = this
let ?n = "n - 1"
from a have n: "Suc ?n = n" by simp
let ?B = "[:0, 1:] ⋅⇩m 1⇩m ?n + ?m (mat_delete A a a)"
have B: "?B ∈ carrier_mat ?n ?n" using A by auto
have "sum (λ p. f p a) ?P = sum (λ p. f p a) ?Pa + sum (λ p. f p a) ?Pz"
by (subst sum.union_disjoint[symmetric], auto simp: finite_permutations Psplit[symmetric])
also have "… = sum (λ p. f p a) ?Pa"
by (subst (2) sum.neutral, insert 0, auto)
also have "… = sum (λ p. g p a) ?Pa"
by (rule sum.cong, auto simp: fg)
also have "… = ?det ?B"
unfolding det_def'[OF B]
unfolding permutation_fix[of a ?n a, unfolded n, OF a a]
unfolding sum.reindex[OF permutation_insert_inj_on[of a ?n a, unfolded n, OF a a]] o_def
proof (rule sum.cong[OF refl])
fix p
let ?Q = "{p. p permutes {0..<?n}}"
assume "p ∈ ?Q"
hence p: "p permutes {0 ..< ?n}" by auto
let ?p = "permutation_insert a a p"
let ?i = "insert_index a"
have sign: "signof ?p = signof p"
unfolding signof_permutation_insert[OF p, unfolded n, OF a a] by simp
show "g (permutation_insert a a p) a = signof p * (∏i = 0..<?n. ?B $$ (i, p i))"
unfolding g_def sign
proof (rule arg_cong[of _ _ "(*) (signof p)"])
have "(∏i∈{0..<n} - {a}. Sum $$ (i, ?p i)) =
prod (($$) Sum) ((λx. (x, ?p x)) ` ({0..<n} - {a}))"
unfolding prod.reindex[OF inj_on_convol_ident, of _ ?p] o_def ..
also have "… = (∏ ii ∈ {(i', ?p i') |i'. i' ∈ {0..<n} - {a}}. Sum $$ ii)"
by (rule prod.cong, auto)
also have "… = prod (($$) Sum) ((λ i. (?i i, ?i (p i))) ` {0 ..< ?n})"
unfolding Determinant.foo[of a ?n a, unfolded n, OF a a p]
by (rule arg_cong[of _ _ "prod _"], auto)
also have "… = prod (λ i. Sum $$ (?i i, ?i (p i))) {0 ..< ?n}"
proof (subst prod.reindex, unfold o_def)
show "inj_on (λi. (?i i, ?i (p i))) {0..<?n}" using insert_index_inj_on[of a]
by (auto simp: inj_on_def)
qed simp
also have "… = (∏i = 0..<?n. ?B $$ (i, p i))"
proof (rule prod.cong[OF refl], rename_tac i)
fix j
assume "j ∈ {0 ..< ?n}"
hence j: "j < ?n" by auto
with p have pj: "p j < ?n" by auto
from j pj have jj: "?i j < n" "?i (p j) < n" by (auto simp: insert_index_def)
let ?jj = "(?i j, ?i (p j))"
note index_adj = mat_delete_index[of _ ?n, unfolded n, OF _ a a j pj]
have "Sum $$ ?jj = lam $$ ?jj + mA $$ ?jj" unfolding Sum_def using jj A lam mA by auto
also have "… = ?B $$ (j, p j)"
unfolding index_adj[OF mA] index_adj[OF lam] using j pj A
by (simp add: mA_def lam_def mat_delete_def)
finally show "Sum $$ ?jj = ?B $$ (j, p j)" .
qed
finally
show "(∏i∈{0..<n} - {a}. Sum $$ (i, ?p i)) = (∏i = 0..<?n. ?B $$ (i, p i))" .
qed
qed
also have "… = char_poly (mat_delete A a a)" unfolding char_poly_def char_poly_matrix_def
using A by simp
also note calculation
} note to_char_poly = this
have "pderiv (char_poly A) = pderiv (?det Sum)"
unfolding char_poly_def char_poly_matrix_def id lam_def mA_def Sum_def by auto
also have "… = sum (λ p. pderiv (signof p * ?e p)) ?P" unfolding det_def'[OF Sum]
pderiv_sum by (rule sum.cong, auto)
also have "… = sum (λ p. (∑a = 0..<n. f p a)) ?P"
by (rule sum.cong[OF refl], subst to_f, auto)
also have "… = (∑a = 0..<n. sum (λ p. f p a) ?P)"
by (rule sum.swap)
also have "… = (∑a <n. char_poly (mat_delete A a a))"
by (rule sum.cong, auto simp: to_char_poly)
finally show ?thesis .
qed
lemma char_poly_0_column: fixes A :: "'a :: idom mat"
assumes 0: "⋀ j. j < n ⟹ A $$ (j,i) = 0"
and A: "A ∈ carrier_mat n n"
and i: "i < n"
shows "char_poly A = monom 1 1 * char_poly (mat_delete A i i)"
proof -
let ?n = "n - 1"
let ?A = "mat_delete A i i"
let ?sum = "[:0, 1:] ⋅⇩m 1⇩m n + map_mat (λa. [:- a:]) A"
define Sum where "Sum = ?sum"
let ?f = "λ j. Sum $$ (j, i) * cofactor Sum j i"
have Sum: "Sum ∈ carrier_mat n n" using A unfolding Sum_def by auto
from A have id: "dim_row A = n" by auto
have "char_poly A = (∑j<n. ?f j)"
unfolding char_poly_def[of A] char_poly_matrix_def
using laplace_expansion_column[OF Sum i] unfolding Sum_def using A by simp
also have "… = ?f i + sum ?f ({..<n} - {i})"
by (rule sum.remove[of _ i], insert i, auto)
also have "… = ?f i"
proof (subst sum.neutral, intro ballI)
fix j
assume "j ∈ {..<n} - {i}"
hence j: "j < n" and ji: "j ≠ i" by auto
show "?f j = 0" unfolding Sum_def using ji j i A 0[OF j] by simp
qed simp
also have "?f i = [:0, 1:] * (cofactor Sum i i)"
unfolding Sum_def using i A 0[OF i] by simp
also have "cofactor Sum i i = det (mat_delete Sum i i)"
unfolding cofactor_def by simp
also have "… = char_poly ?A"
unfolding char_poly_def char_poly_matrix_def Sum_def
proof (rule arg_cong[of _ _ det])
show "mat_delete ?sum i i = [:0, 1:] ⋅⇩m 1⇩m (dim_row ?A) + map_mat (λa. [:- a:]) ?A"
using i A by (auto simp: mat_delete_def)
qed
also have "[:0, 1:] = (monom 1 1 :: 'a poly)" by (rule x_as_monom)
finally show ?thesis .
qed
definition mat_erase :: "'a :: zero mat ⇒ nat ⇒ nat ⇒ 'a mat" where
"mat_erase A i j = Matrix.mat (dim_row A) (dim_col A)
(λ (i',j'). if i' = i ∨ j' = j then 0 else A $$ (i',j'))"
lemma mat_erase_carrier[simp]: "(mat_erase A i j) ∈ carrier_mat nr nc ⟷ A ∈ carrier_mat nr nc"
unfolding mat_erase_def carrier_mat_def by simp
lemma pderiv_char_poly_mat_erase: fixes A :: "'a :: idom mat"
assumes A: "A ∈ carrier_mat n n"
shows "monom 1 1 * pderiv (char_poly A) = (∑i < n. char_poly (mat_erase A i i))"
proof -
show ?thesis unfolding pderiv_char_poly[OF A] sum_distrib_left
proof (rule sum.cong[OF refl])
fix i
assume "i ∈ {..<n}"
hence i: "i < n" by simp
have mA: "mat_erase A i i ∈ carrier_mat n n" using A by simp
show "monom 1 1 * char_poly (mat_delete A i i) = char_poly (mat_erase A i i)"
by (subst char_poly_0_column[OF _ mA i], (insert i A, force simp: mat_erase_def),
rule arg_cong[of _ _ "λ x. f * char_poly x" for f],
auto simp: mat_delete_def mat_erase_def)
qed
qed
end