section ‹Complex matrices› theory Complex_Matrix imports "Jordan_Normal_Form.Matrix" "Jordan_Normal_Form.Conjugate" "Jordan_Normal_Form.Jordan_Normal_Form_Existence" begin subsection ‹Trace of a matrix› definition trace :: "'a::ring mat ⇒ 'a" where "trace A = (∑ i ∈ {0 ..< dim_row A}. A $$ (i,i))" lemma trace_zero [simp]: "trace (0⇩_{m}n n) = 0" by (simp add: trace_def) lemma trace_id [simp]: "trace (1⇩_{m}n) = n" by (simp add: trace_def) lemma trace_comm: fixes A B :: "'a::comm_ring mat" assumes A: "A ∈ carrier_mat n n" and B: "B ∈ carrier_mat n n" shows "trace (A * B) = trace (B * A)" proof (simp add: trace_def) have "(∑i = 0..<n. (A * B) $$ (i, i)) = (∑i = 0..<n. ∑j = 0..<n. A $$ (i,j) * B $$ (j,i))" apply (rule sum.cong) using assms by (auto simp add: scalar_prod_def) also have "… = (∑j = 0..<n. ∑i = 0..<n. A $$ (i,j) * B $$ (j,i))" by (rule sum.swap) also have "… = (∑j = 0..<n. col A j ∙ row B j)" by (metis (no_types, lifting) A B atLeastLessThan_iff carrier_matD index_col index_row scalar_prod_def sum.cong) also have "… = (∑j = 0..<n. row B j ∙ col A j)" apply (rule sum.cong) apply auto apply (subst comm_scalar_prod[where n=n]) apply auto using assms by auto also have "… = (∑j = 0..<n. (B * A) $$ (j, j))" apply (rule sum.cong) using assms by auto finally show "(∑i = 0..<dim_row A. (A * B) $$ (i, i)) = (∑i = 0..<dim_row B. (B * A) $$ (i, i))" using A B by auto qed lemma trace_add_linear: fixes A B :: "'a::comm_ring mat" assumes A: "A ∈ carrier_mat n n" and B: "B ∈ carrier_mat n n" shows "trace (A + B) = trace A + trace B" (is "?lhs = ?rhs") proof - have "?lhs = (∑i=0..<n. A$$(i, i) + B$$(i, i))" unfolding trace_def using A B by auto also have "… = (∑i=0..<n. A$$(i, i)) + (∑i=0..<n. B$$(i, i))" by (auto simp add: sum.distrib) finally have l: "?lhs = (∑i=0..<n. A$$(i, i)) + (∑i=0..<n. B$$(i, i))". have r: "?rhs = (∑i=0..<n. A$$(i, i)) + (∑i=0..<n. B$$(i, i))" unfolding trace_def using A B by auto from l r show ?thesis by auto qed lemma trace_minus_linear: fixes A B :: "'a::comm_ring mat" assumes A: "A ∈ carrier_mat n n" and B: "B ∈ carrier_mat n n" shows "trace (A - B) = trace A - trace B" (is "?lhs = ?rhs") proof - have "?lhs = (∑i=0..<n. A$$(i, i) - B$$(i, i))" unfolding trace_def using A B by auto also have "… = (∑i=0..<n. A$$(i, i)) - (∑i=0..<n. B$$(i, i))" by (auto simp add: sum_subtractf) finally have l: "?lhs = (∑i=0..<n. A$$(i, i)) - (∑i=0..<n. B$$(i, i))". have r: "?rhs = (∑i=0..<n. A$$(i, i)) - (∑i=0..<n. B$$(i, i))" unfolding trace_def using A B by auto from l r show ?thesis by auto qed lemma trace_smult: assumes "A ∈ carrier_mat n n" shows "trace (c ⋅⇩_{m}A) = c * trace A" proof - have "trace (c ⋅⇩_{m}A) = (∑i = 0..<dim_row A. c * A $$ (i, i))" unfolding trace_def using assms by auto also have "… = c * (∑i = 0..<dim_row A. A $$ (i, i))" by (simp add: sum_distrib_left) also have "… = c * trace A" unfolding trace_def by auto ultimately show ?thesis by auto qed subsection ‹Conjugate of a vector› lemma conjugate_scalar_prod: fixes v w :: "'a::conjugatable_ring vec" assumes "dim_vec v = dim_vec w" shows "conjugate (v ∙ w) = conjugate v ∙ conjugate w" using assms by (simp add: scalar_prod_def sum_conjugate conjugate_dist_mul) subsection ‹Inner product› abbreviation inner_prod :: "'a vec ⇒ 'a vec ⇒ 'a :: conjugatable_ring" where "inner_prod v w ≡ w ∙c v" lemma conjugate_scalar_prod_Im [simp]: "Im (v ∙c v) = 0" by (simp add: scalar_prod_def conjugate_vec_def sum.neutral) lemma conjugate_scalar_prod_Re [simp]: "Re (v ∙c v) ≥ 0" by (simp add: scalar_prod_def conjugate_vec_def sum_nonneg) lemma self_cscalar_prod_geq_0: fixes v :: "'a::conjugatable_ordered_field vec" shows "v ∙c v ≥ 0" by (auto simp add: scalar_prod_def, rule sum_nonneg, rule conjugate_square_positive) lemma inner_prod_distrib_left: fixes u v w :: "('a::conjugatable_field) vec" assumes dimu: "u ∈ carrier_vec n" and dimv:"v ∈ carrier_vec n" and dimw: "w ∈ carrier_vec n" shows "inner_prod (v + w) u = inner_prod v u + inner_prod w u" (is "?lhs = ?rhs") proof - have dimcv: "conjugate v ∈ carrier_vec n" and dimcw: "conjugate w ∈ carrier_vec n" using assms by auto have dimvw: "conjugate (v + w) ∈ carrier_vec n" using assms by auto have "u ∙ (conjugate (v + w)) = u ∙ conjugate v + u ∙ conjugate w" using dimv dimw dimu dimcv dimcw by (metis conjugate_add_vec scalar_prod_add_distrib) then show ?thesis by auto qed lemma inner_prod_distrib_right: fixes u v w :: "('a::conjugatable_field) vec" assumes dimu: "u ∈ carrier_vec n" and dimv:"v ∈ carrier_vec n" and dimw: "w ∈ carrier_vec n" shows "inner_prod u (v + w) = inner_prod u v + inner_prod u w" (is "?lhs = ?rhs") proof - have dimvw: "v + w ∈ carrier_vec n" using assms by auto have dimcu: "conjugate u ∈ carrier_vec n" using assms by auto have "(v + w) ∙ (conjugate u) = v ∙ conjugate u + w ∙ conjugate u" apply (simp add: comm_scalar_prod[OF dimvw dimcu]) apply (simp add: scalar_prod_add_distrib[OF dimcu dimv dimw]) apply (insert dimv dimw dimcu, simp add: comm_scalar_prod[of _ n]) done then show ?thesis by auto qed lemma inner_prod_minus_distrib_right: fixes u v w :: "('a::conjugatable_field) vec" assumes dimu: "u ∈ carrier_vec n" and dimv:"v ∈ carrier_vec n" and dimw: "w ∈ carrier_vec n" shows "inner_prod u (v - w) = inner_prod u v - inner_prod u w" (is "?lhs = ?rhs") proof - have dimvw: "v - w ∈ carrier_vec n" using assms by auto have dimcu: "conjugate u ∈ carrier_vec n" using assms by auto have "(v - w) ∙ (conjugate u) = v ∙ conjugate u - w ∙ conjugate u" apply (simp add: comm_scalar_prod[OF dimvw dimcu]) apply (simp add: scalar_prod_minus_distrib[OF dimcu dimv dimw]) apply (insert dimv dimw dimcu, simp add: comm_scalar_prod[of _ n]) done then show ?thesis by auto qed lemma inner_prod_smult_right: fixes u v :: "complex vec" assumes dimu: "u ∈ carrier_vec n" and dimv:"v ∈ carrier_vec n" shows "inner_prod (a ⋅⇩_{v}u) v = conjugate a * inner_prod u v" (is "?lhs = ?rhs") using assms apply (simp add: scalar_prod_def conjugate_dist_mul) apply (subst sum_distrib_left) by (rule sum.cong, auto) lemma inner_prod_smult_left: fixes u v :: "complex vec" assumes dimu: "u ∈ carrier_vec n" and dimv: "v ∈ carrier_vec n" shows "inner_prod u (a ⋅⇩_{v}v) = a * inner_prod u v" (is "?lhs = ?rhs") using assms apply (simp add: scalar_prod_def) apply (subst sum_distrib_left) by (rule sum.cong, auto) lemma inner_prod_smult_left_right: fixes u v :: "complex vec" assumes dimu: "u ∈ carrier_vec n" and dimv: "v ∈ carrier_vec n" shows "inner_prod (a ⋅⇩_{v}u) (b ⋅⇩_{v}v) = conjugate a * b * inner_prod u v" (is "?lhs = ?rhs") using assms apply (simp add: scalar_prod_def) apply (subst sum_distrib_left) by (rule sum.cong, auto) lemma inner_prod_swap: fixes x y :: "complex vec" assumes "y ∈ carrier_vec n" and "x ∈ carrier_vec n" shows "inner_prod y x = conjugate (inner_prod x y)" apply (simp add: scalar_prod_def) apply (rule sum.cong) using assms by auto text ‹Cauchy-Schwarz theorem for complex vectors. This is analogous to aux\_Cauchy and Cauchy\_Schwarz\_ineq in Generalizations2.thy in QR\_Decomposition. Consider merging and moving to Isabelle library.› lemma aux_Cauchy: fixes x y :: "complex vec" assumes "x ∈ carrier_vec n" and "y ∈ carrier_vec n" shows "0 ≤ inner_prod x x + a * (inner_prod x y) + (cnj a) * ((cnj (inner_prod x y)) + a * (inner_prod y y))" proof - have "(inner_prod (x+ a ⋅⇩_{v}y) (x+a ⋅⇩_{v}y)) = (inner_prod (x+a ⋅⇩_{v}y) x) + (inner_prod (x+a ⋅⇩_{v}y) (a ⋅⇩_{v}y))" apply (subst inner_prod_distrib_right) using assms by auto also have "… = inner_prod x x + (a) * (inner_prod x y) + cnj a * ((cnj (inner_prod x y)) + (a) * (inner_prod y y))" apply (subst (1 2) inner_prod_distrib_left[of _ n]) apply (auto simp add: assms) apply (subst (1 2) inner_prod_smult_right[of _ n]) apply (auto simp add: assms) apply (subst inner_prod_smult_left[of _ n]) apply (auto simp add: assms) apply (subst inner_prod_swap[of y n x]) apply (auto simp add: assms) unfolding distrib_left by auto finally show ?thesis by (metis self_cscalar_prod_geq_0) qed lemma Cauchy_Schwarz_complex_vec: fixes x y :: "complex vec" assumes "x ∈ carrier_vec n" and "y ∈ carrier_vec n" shows "inner_prod x y * inner_prod y x ≤ inner_prod x x * inner_prod y y" proof - define cnj_a where "cnj_a = - (inner_prod x y)/ cnj (inner_prod y y)" define a where "a = cnj (cnj_a)" have cnj_rw: "(cnj a) = cnj_a" unfolding a_def by (simp) have rw_0: "cnj (inner_prod x y) + a * (inner_prod y y) = 0" unfolding a_def cnj_a_def using assms(1) assms(2) conjugate_square_eq_0_vec by fastforce have "0 ≤ (inner_prod x x + a * (inner_prod x y) + (cnj a) * ((cnj (inner_prod x y)) + a * (inner_prod y y)))" using aux_Cauchy assms by auto also have "… = (inner_prod x x + a * (inner_prod x y))" unfolding rw_0 by auto also have "… = (inner_prod x x - (inner_prod x y) * cnj (inner_prod x y) / (inner_prod y y))" unfolding a_def cnj_a_def by simp finally have " 0 ≤ (inner_prod x x - (inner_prod x y) * cnj (inner_prod x y) / (inner_prod y y)) " . hence "0 ≤ (inner_prod x x - (inner_prod x y) * cnj (inner_prod x y) / (inner_prod y y)) * (inner_prod y y)" by (auto simp: less_eq_complex_def) also have "… = ((inner_prod x x)*(inner_prod y y) - (inner_prod x y) * cnj (inner_prod x y))" by (smt add.inverse_neutral add_diff_cancel diff_0 diff_divide_eq_iff divide_cancel_right mult_eq_0_iff nonzero_mult_div_cancel_right rw_0) finally have "(inner_prod x y) * cnj (inner_prod x y) ≤ (inner_prod x x)*(inner_prod y y)" by auto then show ?thesis apply (subst inner_prod_swap[of y n x]) by (auto simp add: assms) qed subsection ‹Hermitian adjoint of a matrix› abbreviation adjoint where "adjoint ≡ mat_adjoint" lemma adjoint_dim_row [simp]: "dim_row (adjoint A) = dim_col A" by (simp add: mat_adjoint_def) lemma adjoint_dim_col [simp]: "dim_col (adjoint A) = dim_row A" by (simp add: mat_adjoint_def) lemma adjoint_dim: "A ∈ carrier_mat n n ⟹ adjoint A ∈ carrier_mat n n" using adjoint_dim_col adjoint_dim_row by blast lemma adjoint_def: "adjoint A = mat (dim_col A) (dim_row A) (λ(i,j). conjugate (A $$ (j,i)))" unfolding mat_adjoint_def mat_of_rows_def by auto lemma adjoint_eval: assumes "i < dim_col A" "j < dim_row A" shows "(adjoint A) $$ (i,j) = conjugate (A $$ (j,i))" using assms by (simp add: adjoint_def) lemma adjoint_row: assumes "i < dim_col A" shows "row (adjoint A) i = conjugate (col A i)" apply (rule eq_vecI) using assms by (auto simp add: adjoint_eval) lemma adjoint_col: assumes "i < dim_row A" shows "col (adjoint A) i = conjugate (row A i)" apply (rule eq_vecI) using assms by (auto simp add: adjoint_eval) text ‹The identity <v, A w> = <A* v, w>› lemma adjoint_def_alter: fixes v w :: "'a::conjugatable_field vec" and A :: "'a::conjugatable_field mat" assumes dims: "v ∈ carrier_vec n" "w ∈ carrier_vec m" "A ∈ carrier_mat n m" shows "inner_prod v (A *⇩_{v}w) = inner_prod (adjoint A *⇩_{v}v) w" (is "?lhs = ?rhs") proof - from dims have "?lhs = (∑i=0..<dim_vec v. (∑j=0..<dim_vec w. conjugate (v$i) * A$$(i, j) * w$j))" apply (simp add: scalar_prod_def sum_distrib_right ) apply (rule sum.cong, simp) apply (rule sum.cong, auto) done moreover from assms have "?rhs = (∑i=0..<dim_vec v. (∑j=0..<dim_vec w. conjugate (v$i) * A$$(i, j) * w$j))" apply (simp add: scalar_prod_def adjoint_eval sum_conjugate conjugate_dist_mul sum_distrib_left) apply (subst sum.swap[where ?A = "{0..<n}"]) apply (rule sum.cong, simp) apply (rule sum.cong, auto) done ultimately show ?thesis by simp qed lemma adjoint_one: shows "adjoint (1⇩_{m}n) = (1⇩_{m}n::complex mat)" apply (rule eq_matI) by (auto simp add: adjoint_eval) lemma adjoint_scale: fixes A :: "'a::conjugatable_field mat" shows "adjoint (a ⋅⇩_{m}A) = (conjugate a) ⋅⇩_{m}adjoint A" apply (rule eq_matI) using conjugatable_ring_class.conjugate_dist_mul by (auto simp add: adjoint_eval) lemma adjoint_add: fixes A B :: "'a::conjugatable_field mat" assumes "A ∈ carrier_mat n m" "B ∈ carrier_mat n m" shows "adjoint (A + B) = adjoint A + adjoint B" apply (rule eq_matI) using assms conjugatable_ring_class.conjugate_dist_add by( auto simp add: adjoint_eval) lemma adjoint_minus: fixes A B :: "'a::conjugatable_field mat" assumes "A ∈ carrier_mat n m" "B ∈ carrier_mat n m" shows "adjoint (A - B) = adjoint A - adjoint B" apply (rule eq_matI) using assms apply(auto simp add: adjoint_eval) by (metis add_uminus_conv_diff conjugate_dist_add conjugate_neg) lemma adjoint_mult: fixes A B :: "'a::conjugatable_field mat" assumes "A ∈ carrier_mat n m" "B ∈ carrier_mat m l" shows "adjoint (A * B) = adjoint B * adjoint A" proof (rule eq_matI, auto simp add: adjoint_eval adjoint_row adjoint_col) fix i j assume "i < dim_col B" "j < dim_row A" show "conjugate (row A j ∙ col B i) = conjugate (col B i) ∙ conjugate (row A j)" using assms apply (simp add: conjugate_scalar_prod) apply (subst comm_scalar_prod[where n="dim_row B"]) by (auto simp add: carrier_vecI) qed lemma adjoint_adjoint: fixes A :: "'a::conjugatable_field mat" shows "adjoint (adjoint A) = A" by (rule eq_matI, auto simp add: adjoint_eval) lemma trace_adjoint_positive: fixes A :: "complex mat" shows "trace (A * adjoint A) ≥ 0" apply (auto simp add: trace_def adjoint_col) apply (rule sum_nonneg) by auto subsection ‹Algebraic manipulations on matrices› lemma right_add_zero_mat[simp]: "(A :: 'a :: monoid_add mat) ∈ carrier_mat nr nc ⟹ A + 0⇩_{m}nr nc = A" by (intro eq_matI, auto) lemma add_carrier_mat': "A ∈ carrier_mat nr nc ⟹ B ∈ carrier_mat nr nc ⟹ A + B ∈ carrier_mat nr nc" by simp lemma minus_carrier_mat': "A ∈ carrier_mat nr nc ⟹ B ∈ carrier_mat nr nc ⟹ A - B ∈ carrier_mat nr nc" by auto lemma swap_plus_mat: fixes A B C :: "'a::semiring_1 mat" assumes "A ∈ carrier_mat n n" "B ∈ carrier_mat n n" "C ∈ carrier_mat n n" shows "A + B + C = A + C + B" by (metis assms assoc_add_mat comm_add_mat) lemma uminus_mat: fixes A :: "complex mat" assumes "A ∈ carrier_mat n n" shows "-A = (-1) ⋅⇩_{m}A" by auto ML_file "mat_alg.ML" method_setup mat_assoc = ‹mat_assoc_method› "Normalization of expressions on matrices" lemma mat_assoc_test: fixes A B C D :: "complex mat" assumes "A ∈ carrier_mat n n" "B ∈ carrier_mat n n" "C ∈ carrier_mat n n" "D ∈ carrier_mat n n" shows "(A * B) * (C * D) = A * B * C * D" "adjoint (A * adjoint B) * C = B * (adjoint A * C)" "A * 1⇩_{m}n * 1⇩_{m}n * B * 1⇩_{m}n = A * B" "(A - B) + (B - C) = A + (-B) + B + (-C)" "A + (B - C) = A + B - C" "A - (B + C + D) = A - B - C - D" "(A + B) * (B + C) = A * B + B * B + A * C + B * C" "A - B = A + (-1) ⋅⇩_{m}B" "A * (B - C) * D = A * B * D - A * C * D" "trace (A * B * C) = trace (B * C * A)" "trace (A * B * C * D) = trace (C * D * A * B)" "trace (A + B * C) = trace A + trace (C * B)" "A + B = B + A" "A + B + C = C + B + A" "A + B + (C + D) = A + C + (B + D)" using assms by (mat_assoc n)+ subsection ‹Hermitian matrices› text ‹A Hermitian matrix is a matrix that is equal to its Hermitian adjoint.› definition hermitian :: "'a::conjugatable_field mat ⇒ bool" where "hermitian A ⟷ (adjoint A = A)" lemma hermitian_one: shows "hermitian ((1⇩_{m}n)::('a::conjugatable_field mat))" unfolding hermitian_def proof- have "conjugate (1::'a) = 1" apply (subst mult_1_right[symmetric, of "conjugate 1"]) apply (subst conjugate_id[symmetric, of "conjugate 1 * 1"]) apply (subst conjugate_dist_mul) apply auto done then show "adjoint ((1⇩_{m}n)::('a::conjugatable_field mat)) = (1⇩_{m}n)" by (auto simp add: adjoint_eval) qed subsection ‹Inverse matrices› lemma inverts_mat_symm: fixes A B :: "'a::field mat" assumes dim: "A ∈ carrier_mat n n" "B ∈ carrier_mat n n" and AB: "inverts_mat A B" shows "inverts_mat B A" proof - have "A * B = 1⇩_{m}n" using dim AB unfolding inverts_mat_def by auto with dim have "B * A = 1⇩_{m}n" by (rule mat_mult_left_right_inverse) then show "inverts_mat B A" using dim inverts_mat_def by auto qed lemma inverts_mat_unique: fixes A B C :: "'a::field mat" assumes dim: "A ∈ carrier_mat n n" "B ∈ carrier_mat n n" "C ∈ carrier_mat n n" and AB: "inverts_mat A B" and AC: "inverts_mat A C" shows "B = C" proof - have AB1: "A * B = 1⇩_{m}n" using AB dim unfolding inverts_mat_def by auto have "A * C = 1⇩_{m}n" using AC dim unfolding inverts_mat_def by auto then have CA1: "C * A = 1⇩_{m}n" using mat_mult_left_right_inverse[of A n C] dim by auto then have "C = C * 1⇩_{m}n" using dim by auto also have "… = C * (A * B)" using AB1 by auto also have "… = (C * A) * B" using dim by auto also have "… = 1⇩_{m}n * B" using CA1 by auto also have "… = B" using dim by auto finally show "B = C" .. qed subsection ‹Unitary matrices› text ‹A unitary matrix is a matrix whose Hermitian adjoint is also its inverse.› definition unitary :: "'a::conjugatable_field mat ⇒ bool" where "unitary A ⟷ A ∈ carrier_mat (dim_row A) (dim_row A) ∧ inverts_mat A (adjoint A)" lemma unitaryD2: assumes "A ∈ carrier_mat n n" shows "unitary A ⟹ inverts_mat (adjoint A) A" using assms adjoint_dim inverts_mat_symm unitary_def by blast lemma unitary_simps [simp]: "A ∈ carrier_mat n n ⟹ unitary A ⟹ adjoint A * A = 1⇩_{m}n" "A ∈ carrier_mat n n ⟹ unitary A ⟹ A * adjoint A = 1⇩_{m}n" apply (metis adjoint_dim_row carrier_matD(2) inverts_mat_def unitaryD2) by (simp add: inverts_mat_def unitary_def) lemma unitary_adjoint [simp]: assumes "A ∈ carrier_mat n n" "unitary A" shows "unitary (adjoint A)" unfolding unitary_def using adjoint_dim[OF assms(1)] assms by (auto simp add: unitaryD2[OF assms] adjoint_adjoint) lemma unitary_one: shows "unitary ((1⇩_{m}n)::('a::conjugatable_field mat))" unfolding unitary_def proof - define I where I_def[simp]: "I ≡ ((1⇩_{m}n)::('a::conjugatable_field mat))" have dim: "I ∈ carrier_mat n n" by auto have "hermitian I" using hermitian_one by auto hence "adjoint I = I" using hermitian_def by auto with dim show "I ∈ carrier_mat (dim_row I) (dim_row I) ∧ inverts_mat I (adjoint I)" unfolding inverts_mat_def using dim by auto qed lemma unitary_zero: fixes A :: "'a::conjugatable_field mat" assumes "A ∈ carrier_mat 0 0" shows "unitary A" unfolding unitary_def inverts_mat_def Let_def using assms by auto lemma unitary_elim: assumes dims: "A ∈ carrier_mat n n" "B ∈ carrier_mat n n" "P ∈ carrier_mat n n" and uP: "unitary P" and eq: "P * A * adjoint P = P * B * adjoint P" shows "A = B" proof - have dimaP: "adjoint P ∈ carrier_mat n n" using dims by auto have iv: "inverts_mat P (adjoint P)" using uP unitary_def by auto then have "P * (adjoint P) = 1⇩_{m}n" using inverts_mat_def dims by auto then have aPP: "adjoint P * P = 1⇩_{m}n" using mat_mult_left_right_inverse[OF dims(3) dimaP] by auto have "adjoint P * (P * A * adjoint P) * P = (adjoint P * P) * A * (adjoint P * P)" using dims dimaP by (mat_assoc n) also have "… = 1⇩_{m}n * A * 1⇩_{m}n" using aPP by auto also have "… = A" using dims by auto finally have eqA: "A = adjoint P * (P * A * adjoint P) * P" .. have "adjoint P * (P * B * adjoint P) * P = (adjoint P * P) * B * (adjoint P * P)" using dims dimaP by (mat_assoc n) also have "… = 1⇩_{m}n * B * 1⇩_{m}n" using aPP by auto also have "… = B" using dims by auto finally have eqB: "B = adjoint P * (P * B * adjoint P) * P" .. then show ?thesis using eqA eqB eq by auto qed lemma unitary_is_corthogonal: fixes U :: "'a::conjugatable_field mat" assumes dim: "U ∈ carrier_mat n n" and U: "unitary U" shows "corthogonal_mat U" unfolding corthogonal_mat_def Let_def proof (rule conjI) have dima: "adjoint U ∈ carrier_mat n n" using dim by auto have aUU: "mat_adjoint U * U = (1⇩_{m}n)" apply (insert U[unfolded unitary_def] dim dima, drule conjunct2) apply (drule inverts_mat_symm[of "U", OF dim dima], unfold inverts_mat_def, auto) done then show "diagonal_mat (mat_adjoint U * U)" by (simp add: diagonal_mat_def) show "∀i<dim_col U. (mat_adjoint U * U) $$ (i, i) ≠ 0" using dim by (simp add: aUU) qed lemma unitary_times_unitary: fixes P Q :: "'a:: conjugatable_field mat" assumes dim: "P ∈ carrier_mat n n" "Q ∈ carrier_mat n n" and uP: "unitary P" and uQ: "unitary Q" shows "unitary (P * Q)" proof - have dim_pq: "P * Q ∈ carrier_mat n n" using dim by auto have "(P * Q) * adjoint (P * Q) = P * (Q * adjoint Q) * adjoint P" using dim by (mat_assoc n) also have "… = P * (1⇩_{m}n) * adjoint P" using uQ dim by auto also have "… = P * adjoint P" using dim by (mat_assoc n) also have "… = 1⇩_{m}n" using uP dim by simp finally have "(P * Q) * adjoint (P * Q) = 1⇩_{m}n" by auto hence "inverts_mat (P * Q) (adjoint (P * Q))" using inverts_mat_def dim_pq by auto thus "unitary (P*Q)" using unitary_def dim_pq by auto qed lemma unitary_operator_keep_trace: fixes U A :: "complex mat" assumes dU: "U ∈ carrier_mat n n" and dA: "A ∈ carrier_mat n n" and u: "unitary U" shows "trace A = trace (adjoint U * A * U)" proof - have u': "U * adjoint U = 1⇩_{m}n" using u unfolding unitary_def inverts_mat_def using dU by auto have "trace (adjoint U * A * U) = trace (U * adjoint U * A)" using dU dA by (mat_assoc n) also have "… = trace A" using u' dA by auto finally show ?thesis by auto qed subsection ‹Normalization of vectors› definition vec_norm :: "complex vec ⇒ complex" where "vec_norm v ≡ csqrt (v ∙c v)" lemma vec_norm_geq_0: fixes v :: "complex vec" shows "vec_norm v ≥ 0" unfolding vec_norm_def by (insert self_cscalar_prod_geq_0[of v], simp add: less_eq_complex_def) lemma vec_norm_zero: fixes v :: "complex vec" assumes dim: "v ∈ carrier_vec n" shows "vec_norm v = 0 ⟷ v = 0⇩_{v}n" unfolding vec_norm_def by (subst conjugate_square_eq_0_vec[OF dim, symmetric], rule csqrt_eq_0) lemma vec_norm_ge_0: fixes v :: "complex vec" assumes dim_v: "v ∈ carrier_vec n" and neq0: "v ≠ 0⇩_{v}n" shows "vec_norm v > 0" proof - have geq: "vec_norm v ≥ 0" using vec_norm_geq_0 by auto have neq: "vec_norm v ≠ 0" apply (insert dim_v neq0) apply (drule vec_norm_zero, auto) done show ?thesis using neq geq by (rule dual_order.not_eq_order_implies_strict) qed definition vec_normalize :: "complex vec ⇒ complex vec" where "vec_normalize v = (if (v = 0⇩_{v}(dim_vec v)) then v else 1 / (vec_norm v) ⋅⇩_{v}v)" lemma normalized_vec_dim[simp]: assumes "(v::complex vec) ∈ carrier_vec n" shows "vec_normalize v ∈ carrier_vec n" unfolding vec_normalize_def using assms by auto lemma vec_eq_norm_smult_normalized: shows "v = vec_norm v ⋅⇩_{v}vec_normalize v" proof (cases "v = 0⇩_{v}(dim_vec v)") define n where "n = dim_vec v" then have dimv: "v ∈ carrier_vec n" by auto then have dimnv: "vec_normalize v ∈ carrier_vec n" by auto { case True then have v0: "v = 0⇩_{v}n" using n_def by auto then have n0: "vec_norm v = 0" using vec_norm_def by auto have "vec_norm v ⋅⇩_{v}vec_normalize v = 0⇩_{v}n" unfolding smult_vec_def by (auto simp add: n0 carrier_vecD[OF dimnv]) then show ?thesis using v0 by auto next case False then have v: "v ≠ 0⇩_{v}n" using n_def by auto then have ge0: "vec_norm v > 0" using vec_norm_ge_0 dimv by auto have "vec_normalize v = (1 / vec_norm v) ⋅⇩_{v}v" using False vec_normalize_def by auto then have "vec_norm v ⋅⇩_{v}vec_normalize v = (vec_norm v * (1 / vec_norm v)) ⋅⇩_{v}v" using smult_smult_assoc by auto also have "… = v" using ge0 by auto finally have "v = vec_norm v ⋅⇩_{v}vec_normalize v".. then show "v = vec_norm v ⋅⇩_{v}vec_normalize v" using v by auto } qed lemma normalized_cscalar_prod: fixes v w :: "complex vec" assumes dim_v: "v ∈ carrier_vec n" and dim_w: "w ∈ carrier_vec n" shows "v ∙c w = (vec_norm v * vec_norm w) * (vec_normalize v ∙c vec_normalize w)" unfolding vec_normalize_def apply (split if_split, split if_split) proof (intro conjI impI) note dim0 = dim_v dim_w have dim: "dim_vec v = n" "dim_vec w = n" using dim0 by auto { assume "w = 0⇩_{v}n" "v = 0⇩_{v}n" then have lhs: "v ∙c w = 0" by auto then moreover have rhs: "vec_norm v * vec_norm w * (v ∙c w) = 0" by auto ultimately have "v ∙c w = vec_norm v * vec_norm w * (v ∙c w)" by auto } with dim show "w = 0⇩_{v}(dim_vec w) ⟹ v = 0⇩_{v}(dim_vec v) ⟹ v ∙c w = vec_norm v * vec_norm w * (v ∙c w)" by auto { assume asm: "w = 0⇩_{v}n" "v ≠ 0⇩_{v}n" then have w0: "conjugate w = 0⇩_{v}n" by auto with dim0 have "(1 / vec_norm v ⋅⇩_{v}v) ∙c w = 0" by auto then moreover have rhs: "vec_norm v * vec_norm w * ((1 / vec_norm v ⋅⇩_{v}v) ∙c w) = 0" by auto moreover have "v ∙c w = 0" using w0 dim0 by auto ultimately have "v ∙c w = vec_norm v * vec_norm w * ((1 / vec_norm v ⋅⇩_{v}v) ∙c w)" by auto } with dim show "w = 0⇩_{v}(dim_vec w) ⟹ v ≠ 0⇩_{v}(dim_vec v) ⟹ v ∙c w = vec_norm v * vec_norm w * ((1 / vec_norm v ⋅⇩_{v}v) ∙c w)" by auto { assume asm: "w ≠ 0⇩_{v}n" "v = 0⇩_{v}n" with dim0 have "v ∙c (1 / vec_norm w ⋅⇩_{v}w) = 0" by auto then moreover have rhs: "vec_norm v * vec_norm w * (v ∙c (1 / vec_norm w ⋅⇩_{v}w)) = 0" by auto moreover have "v ∙c w = 0" using asm dim0 by auto ultimately have "v ∙c w = vec_norm v * vec_norm w * (v ∙c (1 / vec_norm w ⋅⇩_{v}w))" by auto } with dim show "w ≠ 0⇩_{v}(dim_vec w) ⟹ v = 0⇩_{v}(dim_vec v) ⟹ v ∙c w = vec_norm v * vec_norm w * (v ∙c (1 / vec_norm w ⋅⇩_{v}w))" by auto { assume asmw: "w ≠ 0⇩_{v}n" and asmv: "v ≠ 0⇩_{v}n" have "vec_norm w > 0" by (insert asmw dim0, rule vec_norm_ge_0, auto) then have cw: "conjugate (1 / vec_norm w) = 1 / vec_norm w" by (simp add: complex_eq_iff complex_is_Real_iff less_complex_def) from dim0 have "((1 / vec_norm v ⋅⇩_{v}v) ∙c (1 / vec_norm w ⋅⇩_{v}w)) = 1 / vec_norm v * (v ∙c (1 / vec_norm w ⋅⇩_{v}w))" by auto also have "… = 1 / vec_norm v * (v ∙ (conjugate (1 / vec_norm w) ⋅⇩_{v}conjugate w))" by (subst conjugate_smult_vec, auto) also have "… = 1 / vec_norm v * conjugate (1 / vec_norm w) * (v ∙ conjugate w)" using dim by auto also have "… = 1 / vec_norm v * (1 / vec_norm w) * (v ∙c w)" using vec_norm_ge_0 cw by auto finally have eq1: "(1 / vec_norm v ⋅⇩_{v}v) ∙c (1 / vec_norm w ⋅⇩_{v}w) = 1 / vec_norm v * (1 / vec_norm w) * (v ∙c w)" . then have "vec_norm v * vec_norm w * ((1 / vec_norm v ⋅⇩_{v}v) ∙c (1 / vec_norm w ⋅⇩_{v}w)) = (v ∙c w)" by (subst eq1, insert vec_norm_ge_0[of v n, OF dim_v asmv] vec_norm_ge_0[of w n, OF dim_w asmw], auto) } with dim show " w ≠ 0⇩_{v}(dim_vec w) ⟹ v ≠ 0⇩_{v}(dim_vec v) ⟹ v ∙c w = vec_norm v * vec_norm w * ((1 / vec_norm v ⋅⇩_{v}v) ∙c (1 / vec_norm w ⋅⇩_{v}w))" by auto qed lemma normalized_vec_norm : fixes v :: "complex vec" assumes dim_v: "v ∈ carrier_vec n" and neq0: "v ≠ 0⇩_{v}n" shows "vec_normalize v ∙c vec_normalize v = 1" unfolding vec_normalize_def proof (simp, rule conjI) show "v = 0⇩_{v}(dim_vec v) ⟶ v ∙c v = 1" using neq0 dim_v by auto have dim_a: "(vec_normalize v) ∈ carrier_vec n" "conjugate (vec_normalize v) ∈ carrier_vec n" using dim_v vec_normalize_def by auto note dim = dim_v dim_a have nvge0: "vec_norm v > 0" using vec_norm_ge_0 neq0 dim_v by auto then have vvvv: "v ∙c v = (vec_norm v) * (vec_norm v)" unfolding vec_norm_def by (metis power2_csqrt power2_eq_square) from nvge0 have "conjugate (vec_norm v) = vec_norm v" by (simp add: complex_eq_iff complex_is_Real_iff less_complex_def) then have "v ∙c (1 / vec_norm v ⋅⇩_{v}v) = 1 / vec_norm v * (v ∙c v)" by (subst conjugate_smult_vec, auto) also have "… = 1 / vec_norm v * vec_norm v * vec_norm v" using vvvv by auto also have "… = vec_norm v" by auto finally have "v ∙c (1 / vec_norm v ⋅⇩_{v}v) = vec_norm v". then show "v ≠ 0⇩_{v}(dim_vec v) ⟶ vec_norm v ≠ 0 ∧ v ∙c (1 / vec_norm v ⋅⇩_{v}v) = vec_norm v" using neq0 nvge0 by auto qed lemma normalize_zero: assumes "v ∈ carrier_vec n" shows "vec_normalize v = 0⇩_{v}n ⟷ v = 0⇩_{v}n" proof show "v = 0⇩_{v}n ⟹ vec_normalize v = 0⇩_{v}n" unfolding vec_normalize_def by auto next have "v ≠ 0⇩_{v}n ⟹ vec_normalize v ≠ 0⇩_{v}n" unfolding vec_normalize_def proof (simp, rule impI) assume asm: "v ≠ 0⇩_{v}n" then have "vec_norm v > 0" using vec_norm_ge_0 assms by auto then have nvge0: "1 / vec_norm v > 0" by (simp add: complex_is_Real_iff less_complex_def) have "∃k < n. v $ k ≠ 0" using asm assms by auto then obtain k where kn: "k < n" and vkneq0: "v $ k ≠ 0" by auto then have "(1 / vec_norm v ⋅⇩_{v}v) $ k = (1 / vec_norm v) * (v $ k)" using assms carrier_vecD index_smult_vec(1) by blast with nvge0 vkneq0 have "(1 / vec_norm v ⋅⇩_{v}v) $ k ≠ 0" by auto then show "1 / vec_norm v ⋅⇩_{v}v ≠ 0⇩_{v}n" using assms kn by fastforce qed then show "vec_normalize v = 0⇩_{v}n ⟹ v = 0⇩_{v}n" by auto qed lemma normalize_normalize[simp]: "vec_normalize (vec_normalize v) = vec_normalize v" proof (rule disjE[of "v = 0⇩_{v}(dim_vec v)" "v ≠ 0⇩_{v}(dim_vec v)"], auto) let ?n = "dim_vec v" { assume "v = 0⇩_{v}?n" then have "vec_normalize v = v" unfolding vec_normalize_def by auto then show "vec_normalize (vec_normalize v) = vec_normalize v" by auto } assume neq0: "v ≠ 0⇩_{v}?n" have dim: "v ∈ carrier_vec ?n" by auto have "vec_norm (vec_normalize v) = 1" unfolding vec_norm_def using normalized_vec_norm[OF dim neq0] by auto then show "vec_normalize (vec_normalize v) = vec_normalize v" by (subst (1) vec_normalize_def, simp) qed subsection ‹Spectral decomposition of normal complex matrices› lemma normalize_keep_corthogonal: fixes vs :: "complex vec list" assumes cor: "corthogonal vs" and dims: "set vs ⊆ carrier_vec n" shows "corthogonal (map vec_normalize vs)" unfolding corthogonal_def proof (rule allI, rule impI, rule allI, rule impI, goal_cases) case c: (1 i j) let ?m = "length vs" have len: "length (map vec_normalize vs) = ?m" by auto have dim: "⋀k. k < ?m ⟹ (vs ! k) ∈ carrier_vec n" using dims by auto have map: "⋀k. k < ?m ⟹ map vec_normalize vs ! k = vec_normalize (vs ! k)" by auto have eq1: "⋀j k. j < ?m ⟹ k < ?m ⟹ ((vs ! j) ∙c (vs ! k) = 0) = (j ≠ k)" using assms unfolding corthogonal_def by auto then have "⋀k. k < ?m ⟹ (vs ! k) ∙c (vs ! k) ≠ 0 " by auto then have "⋀k. k < ?m ⟹ (vs ! k) ≠ (0⇩_{v}n)" using dim by (auto simp add: conjugate_square_eq_0_vec[of _ n, OF dim]) then have vnneq0: "⋀k. k < ?m ⟹ vec_norm (vs ! k) ≠ 0" using vec_norm_zero[OF dim] by auto then have i0: "vec_norm (vs ! i) ≠ 0" and j0: "vec_norm (vs ! j) ≠ 0" using c by auto have "(vs ! i) ∙c (vs ! j) = vec_norm (vs ! i) * vec_norm (vs ! j) * (vec_normalize (vs ! i) ∙c vec_normalize (vs ! j))" by (subst normalized_cscalar_prod[of "vs ! i" n "vs ! j"], auto, insert dim c, auto) with i0 j0 have "(vec_normalize (vs ! i) ∙c vec_normalize (vs ! j) = 0) = ((vs ! i) ∙c (vs ! j) = 0)" by auto with eq1 c have "(vec_normalize (vs ! i) ∙c vec_normalize (vs ! j) = 0) = (i ≠ j)" by auto with map c show "(map vec_normalize vs ! i ∙c map vec_normalize vs ! j = 0) = (i ≠ j)" by auto qed lemma normalized_corthogonal_mat_is_unitary: assumes W: "set ws ⊆ carrier_vec n" and orth: "corthogonal ws" and len: "length ws = n" shows "unitary (mat_of_cols n (map vec_normalize ws))" (is "unitary ?W") proof - define vs where "vs = map vec_normalize ws" define W where "W = mat_of_cols n vs" have W': "set vs ⊆ carrier_vec n" using assms vs_def by auto then have W'': "⋀k. k < length vs ⟹ vs ! k ∈ carrier_vec n" by auto have orth': "corthogonal vs" using assms normalize_keep_corthogonal vs_def by auto have len'[simp]: "length vs = n" using assms vs_def by auto have dimW: "W ∈ carrier_mat n n" using W_def len by auto have "adjoint W ∈ carrier_mat n n" using dimW by auto then have dimaW: "mat_adjoint W ∈ carrier_mat n n" by auto { fix i j assume i: "i < n" and j: "j < n" have dimws: "(ws ! i) ∈ carrier_vec n" "(ws ! j) ∈ carrier_vec n" using W len i j by auto have "(ws ! i) ∙c (ws ! i) ≠ 0" "(ws ! j) ∙c (ws ! j) ≠ 0" using orth corthogonal_def[of ws] len i j by auto then have neq0: "(ws ! i) ≠ 0⇩_{v}n" "(ws ! j) ≠ 0⇩_{v}n" by (auto simp add: conjugate_square_eq_0_vec[of "ws ! i" n]) then have "vec_norm (ws ! i) > 0" "vec_norm (ws ! j) > 0" using vec_norm_ge_0 dimws by auto then have ge0: "vec_norm (ws ! i) * vec_norm (ws ! j) > 0" by (auto simp: less_complex_def) have ws': "vs ! i = vec_normalize (ws ! i)" "vs ! j = vec_normalize (ws ! j)" using len i j vs_def by auto have ii1: "(vs ! i) ∙c (vs ! i) = 1" apply (simp add: ws') apply (rule normalized_vec_norm[of "ws ! i"], rule dimws, rule neq0) done have ij0: "i ≠ j ⟹ (ws ! i) ∙c (ws ! j) = 0" using i j by (insert orth, auto simp add: corthogonal_def[of ws] len) have "i ≠ j ⟹ (ws ! i) ∙c (ws ! j) = (vec_norm (ws ! i) * vec_norm (ws ! j)) * ((vs ! i) ∙c (vs ! j))" apply (auto simp add: ws') apply (rule normalized_cscalar_prod) apply (rule dimws, rule dimws) done with ij0 have ij0': "i ≠ j ⟹ (vs ! i) ∙c (vs ! j) = 0" using ge0 by auto have cWk: "⋀k. k < n ⟹ col W k = vs ! k" unfolding W_def apply (subst col_mat_of_cols) apply (auto simp add: W'') done have "(mat_adjoint W * W) $$ (j, i) = row (mat_adjoint W) j ∙ col W i" by (insert dimW i j dimaW, auto) also have "… = conjugate (col W j) ∙ col W i" by (insert dimW i j dimaW, auto simp add: mat_adjoint_def) also have "… = col W i ∙ conjugate (col W j)" using comm_scalar_prod[of "col W i" n] dimW by auto also have "… = (vs ! i) ∙c (vs ! j)" using W_def col_mat_of_cols i j len cWk by auto finally have "(mat_adjoint W * W) $$ (j, i) = (vs ! i) ∙c (vs ! j)". then have "(mat_adjoint W * W) $$ (j, i) = (if (j = i) then 1 else 0)" by (auto simp add: ii1 ij0') } note maWW = this then have "mat_adjoint W * W = 1⇩_{m}n" unfolding one_mat_def using dimW dimaW by (auto simp add: maWW adjoint_def) then have iv0: "adjoint W * W = 1⇩_{m}n" by auto have dimaW: "adjoint W ∈ carrier_mat n n" using dimaW by auto then have iv1: "W * adjoint W = 1⇩_{m}n" using mat_mult_left_right_inverse dimW iv0 by auto then show "unitary W" unfolding unitary_def inverts_mat_def using dimW dimaW iv0 iv1 by auto qed lemma normalize_keep_eigenvector: assumes ev: "eigenvector A v e" and dim: "A ∈ carrier_mat n n" "v ∈ carrier_vec n" shows "eigenvector A (vec_normalize v) e" unfolding eigenvector_def proof show "vec_normalize v ∈ carrier_vec (dim_row A)" using dim by auto have eg: "A *⇩_{v}v = e ⋅⇩_{v}v" using ev dim eigenvector_def by auto have vneq0: "v ≠ 0⇩_{v}n" using ev dim unfolding eigenvector_def by auto then have s0: "vec_normalize v ≠ 0⇩_{v}n" by (insert dim, subst normalize_zero[of v], auto) from vneq0 have vvge0: "vec_norm v > 0" using vec_norm_ge_0 dim by auto have s1: "A *⇩_{v}vec_normalize v = e ⋅⇩_{v}vec_normalize v" unfolding vec_normalize_def using vneq0 dim apply (auto, simp add: mult_mat_vec) apply (subst eg, auto) done with s0 dim show "vec_normalize v ≠ 0⇩_{v}(dim_row A) ∧ A *⇩_{v}vec_normalize v = e ⋅⇩_{v}vec_normalize v" by auto qed lemma four_block_mat_adjoint: fixes A B C D :: "'a::conjugatable_field mat" assumes dim: "A ∈ carrier_mat nr1 nc1" "B ∈ carrier_mat nr1 nc2" "C ∈ carrier_mat nr2 nc1" "D ∈ carrier_mat nr2 nc2" shows "adjoint (four_block_mat A B C D) = four_block_mat (adjoint A) (adjoint C) (adjoint B) (adjoint D)" by (rule eq_matI, insert dim, auto simp add: adjoint_eval) fun unitary_schur_decomposition :: "complex mat ⇒ complex list ⇒ complex mat × complex mat × complex mat" where "unitary_schur_decomposition A [] = (A, 1⇩_{m}(dim_row A), 1⇩_{m}(dim_row A))" | "unitary_schur_decomposition A (e # es) = (let n = dim_row A; n1 = n - 1; v' = find_eigenvector A e; v = vec_normalize v'; ws0 = gram_schmidt n (basis_completion v); ws = map vec_normalize ws0; W = mat_of_cols n ws; W' = corthogonal_inv W; A' = W' * A * W; (A1,A2,A0,A3) = split_block A' 1 1; (B,P,Q) = unitary_schur_decomposition A3 es; z_row = (0⇩_{m}1 n1); z_col = (0⇩_{m}n1 1); one_1 = 1⇩_{m}1 in (four_block_mat A1 (A2 * P) A0 B, W * four_block_mat one_1 z_row z_col P, four_block_mat one_1 z_row z_col Q * W'))" theorem unitary_schur_decomposition: assumes A: "(A::complex mat) ∈ carrier_mat n n" and c: "char_poly A = (∏ (e :: complex) ← es. [:- e, 1:])" and B: "unitary_schur_decomposition A es = (B,P,Q)" shows "similar_mat_wit A B P Q ∧ upper_triangular B ∧ diag_mat B = es ∧ unitary P ∧ (Q = adjoint P)" using assms proof (induct es arbitrary: n A B P Q) case Nil with degree_monic_char_poly[of A n] show ?case by (auto intro: similar_mat_wit_refl simp: diag_mat_def unitary_zero) next case (Cons e es n A C P Q) let ?n1 = "n - 1" from Cons have A: "A ∈ carrier_mat n n" and dim: "dim_row A = n" by auto let ?cp = "char_poly A" from Cons(3) have cp: "?cp = [: -e, 1 :] * (∏e ← es. [:- e, 1:])" by auto have mon: "monic (∏e← es. [:- e, 1:])" by (rule monic_prod_list, auto) have deg: "degree ?cp = Suc (degree (∏e← es. [:- e, 1:]))" unfolding cp by (subst degree_mult_eq, insert mon, auto) with degree_monic_char_poly[OF A] have n: "n ≠ 0" by auto define v' where "v' = find_eigenvector A e" define v where "v = vec_normalize v'" define b where "b = basis_completion v" define ws0 where "ws0 = gram_schmidt n b" define ws where "ws = map vec_normalize ws0" define W where "W = mat_of_cols n ws" define W' where "W' = corthogonal_inv W" define A' where "A' = W' * A * W" obtain A1 A2 A0 A3 where splitA': "split_block A' 1 1 = (A1,A2,A0,A3)" by (cases "split_block A' 1 1", auto) obtain B P' Q' where schur: "unitary_schur_decomposition A3 es = (B,P',Q')" by (cases "unitary_schur_decomposition A3 es", auto) let ?P' = "four_block_mat (1⇩_{m}1) (0⇩_{m}1 ?n1) (0⇩_{m}?n1 1) P'" let ?Q' = "four_block_mat (1⇩_{m}1) (0⇩_{m}1 ?n1) (0⇩_{m}?n1 1) Q'" have C: "C = four_block_mat A1 (A2 * P') A0 B" and P: "P = W * ?P'" and Q: "Q = ?Q' * W'" using Cons(4) unfolding unitary_schur_decomposition.simps Let_def list.sel dim v'_def[symmetric] v_def[symmetric] b_def[symmetric] ws0_def[symmetric] ws_def[symmetric] W'_def[symmetric] W_def[symmetric] A'_def[symmetric] split splitA' schur by auto have e: "eigenvalue A e" unfolding eigenvalue_root_char_poly[OF A] cp by simp from find_eigenvector[OF A e] have ev': "eigenvector A v' e" unfolding v'_def . then have "v' ∈ carrier_vec n" unfolding eigenvector_def using A by auto with ev' have ev: "eigenvector A v e" unfolding v_def using A dim normalize_keep_eigenvector by auto from this[unfolded eigenvector_def] have v[simp]: "v ∈ carrier_vec n" and v0: "v ≠ 0⇩_{v}n" using A by auto interpret cof_vec_space n "TYPE(complex)" . from basis_completion[OF v v0, folded b_def] have span_b: "span (set b) = carrier_vec n" and dist_b: "distinct b" and indep: "¬ lin_dep (set b)" and b: "set b ⊆ carrier_vec n" and hdb: "hd b = v" and len_b: "length b = n" by auto from hdb len_b n obtain vs where bv: "b = v # vs" by (cases b, auto) from gram_schmidt_result[OF b dist_b indep refl, folded ws0_def] have ws0: "set ws0 ⊆ carrier_vec n" "corthogonal ws0" "length ws0 = n" by (auto simp: len_b) then have ws: "set ws ⊆ carrier_vec n" "corthogonal ws" "length ws = n" unfolding ws_def using normalize_keep_corthogonal by auto have ws0ne: "ws0 ≠ []" using ‹length ws0 = n› n by auto from gram_schmidt_hd[OF v, of vs, folded bv] have hdws0: "hd ws0 = (vec_normalize v')" unfolding ws0_def v_def . have "hd ws = vec_normalize (hd ws0)" unfolding ws_def using hd_map[OF ws0ne] by auto then have hdws: "hd ws = v" unfolding v_def using normalize_normalize[of v'] hdws0 by auto have orth_W: "corthogonal_mat W" using orthogonal_mat_of_cols ws unfolding W_def. have W: "W ∈ carrier_mat n n" using ws unfolding W_def using mat_of_cols_carrier(1)[of n ws] by auto have W': "W' ∈ carrier_mat n n" unfolding W'_def corthogonal_inv_def using W by (auto simp: mat_of_rows_def) from corthogonal_inv_result[OF orth_W] have W'W: "inverts_mat W' W" unfolding W'_def . hence WW': "inverts_mat W W'" using mat_mult_left_right_inverse[OF W' W] W' W unfolding inverts_mat_def by auto have A': "A' ∈ carrier_mat n n" using W W' A unfolding A'_def by auto have A'A_wit: "similar_mat_wit A' A W' W" by (rule similar_mat_witI[of _ _ n], insert W W' A A' W'W WW', auto simp: A'_def inverts_mat_def) hence A'A: "similar_mat A' A" unfolding similar_mat_def by blast from similar_mat_wit_sym[OF A'A_wit] have simAA': "similar_mat_wit A A' W W'" by auto have eigen[simp]: "A *⇩_{v}v = e ⋅⇩_{v}v" and v0: "v ≠ 0⇩_{v}n" using v_def v'_def find_eigenvector[OF A e] A normalize_keep_eigenvector unfolding eigenvector_def by auto let ?f = "(λ i. if i = 0 then e else 0)" have col0: "col A' 0 = vec n ?f" unfolding A'_def W'_def W_def using corthogonal_col_ev_0[OF A v v0 eigen n hdws ws]. from A' n have "dim_row A' = 1 + ?n1" "dim_col A' = 1 + ?n1" by auto from split_block[OF splitA' this] have A2: "A2 ∈ carrier_mat 1 ?n1" and A3: "A3 ∈ carrier_mat ?n1 ?n1" and A'block: "A' = four_block_mat A1 A2 A0 A3" by auto have A1id: "A1 = mat 1 1 (λ _. e)" using splitA'[unfolded split_block_def Let_def] arg_cong[OF col0, of "λ v. v $ 0"] A' n by (auto simp: col_def) have A1: "A1 ∈ carrier_mat 1 1" unfolding A1id by auto { fix i assume "i < ?n1" with arg_cong[OF col0, of "λ v. v $ Suc i"] A' have "A' $$ (Suc i, 0) = 0" by auto } note A'0 = this have A0id: "A0 = 0⇩_{m}?n1 1" using splitA'[unfolded split_block_def Let_def] A'0 A' by auto have A0: "A0 ∈ carrier_mat ?n1 1" unfolding A0id by auto from cp char_poly_similar[OF A'A] have cp: "char_poly A' = [: -e,1 :] * (∏ e ← es. [:- e, 1:])" by simp also have "char_poly A' = char_poly A1 * char_poly A3" unfolding A'block A0id by (rule char_poly_four_block_zeros_col[OF A1 A2 A3]) also have "char_poly A1 = [: -e,1 :]" by (simp add: A1id char_poly_defs det_def) finally have cp: "char_poly A3 = (∏ e ← es. [:- e, 1:])" by (metis mult_cancel_left pCons_eq_0_iff zero_neq_one) from Cons(1)[OF A3 cp schur] have simIH: "similar_mat_wit A3 B P' Q'" and ut: "upper_triangular B" and diag: "diag_mat B = es" and uP': "unitary P'" and Q'P': "Q' = adjoint P'" by auto from similar_mat_witD2[OF A3 simIH] have B: "B ∈ carrier_mat ?n1 ?n1" and P': "P' ∈ carrier_mat ?n1 ?n1" and Q': "Q' ∈ carrier_mat ?n1 ?n1" and PQ': "P' * Q' = 1⇩_{m}?n1" by auto have A0_eq: "A0 = P' * A0 * 1⇩_{m}1" unfolding A0id using P' by auto have simA'C: "similar_mat_wit A' C ?P' ?Q'" unfolding A'block C by (rule similar_mat_wit_four_block[OF similar_mat_wit_refl[OF A1] simIH _ A0_eq A1 A3 A0], insert PQ' A2 P' Q', auto) have ut1: "upper_triangular A1" unfolding A1id by auto have ut: "upper_triangular C" unfolding C A0id by (intro upper_triangular_four_block[OF _ B ut1 ut], auto simp: A1id) from A1id have diagA1: "diag_mat A1 = [e]" unfolding diag_mat_def by auto from diag_four_block_mat[OF A1 B] have diag: "diag_mat C = e # es" unfolding diag diagA1 C by simp have aW: "adjoint W ∈ carrier_mat n n" using W by auto have aW': "adjoint W' ∈ carrier_mat n n" using W' by auto have "unitary W" using W_def ws_def ws0 normalized_corthogonal_mat_is_unitary by auto then have ivWaW: "inverts_mat W (adjoint W)" using unitary_def W aW by auto with WW' have W'aW: "W' = (adjoint W)" using inverts_mat_unique W W' aW by auto then have "adjoint W' = W" using adjoint_adjoint by auto with ivWaW have "inverts_mat W' (adjoint W')" using inverts_mat_symm W aW W'aW by auto then have "unitary W'" using unitary_def W' by auto have newP': "P' ∈ carrier_mat (n - Suc 0) (n - Suc 0)" using P' by auto have rl: "⋀ x1 x2 x3 x4 y1 y2 y3 y4 f. x1 = y1 ⟹ x2 = y2 ⟹ x3 = y3 ⟹ x4 = y4 ⟹ f x1 x2 x3 x4 = f y1 y2 y3 y4" by simp have Q'aP': "?Q' = adjoint ?P'" apply (subst four_block_mat_adjoint, auto simp add: newP') apply (rule rl[where f2 = four_block_mat]) apply (auto simp add: eq_matI adjoint_eval Q'P') done have "adjoint P = adjoint ?P' * adjoint W" using W newP' n apply (simp add: P) apply (subst adjoint_mult[of W, symmetric]) apply (auto simp add: W P' carrier_matD[of W n n]) done also have "… = ?Q' * W'" using Q'aP' W'aW by auto also have "… = Q" using Q by auto finally have QaP: "Q = adjoint P" .. from similar_mat_wit_trans[OF simAA' simA'C, folded P Q] have smw: "similar_mat_wit A C P Q" by blast then have dimP: "P ∈ carrier_mat n n" and dimQ: "Q ∈ carrier_mat n n" unfolding similar_mat_wit_def using A by auto from smw have "P * Q = 1⇩_{m}n" unfolding similar_mat_wit_def using A by auto then have "inverts_mat P Q" using inverts_mat_def dimP by auto then have uP: "unitary P" using QaP unitary_def dimP by auto from ut similar_mat_wit_trans[OF simAA' simA'C, folded P Q] diag uP QaP show ?case by blast qed lemma complex_mat_char_poly_factorizable: fixes A :: "complex mat" assumes "A ∈ carrier_mat n n" shows "∃as. char_poly A = (∏ a ← as. [:- a, 1:]) ∧ length as = n" proof - let ?ca = "char_poly A" have ex0: "∃bs. Polynomial.smult (lead_coeff ?ca) (∏b←bs. [:- b, 1:]) = ?ca ∧ length bs = degree ?ca" by (simp add: fundamental_theorem_algebra_factorized) then obtain bs where " Polynomial.smult (lead_coeff ?ca) (∏b←bs. [:- b, 1:]) = ?ca ∧ length bs = degree ?ca" by auto moreover have "lead_coeff ?ca = (1::complex)" using assms degree_monic_char_poly by blast ultimately have ex1: "?ca = (∏b←bs. [:- b, 1:]) ∧ length bs = degree ?ca" by auto moreover have "degree ?ca = n" by (simp add: assms degree_monic_char_poly) ultimately show ?thesis by auto qed lemma complex_mat_has_unitary_schur_decomposition: fixes A :: "complex mat" assumes "A ∈ carrier_mat n n" shows "∃B P es. similar_mat_wit A B P (adjoint P) ∧ unitary P ∧ char_poly A = (∏ (e :: complex) ← es. [:- e, 1:]) ∧ diag_mat B = es" proof - have "∃es. char_poly A = (∏ e ← es. [:- e, 1:]) ∧ length es = n" using assms by (simp add: complex_mat_char_poly_factorizable) then obtain es where es: "char_poly A = (∏ e ← es. [:- e, 1:]) ∧ length es = n" by auto obtain B P Q where B: "unitary_schur_decomposition A es = (B,P,Q)" by (cases "unitary_schur_decomposition A es", auto) have "similar_mat_wit A B P Q ∧ upper_triangular B ∧ unitary P ∧ (Q = adjoint P) ∧ char_poly A = (∏ (e :: complex) ← es. [:- e, 1:]) ∧ diag_mat B = es" using assms es B by (auto simp add: unitary_schur_decomposition) then show ?thesis by auto qed lemma normal_upper_triangular_matrix_is_diagonal: fixes A :: "'a::conjugatable_ordered_field mat" assumes "A ∈ carrier_mat n n" and tri: "upper_triangular A" and norm: "A * adjoint A = adjoint A * A" shows "diagonal_mat A" proof (rule disjE[of "n = 0" "n > 0"], blast) have dim: "dim_row A = n" "dim_col A = n" using assms by auto from norm have eq0: "⋀i j. (A * adjoint A)$$(i,j) = (adjoint A * A)$$(i,j)" by auto have nat_induct_strong: "⋀P. (P::nat⇒bool) 0 ⟹ (⋀i. i < n ⟹ (⋀k. k < i ⟹ P k) ⟹ P i) ⟹ (⋀i. i < n ⟹ P i)" by (metis dual_order.strict_trans infinite_descent0 linorder_neqE_nat) show "n = 0 ⟹ ?thesis" using dim unfolding diagonal_mat_def by auto show "n > 0 ⟹ ?thesis" unfolding diagonal_mat_def dim apply (rule allI, rule impI) apply (rule nat_induct_strong) proof (rule allI, rule impI, rule impI) assume asm: "n > 0" from tri upper_triangularD[of A 0 j] dim have z0: "⋀j. 0< j ⟹ j < n ⟹ A$$(j, 0) = 0" by auto then have ada00: "(adjoint A * A)$$(0,0) = conjugate (A$$