# Theory Spectral_Theory_Complements

(*
Author:
Mnacho Echenim, Université Grenoble Alpes
*)

theory Spectral_Theory_Complements imports "HOL-Combinatorics.Permutations"
"Projective_Measurements.Linear_Algebra_Complements"
"Projective_Measurements.Projective_Measurements"

begin
section ‹Some preliminary results›

subsection ‹Roots of a polynomial›

text ‹Results on polynomials, the main one being that
the set of roots of a polynomial is uniquely defined.›

lemma root_poly_linear:
shows "poly (∏a←L. [:- a, 1:]) (c::'a :: field) = 0 ⟹ c∈ set L"
proof (induct L)
case Nil
thus ?case using Nil by simp
next
case (Cons a L)
show ?case
proof (cases "poly (∏a←L. [:- a, 1:]) c = 0")
case True
then show ?thesis using Cons by auto
next
case False
hence "poly [:- a, 1:] c = 0" using Cons by auto
hence "a = c" by auto
thus ?thesis by auto
qed
qed

lemma poly_root_set_subseteq:
assumes "(∏(a::'a::field)←L. [:- a, 1:]) = (∏a←M. [:- a, 1:])"
shows "set L ⊆ set M"
proof
fix x
assume "x∈ set L"
hence "poly (∏(a::'a::field)←L. [:- a, 1:]) x = 0" using linear_poly_root[of x] by simp
hence "poly (∏(a::'a::field)←M. [:- a, 1:]) x = 0" using assms by simp
thus "x∈ set M" using root_poly_linear[of M] by simp
qed

lemma poly_root_set_eq:
assumes "(∏(a::'a::field)←L. [:- a, 1:]) = (∏a←M. [:- a, 1:])"
shows "set L = set M" using assms poly_root_set_subseteq

subsection ‹Linear algebra preliminaries›

lemma minus_zero_vec_eq:
assumes "dim_vec v = n"
and "dim_vec w = n"
and "v - w = 0⇩v n"
shows "v = w"
proof -
have "v = v - w + w" using assms
zero_minus_vec)
also have "... = 0⇩v n + w" using assms by simp
also have "... = w" using assms left_zero_vec[of w n]
by (metis carrier_vec_dim_vec)
finally show ?thesis .
qed

lemma right_minus_zero_mat:
shows "A - 0⇩m (dim_row A) (dim_col A) = A"
by (intro eq_matI, auto)

lemma smult_zero:
shows "(0::'a::comm_ring) ⋅⇩m A = 0⇩m (dim_row A) (dim_col A)" by auto

lemma  rank_1_proj_col_carrier:
assumes "i < dim_col A"
shows "rank_1_proj (Matrix.col A i) ∈ carrier_mat (dim_row A) (dim_row A)"
proof -
have "dim_vec (Matrix.col A i) = dim_row A" by simp
thus ?thesis by (metis rank_1_proj_carrier)
qed

shows "Complex_Matrix.adjoint (0⇩m n m) = ((0⇩m m n):: 'a::conjugatable_field Matrix.mat)"

lemma assoc_mat_mult_vec':
assumes "A ∈ carrier_mat n n"
and "B∈ carrier_mat n n"
and "C∈ carrier_mat n n"
and "v∈ carrier_vec n"
shows "A * B * C *⇩v v = A *⇩v (B *⇩v (C *⇩v v))" using assms
by (smt (z3) assoc_mult_mat_vec mult_carrier_mat mult_mat_vec_carrier)

"A ∈ carrier_mat n m ⟹ Complex_Matrix.adjoint A ∈ carrier_mat m n"

definition mat_conj where
"mat_conj U V = U * V * (Complex_Matrix.adjoint U)"

shows "mat_conj (Complex_Matrix.adjoint U) V =
Complex_Matrix.adjoint U * V * U" unfolding mat_conj_def

lemma map2_mat_conj_exp:
assumes "length A = length B"
shows "map2 (*) (map2 (*) A B) (map Complex_Matrix.adjoint A) =
map2 mat_conj A B"  using assms
proof (induct A arbitrary: B)
case Nil
then show ?case by simp
next
case (Cons a A)
hence "0 < length B" by auto
hence "B = hd B # (tl B)" by simp
hence "length (tl B) = length A" using Cons by simp
have "map2 (*) (map2 (*) (a # A) B) (map Complex_Matrix.adjoint (a # A)) =
a * hd B * Complex_Matrix.adjoint a #
map2 (*) (map2 (*) A (tl B)) (map Complex_Matrix.adjoint A)"
by (metis (no_types, lifting) ‹B = hd B # tl B› list.map(2)
split_conv zip_Cons_Cons)
also have "... = mat_conj a (hd B) # map2 mat_conj A (tl B)"
using Cons ‹length (tl B) = length A›
unfolding mat_conj_def
by presburger
also have "... = map2 mat_conj (a#A) B" using ‹B = hd B # (tl B)›
by (metis (no_types, opaque_lifting) list.map(2) prod.simps(2)
zip_Cons_Cons)
finally show ?case .
qed

lemma mat_conj_unit_commute:
assumes "unitary U"
and "U*A = A*U"
and "A∈ carrier_mat n n"
and "U∈ carrier_mat n n"
shows "mat_conj U A = A"
proof -
have "mat_conj U A = A*U * Complex_Matrix.adjoint U" using assms
unfolding mat_conj_def by simp
also have "... = A * (U * Complex_Matrix.adjoint U)"
proof (rule assoc_mult_mat, auto simp add: assms)
show "U ∈ carrier_mat (dim_col A) (dim_col U)"
using assms(3) assms(4) by auto
qed
also have "... = A" using assms by simp
finally show ?thesis .
qed

lemma hermitian_mat_conj:
assumes "A∈ carrier_mat n n"
and "U ∈ carrier_mat n n"
and "hermitian A"
shows "hermitian (mat_conj U A)"
proof -
U * Complex_Matrix.adjoint (U * A)"
also have "... = U * A * Complex_Matrix.adjoint U"
by (metis adjoint_dim' assms assoc_mult_mat hermitian_def)
finally show ?thesis unfolding hermitian_def mat_conj_def .
qed

lemma hermitian_mat_conj':
assumes "A∈ carrier_mat n n"
and "U ∈ carrier_mat n n"
and "hermitian A"
shows "hermitian (mat_conj (Complex_Matrix.adjoint U) A)"
carrier_matD(1) carrier_matD(2) carrier_mat_triv hermitian_mat_conj)

lemma mat_conj_uminus_eq:
assumes "A∈ carrier_mat n n"
and "U∈ carrier_mat n n"
and "B ∈ carrier_mat n n"
and "A = mat_conj U B"
shows "-A = mat_conj U (-B)" using assms unfolding mat_conj_def by auto

lemma mat_conj_smult:
assumes "A∈ carrier_mat n n"
and "U∈ carrier_mat n n"
and "B ∈ carrier_mat n n"
and "A = U * B * (Complex_Matrix.adjoint U)"
shows "x  ⋅⇩m A = U * (x  ⋅⇩m B) * (Complex_Matrix.adjoint U)" using assms mult_smult_distrib
by (smt (z3) adjoint_dim' mult_carrier_mat mult_smult_assoc_mat)

fixes A::"'a::conjugatable_field Matrix.mat"
assumes "A∈ carrier_mat n m"
shows "hermitian ((Complex_Matrix.adjoint A) * A)" unfolding hermitian_def
proof -
define C where "C = (Complex_Matrix.adjoint A) * A"
also have "... = Complex_Matrix.adjoint A * A" using assms
finally show "Complex_Matrix.adjoint C = C" using C_def by simp
qed

lemma hermitian_square_hermitian:
fixes A::"'a::conjugatable_field Matrix.mat"
assumes "hermitian A"
shows "hermitian (A * A)"
proof -
using adjoint_mult by (metis assms hermitian_square)
also have "... = A * A" using assms unfolding hermitian_def by simp
finally show ?thesis unfolding hermitian_def .
qed

section ‹Properties of the spectrum of a matrix›

subsection ‹Results on diagonal matrices›

lemma diagonal_mat_uminus:
fixes A::"'a::{ring} Matrix.mat"
assumes "diagonal_mat A"
shows "diagonal_mat (-A)" using assms unfolding diagonal_mat_def uminus_mat_def by auto

lemma diagonal_mat_smult:
fixes A::"'a::{ring} Matrix.mat"
assumes "diagonal_mat A"
shows "diagonal_mat (x ⋅⇩mA)" using assms unfolding diagonal_mat_def uminus_mat_def by auto

lemma diagonal_imp_upper_triangular:
assumes "diagonal_mat A"
and "A ∈ carrier_mat n n"
shows "upper_triangular A"  unfolding  upper_triangular_def
proof (intro allI impI)
fix i j
assume "i < dim_row A" and "j < i"
hence "j < dim_col A" "j ≠ i" using assms by auto
thus "A $$(i,j) = 0" using assms ‹i < dim_row A› unfolding diagonal_mat_def by simp qed lemma set_diag_mat_uminus: assumes "A∈ carrier_mat n n" shows "set (diag_mat (-A)) = {-a |a. a∈ set (diag_mat A)}" (is "?L = ?R") proof show "?L ⊆ ?R" proof fix x assume "x ∈ set (diag_mat (- A))" hence "∃i < length (diag_mat (-A)). nth (diag_mat (-A)) i = x" using in_set_conv_nth[of x] by simp from this obtain i where "i < length (diag_mat (-A))" and "nth (diag_mat (-A)) i = x" by auto note iprop = this hence "i < dim_row (-A)" unfolding diag_mat_def by simp hence "i < n" using assms by simp have "x = (-A)$$(i,i)" using iprop unfolding diag_mat_def by simp
also have "... = - A$$(i,i)" using ‹i < n› assms unfolding uminus_mat_def by auto also have "... ∈ ?R" using iprop assms ‹i < n› in_set_conv_nth[of "A$$(i,i)"] by (metis (mono_tags, lifting) carrier_matD(1)
diag_elems_mem diag_elems_set_diag_mat mem_Collect_eq)
finally show "x ∈ ?R" .
qed
next
show "?R ⊆ ?L"
proof
fix x
assume "x∈ ?R"
hence "∃i < length (diag_mat A). -(nth (diag_mat A)  i) = x"
using in_set_conv_nth[of x] by (smt (z3) in_set_conv_nth mem_Collect_eq)
from this obtain i where "i < length (diag_mat A)" and "-(nth (diag_mat A)  i) = x"
by auto note iprop = this
hence "i < dim_row (-A)" unfolding diag_mat_def by simp
hence "i < n" using assms by simp
have "x = -A$$(i,i)" using iprop unfolding diag_mat_def by simp also have "... = (- A)$$(i,i)" using ‹i < n› assms unfolding uminus_mat_def by auto
also have "... ∈ ?L" using iprop assms ‹i < n›
in_set_conv_nth[of "A$$(i,i)"] by (metis ‹i < dim_row (- A)› diag_elems_mem diag_elems_set_diag_mat) finally show "x ∈ ?L" . qed qed lemma set_diag_mat_smult: assumes "A∈ carrier_mat n n" shows "set (diag_mat (x ⋅⇩m A)) = {x * a |a. a∈ set (diag_mat A)}" (is "?L = ?R") proof show "?L ⊆ ?R" proof fix b assume "b ∈ set (diag_mat (x ⋅⇩m A))" hence "∃i < length (diag_mat (x ⋅⇩m A)). nth (diag_mat (x ⋅⇩m A)) i = b" using in_set_conv_nth[of b] by simp from this obtain i where "i < length (diag_mat (x ⋅⇩m A))" and "nth (diag_mat (x ⋅⇩m A)) i = b" by auto note iprop = this hence "i < dim_row (x ⋅⇩m A)" unfolding diag_mat_def by simp hence "i < n" using assms by simp have "b = (x ⋅⇩m A)$$(i,i)" using iprop unfolding diag_mat_def by simp
also have "... = x * A$$(i,i)" using ‹i < n› assms unfolding uminus_mat_def by auto also have "... ∈ ?R" using iprop assms ‹i < n› in_set_conv_nth[of "A$$(i,i)"]
by (metis (mono_tags, lifting) carrier_matD(1) diag_elems_mem diag_elems_set_diag_mat
mem_Collect_eq)
finally show "b ∈ ?R" .
qed
next
show "?R ⊆ ?L"
proof
fix b
assume "b∈ ?R"
hence "∃i < length (diag_mat A). x * (nth (diag_mat A)  i) = b"
using in_set_conv_nth[of x] by (smt (z3) in_set_conv_nth mem_Collect_eq)
from this obtain i where "i < length (diag_mat A)" and "x * (nth (diag_mat A)  i) = b"
by auto note iprop = this
hence "i < dim_row (x ⋅⇩m A)" unfolding diag_mat_def by simp
hence "i < n" using assms by simp
have "b = x *A$$(i,i)" using iprop unfolding diag_mat_def by simp also have "... = (x ⋅⇩m A)$$(i,i)" using ‹i < n› assms unfolding uminus_mat_def by auto
also have "... ∈ ?L" using iprop assms ‹i < n›
in_set_conv_nth[of "A$$(i,i)"] by (metis ‹i < dim_row (x ⋅⇩m A)› diag_elems_mem diag_elems_set_diag_mat) finally show "b ∈ ?L" . qed qed lemma diag_mat_diagonal_eq: assumes "diag_mat A = diag_mat B" and "diagonal_mat A" and "diagonal_mat B" and "dim_col A = dim_col B" shows "A = B" proof show c: "dim_col A = dim_col B" using assms by simp show r: "dim_row A = dim_row B" using assms unfolding diag_mat_def proof - assume "map (λi. A$$ (i, i)) [0..<dim_row A] = map (λi. B $$(i, i)) [0..<dim_row B]" then show ?thesis by (metis (lifting) length_map length_upt verit_minus_simplify(2)) qed fix i j assume "i < dim_row B" and "j < dim_col B" show "A$$ (i, j) = B $$(i, j)" proof (cases "i = j") case False thus ?thesis using assms c r unfolding diagonal_mat_def by (simp add: ‹dim_row A = dim_row B› ‹i ≠ j› ‹i < dim_row B› ‹j < dim_col B›) next case True hence "A$$ (i,j) = A $$(i,i)" by simp also have "... = (diag_mat A)!i" using c r ‹i < dim_row B› unfolding diag_mat_def by simp also have "... = (diag_mat B)!i" using assms by simp also have "... = B$$(i,i)"  using c r ‹i < dim_row B› unfolding diag_mat_def by simp
also have "... = B $$(i,j)" using True by simp finally show "A$$(i,j) = B $$(i,j)" . qed qed lemma diag_elems_ne: assumes "B ∈ carrier_mat n n" and "0 < n" shows "diag_elems B ≠ {}" proof - have "B$$(0,0) ∈ diag_elems B" using assms by simp
thus ?thesis by auto
qed

lemma diagonal_mat_mult_vec:
fixes B::"'a::conjugatable_field Matrix.mat"
assumes "diagonal_mat B"
and "B ∈ carrier_mat n n"
and "v∈ carrier_vec n"
and "i < n"
shows "vec_index (B *⇩v v) i = B $$(i,i) * (vec_index v i)" proof - have "vec_index (B *⇩v v) i = Matrix.scalar_prod (Matrix.row B i) v" using mult_mat_vec_def assms by simp also have "... = (∑ j ∈ {0 ..< n}. vec_index (Matrix.row B i) j * (vec_index v j))" using Matrix.scalar_prod_def assms(3) carrier_vecD by blast also have "... = (∑ j ∈ {0 ..< n}. B$$ (i,j) * (vec_index v j))"
proof -
have "⋀j. j < n ⟹ vec_index (Matrix.row B i) j = B $$(i,j)" using assms by auto thus ?thesis by auto qed also have "... = B$$ (i,i) * (vec_index v i)"
proof (rule sum_but_one, (auto simp add: assms))
show "⋀j. j < n ⟹ j ≠ i ⟹ B $$(i, j) = 0" using assms unfolding diagonal_mat_def by force qed finally show ?thesis . qed lemma diagonal_mat_mult_index: fixes B::"'a::{ring} Matrix.mat" assumes "diagonal_mat A" and "A∈ carrier_mat n n" and "B ∈ carrier_mat n n" and "i < n" and "j < n" shows "(A * B)$$ (i,j) = A$$(i,i) * B$$(i,j)" unfolding diagonal_mat_def
proof -
have "dim_row (A * B) = n" using assms by simp
have "dim_col (A * B) = n" using  assms by simp
have jvec: "⋀j. j < n ⟹ dim_vec (Matrix.col B j) = n" using assms by simp
have "(A * B) $$(i,j) = Matrix.scalar_prod (Matrix.row A i) (Matrix.col B j)" using assms by (metis carrier_matD(1) carrier_matD(2) index_mult_mat(1)) also have "... = (∑ k ∈ {0 ..< n}. vec_index (Matrix.row A i) k * vec_index (Matrix.col B j) k)" using assms jvec unfolding Matrix.scalar_prod_def by simp also have "... = vec_index (Matrix.row A i) i * vec_index (Matrix.col B j) i" proof (rule sum_but_one) show "i < n" using assms ‹dim_row (A * B) = n› by simp show "∀k<n. k ≠ i ⟶ vec_index (Matrix.row A i) k = 0" using assms ‹i < n› unfolding diagonal_mat_def by auto qed also have "... = A$$(i,i) * B$$(i,j)" using assms by (metis carrier_matD(1) carrier_matD(2) index_col index_row(1)) finally show ?thesis . qed lemma diagonal_mat_mult_index': fixes A::"'a::comm_ring Matrix.mat" assumes "A ∈ carrier_mat n n" and "B∈ carrier_mat n n" and "diagonal_mat B" and "j < n" and "i < n" shows "(A*B)$$(i,j) = B$$(j,j) *A$$ (i, j)"
(*"(B*A) $$(i,j) = B$$(i,i) *A $$(i, j)"*) proof - have "(A*B)$$ (i,j) = Matrix.scalar_prod (Matrix.row A i) (Matrix.col B j)" using assms
times_mat_def[of A] by simp
also have "... = Matrix.scalar_prod (Matrix.col B j) (Matrix.row A i)"
using comm_scalar_prod[of "Matrix.row A i" n] assms by auto
also have "... = (Matrix.vec_index (Matrix.col B j) j) * (Matrix.vec_index  (Matrix.row A i) j)"
unfolding Matrix.scalar_prod_def
proof (rule sum_but_one)
show "j < dim_vec (Matrix.row A i)" using assms by simp
show "∀ia<dim_vec (Matrix.row A i). ia ≠ j ⟶ Matrix.vec_index (Matrix.col B j) ia = 0"
using assms
by (metis carrier_matD(1) carrier_matD(2) diagonal_mat_def index_col index_row(2))
qed
also have "... = B $$(j,j) * A$$(i,j)" using assms by auto
finally show "(A * B) $$(i, j) = B$$ (j, j) * A $$(i, j)" . qed lemma diagonal_mat_times_diag: assumes "A∈ carrier_mat n n" and "B∈ carrier_mat n n" and "diagonal_mat A" and "diagonal_mat B" shows "diagonal_mat (A*B)" unfolding diagonal_mat_def proof (intro allI impI) fix i j assume "i < dim_row (A * B)" and "j < dim_col (A * B)" and "i ≠ j" thus "(A * B)$$ (i, j) = 0" using assms diag_mat_mult_diag_mat[of A n B]
by simp
qed

lemma diagonal_mat_commute:
fixes A::"'a::{comm_ring} Matrix.mat"
assumes "A∈ carrier_mat n n"
and "B∈ carrier_mat n n"
and "diagonal_mat A"
and "diagonal_mat B"
shows "A * B = B * A"
proof (rule eq_matI)
show "dim_row (A * B) = dim_row (B * A)" using assms by simp
show "dim_col (A * B) = dim_col (B * A)" using assms by simp
have bac: "B*A ∈ carrier_mat n n" using assms by simp
fix i j
assume "i < dim_row (B*A)" and "j < dim_col (B*A)" note ij = this
have "(A * B) $$(i, j) = A$$ (i, j) * B$$(i,j)" using ij diagonal_mat_mult_index assms bac by (metis carrier_matD(1) carrier_matD(2) diagonal_mat_def mult_zero_right) also have "... = B$$(i,j) * A $$(i, j)" by (simp add: Groups.mult_ac(2)) also have "... = (B*A)$$ (i,j)" using ij diagonal_mat_mult_index assms bac
by (metis carrier_matD(1) carrier_matD(2) diagonal_mat_def mult_not_zero)
finally show "(A * B) $$(i, j) = (B*A)$$ (i,j)" .
qed

lemma diagonal_mat_sq_index:
fixes B::"'a::{ring} Matrix.mat"
assumes "diagonal_mat B"
and "B ∈ carrier_mat n n"
and "i < n"
and "j < n"
shows "(B * B) $$(i,j) = B$$(i,i) * B$$(j,i)" proof - have "(B * B)$$ (i,j) = B$$(i,i) * B$$(i,j)"
using assms diagonal_mat_mult_index[of B] by simp
also have "... = B$$(i,i) * B$$(j,i)" using assms unfolding diagonal_mat_def
by (metis carrier_matD(1) carrier_matD(2))
finally show ?thesis .
qed

lemma diagonal_mat_sq_index':
fixes B::"'a::{ring} Matrix.mat"
assumes "diagonal_mat B"
and "B ∈ carrier_mat n n"
and "i < n"
and "j < n"
shows "(B * B) $$(i,j) = B$$(i,j) * B$$(i,j)" proof - have eq: "(B * B)$$ (i,j) = B$$(i,i) * B$$(j,i)"
using assms diagonal_mat_sq_index by metis
show ?thesis
proof (cases "i = j")
case True
then show ?thesis using eq by simp
next
case False
hence "B$$(i,j) = 0" using assms unfolding diagonal_mat_def by simp hence "(B * B)$$ (i,j) = 0" using eq
by (metis assms diagonal_mat_mult_index mult_not_zero)
thus ?thesis using eq ‹B$$(i,j) = 0› by simp qed qed lemma diagonal_mat_sq_diag: fixes B::"'a::{ring} Matrix.mat" assumes "diagonal_mat B" and "B ∈ carrier_mat n n" shows "diagonal_mat (B * B)" unfolding diagonal_mat_def proof (intro allI impI) have "dim_row (B * B) = n" using assms by simp have "dim_col (B * B) = n" using assms by simp have jvec: "⋀j. j < n ⟹ dim_vec (Matrix.col B j) = n" using assms by simp fix i j assume "i < dim_row (B * B)" and "j < dim_col (B * B)" and "i ≠ j" note ijprops = this thus "(B * B)$$ (i,j) = 0" using diagonal_mat_sq_index
by (metis ‹dim_col (B * B) = n› ‹dim_row (B * B) = n› assms(1) assms(2) carrier_matD(1)
carrier_matD(2) diagonal_mat_def mult_not_zero)
qed

lemma real_diagonal_hermitian:
fixes B::"complex Matrix.mat"
assumes "B∈ carrier_mat n n"
and "diagonal_mat B"
and "∀i < dim_row B. B$$(i, i) ∈ Reals" shows "hermitian B" unfolding hermitian_def proof (rule eq_matI) show "dim_row (Complex_Matrix.adjoint B) = dim_row B" using assms by auto show "dim_col (Complex_Matrix.adjoint B) = dim_col B" using assms by auto next fix i j assume "i < dim_row B" and "j < dim_col B" note ij = this show "Complex_Matrix.adjoint B$$ (i, j) = B $$(i, j)" proof (cases "i = j") case True thus ?thesis using assms ij Reals_cnj_iff unfolding diagonal_mat_def Complex_Matrix.adjoint_def by simp next case False then show ?thesis using assms ij unfolding diagonal_mat_def Complex_Matrix.adjoint_def by simp qed qed subsection ‹Unitary equivalence› definition unitarily_equiv where "unitarily_equiv A B U ≡ (unitary U ∧ similar_mat_wit A B U (Complex_Matrix.adjoint U))" lemma unitarily_equivD: assumes "unitarily_equiv A B U" shows "unitary U" "similar_mat_wit A B U (Complex_Matrix.adjoint U)" using assms unfolding unitarily_equiv_def by auto lemma unitarily_equivI: assumes "similar_mat_wit A B U (Complex_Matrix.adjoint U)" and "unitary U" shows "unitarily_equiv A B U" using assms unfolding unitarily_equiv_def by simp lemma unitarily_equivI': assumes "A = mat_conj U B" and "unitary U" and "A∈ carrier_mat n n" and "B∈ carrier_mat n n" shows "unitarily_equiv A B U" using assms unfolding unitarily_equiv_def similar_mat_wit_def by (metis (mono_tags, opaque_lifting) Complex_Matrix.unitary_def carrier_matD(1) empty_subsetI index_mult_mat(2) index_one_mat(2) insert_commute insert_subset unitary_adjoint unitary_simps(1) unitary_simps(2) mat_conj_def) lemma unitarily_equiv_carrier: assumes "A∈ carrier_mat n n" and "unitarily_equiv A B U" shows "B ∈ carrier_mat n n" "U∈ carrier_mat n n" proof - show "B ∈ carrier_mat n n" by (metis assms carrier_matD(1) similar_mat_witD(5) unitarily_equivD(2)) show "U ∈ carrier_mat n n" by (metis assms similar_mat_witD2(6) unitarily_equivD(2)) qed lemma unitarily_equiv_carrier': assumes "unitarily_equiv A B U" shows "A ∈ carrier_mat (dim_row A) (dim_row A)" "B ∈ carrier_mat (dim_row A) (dim_row A)" "U∈ carrier_mat (dim_row A) (dim_row A)" proof - show "A ∈ carrier_mat (dim_row A) (dim_row A)" by (metis assms carrier_mat_triv similar_mat_witD2(4) unitarily_equivD(2)) thus "U ∈ carrier_mat (dim_row A) (dim_row A)" using assms unitarily_equiv_carrier(2) by blast show "B ∈ carrier_mat (dim_row A) (dim_row A)" by (metis assms similar_mat_witD(5) unitarily_equivD(2)) qed lemma unitarily_equiv_eq: assumes "unitarily_equiv A B U" shows "A = U * B * (Complex_Matrix.adjoint U)" using assms unfolding unitarily_equiv_def similar_mat_wit_def by meson lemma unitarily_equiv_smult: assumes "A∈ carrier_mat n n" and "unitarily_equiv A B U" shows "unitarily_equiv (x ⋅⇩m A) (x ⋅⇩m B) U" proof (rule unitarily_equivI) show "similar_mat_wit (x ⋅⇩m A) (x ⋅⇩m B) U (Complex_Matrix.adjoint U)" using mat_conj_smult assms by (simp add: similar_mat_wit_smult unitarily_equivD(2)) show "unitary U" using assms unitarily_equivD(1)[of A] by simp qed lemma unitarily_equiv_uminus: assumes "A∈ carrier_mat n n" and "unitarily_equiv A B U" shows "unitarily_equiv (-A) (-B) U" proof (rule unitarily_equivI) show "similar_mat_wit (-A) (-B) U (Complex_Matrix.adjoint U)" using mat_conj_uminus_eq assms by (smt (z3) adjoint_dim_col adjoint_dim_row carrier_matD(1) carrier_matD(2) carrier_mat_triv index_uminus_mat(2) index_uminus_mat(3) similar_mat_witI unitarily_equivD(1) unitarily_equiv_carrier(1) unitarily_equiv_carrier(2) unitarily_equiv_eq unitary_simps(1) unitary_simps(2) mat_conj_def) show "unitary U" using assms unitarily_equivD(1)[of A] by simp qed lemma unitarily_equiv_adjoint: assumes "unitarily_equiv A B U" shows "unitarily_equiv B A (Complex_Matrix.adjoint U)" unfolding unitarily_equiv_def proof show "Complex_Matrix.unitary (Complex_Matrix.adjoint U)" using Complex_Matrix.unitary_def assms unitarily_equiv_def unitary_adjoint by blast have "similar_mat_wit B A (Complex_Matrix.adjoint U) U" unfolding similar_mat_wit_def Let_def proof (intro conjI) show car: "{B, A, Complex_Matrix.adjoint U, U} ⊆ carrier_mat (dim_row B) (dim_row B)" by (metis assms insert_commute similar_mat_wit_def similar_mat_wit_dim_row unitarily_equivD(2)) show "Complex_Matrix.adjoint U * U = 1⇩m (dim_row B)" using car by (meson assms insert_subset unitarily_equivD(1) unitary_simps(1)) show "U * Complex_Matrix.adjoint U = 1⇩m (dim_row B)" by (meson assms similar_mat_wit_def similar_mat_wit_sym unitarily_equivD(2)) have "Complex_Matrix.adjoint U * A * U = Complex_Matrix.adjoint U * (U * B * Complex_Matrix.adjoint U) * U" using assms unitarily_equiv_eq by auto also have "... = B" by (metis assms similar_mat_wit_def similar_mat_wit_sym unitarily_equivD(2)) finally show "B = Complex_Matrix.adjoint U * A * U" by simp qed thus "similar_mat_wit B A (Complex_Matrix.adjoint U) (Complex_Matrix.adjoint (Complex_Matrix.adjoint U))" by (simp add: Complex_Matrix.adjoint_adjoint) qed lemma unitary_mult_conjugate: assumes "A ∈ carrier_mat n n" and "V∈ carrier_mat n n" and "U∈ carrier_mat n n" and "B∈ carrier_mat n n" and "unitary V" and "mat_conj (Complex_Matrix.adjoint V) A = mat_conj U B" shows "A = V* U * B * Complex_Matrix.adjoint (V * U)" proof - have "Complex_Matrix.adjoint V *A * V ∈ carrier_mat n n" using assms by (metis adjoint_dim_row carrier_matD(2) carrier_mat_triv index_mult_mat(2) index_mult_mat(3)) have "A * V = V * (Complex_Matrix.adjoint V) * (A * V)" using assms by simp also have "... = V * (Complex_Matrix.adjoint V *(A * V))" proof (rule assoc_mult_mat, auto simp add: assms) show "A * V ∈ carrier_mat (dim_row V) (dim_row V)" using assms by auto qed also have "... = V * (Complex_Matrix.adjoint V *A * V)" by (metis adjoint_dim' assms(1) assms(2) assoc_mult_mat) also have "... = V * (U * B * (Complex_Matrix.adjoint U))" using assms by (simp add: Complex_Matrix.adjoint_adjoint mat_conj_def) also have "... = V * (U * (B * (Complex_Matrix.adjoint U)))" by (metis adjoint_dim' assms(3) assms(4) assoc_mult_mat) also have "... = V * U * (B * (Complex_Matrix.adjoint U))" proof (rule assoc_mult_mat[symmetric], auto simp add: assms) show "U ∈ carrier_mat (dim_col V) (dim_row B)" using assms by auto qed also have "... = V * U * B * (Complex_Matrix.adjoint U)" proof (rule assoc_mult_mat[symmetric], auto simp add: assms) show "B ∈ carrier_mat (dim_col U) (dim_col U)" using assms by auto qed finally have eq: "A * V = V * U * B * (Complex_Matrix.adjoint U)" . have "A = A * (V * Complex_Matrix.adjoint V)" using assms by simp also have "... = A * V * Complex_Matrix.adjoint V" proof (rule assoc_mult_mat[symmetric], auto simp add: assms) show "V ∈ carrier_mat (dim_col A) (dim_col V)" using assms by auto qed also have "... = V * U * B * (Complex_Matrix.adjoint U) * (Complex_Matrix.adjoint V)" using eq by simp also have "... = V * U * B * ((Complex_Matrix.adjoint U) * (Complex_Matrix.adjoint V))" proof (rule assoc_mult_mat, auto simp add: assms) show "Complex_Matrix.adjoint U ∈ carrier_mat (dim_col B) (dim_col V)" using adjoint_dim' assms by auto qed also have "... = V* U * B * Complex_Matrix.adjoint (V * U)" by (metis adjoint_mult assms(2) assms(3)) finally show ?thesis . qed lemma unitarily_equiv_conjugate: assumes "A∈ carrier_mat n n" and "V∈ carrier_mat n n" and "U ∈ carrier_mat n n" and "B∈ carrier_mat n n" and "unitarily_equiv (mat_conj (Complex_Matrix.adjoint V) A) B U" and "unitary V" shows "unitarily_equiv A B (V * U)" unfolding unitarily_equiv_def proof show "Complex_Matrix.unitary (V*U)" using assms by (simp add: unitarily_equivD(1) unitary_times_unitary) show "similar_mat_wit A B (V*U) (Complex_Matrix.adjoint (V*U))" unfolding similar_mat_wit_def Let_def proof (intro conjI) show "{A, B, V*U, Complex_Matrix.adjoint (V*U)} ⊆ carrier_mat (dim_row A) (dim_row A)" using assms by auto show "V*U * Complex_Matrix.adjoint (V*U) = 1⇩m (dim_row A)" by (metis Complex_Matrix.unitary_def ‹Complex_Matrix.unitary (V * U)› assms(1) assms(2) carrier_matD(1) index_mult_mat(2) inverts_mat_def) show "Complex_Matrix.adjoint (V * U) * (V * U) = 1⇩m (dim_row A)" by (metis Complex_Matrix.unitary_def ‹Complex_Matrix.unitary (V * U)› ‹V * U * Complex_Matrix.adjoint (V * U) = 1⇩m (dim_row A)› index_mult_mat(2) index_one_mat(2) unitary_simps(1)) show "A = V * U * B * Complex_Matrix.adjoint (V * U)" proof (rule unitary_mult_conjugate[of _ n], auto simp add: assms) show "mat_conj (Complex_Matrix.adjoint V) A = mat_conj U B" using assms by (simp add: mat_conj_def unitarily_equiv_eq) qed qed qed lemma mat_conj_commute: assumes "A ∈ carrier_mat n n" and "B∈ carrier_mat n n" and "U ∈ carrier_mat n n" and "unitary U" and "A*B = B*A" shows "(mat_conj (Complex_Matrix.adjoint U) A) * (mat_conj (Complex_Matrix.adjoint U) B) = (mat_conj (Complex_Matrix.adjoint U) B) * (mat_conj (Complex_Matrix.adjoint U) A)" (is "?L*?R = ?R* ?L") proof - have u: "Complex_Matrix.adjoint U ∈ carrier_mat n n" using assms by (simp add: adjoint_dim') have ca: "Complex_Matrix.adjoint U * A * U ∈ carrier_mat n n" using assms by auto have cb: "Complex_Matrix.adjoint U * B * U ∈ carrier_mat n n" using assms by auto have "?L * ?R = ?L * (Complex_Matrix.adjoint U * (B * U))" proof - have "Complex_Matrix.adjoint U * B * U = Complex_Matrix.adjoint U * (B * U)" using assoc_mult_mat[of _ n n B n U] assms by (meson adjoint_dim') thus ?thesis using mat_conj_adjoint by metis qed also have "... = ?L * Complex_Matrix.adjoint U * (B*U)" proof - have "∃na nb. Complex_Matrix.adjoint U ∈ carrier_mat n na ∧ B * U ∈ carrier_mat na nb" by (metis (no_types) assms(2) carrier_matD(1) carrier_mat_triv index_mult_mat(2) u) then show ?thesis using ca by (metis assoc_mult_mat mat_conj_adjoint) qed also have "... = Complex_Matrix.adjoint U * A* (U * (Complex_Matrix.adjoint U)) * (B * U)" proof - have "Complex_Matrix.adjoint U * A * U * Complex_Matrix.adjoint U = Complex_Matrix.adjoint U * A * (U * Complex_Matrix.adjoint U)" using assoc_mult_mat[of "Complex_Matrix.adjoint U * A" n n] by (metis assms(1) assms(3) mult_carrier_mat u) thus ?thesis by (simp add: mat_conj_adjoint) qed also have "... = Complex_Matrix.adjoint U * A* (B * U)" using assms by auto also have "... = Complex_Matrix.adjoint U * A * B * U" proof (rule assoc_mult_mat[symmetric], auto simp add: assms) show "B ∈ carrier_mat (dim_col A) (dim_row U)" using assms by simp qed also have "... = Complex_Matrix.adjoint U * (A * B) * U" using assms u by auto also have "... = Complex_Matrix.adjoint U * (B * A) * U" using assms by simp also have "... = Complex_Matrix.adjoint U * B * A * U" using assms u by auto also have "... = Complex_Matrix.adjoint U * B * (A * U)" proof (rule assoc_mult_mat, auto simp add: assms) show "A ∈ carrier_mat (dim_col B) (dim_row U)" using assms by simp qed also have "... = Complex_Matrix.adjoint U * B* (U * (Complex_Matrix.adjoint U)) * (A * U)" using assms by auto also have "... = Complex_Matrix.adjoint U * B* U * (Complex_Matrix.adjoint U) * (A * U)" proof - have "Complex_Matrix.adjoint U * B * U * Complex_Matrix.adjoint U = Complex_Matrix.adjoint U * B * (U * Complex_Matrix.adjoint U)" proof (rule assoc_mult_mat, auto simp add: assms) show "U ∈ carrier_mat (dim_col B) (dim_col U)" using assms by simp qed thus ?thesis by simp qed also have "... = Complex_Matrix.adjoint U * B* U * ((Complex_Matrix.adjoint U) * (A * U))" proof (rule assoc_mult_mat, auto simp add: u cb) show "A * U ∈ carrier_mat (dim_row U) n" using assms by simp qed also have "... = Complex_Matrix.adjoint U * B* U * ((Complex_Matrix.adjoint U) * A * U)" proof - have "(Complex_Matrix.adjoint U) * (A * U) = (Complex_Matrix.adjoint U) * A * U" proof (rule assoc_mult_mat[symmetric], auto simp add: assms u) show "A ∈ carrier_mat (dim_row U) (dim_row U)" using assms by simp qed thus ?thesis by simp qed finally show ?thesis by (metis mat_conj_adjoint) qed lemma unitarily_equiv_commute: assumes "unitarily_equiv A B U" and "A*C = C*A" shows "B * (Complex_Matrix.adjoint U * C * U) = Complex_Matrix.adjoint U * C * U * B" proof - note car = unitarily_equiv_carrier'[OF assms(1)] have cr: "dim_row C = dim_col A" by (metis assms(2) car(1) carrier_matD(2) index_mult_mat(2)) have cd: "dim_col C = dim_row A" by (metis ‹dim_row C = dim_col A› assms(2) index_mult_mat(2) index_mult_mat(3)) have "Complex_Matrix.adjoint U * A * U = B" using assms unitarily_equiv_adjoint by (metis Complex_Matrix.adjoint_adjoint unitarily_equiv_eq) thus ?thesis using mat_conj_commute assms car by (metis carrier_matD(2) carrier_matI cd cr mat_conj_adjoint unitarily_equivD(1)) qed definition unitary_diag where "unitary_diag A B U ≡ unitarily_equiv A B U ∧ diagonal_mat B" lemma unitary_diagI: assumes "similar_mat_wit A B U (Complex_Matrix.adjoint U)" and "diagonal_mat B" and "unitary U" shows "unitary_diag A B U" using assms unfolding unitary_diag_def unitarily_equiv_def by simp lemma unitary_diagI': assumes "A∈ carrier_mat n n" and "B∈ carrier_mat n n" and "diagonal_mat B" and "unitary U" and "A = mat_conj U B" shows "unitary_diag A B U" unfolding unitary_diag_def proof show "diagonal_mat B" using assms by simp show "unitarily_equiv A B U" using assms unitarily_equivI' by metis qed lemma unitary_diagD: assumes "unitary_diag A B U" shows "similar_mat_wit A B U (Complex_Matrix.adjoint U)" "diagonal_mat B" "unitary U" using assms unfolding unitary_diag_def unitarily_equiv_def by simp+ lemma unitary_diag_imp_unitarily_equiv[simp]: assumes "unitary_diag A B U" shows "unitarily_equiv A B U" using assms unfolding unitary_diag_def by simp lemma unitary_diag_diagonal[simp]: assumes "unitary_diag A B U" shows "diagonal_mat B" using assms unfolding unitary_diag_def by simp lemma unitary_diag_carrier: assumes "A∈ carrier_mat n n" and "unitary_diag A B U" shows "B ∈ carrier_mat n n" "U∈ carrier_mat n n" proof - show "B ∈ carrier_mat n n" using assms unitarily_equiv_carrier(1)[of A n B U] by simp show "U ∈ carrier_mat n n" using assms unitarily_equiv_carrier(2)[of A n B U] by simp qed lemma unitary_mult_square_eq: assumes "A∈ carrier_mat n n" and "U∈ carrier_mat n n" and "B ∈ carrier_mat n n" and "A = mat_conj U B" and "(Complex_Matrix.adjoint U) * U = 1⇩m n" shows "A * A = mat_conj U (B*B)" proof - have "A * A = U * B * (Complex_Matrix.adjoint U) * (U * B * (Complex_Matrix.adjoint U))" using assms unfolding mat_conj_def by simp also have "... = U * B * ((Complex_Matrix.adjoint U) * U) * (B * (Complex_Matrix.adjoint U))" by (smt (z3) adjoint_dim_col adjoint_dim_row assms(3) assms(5) assoc_mult_mat carrier_matD(2) carrier_mat_triv index_mult_mat(2) index_mult_mat(3) right_mult_one_mat') also have "... = U * B * (B * (Complex_Matrix.adjoint U))" using assms by simp also have "... = U * (B * B) * (Complex_Matrix.adjoint U)" by (smt (z3) adjoint_dim_row assms(2) assms(3) assoc_mult_mat carrier_matD(2) carrier_mat_triv index_mult_mat(3)) finally show ?thesis unfolding mat_conj_def . qed lemma hermitian_square_similar_mat_wit: fixes A::"complex Matrix.mat" assumes "hermitian A" and "A∈ carrier_mat n n" and "unitary_diag A B U" shows "similar_mat_wit (A * A) (B * B) U (Complex_Matrix.adjoint U)" proof - have "B∈ carrier_mat n n" using unitary_diag_carrier[of A] assms by metis hence "B * B∈ carrier_mat n n" by simp have "unitary U" using assms unitary_diagD[of A] by simp have "A * A= mat_conj U (B*B)" using assms unitary_mult_square_eq[of A n] by (metis ‹B ∈ carrier_mat n n› ‹Complex_Matrix.unitary U› mat_conj_def unitarily_equiv_carrier(2) unitarily_equiv_eq unitary_diag_def unitary_simps(1)) moreover have "{A * A, B * B, U, Complex_Matrix.adjoint U} ⊆ carrier_mat n n" by (metis ‹B * B ∈ carrier_mat n n› adjoint_dim' assms(2) assms(3) empty_subsetI insert_subsetI mult_carrier_mat unitary_diag_carrier(2)) moreover have "U * Complex_Matrix.adjoint U = 1⇩m n ∧ Complex_Matrix.adjoint U * U = 1⇩m n" by (meson ‹Complex_Matrix.unitary U› calculation(2) insert_subset unitary_simps(1) unitary_simps(2)) ultimately show ?thesis unfolding similar_mat_wit_def mat_conj_def by auto qed lemma unitarily_equiv_square: assumes "A∈ carrier_mat n n" and "unitarily_equiv A B U" shows "unitarily_equiv (A*A) (B*B) U" proof (rule unitarily_equivI) show "unitary U" using assms unitarily_equivD(1)[of A] by simp show "similar_mat_wit (A * A) (B * B) U (Complex_Matrix.adjoint U)" by (smt (z3) ‹Complex_Matrix.unitary U› assms carrier_matD(1) carrier_matD(2) carrier_mat_triv index_mult_mat(2) index_mult_mat(3) similar_mat_witI unitarily_equiv_carrier(1) unitarily_equiv_carrier(2) unitarily_equiv_eq unitary_mult_square_eq unitary_simps(1) unitary_simps(2) mat_conj_def) qed lemma conjugate_eq_unitarily_equiv: assumes "A∈ carrier_mat n n" and "V∈ carrier_mat n n" and "unitarily_equiv A B U" and "unitary V" and "V * B * (Complex_Matrix.adjoint V) = B" shows "unitarily_equiv A B (U*V)" unfolding unitarily_equiv_def similar_mat_wit_def Let_def proof (intro conjI) have "B∈ carrier_mat n n" using assms(1) assms(3) unitarily_equiv_carrier(1) by blast have "U∈ carrier_mat n n" using assms(1) assms(3) unitarily_equiv_carrier(2) by auto show u: "unitary (U*V)" by (metis Complex_Matrix.unitary_def adjoint_dim_col assms(1) assms(2) assms(3) assms(4) carrier_matD(2) index_mult_mat(3) unitarily_equivD(1) unitarily_equiv_eq unitary_times_unitary) thus l: "U * V * Complex_Matrix.adjoint (U * V) = 1⇩m (dim_row A)" by (metis Complex_Matrix.unitary_def assms(1) assms(2) carrier_matD(1) carrier_matD(2) index_mult_mat(3) inverts_mat_def) thus r: "Complex_Matrix.adjoint (U * V) * (U * V) = 1⇩m (dim_row A)" using u by (metis Complex_Matrix.unitary_def index_mult_mat(2) index_one_mat(2) unitary_simps(1)) show "{A, B, U * V, Complex_Matrix.adjoint (U * V)} ⊆ carrier_mat (dim_row A) (dim_row A)" using ‹B ∈ carrier_mat n n› ‹U ∈ carrier_mat n n› adjoint_dim' assms by auto have "U * V * B * Complex_Matrix.adjoint (U * V) = U * V * B * (Complex_Matrix.adjoint V * Complex_Matrix.adjoint U)" by (metis ‹U ∈ carrier_mat n n› adjoint_mult assms(2)) also have "... = U * V * B * Complex_Matrix.adjoint V * Complex_Matrix.adjoint U" proof (rule assoc_mult_mat[symmetric], auto simp add: assms) show "Complex_Matrix.adjoint V ∈ carrier_mat (dim_col B) (dim_col U)" using ‹B ∈ carrier_mat n n› ‹U ∈ carrier_mat n n› adjoint_dim assms(2) by auto qed also have "... = U * V * B * (Complex_Matrix.adjoint V * Complex_Matrix.adjoint U)" proof (rule assoc_mult_mat, auto simp add: assms) show "Complex_Matrix.adjoint V ∈ carrier_mat (dim_col B) (dim_col U)" by (metis ‹B ∈ carrier_mat n n› ‹U ∈ carrier_mat n n› adjoint_dim' assms(2) carrier_matD(2)) qed also have "... = U * V * (B * (Complex_Matrix.adjoint V * Complex_Matrix.adjoint U))" proof (rule assoc_mult_mat, auto simp add: assms) show "B ∈ carrier_mat (dim_col V) (dim_col V)" by (metis ‹B ∈ carrier_mat n n› assms(2) carrier_matD(2)) qed also have "... = U * (V * (B * (Complex_Matrix.adjoint V * Complex_Matrix.adjoint U)))" proof (rule assoc_mult_mat, auto simp add: assms) show "V ∈ carrier_mat (dim_col U) (dim_row B)" using ‹B ∈ carrier_mat n n› ‹U ∈ carrier_mat n n› assms(2) by auto qed finally have eq: "U * V * B * Complex_Matrix.adjoint (U * V) = U * (V * (B * (Complex_Matrix.adjoint V * Complex_Matrix.adjoint U)))" . have "V * (B * (Complex_Matrix.adjoint V * Complex_Matrix.adjoint U)) = V * B * (Complex_Matrix.adjoint V * Complex_Matrix.adjoint U)" proof (rule assoc_mult_mat[symmetric], auto simp add: assms) show "B ∈ carrier_mat (dim_col V) (dim_col V)" using ‹B ∈ carrier_mat n n› assms(2) by auto qed also have "... = V * B * Complex_Matrix.adjoint V * Complex_Matrix.adjoint U" proof (rule assoc_mult_mat[symmetric], auto simp add: assms) show "Complex_Matrix.adjoint V ∈ carrier_mat (dim_col B) (dim_col U)" by (metis ‹B ∈ carrier_mat n n› ‹U ∈ carrier_mat n n› adjoint_dim_row assms(2) assms(5) carrier_matD(2) carrier_mat_triv index_mult_mat(3)) qed also have "... = B * Complex_Matrix.adjoint U" using assms by simp finally have "V *(B *(Complex_Matrix.adjoint V * Complex_Matrix.adjoint U)) = B* Complex_Matrix.adjoint U" . hence "U * V * B * Complex_Matrix.adjoint (U * V) = U * B * Complex_Matrix.adjoint U" using eq by (metis ‹B ∈ carrier_mat n n› ‹U ∈ carrier_mat n n› adjoint_dim' assoc_mult_mat) also have "... = A" using assms unitarily_equiv_eq[of A B U] by simp finally show "A = U * V * B * Complex_Matrix.adjoint (U * V)" by simp qed definition real_diag_decomp where "real_diag_decomp A B U ≡ unitary_diag A B U ∧ (∀i < dim_row B. B$$(i, i) ∈ Reals)"

lemma real_diag_decompD[simp]:
assumes "real_diag_decomp A B U"
shows "unitary_diag A B U"
"(∀i < dim_row B. B$$(i, i) ∈ Reals)" using assms unfolding real_diag_decomp_def unitary_diag_def by auto lemma hermitian_decomp_decomp': fixes A::"complex Matrix.mat" assumes "hermitian_decomp A B U" shows "real_diag_decomp A B U" using assms unfolding hermitian_decomp_def by (metis real_diag_decomp_def unitarily_equiv_def unitary_diag_def) lemma real_diag_decomp_hermitian: fixes A::"complex Matrix.mat" assumes "real_diag_decomp A B U" shows "hermitian A" proof - have ud: "unitary_diag A B U" using assms real_diag_decompD by simp hence "A = U * B * (Complex_Matrix.adjoint U)" by (simp add: unitarily_equiv_eq) have "Complex_Matrix.adjoint A = Complex_Matrix.adjoint (U * B * (Complex_Matrix.adjoint U))" using ud assms unitarily_equiv_eq unitary_diag_imp_unitarily_equiv by blast also have "... = Complex_Matrix.adjoint (Complex_Matrix.adjoint U) * Complex_Matrix.adjoint B * Complex_Matrix.adjoint U" by (smt (z3) ud Complex_Matrix.adjoint_adjoint Complex_Matrix.unitary_def adjoint_dim_col adjoint_mult assms assoc_mult_mat calculation carrier_matD(2) carrier_mat_triv index_mult_mat(2) index_mult_mat(3) similar_mat_witD2(5) similar_mat_wit_dim_row unitary_diagD(1) unitary_diagD(3)) also have "... = U * Complex_Matrix.adjoint B * Complex_Matrix.adjoint U" by (simp add: Complex_Matrix.adjoint_adjoint) also have "... = U * B * Complex_Matrix.adjoint U" using real_diagonal_hermitian by (metis assms hermitian_def real_diag_decomp_def similar_mat_witD(5) unitary_diagD(1) unitary_diagD(2)) also have "... = A" using ‹A = U * B * (Complex_Matrix.adjoint U)› by simp finally show ?thesis unfolding hermitian_def by simp qed lemma unitary_conjugate_real_diag_decomp: assumes "A∈ carrier_mat n n" and "Us∈ carrier_mat n n" and "unitary Us" and "real_diag_decomp (mat_conj (Complex_Matrix.adjoint Us) A) B U" shows "real_diag_decomp A B (Us * U)" unfolding real_diag_decomp_def proof (intro conjI allI impI) show "⋀i. i < dim_row B ⟹ B$$ (i, i) ∈ ℝ" using assms
unfolding real_diag_decomp_def by simp
show "unitary_diag A B (Us * U)" unfolding unitary_diag_def
proof (rule conjI)
show "diagonal_mat B" using assms real_diag_decompD(1) unitary_diagD(2)
by metis
show "unitarily_equiv A B (Us * U)"
proof (rule unitarily_equiv_conjugate)
show "A∈ carrier_mat n n" using assms by simp
show "unitary Us" using assms by simp
show "Us ∈ carrier_mat n n" using assms by simp
show "unitarily_equiv (mat_conj (Complex_Matrix.adjoint Us) A) B U"
using assms real_diag_decompD(1) unfolding unitary_diag_def by metis
thus "U ∈ carrier_mat n n"
by (metis (mono_tags) adjoint_dim' assms(2) carrier_matD(1)
index_mult_mat(2) mat_conj_def unitarily_equiv_carrier'(3))
show "B∈ carrier_mat n n"
using ‹unitarily_equiv (mat_conj (Complex_Matrix.adjoint Us) A) B U›
assms(2) unitarily_equiv_carrier'(2)
by (metis ‹U ∈ carrier_mat n n› carrier_matD(2)
unitarily_equiv_carrier'(3))
qed
qed
qed

subsection ‹On the spectrum of a matrix›

lemma similar_spectrum_eq:
fixes A::"complex Matrix.mat"
assumes "A∈ carrier_mat n n"
and "similar_mat A B"
and "upper_triangular B"
shows "spectrum A = set (diag_mat B)"
proof -
have "(∏a←(eigvals A). [:- a, 1:]) = char_poly A"
using eigvals_poly_length assms by simp
also have "... = char_poly B"
proof (rule char_poly_similar)
show "similar_mat A B" using assms real_diag_decompD(1)
using similar_mat_def by blast
qed
also have "... = (∏a←diag_mat B. [:- a, 1:])"
proof (rule char_poly_upper_triangular)
show "B∈ carrier_mat n n" using assms similar_matD by auto
thus "upper_triangular B" using assms by simp
qed
finally have "(∏a←(eigvals A). [:- a, 1:]) = (∏a←diag_mat B. [:- a, 1:])" .
thus ?thesis using poly_root_set_eq unfolding spectrum_def by metis
qed

lemma unitary_diag_spectrum_eq:
fixes A::"complex Matrix.mat"
assumes "A∈ carrier_mat n n"
and "unitary_diag A B U"
shows "spectrum A = set (diag_mat B)"
proof (rule similar_spectrum_eq)
show "A ∈ carrier_mat n n" using assms by simp
show "similar_mat A B" using assms unitary_diagD(1)
by (metis similar_mat_def)
show "upper_triangular B" using assms
unitary_diagD(2) unitary_diagD(1)  diagonal_imp_upper_triangular
by (metis similar_mat_witD2(5))
qed

lemma unitary_diag_spectrum_eq':
fixes A::"complex Matrix.mat"
assumes "A∈ carrier_mat n n"
and "unitary_diag A B U"
shows "spectrum A = diag_elems B"
proof -
have "spectrum A = set (diag_mat B)" using assms unitary_diag_spectrum_eq
by simp
also have "... = diag_elems B" using diag_elems_set_diag_mat[of B] by simp
finally show "spectrum A = diag_elems B" .
qed

lemma hermitian_real_diag_decomp:
fixes A::"complex Matrix.mat"
assumes "A∈ carrier_mat n n"
and "0 < n"
and "hermitian A"
obtains B U where "real_diag_decomp A B U"
proof -
{
have es: "char_poly A = (∏ (e :: complex) ← (eigvals A). [:- e, 1:])"
using assms  eigvals_poly_length by auto
obtain B U Q where us: "unitary_schur_decomposition A (eigvals A) = (B,U,Q)"
by (cases "unitary_schur_decomposition A (eigvals A)")
hence pr: "similar_mat_wit A B U (Complex_Matrix.adjoint U) ∧ diagonal_mat B ∧
diag_mat B = (eigvals A) ∧ unitary U ∧ (∀i < n. B(i, i) ∈ Reals)"
using hermitian_eigenvalue_real assms  es by auto
moreover have "dim_row B = n" using assms similar_mat_wit_dim_row[of A]
pr by auto
ultimately have "real_diag_decomp A B U" using unitary_diagI[of A]
unfolding real_diag_decomp_def by simp
hence "∃ B U. real_diag_decomp A B U" by auto
}
thus ?thesis using that by auto
qed

lemma  spectrum_smult:
fixes A::"complex Matrix.mat"
assumes "hermitian A"
and "A∈ carrier_mat n n"
and "0 < n"
shows "spectrum (x ⋅⇩m A) = {x * a|a. a∈ spectrum A}"
proof -
obtain B U where bu: "real_diag_decomp A B U"
using assms hermitian_real_diag_decomp[of A] by auto
hence "spectrum (x ⋅⇩m A) = set (diag_mat (x ⋅⇩m B))"
using assms unitary_diag_spectrum_eq[of "x ⋅⇩m A"]
unitarily_equiv_smult[of A]
by (meson  diagonal_mat_smult real_diag_decompD(1) real_diag_decompD(2)
smult_carrier_mat unitary_diag_def)
also have "... = {x * a |a. a ∈ set (diag_mat B)}"
using assms set_diag_mat_smult[of B n x ]
by (meson bu real_diag_decompD(1) unitary_diag_carrier(1))
also have "... = {x * a|a. a∈ spectrum A}"
using assms unitary_diag_spectrum_eq[of A] bu real_diag_decompD(1)
by metis
finally show ?thesis .
qed

lemma  spectrum_uminus:
fixes A::"complex Matrix.mat"
assumes "hermitian A"
and "A∈ carrier_mat n n"
and "0 < n"
shows "spectrum (-A) = {-a|a. a∈ spectrum A}"
proof -
obtain B U where bu: "real_diag_decomp A B U"
using assms hermitian_real_diag_decomp[of A] by auto
hence "spectrum (-A) = set (diag_mat (-B))"
using assms unitary_diag_spectrum_eq[of "-A"]
unitarily_equiv_uminus[of A]
by (meson diagonal_mat_uminus real_diag_decompD uminus_carrier_iff_mat
unitary_diag_def)
also have "... = {-a |a. a ∈ set (diag_mat B)}"
using assms set_diag_mat_uminus[of B n]
by (meson bu real_diag_decompD(1) unitary_diag_carrier(1))
also have "... = {-a|a. a∈ spectrum A}"
using assms unitary_diag_spectrum_eq[of A] bu real_diag_decompD(1)
by metis
finally show ?thesis .
qed

section ‹Properties of the inner product›

subsection ‹Some analysis complements›

shows "z + cnj z ≤ 2 * cmod z"
proof -
have z: "z + cnj z = 2 * Re z" by (simp add: complex_add_cnj)
have "Re z ≤ cmod z" by (simp add: complex_Re_le_cmod)
hence "2 *complex_of_real (Re z) ≤ 2 * complex_of_real (cmod z)"
using less_eq_complex_def by auto
thus ?thesis using z by simp
qed

lemma abs_real:
fixes x::complex
assumes "x∈ Reals"
shows "abs x ∈ Reals" unfolding abs_complex_def by auto

lemma csqrt_cmod_square:
shows "csqrt ((cmod z)⇧2) = cmod z"
proof -
have "csqrt ((cmod z)⇧2) = sqrt (Re ((cmod z)⇧2))" by force
also have "... = cmod z" by simp
finally show ?thesis .
qed

lemma cpx_real_le:
fixes z::complex
assumes "0 ≤ z"
and "0 ≤ u"
and "z⇧2 ≤ u⇧2"
shows "z ≤ u"
proof -
have "z^2 = Re (z^2)" "u^2 = Re (u^2)" using assms
by (metis Im_complex_of_real Im_power_real Re_complex_of_real
complex_eq_iff less_eq_complex_def zero_complex.sel(2))+
hence rl: "Re (z^2) ≤ Re (u^2)" using assms less_eq_complex_def by simp
have "sqrt (Re (z^2)) = z" "sqrt (Re (u^2)) = u"   using assms complex_eqI
less_eq_complex_def by auto
have "z = sqrt (Re (z^2))" using assms complex_eqI less_eq_complex_def
by auto
also have "... ≤ sqrt (Re (u^2))" using rl less_eq_complex_def by simp
finally show "z ≤ u" using assms complex_eqI less_eq_complex_def by auto
qed

lemma mult_conj_real:
fixes v::complex
shows "v * (conjugate v) ∈ Reals"
proof -
have "0 ≤ v * (conjugate v)" using less_eq_complex_def by simp
thus ?thesis by (simp add: complex_is_Real_iff)
qed

lemma real_sum_real:
assumes "⋀i. i < n ⟹ ((f i)::complex) ∈ Reals"
shows "(∑ i ∈ {0 ..< n}. f i) ∈ Reals"
using assms atLeastLessThan_iff by blast

lemma real_mult_re:
assumes "a∈ Reals" and "b∈ Reals"
shows "Re (a * b) = Re a * Re b" using assms
by (metis Re_complex_of_real Reals_cases of_real_mult)

lemma complex_positive_Im:
fixes b::complex
assumes "0 ≤ b"
shows "Im b = 0"
by (metis assms less_eq_complex_def zero_complex.simps(2))

lemma cmod_pos:
fixes z::complex
assumes "0 ≤ z"
shows "cmod z = z"
proof -
have "Im z = 0" using assms complex_positive_Im by simp
thus ?thesis using complex_norm
by (metis assms complex.exhaust_sel complex_of_real_def less_eq_complex_def norm_of_real
real_sqrt_abs real_sqrt_pow2 real_sqrt_power zero_complex.simps(1))
qed

lemma cpx_pos_square_pos:
fixes z::complex
assumes "0 ≤ z"
shows "0 ≤ z⇧2"
proof -
have "Im z = 0" using assms by (simp add: complex_positive_Im)
hence "Re (z⇧2) = (Re z)⇧2" by simp
moreover have "Im (z⇧2) = 0" by (simp add: ‹Im z = 0›)
ultimately show ?thesis by (simp add: less_eq_complex_def)
qed

lemma cmod_mult_pos:
fixes b:: complex
fixes z::complex
assumes "0 ≤ b"
shows "cmod (b * z) =  Re b * cmod z" using complex_positive_Im
Im_complex_of_real Re_complex_of_real abs_of_nonneg  assms cmod_Im_le_iff
less_eq_complex_def  norm_mult of_real_0
by (metis (full_types) cmod_eq_Re)

lemma cmod_conjugate_square_eq:
fixes z::complex
shows "cmod (z *  (conjugate z)) = z * (conjugate z)"
proof -
have "0 ≤ z * (conjugate z)"
using conjugate_square_positive less_eq_complex_def by auto
thus ?thesis using cmod_pos by simp
qed

lemma pos_sum_gt_comp:
assumes "finite I"
and "⋀i. i ∈ I ⟹ (0::real) ≤ f i"
and "j∈ I"
and "c < f j"
shows "c < sum f I"
proof -
have "c < f j" using assms by simp
also have "... ≤ f j + sum f (I -{j})"
by (smt (z3) DiffD1 assms(2) sum_nonneg)
also have "... = sum f I" using assms
finally show ?thesis .
qed

lemma pos_sum_le_comp:
assumes "finite I"
and "⋀i. i ∈ I ⟹ (0::real) ≤ f i"
and "sum f I ≤ c"
shows "∀i ∈ I. f i ≤ c"
proof (rule ccontr)
assume "¬ (∀i∈I. f i ≤ c)"
hence "∃j∈ I. c < f j" by fastforce
from this obtain j where "j∈ I" and "c < f j" by auto
hence "c < sum f I" using assms pos_sum_gt_comp[of I] by simp
thus False using assms by simp
qed

lemma square_pos_mult_le:
assumes "finite I"
and "⋀i. i ∈ I ⟹ ((0::real) ≤ f i ∧ f i ≤ 1)"
shows "sum (λx. f x * f x) I ≤ sum f I" using assms
proof (induct rule:finite_induct)
case empty
then show ?case by simp
next
case (insert x F)
have "sum (λx. f x * f x) (insert x F) = f x * f x + sum (λx. f x * f x) F"
also have "... ≤ f x * f x + sum f F" using insert by simp
also have "... ≤ f x + sum f F" using insert mult_left_le[of "f x" "f x"]
by simp
also have "... = sum f (insert x F)" using insert by simp
finally show ?case .
qed

lemma square_pos_mult_lt:
assumes "finite I"
and "⋀i. i ∈ I ⟹ ((0::real) ≤ f i ∧ f i ≤ 1)"
and "j ∈ I"
and "f j < 1"
and "0 < f j"
shows "sum (λx. f x * f x) I < sum f I" using assms
proof -
have "sum (λx. f x * f x) I =
sum (λx. f x * f x) {j} + sum (λx. f x * f x) (I-{j})"
using assms sum.remove by fastforce
also have "... = f j * f j + sum (λx. f x * f x) (I-{j})" by simp
also have "... < f j + sum (λx. f x * f x) (I-{j})" using assms by simp
also have "... ≤ f j + sum f (I - {j})"
using assms square_pos_mult_le[of "I - {j}"] by simp
also have "... = sum f I"
by (metis assms(1) assms(3) sum.remove)
finally show ?thesis .
qed

subsection ‹Inner product results›

text ‹In particular we prove the triangle inequality, i.e. that for vectors $u$ and $v$
we have $\| u+ v \| \leq \| u \| + \| v \|$.›

lemma inner_prod_vec_norm_pow2:
shows "(vec_norm v)⇧2 = v ∙c v" using vec_norm_def
by (metis power2_csqrt)

lemma inner_prod_mult_mat_vec_left:
assumes "v