Theory Matrix_Limit
section ‹Matrix limits›
theory Matrix_Limit
imports Complex_Matrix
begin
subsection ‹Definition of limit of matrices›
definition limit_mat :: "(nat ⇒ complex mat) ⇒ complex mat ⇒ nat ⇒ bool" where
"limit_mat X A m ⟷ (∀ n. X n ∈ carrier_mat m m ∧ A ∈ carrier_mat m m ∧
(∀ i < m. ∀ j < m. (λ n. (X n) $$ (i, j)) ⇢ (A $$ (i, j))))"
lemma limit_mat_unique:
assumes limA: "limit_mat X A m" and limB: "limit_mat X B m"
shows "A = B"
proof -
have dim: "A ∈ carrier_mat m m" "B ∈ carrier_mat m m" using limA limB limit_mat_def by auto
{
fix i j assume i: "i < m" and j: "j < m"
have "(λ n. (X n) $$ (i, j)) ⇢ (A $$ (i, j))" using limit_mat_def limA i j by auto
moreover have "(λ n. (X n) $$ (i, j)) ⇢ (B $$ (i, j))" using limit_mat_def limB i j by auto
ultimately have "(A $$ (i, j)) = (B $$ (i, j))" using LIMSEQ_unique by auto
}
then show "A = B" using mat_eq_iff dim by auto
qed
lemma limit_mat_const:
fixes A :: "complex mat"
assumes "A ∈ carrier_mat m m"
shows "limit_mat (λk. A) A m"
unfolding limit_mat_def using assms by auto
lemma limit_mat_scale:
fixes X :: "nat ⇒ complex mat" and A :: "complex mat"
assumes limX: "limit_mat X A m"
shows "limit_mat (λn. c ⋅⇩m X n) (c ⋅⇩m A) m"
proof -
have dimA: "A ∈ carrier_mat m m" using limX limit_mat_def by auto
have dimX: "⋀n. X n ∈ carrier_mat m m" using limX unfolding limit_mat_def by auto
have "⋀i j. i < m ⟹ j < m ⟹ (λn. (c ⋅⇩m X n) $$ (i, j)) ⇢ (c ⋅⇩m A) $$ (i, j)"
proof -
fix i j assume i: "i < m" and j: "j < m"
have "(λn. (X n) $$ (i, j)) ⇢ A$$(i, j)" using limX limit_mat_def i j by auto
moreover have "(λn. c) ⇢ c" by auto
ultimately have "(λn. c * (X n) $$ (i, j)) ⇢ c * A$$(i, j)"
using tendsto_mult[of "λn. c" c] limX limit_mat_def by auto
moreover have "(c ⋅⇩m X n) $$ (i, j) = c * (X n) $$ (i, j)" for n
using index_smult_mat(1)[of i "X n" j c] i j dimX[of n] by auto
moreover have "(c ⋅⇩m A) $$ (i, j) = c * A $$ (i, j)"
using index_smult_mat(1)[of i "A" j c] i j dimA by auto
ultimately show "(λn. (c ⋅⇩m X n) $$ (i, j)) ⇢ (c ⋅⇩m A) $$ (i, j)" by auto
qed
then show ?thesis unfolding limit_mat_def using dimA dimX by auto
qed
lemma limit_mat_add:
fixes X :: "nat ⇒ complex mat" and Y :: "nat ⇒ complex mat" and A :: "complex mat"
and m :: nat and B :: "complex mat"
assumes limX: "limit_mat X A m" and limY: "limit_mat Y B m"
shows "limit_mat (λk. X k + Y k) (A + B) m"
proof -
have dimA: "A ∈ carrier_mat m m" using limX limit_mat_def by auto
have dimB: "B ∈ carrier_mat m m" using limY limit_mat_def by auto
have dimX: "⋀n. X n ∈ carrier_mat m m" using limX unfolding limit_mat_def by auto
have dimY: "⋀n. Y n ∈ carrier_mat m m" using limY unfolding limit_mat_def by auto
then have dimXAB: "∀n. X n + Y n ∈ carrier_mat m m ∧ A + B ∈ carrier_mat m m" using dimA dimB dimX dimY
by (simp)
have "(⋀i j. i < m ⟹ j < m ⟹ (λn. (X n + Y n) $$ (i, j)) ⇢ (A + B) $$ (i, j))"
proof -
fix i j assume i: "i < m" and j: "j < m"
have "(λn. (X n) $$ (i, j)) ⇢ A$$(i, j)" using limX limit_mat_def i j by auto
moreover have "(λn. (Y n) $$ (i, j)) ⇢ B$$(i, j)" using limY limit_mat_def i j by auto
ultimately have "(λn. (X n)$$(i, j) + (Y n) $$ (i, j)) ⇢ (A$$(i, j) + B$$(i, j))"
using tendsto_add[of "λn. (X n) $$ (i, j)" "A $$ (i, j)"] by auto
moreover have "(X n + Y n) $$ (i, j) = (X n)$$(i, j) + (Y n) $$ (i, j)" for n
using i j dimX dimY index_add_mat(1)[of i "Y n" j "X n"] by fastforce
moreover have "(A + B) $$ (i, j) = A$$(i, j) + B$$(i, j)"
using i j dimA dimB by fastforce
ultimately show "(λn. (X n + Y n) $$ (i, j)) ⇢ (A + B) $$ (i, j)" by auto
qed
then show ?thesis
unfolding limit_mat_def using dimXAB by auto
qed
lemma limit_mat_minus:
fixes X :: "nat ⇒ complex mat" and Y :: "nat ⇒ complex mat" and A :: "complex mat"
and m :: nat and B :: "complex mat"
assumes limX: "limit_mat X A m" and limY: "limit_mat Y B m"
shows "limit_mat (λk. X k - Y k) (A - B) m"
proof -
have dimA: "A ∈ carrier_mat m m" using limX limit_mat_def by auto
have dimB: "B ∈ carrier_mat m m" using limY limit_mat_def by auto
have dimX: "⋀n. X n ∈ carrier_mat m m" using limX unfolding limit_mat_def by auto
have dimY: "⋀n. Y n ∈ carrier_mat m m" using limY unfolding limit_mat_def by auto
have "-1 ⋅⇩m Y n = - Y n" for n using dimY by auto
moreover have "-1 ⋅⇩m B = - B" using dimB by auto
ultimately have "limit_mat (λn. - Y n) (- B) m" using limit_mat_scale[OF limY, of "-1"] by auto
then have "limit_mat (λn. X n + (- Y n)) (A + (- B)) m" using limit_mat_add limX by auto
moreover have "X n + (- Y n) = X n - Y n" for n using dimX dimY by auto
moreover have "A + (- B) = A - B" by auto
ultimately show ?thesis by auto
qed
lemma limit_mat_mult:
fixes X :: "nat ⇒ complex mat" and Y :: "nat ⇒ complex mat" and A :: "complex mat"
and m :: nat and B :: "complex mat"
assumes limX: "limit_mat X A m" and limY: "limit_mat Y B m"
shows "limit_mat (λk. X k * Y k) (A * B) m"
proof -
have dimA: "A ∈ carrier_mat m m" using limX limit_mat_def by auto
have dimB: "B ∈ carrier_mat m m" using limY limit_mat_def by auto
have dimX: "⋀n. X n ∈ carrier_mat m m" using limX unfolding limit_mat_def by auto
have dimY: "⋀n. Y n ∈ carrier_mat m m" using limY unfolding limit_mat_def by auto
then have dimXAB: "∀n. X n * Y n ∈ carrier_mat m m ∧ A * B ∈ carrier_mat m m" using dimA dimB dimX dimY
by fastforce
have "(⋀i j. i < m ⟹ j < m ⟹ (λn. (X n * Y n) $$ (i, j)) ⇢ (A * B) $$ (i, j))"
proof -
fix i j assume i: "i < m" and j: "j < m"
have eqn: "(X n * Y n) $$ (i, j) = (∑k=0..<m. (X n)$$(i, k) * (Y n)$$(k, j))" for n
using i j dimX[of n] dimY[of n] by (auto simp add: scalar_prod_def)
have eq: "(A * B) $$ (i, j) = (∑k=0..<m. A$$(i,k) * B$$(k,j))"
using i j dimB dimA by (auto simp add: scalar_prod_def)
have "(λn. (X n) $$ (i, k)) ⇢ A$$(i, k)" if "k < m" for k using limX limit_mat_def that i by auto
moreover have "(λn. (Y n) $$ (k, j)) ⇢ B$$(k, j)" if "k < m" for k using limY limit_mat_def that j by auto
ultimately have "(λn. (X n)$$(i, k) * (Y n)$$(k,j)) ⇢ A$$(i, k) * B$$(k, j)" if "k < m" for k
using tendsto_mult[of "λn. (X n) $$ (i, k)" "A$$(i, k)" _ "λn. (Y n)$$(k, j)" "B$$(k, j)"] that by auto
then have "(λn. (∑k=0..<m. (X n)$$(i,k) * (Y n)$$(k,j))) ⇢ (∑k=0..<m. A$$(i,k) * B$$(k,j))"
using tendsto_sum[of "{0..<m}" "λk n. (X n)$$(i,k) * (Y n)$$(k,j)" "λk. A$$(i, k) * B$$(k, j)"] by auto
then show "(λn. (X n * Y n) $$ (i, j)) ⇢ (A * B) $$ (i, j)" using eqn eq by auto
qed
then show ?thesis
unfolding limit_mat_def using dimXAB by fastforce
qed
text ‹Adding matrix A to the sequence X›
definition mat_add_seq :: "complex mat ⇒ (nat ⇒ complex mat) ⇒ nat ⇒ complex mat" where
"mat_add_seq A X = (λn. A + X n)"
lemma mat_add_limit:
fixes X :: "nat ⇒ complex mat" and A :: "complex mat" and m :: nat and B :: "complex mat"
assumes dimB: "B ∈ carrier_mat m m" and limX: "limit_mat X A m"
shows "limit_mat (mat_add_seq B X) (B + A) m"
unfolding mat_add_seq_def using limit_mat_add limit_mat_const[OF dimB] limX by auto
lemma mat_minus_limit:
fixes X :: "nat ⇒ complex mat" and A :: "complex mat" and m :: nat and B :: "complex mat"
assumes dimB: "B ∈ carrier_mat m m" and limX: "limit_mat X A m"
shows "limit_mat (λn. B - X n) (B - A) m"
using limit_mat_minus limit_mat_const[OF dimB] limX by auto
text ‹Multiply matrix A by the sequence X›
definition mat_mult_seq :: "complex mat ⇒ (nat ⇒ complex mat) ⇒ nat ⇒ complex mat" where
"mat_mult_seq A X = (λn. A * X n)"
lemma mat_mult_limit:
fixes X :: "nat ⇒ complex mat" and A B :: "complex mat" and m :: nat
assumes dimB: "B ∈ carrier_mat m m" and limX: "limit_mat X A m"
shows "limit_mat (mat_mult_seq B X) (B * A) m"
unfolding mat_mult_seq_def using limit_mat_mult limit_mat_const[OF dimB] limX by auto
lemma mult_mat_limit:
fixes X :: "nat ⇒ complex mat" and A B :: "complex mat" and m :: nat
assumes dimB: "B ∈ carrier_mat m m" and limX: "limit_mat X A m"
shows "limit_mat (λk. X k * B) (A * B) m"
unfolding mat_mult_seq_def using limit_mat_mult limit_mat_const[OF dimB] limX by auto
lemma quadratic_form_mat:
fixes A :: "complex mat" and v :: "complex vec" and m :: nat
assumes dimv: "dim_vec v = m" and dimA: "A ∈ carrier_mat m m"
shows "inner_prod v (A *⇩v v) = (∑i=0..<m. (∑j=0..<m. conjugate (v$i) * A$$(i, j) * v$j))"
proof -
have "inner_prod v (A *⇩v v) = (∑i=0..<m. (∑j=0..<m.
conjugate (v$i) * A$$(i, j) * v$j))"
unfolding scalar_prod_def using dimv dimA
apply (simp add: scalar_prod_def sum_distrib_right)
apply (rule sum.cong, auto, rule sum.cong, auto)
done
then show ?thesis by auto
qed
lemma sum_subtractff:
fixes h g :: "nat ⇒ nat ⇒'a::ab_group_add"
shows "(∑x∈A. ∑y∈B. h x y - g x y) = (∑x∈A. ∑y∈B. h x y) - (∑x∈A. ∑y∈B. g x y)"
proof -
have "∀ x ∈ A. (∑y∈B. h x y - g x y) = (∑y∈B. h x y) - (∑y∈B. g x y)"
proof -
{
fix x assume x: "x ∈ A"
have "(∑y∈B. h x y - g x y) = (∑y∈B. h x y) - (∑y∈B. g x y)"
using sum_subtractf by auto
}
then show ?thesis using sum_subtractf by blast
qed
then have "(∑x∈A.∑y∈B. h x y - g x y) = (∑x∈A. ((∑y∈B. h x y) - (∑y∈B. g x y)))" by auto
also have "… = (∑x∈A. ∑y∈B. h x y) - (∑x∈A. ∑y∈B. g x y)"
by (simp add: sum_subtractf)
finally have " (∑x∈A. ∑y∈B. h x y - g x y) = (∑x∈A. sum (h x) B) - (∑x∈A. sum (g x) B)" by auto
then show ?thesis by auto
qed
lemma sum_abs_complex:
fixes h :: "nat ⇒ nat ⇒ complex"
shows "cmod (∑x∈A.∑y∈B. h x y) ≤ (∑x∈A. ∑y∈B. cmod(h x y))"
proof -
have B: "∀ x ∈ A. cmod( ∑y∈B .h x y) ≤ (∑y∈B. cmod(h x y))" using sum_abs norm_sum by blast
have "cmod (∑x∈A.∑y∈B. h x y) ≤ (∑x∈A. cmod( ∑y∈B .h x y))" using sum_abs norm_sum by blast
also have "… ≤ (∑x∈A. ∑y∈B. cmod(h x y))" using sum_abs norm_sum B
by (simp add: sum_mono)
finally have "cmod (∑x∈A. ∑y∈B. h x y) ≤ (∑x∈A. ∑y∈B. cmod (h x y))" by auto
then show ?thesis by auto
qed
lemma hermitian_mat_lim_is_hermitian:
fixes X :: "nat ⇒ complex mat" and A :: "complex mat" and m :: nat
assumes limX: "limit_mat X A m" and herX: "∀ n. hermitian (X n)"
shows "hermitian A"
proof -
have dimX: "∀n. X n ∈ carrier_mat m m" using limX unfolding limit_mat_def by auto
have dimA : "A ∈ carrier_mat m m" using limX unfolding limit_mat_def by auto
from herX have herXn: "∀ n. adjoint (X n) = (X n)" unfolding hermitian_def by auto
from limX have limXn: "∀i<m. ∀j<m. (λn. X n $$ (i, j)) ⇢ A $$ (i, j)" unfolding limit_mat_def by auto
have "∀i<m. ∀j<m.(adjoint A)$$ (i, j) = A$$ (i, j)"
proof -
{
fix i j assume i: "i < m" and j: "j < m"
have aij: "(adjoint A)$$ (i, j) = conjugate (A $$ (j,i))" using adjoint_eval i j dimA by blast
have ij: "(λn. X n $$ (i, j)) ⇢ A $$ (i, j)" using limXn i j by auto
have ji: "(λn. X n $$ (j, i)) ⇢ A $$ (j, i)" using limXn i j by auto
then have "∀r>0. ∃no. ∀n≥no. dist (conjugate (X n $$ (j, i))) (conjugate (A $$ (j, i))) < r"
proof -
{
fix r :: real assume r : "r > 0"
have "∃no. ∀n≥no. cmod (X n $$ (j, i) - A $$ (j, i)) < r" using ji r unfolding LIMSEQ_def dist_norm by auto
then obtain no where Xji: "∀n≥no. cmod (X n $$ (j, i) - A $$ (j, i)) < r" by auto
then have "∀n≥no. cmod (conjugate (X n $$ (j, i) - A $$ (j, i))) < r"
using complex_mod_cnj conjugate_complex_def by presburger
then have "∀n≥no. dist (conjugate (X n $$ (j, i))) (conjugate (A $$ (j, i))) < r" unfolding dist_norm by auto
then have "∃no. ∀n≥no. dist (conjugate (X n $$ (j, i))) (conjugate (A $$ (j, i))) < r" by auto
}
then show ?thesis by auto
qed
then have conjX: "(λn. conjugate (X n $$ (j, i))) ⇢ conjugate (A $$ (j, i))" unfolding LIMSEQ_def by auto
from herXn have "∀ n. conjugate (X n $$ (j,i)) = X n$$ (i, j)" using adjoint_eval i j dimX
by (metis adjoint_dim_col carrier_matD(1))
then have "(λn. X n $$ (i, j)) ⇢ conjugate (A $$ (j, i))" using conjX by auto
then have "conjugate (A $$ (j,i)) = A$$ (i, j)" using ij by (simp add: LIMSEQ_unique)
then have "(adjoint A)$$ (i, j) = A$$ (i, j)" using adjoint_eval i j by (simp add:aij)
}
then show ?thesis by auto
qed
then have "hermitian A" using hermitian_def dimA
by (metis adjoint_dim carrier_matD(1) carrier_matD(2) eq_matI)
then show ?thesis by auto
qed
lemma quantifier_change_order_once:
fixes P :: "nat ⇒ nat ⇒ bool" and m :: nat
shows "∀j<m. ∃no. ∀n≥no. P n j ⟹ ∃no. ∀j<m. ∀n≥no. P n j"
proof (induct m)
case 0
then show ?case by auto
next
case (Suc m)
then show ?case
proof -
have mm: "∃no. ∀j<m. ∀n≥no. P n j" using Suc by auto
then obtain M where MM: "∀j<m. ∀n≥M. P n j" by auto
have sucm: "∃no. ∀n≥no. P n m" using Suc(2) by auto
then obtain N where NN: "∀n≥N. P n m" by auto
let ?N = "max M N"
from MM NN have "∀j<Suc m. ∀n≥?N. P n j"
by (metis less_antisym max.boundedE)
then have "∃no. ∀j<Suc m. ∀n≥no. P n j" by blast
then show ?thesis by auto
qed
qed
lemma quantifier_change_order_twice:
fixes P :: "nat ⇒ nat ⇒ nat ⇒ bool" and m n :: nat
shows "∀i<m. ∀j<n. ∃ no. ∀n≥no. P n i j ⟹ ∃no. ∀i<m. ∀j<n. ∀n≥no. P n i j"
proof -
assume fact: "∀i<m. ∀j<n. ∃ no. ∀n≥no. P n i j"
have one: "∀i<m. ∃no.∀j<n. ∀n≥no. P n i j"
using fact quantifier_change_order_once by auto
have two: "∀i<m. ∃no.∀j<n. ∀n≥no. P n i j ⟹ ∃no. ∀i<m. ∀j<n. ∀n≥no. P n i j"
proof (induct m)
case 0
then show ?case by auto
next
case (Suc m)
then show ?case
proof -
obtain M where MM: "∀i<m. ∀j<n. ∀n≥M. P n i j" using Suc by auto
obtain N where NN: "∀j<n. ∀n≥N. P n m j" using Suc(2) by blast
let ?N = "max M N"
from MM NN have "∀i<Suc m. ∀j<n. ∀n≥?N. P n i j"
by (metis less_antisym max.boundedE)
then have "∃no. ∀i<Suc m. ∀j<n. ∀n≥no. P n i j" by blast
then show ?thesis by auto
qed
qed
with fact show ?thesis using one by auto
qed
lemma pos_mat_lim_is_pos:
fixes X :: "nat ⇒ complex mat" and A :: "complex mat" and m :: nat
assumes limX: "limit_mat X A m" and posX: "∀n. positive (X n)"
shows "positive A"
proof (rule ccontr)
have dimX : "∀n. X n ∈ carrier_mat m m" using limX unfolding limit_mat_def by auto
have dimA : "A ∈ carrier_mat m m" using limX unfolding limit_mat_def by auto
have herX : "∀ n. hermitian (X n)" using posX positive_is_hermitian by auto
then have herA : "hermitian A" using hermitian_mat_lim_is_hermitian limX by auto
then have herprod: "∀ v. dim_vec v = dim_col A ⟶ inner_prod v (A *⇩v v) ∈ Reals"
using hermitian_inner_prod_real dimA by auto
assume npA: " ¬ positive A"
from npA have "¬ (A ∈ carrier_mat (dim_col A) (dim_col A)) ∨ ¬ (∀v. dim_vec v = dim_col A ⟶ 0 ≤ inner_prod v (A *⇩v v))"
unfolding positive_def by blast
then have evA: "∃ v. dim_vec v = dim_col A ∧ ¬ inner_prod v (A *⇩v v) ≥ 0" using dimA by blast
then have "∃ v. dim_vec v = dim_col A ∧ inner_prod v (A *⇩v v) < 0"
proof -
obtain v where vA: "dim_vec v = dim_col A ∧ ¬ inner_prod v (A *⇩v v) ≥ 0" using evA by auto
from vA herprod have "¬ 0 ≤ inner_prod v (A *⇩v v) ∧ inner_prod v (A *⇩v v) ∈ Reals" by auto
then have "inner_prod v (A *⇩v v) < 0"
using complex_is_Real_iff by (auto simp: less_complex_def less_eq_complex_def)
then have "∃ v. dim_vec v = dim_col A ∧ inner_prod v (A *⇩v v) < 0" using vA by auto
then show ?thesis by auto
qed
then obtain v where neg: "dim_vec v = dim_col A ∧ inner_prod v (A *⇩v v) < 0" by auto
have nzero: "v ≠ 0⇩v m"
proof (rule ccontr)
assume nega: " ¬ v ≠ 0⇩v m"
have zero: "v = 0⇩v m" using nega by auto
have "(A *⇩v v) = 0⇩v m" unfolding mult_mat_vec_def using zero
using dimA by auto
then have zerov: "inner_prod v (A *⇩v v) = 0" by (simp add: zero)
from neg zerov have "¬ v ≠ 0⇩v m ⟹ False" using dimA by auto
with nega show False by auto
qed
have invgeq: "inner_prod v v > 0"
proof -
have "inner_prod v v = vec_norm v * vec_norm v" unfolding vec_norm_def
by (metis carrier_matD(2) carrier_vec_dim_vec dimA mult_cancel_left1 neg normalized_cscalar_prod normalized_vec_norm nzero vec_norm_def)
moreover have "vec_norm v > 0" using nzero vec_norm_ge_0 neg dimA
by (metis carrier_matD(2) carrier_vec_dim_vec)
ultimately have "inner_prod v v > 0" by (auto simp: less_eq_complex_def less_complex_def)
then show ?thesis by auto
qed
have invv: "inner_prod v v = (∑i = 0..<m. cmod (conjugate (v $ i) * (v $ i)))"
proof -
{
have "∀ i < m. conjugate (v $ i) * (v $ i) ≥ 0" using conjugate_square_smaller_0
by (simp add: less_eq_complex_def)
then have vi: "∀ i < m. conjugate (v $ i) * (v $ i) = cmod (conjugate (v $ i) * (v $ i))" using cmod_eq_Re
by (simp add: complex.expand)
have "inner_prod v v= (∑i = 0..<m. ((v $ i) * conjugate (v $ i)))"
unfolding scalar_prod_def conjugate_vec_def using neg dimA by auto
also have "… = (∑i = 0..<m. (conjugate (v $ i) * (v $ i)))"
by (meson mult.commute)
also have "… = (∑i = 0..<m. cmod (conjugate (v $ i) * (v $ i)))" using vi by auto
finally have "inner_prod v v = (∑i = 0..<m. cmod (conjugate (v $ i) * (v $ i)))" by auto
}
then show ?thesis by auto
qed
let ?r = "inner_prod v (A *⇩v v)" have rl: "?r < 0" using neg by auto
have vAv: "inner_prod v (A *⇩v v) = (∑i=0..<m. (∑j=0..<m.
conjugate (v$i) * A$$(i, j) * v$j))" using quadratic_form_mat dimA neg by auto
from limX have limij: "∀i<m. ∀j<m. (λn. X n $$ (i, j)) ⇢ A $$ (i, j)" unfolding limit_mat_def by auto
then have limXv: "(λ n. inner_prod v ((X n) *⇩v v)) ⇢ inner_prod v (A *⇩v v)"
proof -
have XAless: "cmod (inner_prod v (X n *⇩v v) - inner_prod v (A *⇩v v)) ≤
(∑i = 0..<m. ∑j = 0..<m. cmod (conjugate (v $ i)) * cmod (X n $$ (i, j) - A $$ (i, j)) * cmod (v $ j))" for n
proof -
have "∀ i < m. ∀ j < m. conjugate (v$i) * X n $$(i, j) * v$j - conjugate (v$i) * A$$(i, j) * v$j =
conjugate (v$i) * (X n $$(i, j)-A$$(i, j)) * v$j"
by (simp add: mult.commute right_diff_distrib)
then have ele: "∀ i < m.(∑j=0..<m.(conjugate (v$i) * X n $$(i, j) * v$j - conjugate (v$i) * A$$(i, j) * v$j)) = (∑j=0..<m.(
conjugate (v$i) * (X n $$(i, j)-A$$(i, j)) * v$j))" by auto
have "∀ i < m. ∀ j < m. cmod(conjugate (v $ i) * (X n $$ (i, j) - A $$ (i, j)) * v $ j) =
cmod(conjugate (v $ i)) * cmod (X n $$ (i, j) - A $$ (i, j)) * cmod(v $ j)"
by (simp add: norm_mult)
then have less: "∀ i < m.(∑j = 0..<m. cmod(conjugate (v $ i) * (X n $$ (i, j) - A $$ (i, j)) * v $ j)) =
(∑j = 0..<m. cmod(conjugate (v $ i)) * cmod (X n $$ (i, j) - A $$ (i, j)) * cmod(v $ j))" by auto
have "inner_prod v (X n *⇩v v) - inner_prod v (A *⇩v v) = (∑i=0..<m. (∑j=0..<m.
conjugate (v$i) * X n $$(i, j) * v$j)) - (∑i=0..<m. (∑j=0..<m.
conjugate (v$i) * A$$(i, j) * v$j))" using quadratic_form_mat neg dimA dimX by auto
also have "… = (∑i=0..<m. (∑j=0..<m.(
conjugate (v$i) * X n $$(i, j) * v$j - conjugate (v$i) * A$$(i, j) * v$j)))"
using sum_subtractff[of "λ i j. conjugate (v $ i) * X n $$ (i, j) * v $ j" "λ i j. conjugate (v $ i) * A $$ (i, j) * v $ j" "{0..<m}"] by auto
also have "… = (∑i=0..<m. (∑j=0..<m.(
conjugate (v$i) * (X n $$(i, j)-A$$(i, j)) * v$j)))" using ele by auto
finally have minusXA: "inner_prod v (X n *⇩v v) - inner_prod v (A *⇩v v) = (∑i = 0..<m. ∑j = 0..<m. conjugate (v $ i) * (X n $$ (i, j) - A $$ (i, j)) * v $ j)" by auto
from minusXA have "cmod (inner_prod v (X n *⇩v v) - inner_prod v (A *⇩v v)) =
cmod (∑i = 0..<m. ∑j = 0..<m. conjugate (v $ i) * (X n $$ (i, j) - A $$ (i, j)) * v $ j)" by auto
also have "… ≤ (∑i = 0..<m. ∑j = 0..<m. cmod(conjugate (v $ i) * (X n $$ (i, j) - A $$ (i, j)) * v $ j))"
using sum_abs_complex by simp
also have "… = (∑i = 0..<m. ∑j = 0..<m. cmod(conjugate (v $ i)) * cmod (X n $$ (i, j) - A $$ (i, j)) * cmod(v $ j))"
using less by auto
finally show ?thesis by auto
qed
from limij have limijm: " ∀i<m. ∀j<m. ∀r>0. ∃no. ∀n≥no. cmod (X n $$ (i, j) - A $$ (i, j)) < r"
unfolding LIMSEQ_def dist_norm by auto
from limX have mg: "m > 0" using limit_mat_def
by (metis carrier_matD(1) carrier_matD(2) mat_eq_iff neq0_conv not_less0 npA posX)
have cmoda: "∃no. ∀n≥no. (∑i = 0..<m. ∑j = 0..<m. cmod (conjugate (v $ i)) * cmod (X n $$ (i, j) - A $$ (i, j)) * cmod (v $ j)) < r"
if r: "r > 0" for r
proof -
let ?u = "(∑i = 0..<m. ∑j = 0..<m.((cmod (conjugate (v $ i)) * cmod (v $ j))))"
have ug: "?u > 0"
proof -
have ur: "?u = (∑i = 0..<m. (cmod (conjugate (v $ i)) * (∑j = 0..<m.( cmod (v $ j)))))" by (simp add: sum_distrib_left)
have "(∑j = 0..<m.( cmod (v $ j))) ≥ cmod (v $ i)" if i: "i < m" for i
using member_le_sum[of i "{0..<m}" "λ j. cmod (v$j)"] cmod_def i by simp
then have "∀ i < m. (cmod (conjugate (v $ i)) * (∑j = 0..<m.( cmod (v $ j)))) ≥ (cmod (conjugate (v $ i)) * cmod (v $ i))"
by (simp add: mult_left_mono)
then have "?u ≥ (∑i = 0..<m. (cmod (conjugate (v $ i)) *cmod (v $ i)))"
using ur sum_mono[of "{0..<m}" "λ i. cmod (conjugate (v $ i)) * cmod (v $ i)" "λ i. cmod (conjugate (v $ i)) * (∑j = 0..<m. cmod (v $ j))"]
by auto
moreover have "(∑i = 0..<m. cmod (conjugate (v $ i) *cmod (v $ i))) = (∑i = 0..<m. cmod (conjugate (v $ i) * (v $ i)))"
using norm_ge_zero norm_mult norm_of_real by (metis (no_types, opaque_lifting) abs_of_nonneg)
moreover have "(∑i = 0..<m. cmod (conjugate (v $ i) * (v $ i))) = inner_prod v v" using invv by auto
ultimately have "?u ≥ inner_prod v v"
by (metis (no_types, lifting) Im_complex_of_real Re_complex_of_real invv less_eq_complex_def norm_mult sum.cong)
then have "?u > 0" using invgeq by (auto simp: less_eq_complex_def less_complex_def)
then show ?thesis by auto
qed
let ?s = "r / (2 * ?u)"
have sgz: "?s > 0" using ug rl
by (smt divide_pos_pos dual_order.strict_iff_order linordered_semiring_strict_class.mult_pos_pos zero_less_norm_iff r)
from limijm have sij: "∃no. ∀n≥no. cmod (X n $$ (i, j) - A $$ (i, j)) < ?s" if i: "i < m" and j: "j < m" for i j
proof -
obtain N where Ns: "∀n≥N. cmod (X n $$ (i, j) - A $$ (i, j)) < ?s" using sgz limijm i j by blast
then show ?thesis by auto
qed
then have "∃no. ∀i<m. ∀j<m. ∀n≥no. cmod (X n $$ (i, j) - A $$ (i, j)) < ?s"
using quantifier_change_order_twice[of m m "λ n i j. (cmod (X n $$ (i, j) - A $$ (i, j))<?s)"] by auto
then obtain N where Nno: "∀i<m. ∀j<m. ∀n≥N. cmod (X n $$ (i, j) - A $$ (i, j)) < ?s" by auto
then have mmN: "cmod (conjugate (v $ i)) * cmod (X n $$ (i, j) - A $$ (i, j)) * cmod (v $ j)
≤ ?s * (cmod (conjugate (v $ i)) * cmod (v $ j))"
if i: "i < m" and j: "j < m" and n: "n ≥ N" for i j n
proof -
have geq: "cmod (conjugate (v $ i)) ≥ 0 ∧ cmod (v $ j)≥0" by simp
then have "cmod (conjugate (v $ i)) * cmod (X n $$ (i, j) - A $$ (i, j)) ≤cmod (conjugate (v $ i)) * ?s" using Nno i j n
by (smt mult_left_mono)
then have "cmod (conjugate (v $ i)) * cmod (X n $$ (i, j) - A $$ (i, j)) * cmod (v $ j)
≤ cmod (conjugate (v $ i)) *?s * cmod (v $ j)" using geq mult_right_mono by blast
also have "… = ?s * (cmod (conjugate (v $ i)) * cmod (v $ j))" by simp
finally show ?thesis by auto
qed
then have "(∑i = 0..<m. ∑j = 0..<m. cmod (conjugate (v $ i)) * cmod (X n $$ (i, j) - A $$ (i, j)) * cmod (v $ j)) < r"
if n: "n ≥ N" for n
proof -
have mmX: "∀i<m. ∀j<m. cmod (conjugate (v $ i)) * cmod (X n $$ (i, j) - A $$ (i, j)) * cmod (v $ j)
≤ ?s * (cmod (conjugate (v $ i)) * cmod (v $ j))" using n mmN by blast
have "(∑j = 0..<m. cmod (conjugate (v $ i)) * cmod (X n $$ (i, j) - A $$ (i, j)) * cmod (v $ j))
≤ (∑j = 0..<m.(?s * (cmod (conjugate (v $ i)) * cmod (v $ j))))" if i: "i < m" for i
proof -
have "∀j<m. cmod (conjugate (v $ i)) * cmod (X n $$ (i, j) - A $$ (i, j)) * cmod (v $ j)
≤ ?s * (cmod (conjugate (v $ i)) * cmod (v $ j))" using mmX i by auto
then show ?thesis
using sum_mono[of "{0..<m}" "λ j. cmod (conjugate (v $ i)) * cmod (X n $$ (i, j) - A $$ (i, j)) * cmod (v $ j)" "λ j. (?s * (cmod (conjugate (v $ i)) * cmod (v $ j)))"]
atLeastLessThan_iff by blast
qed
then have "(∑i = 0..<m. ∑j = 0..<m. cmod (conjugate (v $ i)) * cmod (X n $$ (i, j) - A $$ (i, j)) * cmod (v $ j))
≤ (∑i = 0..<m. ∑j = 0..<m.(?s * (cmod (conjugate (v $ i)) * cmod (v $ j))))" using sum_mono atLeastLessThan_iff
by (metis (no_types, lifting))
also have "… = ?s * (∑i = 0..<m. ∑j = 0..<m.((cmod (conjugate (v $ i)) * cmod (v $ j))))" by (simp add: sum_distrib_left)
also have "… = r / 2" using nonzero_mult_divide_mult_cancel_right sgz by fastforce
finally show ?thesis using r by auto
qed
then show ?thesis by auto
qed
then have XnAv:"∃no. ∀n≥no. cmod (inner_prod v (X n *⇩v v) - inner_prod v (A *⇩v v)) < r" if r: "r > 0" for r
proof -
obtain no where nno: "∀n≥no. (∑i = 0..<m. ∑j = 0..<m. cmod (conjugate (v $ i)) * cmod (X n $$ (i, j) - A $$ (i, j)) * cmod (v $ j)) < r"
using r cmoda neg by auto
then have "∀n≥no. cmod (inner_prod v (X n *⇩v v) - inner_prod v (A *⇩v v)) < r" using XAless neg by smt
then show ?thesis by auto
qed
then have "(λn. inner_prod v (X n *⇩v v)) ⇢ inner_prod v (A *⇩v v)" unfolding LIMSEQ_def dist_norm by auto
then show ?thesis by auto
qed
from limXv have "∀r>0. ∃no. ∀n≥no. cmod (inner_prod v (X n *⇩v v) - inner_prod v (A *⇩v v)) < r" unfolding LIMSEQ_def dist_norm by auto
then have "∃no. ∀n≥no. cmod (inner_prod v (X n *⇩v v) - inner_prod v (A *⇩v v)) < -?r" using rl
by (auto simp: less_eq_complex_def less_complex_def)
then obtain N where Ng: "∀n≥N. cmod (inner_prod v (X n *⇩v v) - inner_prod v (A *⇩v v)) < -?r" by auto
then have XN: "cmod (inner_prod v (X N *⇩v v) - inner_prod v (A *⇩v v)) < -?r" by auto
from posX have "positive (X N)" by auto
then have XNv:"inner_prod v (X N *⇩v v) ≥ 0"
by (metis Complex_Matrix.positive_def carrier_matD(2) dimA dimX neg)
from rl XNv have XX: "cmod (inner_prod v (X N *⇩v v) - inner_prod v (A *⇩v v)) = cmod(inner_prod v (X N *⇩v v)) - cmod(inner_prod v (A *⇩v v))"
using XN cmod_eq_Re by (auto simp: less_eq_complex_def less_complex_def)
then have YY: "cmod(inner_prod v (X N *⇩v v)) - cmod(inner_prod v (A *⇩v v)) < -?r" using XN by auto
then have "cmod(inner_prod v (X N *⇩v v)) - cmod(inner_prod v (A *⇩v v)) < cmod(inner_prod v (A *⇩v v))"
using rl cmod_eq_Re by (auto simp: less_eq_complex_def less_complex_def)
then have "cmod(inner_prod v (X N *⇩v v)) < 0" using XNv XX YY cmod_eq_Re
by (auto simp: less_eq_complex_def less_complex_def)
then have "False" using XNv by simp
with npA show False by auto
qed
lemma limit_mat_ignore_initial_segment:
"limit_mat g A d ⟹ limit_mat (λn. g (n + k)) A d"
proof -
assume asm: "limit_mat g A d"
then have lim: "∀ i < d. ∀ j < d. (λ n. (g n) $$ (i, j)) ⇢ (A $$ (i, j))" using limit_mat_def by auto
then have limk: "∀ i < d. ∀ j < d. (λ n. (g (n + k)) $$ (i, j)) ⇢ (A $$ (i, j))"
proof -
{
fix i j assume dims: "i < d" "j < d"
then have "(λ n. (g n) $$ (i, j)) ⇢ (A $$ (i, j))" using lim by auto
then have "(λ n. (g (n + k)) $$ (i, j)) ⇢ (A $$ (i, j))" using LIMSEQ_ignore_initial_segment by auto
}
then show "∀ i < d. ∀ j < d. (λ n. (g (n + k)) $$ (i, j)) ⇢ (A $$ (i, j))" by auto
qed
have "∀ n. g n ∈ carrier_mat d d" using asm unfolding limit_mat_def by auto
then have "∀ n. g (n + k) ∈ carrier_mat d d" by auto
moreover have "A ∈ carrier_mat d d" using asm limit_mat_def by auto
ultimately show "limit_mat (λn. g (n + k)) A d" using limit_mat_def limk by auto
qed
lemma mat_trace_limit:
"limit_mat g A d ⟹ (λn. trace (g n)) ⇢ trace A"
proof -
assume lim: "limit_mat g A d"
then have dgn: "g n ∈ carrier_mat d d" for n using limit_mat_def by auto
from lim have dA: "A ∈ carrier_mat d d" using limit_mat_def by auto
have trg: "trace (g n) = (∑k=0..<d. (g n)$$(k, k))" for n unfolding trace_def using carrier_matD[OF dgn] by auto
have "∀k < d. (λn. (g n)$$(k, k)) ⇢ A$$(k, k)" using limit_mat_def lim by auto
then have "(λn. (∑k=0..<d. (g n)$$(k, k))) ⇢ (∑k=0..<d. A$$(k, k))"
using tendsto_sum[where ?I = "{0..<d}" and ?f = "(λk n. (g n)$$(k, k))"] by auto
then show "(λn. trace (g n)) ⇢ trace A" unfolding trace_def
using trg carrier_matD[OF dgn] carrier_matD[OF dA] by auto
qed
subsection ‹Existence of least upper bound for the L\"{o}wner order›
definition lowner_is_lub :: "(nat ⇒ complex mat) ⇒ complex mat ⇒ bool" where
"lowner_is_lub f M ⟷ (∀n. f n ≤⇩L M) ∧ (∀M'. (∀n. f n ≤⇩L M') ⟶ M ≤⇩L M')"
locale matrix_seq =
fixes dim :: nat
and f :: "nat ⇒ complex mat"
assumes
dim: "⋀n. f n ∈ carrier_mat dim dim" and
pdo: "⋀n. partial_density_operator (f n)" and
inc: "⋀n. lowner_le (f n) (f (Suc n))"
begin
definition lowner_is_lub :: "complex mat ⇒ bool" where
"lowner_is_lub M ⟷ (∀n. f n ≤⇩L M) ∧ (∀M'. (∀n. f n ≤⇩L M') ⟶ M ≤⇩L M')"
lemma lowner_is_lub_dim:
assumes "lowner_is_lub M"
shows "M ∈ carrier_mat dim dim"
proof -
have "f 0 ≤⇩L M" using assms lowner_is_lub_def by auto
then have 1: "dim_row (f 0) = dim_row M ∧ dim_col (f 0) = dim_col M"
using lowner_le_def by auto
moreover have 2: "f 0 ∈ carrier_mat dim dim"
using dim by auto
ultimately show ?thesis by auto
qed
lemma trace_adjoint_eq_u:
fixes A :: "complex mat"
shows "trace (A * adjoint A) = (∑ i ∈ {0 ..< dim_row A}. ∑ j ∈ {0 ..< dim_col A}. (norm(A $$ (i,j)))⇧2)"
proof -
have "trace (A * adjoint A) = (∑ i ∈ {0 ..< dim_row A}. row A i ∙ conjugate (row A i))"
by (simp add: trace_def cmod_def adjoint_def scalar_prod_def)
also have "… = (∑ i ∈ {0 ..< dim_row A}. ∑ j ∈ {0 ..< dim_col A}. (norm(A $$ (i,j)))⇧2)"
proof (simp add: scalar_prod_def cmod_def)
have cnjmul: "∀ i ia. A $$ (i, ia) * cnj (A $$ (i, ia)) =
((complex_of_real (Re (A $$ (i, ia))))⇧2 + (complex_of_real (Im (A $$ (i, ia))))⇧2)"
by (simp add: complex_mult_cnj)
then have "∀ i. (∑ia = 0..<dim_col A. A $$ (i, ia) * cnj (A $$ (i, ia))) =
(∑ia = 0..<dim_col A. ((complex_of_real (Re (A $$ (i, ia))))⇧2 + (complex_of_real (Im (A $$ (i, ia))))⇧2))"
by auto
then show"(∑i = 0..<dim_row A. ∑ia = 0..<dim_col A. A $$ (i, ia) * cnj (A $$ (i, ia))) =
(∑x = 0..<dim_row A. ∑xa = 0..<dim_col A. (complex_of_real (Re (A $$ (x, xa))))⇧2) +
(∑x = 0..<dim_row A. ∑xa = 0..<dim_col A. (complex_of_real (Im (A $$ (x, xa))))⇧2)"
by auto
qed
finally show ?thesis .
qed
lemma trace_adjoint_element_ineq:
fixes A :: "complex mat"
assumes rindex: "i ∈ {0 ..< dim_row A}"
and cindex: "j ∈ {0 ..< dim_col A}"
shows "(norm(A $$ (i,j)))⇧2 ≤ trace (A * adjoint A)"
proof (simp add: trace_adjoint_eq_u less_eq_complex_def)
have ineqi: "(cmod (A $$ (i, j)))⇧2 ≤ (∑xa = 0..<dim_col A. (cmod (A $$ (i, xa)))⇧2)"
using cindex member_le_sum[of j " {0 ..< dim_col A}" "λ x. (cmod (A $$ (i, x)))⇧2"] by auto
also have ineqj: "… ≤ (∑x = 0..<dim_row A. ∑xa = 0..<dim_col A. (cmod (A $$ (x, xa)))⇧2)"
using rindex member_le_sum[of i " {0 ..< dim_row A}" "λ x. ∑xa = 0..<dim_col A. (cmod (A $$ (x, xa)))⇧2"]
by (simp add: sum_nonneg)
then show "(cmod (A $$ (i, j)))⇧2 ≤ (∑x = 0..<dim_row A. ∑xa = 0..<dim_col A. (cmod (A $$ (x, xa)))⇧2)"
using ineqi by linarith
qed
lemma positive_is_normal:
fixes A :: "complex mat"
assumes pos: "positive A"
shows "A * adjoint A = adjoint A * A"
proof -
have hA: "hermitian A" using positive_is_hermitian pos by auto
then show ?thesis by (simp add: hA hermitian_is_normal)
qed
lemma diag_mat_mul_diag_diag:
fixes A B :: "complex mat"
assumes dimA: "A ∈ carrier_mat n n" and dimB: "B ∈ carrier_mat n n"
and dA: "diagonal_mat A" and dB: "diagonal_mat B"
shows "diagonal_mat (A * B)"
proof -
have AB: "A * B = mat n n (λ(i,j). (if (i = j) then (A$$(i, i)) * (B$$(i, i)) else 0))"
using diag_mat_mult_diag_mat[of A n B] dimA dimB dA dB by auto
then have dAB: "∀i<n. ∀j<n. i ≠ j ⟶ (A*B) $$ (i,j) = 0"
proof -
{
fix i j assume i: "i < n" and j: "j < n" and ij: "i ≠ j"
have "(A*B) $$ (i,j) = 0" using AB i j ij by auto
}
then show ?thesis by auto
qed
then show ?thesis using diagonal_mat_def dAB dimA dimB
by (metis carrier_matD(1) carrier_matD(2) index_mult_mat(2) index_mult_mat(3))
qed
lemma diag_mat_mul_diag_ele:
fixes A B :: "complex mat"
assumes dimA: "A ∈ carrier_mat n n" and dimB: "B ∈ carrier_mat n n"
and dA: "diagonal_mat A" and dB: "diagonal_mat B"
shows "∀i<n. (A*B) $$ (i,i) = A$$(i, i) * B$$(i, i)"
proof -
have AB: "A * B = mat n n (λ(i,j). if i = j then (A$$(i, i)) * (B$$(i, i)) else 0)"
using diag_mat_mult_diag_mat[of A n B] dimA dimB dA dB by auto
then show ?thesis
using AB by auto
qed
lemma trace_square_less_square_trace:
fixes B :: "complex mat"
assumes dimB: "B ∈ carrier_mat n n"
and dB: "diagonal_mat B" and pB: "⋀i. i < n ⟹ B$$(i, i) ≥ 0"
shows "trace (B*B) ≤ (trace B)⇧2"
proof -
have tB: "trace B = (∑ i ∈ {0 ..<n}. B $$ (i,i))" using assms trace_def[of B] carrier_mat_def by auto
then have tBtB: "(trace B)⇧2 = (∑ i ∈ {0 ..<n}.∑ j ∈ {0 ..<n}. B $$ (i,i)*B $$ (j,j))"
proof -
show ?thesis
by (metis (no_types) semiring_normalization_rules(29) sum_product tB)
qed
have BB: "⋀i. i < n ⟹ (B*B) $$ (i,i) = (B$$(i, i))⇧2" using diag_mat_mul_diag_ele[of B n B] dimB dB
by (metis numeral_1_eq_Suc_0 power_Suc0_right power_add_numeral semiring_norm(2))
have tBB: "trace (B*B) = (∑ i ∈ {0 ..<n}. (B*B) $$ (i,i))" using assms trace_def[of "B*B"] carrier_mat_def by auto
also have "… = (∑ i ∈ {0 ..<n}. (B$$(i, i))⇧2)" using BB by auto
finally have BBt: " trace (B * B) = (∑i = 0..<n. (B $$ (i, i))⇧2)" by auto
have lesseq: "∀i ∈ {0 ..<n}. (B $$ (i, i))⇧2 ≤ (∑ j ∈ {0 ..<n}. B $$ (i,i)*B $$ (j,j))"
proof -
{
fix i assume i: "i < n"
have "(∑j = 0..<n. B $$ (i, i) * B $$ (j, j)) = (B $$ (i, i))⇧2 + sum (λ j. (B $$ (i, i) * B $$ (j, j))) ({0 ..<n} - {i})"
by (metis (no_types, lifting) BB atLeastLessThan_iff dB diag_mat_mul_diag_ele dimB finite_atLeastLessThan i not_le not_less_zero sum.remove)
moreover have "(sum (λ j. (B $$ (i, i) * B $$ (j, j))) ({0 ..<n} - {i})) ≥ 0"
proof (cases "{0..<n} - {i} ≠ {}")
case True
then show ?thesis using pB i sum_nonneg[of "{0..<n} - {i}" "λ j. (B $$ (i, i) * B $$ (j, j))"] by auto
next
case False
have "(∑j∈{0..<n} - {i}. B $$ (i, i) * B $$ (j, j)) = 0" using False by fastforce
then show ?thesis by auto
qed
ultimately have "(∑j = 0..<n. B $$ (i, i) * B $$ (j, j)) ≥ (B $$ (i, i))⇧2" by auto
}
then show ?thesis by auto
qed
from tBtB BBt lesseq have "trace (B*B) ≤ (trace B)⇧2"
using sum_mono[of "{0..<n}" "λ i. (B $$ (i, i))⇧2" "λ i. (∑j = 0..<n. B $$ (i, i) * B $$ (j, j))"]
by (metis (no_types, lifting))
then show ?thesis by auto
qed
lemma trace_positive_eq:
fixes A :: "complex mat"
assumes pos: "positive A"
shows "trace (A * adjoint A) ≤ (trace A)⇧2"
proof -
from assms have normal: "A * adjoint A = adjoint A * A" by (rule positive_is_normal)
moreover
from assms positive_dim_eq obtain n where cA: "A ∈ carrier_mat n n" by auto
moreover
from assms complex_mat_char_poly_factorizable cA obtain es where charpo: " char_poly A = (∏ a ← es. [:- a, 1:]) ∧ length es = n" by auto
moreover
obtain B P Q where B: "unitary_schur_decomposition A es = (B,P,Q)" by (cases "unitary_schur_decomposition A es", auto)
ultimately have
smw: "similar_mat_wit A B P (adjoint P)"
and ut: "diagonal_mat B"
and uP: "unitary P"
and dB: "diag_mat B = es"
and QaP: "Q = adjoint P"
using normal_complex_mat_has_spectral_decomposition[of A n es B P Q] unitary_schur_decomposition by auto
from smw cA QaP uP have cB: "B ∈ carrier_mat n n" and cP: "P ∈ carrier_mat n n" and cQ: "Q ∈ carrier_mat n n"
unfolding similar_mat_wit_def Let_def unitary_def by auto
then have caP: "adjoint P ∈ carrier_mat n n" using adjoint_dim[of P n] by auto
from smw QaP cA have A: "A = P * B * adjoint P" and traceA: "trace A = trace (P * B * Q)" and PB: "P * Q = 1⇩m n ∧ Q * P = 1⇩m n"
unfolding similar_mat_wit_def by auto
have traceAB: "trace (P * B * Q) = trace ((Q*P)*B)"
using cQ cP cB by (mat_assoc n)
also have traceelim: "… = trace B" using traceAB PB cA cB cP cQ left_mult_one_mat[of "P*Q" n n]
using similar_mat_wit_sym by auto
finally have traceAB: "trace A = trace B" using traceA by auto
from A cB cP have aAa: "adjoint A = adjoint((P * B) * adjoint P)" by auto
have aA: "adjoint A = P * adjoint B * adjoint P"
unfolding aAa using cP cB by (mat_assoc n)
have hA: "hermitian A" using pos positive_is_hermitian by auto
then have AaA: "A = adjoint A" using hA hermitian_def[of A] by auto
then have PBaP: "P * B * adjoint P = P * adjoint B * adjoint P" using A aA by auto
then have BaB: "B = adjoint B" using unitary_elim[of B n "adjoint B" P] uP cP cB adjoint_dim[of B n] by auto
have aPP: "adjoint P * P = 1⇩m n" using uP PB QaP by blast
have "A * A = P * B * (adjoint P * P) * B * adjoint P"
unfolding A using cP cB by (mat_assoc n)
also have "… = P * B * B * adjoint P"
unfolding aPP using cP cB by (mat_assoc n)
finally have AA: "A * A = P * B * B * adjoint P" by auto
then have tAA: "trace (A*A) = trace (P * B * B * adjoint P)" by auto
also have tBB: "… = trace (adjoint P * P * B * B)" using cP cB by (mat_assoc n)
also have "… = trace (B * B)" using uP unitary_def[of P] inverts_mat_def[of P "adjoint P"]
using PB QaP cB by auto
finally have traceAABB: "trace (A * A) = trace (B * B)" by auto
have BP: "⋀i. i < n ⟹ B$$(i, i) ≥ 0"
proof -
{
fix i assume i: "i < n"
then have "B$$(i, i) ≥ 0" using positive_eigenvalue_positive[of A n es B P Q i] cA pos charpo B by auto
then show "B$$(i, i) ≥ 0" by auto
}
qed
have Brel: "trace (B*B) ≤ (trace B)⇧2" using trace_square_less_square_trace[of B n] cB ut BP by auto
from AaA traceAABB traceAB Brel have "trace (A*adjoint A) ≤ (trace A)⇧2" by auto
then show ?thesis by auto
qed
lemma lowner_le_transitive:
fixes m n :: nat
assumes re: "n ≥ m"
shows "positive (f n - f m)"
proof -
from re show "positive (f n - f m)"
proof (induct n)
case 0
then show ?case using positive_zero
by (metis dim le_0_eq minus_r_inv_mat)
next
case (Suc n)
then show ?case
proof (cases "Suc n = m")
case True
then show ?thesis using positive_zero
by (metis dim minus_r_inv_mat)
next
case False
then show ?thesis
proof -
from False Suc have nm: "n ≥ m" by linarith
from Suc nm have pnm: "positive (f n - f m)" by auto
from inc have "positive (f (Suc n) - f n)" unfolding lowner_le_def by auto
then have pf: "positive ((f (Suc n) - f n) + (f n - f m))" using positive_add dim pnm
by (meson minus_carrier_mat)
have "(f (Suc n) - f n) + (f n - f m) = f (Suc n) + ((- f n) + f n) + (- f m)"
using local.dim by (mat_assoc dim, auto)
also have "… = f (Suc n) + 0⇩m dim dim + (- f m)"
using local.dim by (subst uminus_l_inv_mat[where nc=dim and nr=dim], auto)
also have "… = f (Suc n) - f m"
using local.dim by (mat_assoc dim, auto)
finally have re: "f (Suc n) - f n + (f n - f m) = f (Suc n) - f m" .
from pf re have "positive (f (Suc n) - f m)" by auto
then show ?thesis by auto
qed
qed
qed
qed
text ‹The sequence of matrices converges pointwise.›
lemma inc_partial_density_operator_converge:
assumes i: "i ∈ {0 ..<dim}" and j: "j ∈ {0 ..<dim}"
shows "convergent (λn. f n $$ (i, j))"
proof-
have tracefn: "trace (f n) ≥ 0 ∧ trace (f n) ≤ 1" for n
proof -
from pdo show ?thesis
unfolding partial_density_operator_def using positive_trace[of "f n"]
using dim by blast
qed
from tracefn have normf: "norm(trace (f n)) ≤ norm(trace (f (Suc n))) ∧ norm(trace (f n)) ≤ 1" for n
proof -
have trless: "trace (f n) ≤ trace (f (Suc n))"
using pdo inc dim positive_trace[of "f(Suc n) - f n"] trace_minus_linear[of "f (Suc n)" dim "f n"]
unfolding partial_density_operator_def lowner_le_def
using Complex_Matrix.positive_def by force
moreover from trless tracefn have "norm(trace (f n)) ≤ norm(trace (f (Suc n)))" unfolding cmod_def
by (simp add: less_eq_complex_def less_complex_def)
moreover from trless tracefn have "norm(trace (f n)) ≤ 1" using pdo partial_density_operator_def cmod_def
by (simp add: less_eq_complex_def less_complex_def)
ultimately show ?thesis by auto
qed
then have inctrace: "incseq (λ n. norm(trace (f n)))" by (simp add: incseq_SucI)
then have tr_sup: "(λ n. norm(trace (f n))) ⇢ (SUP i. norm (trace (f i)))"
using LIMSEQ_incseq_SUP[of "λ n. norm(trace (f n))"] pdo partial_density_operator_def normf by (meson bdd_aboveI2)
then have tr_cauchy: "Cauchy (λ n. norm(trace (f n)))" using Cauchy_convergent_iff convergent_def by blast
then have tr_cauchy_def: "∀e>0. ∃M. ∀m≥M. ∀n≥M. dist(norm(trace (f n))) (norm(trace (f m))) < e" unfolding Cauchy_def by blast
moreover have "∀m n. dist(norm(trace (f m))) (norm(trace (f n))) = norm(trace (f m) - trace (f n))"
using tracefn cmod_eq_Re dist_real_def by (auto simp: less_eq_complex_def less_complex_def)
ultimately have norm_trace: "∀e>0.∃M. ∀m≥M. ∀n≥M. norm((trace (f n)) - (trace (f m))) < e" by auto
have eq_minus: "∀ m n. trace (f m) - trace (f n) = trace (f m - f n)" using trace_minus_linear dim by metis
from eq_minus norm_trace have norm_trace_cauchy: "∀e>0.∃M. ∀m≥M. ∀n≥M. norm((trace (f n - f m))) < e" by auto
then have norm_trace_cauchy_iff: "∀e>0.∃M. ∀m≥M. ∀n≥m. norm((trace (f n - f m))) < e"
by (meson order_trans_rules(23))
then have norm_square: "∀e>0.∃M. ∀m≥M. ∀n≥m. (norm((trace (f n - f m))))⇧2 < e⇧2"
by (metis abs_of_nonneg norm_ge_zero order_less_le real_sqrt_abs real_sqrt_less_iff)
have tr_re: "∀ m. ∀ n ≥ m. trace ((f n - f m) * adjoint (f n - f m)) ≤ ((trace (f n- f m)))⇧2"
using trace_positive_eq lowner_le_transitive by auto
have tr_re_g: "∀ m. ∀ n ≥ m. trace ((f n - f m) * adjoint (f n - f m)) ≥ 0"
using lowner_le_transitive positive_trace trace_adjoint_positive by auto
have norm_trace_fmn: "norm(trace ((f n - f m) * adjoint (f n - f m))) ≤ (norm(trace (f n - f m)))⇧2" if nm: "n ≥ m" for m n
proof -
have mnA: "trace ((f n - f m) * adjoint (f n - f m)) ≤ (trace (f n - f m))⇧2" using tr_re nm by auto
have mnB: "trace ((f n - f m) * adjoint (f n - f m)) ≥ 0" using tr_re_g