[STATEMENT]
lemma lowner_lub_form:
  "lowner_is_lub (mat dim dim (\<lambda> (i, j). (lim (\<lambda> n. (f n) $$ (i, j)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.lowner_is_lub (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.lowner_is_lub (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))
[PROOF STEP]
from inc_partial_density_operator_converge
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?i \<in> {0..<dim}; ?j \<in> {0..<dim}\<rbrakk> \<Longrightarrow> convergent (\<lambda>n. f n $$ (?i, ?j))
[PROOF STEP]
have conf: "\<forall> i \<in> {0 ..<dim}.  \<forall> j \<in> {0 ..<dim}. convergent (\<lambda> n. f n $$ (i, j))"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i \<in> {0..<dim}; ?j \<in> {0..<dim}\<rbrakk> \<Longrightarrow> convergent (\<lambda>n. f n $$ (?i, ?j))

goal (1 subgoal):
 1. \<forall>i\<in>{0..<dim}. \<forall>j\<in>{0..<dim}. convergent (\<lambda>n. f n $$ (i, j))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>{0..<dim}. \<forall>j\<in>{0..<dim}. convergent (\<lambda>n. f n $$ (i, j))

goal (1 subgoal):
 1. local.lowner_is_lub (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))
[PROOF STEP]
let ?A = "mat dim dim (\<lambda> (i, j). (lim (\<lambda> n. (f n) $$ (i, j))))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.lowner_is_lub (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))
[PROOF STEP]
have dim_A: "?A \<in> carrier_mat dim dim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<in> carrier_mat dim dim
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<in> carrier_mat dim dim

goal (1 subgoal):
 1. local.lowner_is_lub (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))
[PROOF STEP]
have lim_A: "(\<lambda>n. f n $$ (i, j)) \<longlonglongrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (i, j)"
    if i: "i < dim" and j: "j < dim" for i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. f n $$ (i, j)) \<longlonglongrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (i, j)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>n. f n $$ (i, j)) \<longlonglongrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (i, j)
[PROOF STEP]
from i j
[PROOF STATE]
proof (chain)
picking this:
i < dim
j < dim
[PROOF STEP]
have ij: "mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (i, j) = lim (\<lambda>n. f n $$ (i, j))"
[PROOF STATE]
proof (prove)
using this:
i < dim
j < dim

goal (1 subgoal):
 1. mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (i, j) = lim (\<lambda>n. f n $$ (i, j))
[PROOF STEP]
by (metis case_prod_conv index_mat(1))
[PROOF STATE]
proof (state)
this:
mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (i, j) = lim (\<lambda>n. f n $$ (i, j))

goal (1 subgoal):
 1. (\<lambda>n. f n $$ (i, j)) \<longlonglongrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (i, j)
[PROOF STEP]
have "convergent (\<lambda>n. f n $$ (i, j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convergent (\<lambda>n. f n $$ (i, j))
[PROOF STEP]
using conf i j
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>{0..<dim}. \<forall>j\<in>{0..<dim}. convergent (\<lambda>n. f n $$ (i, j))
i < dim
j < dim

goal (1 subgoal):
 1. convergent (\<lambda>n. f n $$ (i, j))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
convergent (\<lambda>n. f n $$ (i, j))

goal (1 subgoal):
 1. (\<lambda>n. f n $$ (i, j)) \<longlonglongrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (i, j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
convergent (\<lambda>n. f n $$ (i, j))
[PROOF STEP]
have "(\<lambda>n. f n $$ (i, j))  \<longlonglongrightarrow> lim (\<lambda>n. f n $$ (i, j)) "
[PROOF STATE]
proof (prove)
using this:
convergent (\<lambda>n. f n $$ (i, j))

goal (1 subgoal):
 1. (\<lambda>n. f n $$ (i, j)) \<longlonglongrightarrow> lim (\<lambda>n. f n $$ (i, j))
[PROOF STEP]
using convergent_LIMSEQ_iff
[PROOF STATE]
proof (prove)
using this:
convergent (\<lambda>n. f n $$ (i, j))
convergent ?X = ?X \<longlonglongrightarrow> lim ?X

goal (1 subgoal):
 1. (\<lambda>n. f n $$ (i, j)) \<longlonglongrightarrow> lim (\<lambda>n. f n $$ (i, j))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. f n $$ (i, j)) \<longlonglongrightarrow> lim (\<lambda>n. f n $$ (i, j))

goal (1 subgoal):
 1. (\<lambda>n. f n $$ (i, j)) \<longlonglongrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (i, j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. f n $$ (i, j)) \<longlonglongrightarrow> lim (\<lambda>n. f n $$ (i, j))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. f n $$ (i, j)) \<longlonglongrightarrow> lim (\<lambda>n. f n $$ (i, j))

goal (1 subgoal):
 1. (\<lambda>n. f n $$ (i, j)) \<longlonglongrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (i, j)
[PROOF STEP]
using ij
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. f n $$ (i, j)) \<longlonglongrightarrow> lim (\<lambda>n. f n $$ (i, j))
mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (i, j) = lim (\<lambda>n. f n $$ (i, j))

goal (1 subgoal):
 1. (\<lambda>n. f n $$ (i, j)) \<longlonglongrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (i, j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. f n $$ (i, j)) \<longlonglongrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (i, j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i < dim; ?j < dim\<rbrakk> \<Longrightarrow> (\<lambda>n. f n $$ (?i, ?j)) \<longlonglongrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (?i, ?j)

goal (1 subgoal):
 1. local.lowner_is_lub (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))
[PROOF STEP]
from dim dim_A lim_A
[PROOF STATE]
proof (chain)
picking this:
f ?n \<in> carrier_mat dim dim
mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<in> carrier_mat dim dim
\<lbrakk>?i < dim; ?j < dim\<rbrakk> \<Longrightarrow> (\<lambda>n. f n $$ (?i, ?j)) \<longlonglongrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (?i, ?j)
[PROOF STEP]
have lim_mat_A: "limit_mat f ?A dim"
[PROOF STATE]
proof (prove)
using this:
f ?n \<in> carrier_mat dim dim
mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<in> carrier_mat dim dim
\<lbrakk>?i < dim; ?j < dim\<rbrakk> \<Longrightarrow> (\<lambda>n. f n $$ (?i, ?j)) \<longlonglongrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (?i, ?j)

goal (1 subgoal):
 1. limit_mat f (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) dim
[PROOF STEP]
unfolding limit_mat_def
[PROOF STATE]
proof (prove)
using this:
f ?n \<in> carrier_mat dim dim
mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<in> carrier_mat dim dim
\<lbrakk>?i < dim; ?j < dim\<rbrakk> \<Longrightarrow> (\<lambda>n. f n $$ (?i, ?j)) \<longlonglongrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (?i, ?j)

goal (1 subgoal):
 1. \<forall>n. f n \<in> carrier_mat dim dim \<and> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<in> carrier_mat dim dim \<and> (\<forall>i<dim. \<forall>j<dim. (\<lambda>n. f n $$ (i, j)) \<longlonglongrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (i, j))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
limit_mat f (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) dim

goal (1 subgoal):
 1. local.lowner_is_lub (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))
[PROOF STEP]
have is_ub: "f n \<le>\<^sub>L ?A" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
[PROOF STEP]
have "\<forall> m \<ge> n. positive (f m - f n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m\<ge>n. positive (f m - f n)
[PROOF STEP]
using lowner_le_transitive
[PROOF STATE]
proof (prove)
using this:
?m \<le> ?n \<Longrightarrow> positive (f ?n - f ?m)

goal (1 subgoal):
 1. \<forall>m\<ge>n. positive (f m - f n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>m\<ge>n. positive (f m - f n)

goal (1 subgoal):
 1. f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>m\<ge>n. positive (f m - f n)
[PROOF STEP]
have le: "\<forall> m \<ge> n. f n \<le>\<^sub>L f m "
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<ge>n. positive (f m - f n)

goal (1 subgoal):
 1. \<forall>m\<ge>n. f n \<le>\<^sub>L f m
[PROOF STEP]
unfolding lowner_le_def
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<ge>n. positive (f m - f n)

goal (1 subgoal):
 1. \<forall>m\<ge>n. dim_row (f n) = dim_row (f m) \<and> dim_col (f n) = dim_col (f m) \<and> positive (f m - f n)
[PROOF STEP]
using dim
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<ge>n. positive (f m - f n)
f ?n \<in> carrier_mat dim dim

goal (1 subgoal):
 1. \<forall>m\<ge>n. dim_row (f n) = dim_row (f m) \<and> dim_col (f n) = dim_col (f m) \<and> positive (f m - f n)
[PROOF STEP]
by (metis carrier_matD(1) carrier_matD(2))
[PROOF STATE]
proof (state)
this:
\<forall>m\<ge>n. f n \<le>\<^sub>L f m

goal (1 subgoal):
 1. f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
[PROOF STEP]
have dimn: "f n \<in> carrier_mat dim dim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f n \<in> carrier_mat dim dim
[PROOF STEP]
using dim
[PROOF STATE]
proof (prove)
using this:
f ?n \<in> carrier_mat dim dim

goal (1 subgoal):
 1. f n \<in> carrier_mat dim dim
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f n \<in> carrier_mat dim dim

goal (1 subgoal):
 1. f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f n \<in> carrier_mat dim dim
[PROOF STEP]
have limAf: "limit_mat (mat_seq_minus f (f n)) (?A - f n) dim"
[PROOF STATE]
proof (prove)
using this:
f n \<in> carrier_mat dim dim

goal (1 subgoal):
 1. limit_mat (mat_seq_minus f (f n)) (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) - f n) dim
[PROOF STEP]
using minus_mat_limit lim_mat_A
[PROOF STATE]
proof (prove)
using this:
f n \<in> carrier_mat dim dim
\<lbrakk>?B \<in> carrier_mat ?m ?m; limit_mat ?X ?A ?m\<rbrakk> \<Longrightarrow> limit_mat (mat_seq_minus ?X ?B) (?A - ?B) ?m
limit_mat f (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) dim

goal (1 subgoal):
 1. limit_mat (mat_seq_minus f (f n)) (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) - f n) dim
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
limit_mat (mat_seq_minus f (f n)) (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) - f n) dim

goal (1 subgoal):
 1. f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
[PROOF STEP]
have " \<forall>m\<ge>n. positive (f m - f n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m\<ge>n. positive (f m - f n)
[PROOF STEP]
using lowner_le_transitive
[PROOF STATE]
proof (prove)
using this:
?m \<le> ?n \<Longrightarrow> positive (f ?n - f ?m)

goal (1 subgoal):
 1. \<forall>m\<ge>n. positive (f m - f n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>m\<ge>n. positive (f m - f n)

goal (1 subgoal):
 1. f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>m\<ge>n. positive (f m - f n)
[PROOF STEP]
have "\<exists>k. \<forall>m\<ge>k. positive (f m - f n)"
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<ge>n. positive (f m - f n)

goal (1 subgoal):
 1. \<exists>k. \<forall>m\<ge>k. positive (f m - f n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k. \<forall>m\<ge>k. positive (f m - f n)

goal (1 subgoal):
 1. f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>k. \<forall>m\<ge>k. positive (f m - f n)
[PROOF STEP]
have posAf: "\<exists> k. \<forall> m \<ge> k. positive ((mat_seq_minus f (f n)) m)"
[PROOF STATE]
proof (prove)
using this:
\<exists>k. \<forall>m\<ge>k. positive (f m - f n)

goal (1 subgoal):
 1. \<exists>k. \<forall>m\<ge>k. positive (mat_seq_minus f (f n) m)
[PROOF STEP]
unfolding mat_seq_minus_def
[PROOF STATE]
proof (prove)
using this:
\<exists>k. \<forall>m\<ge>k. positive (f m - f n)

goal (1 subgoal):
 1. \<exists>k. \<forall>m\<ge>k. positive (f m - f n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k. \<forall>m\<ge>k. positive (mat_seq_minus f (f n) m)

goal (1 subgoal):
 1. f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
[PROOF STEP]
from limAf posAf
[PROOF STATE]
proof (chain)
picking this:
limit_mat (mat_seq_minus f (f n)) (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) - f n) dim
\<exists>k. \<forall>m\<ge>k. positive (mat_seq_minus f (f n) m)
[PROOF STEP]
have "positive (?A - f n)"
[PROOF STATE]
proof (prove)
using this:
limit_mat (mat_seq_minus f (f n)) (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) - f n) dim
\<exists>k. \<forall>m\<ge>k. positive (mat_seq_minus f (f n) m)

goal (1 subgoal):
 1. positive (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) - f n)
[PROOF STEP]
using pos_mat_lim_is_pos_aux
[PROOF STATE]
proof (prove)
using this:
limit_mat (mat_seq_minus f (f n)) (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) - f n) dim
\<exists>k. \<forall>m\<ge>k. positive (mat_seq_minus f (f n) m)
\<lbrakk>limit_mat ?X ?A ?m; \<exists>k. \<forall>n\<ge>k. positive (?X n)\<rbrakk> \<Longrightarrow> positive ?A

goal (1 subgoal):
 1. positive (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) - f n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) - f n)

goal (1 subgoal):
 1. f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
positive (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) - f n)
[PROOF STEP]
have "f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))"
[PROOF STATE]
proof (prove)
using this:
positive (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) - f n)

goal (1 subgoal):
 1. f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
[PROOF STEP]
unfolding lowner_le_def
[PROOF STATE]
proof (prove)
using this:
positive (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) - f n)

goal (1 subgoal):
 1. dim_row (f n) = dim_row (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) \<and> dim_col (f n) = dim_col (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) \<and> positive (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) - f n)
[PROOF STEP]
using dim
[PROOF STATE]
proof (prove)
using this:
positive (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) - f n)
f ?n \<in> carrier_mat dim dim

goal (1 subgoal):
 1. dim_row (f n) = dim_row (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) \<and> dim_col (f n) = dim_col (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) \<and> positive (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) - f n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))

goal (1 subgoal):
 1. f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))

goal (1 subgoal):
 1. f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f ?n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))

goal (1 subgoal):
 1. local.lowner_is_lub (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))
[PROOF STEP]
have is_lub: "?A \<le>\<^sub>L M'" if ub: "\<forall>n. f n \<le>\<^sub>L M'" for M'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L M'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L M'
[PROOF STEP]
have dim_M: "M' \<in> carrier_mat dim dim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M' \<in> carrier_mat dim dim
[PROOF STEP]
using ub
[PROOF STATE]
proof (prove)
using this:
\<forall>n. f n \<le>\<^sub>L M'

goal (1 subgoal):
 1. M' \<in> carrier_mat dim dim
[PROOF STEP]
unfolding lowner_le_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n. dim_row (f n) = dim_row M' \<and> dim_col (f n) = dim_col M' \<and> positive (M' - f n)

goal (1 subgoal):
 1. M' \<in> carrier_mat dim dim
[PROOF STEP]
using dim
[PROOF STATE]
proof (prove)
using this:
\<forall>n. dim_row (f n) = dim_row M' \<and> dim_col (f n) = dim_col M' \<and> positive (M' - f n)
f ?n \<in> carrier_mat dim dim

goal (1 subgoal):
 1. M' \<in> carrier_mat dim dim
[PROOF STEP]
by (metis carrier_matD(1) carrier_matD(2) carrier_mat_triv)
[PROOF STATE]
proof (state)
this:
M' \<in> carrier_mat dim dim

goal (1 subgoal):
 1. mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L M'
[PROOF STEP]
from ub
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. f n \<le>\<^sub>L M'
[PROOF STEP]
have posAf: "\<forall> n. positive (minus_mat_seq M' f n)"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. f n \<le>\<^sub>L M'

goal (1 subgoal):
 1. \<forall>n. positive (minus_mat_seq M' f n)
[PROOF STEP]
unfolding minus_mat_seq_def lowner_le_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n. dim_row (f n) = dim_row M' \<and> dim_col (f n) = dim_col M' \<and> positive (M' - f n)

goal (1 subgoal):
 1. \<forall>n. positive (M' - f n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n. positive (minus_mat_seq M' f n)

goal (1 subgoal):
 1. mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L M'
[PROOF STEP]
have limAf: "limit_mat (minus_mat_seq M' f) (M' - ?A) dim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. limit_mat (minus_mat_seq M' f) (M' - mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) dim
[PROOF STEP]
using mat_minus_limit dim_A lim_mat_A
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?A \<in> carrier_mat ?m ?m; limit_mat ?X ?A ?m\<rbrakk> \<Longrightarrow> limit_mat (minus_mat_seq ?B ?X) (?B - ?A) ?m
mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<in> carrier_mat dim dim
limit_mat f (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) dim

goal (1 subgoal):
 1. limit_mat (minus_mat_seq M' f) (M' - mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) dim
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
limit_mat (minus_mat_seq M' f) (M' - mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) dim

goal (1 subgoal):
 1. mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L M'
[PROOF STEP]
from posAf limAf
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. positive (minus_mat_seq M' f n)
limit_mat (minus_mat_seq M' f) (M' - mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) dim
[PROOF STEP]
have  "positive (M' - ?A)"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. positive (minus_mat_seq M' f n)
limit_mat (minus_mat_seq M' f) (M' - mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) dim

goal (1 subgoal):
 1. positive (M' - mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))
[PROOF STEP]
using pos_mat_lim_is_pos_aux
[PROOF STATE]
proof (prove)
using this:
\<forall>n. positive (minus_mat_seq M' f n)
limit_mat (minus_mat_seq M' f) (M' - mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) dim
\<lbrakk>limit_mat ?X ?A ?m; \<exists>k. \<forall>n\<ge>k. positive (?X n)\<rbrakk> \<Longrightarrow> positive ?A

goal (1 subgoal):
 1. positive (M' - mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive (M' - mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))

goal (1 subgoal):
 1. mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L M'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
positive (M' - mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))
[PROOF STEP]
have "?A \<le>\<^sub>L M'"
[PROOF STATE]
proof (prove)
using this:
positive (M' - mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))

goal (1 subgoal):
 1. mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L M'
[PROOF STEP]
unfolding lowner_le_def
[PROOF STATE]
proof (prove)
using this:
positive (M' - mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))

goal (1 subgoal):
 1. dim_row (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) = dim_row M' \<and> dim_col (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) = dim_col M' \<and> positive (M' - mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))
[PROOF STEP]
using dim dim_A dim_M
[PROOF STATE]
proof (prove)
using this:
positive (M' - mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))
f ?n \<in> carrier_mat dim dim
mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<in> carrier_mat dim dim
M' \<in> carrier_mat dim dim

goal (1 subgoal):
 1. dim_row (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) = dim_row M' \<and> dim_col (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) = dim_col M' \<and> positive (M' - mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L M'

goal (1 subgoal):
 1. mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L M'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L M'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L M'

goal (1 subgoal):
 1. mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L M'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L M'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n. f n \<le>\<^sub>L ?M' \<Longrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L ?M'

goal (1 subgoal):
 1. local.lowner_is_lub (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))
[PROOF STEP]
from is_ub is_lub
[PROOF STATE]
proof (chain)
picking this:
f ?n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
\<forall>n. f n \<le>\<^sub>L ?M' \<Longrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L ?M'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f ?n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
\<forall>n. f n \<le>\<^sub>L ?M' \<Longrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L ?M'

goal (1 subgoal):
 1. local.lowner_is_lub (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))
[PROOF STEP]
unfolding lowner_is_lub_def
[PROOF STATE]
proof (prove)
using this:
f ?n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
\<forall>n. f n \<le>\<^sub>L ?M' \<Longrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L ?M'

goal (1 subgoal):
 1. (\<forall>n. f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) \<and> (\<forall>M'. (\<forall>n. f n \<le>\<^sub>L M') \<longrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L M')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.lowner_is_lub (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))

goal:
No subgoals!
[PROOF STEP]
qed