Quelle  Matrix_Limit.thy

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 (verit) divide_pos_pos dual_order.strict_iff_order 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 (verit) 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 (verit))
      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)))²)"
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)))²)"
    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))))² + (complex_of_real (Im (A $$ (i, ia))))²)"
        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))))² + (complex_of_real (Im (A $$ (i, ia))))²))"
        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))))²) +
        (∑x = 0..<dim_row A. ∑xa = 0..<dim_col A. (complex_of_real (Im (A $$ (x, xa))))²)"
        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)))² ≤ trace (A * adjoint A)"
proof (simp add: trace_adjoint_eq_u less_eq_complex_def)
  have ineqi: "(cmod (A $$ (i, j)))² ≤ (∑xa = 0..<dim_col A. (cmod (A $$ (i, xa)))²)"
    using cindex member_le_sum[of j " {0 ..< dim_col A}" "λ x. (cmod (A $$ (i, x)))²"] by auto
  also have ineqj: "… ≤ (∑x = 0..<dim_row A. ∑xa = 0..<dim_col A. (cmod (A $$ (x, xa)))²)"
    using rindex member_le_sum[of i " {0 ..< dim_row A}" "λ x. ∑xa = 0..<dim_col A. (cmod (A $$ (x, xa)))²"]
    by (simp add: sum_nonneg)
  then show "(cmod (A $$ (i, j)))² ≤ (∑x = 0..<dim_row A. ∑xa = 0..<dim_col A. (cmod (A $$ (x, xa)))²)"
  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)²"
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)² = (∑ 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))²" 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))²)" using BB by auto
  finally have BBt: " trace (B * B) = (∑i = 0..<n. (B $$ (i, i))²)" by auto
  have lesseq: "∀i ∈ {0 ..<n}. (B $$ (i, i))² ≤ (∑ 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))² + 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))²" by auto
   }
   then show ?thesis by auto
 qed
  from tBtB BBt lesseq have "trace (B*B) ≤ (trace B)²"
    using sum_mono[of "{0..<n}" "λ i. (B $$ (i, i))²" "λ 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)²"
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)²" 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)²" 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))))² < e²"
    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)))²"
    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)))²" 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))²" using tr_re nm by auto
    have mnB: "trace ((f n - f m) * adjoint (f n - f m)) ≥ 0" using tr_re_g nm by auto
    from mnA mnB show ?thesis
      by (smt (verit) cmod_eq_Re less_eq_complex_def norm_power zero_complex.sel(1) zero_complex.sel(2))
  qed
  then have cauchy_adj: "∃M. ∀m≥M. ∀n≥m. norm(trace ((f n- f m) * adjoint (f n - f m))) < e²" if e: "e > 0" for e
  proof -
    have "∃M. ∀m≥M. ∀n≥m. (cmod (trace (f n - f m)))² < e²" using norm_square e by auto
    then obtain M where " ∀m≥M. ∀n≥m. (cmod (trace (f n - f m)))² < e²" by auto
    then have "∀m≥M. ∀n≥m. norm(trace ((f n- f m) * adjoint (f n - f m))) < e²" using norm_trace_fmn  by fastforce
    then show ?thesis by auto
  qed

  have norm_minus: "∀ m. ∀ n ≥ m. (norm ((f n - f m) $$ (i, j)))² ≤ trace ((f n - f m) * adjoint (f n - f m))"
    using trace_adjoint_element_ineq i j
    by (smt (verit) adjoint_dim_row carrier_matD(1) index_minus_mat(2) index_mult_mat(2) lowner_le_transitive matrix_seq_axioms matrix_seq_def positive_is_normal)
  then have norm_minus_le: "(norm ((f n - f m) $$ (i, j)))² ≤ norm (trace ((f n - f m) * adjoint (f n - f m)))" if nm: "n ≥ m" for n m
  proof -
    have "(norm ((f n - f m) $$ (i, j)))² ≤ (trace ((f n - f m) * adjoint (f n - f m)))" using norm_minus nm by auto
    also have "… = norm (trace ((f n - f m) * adjoint (f n - f m)))" using tr_re_g nm
      by (smt (verit) Re_complex_of_real less_eq_complex_def matrix_seq.trace_adjoint_eq_u matrix_seq_axioms mult_cancel_left2 norm_one norm_scaleR of_real_def of_real_hom.hom_zero)
    finally show ?thesis by (auto simp: less_eq_complex_def less_complex_def)
  qed

  from norm_minus_le cauchy_adj have cauchy_ij: "∃M. ∀m≥M. ∀n≥m. (norm ((f n - f m) $$ (i, j)))² < e²" if e: "e > 0" for e
  proof -
    have "∃M. ∀m≥M. ∀n≥m. norm(trace ((f n- f m) * adjoint (f n - f m))) < e²" using cauchy_adj e by auto
    then obtain M where " ∀m≥M. ∀n≥m. norm(trace ((f n - f m) * adjoint (f n - f m))) < e²" by auto
    then have "∀m≥M. ∀n≥m. (norm ((f n - f m) $$ (i, j)))² < e²" using norm_minus_le by fastforce
    then show ?thesis by auto
  qed
  then have cauchy_ij_norm: "∃M. ∀m≥M. ∀n≥m. (norm ((f n - f m) $$ (i, j))) < e" if e: "e > 0" for e
  proof -
    have "∃M. ∀m≥M. ∀n≥m. (norm ((f n - f m) $$ (i, j)))² < e²" using cauchy_ij e by auto
    then obtain M where mn: "∀m≥M. ∀n≥m. (norm ((f n - f m) $$ (i, j)))² < e²" by auto
    have "(norm ((f n - f m) $$ (i, j))) < e" if m: "m ≥ M" and n: "n ≥ m" for m n :: nat
    proof -
      from m n mn have "(norm ((f n- f m) $$ (i, j)))² < e²" by auto
      then show ?thesis
      using e power_less_imp_less_base by fastforce
    qed
    then show ?thesis by auto
  qed

  have cauchy_final: "∃M. ∀m≥M. ∀n≥M. norm ((f m) $$ (i, j) - (f n) $$ (i, j)) < e" if e: "e > 0" for e
  proof -
    obtain M where mnm: "∀m≥M. ∀n≥m. norm ((f n - f m) $$ (i, j)) < e" using cauchy_ij_norm e by auto
    have "norm ((f m) $$ (i, j) - (f n) $$ (i, j)) < e" if m: "m ≥ M" and n: "n ≥ M" for m n
    proof (cases "n ≥ m")
      case True
      then show ?thesis
      proof -
        from mnm m True have "norm ((f n) $$ (i, j) - (f m) $$ (i, j)) < e"
          by (metis atLeastLessThan_iff carrier_matD(1) carrier_matD(2) dim i index_minus_mat(1) j)
        then have "norm ((f m) $$ (i, j) - (f n) $$ (i, j)) < e" by (simp add: norm_minus_commute)
        then show ?thesis by auto
      qed
    next
      case False
      then show ?thesis
      proof -
        from False n mnm have norm: "norm ((f m - f n) $$ (i, j)) < e" by auto
        have minus: "(f m - f n) $$ (i, j) = f m $$ (i, j) -f n $$ (i, j)"
          by (metis atLeastLessThan_iff carrier_matD(1) carrier_matD(2) dim i index_minus_mat(1) j)
        also have "… = - (f n - f m) $$ (i, j)" using dim
          by (metis atLeastLessThan_iff carrier_matD(1) carrier_matD(2) i index_minus_mat(1) j minus_diff_eq)
        finally have fmn: "(f m - f n) $$ (i, j) = - (f n - f m) $$ (i, j)" by auto
        then have "norm ((- (f n - f m)) $$ (i, j)) < e" using norm
          by (metis (no_types, lifting) atLeastLessThan_iff carrier_matD(1) carrier_matD(2) i
              index_minus_mat(2) index_minus_mat(3) index_uminus_mat(1) j matrix_seq_axioms matrix_seq_def)
        then have "norm (((f n - f m)) $$ (i, j)) < e" using fmn norm by auto
        then have "norm (f n $$ (i, j) - f m $$ (i, j)) < e"
          by (metis minus norm norm_minus_commute)
        then have "norm (f m $$ (i, j) - f n $$ (i, j)) < e" by (simp add: norm_minus_commute)
        then show ?thesis by auto
      qed
    qed
    then show ?thesis by auto
  qed

  from cauchy_final have "Cauchy (λ n. f n $$ (i, j))" by (simp add: Cauchy_def dist_norm)
  then show ?thesis by (simp add: Cauchy_convergent_iff)
qed


definition mat_seq_minus ::  "(nat ==> complex mat) ==> complex mat ==> nat ==> complex mat" where
  "mat_seq_minus X A = (λn. X n - A)"

definition minus_mat_seq :: "complex mat ==> (nat ==> complex mat) ==> nat ==> complex mat" where
  "minus_mat_seq A X = (λn. A - X n)"

lemma pos_mat_lim_is_pos_aux:
  fixes X :: "nat ==> complex mat" and A :: "complex mat" and m :: nat
  assumes limX: "limit_mat X A m" and posX: "∃k. ∀n≥k. positive (X n)"
  shows "positive A"
proof -
  from posX obtain k where posk: "∀ n≥k. positive (X n)" by auto
  let ?Y = "λn. X (n + k)"
  have posY: "∀n. positive (?Y n)" using posk by auto

  from limX have dimXA: "∀n. X (n + k) ∈ carrier_mat m m ∧ A ∈ carrier_mat m m"
    unfolding limit_mat_def by auto

  have "(λn. X (n + k) $$ (i, j)) <---- A $$ (i, j)" if i: "i < m" and j: "j < m" for i j
  proof -
    have "(λn. X n $$ (i, j)) <---- A $$ (i, j)" using limX limit_mat_def i j by auto
    then have limseqX: "∀r>0. ∃no. ∀n≥no. dist (X n $$ (i, j)) (A $$ (i, j)) < r" unfolding LIMSEQ_def by auto
    then have "∃no. ∀n≥no. dist (X (n + k) $$ (i, j)) (A $$ (i, j)) < r" if r: "r > 0" for r
    proof -
      obtain no where "∀n≥no. dist (X n $$ (i, j)) (A $$ (i, j)) < r" using limseqX r by auto
      then have "∀n≥no. dist (X (n + k) $$ (i, j)) (A $$ (i, j)) < r" by auto
      then show ?thesis by auto
    qed
    then show ?thesis unfolding LIMSEQ_def by auto
  qed
  then have limXA: "limit_mat (λn. X (n + k)) A m" unfolding limit_mat_def using dimXA by auto

  from posY limXA have "positive A" using pos_mat_lim_is_pos[of ?Y A m] by auto
  then show ?thesis by auto
qed

lemma minus_mat_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_seq_minus X B) (A - B) m"
proof -
  have dimXAB: "∀n. X n - B ∈ carrier_mat m m ∧ A - B ∈ carrier_mat m m" using index_minus_mat dimB by auto
  have "(λn. (X n - B) $$ (i, j)) <---- (A - B) $$ (i, j)" if i: "i < m" and j: "j < m" for i j
  proof -
    from limX i j have "(λn. (X n) $$ (i, j)) <---- (A) $$ (i, j)" unfolding limit_mat_def by auto
    then have X: "∀r>0. ∃no. ∀n≥no. dist (X n $$ (i, j)) (A $$ (i, j)) < r" unfolding LIMSEQ_def by auto
    then have XB: "∃no. ∀n≥no. dist ((X n - B) $$ (i, j)) ((A - B) $$ (i, j)) < r" if r: "r > 0" for r
    proof -
      obtain no where "∀n≥no. dist (X n $$ (i, j)) (A $$ (i, j)) < r"  using r X by auto
      then have dist:  "∀n≥no. norm (X n $$ (i, j) - A $$ (i, j)) < r" unfolding dist_norm  by auto
      then have "norm ((X n - B) $$ (i, j) - (A - B) $$ (i, j)) < r" if n: "n ≥ no" for n
      proof -
        have "(X n - B) $$ (i, j) - (A - B) $$ (i, j) = (X n) $$ (i, j) - A $$ (i, j)"
          using dimB i j by auto
        then have "norm ((X n - B) $$ (i, j) - (A - B) $$ (i, j)) = norm ((X n) $$ (i, j) - A $$ (i, j))" by auto
        then show ?thesis using dist n by auto
      qed
      then show ?thesis using dist_norm by metis
    qed
    then show ?thesis unfolding LIMSEQ_def by auto
  qed
  then show ?thesis
    unfolding limit_mat_def mat_seq_minus_def using dimXAB by auto
qed

lemma mat_minus_limit:
  fixes X :: "nat ==> complex mat" and A :: "complex mat" and m :: nat and B :: "complex mat"
  assumes dimA: "A ∈ carrier_mat m m" and limX: "limit_mat X A m"
  shows "limit_mat (minus_mat_seq B X) (B - A) m"
proof-
  have dimX : "∀n. X n ∈ carrier_mat m m" using limX unfolding limit_mat_def by auto
  then have dimXAB: "∀n. B - X n ∈ carrier_mat m m ∧ B - A ∈ carrier_mat m m" using index_minus_mat dimA
    by (simp add: minus_carrier_mat)

  have "(λn. (B - X n) $$ (i, j)) <---- (B - A) $$ (i, j)" if i: "i < m" and j: "j < m" for i j
  proof -
    from limX i j have "(λn. (X n) $$ (i, j)) <---- (A) $$ (i, j)" unfolding limit_mat_def by auto
    then have X: "∀r>0. ∃no. ∀n≥no. dist (X n $$ (i, j)) (A $$ (i, j)) < r" unfolding LIMSEQ_def by auto
    then have XB: "∃no. ∀n≥no. dist ((B - X n) $$ (i, j)) ((B - A) $$ (i, j)) < r" if r: "r > 0" for r
    proof -
      obtain no where "∀n≥no. dist (X n $$ (i, j)) (A $$ (i, j)) < r" using r X by auto
      then have dist: "∀n≥no. norm (X n $$ (i, j) - A $$ (i, j)) < r" unfolding dist_norm by auto
      then have "norm ((B - X n) $$ (i, j) - (B - A) $$ (i, j)) < r" if n: "n ≥ no" for n
      proof -
        have "(B - X n) $$ (i, j) - (B - A) $$ (i, j) = - ((X n) $$ (i, j) - A $$ (i, j))"
          using dimA i j
          by (smt (verit) cancel_ab_semigroup_add_class.diff_right_commute cancel_comm_monoid_add_class.diff_cancel carrier_matD(1) carrier_matD(2) diff_add_cancel dimX index_minus_mat(1) minus_diff_eq)
        then have "norm ((B - X n) $$ (i, j) - (B - A) $$ (i, j)) = norm ((X n) $$ (i, j) - A $$ (i, j))"
          by (metis norm_minus_cancel)
        then show ?thesis using dist n by auto
      qed
      then show ?thesis using dist_norm by metis
    qed
    then show ?thesis unfolding LIMSEQ_def by auto
  qed
  then have "limit_mat (minus_mat_seq B X) (B - A) m"
    unfolding limit_mat_def minus_mat_seq_def using dimXAB by auto
  then show ?thesis by auto
qed

lemma lowner_lub_form:
  "lowner_is_lub (mat dim dim (λ (i, j). (lim (λ n. (f n) $$ (i, j)))))"
proof -
  from inc_partial_density_operator_converge
  have conf: "∀ i ∈ {0 ..<dim}. ∀ j ∈ {0 ..<dim}. convergent (λ n. f n $$ (i, j))" by auto
  let ?A = "mat dim dim (λ (i, j). (lim (λ n. (f n) $$ (i, j))))"
  have dim_A: "?A ∈ carrier_mat dim dim" by auto
  have lim_A: "(λn. f n $$ (i, j)) <---- mat dim dim (λ(i, j). lim (λn. f n $$ (i, j))) $$ (i, j)"
    if i: "i < dim" and j: "j < dim" for i j
  proof -
    from i j have ij: "mat dim dim (λ(i, j). lim (λn. f n $$ (i, j))) $$ (i, j) = lim (λn. f n $$ (i, j))"
      by (metis case_prod_conv index_mat(1))
    have "convergent (λn. f n $$ (i, j))" using conf i j by auto
    then have "(λn. f n $$ (i, j)) <---- lim (λn. f n $$ (i, j)) " using convergent_LIMSEQ_iff by auto
    then show ?thesis using ij by auto
  qed

  from dim dim_A lim_A have lim_mat_A: "limit_mat f ?A dim" unfolding limit_mat_def by auto

  have is_ub: "f n ≤_L ?A" for n
  proof -
    have "∀ m ≥ n. positive (f m - f n)" using lowner_le_transitive by auto
    then have le: "∀ m ≥ n. f n ≤_L f m " unfolding lowner_le_def using dim
      by (metis carrier_matD(1) carrier_matD(2))
    have dimn: "f n ∈ carrier_mat dim dim" using dim by auto
    then have limAf: "limit_mat (mat_seq_minus f (f n)) (?A - f n) dim" using minus_mat_limit lim_mat_A by auto

    have " ∀m≥n. positive (f m - f n)" using lowner_le_transitive by auto
    then have "∃k. ∀m≥k. positive (f m - f n)" by auto
    then have posAf: "∃ k. ∀ m ≥ k. positive ((mat_seq_minus f (f n)) m)" unfolding mat_seq_minus_def by auto

    from limAf posAf have "positive (?A - f n)" using pos_mat_lim_is_pos_aux by auto
    then have "f n ≤_L mat dim dim (λ(i, j). lim (λn. f n $$ (i, j)))" unfolding lowner_le_def using dim by auto
    then show ?thesis by auto
  qed

  have is_lub: "?A ≤_L M'" if ub: "∀n. f n ≤_L M'" for M'
  proof -
    have dim_M: "M' ∈ carrier_mat dim dim" using ub unfolding lowner_le_def using dim
      by (metis carrier_matD(1) carrier_matD(2) carrier_mat_triv)
    from ub have posAf: "∀ n. positive (minus_mat_seq M' f n)" unfolding minus_mat_seq_def lowner_le_def by auto
    have limAf: "limit_mat (minus_mat_seq M' f) (M' - ?A) dim"
      using mat_minus_limit dim_A lim_mat_A by auto
    from posAf limAf have  "positive (M' - ?A)" using pos_mat_lim_is_pos_aux by auto
    then have "?A ≤_L M'" unfolding lowner_le_def using dim dim_A dim_M by auto
    then show ?thesis by auto
  qed

  from is_ub is_lub show ?thesis unfolding lowner_is_lub_def by auto
qed

text ‹Lowner partial order is a complete partial order.›
lemma lowner_lub_exists: "∃M. lowner_is_lub M"
  using lowner_lub_form by auto

lemma lowner_lub_unique: "∃!M. lowner_is_lub M"
proof (rule HOL.ex_ex1I)
  show "∃M. lowner_is_lub M"
    by (rule lowner_lub_exists)
next
  fix M N
  assume M: "lowner_is_lub M" and N: "lowner_is_lub N"
  have Md: "M ∈ carrier_mat dim dim" using M by (rule lowner_is_lub_dim)
  have Nd: "N ∈ carrier_mat dim dim" using N by (rule lowner_is_lub_dim)
  have MN: "M ≤_L N" using M N by (simp add: lowner_is_lub_def)
  have NM: "N ≤_L M" using M N by (simp add: lowner_is_lub_def)
  show "M = N" using MN NM by (auto intro: lowner_le_antisym[OF Md Nd])
qed

definition lowner_lub :: "complex mat" where
  "lowner_lub = (THE M. lowner_is_lub M)"

lemma lowner_lub_prop: "lowner_is_lub lowner_lub"
  unfolding lowner_lub_def
  apply (rule HOL.theI')
  by (rule lowner_lub_unique)

lemma lowner_lub_is_limit:
  "limit_mat f lowner_lub dim"
proof -
  define A where "A = lowner_lub"
  then have "A = (THE M. lowner_is_lub M)" using lowner_lub_def by auto
  then have Af: "A = (mat dim dim (λ (i, j). (lim (λ n. (f n) $$ (i, j)))))"
    using lowner_lub_form lowner_lub_unique by auto
  show "limit_mat f A dim" unfolding Af limit_mat_def
    apply (auto simp add: dim)
  proof -
    fix i j assume dims: "i < dim" "j < dim"
    then have "convergent (λn. f n $$ (i, j))" using inc_partial_density_operator_converge by auto
    then show "(λn. f n $$ (i, j)) <---- lim (λn. f n $$ (i, j))" using convergent_LIMSEQ_iff by auto
  qed
qed

lemma lowner_lub_trace:
  assumes "∀ n. trace (f n) ≤ x"
  shows "trace lowner_lub ≤ x"
proof -
  have "∀ n. trace (f n) ≥ 0" using positive_trace pdo unfolding partial_density_operator_def
    using dim by blast
  then have Re: "∀ n. Re (trace (f n)) ≥ 0 ∧ Im (trace (f n)) = 0"
    by (auto simp: less_eq_complex_def less_complex_def)
  then have lex: "∀ n. Re (trace (f n)) ≤ Re x ∧ Im x = 0" using assms
    by (auto simp: less_eq_complex_def less_complex_def)

  have "limit_mat f lowner_lub dim"  using lowner_lub_is_limit by auto
  then have conv: "(λn. trace (f n)) <---- trace lowner_lub" using mat_trace_limit by auto
  then have "(λn. Re (trace (f n))) <---- Re (trace lowner_lub)"
    by (simp add: tendsto_Re)
  then have Rell: "Re (trace lowner_lub) ≤ Re x"
    using lex Lim_bounded[of "(λn. Re (trace (f n)))" "Re (trace lowner_lub)" 0 "Re x"] by simp

  from conv have "(λn. Im (trace (f n))) <---- Im (trace lowner_lub)"
    by (simp add: tendsto_Im)
  then  have Imll: "Im (trace lowner_lub) = 0" using Re
    by (simp add: Lim_bounded Lim_bounded2 dual_order.antisym)

  from Rell Imll lex show ?thesis by (simp add: less_eq_complex_def less_complex_def)
qed

lemma lowner_lub_is_positive:
  shows "positive lowner_lub"
  using lowner_lub_is_limit pos_mat_lim_is_pos pdo unfolding partial_density_operator_def by auto

end

subsection ‹Finite sum of matrices›

text ‹Add f in the interval [0, n)›
fun matrix_sum :: "nat ==> (nat ==> 'b::semiring_1 mat) ==> nat ==> 'b mat" where
  "matrix_sum d f 0 = 0_m d d"
| "matrix_sum d f (Suc n) = f n + matrix_sum d f n"

definition matrix_inf_sum :: "nat ==> (nat ==> complex mat) ==> complex mat" where
  "matrix_inf_sum d f = matrix_seq.lowner_lub (λn. matrix_sum d f n)"

lemma matrix_sum_dim:
  fixes f :: "nat ==> 'b::semiring_1 mat"
  shows "(∧k. k < n ==> f k ∈ carrier_mat d d) ==> matrix_sum d f n ∈ carrier_mat d d"
proof (induct n)
  case 0
  show ?case by auto
next
  case (Suc n)
  then have "f n ∈ carrier_mat d d" by auto
  then show ?case using Suc by auto
qed

lemma matrix_sum_cong:
  fixes f :: "nat ==> 'b::semiring_1 mat"
  shows "(∧k. k < n ==> f k = f' k) ==> matrix_sum d f n = matrix_sum d f' n"
proof (induct n)
  casecase 0
  show
next
 ( java.lang.StringIndexOutOfBoundsException: Index 14 out of bounds for length 14
  then( groupI addjava.lang.StringIndexOutOfBoundsException: Index 48 out of bounds for length 48
qed

lemma matrix_sum_add:
  fixes f :: "nat ==> 'b::semiring_1 mat" and  g :: "nat ==> 'b::semiring_1 mat" and  h :: "nat ==> 'b::semiring_1 mat"
  shows "(∧k. k < n ==> f k ∈ carrier_mat d d) ==> (∧k. k < n ==> g k ∈ carrier_mat d d) ==> (∧k. k < n ==> h k ∈ carrier_mat d d) ==>
     (∧k. k < n ==> f k = g k + h k) ==> matrix_sum d f n = matrix_sum d g n + matrix_sum d h n"
proof (induct n)
  case 0
  then show ?case by auto
next
  case (Suc n)
  then show ?case
  proof -
    have gh: "matrix_sum d g n ∈ carrier_mat d d ∧ matrix_sum d h n ∈ carrier_mat d d"
      using matrix_sum_dim Suc(3, 4) by (simp add: matrix_sum_dim)

    have nSuc: "n < Suc n" by auto
    have sumf: "matrix_sum d f n = matrix_sum d g n + matrix_sum d h n" using Suc by auto
    have "matrix_sum d f (Suc n) = matrix_sum d g (Suc n) + matrix_sum d h (Suc n)"
      unfolding matrix_sum.simps Suc(5)[OF nSuc] sumf
      apply (mat_assoc d) using gh Suc by auto
    then show ?thesis by auto
  qed
qed

lemma matrix_sum_smult:
  fixes f :: "nat ==> 'b::semiring_1 mat"
  shows "(∧k. k < n ==> f k ∈ carrier_mat d d) ==>
        matrix_sum d (λ k. c ⋅_m f k) n = c ⋅_m matrix_sum d f n"
proof (induct n)
  case 0
  then show ?case by auto
next
  case (Suc n)
  then show ?case
    apply auto
    using add_smult_distrib_left_mat Suc matrix_sum_dim
    by (metis lessI less_SucI)
qed

lemma matrix_sum_remove:
  fixes f :: "nat ==> 'b::semiring_1 mat"
  assumes j: "j < n"
    and df: "(∧k. k < n ==> f k ∈ carrier_mat d d)"
    and f': "(∧k. f' k = (if k = j then 0_m d d else f k))"
  shows "matrix_sum d f n = f j + matrix_sum d f' n"
proof -
  have df': "∧k. k < n ==> f' k ∈ carrier_mat d d" using f' df by auto
  have dsf: "k < n ==> matrix_sum d f k ∈ carrier_mat d d" for k using matrix_sum_dim[OF df] by auto
  have dsf': "k < n ==> matrix_sum d f' k ∈ carrier_mat d d" for k using matrix_sum_dim[OF df'] by auto
  have flj: "∧k. k < j ==> f' k = f k" using j f' by auto
  then have "matrix_sum d f j = matrix_sum d f' j" using matrix_sum_cong[of j f' f, OF flj] df df' j by auto
  then have eqj: "matrix_sum d f (Suc j) = f j + matrix_sum d f' (Suc j)" unfolding matrix_sum.simps
    by (subst (1) f', simp add: df dsf' j)
  have lm: "(j + 1) + l ≤ n ==> matrix_sum d f ((j + 1) + l) = f j + matrix_sum d f' ((j + 1) + l)" for l
  proof (induct l)
    case 0
    show ?case using j eqj by auto
  next
    case (Suc l) then have eq: "matrix_sum d f ((j + 1) + l) = f j + matrix_sum d f' ((j + 1) + l)" by auto
    have s: "((j + 1) + Suc l) = Suc ((j + 1) + l)" by simp
    have eqf': "f' (j + 1 + l) = f (j + 1 + l)" using f' Suc by auto
    have dims: "f (j + 1 + l) ∈ carrier_mat d d" "f j ∈ carrier_mat d d" "matrix_sum d f' (j + 1 + l) ∈ carrier_mat d d" using df df' dsf' Suc by auto
    show ?case apply (subst (1 2) s) unfolding matrix_sum.simps
      apply (subst eq, subst eqf')
      apply (mat_assoc d) using dims by auto
  qed
  have p: "(j + 1) + (n - j - 1) ≤ n" using j by auto
  show ?thesis using lm[OF p] j by auto
qed

lemma matrix_sum_Suc_remove_head:
  fixes f :: "nat ==> complex mat"
  shows "(∧k. k < n + 1 ==> f k ∈ carrier_mat d d) ==>
    matrix_sum d f (n + 1) = f 0 + matrix_sum d (λk. f (k + 1)) n"
proof (induct n)
  case 0
  then show ?case by auto
next
  case (Suc n)
  then have dSS: "∧k. k < Suc (Suc n) ==> f k ∈ carrier_mat d d" by auto
  have ds: "matrix_sum d (λk. f (k + 1)) n ∈ carrier_mat d d" using matrix_sum_dim[OF dSS, of "n" "λk. k + 1"] by auto
  have "matrix_sum d f (Suc n + 1) = f (n + 1) + matrix_sum d f (n + 1)" by auto
  also have "… = f (n + 1) + (f 0 + matrix_sum d (λk. f (k + 1)) n)" using Suc by auto
  also have "… = f 0 + (f (n + 1) + matrix_sum d (λk. f (k + 1)) n)"
    using ds apply (mat_assoc d) using dSS by auto
  finally show ?case by auto
qed

lemma matrix_sum_positive:
  fixes f :: "nat ==> complex mat"
  shows "(∧k. k < n ==> f k ∈ carrier_mat d d) ==> (∧k. k < n ==> positive (f k))
    ==> positive (matrix_sum d f n)"
proof (induct n)
  case 0
  show ?case using positive_zero by auto
next
  case (Suc n)
  then have dfn: "f n ∈ carrier_mat d d" and psn: "positive (matrix_sum d f n)" and pn: "positive (f n)" and d: "k < n ==> f k ∈ carrier_mat d d" for k by auto
  then have dsn: "matrix_sum d f n ∈ carrier_mat d d" using matrix_sum_dim by auto
  show ?case unfolding matrix_sum.simps using positive_add[OF pn psn dfn dsn] by auto
qed

lemma matrix_sum_mult_right:
  shows "(∧k. k < n ==> f k ∈ carrier_mat d d) ==> A ∈ carrier_mat d d
    ==> matrix_sum d (λk. (f k) * A) n = matrix_sum d (λk. f k) n * A"
proof (induct n)
  case 0
  then show ?case by auto
next
  case (Suc n)
  then have "k < n ==> f k ∈ carrier_mat d d" and dfn: "f n ∈ carrier_mat d d" for k by auto
  then have dsfn: "matrix_sum d f n ∈ carrier_mat d d" using matrix_sum_dim by auto
  have "(f n + matrix_sum d f n) * A = f n * A + matrix_sum d f n * A"
    apply (mat_assoc d) using Suc dsfn by auto
  also have "… = f n * A + matrix_sum d (λk. f k * A) n" using Suc by auto
  finally show ?case by auto
qed

lemma matrix_sum_add_distrib:
  shows "(∧k. k < n ==> f k ∈ carrier_mat d d) ==> (∧k. k < n ==> g k ∈ carrier_mat d d)
    ==> matrix_sum d (λk. (f k) + (g k)) n = matrix_sum d f n + matrix_sum d g n"
proof (induct n)
  case 0
  then show ?case by auto
next
  case (Suc n)
  then have dfn: "f n ∈ carrier_mat d d" and dgn: "g n ∈ carrier_mat d d"
    and dfk: "k < n ==> f k ∈ carrier_mat d d" and dgk: "k < n ==> g k ∈ carrier_mat d d"
    and eq: "matrix_sum d (λk. f k + g k) n = matrix_sum d f n + matrix_sum d g n" for k by auto
  have dsf: "matrix_sum d f n ∈ carrier_mat d d" using matrix_sum_dim dfk by auto
  have dsg: "matrix_sum d g n ∈ carrier_mat d d" using matrix_sum_dim dgk by auto
  show ?case unfolding matrix_sum.simps eq
    using dfn dgn dsf dsg by (mat_assoc d)
qed

lemma matrix_sum_minus_distrib:
  fixes f g :: "nat ==> complex mat"
  shows "(∧k. k < n ==> f k ∈ carrier_mat d d) ==> (∧k. k < n ==> g k ∈ carrier_mat d d)
    ==> matrix_sum d (λk. (f k) - (g k)) n = matrix_sum d f n - matrix_sum d g n"
proof -
  have eq: "-1 ⋅_m g k = - g k" for k by auto
  assume dfk: "∧k. k < n ==> f k ∈ carrier_mat d d" and dgk: "∧k. k < n ==> (g k) ∈ carrier_mat d d"
  then have "k < n ==> (f k) - (g k) = (f k) + (- (g k))" for k by auto
  then have "matrix_sum d (λk. (f k) - (g k)) n = matrix_sum d (λk. (f k) + (- (g k))) n"
    using matrix_sum_cong[of n "λk. (f k) - (g k)"] dfk dgk by auto
  also have "… = matrix_sum d f n + matrix_sum d (λk. - (g k)) n"
    using matrix_sum_add_distrib[of n "f"] dfk dgk by auto
  also have "… = matrix_sum d f n - matrix_sum d g n"
    apply (subgoal_tac "matrix_sum d (λk. - (g k)) n = - matrix_sum d g n", auto)
    apply (subgoal_tac "- 1 ⋅_m matrix_sum d g n = - matrix_sum d g n")
    by (simp add: matrix_sum_smult[of n g d "-1", OF dgk, simplified eq, simplified], auto)
  finally show ?thesis .
qed

lemma matrix_sum_shift_Suc:
  shows "(∧k. k < (Suc n) ==> f k ∈ carrier_mat d d)
    ==> matrix_sum d f (Suc n) = f 0 + matrix_sum d (λk. f (Suc k)) n"
proof (induct n)
  case 0
  then show ?case by auto
next
  case (Suc n)
  have dfk: "k < Suc (Suc n) ==> f k ∈ carrier_mat d d" for k using Suc by auto
  have dsSk: "k < Suc n ==> matrix_sum d (λk. f (Suc k)) n ∈ carrier_mat d d" for k using matrix_sum_dim[of _ "λk. f (Suc k)"] dfk by fastforce
  have "matrix_sum d f (Suc (Suc n)) = f (Suc n) + matrix_sum d f (Suc n)" by auto
  also have "… = f (Suc n) + f 0 + matrix_sum d (λk. f (Suc k)) n" using Suc dsSk assoc_add_mat[of "f (Suc n)" d d "f 0"] by fastforce
  also have "… = f 0 + (f (Suc n) + matrix_sum d (λk. f (Suc k)) n)" apply (mat_assoc d) using dsSk dfk by auto
  also have "… = f 0 + matrix_sum d (λk. f (Suc k)) (Suc n)"  by auto
  finally show ?case .
qed

lemma lowner_le_matrix_sum:
  fixes f g :: "nat ==> complex mat"
  shows "(∧k. k < n ==> f k ∈ carrier_mat d d) ==> (∧k. k < n ==> g k ∈ carrier_mat d d)
    ==> (∧k. k < n ==> f k ≤_L g k)
    ==> matrix_sum d f n ≤_L matrix_sum d g n"
proof (induct n)
  case 0
  show ?case unfolding matrix_sum.simps using lowner_le_refl[of "0_m d d" d] by auto
next
  case (Suc n)
  then have dfn: "f n ∈ carrier_mat d d" and dgn: "g n ∈ carrier_mat d d" and le1: "f n ≤_L g n" by auto
  then have le2: "matrix_sum d f n ≤_L matrix_sum d g n" using Suc by auto
  have "k < n ==> f k ∈ carrier_mat d d" for k using Suc by auto
  then have dsf: "matrix_sum d f n ∈ carrier_mat d d" using matrix_sum_dim by auto
  have "k < n ==> g k ∈ carrier_mat d d" for k using Suc by auto
  then have dsg: "matrix_sum d g n ∈ carrier_mat d d" using matrix_sum_dim by auto
  show ?case unfolding matrix_sum.simps using lowner_le_add dfn dsf dgn dsg le1 le2 by auto
qed

lemma lowner_lub_add:
  assumes "matrix_seq d f" "matrix_seq d g" "∀ n. trace (f n + g n) ≤ 1"
  shows "matrix_seq.lowner_lub (λn. f n + g n) = matrix_seq.lowner_lub f + matrix_seq.lowner_lub g"
proof -
  have msf: "matrix_seq.lowner_is_lub f (matrix_seq.lowner_lub f)" using assms(1) matrix_seq.lowner_lub_prop by auto
  then have "limit_mat f (matrix_seq.lowner_lub f) d" using matrix_seq.lowner_lub_is_limit assms by auto
  then have lim1: "∀i<d. ∀j<d. (λn. f n $$ (i, j)) <---- (matrix_seq.lowner_lub f) $$ (i, j)" using limit_mat_def assms by auto

  have msg: "matrix_seq.lowner_is_lub g (matrix_seq.lowner_lub g)" using assms(2) matrix_seq.lowner_lub_prop by auto
  then have "limit_mat g (matrix_seq.lowner_lub g) d" using matrix_seq.lowner_lub_is_limit assms by auto
  then have lim2: "∀i<d. ∀j<d. (λn. g n $$ (i, j)) <---- (matrix_seq.lowner_lub g) $$ (i, j)" using limit_mat_def assms by auto

  have "∀n. f n + g n ∈ carrier_mat d d" using assms unfolding matrix_seq_def by fastforce
  moreover have "∀n. partial_density_operator (f n + g n)" using assms
    unfolding matrix_seq_def partial_density_operator_def using positive_add by blast
  moreover have "(f n + g n) ≤_L (f (Suc n) + g (Suc n))" for n
    using assms
    unfolding matrix_seq_def using lowner_le_add[of "f n" d  "f (Suc n)" "g n" "g (Suc n)"] by auto
  ultimately have msfg: "matrix_seq d (λn. f n + g n)" using assms unfolding matrix_seq_def by auto
  then have mslfg: "matrix_seq.lowner_is_lub (λn. f n + g n) (matrix_seq.lowner_lub (λn. f n + g n))"
    using matrix_seq.lowner_lub_prop by auto
  then have "limit_mat (λn. f n + g n) (matrix_seq.lowner_lub (λn. f n + g n)) d" using matrix_seq.lowner_lub_is_limit msfg by auto
  then have lim3: "∀i<d. ∀j<d. (λn. (f n + g n) $$ (i, j)) <---- (matrix_seq.lowner_lub (λn. f n + g n)) $$ (i, j)" using limit_mat_def assms by auto

  have "∀ i<d. ∀ j<d. ∀ n. (f n + g n) $$ (i, j) = f n $$ (i, j) + g n $$ (i, j)" using assms unfolding matrix_seq_def
    by (metis carrier_matD(1) carrier_matD(2) index_add_mat(1))
  then have add: "∀i<d. ∀j<d. (λn. f n $$ (i, j) + g n $$ (i, j)) <---- (matrix_seq.lowner_lub (λn. f n + g n)) $$ (i, j)" using lim3 by auto
  have "matrix_seq.lowner_lub f $$ (i, j) + matrix_seq.lowner_lub g $$ (i, j) = matrix_seq.lowner_lub (λn. f n + g n) $$ (i, j)"
    if i: "i < d" and j: "j < d" for i j
  proof -
    have "(λn. f n $$ (i, j)) <---- matrix_seq.lowner_lub f $$ (i, j)" using lim1 i j by auto
    moreover have "(λn. g n $$ (i, j)) <---- matrix_seq.lowner_lub g $$ (i, j)" using lim2 i j by auto
    ultimately have "(λn. f n $$ (i, j) + g n $$ (i, j)) <---- matrix_seq.lowner_lub f $$ (i, j) + matrix_seq.lowner_lub g $$ (i, j)"
      using tendsto_add[of "λn. f n $$ (i, j)" "matrix_seq.lowner_lub f $$ (i, j)" sequentially "λn. g n $$ (i, j)" "matrix_seq.lowner_lub g $$ (i, j)"] by auto
    moreover have "(λn. f n $$ (i, j) + g n $$ (i, j)) <---- matrix_seq.lowner_lub (λn. f n + g n) $$ (i, j)"  using add i j by auto
    ultimately show ?thesis using LIMSEQ_unique by auto
  qed
  moreover have "matrix_seq.lowner_lub f ∈ carrier_mat d d" using matrix_seq.lowner_is_lub_dim assms(1) msf unfolding matrix_seq_def by auto
  moreover have "matrix_seq.lowner_lub g ∈ carrier_mat d d" using matrix_seq.lowner_is_lub_dim assms(2) msg unfolding matrix_seq_def by auto
  moreover have "matrix_seq.lowner_lub (λn. f n + g n) ∈ carrier_mat d d" using matrix_seq.lowner_is_lub_dim  msfg mslfg unfolding matrix_seq_def by auto
  ultimately show ?thesis  unfolding matrix_seq_def using mat_eq_iff by auto
qed

lemma lowner_lub_scale:
  fixes c :: real
  assumes "matrix_seq d f"  "∀ n. trace (c ⋅_m f n) ≤ 1"  "c≥0"
  shows "matrix_seq.lowner_lub (λn. c ⋅_m f n) = c ⋅_m matrix_seq.lowner_lub f"
proof -
  have msf: "matrix_seq.lowner_is_lub f (matrix_seq.lowner_lub f)"
    using assms(1) matrix_seq.lowner_lub_prop by auto
  then have "limit_mat f (matrix_seq.lowner_lub f) d"
    using matrix_seq.lowner_lub_is_limit assms by auto
  then have lim1: "∀i<d. ∀j<d. (λn. f n $$ (i, j)) <---- (matrix_seq.lowner_lub f) $$ (i, j)"
    using limit_mat_def assms by auto

  have dimcf: "∀n. c ⋅_m f n ∈ carrier_mat d d" using assms unfolding matrix_seq_def by fastforce
  moreover have "∀n. partial_density_operator (c ⋅_m f n)" using assms
    unfolding matrix_seq_def partial_density_operator_def using positive_scale by blast
  moreover have "∀n. c ⋅_m f n ≤_L c ⋅_m f (Suc n)" using lowner_le_smult assms(1,3)
    unfolding matrix_seq_def partial_density_operator_def by blast
  ultimately have mscf: "matrix_seq d (λn. c ⋅_m f n)"  unfolding matrix_seq_def by auto
  then have mslfg: "matrix_seq.lowner_is_lub (λn. c ⋅_m f n) (matrix_seq.lowner_lub (λn. c ⋅_m f n))"
    using matrix_seq.lowner_lub_prop by auto
  then have "limit_mat (λn. c ⋅_m f n) (matrix_seq.lowner_lub (λn. c ⋅_m f n)) d"
    using matrix_seq.lowner_lub_is_limit mscf by auto
  then have lim3: "∀i<d. ∀j<d. (λn. (c ⋅_m f n) $$ (i, j)) <---- (matrix_seq.lowner_lub (λn. c ⋅_m f n)) $$ (i, j)"
    using limit_mat_def assms by auto

  from mslfg mscf have dleft: "matrix_seq.lowner_lub (λn. c ⋅_m f n) ∈ carrier_mat d d"
    using matrix_seq.lowner_is_lub_dim by auto
  have dllf: "matrix_seq.lowner_lub f ∈ carrier_mat d d"
    using matrix_seq.lowner_is_lub_dim assms(1) msf unfolding matrix_seq_def by auto
  then  have dright: "c ⋅_m matrix_seq.lowner_lub f ∈ carrier_mat d d" using index_smult_mat(2,3) by auto
  have "∀ i<d. ∀ j<d. ∀ n. (c ⋅_m f n) $$ (i, j) = c * f n $$ (i, j)"
    using assms(1) unfolding matrix_seq_def using index_smult_mat(1)
    by (metis carrier_matD(1-2))
  then have smult: "∀i<d. ∀j<d. (λn. c * f n $$ (i, j)) <---- (matrix_seq.lowner_lub (λn. c ⋅_m f n)) $$ (i, j)"
    using lim3 by auto
  have ij: "(c ⋅_m matrix_seq.lowner_lub f) $$ (i, j) = (matrix_seq.lowner_lub (λn. c ⋅_m f n)) $$ (i, j)"
    if i: "i < d" and j: "j < d" for i j
  proof -
    have "(λn. f n $$ (i, j)) <---- matrix_seq.lowner_lub f $$ (i, j)" using lim1 i j by auto
    moreover have "∀i<d. ∀j<d.(c ⋅_m matrix_seq.lowner_lub f) $$ (i, j) = c * matrix_seq.lowner_lub f $$ (i, j)"
      using index_smult_mat dllf by fastforce
    ultimately have "∀i<d. ∀j<d. (λn. c * f n $$ (i, j)) <----(c ⋅_m matrix_seq.lowner_lub f) $$ (i, j)"
      using tendsto_intros(18)[of "λn. c" "c" sequentially "λn. f n $$ (i, j)" "matrix_seq.lowner_lub f $$ (i, j)"] i j
      by (simp add: lim1 tendsto_mult_left)
    then show ?thesis using smult i j LIMSEQ_unique by metis
  qed

  from dleft dright ij show ?thesis
    using mat_eq_iff[of "matrix_seq.lowner_lub (λn. c ⋅_m f n)" "c ⋅_m matrix_seq.lowner_lub f"]
    by (metis (mono_tags) carrier_matD(1) carrier_matD(2))
qed

lemma trace_matrix_sum_linear:
  fixes f :: "nat ==> complex mat"
  shows "(∧k. k < n ==> f k ∈ carrier_mat d d) ==> trace (matrix_sum d f n) = sum (λk. trace (f k)) {0..<n}"
proof (induct n)
  case 0
  show ?case by auto
next
  case (Suc n)
  then have "∧k. k < n ==> f k ∈ carrier_mat d d" by auto
  then have ds: "matrix_sum d f n ∈ carrier_mat d d" using matrix_sum_dim by auto
  have "trace (matrix_sum d f (Suc n)) = trace (f n) + trace (matrix_sum d f n)"
    unfolding matrix_sum.simps apply (mat_assoc d) using ds Suc by auto
  also have "… = sum (trace ∘ f) {0..<n} + (trace ∘ f) n" using Suc by auto
  also have "… = sum (trace ∘ f) {0..<Suc n}" by auto
  finally show ?case by auto
qed

lemma matrix_sum_distrib_left:
  fixes f :: "nat ==> complex mat"
  shows "P ∈ carrier_mat d d ==> (∧k. k < n ==> f k ∈ carrier_mat d d) ==> matrix_sum d (λk. P * (f k)) n = P * (matrix_sum d f n)"
proof (induct n)
  case 0
  show ?case unfolding matrix_sum.simps using 0 by auto
next
  case (Suc n)
  then have "∧k. k < n ==> f k ∈ carrier_mat d d" by auto
  then have ds: "matrix_sum d f n ∈ carrier_mat d d" using matrix_sum_dim by auto
  then have dPf: "∧k. k < n ==> P * f k ∈ carrier_mat d d" using Suc by auto
  then have "matrix_sum d (λk. P * f k) n ∈ carrier_mat d d" using matrix_sum_dim[OF dPf] by auto
  have "matrix_sum d (λk. P * f k) (Suc n) = P * f n + matrix_sum d (λk. P * f k) n " unfolding matrix_sum.simps using Suc(2) by auto
  also have "… = P * f n + P * matrix_sum d f n" using Suc by auto
  also have "… = P * (f n + matrix_sum d f n)" apply (mat_assoc d) using ds dPf Suc by auto
  finally show "matrix_sum d (λk. P * f k) (Suc n) = P * (matrix_sum d f (Suc n))" by auto
qed

subsection ‹Measurement›

definition measurement :: "nat ==> nat ==> (nat ==> complex mat) ==> bool" where
  "measurement d n M ⟷ (∀j < n. M j ∈ carrier_mat d d)
                        ∧ matrix_sum d (λj. (adjoint (M j)) * M j) n = 1_m d"

lemma measurement_dim:
  assumes "measurement d n M"
  shows "∧k. k < n ==> (M k) ∈ carrier_mat d d"
  using assms unfolding measurement_def by auto

lemma measurement_id2:
  assumes "measurement d 2 M"
  shows "adjoint (M 0) * M 0 + adjoint (M 1) * M 1 = 1_m d"
proof -
  have ssz: "(Suc (Suc 0)) = 2" by auto
  have "M 0 ∈ carrier_mat d d" "M 1 ∈ carrier_mat d d" using assms measurement_def by auto
  then have "adjoint (M 0) * M 0 + adjoint (M 1) * M 1 = matrix_sum d (λj. (adjoint (M j)) * M j) (Suc (Suc 0)) "
    by auto
  also have "… = matrix_sum d (λj. (adjoint (M j)) * M j) (2::nat)" by (subst ssz, auto)
  also have "… = 1_m d" using measurement_def[of d 2 M] assms by auto
  finally show ?thesis by auto
qed

text ‹Result of measurement on $\rho$ by matrix M›
definition measurement_res :: "complex mat ==> complex mat ==> complex mat" where
  "measurement_res M ρ = M * ρ * adjoint M"

lemma add_positive_le_reduce1:
  assumes dA: "A ∈ carrier_mat n n" and dB: "B ∈ carrier_mat n n" and dC: "C ∈ carrier_mat n n"
    and pB: "positive B" and le: "A + B ≤_L C"
  shows "A ≤_L C"
  unfolding lowner_le_def positive_def
proof (auto simp add: carrier_matD[OF dA] carrier_matD[OF dC] simp del: less_eq_complex_def)
  have eq: "C - (A + B) = (C - A + (-B))" using dA dB dC by auto
  have "positive (C - (A + B))" using le lowner_le_def dA dB dC by auto
  with eq have p: "positive (C - A + (-B))" by auto
  fix v :: "complex vec" assume " n = dim_vec v"
  then have dv: "v ∈ carrier_vec n" by auto
  have ge: "inner_prod v (B *_v v) ≥ 0" using pB dv dB positive_def by auto
  have "0 ≤ inner_prod v ((C - A + (-B)) *_v v) " using p positive_def dv dA dB dC by auto
  also have "… = inner_prod v ((C - A)*_v v + (-B) *_v v) "
    using dv dA dB dC add_mult_distrib_mat_vec[OF minus_carrier_mat[OF dA]] by auto
  also have "… = inner_prod v ((C - A) *_v v) + inner_prod v ((-B) *_v v)"
    apply (subst inner_prod_distrib_right)
    by (rule dv, auto simp add: mult_mat_vec_carrier[OF minus_carrier_mat[OF dA]] mult_mat_vec_carrier[OF uminus_carrier_mat[OF dB]] dv)
  also have "… = inner_prod v ((C - A) *_v v) - inner_prod v (B *_v v)" using dB dv by auto
  also have "… ≤ inner_prod v ((C - A) *_v v)" using ge by auto
  finally show "0 ≤ inner_prod v ((C - A) *_v v)".
qed

lemma add_positive_le_reduce2:
  assumes dA: "A ∈ carrier_mat n n" and dB: "B ∈ carrier_mat n n" and dC: "C ∈ carrier_mat n n"
    and pB: "positive B" and le: "B + A ≤_L C"
  shows "A ≤_L C"
  apply (subgoal_tac "B + A = A + B") using add_positive_le_reduce1[of A n B C] assms by auto

lemma measurement_le_one_mat:
  assumes "measurement d n f"
  shows "∧j. j < n ==> adjoint (f j) * f j ≤_L 1_m d"
proof -
  fix j assume j: "j < n"
  define M where "M = adjoint (f j) * f j"
  have df: "k < n ==> f k ∈ carrier_mat d d" for k using assms measurement_dim by auto
  have daf: "k < n ==> adjoint (f k) * f k ∈ carrier_mat d d" for k
  proof -
    assume "k < n"
    then have "f k ∈ carrier_mat d d" "adjoint (f k) ∈ carrier_mat d d" using df adjoint_dim by auto
    then show "adjoint (f k) * f k ∈ carrier_mat d d" by auto
  qed
  have pafj: "k < n ==> positive (adjoint (f k) * (f k)) "  for k
    apply (subst (2) adjoint_adjoint[of "f k", symmetric])
    by (metis adjoint_adjoint daf positive_if_decomp)
  define f' where "∧k. f' k = (if k = j then 0_m d d else adjoint (f k) * f k)"
  have pf': "k < n ==> positive (f' k)" for k unfolding f'_def using positive_zero pafj j by auto
  have df': "k < n ==> f' k ∈ carrier_mat d d" for k using daf j zero_carrier_mat f'_def by auto
  then have dsf': "matrix_sum d f' n ∈ carrier_mat d d" using matrix_sum_dim[of n f' d] by auto
  have psf': "positive (matrix_sum d f' n)" using matrix_sum_positive pafj df' pf' by auto
  have "M + matrix_sum d f' n = matrix_sum d (λk. adjoint (f k) * f k) n"
    using matrix_sum_remove[OF j , of "(λk. adjoint (f k) * f k)", OF daf, of f'] f'_def unfolding M_def by auto
  also have "… = 1_m d" using measurement_def assms by auto
  finally have "M + matrix_sum d f' n = 1_m d".
  moreover have "1_m d ≤_L 1_m d" using lowner_le_refl[of _ d] by auto
  ultimately have "(M + matrix_sum d f' n) ≤_L 1_m d" by auto
  then show "M ≤_L 1_m d" unfolding M_def using add_positive_le_reduce1[OF _ dsf' one_carrier_mat psf'] daf j by auto
qed

lemma pdo_close_under_measurement:
  fixes M ρ :: "complex mat"
  assumes dM: "M ∈ carrier_mat n n" and dr: "ρ ∈ carrier_mat n n"
    and pdor: "partial_density_operator ρ"
    and le: "adjoint M * M ≤_L 1_m n"
  shows "partial_density_operator (M * ρ * adjoint M)"
  unfolding partial_density_operator_def
proof
  show "positive (M * ρ * adjoint M)"
    using positive_close_under_left_right_mult_adjoint[OF dM dr] pdor partial_density_operator_def by auto
next
  have daM: "adjoint M ∈ carrier_mat n n" using dM by auto
  then have daMM: "adjoint M * M ∈ carrier_mat n n" using dM by auto
  have "trace (M * ρ * adjoint M) = trace (adjoint M * M * ρ)"
    using dM dr by (mat_assoc n)
  also have "… ≤ trace (1_m n * ρ)"
    using lowner_le_trace[where ?B = "1_m n" and ?A = "adjoint M * M", OF daMM one_carrier_mat] le dr pdor by auto
  also have "… = trace ρ" using dr by auto
  also have "… ≤ 1" using pdor partial_density_operator_def by auto
  finally show "trace (M * ρ * adjoint M) ≤ 1" by auto
qed

lemma trace_measurement:
  assumes m: "measurement d n M" and dA: "A ∈ carrier_mat d d"
  shows "trace (matrix_sum d (λk. (M k) * A * adjoint (M k)) n) = trace A"
proof -
  have dMk: "k < n ==> (M k) ∈ carrier_mat d d" for k using m unfolding measurement_def by auto
  then have daMk: "k < n ==> adjoint (M k) ∈ carrier_mat d d" for k using m adjoint_dim unfolding measurement_def by auto
  have d1: "k < n ==> M k * A * adjoint (M k) ∈ carrier_mat d d"for k using dMk daMk dA by fastforce
  then have ds1: "k < n ==> matrix_sum d (λk. M k * A * adjoint (M k)) k ∈ carrier_mat d d" for k
    using matrix_sum_dim[of k "λk. M k * A * adjoint (M k)" d] by auto
  have d2: "k < n ==> adjoint (M k) *M k * A ∈ carrier_mat d d" for k using daMk dMk dA by fastforce
  then have ds2: "k < n ==> matrix_sum d (λk. adjoint (M k) *M k * A) k ∈ carrier_mat d d" for k
    using matrix_sum_dim[of k "λk. adjoint (M k) *M k * A" d] by auto
  have daMMk: "k < n ==> adjoint (M k) * M k ∈ carrier_mat d d" for k using dMk by fastforce
  have "k ≤ n ==> trace (matrix_sum d (λk. (M k) * A * adjoint (M k)) k) = trace (matrix_sum d (λk. adjoint (M k) * (M k) * A) k)" for k
  proof (induct k)
    case 0
    then show ?case by auto
  next
    case (Suc k)
    then have k: "k < n" by auto
    have "trace (M k * A * adjoint (M k)) = trace (adjoint (M k) * M k * A)"
      using dA apply (mat_assoc d) using dMk k by auto
    then show ?case unfolding matrix_sum.simps using ds1 ds2 d1 d2 k Suc daMk dMk dA
      by (subst trace_add_linear[of _ d], auto)+
  qed
  then have "trace (matrix_sum d (λk. (M k) * A * adjoint (M k)) n) = trace (matrix_sum d (λk. adjoint (M k) * (M k) * A) n)" by auto
  also have "… = trace (matrix_sum d (λk. adjoint (M k) * (M k)) n * A)" using matrix_sum_mult_right[OF daMMk, of n id A] dA by auto
  also have "… = trace A" using m dA unfolding measurement_def by auto
  finally show ?thesis by auto
qed

lemma mat_inc_seq_positive_transform:
  assumes dfn: "∧n. f n ∈ carrier_mat d d"
    and inc: "∧n. f n ≤_L f (Suc n)"
  shows "∧n. f n - f 0 ∈ carrier_mat d d" and "∧n. (f n - f 0) ≤_L (f (Suc n) - f 0)"
proof -
  show "∧n. f n - f 0 ∈ carrier_mat d d" using dfn by fastforce
  have "f 0 ≤_L f 0" using lowner_le_refl[of "f 0" d] dfn by auto
  then show "(f n - f 0) ≤_L (f (Suc n) - f 0)" for n
    using lowner_le_minus[of "f n" d "f (Suc n)" "f 0" "f 0"] dfn inc by fastforce
qed

lemma mat_inc_seq_lub:
  assumes dfn: "∧n. f n ∈ carrier_mat d d"
    and inc: "∧n. f n ≤_L f (Suc n)"
    and ub: "∧n. f n ≤_L A"
  shows "∃B. lowner_is_lub f B ∧ limit_mat f B d"
proof -
  have dmfn0: "∧n. f n - f 0 ∈ carrier_mat d d" and incm0: "∧n. (f n - f 0) ≤_L (f (Suc n) - f 0)"
    using mat_inc_seq_positive_transform[OF dfn, of id] assms by auto
  define c where "c = 1 / (trace (A - f 0) + 1)"
  have "f 0 ≤_L A" using ub by auto
  then have dA: "A ∈ carrier_mat d d" using ub unfolding lowner_le_def using dfn[of 0] by fastforce
  then have dAmf0: "A - f 0 ∈ carrier_mat d d" using dfn[of 0] by auto
  have "positive (A - f 0)" using ub lowner_le_def by auto
  then have tgeq0: "trace (A - f 0) ≥ 0" using positive_trace dAmf0 by auto
  then have "trace (A - f 0) + 1 > 0" by (auto simp: less_eq_complex_def less_complex_def)
  then have gtc: "c > 0" unfolding c_def using complex_is_Real_iff
    by (auto simp: less_eq_complex_def less_complex_def)
  then have gtci: "(1 / c) > 0" using complex_is_Real_iff
    by (auto simp: less_eq_complex_def less_complex_def)

  have "trace (c ⋅_m (A - f 0)) = c * trace (A - f 0)"
    using trace_smult dAmf0 by auto
  also have "… = (1 / (trace (A - f 0) + 1)) * trace (A - f 0)" unfolding c_def by auto
  also have "… < 1" using tgeq0 by (simp add: complex_is_Real_iff less_eq_complex_def less_complex_def)
  finally have lt1: "trace (c ⋅_m (A - f 0)) < 1".

  have le0: "- f 0 ≤_L - f 0" using lowner_le_refl[of "- f 0" d] dfn by auto

  have dmf0: "- f 0 ∈ carrier_mat d d" using dfn by auto
  have mf0smcle: "(c ⋅_m (X - f 0)) ≤_L (c ⋅_m (Y - f 0))" if "X ≤_L Y" and "X ∈ carrier_mat d d" and "Y ∈ carrier_mat d d" for X Y
  proof -
    have "(X - f 0) ≤_L (Y - f 0)"
      using lowner_le_minus[of "X" d "Y" "f 0" "f 0"] that dfn lowner_le_refl by auto
    then show ?thesis using lowner_le_smultc[of c "(X - f 0)" "Y - f 0" d] using that dfn gtc by fastforce
  qed
  have "(c ⋅_m (f n - f 0)) ≤_L (c ⋅_m (A - f 0))" for n
    using mf0smcle ub dfn dA by auto
  then have "trace (c ⋅_m (f n - f 0)) ≤ trace (c ⋅_m (A - f 0))" for n
    using lowner_le_imp_trace_le[of "c ⋅_m (f n - f 0)" d] dmfn0 dAmf0 by auto
  then have trlt1: "trace (c ⋅_m (f n - f 0)) < 1" for n using lt1
    unfolding less_eq_complex_def less_complex_def
    by (metis add.commute add_less_cancel_right add_mono_thms_linordered_field(3))

  have "f 0 ≤_L f n" for n
  proof (induct n)
    case 0
    then show ?case using dfn lowner_le_refl by auto
  next
    case (Suc n)
    then show ?case using dfn lowner_le_trans[of "f 0" d "f n"] inc by auto
  qed
  then have "positive (f n - f 0)" for n using lowner_le_def by auto
  then have p: "positive (c ⋅_m (f n - f 0))" for n
    by (intro positive_smult, insert gtc dmfn0, auto)

  have inc': "c ⋅_m (f n - f 0) ≤_L c ⋅_m (f (Suc n) - f 0)" for n
    using incm0 lowner_le_smultc[of c "f n - f 0"] gtc dmfn0 by fastforce

  define g where "g n = c ⋅_m (f n - f 0)" for n
  then have "positive (g n)" and "trace (g n) < 1" and "(g n) ≤_L (g (Suc n))" and dgn: "(g n) ∈ carrier_mat d d" for n
    unfolding g_def using p trlt1 inc' dmfn0 by auto
  then have ms: "matrix_seq d g" unfolding matrix_seq_def partial_density_operator_def
    by (simp add: less_eq_complex_def less_complex_def dual_order.strict_iff_not)
  then have uniM: "∃!M. matrix_seq.lowner_is_lub g M" using matrix_seq.lowner_lub_unique by auto
  then obtain M where M: "matrix_seq.lowner_is_lub g M" by auto
  then have leg: "g n ≤_L M" and lubg: "∧M'. (∀n. g n ≤_L M') ⟶ M ≤_L M'" for n
    unfolding matrix_seq.lowner_is_lub_def[OF ms] by auto
  have "M = matrix_seq.lowner_lub g"
    using matrix_seq.lowner_lub_def[OF ms] M uniM theI_unique[of "matrix_seq.lowner_is_lub g"] by auto
  then have limg: "limit_mat g M d" using M matrix_seq.lowner_lub_is_limit[OF ms] by auto
  then have dM: "M ∈ carrier_mat d d" unfolding limit_mat_def by auto

  define B where "B = f 0 + (1 / c) ⋅_m M"
  have eqinv: "f 0 + (1 / c) ⋅_m (c ⋅_m (X - f 0)) = X" if "X ∈ carrier_mat d d" for X
  proof -
    have "f 0 + (1 / c) ⋅_m (c ⋅_m (X - f 0)) = f 0 + (1 / c * c) ⋅_m (X - f 0)"
      apply (subgoal_tac "(1 / c) ⋅_m (c ⋅_m (X - f 0)) = (1 / c * c) ⋅_m (X - f 0)", simp)
      using smult_smult_mat dfn that by auto
    also have "… = f 0 + 1 ⋅_m (X - f 0)" using gtc by auto
    also have "… = f 0 + (X - f 0)" by auto
    also have "… = (- f 0) + f 0 + X" apply (mat_assoc d) using that dfn by auto
    also have "… = 0_m d d + X" using dfn uminus_l_inv_mat[of "f 0" d d] by fastforce
    also have "… = X" using that by auto
    finally show ?thesis by auto
  qed
  have "limit_mat (λn. (1 / c) ⋅_m g n) ((1 / c) ⋅_m M) d" using limit_mat_scale[OF limg] gtci by auto
  then have "limit_mat (λn. f 0 + (1 / c) ⋅_m g n) (f 0 + (1 / c) ⋅_m M ) d"
    using mat_add_limit[of "f 0"] limg dfn unfolding mat_add_seq_def by auto
  then have limf: "limit_mat f B d" using eqinv[OF dfn] unfolding B_def g_def by auto

  have f0acmcile: "(f 0 + (1 / c) ⋅_m X) ≤_L (f 0 + (1 / c) ⋅_m Y )" if "X ≤_L Y" and "X ∈ carrier_mat d d" and "Y ∈ carrier_mat d d" for X Y
  proof -
    have "((1 / c) ⋅_m X) ≤_L ((1 / c) ⋅_m Y)"
      using lowner_le_smultc[of "1/c"] that gtci by fastforce
    then show "(f 0 + (1 / c) ⋅_m X) ≤_L (f 0 + (1 / c) ⋅_m Y)"
      using lowner_le_add[of _ d _ "(1 / c) ⋅_m X" "(1 / c) ⋅_m Y"]
        that gtci dfn lowner_le_refl[of "f 0", OF dfn] by fastforce
  qed

  have "(f 0 + (1 / c) ⋅_m g n) ≤_L (f 0 + (1 / c) ⋅_m M )" for n
    using f0acmcile[OF leg dgn dM] by auto
  then have lubf: "f n ≤_L B" for n using eqinv[OF dfn] g_def B_def by auto

  {
    fix B' assume asm: "∀n. f n ≤_L B'"
    then have "f 0 ≤_L B'" by auto
    then have dB': "B' ∈ carrier_mat d d" unfolding lowner_le_def using dfn[of 0] by auto
    have "f n ≤_L B'" for n using asm by auto
    then have "(c ⋅_m (f n - f 0)) ≤_L (c ⋅_m (B' - f 0))" for n
      using mf0smcle[of "f n" B'] dfn dB' by auto
    then have "g n ≤_L (c ⋅_m (B' - f 0))" for n using g_def by auto
    then have "M ≤_L  (c ⋅_m (B' - f 0))" using lubg by auto
    then have "(f 0 + (1 / c) ⋅_m M) ≤_L (f 0 + (1 / c) ⋅_m (c ⋅_m (B' - f 0)))"
      using f0acmcile[of "M" "(c ⋅_m (B' - f 0))", OF _ dM] using dB' dfn by fastforce
    then have "B ≤_L B'" unfolding B_def using eqinv[OF dB'] by auto
  }
  with limf lubf have "((∀n. f n ≤_L B) ∧ (∀M'. (∀n. f n ≤_L M') ⟶ B ≤_L M')) ∧ limit_mat f B d" by auto
  then show ?thesis unfolding lowner_is_lub_def by auto
qed

end