[STATEMENT]
lemma nonzero_Ax: assumes x: "x \<in> X"
  shows "A *v x \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *v x \<noteq> 0
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A *v x = 0 \<Longrightarrow> False
[PROOF STEP]
assume 0: "A *v x = 0"
[PROOF STATE]
proof (state)
this:
A *v x = 0

goal (1 subgoal):
 1. A *v x = 0 \<Longrightarrow> False
[PROOF STEP]
from x[unfolded X_def]
[PROOF STATE]
proof (chain)
picking this:
x \<in> {x. le_vec 0 x \<and> x \<noteq> 0}
[PROOF STEP]
have x: "le_vec 0 x" "x \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
x \<in> {x. le_vec 0 x \<and> x \<noteq> 0}

goal (1 subgoal):
 1. le_vec 0 x &&& x \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
le_vec 0 x
x \<noteq> 0

goal (1 subgoal):
 1. A *v x = 0 \<Longrightarrow> False
[PROOF STEP]
from x(2)
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> 0
[PROOF STEP]
obtain j where xj: "x $ j \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0

goal (1 subgoal):
 1. (\<And>j. x $h j \<noteq> 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis vec_eq_iff zero_index)
[PROOF STATE]
proof (state)
this:
x $h j \<noteq> 0

goal (1 subgoal):
 1. A *v x = 0 \<Longrightarrow> False
[PROOF STEP]
from A_nonzero_fixed_j[of j]
[PROOF STATE]
proof (chain)
picking this:
\<exists>i. A $h i $h j \<noteq> 0
[PROOF STEP]
obtain i where Aij: "A $ i $ j \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>i. A $h i $h j \<noteq> 0

goal (1 subgoal):
 1. (\<And>i. A $h i $h j \<noteq> 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A $h i $h j \<noteq> 0

goal (1 subgoal):
 1. A *v x = 0 \<Longrightarrow> False
[PROOF STEP]
from arg_cong[OF 0, of "\<lambda> v. v $ i", unfolded matrix_vector_mult_def]
[PROOF STATE]
proof (chain)
picking this:
(\<chi>i. \<Sum>j\<in>UNIV. A $h i $h j * x $h j) $h i = 0 $h i
[PROOF STEP]
have "0 = (\<Sum> k \<in> UNIV. A $h i $h k * x $h k)"
[PROOF STATE]
proof (prove)
using this:
(\<chi>i. \<Sum>j\<in>UNIV. A $h i $h j * x $h j) $h i = 0 $h i

goal (1 subgoal):
 1. 0 = (\<Sum>k\<in>UNIV. A $h i $h k * x $h k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 = (\<Sum>k\<in>UNIV. A $h i $h k * x $h k)

goal (1 subgoal):
 1. A *v x = 0 \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 = (\<Sum>k\<in>UNIV. A $h i $h k * x $h k)

goal (1 subgoal):
 1. A *v x = 0 \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = A $h i $h j * x $h j + (\<Sum> k \<in> UNIV - {j}. A $h i $h k * x $h k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k\<in>UNIV. A $h i $h k * x $h k) = A $h i $h j * x $h j + (\<Sum>k\<in>UNIV - {j}. A $h i $h k * x $h k)
[PROOF STEP]
by (subst sum.remove[of _ j], auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>k\<in>UNIV. A $h i $h k * x $h k) = A $h i $h j * x $h j + (\<Sum>k\<in>UNIV - {j}. A $h i $h k * x $h k)

goal (1 subgoal):
 1. A *v x = 0 \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>k\<in>UNIV. A $h i $h k * x $h k) = A $h i $h j * x $h j + (\<Sum>k\<in>UNIV - {j}. A $h i $h k * x $h k)

goal (1 subgoal):
 1. A *v x = 0 \<Longrightarrow> False
[PROOF STEP]
have "\<dots> > 0 + 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 + 0 < A $h i $h j * x $h j + (\<Sum>k\<in>UNIV - {j}. A $h i $h k * x $h k)
[PROOF STEP]
by (rule add_less_le_mono, insert nonneg[of i] Aij x(1) xj,
    auto intro!: sum_nonneg mult_pos_pos simp: dual_order.not_eq_order_implies_strict)
[PROOF STATE]
proof (state)
this:
0 + 0 < A $h i $h j * x $h j + (\<Sum>k\<in>UNIV - {j}. A $h i $h k * x $h k)

goal (1 subgoal):
 1. A *v x = 0 \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
0 + 0 < 0
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
0 + 0 < 0

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma r_witness: assumes x: "x \<in> X"
  shows "\<exists> j. x $ j > 0 \<and> r x = (A *v x) $ j / x $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j. 0 < x $h j \<and> r x = (A *v x) $h j / x $h j
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>j. 0 < x $h j \<and> r x = (A *v x) $h j / x $h j
[PROOF STEP]
from x[unfolded X_def]
[PROOF STATE]
proof (chain)
picking this:
x \<in> {x. le_vec 0 x \<and> x \<noteq> 0}
[PROOF STEP]
have x: "le_vec 0 x" "x \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
x \<in> {x. le_vec 0 x \<and> x \<noteq> 0}

goal (1 subgoal):
 1. le_vec 0 x &&& x \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
le_vec 0 x
x \<noteq> 0

goal (1 subgoal):
 1. \<exists>j. 0 < x $h j \<and> r x = (A *v x) $h j / x $h j
[PROOF STEP]
let ?A = "{ (A *v x) $ j / x $ j | j. x $ j \<noteq> 0 }"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>j. 0 < x $h j \<and> r x = (A *v x) $h j / x $h j
[PROOF STEP]
from x(2)
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> 0
[PROOF STEP]
obtain j where "x $ j \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0

goal (1 subgoal):
 1. (\<And>j. x $h j \<noteq> 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis vec_eq_iff zero_index)
[PROOF STATE]
proof (state)
this:
x $h j \<noteq> 0

goal (1 subgoal):
 1. \<exists>j. 0 < x $h j \<and> r x = (A *v x) $h j / x $h j
[PROOF STEP]
hence empty: "?A \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
x $h j \<noteq> 0

goal (1 subgoal):
 1. {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0} \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(A *v x) $h j / x $h j |j. x $h j \<noteq> 0} \<noteq> {}

goal (1 subgoal):
 1. \<exists>j. 0 < x $h j \<and> r x = (A *v x) $h j / x $h j
[PROOF STEP]
from Min_in[OF _ this, folded r_def]
[PROOF STATE]
proof (chain)
picking this:
finite {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0} \<Longrightarrow> r x \<in> {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0}
[PROOF STEP]
obtain j where "x $ j \<noteq> 0" and rx: "r x = (A *v x) $ j / x $ j"
[PROOF STATE]
proof (prove)
using this:
finite {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0} \<Longrightarrow> r x \<in> {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0}

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>x $h j \<noteq> 0; r x = (A *v x) $h j / x $h j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x $h j \<noteq> 0
r x = (A *v x) $h j / x $h j

goal (1 subgoal):
 1. \<exists>j. 0 < x $h j \<and> r x = (A *v x) $h j / x $h j
[PROOF STEP]
with x
[PROOF STATE]
proof (chain)
picking this:
le_vec 0 x
x \<noteq> 0
x $h j \<noteq> 0
r x = (A *v x) $h j / x $h j
[PROOF STEP]
have "x $ j > 0"
[PROOF STATE]
proof (prove)
using this:
le_vec 0 x
x \<noteq> 0
x $h j \<noteq> 0
r x = (A *v x) $h j / x $h j

goal (1 subgoal):
 1. 0 < x $h j
[PROOF STEP]
by (auto simp: dual_order.not_eq_order_implies_strict)
[PROOF STATE]
proof (state)
this:
0 < x $h j

goal (1 subgoal):
 1. \<exists>j. 0 < x $h j \<and> r x = (A *v x) $h j / x $h j
[PROOF STEP]
with rx
[PROOF STATE]
proof (chain)
picking this:
r x = (A *v x) $h j / x $h j
0 < x $h j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r x = (A *v x) $h j / x $h j
0 < x $h j

goal (1 subgoal):
 1. \<exists>j. 0 < x $h j \<and> r x = (A *v x) $h j / x $h j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>j. 0 < x $h j \<and> r x = (A *v x) $h j / x $h j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rx_nonneg: assumes x: "x \<in> X"
  shows "r x \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> r x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 \<le> r x
[PROOF STEP]
from x[unfolded X_def]
[PROOF STATE]
proof (chain)
picking this:
x \<in> {x. le_vec 0 x \<and> x \<noteq> 0}
[PROOF STEP]
have x: "le_vec 0 x" "x \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
x \<in> {x. le_vec 0 x \<and> x \<noteq> 0}

goal (1 subgoal):
 1. le_vec 0 x &&& x \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
le_vec 0 x
x \<noteq> 0

goal (1 subgoal):
 1. 0 \<le> r x
[PROOF STEP]
let ?A = "{ (A *v x) $ j / x $ j | j. x $ j \<noteq> 0 }"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 \<le> r x
[PROOF STEP]
from r_witness[OF \<open>x \<in> X\<close>]
[PROOF STATE]
proof (chain)
picking this:
\<exists>j. 0 < x $h j \<and> r x = (A *v x) $h j / x $h j
[PROOF STEP]
have empty: "?A \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
\<exists>j. 0 < x $h j \<and> r x = (A *v x) $h j / x $h j

goal (1 subgoal):
 1. {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0} \<noteq> {}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
{(A *v x) $h j / x $h j |j. x $h j \<noteq> 0} \<noteq> {}

goal (1 subgoal):
 1. 0 \<le> r x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> r x
[PROOF STEP]
unfolding r_def X_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> Min {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0}
[PROOF STEP]
proof (subst Min_ge_iff, force, use empty in force, intro ballI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0} \<Longrightarrow> 0 \<le> xa
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0} \<Longrightarrow> 0 \<le> xa
[PROOF STEP]
assume "y \<in> ?A"
[PROOF STATE]
proof (state)
this:
y \<in> {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0}

goal (1 subgoal):
 1. \<And>xa. xa \<in> {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0} \<Longrightarrow> 0 \<le> xa
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0}
[PROOF STEP]
obtain j where "y = (A *v x) $ j / x $ j" and "x $ j \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
y \<in> {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0}

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>y = (A *v x) $h j / x $h j; x $h j \<noteq> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y = (A *v x) $h j / x $h j
x $h j \<noteq> 0

goal (1 subgoal):
 1. \<And>xa. xa \<in> {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0} \<Longrightarrow> 0 \<le> xa
[PROOF STEP]
from nonneg_Ax[OF \<open>x \<in> X\<close>] this x
[PROOF STATE]
proof (chain)
picking this:
le_vec 0 (A *v x)
y = (A *v x) $h j / x $h j
x $h j \<noteq> 0
le_vec 0 x
x \<noteq> 0
[PROOF STEP]
show "0 \<le> y"
[PROOF STATE]
proof (prove)
using this:
le_vec 0 (A *v x)
y = (A *v x) $h j / x $h j
x $h j \<noteq> 0
le_vec 0 x
x \<noteq> 0

goal (1 subgoal):
 1. 0 \<le> y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 \<le> r x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rx_pos: assumes x: "lt_vec 0 x"
  shows "r x > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < r x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < r x
[PROOF STEP]
from Ax_pos[OF x]
[PROOF STATE]
proof (chain)
picking this:
lt_vec 0 (A *v x)
[PROOF STEP]
have lt: "lt_vec 0 (A *v x)"
[PROOF STATE]
proof (prove)
using this:
lt_vec 0 (A *v x)

goal (1 subgoal):
 1. lt_vec 0 (A *v x)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
lt_vec 0 (A *v x)

goal (1 subgoal):
 1. 0 < r x
[PROOF STEP]
from x
[PROOF STATE]
proof (chain)
picking this:
lt_vec 0 x
[PROOF STEP]
have x': "x \<in> X"
[PROOF STATE]
proof (prove)
using this:
lt_vec 0 x

goal (1 subgoal):
 1. x \<in> X
[PROOF STEP]
unfolding X_def order.strict_iff_order
[PROOF STATE]
proof (prove)
using this:
\<forall>i. 0 $h i \<le> x $h i \<and> 0 $h i \<noteq> x $h i

goal (1 subgoal):
 1. x \<in> {x. le_vec 0 x \<and> x \<noteq> 0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> X

goal (1 subgoal):
 1. 0 < r x
[PROOF STEP]
let ?A = "{ (A *v x) $ j / x $ j | j. x $ j \<noteq> 0 }"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < r x
[PROOF STEP]
from r_witness[OF \<open>x \<in> X\<close>]
[PROOF STATE]
proof (chain)
picking this:
\<exists>j. 0 < x $h j \<and> r x = (A *v x) $h j / x $h j
[PROOF STEP]
have empty: "?A \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
\<exists>j. 0 < x $h j \<and> r x = (A *v x) $h j / x $h j

goal (1 subgoal):
 1. {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0} \<noteq> {}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
{(A *v x) $h j / x $h j |j. x $h j \<noteq> 0} \<noteq> {}

goal (1 subgoal):
 1. 0 < r x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < r x
[PROOF STEP]
unfolding r_def X_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < Min {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0}
[PROOF STEP]
proof (subst Min_gr_iff, force, use empty in force, intro ballI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0} \<Longrightarrow> 0 < xa
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0} \<Longrightarrow> 0 < xa
[PROOF STEP]
assume "y \<in> ?A"
[PROOF STATE]
proof (state)
this:
y \<in> {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0}

goal (1 subgoal):
 1. \<And>xa. xa \<in> {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0} \<Longrightarrow> 0 < xa
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0}
[PROOF STEP]
obtain j where "y = (A *v x) $ j / x $ j" and "x $ j \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
y \<in> {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0}

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>y = (A *v x) $h j / x $h j; x $h j \<noteq> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y = (A *v x) $h j / x $h j
x $h j \<noteq> 0

goal (1 subgoal):
 1. \<And>xa. xa \<in> {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0} \<Longrightarrow> 0 < xa
[PROOF STEP]
from lt this x
[PROOF STATE]
proof (chain)
picking this:
lt_vec 0 (A *v x)
y = (A *v x) $h j / x $h j
x $h j \<noteq> 0
lt_vec 0 x
[PROOF STEP]
show "0 < y"
[PROOF STATE]
proof (prove)
using this:
lt_vec 0 (A *v x)
y = (A *v x) $h j / x $h j
x $h j \<noteq> 0
lt_vec 0 x

goal (1 subgoal):
 1. 0 < y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < r x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rx_le_Ax: assumes x: "x \<in> X"
  shows "le_vec (r x *s x) (A *v x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. le_vec (r x *s x) (A *v x)
[PROOF STEP]
proof (intro allI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. (r x *s x) $h i \<le> (A *v x) $h i
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. (r x *s x) $h i \<le> (A *v x) $h i
[PROOF STEP]
show "(r x *s x) $h i \<le> (A *v x) $h i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r x *s x) $h i \<le> (A *v x) $h i
[PROOF STEP]
proof (cases "x $ i = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x $h i = 0 \<Longrightarrow> (r x *s x) $h i \<le> (A *v x) $h i
 2. x $h i \<noteq> 0 \<Longrightarrow> (r x *s x) $h i \<le> (A *v x) $h i
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x $h i = 0

goal (2 subgoals):
 1. x $h i = 0 \<Longrightarrow> (r x *s x) $h i \<le> (A *v x) $h i
 2. x $h i \<noteq> 0 \<Longrightarrow> (r x *s x) $h i \<le> (A *v x) $h i
[PROOF STEP]
with nonneg_Ax[OF x]
[PROOF STATE]
proof (chain)
picking this:
le_vec 0 (A *v x)
x $h i = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
le_vec 0 (A *v x)
x $h i = 0

goal (1 subgoal):
 1. (r x *s x) $h i \<le> (A *v x) $h i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(r x *s x) $h i \<le> (A *v x) $h i

goal (1 subgoal):
 1. x $h i \<noteq> 0 \<Longrightarrow> (r x *s x) $h i \<le> (A *v x) $h i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x $h i \<noteq> 0 \<Longrightarrow> (r x *s x) $h i \<le> (A *v x) $h i
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x $h i \<noteq> 0

goal (1 subgoal):
 1. x $h i \<noteq> 0 \<Longrightarrow> (r x *s x) $h i \<le> (A *v x) $h i
[PROOF STEP]
with x[unfolded X_def]
[PROOF STATE]
proof (chain)
picking this:
x \<in> {x. le_vec 0 x \<and> x \<noteq> 0}
x $h i \<noteq> 0
[PROOF STEP]
have pos: "x $ i > 0"
[PROOF STATE]
proof (prove)
using this:
x \<in> {x. le_vec 0 x \<and> x \<noteq> 0}
x $h i \<noteq> 0

goal (1 subgoal):
 1. 0 < x $h i
[PROOF STEP]
by (auto simp: dual_order.not_eq_order_implies_strict)
[PROOF STATE]
proof (state)
this:
0 < x $h i

goal (1 subgoal):
 1. x $h i \<noteq> 0 \<Longrightarrow> (r x *s x) $h i \<le> (A *v x) $h i
[PROOF STEP]
from False
[PROOF STATE]
proof (chain)
picking this:
x $h i \<noteq> 0
[PROOF STEP]
have "(A *v x) $h i / x $ i \<in> { (A *v x) $ j / x $ j | j. x $ j \<noteq> 0 }"
[PROOF STATE]
proof (prove)
using this:
x $h i \<noteq> 0

goal (1 subgoal):
 1. (A *v x) $h i / x $h i \<in> {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(A *v x) $h i / x $h i \<in> {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0}

goal (1 subgoal):
 1. x $h i \<noteq> 0 \<Longrightarrow> (r x *s x) $h i \<le> (A *v x) $h i
[PROOF STEP]
hence "(A *v x) $h i / x $ i \<ge> r x"
[PROOF STATE]
proof (prove)
using this:
(A *v x) $h i / x $h i \<in> {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0}

goal (1 subgoal):
 1. r x \<le> (A *v x) $h i / x $h i
[PROOF STEP]
unfolding r_def
[PROOF STATE]
proof (prove)
using this:
(A *v x) $h i / x $h i \<in> {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0}

goal (1 subgoal):
 1. Min {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0} \<le> (A *v x) $h i / x $h i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r x \<le> (A *v x) $h i / x $h i

goal (1 subgoal):
 1. x $h i \<noteq> 0 \<Longrightarrow> (r x *s x) $h i \<le> (A *v x) $h i
[PROOF STEP]
hence "x $ i * r x \<le> x $ i * ((A *v x) $h i / x $ i)"
[PROOF STATE]
proof (prove)
using this:
r x \<le> (A *v x) $h i / x $h i

goal (1 subgoal):
 1. x $h i * r x \<le> x $h i * ((A *v x) $h i / x $h i)
[PROOF STEP]
unfolding mult_le_cancel_left_pos[OF pos]
[PROOF STATE]
proof (prove)
using this:
r x \<le> (A *v x) $h i / x $h i

goal (1 subgoal):
 1. r x \<le> (A *v x) $h i / x $h i
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x $h i * r x \<le> x $h i * ((A *v x) $h i / x $h i)

goal (1 subgoal):
 1. x $h i \<noteq> 0 \<Longrightarrow> (r x *s x) $h i \<le> (A *v x) $h i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x $h i * r x \<le> x $h i * ((A *v x) $h i / x $h i)

goal (1 subgoal):
 1. x $h i \<noteq> 0 \<Longrightarrow> (r x *s x) $h i \<le> (A *v x) $h i
[PROOF STEP]
have "\<dots> = (A *v x) $h i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x $h i * ((A *v x) $h i / x $h i) = (A *v x) $h i
[PROOF STEP]
using pos
[PROOF STATE]
proof (prove)
using this:
0 < x $h i

goal (1 subgoal):
 1. x $h i * ((A *v x) $h i / x $h i) = (A *v x) $h i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x $h i * ((A *v x) $h i / x $h i) = (A *v x) $h i

goal (1 subgoal):
 1. x $h i \<noteq> 0 \<Longrightarrow> (r x *s x) $h i \<le> (A *v x) $h i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x $h i * r x \<le> (A *v x) $h i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x $h i * r x \<le> (A *v x) $h i

goal (1 subgoal):
 1. (r x *s x) $h i \<le> (A *v x) $h i
[PROOF STEP]
by (simp add: ac_simps)
[PROOF STATE]
proof (state)
this:
(r x *s x) $h i \<le> (A *v x) $h i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(r x *s x) $h i \<le> (A *v x) $h i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rho_le_x_Ax_imp_rho_le_rx: assumes x: "x \<in> X"
  and \<rho>: "le_vec (\<rho> *s x) (A *v x)"
shows "\<rho> \<le> r x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<rho> \<le> r x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<rho> \<le> r x
[PROOF STEP]
from r_witness[OF x]
[PROOF STATE]
proof (chain)
picking this:
\<exists>j. 0 < x $h j \<and> r x = (A *v x) $h j / x $h j
[PROOF STEP]
obtain j where
    rx: "r x = (A *v x) $ j / x $ j" and xj: "x $ j > 0" "x $ j \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>j. 0 < x $h j \<and> r x = (A *v x) $h j / x $h j

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>r x = (A *v x) $h j / x $h j; 0 < x $h j; 0 \<le> x $h j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r x = (A *v x) $h j / x $h j
0 < x $h j
0 \<le> x $h j

goal (1 subgoal):
 1. \<rho> \<le> r x
[PROOF STEP]
from divide_right_mono[OF \<rho>[rule_format, of j] xj(2)]
[PROOF STATE]
proof (chain)
picking this:
(\<rho> *s x) $h j / x $h j \<le> (A *v x) $h j / x $h j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<rho> *s x) $h j / x $h j \<le> (A *v x) $h j / x $h j

goal (1 subgoal):
 1. \<rho> \<le> r x
[PROOF STEP]
unfolding rx
[PROOF STATE]
proof (prove)
using this:
(\<rho> *s x) $h j / x $h j \<le> (A *v x) $h j / x $h j

goal (1 subgoal):
 1. \<rho> \<le> (A *v x) $h j / x $h j
[PROOF STEP]
using xj
[PROOF STATE]
proof (prove)
using this:
(\<rho> *s x) $h j / x $h j \<le> (A *v x) $h j / x $h j
0 < x $h j
0 \<le> x $h j

goal (1 subgoal):
 1. \<rho> \<le> (A *v x) $h j / x $h j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<rho> \<le> r x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rx_Max: assumes x: "x \<in> X"
  shows "r x = Sup { \<rho> . le_vec (\<rho> *s x) (A *v x) }" (is "_ = Sup ?S")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r x = Sup {\<rho>. le_vec (\<rho> *s x) (A *v x)}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r x = Sup {\<rho>. le_vec (\<rho> *s x) (A *v x)}
[PROOF STEP]
have "r x \<in> ?S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r x \<in> {\<rho>. le_vec (\<rho> *s x) (A *v x)}
[PROOF STEP]
using rx_le_Ax[OF x]
[PROOF STATE]
proof (prove)
using this:
le_vec (r x *s x) (A *v x)

goal (1 subgoal):
 1. r x \<in> {\<rho>. le_vec (\<rho> *s x) (A *v x)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r x \<in> {\<rho>. le_vec (\<rho> *s x) (A *v x)}

goal (1 subgoal):
 1. r x = Sup {\<rho>. le_vec (\<rho> *s x) (A *v x)}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
r x \<in> {\<rho>. le_vec (\<rho> *s x) (A *v x)}

goal (1 subgoal):
 1. r x = Sup {\<rho>. le_vec (\<rho> *s x) (A *v x)}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
r x \<in> {\<rho>. le_vec (\<rho> *s x) (A *v x)}

goal (1 subgoal):
 1. r x = Sup {\<rho>. le_vec (\<rho> *s x) (A *v x)}
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r x = Sup {\<rho>. le_vec (\<rho> *s x) (A *v x)}
[PROOF STEP]
assume "y \<in> ?S"
[PROOF STATE]
proof (state)
this:
y \<in> {\<rho>. le_vec (\<rho> *s x) (A *v x)}

goal (1 subgoal):
 1. r x = Sup {\<rho>. le_vec (\<rho> *s x) (A *v x)}
[PROOF STEP]
hence y: "le_vec (y *s x) (A *v x)"
[PROOF STATE]
proof (prove)
using this:
y \<in> {\<rho>. le_vec (\<rho> *s x) (A *v x)}

goal (1 subgoal):
 1. le_vec (y *s x) (A *v x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
le_vec (y *s x) (A *v x)

goal (1 subgoal):
 1. r x = Sup {\<rho>. le_vec (\<rho> *s x) (A *v x)}
[PROOF STEP]
from rho_le_x_Ax_imp_rho_le_rx[OF x this]
[PROOF STATE]
proof (chain)
picking this:
y \<le> r x
[PROOF STEP]
have "y \<le> r x"
[PROOF STATE]
proof (prove)
using this:
y \<le> r x

goal (1 subgoal):
 1. y \<le> r x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
y \<le> r x

goal (1 subgoal):
 1. r x = Sup {\<rho>. le_vec (\<rho> *s x) (A *v x)}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?y2 \<in> {\<rho>. le_vec (\<rho> *s x) (A *v x)} \<Longrightarrow> ?y2 \<le> r x

goal (1 subgoal):
 1. r x = Sup {\<rho>. le_vec (\<rho> *s x) (A *v x)}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
r x \<in> {\<rho>. le_vec (\<rho> *s x) (A *v x)}
?y2 \<in> {\<rho>. le_vec (\<rho> *s x) (A *v x)} \<Longrightarrow> ?y2 \<le> r x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r x \<in> {\<rho>. le_vec (\<rho> *s x) (A *v x)}
?y2 \<in> {\<rho>. le_vec (\<rho> *s x) (A *v x)} \<Longrightarrow> ?y2 \<le> r x

goal (1 subgoal):
 1. r x = Sup {\<rho>. le_vec (\<rho> *s x) (A *v x)}
[PROOF STEP]
by (metis (mono_tags, lifting) cSup_eq_maximum)
[PROOF STATE]
proof (state)
this:
r x = Sup {\<rho>. le_vec (\<rho> *s x) (A *v x)}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma r_smult: assumes x: "x \<in> X"
  and a: "a > 0"
shows "r (a *s x) = r x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r (a *s x) = r x
[PROOF STEP]
unfolding r_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min {(A *v (a *s x)) $h j / (a *s x) $h j |j. (a *s x) $h j \<noteq> 0} = Min {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0}
[PROOF STEP]
by (rule arg_cong[of _ _ Min], unfold vector_smult_distrib, insert a, simp)


[STATEMENT]
lemma bounded_X1: "bounded X1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded X1
[PROOF STEP]
unfolding bounded_iff X1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a. \<forall>x\<in>X \<inter> {x. norm x = 1}. norm x \<le> a
[PROOF STEP]
by auto


[STATEMENT]
lemma closed_X1: "closed X1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed X1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. closed X1
[PROOF STEP]
have X1: "X1 = {x. le_vec 0 x \<and> norm x = 1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X1 = {x. le_vec 0 x \<and> norm x = 1}
[PROOF STEP]
unfolding X1_def X_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. le_vec 0 x \<and> x \<noteq> 0} \<inter> {x. norm x = 1} = {x. le_vec 0 x \<and> norm x = 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
X1 = {x. le_vec 0 x \<and> norm x = 1}

goal (1 subgoal):
 1. closed X1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed X1
[PROOF STEP]
unfolding X1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed {x. le_vec 0 x \<and> norm x = 1}
[PROOF STEP]
by (intro closed_Collect_conj closed_Collect_all  closed_Collect_le closed_Collect_eq,
      auto intro: continuous_intros)
[PROOF STATE]
proof (state)
this:
closed X1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma compact_X1: "compact X1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compact X1
[PROOF STEP]
using bounded_X1 closed_X1
[PROOF STATE]
proof (prove)
using this:
bounded X1
closed X1

goal (1 subgoal):
 1. compact X1
[PROOF STEP]
by (simp add: compact_eq_bounded_closed)


[STATEMENT]
lemma continuous_pow_A_1: "continuous_on R pow_A_1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on R pow_A_1
[PROOF STEP]
unfolding pow_A_1_def continuous_on
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>R. ((*v) A1n \<longlongrightarrow> A1n *v x) (at x within R)
[PROOF STEP]
by (auto intro: tendsto_intros)


[STATEMENT]
lemma compact_Y: "compact Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compact Y
[PROOF STEP]
unfolding Y_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compact (pow_A_1 ` X1)
[PROOF STEP]
using compact_X1 continuous_pow_A_1[of X1]
[PROOF STATE]
proof (prove)
using this:
compact X1
continuous_on X1 pow_A_1

goal (1 subgoal):
 1. compact (pow_A_1 ` X1)
[PROOF STEP]
by (metis compact_continuous_image)


[STATEMENT]
lemma Y_pos_main: assumes y: "y \<in> pow_A_1 ` X"
  shows "y $ i > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < y $h i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < y $h i
[PROOF STEP]
from y
[PROOF STATE]
proof (chain)
picking this:
y \<in> pow_A_1 ` X
[PROOF STEP]
obtain x where x: "x \<in> X" and y: "y = pow_A_1 x"
[PROOF STATE]
proof (prove)
using this:
y \<in> pow_A_1 ` X

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> X; y = pow_A_1 x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding Y_def X1_def
[PROOF STATE]
proof (prove)
using this:
y \<in> pow_A_1 ` X

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> X; y = pow_A_1 x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> X
y = pow_A_1 x

goal (1 subgoal):
 1. 0 < y $h i
[PROOF STEP]
from r_witness[OF x]
[PROOF STATE]
proof (chain)
picking this:
\<exists>j. 0 < x $h j \<and> r x = (A *v x) $h j / x $h j
[PROOF STEP]
obtain j where xj: "x $ j > 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>j. 0 < x $h j \<and> r x = (A *v x) $h j / x $h j

goal (1 subgoal):
 1. (\<And>j. 0 < x $h j \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < x $h j

goal (1 subgoal):
 1. 0 < y $h i
[PROOF STEP]
from x[unfolded X_def]
[PROOF STATE]
proof (chain)
picking this:
x \<in> {x. le_vec 0 x \<and> x \<noteq> 0}
[PROOF STEP]
have xi: "x $ i \<ge> 0" for i
[PROOF STATE]
proof (prove)
using this:
x \<in> {x. le_vec 0 x \<and> x \<noteq> 0}

goal (1 subgoal):
 1. 0 \<le> x $h i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> x $h ?i

goal (1 subgoal):
 1. 0 < y $h i
[PROOF STEP]
have nonneg: "0 \<le> A1n $ i $ k * x $ k" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> A1n $h i $h k * x $h k
[PROOF STEP]
using A1n_pos[of i k] xi[of k]
[PROOF STATE]
proof (prove)
using this:
0 < A1n $h i $h k
0 \<le> x $h k

goal (1 subgoal):
 1. 0 \<le> A1n $h i $h k * x $h k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> A1n $h i $h ?k * x $h ?k

goal (1 subgoal):
 1. 0 < y $h i
[PROOF STEP]
have "y $ i = (\<Sum>j\<in>UNIV. A1n $ i $ j * x $ j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y $h i = (\<Sum>j\<in>UNIV. A1n $h i $h j * x $h j)
[PROOF STEP]
unfolding y pow_A_1_def matrix_vector_mult_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>i. \<Sum>j\<in>UNIV. A1n $h i $h j * x $h j) $h i = (\<Sum>j\<in>UNIV. A1n $h i $h j * x $h j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y $h i = (\<Sum>j\<in>UNIV. A1n $h i $h j * x $h j)

goal (1 subgoal):
 1. 0 < y $h i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
y $h i = (\<Sum>j\<in>UNIV. A1n $h i $h j * x $h j)

goal (1 subgoal):
 1. 0 < y $h i
[PROOF STEP]
have "\<dots> = A1n $ i $ j * x $ j + (\<Sum>j\<in>UNIV - {j}. A1n $ i $ j * x $ j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j\<in>UNIV. A1n $h i $h j * x $h j) = A1n $h i $h j * x $h j + (\<Sum>j\<in>UNIV - {j}. A1n $h i $h j * x $h j)
[PROOF STEP]
by (subst sum.remove, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>UNIV. A1n $h i $h j * x $h j) = A1n $h i $h j * x $h j + (\<Sum>j\<in>UNIV - {j}. A1n $h i $h j * x $h j)

goal (1 subgoal):
 1. 0 < y $h i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>UNIV. A1n $h i $h j * x $h j) = A1n $h i $h j * x $h j + (\<Sum>j\<in>UNIV - {j}. A1n $h i $h j * x $h j)

goal (1 subgoal):
 1. 0 < y $h i
[PROOF STEP]
have "\<dots> > 0 + 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 + 0 < A1n $h i $h j * x $h j + (\<Sum>j\<in>UNIV - {j}. A1n $h i $h j * x $h j)
[PROOF STEP]
by (rule add_less_le_mono, insert xj A1n_pos nonneg,
    auto intro!: sum_nonneg mult_pos_pos simp: dual_order.not_eq_order_implies_strict)
[PROOF STATE]
proof (state)
this:
0 + 0 < A1n $h i $h j * x $h j + (\<Sum>j\<in>UNIV - {j}. A1n $h i $h j * x $h j)

goal (1 subgoal):
 1. 0 < y $h i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
0 + 0 < y $h i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 + 0 < y $h i

goal (1 subgoal):
 1. 0 < y $h i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < y $h i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Y_pos: assumes y: "y \<in> Y"
  shows "y $ i > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < y $h i
[PROOF STEP]
using Y_pos_main[of y i] y
[PROOF STATE]
proof (prove)
using this:
y \<in> pow_A_1 ` X \<Longrightarrow> 0 < y $h i
y \<in> Y

goal (1 subgoal):
 1. 0 < y $h i
[PROOF STEP]
unfolding Y_def X1_def
[PROOF STATE]
proof (prove)
using this:
y \<in> pow_A_1 ` X \<Longrightarrow> 0 < y $h i
y \<in> pow_A_1 ` (X \<inter> {x. norm x = 1})

goal (1 subgoal):
 1. 0 < y $h i
[PROOF STEP]
by auto


[STATEMENT]
lemma Y_nonzero: assumes y: "y \<in> Y"
  shows "y $ i \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y $h i \<noteq> 0
[PROOF STEP]
using Y_pos[OF y, of i]
[PROOF STATE]
proof (prove)
using this:
0 < y $h i

goal (1 subgoal):
 1. y $h i \<noteq> 0
[PROOF STEP]
by auto


[STATEMENT]
lemma r'_r: assumes x: "x \<in> Y" shows "r' x = r x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r' x = r x
[PROOF STEP]
unfolding r'_def r_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (MIN j. (A *v x) $h j / x $h j) = Min {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0}
[PROOF STEP]
proof (rule arg_cong[of _ _ Min])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. range (\<lambda>j. (A *v x) $h j / x $h j) = {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0}
[PROOF STEP]
have "range (\<lambda>j. (A *v x) $ j / x $ j) \<subseteq> {(A *v x) $ j / x $ j |j. x $ j \<noteq> 0}" (is "?L \<subseteq> ?R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range (\<lambda>j. (A *v x) $h j / x $h j) \<subseteq> {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> range (\<lambda>j. (A *v x) $h j / x $h j) \<Longrightarrow> xa \<in> {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0}
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> range (\<lambda>j. (A *v x) $h j / x $h j) \<Longrightarrow> xa \<in> {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0}
[PROOF STEP]
assume "y \<in> ?L"
[PROOF STATE]
proof (state)
this:
y \<in> range (\<lambda>j. (A *v x) $h j / x $h j)

goal (1 subgoal):
 1. \<And>xa. xa \<in> range (\<lambda>j. (A *v x) $h j / x $h j) \<Longrightarrow> xa \<in> {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> range (\<lambda>j. (A *v x) $h j / x $h j)
[PROOF STEP]
obtain j where "y = (A *v x) $ j / x $ j"
[PROOF STATE]
proof (prove)
using this:
y \<in> range (\<lambda>j. (A *v x) $h j / x $h j)

goal (1 subgoal):
 1. (\<And>j. y = (A *v x) $h j / x $h j \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y = (A *v x) $h j / x $h j

goal (1 subgoal):
 1. \<And>xa. xa \<in> range (\<lambda>j. (A *v x) $h j / x $h j) \<Longrightarrow> xa \<in> {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0}
[PROOF STEP]
with Y_pos[OF x, of j]
[PROOF STATE]
proof (chain)
picking this:
0 < x $h j
y = (A *v x) $h j / x $h j
[PROOF STEP]
show "y \<in> ?R"
[PROOF STATE]
proof (prove)
using this:
0 < x $h j
y = (A *v x) $h j / x $h j

goal (1 subgoal):
 1. y \<in> {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
range (\<lambda>j. (A *v x) $h j / x $h j) \<subseteq> {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0}

goal (1 subgoal):
 1. range (\<lambda>j. (A *v x) $h j / x $h j) = {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
range (\<lambda>j. (A *v x) $h j / x $h j) \<subseteq> {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0}

goal (1 subgoal):
 1. range (\<lambda>j. (A *v x) $h j / x $h j) = {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0}
[PROOF STEP]
have "?L \<supseteq> ?R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0} \<subseteq> range (\<lambda>j. (A *v x) $h j / x $h j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(A *v x) $h j / x $h j |j. x $h j \<noteq> 0} \<subseteq> range (\<lambda>j. (A *v x) $h j / x $h j)

goal (1 subgoal):
 1. range (\<lambda>j. (A *v x) $h j / x $h j) = {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
range (\<lambda>j. (A *v x) $h j / x $h j) \<subseteq> {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0}
{(A *v x) $h j / x $h j |j. x $h j \<noteq> 0} \<subseteq> range (\<lambda>j. (A *v x) $h j / x $h j)
[PROOF STEP]
show "?L = ?R"
[PROOF STATE]
proof (prove)
using this:
range (\<lambda>j. (A *v x) $h j / x $h j) \<subseteq> {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0}
{(A *v x) $h j / x $h j |j. x $h j \<noteq> 0} \<subseteq> range (\<lambda>j. (A *v x) $h j / x $h j)

goal (1 subgoal):
 1. range (\<lambda>j. (A *v x) $h j / x $h j) = {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
range (\<lambda>j. (A *v x) $h j / x $h j) = {(A *v x) $h j / x $h j |j. x $h j \<noteq> 0}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma continuous_Y_r: "continuous_on Y r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on Y r
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. continuous_on Y r
[PROOF STEP]
have *: "(\<forall> y \<in> Y. P y (r y)) = (\<forall> y \<in> Y. P y (r' y))" for P
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>y\<in>Y. P y (r y)) = (\<forall>y\<in>Y. P y (r' y))
[PROOF STEP]
using r'_r
[PROOF STATE]
proof (prove)
using this:
?x \<in> Y \<Longrightarrow> r' ?x = r ?x

goal (1 subgoal):
 1. (\<forall>y\<in>Y. P y (r y)) = (\<forall>y\<in>Y. P y (r' y))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<forall>y\<in>Y. ?P y (r y)) = (\<forall>y\<in>Y. ?P y (r' y))

goal (1 subgoal):
 1. continuous_on Y r
[PROOF STEP]
have "continuous_on Y r = continuous_on Y r'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on Y r = continuous_on Y r'
[PROOF STEP]
by (rule continuous_on_cong[OF refl r'_r[symmetric]])
[PROOF STATE]
proof (state)
this:
continuous_on Y r = continuous_on Y r'

goal (1 subgoal):
 1. continuous_on Y r
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
continuous_on Y r = continuous_on Y r'

goal (1 subgoal):
 1. continuous_on Y r
[PROOF STEP]
have \<dots>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on Y r'
[PROOF STEP]
unfolding continuous_on r'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>Y. ((\<lambda>x. MIN j. (A *v x) $h j / x $h j) \<longlongrightarrow> (MIN j. (A *v x) $h j / x $h j)) (at x within Y)
[PROOF STEP]
using Y_nonzero
[PROOF STATE]
proof (prove)
using this:
?y \<in> Y \<Longrightarrow> ?y $h ?i \<noteq> 0

goal (1 subgoal):
 1. \<forall>x\<in>Y. ((\<lambda>x. MIN j. (A *v x) $h j / x $h j) \<longlongrightarrow> (MIN j. (A *v x) $h j / x $h j)) (at x within Y)
[PROOF STEP]
by (auto intro!: tendsto_Min tendsto_intros)
[PROOF STATE]
proof (state)
this:
continuous_on Y r'

goal (1 subgoal):
 1. continuous_on Y r
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
continuous_on Y r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
continuous_on Y r

goal (1 subgoal):
 1. continuous_on Y r
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
continuous_on Y r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma X1_nonempty: "X1 \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X1 \<noteq> {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. X1 \<noteq> {}
[PROOF STEP]
define x where "x = ((\<chi> i. if i = undefined then 1 else 0) :: real ^ 'n)"
[PROOF STATE]
proof (state)
this:
x = (\<chi>i. if i = undefined then 1 else 0)

goal (1 subgoal):
 1. X1 \<noteq> {}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
x = (\<chi>i. if i = undefined then 1 else 0)

goal (1 subgoal):
 1. X1 \<noteq> {}
[PROOF STEP]
assume "x = 0"
[PROOF STATE]
proof (state)
this:
x = 0

goal (1 subgoal):
 1. X1 \<noteq> {}
[PROOF STEP]
from arg_cong[OF this, of "\<lambda> x. x $ undefined"]
[PROOF STATE]
proof (chain)
picking this:
x $h undefined = 0 $h undefined
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
x $h undefined = 0 $h undefined

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding x_def
[PROOF STATE]
proof (prove)
using this:
(\<chi>i. if i = undefined then 1 else 0) $h undefined = 0 $h undefined

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. X1 \<noteq> {}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
x = 0 \<Longrightarrow> False

goal (1 subgoal):
 1. X1 \<noteq> {}
[PROOF STEP]
hence x: "x \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
x = 0 \<Longrightarrow> False

goal (1 subgoal):
 1. x \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<noteq> 0

goal (1 subgoal):
 1. X1 \<noteq> {}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<noteq> 0

goal (1 subgoal):
 1. X1 \<noteq> {}
[PROOF STEP]
have "le_vec 0 x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. le_vec 0 x
[PROOF STEP]
unfolding x_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. le_vec 0 (\<chi>i. if i = undefined then 1 else 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
le_vec 0 x

goal (1 subgoal):
 1. X1 \<noteq> {}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
le_vec 0 x

goal (1 subgoal):
 1. X1 \<noteq> {}
[PROOF STEP]
have "norm x = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm x = 1
[PROOF STEP]
unfolding norm_vec_def L2_set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqrt (\<Sum>i\<in>UNIV. (norm (x $h i))\<^sup>2) = 1
[PROOF STEP]
by (auto, subst sum.remove[of _ undefined], auto simp: x_def)
[PROOF STATE]
proof (state)
this:
norm x = 1

goal (1 subgoal):
 1. X1 \<noteq> {}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> 0
le_vec 0 x
norm x = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0
le_vec 0 x
norm x = 1

goal (1 subgoal):
 1. X1 \<noteq> {}
[PROOF STEP]
unfolding X1_def X_def
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0
le_vec 0 x
norm x = 1

goal (1 subgoal):
 1. {x. le_vec 0 x \<and> x \<noteq> 0} \<inter> {x. norm x = 1} \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
X1 \<noteq> {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Y_nonempty: "Y \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Y \<noteq> {}
[PROOF STEP]
unfolding Y_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pow_A_1 ` X1 \<noteq> {}
[PROOF STEP]
using X1_nonempty
[PROOF STATE]
proof (prove)
using this:
X1 \<noteq> {}

goal (1 subgoal):
 1. pow_A_1 ` X1 \<noteq> {}
[PROOF STEP]
by auto


[STATEMENT]
lemma z: "z \<in> Y" and sr_max_Y: "\<And> y. y \<in> Y \<Longrightarrow> r y \<le> sr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<in> Y &&& (\<And>y. y \<in> Y \<Longrightarrow> r y \<le> sr)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. z \<in> Y
 2. \<And>y. y \<in> Y \<Longrightarrow> r y \<le> sr
[PROOF STEP]
let ?P = "\<lambda> z. z \<in> Y \<and> (\<forall> y \<in> Y. r y \<le> r z)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. z \<in> Y
 2. \<And>y. y \<in> Y \<Longrightarrow> r y \<le> sr
[PROOF STEP]
from continuous_attains_sup[OF compact_Y Y_nonempty continuous_Y_r]
[PROOF STATE]
proof (chain)
picking this:
\<exists>x\<in>Y. \<forall>y\<in>Y. r y \<le> r x
[PROOF STEP]
obtain y where "?P y"
[PROOF STATE]
proof (prove)
using this:
\<exists>x\<in>Y. \<forall>y\<in>Y. r y \<le> r x

goal (1 subgoal):
 1. (\<And>y. y \<in> Y \<and> (\<forall>ya\<in>Y. r ya \<le> r y) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y \<in> Y \<and> (\<forall>ya\<in>Y. r ya \<le> r y)

goal (2 subgoals):
 1. z \<in> Y
 2. \<And>y. y \<in> Y \<Longrightarrow> r y \<le> sr
[PROOF STEP]
from someI[of ?P, OF this, folded z_def]
[PROOF STATE]
proof (chain)
picking this:
z \<in> Y \<and> (\<forall>y\<in>Y. r y \<le> sr)
[PROOF STEP]
show "z \<in> Y" "\<And> y. y \<in> Y \<Longrightarrow> r y \<le> r z"
[PROOF STATE]
proof (prove)
using this:
z \<in> Y \<and> (\<forall>y\<in>Y. r y \<le> sr)

goal (1 subgoal):
 1. z \<in> Y &&& (\<And>y. y \<in> Y \<Longrightarrow> r y \<le> sr)
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
z \<in> Y
?y \<in> Y \<Longrightarrow> r ?y \<le> sr

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Y_subset_X: "Y \<subseteq> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Y \<subseteq> X
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Y \<Longrightarrow> x \<in> X
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Y \<Longrightarrow> x \<in> X
[PROOF STEP]
assume "y \<in> Y"
[PROOF STATE]
proof (state)
this:
y \<in> Y

goal (1 subgoal):
 1. \<And>x. x \<in> Y \<Longrightarrow> x \<in> X
[PROOF STEP]
from Y_pos[OF this]
[PROOF STATE]
proof (chain)
picking this:
0 < y $h ?i
[PROOF STEP]
show "y \<in> X"
[PROOF STATE]
proof (prove)
using this:
0 < y $h ?i

goal (1 subgoal):
 1. y \<in> X
[PROOF STEP]
unfolding X_def
[PROOF STATE]
proof (prove)
using this:
0 < y $h ?i

goal (1 subgoal):
 1. y \<in> {x. le_vec 0 x \<and> x \<noteq> 0}
[PROOF STEP]
by (auto simp: order.strict_iff_order)
[PROOF STATE]
proof (state)
this:
y \<in> X

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma zX: "z \<in> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<in> X
[PROOF STEP]
using z(1) Y_subset_X
[PROOF STATE]
proof (prove)
using this:
z \<in> Y
Y \<subseteq> X

goal (1 subgoal):
 1. z \<in> X
[PROOF STEP]
by auto


[STATEMENT]
lemma le_vec_mono_left: assumes B: "\<And> i j. B $ i $ j \<ge> 0"
  and "le_vec x y"
shows "le_vec (B *v x) (B *v y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. le_vec (B *v x) (B *v y)
[PROOF STEP]
proof (intro allI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. (B *v x) $h i \<le> (B *v y) $h i
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. (B *v x) $h i \<le> (B *v y) $h i
[PROOF STEP]
show "(B *v x) $ i \<le> (B *v y) $ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (B *v x) $h i \<le> (B *v y) $h i
[PROOF STEP]
unfolding matrix_vector_mult_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>i. \<Sum>j\<in>UNIV. B $h i $h j * x $h j) $h i \<le> (\<chi>i. \<Sum>j\<in>UNIV. B $h i $h j * y $h j) $h i
[PROOF STEP]
using B[of i] assms(2)
[PROOF STATE]
proof (prove)
using this:
0 \<le> B $h i $h ?j
le_vec x y

goal (1 subgoal):
 1. (\<chi>i. \<Sum>j\<in>UNIV. B $h i $h j * x $h j) $h i \<le> (\<chi>i. \<Sum>j\<in>UNIV. B $h i $h j * y $h j) $h i
[PROOF STEP]
by (auto intro!: sum_mono mult_left_mono)
[PROOF STATE]
proof (state)
this:
(B *v x) $h i \<le> (B *v y) $h i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma matpow_1_commute: "matpow (A + mat 1) n ** A = A ** matpow (A + mat 1) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matpow (A + mat 1) n ** A = A ** matpow (A + mat 1) n
[PROOF STEP]
by (induct n, auto simp: matrix_add_rdistrib matrix_add_ldistrib matrix_mul_rid matrix_mul_lid
  matrix_mul_assoc[symmetric])


[STATEMENT]
lemma A1n_commute: "A1n ** A = A ** A1n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A1n ** A = A ** A1n
[PROOF STEP]
unfolding A1n_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matpow (A + mat 1) N ** A = A ** matpow (A + mat 1) N
[PROOF STEP]
by (rule matpow_1_commute)


[STATEMENT]
lemma le_vec_pow_A_1: assumes le: "le_vec (rho *s x) (A *v x)"
  shows "le_vec (rho *s pow_A_1 x) (A *v pow_A_1 x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. le_vec (rho *s pow_A_1 x) (A *v pow_A_1 x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. le_vec (rho *s pow_A_1 x) (A *v pow_A_1 x)
[PROOF STEP]
have "A1n $ i $ j \<ge> 0" for i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> A1n $h i $h j
[PROOF STEP]
using A1n_pos[of i j]
[PROOF STATE]
proof (prove)
using this:
0 < A1n $h i $h j

goal (1 subgoal):
 1. 0 \<le> A1n $h i $h j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> A1n $h ?i $h ?j

goal (1 subgoal):
 1. le_vec (rho *s pow_A_1 x) (A *v pow_A_1 x)
[PROOF STEP]
from le_vec_mono_left[OF this le]
[PROOF STATE]
proof (chain)
picking this:
le_vec (A1n *v (rho *s x)) (A1n *v (A *v x))
[PROOF STEP]
have "le_vec (A1n *v (rho *s x)) (A1n *v (A *v x))"
[PROOF STATE]
proof (prove)
using this:
le_vec (A1n *v (rho *s x)) (A1n *v (A *v x))

goal (1 subgoal):
 1. le_vec (A1n *v (rho *s x)) (A1n *v (A *v x))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
le_vec (A1n *v (rho *s x)) (A1n *v (A *v x))

goal (1 subgoal):
 1. le_vec (rho *s pow_A_1 x) (A *v pow_A_1 x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
le_vec (A1n *v (rho *s x)) (A1n *v (A *v x))

goal (1 subgoal):
 1. le_vec (rho *s pow_A_1 x) (A *v pow_A_1 x)
[PROOF STEP]
have "A1n *v (A *v x) = (A1n ** A) *v x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A1n *v (A *v x) = A1n ** A *v x
[PROOF STEP]
by (simp add: matrix_vector_mul_assoc)
[PROOF STATE]
proof (state)
this:
A1n *v (A *v x) = A1n ** A *v x

goal (1 subgoal):
 1. le_vec (rho *s pow_A_1 x) (A *v pow_A_1 x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
A1n *v (A *v x) = A1n ** A *v x

goal (1 subgoal):
 1. le_vec (rho *s pow_A_1 x) (A *v pow_A_1 x)
[PROOF STEP]
have "\<dots> = A *v (A1n *v x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A1n ** A *v x = A *v (A1n *v x)
[PROOF STEP]
unfolding A1n_commute
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A ** A1n *v x = A *v (A1n *v x)
[PROOF STEP]
by (simp add: matrix_vector_mul_assoc)
[PROOF STATE]
proof (state)
this:
A1n ** A *v x = A *v (A1n *v x)

goal (1 subgoal):
 1. le_vec (rho *s pow_A_1 x) (A *v pow_A_1 x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
A1n ** A *v x = A *v (A1n *v x)

goal (1 subgoal):
 1. le_vec (rho *s pow_A_1 x) (A *v pow_A_1 x)
[PROOF STEP]
have "\<dots> = A *v (pow_A_1 x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *v (A1n *v x) = A *v pow_A_1 x
[PROOF STEP]
unfolding pow_A_1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *v (A1n *v x) = A *v (A1n *v x)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
A *v (A1n *v x) = A *v pow_A_1 x

goal (1 subgoal):
 1. le_vec (rho *s pow_A_1 x) (A *v pow_A_1 x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
A *v (A1n *v x) = A *v pow_A_1 x

goal (1 subgoal):
 1. le_vec (rho *s pow_A_1 x) (A *v pow_A_1 x)
[PROOF STEP]
have "A1n *v (rho *s x) = rho *s (A1n *v x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A1n *v (rho *s x) = rho *s (A1n *v x)
[PROOF STEP]
unfolding vector_smult_distrib
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rho *s (A1n *v x) = rho *s (A1n *v x)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
A1n *v (rho *s x) = rho *s (A1n *v x)

goal (1 subgoal):
 1. le_vec (rho *s pow_A_1 x) (A *v pow_A_1 x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
A1n *v (rho *s x) = rho *s (A1n *v x)

goal (1 subgoal):
 1. le_vec (rho *s pow_A_1 x) (A *v pow_A_1 x)
[PROOF STEP]
have "\<dots> = rho *s pow_A_1 x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rho *s (A1n *v x) = rho *s pow_A_1 x
[PROOF STEP]
unfolding pow_A_1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rho *s (A1n *v x) = rho *s (A1n *v x)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
rho *s (A1n *v x) = rho *s pow_A_1 x

goal (1 subgoal):
 1. le_vec (rho *s pow_A_1 x) (A *v pow_A_1 x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
le_vec (rho *s pow_A_1 x) (A *v pow_A_1 x)
[PROOF STEP]
show "le_vec (rho *s pow_A_1 x) (A *v pow_A_1 x)"
[PROOF STATE]
proof (prove)
using this:
le_vec (rho *s pow_A_1 x) (A *v pow_A_1 x)

goal (1 subgoal):
 1. le_vec (rho *s pow_A_1 x) (A *v pow_A_1 x)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
le_vec (rho *s pow_A_1 x) (A *v pow_A_1 x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma r_pow_A_1: assumes x: "x \<in> X"
  shows "r x \<le> r (pow_A_1 x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r x \<le> r (pow_A_1 x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r x \<le> r (pow_A_1 x)
[PROOF STEP]
let ?y = "pow_A_1 x"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r x \<le> r (pow_A_1 x)
[PROOF STEP]
have "?y \<in> pow_A_1 ` X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pow_A_1 x \<in> pow_A_1 ` X
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
x \<in> X

goal (1 subgoal):
 1. pow_A_1 x \<in> pow_A_1 ` X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pow_A_1 x \<in> pow_A_1 ` X

goal (1 subgoal):
 1. r x \<le> r (pow_A_1 x)
[PROOF STEP]
from Y_pos_main[OF this]
[PROOF STATE]
proof (chain)
picking this:
0 < pow_A_1 x $h ?i
[PROOF STEP]
have y: "?y \<in> X"
[PROOF STATE]
proof (prove)
using this:
0 < pow_A_1 x $h ?i

goal (1 subgoal):
 1. pow_A_1 x \<in> X
[PROOF STEP]
unfolding X_def
[PROOF STATE]
proof (prove)
using this:
0 < pow_A_1 x $h ?i

goal (1 subgoal):
 1. pow_A_1 x \<in> {x. le_vec 0 x \<and> x \<noteq> 0}
[PROOF STEP]
by (auto simp: order.strict_iff_order)
[PROOF STATE]
proof (state)
this:
pow_A_1 x \<in> X

goal (1 subgoal):
 1. r x \<le> r (pow_A_1 x)
[PROOF STEP]
let ?A = "{\<rho>. le_vec (\<rho> *s x) (A *v x)}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r x \<le> r (pow_A_1 x)
[PROOF STEP]
let ?B = "{\<rho>. le_vec (\<rho> *s pow_A_1 x) (A *v pow_A_1 x)}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r x \<le> r (pow_A_1 x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r x \<le> r (pow_A_1 x)
[PROOF STEP]
unfolding rx_Max[OF x] rx_Max[OF y]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sup {\<rho>. le_vec (\<rho> *s x) (A *v x)} \<le> Sup {\<rho>. le_vec (\<rho> *s pow_A_1 x) (A *v pow_A_1 x)}
[PROOF STEP]
proof (rule cSup_mono)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. {\<rho>. le_vec (\<rho> *s x) (A *v x)} \<noteq> {}
 2. bdd_above {\<rho>. le_vec (\<rho> *s pow_A_1 x) (A *v pow_A_1 x)}
 3. \<And>b. b \<in> {\<rho>. le_vec (\<rho> *s x) (A *v x)} \<Longrightarrow> \<exists>a\<in>{\<rho>. le_vec (\<rho> *s pow_A_1 x) (A *v pow_A_1 x)}. b \<le> a
[PROOF STEP]
show "bdd_above ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_above {\<rho>. le_vec (\<rho> *s pow_A_1 x) (A *v pow_A_1 x)}
[PROOF STEP]
using rho_le_x_Ax_imp_rho_le_rx[OF y]
[PROOF STATE]
proof (prove)
using this:
le_vec (?\<rho> *s pow_A_1 x) (A *v pow_A_1 x) \<Longrightarrow> ?\<rho> \<le> r (pow_A_1 x)

goal (1 subgoal):
 1. bdd_above {\<rho>. le_vec (\<rho> *s pow_A_1 x) (A *v pow_A_1 x)}
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
bdd_above {\<rho>. le_vec (\<rho> *s pow_A_1 x) (A *v pow_A_1 x)}

goal (2 subgoals):
 1. {\<rho>. le_vec (\<rho> *s x) (A *v x)} \<noteq> {}
 2. \<And>b. b \<in> {\<rho>. le_vec (\<rho> *s x) (A *v x)} \<Longrightarrow> \<exists>a\<in>{\<rho>. le_vec (\<rho> *s pow_A_1 x) (A *v pow_A_1 x)}. b \<le> a
[PROOF STEP]
show "?A \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {\<rho>. le_vec (\<rho> *s x) (A *v x)} \<noteq> {}
[PROOF STEP]
using rx_le_Ax[OF x]
[PROOF STATE]
proof (prove)
using this:
le_vec (r x *s x) (A *v x)

goal (1 subgoal):
 1. {\<rho>. le_vec (\<rho> *s x) (A *v x)} \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{\<rho>. le_vec (\<rho> *s x) (A *v x)} \<noteq> {}

goal (1 subgoal):
 1. \<And>b. b \<in> {\<rho>. le_vec (\<rho> *s x) (A *v x)} \<Longrightarrow> \<exists>a\<in>{\<rho>. le_vec (\<rho> *s pow_A_1 x) (A *v pow_A_1 x)}. b \<le> a
[PROOF STEP]
fix rho
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b. b \<in> {\<rho>. le_vec (\<rho> *s x) (A *v x)} \<Longrightarrow> \<exists>a\<in>{\<rho>. le_vec (\<rho> *s pow_A_1 x) (A *v pow_A_1 x)}. b \<le> a
[PROOF STEP]
assume "rho \<in> ?A"
[PROOF STATE]
proof (state)
this:
rho \<in> {\<rho>. le_vec (\<rho> *s x) (A *v x)}

goal (1 subgoal):
 1. \<And>b. b \<in> {\<rho>. le_vec (\<rho> *s x) (A *v x)} \<Longrightarrow> \<exists>a\<in>{\<rho>. le_vec (\<rho> *s pow_A_1 x) (A *v pow_A_1 x)}. b \<le> a
[PROOF STEP]
hence "le_vec (rho *s x) (A *v x)"
[PROOF STATE]
proof (prove)
using this:
rho \<in> {\<rho>. le_vec (\<rho> *s x) (A *v x)}

goal (1 subgoal):
 1. le_vec (rho *s x) (A *v x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
le_vec (rho *s x) (A *v x)

goal (1 subgoal):
 1. \<And>b. b \<in> {\<rho>. le_vec (\<rho> *s x) (A *v x)} \<Longrightarrow> \<exists>a\<in>{\<rho>. le_vec (\<rho> *s pow_A_1 x) (A *v pow_A_1 x)}. b \<le> a
[PROOF STEP]
from le_vec_pow_A_1[OF this]
[PROOF STATE]
proof (chain)
picking this:
le_vec (rho *s pow_A_1 x) (A *v pow_A_1 x)
[PROOF STEP]
have "rho \<in> ?B"
[PROOF STATE]
proof (prove)
using this:
le_vec (rho *s pow_A_1 x) (A *v pow_A_1 x)

goal (1 subgoal):
 1. rho \<in> {\<rho>. le_vec (\<rho> *s pow_A_1 x) (A *v pow_A_1 x)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rho \<in> {\<rho>. le_vec (\<rho> *s pow_A_1 x) (A *v pow_A_1 x)}

goal (1 subgoal):
 1. \<And>b. b \<in> {\<rho>. le_vec (\<rho> *s x) (A *v x)} \<Longrightarrow> \<exists>a\<in>{\<rho>. le_vec (\<rho> *s pow_A_1 x) (A *v pow_A_1 x)}. b \<le> a
[PROOF STEP]
thus "\<exists> rho' \<in> ?B. rho \<le> rho'"
[PROOF STATE]
proof (prove)
using this:
rho \<in> {\<rho>. le_vec (\<rho> *s pow_A_1 x) (A *v pow_A_1 x)}

goal (1 subgoal):
 1. \<exists>rho'\<in>{\<rho>. le_vec (\<rho> *s pow_A_1 x) (A *v pow_A_1 x)}. rho \<le> rho'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>rho'\<in>{\<rho>. le_vec (\<rho> *s pow_A_1 x) (A *v pow_A_1 x)}. rho \<le> rho'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
r x \<le> r (pow_A_1 x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sr_max: assumes x: "x \<in> X"
  shows "r x \<le> sr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r x \<le> sr
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r x \<le> sr
[PROOF STEP]
let ?n = "norm x"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r x \<le> sr
[PROOF STEP]
define x' where "x' = inverse ?n *s x"
[PROOF STATE]
proof (state)
this:
x' = inverse (norm x) *s x

goal (1 subgoal):
 1. r x \<le> sr
[PROOF STEP]
from x[unfolded X_def]
[PROOF STATE]
proof (chain)
picking this:
x \<in> {x. le_vec 0 x \<and> x \<noteq> 0}
[PROOF STEP]
have x0: "x \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
x \<in> {x. le_vec 0 x \<and> x \<noteq> 0}

goal (1 subgoal):
 1. x \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<noteq> 0

goal (1 subgoal):
 1. r x \<le> sr
[PROOF STEP]
hence n: "?n > 0"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0

goal (1 subgoal):
 1. 0 < norm x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < norm x

goal (1 subgoal):
 1. r x \<le> sr
[PROOF STEP]
have x': "x' \<in> X1" "x' \<in> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x' \<in> X1 &&& x' \<in> X
[PROOF STEP]
using x n
[PROOF STATE]
proof (prove)
using this:
x \<in> X
0 < norm x

goal (1 subgoal):
 1. x' \<in> X1 &&& x' \<in> X
[PROOF STEP]
unfolding X1_def X_def x'_def
[PROOF STATE]
proof (prove)
using this:
x \<in> {x. le_vec 0 x \<and> x \<noteq> 0}
0 < norm x

goal (1 subgoal):
 1. inverse (norm x) *s x \<in> {x. le_vec 0 x \<and> x \<noteq> 0} \<inter> {x. norm x = 1} &&& inverse (norm x) *s x \<in> {x. le_vec 0 x \<and> x \<noteq> 0}
[PROOF STEP]
by (auto simp: norm_smult)
[PROOF STATE]
proof (state)
this:
x' \<in> X1
x' \<in> X

goal (1 subgoal):
 1. r x \<le> sr
[PROOF STEP]
have id: "r x = r x'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r x = r x'
[PROOF STEP]
unfolding x'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r x = r (inverse (norm x) *s x)
[PROOF STEP]
by (rule sym, rule r_smult[OF x], insert n, auto)
[PROOF STATE]
proof (state)
this:
r x = r x'

goal (1 subgoal):
 1. r x \<le> sr
[PROOF STEP]
define y where "y = pow_A_1 x'"
[PROOF STATE]
proof (state)
this:
y = pow_A_1 x'

goal (1 subgoal):
 1. r x \<le> sr
[PROOF STEP]
from x'
[PROOF STATE]
proof (chain)
picking this:
x' \<in> X1
x' \<in> X
[PROOF STEP]
have y: "y \<in> Y"
[PROOF STATE]
proof (prove)
using this:
x' \<in> X1
x' \<in> X

goal (1 subgoal):
 1. y \<in> Y
[PROOF STEP]
unfolding Y_def y_def
[PROOF STATE]
proof (prove)
using this:
x' \<in> X1
x' \<in> X

goal (1 subgoal):
 1. pow_A_1 x' \<in> pow_A_1 ` X1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> Y

goal (1 subgoal):
 1. r x \<le> sr
[PROOF STEP]
note id
[PROOF STATE]
proof (state)
this:
r x = r x'

goal (1 subgoal):
 1. r x \<le> sr
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
r x = r x'

goal (1 subgoal):
 1. r x \<le> sr
[PROOF STEP]
have "r x' \<le> r y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r x' \<le> r y
[PROOF STEP]
using r_pow_A_1[OF x'(2)]
[PROOF STATE]
proof (prove)
using this:
r x' \<le> r (pow_A_1 x')

goal (1 subgoal):
 1. r x' \<le> r y
[PROOF STEP]
unfolding y_def
[PROOF STATE]
proof (prove)
using this:
r x' \<le> r (pow_A_1 x')

goal (1 subgoal):
 1. r x' \<le> r (pow_A_1 x')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
r x' \<le> r y

goal (1 subgoal):
 1. r x \<le> sr
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
r x' \<le> r y

goal (1 subgoal):
 1. r x \<le> sr
[PROOF STEP]
have "\<dots> \<le> r z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r y \<le> sr
[PROOF STEP]
using sr_max_Y[OF y]
[PROOF STATE]
proof (prove)
using this:
r y \<le> sr

goal (1 subgoal):
 1. r y \<le> sr
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
r y \<le> sr

goal (1 subgoal):
 1. r x \<le> sr
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
r x \<le> sr
[PROOF STEP]
show "r x \<le> r z"
[PROOF STATE]
proof (prove)
using this:
r x \<le> sr

goal (1 subgoal):
 1. r x \<le> sr
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
r x \<le> sr

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma z_pos: "z $ i > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < z $h i
[PROOF STEP]
using Y_pos[OF z(1)]
[PROOF STATE]
proof (prove)
using this:
0 < z $h ?i

goal (1 subgoal):
 1. 0 < z $h i
[PROOF STEP]
by auto


[STATEMENT]
lemma sr_pos: "sr > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < sr
[PROOF STEP]
by (rule rx_pos, insert z_pos, auto)


[STATEMENT]
lemma sr_imp_eigen_vector_main: "sr *s u = A *v u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sr *s u = A *v u
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sr *s u \<noteq> A *v u \<Longrightarrow> False
[PROOF STEP]
assume *: "sr *s u \<noteq> A *v u"
[PROOF STATE]
proof (state)
this:
sr *s u \<noteq> A *v u

goal (1 subgoal):
 1. sr *s u \<noteq> A *v u \<Longrightarrow> False
[PROOF STEP]
let ?x = "A *v u - sr *s u"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sr *s u \<noteq> A *v u \<Longrightarrow> False
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
sr *s u \<noteq> A *v u
[PROOF STEP]
have 0: "?x \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
sr *s u \<noteq> A *v u

goal (1 subgoal):
 1. A *v u - sr *s u \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A *v u - sr *s u \<noteq> 0

goal (1 subgoal):
 1. sr *s u \<noteq> A *v u \<Longrightarrow> False
[PROOF STEP]
let ?y = "pow_A_1 u"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sr *s u \<noteq> A *v u \<Longrightarrow> False
[PROOF STEP]
have "le_vec (sr *s u) (A *v u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. le_vec (sr *s u) (A *v u)
[PROOF STEP]
using rx_le_Ax[OF u]
[PROOF STATE]
proof (prove)
using this:
le_vec (r u *s u) (A *v u)

goal (1 subgoal):
 1. le_vec (sr *s u) (A *v u)
[PROOF STEP]
unfolding ru
[PROOF STATE]
proof (prove)
using this:
le_vec (sr *s u) (A *v u)

goal (1 subgoal):
 1. le_vec (sr *s u) (A *v u)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
le_vec (sr *s u) (A *v u)

goal (1 subgoal):
 1. sr *s u \<noteq> A *v u \<Longrightarrow> False
[PROOF STEP]
hence le: "le_vec 0 ?x"
[PROOF STATE]
proof (prove)
using this:
le_vec (sr *s u) (A *v u)

goal (1 subgoal):
 1. le_vec 0 (A *v u - sr *s u)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
le_vec 0 (A *v u - sr *s u)

goal (1 subgoal):
 1. sr *s u \<noteq> A *v u \<Longrightarrow> False
[PROOF STEP]
from 0 le
[PROOF STATE]
proof (chain)
picking this:
A *v u - sr *s u \<noteq> 0
le_vec 0 (A *v u - sr *s u)
[PROOF STEP]
have x: "?x \<in> X"
[PROOF STATE]
proof (prove)
using this:
A *v u - sr *s u \<noteq> 0
le_vec 0 (A *v u - sr *s u)

goal (1 subgoal):
 1. A *v u - sr *s u \<in> X
[PROOF STEP]
unfolding X_def
[PROOF STATE]
proof (prove)
using this:
A *v u - sr *s u \<noteq> 0
le_vec 0 (A *v u - sr *s u)

goal (1 subgoal):
 1. A *v u - sr *s u \<in> {x. le_vec 0 x \<and> x \<noteq> 0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A *v u - sr *s u \<in> X

goal (1 subgoal):
 1. sr *s u \<noteq> A *v u \<Longrightarrow> False
[PROOF STEP]
have y_pos: "lt_vec 0 ?y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lt_vec 0 (pow_A_1 u)
[PROOF STEP]
using Y_pos_main[of ?y] u
[PROOF STATE]
proof (prove)
using this:
pow_A_1 u \<in> pow_A_1 ` X \<Longrightarrow> 0 < pow_A_1 u $h ?i
u \<in> X

goal (1 subgoal):
 1. lt_vec 0 (pow_A_1 u)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lt_vec 0 (pow_A_1 u)

goal (1 subgoal):
 1. sr *s u \<noteq> A *v u \<Longrightarrow> False
[PROOF STEP]
hence y: "?y \<in> X"
[PROOF STATE]
proof (prove)
using this:
lt_vec 0 (pow_A_1 u)

goal (1 subgoal):
 1. pow_A_1 u \<in> X
[PROOF STEP]
unfolding X_def
[PROOF STATE]
proof (prove)
using this:
lt_vec 0 (pow_A_1 u)

goal (1 subgoal):
 1. pow_A_1 u \<in> {x. le_vec 0 x \<and> x \<noteq> 0}
[PROOF STEP]
by (auto simp: order.strict_iff_order)
[PROOF STATE]
proof (state)
this:
pow_A_1 u \<in> X

goal (1 subgoal):
 1. sr *s u \<noteq> A *v u \<Longrightarrow> False
[PROOF STEP]
from Y_pos_main[of "pow_A_1 ?x"] x
[PROOF STATE]
proof (chain)
picking this:
pow_A_1 (A *v u - sr *s u) \<in> pow_A_1 ` X \<Longrightarrow> 0 < pow_A_1 (A *v u - sr *s u) $h ?i
A *v u - sr *s u \<in> X
[PROOF STEP]
have "lt_vec 0 (pow_A_1 ?x)"
[PROOF STATE]
proof (prove)
using this:
pow_A_1 (A *v u - sr *s u) \<in> pow_A_1 ` X \<Longrightarrow> 0 < pow_A_1 (A *v u - sr *s u) $h ?i
A *v u - sr *s u \<in> X

goal (1 subgoal):
 1. lt_vec 0 (pow_A_1 (A *v u - sr *s u))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lt_vec 0 (pow_A_1 (A *v u - sr *s u))

goal (1 subgoal):
 1. sr *s u \<noteq> A *v u \<Longrightarrow> False
[PROOF STEP]
hence lt: "lt_vec (sr *s ?y) (A *v ?y)"
[PROOF STATE]
proof (prove)
using this:
lt_vec 0 (pow_A_1 (A *v u - sr *s u))

goal (1 subgoal):
 1. lt_vec (sr *s pow_A_1 u) (A *v pow_A_1 u)
[PROOF STEP]
unfolding pow_A_1_def matrix_vector_right_distrib_diff
    matrix_vector_mul_assoc A1n_commute vector_smult_distrib
[PROOF STATE]
proof (prove)
using this:
lt_vec 0 (A ** A1n *v u - sr *s (A1n *v u))

goal (1 subgoal):
 1. lt_vec (sr *s (A1n *v u)) (A ** A1n *v u)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lt_vec (sr *s pow_A_1 u) (A *v pow_A_1 u)

goal (1 subgoal):
 1. sr *s u \<noteq> A *v u \<Longrightarrow> False
[PROOF STEP]
let ?f = "(\<lambda> i. (A *v ?y - sr *s ?y) $ i / ?y $ i)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sr *s u \<noteq> A *v u \<Longrightarrow> False
[PROOF STEP]
let ?U = "UNIV :: 'n set"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sr *s u \<noteq> A *v u \<Longrightarrow> False
[PROOF STEP]
define eps where "eps = Min (?f ` ?U)"
[PROOF STATE]
proof (state)
this:
eps = (MIN i. (A *v pow_A_1 u - sr *s pow_A_1 u) $h i / pow_A_1 u $h i)

goal (1 subgoal):
 1. sr *s u \<noteq> A *v u \<Longrightarrow> False
[PROOF STEP]
have U: "finite (?f ` ?U)" "?f ` ?U \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (range (\<lambda>i. (A *v pow_A_1 u - sr *s pow_A_1 u) $h i / pow_A_1 u $h i)) &&& range (\<lambda>i. (A *v pow_A_1 u - sr *s pow_A_1 u) $h i / pow_A_1 u $h i) \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (range (\<lambda>i. (A *v pow_A_1 u - sr *s pow_A_1 u) $h i / pow_A_1 u $h i))
range (\<lambda>i. (A *v pow_A_1 u - sr *s pow_A_1 u) $h i / pow_A_1 u $h i) \<noteq> {}

goal (1 subgoal):
 1. sr *s u \<noteq> A *v u \<Longrightarrow> False
[PROOF STEP]
have eps: "eps > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < eps
[PROOF STEP]
unfolding eps_def Min_gr_iff[OF U]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ball (range (\<lambda>i. (A *v pow_A_1 u - sr *s pow_A_1 u) $h i / pow_A_1 u $h i)) ((<) 0)
[PROOF STEP]
using lt sr_pos y_pos
[PROOF STATE]
proof (prove)
using this:
lt_vec (sr *s pow_A_1 u) (A *v pow_A_1 u)
0 < sr
lt_vec 0 (pow_A_1 u)

goal (1 subgoal):
 1. Ball (range (\<lambda>i. (A *v pow_A_1 u - sr *s pow_A_1 u) $h i / pow_A_1 u $h i)) ((<) 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < eps

goal (1 subgoal):
 1. sr *s u \<noteq> A *v u \<Longrightarrow> False
[PROOF STEP]
have le: "le_vec ((sr + eps) *s ?y) (A *v ?y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. le_vec ((sr + eps) *s pow_A_1 u) (A *v pow_A_1 u)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. ((sr + eps) *s pow_A_1 u) $h i \<le> (A *v pow_A_1 u) $h i
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. ((sr + eps) *s pow_A_1 u) $h i \<le> (A *v pow_A_1 u) $h i
[PROOF STEP]
have "((sr + eps) *s ?y) $ i = sr * ?y $ i + eps * ?y $ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((sr + eps) *s pow_A_1 u) $h i = sr * pow_A_1 u $h i + eps * pow_A_1 u $h i
[PROOF STEP]
by (simp add: comm_semiring_class.distrib)
[PROOF STATE]
proof (state)
this:
((sr + eps) *s pow_A_1 u) $h i = sr * pow_A_1 u $h i + eps * pow_A_1 u $h i

goal (1 subgoal):
 1. \<And>i. ((sr + eps) *s pow_A_1 u) $h i \<le> (A *v pow_A_1 u) $h i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((sr + eps) *s pow_A_1 u) $h i = sr * pow_A_1 u $h i + eps * pow_A_1 u $h i

goal (1 subgoal):
 1. \<And>i. ((sr + eps) *s pow_A_1 u) $h i \<le> (A *v pow_A_1 u) $h i
[PROOF STEP]
have "\<dots> \<le> sr * ?y $ i + ?f i * ?y $ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sr * pow_A_1 u $h i + eps * pow_A_1 u $h i \<le> sr * pow_A_1 u $h i + (A *v pow_A_1 u - sr *s pow_A_1 u) $h i / pow_A_1 u $h i * pow_A_1 u $h i
[PROOF STEP]
proof (rule add_left_mono[OF mult_right_mono])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. eps \<le> (A *v pow_A_1 u - sr *s pow_A_1 u) $h i / pow_A_1 u $h i
 2. 0 \<le> pow_A_1 u $h i
[PROOF STEP]
show "0 \<le> ?y $ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> pow_A_1 u $h i
[PROOF STEP]
using y_pos[rule_format, of i]
[PROOF STATE]
proof (prove)
using this:
0 $h i < pow_A_1 u $h i

goal (1 subgoal):
 1. 0 \<le> pow_A_1 u $h i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> pow_A_1 u $h i

goal (1 subgoal):
 1. eps \<le> (A *v pow_A_1 u - sr *s pow_A_1 u) $h i / pow_A_1 u $h i
[PROOF STEP]
show "eps \<le> ?f i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eps \<le> (A *v pow_A_1 u - sr *s pow_A_1 u) $h i / pow_A_1 u $h i
[PROOF STEP]
unfolding eps_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (MIN i. (A *v pow_A_1 u - sr *s pow_A_1 u) $h i / pow_A_1 u $h i) \<le> (A *v pow_A_1 u - sr *s pow_A_1 u) $h i / pow_A_1 u $h i
[PROOF STEP]
by (rule Min_le, auto)
[PROOF STATE]
proof (state)
this:
eps \<le> (A *v pow_A_1 u - sr *s pow_A_1 u) $h i / pow_A_1 u $h i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sr * pow_A_1 u $h i + eps * pow_A_1 u $h i \<le> sr * pow_A_1 u $h i + (A *v pow_A_1 u - sr *s pow_A_1 u) $h i / pow_A_1 u $h i * pow_A_1 u $h i

goal (1 subgoal):
 1. \<And>i. ((sr + eps) *s pow_A_1 u) $h i \<le> (A *v pow_A_1 u) $h i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sr * pow_A_1 u $h i + eps * pow_A_1 u $h i \<le> sr * pow_A_1 u $h i + (A *v pow_A_1 u - sr *s pow_A_1 u) $h i / pow_A_1 u $h i * pow_A_1 u $h i

goal (1 subgoal):
 1. \<And>i. ((sr + eps) *s pow_A_1 u) $h i \<le> (A *v pow_A_1 u) $h i
[PROOF STEP]
have "\<dots> = (A *v ?y) $ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sr * pow_A_1 u $h i + (A *v pow_A_1 u - sr *s pow_A_1 u) $h i / pow_A_1 u $h i * pow_A_1 u $h i = (A *v pow_A_1 u) $h i
[PROOF STEP]
using sr_pos y_pos[rule_format, of i]
[PROOF STATE]
proof (prove)
using this:
0 < sr
0 $h i < pow_A_1 u $h i

goal (1 subgoal):
 1. sr * pow_A_1 u $h i + (A *v pow_A_1 u - sr *s pow_A_1 u) $h i / pow_A_1 u $h i * pow_A_1 u $h i = (A *v pow_A_1 u) $h i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sr * pow_A_1 u $h i + (A *v pow_A_1 u - sr *s pow_A_1 u) $h i / pow_A_1 u $h i * pow_A_1 u $h i = (A *v pow_A_1 u) $h i

goal (1 subgoal):
 1. \<And>i. ((sr + eps) *s pow_A_1 u) $h i \<le> (A *v pow_A_1 u) $h i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
((sr + eps) *s pow_A_1 u) $h i \<le> (A *v pow_A_1 u) $h i
[PROOF STEP]
show "((sr + eps) *s ?y) $ i \<le> (A *v ?y) $ i"
[PROOF STATE]
proof (prove)
using this:
((sr + eps) *s pow_A_1 u) $h i \<le> (A *v pow_A_1 u) $h i

goal (1 subgoal):
 1. ((sr + eps) *s pow_A_1 u) $h i \<le> (A *v pow_A_1 u) $h i
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
((sr + eps) *s pow_A_1 u) $h i \<le> (A *v pow_A_1 u) $h i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
le_vec ((sr + eps) *s pow_A_1 u) (A *v pow_A_1 u)

goal (1 subgoal):
 1. sr *s u \<noteq> A *v u \<Longrightarrow> False
[PROOF STEP]
from rho_le_x_Ax_imp_rho_le_rx[OF y le]
[PROOF STATE]
proof (chain)
picking this:
sr + eps \<le> r (pow_A_1 u)
[PROOF STEP]
have "r ?y \<ge> sr + eps"
[PROOF STATE]
proof (prove)
using this:
sr + eps \<le> r (pow_A_1 u)

goal (1 subgoal):
 1. sr + eps \<le> r (pow_A_1 u)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sr + eps \<le> r (pow_A_1 u)

goal (1 subgoal):
 1. sr *s u \<noteq> A *v u \<Longrightarrow> False
[PROOF STEP]
with sr_max[OF y] eps
[PROOF STATE]
proof (chain)
picking this:
r (pow_A_1 u) \<le> sr
0 < eps
sr + eps \<le> r (pow_A_1 u)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
r (pow_A_1 u) \<le> sr
0 < eps
sr + eps \<le> r (pow_A_1 u)

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sr_imp_eigen_vector: "eigen_vector A u sr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eigen_vector A u sr
[PROOF STEP]
unfolding eigen_vector_def sr_imp_eigen_vector_main
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<noteq> 0 \<and> A *v u = A *v u
[PROOF STEP]
using u
[PROOF STATE]
proof (prove)
using this:
u \<in> X

goal (1 subgoal):
 1. u \<noteq> 0 \<and> A *v u = A *v u
[PROOF STEP]
unfolding X_def
[PROOF STATE]
proof (prove)
using this:
u \<in> {x. le_vec 0 x \<and> x \<noteq> 0}

goal (1 subgoal):
 1. u \<noteq> 0 \<and> A *v u = A *v u
[PROOF STEP]
by auto


[STATEMENT]
lemma sr_u_pos: "lt_vec 0 u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lt_vec 0 u
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lt_vec 0 u
[PROOF STEP]
let ?y = "pow_A_1 u"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lt_vec 0 u
[PROOF STEP]
define n where "n = N"
[PROOF STATE]
proof (state)
this:
n = N

goal (1 subgoal):
 1. lt_vec 0 u
[PROOF STEP]
define c where "c = (sr + 1)^N"
[PROOF STATE]
proof (state)
this:
c = (sr + 1) ^ N

goal (1 subgoal):
 1. lt_vec 0 u
[PROOF STEP]
have c: "c > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < c
[PROOF STEP]
using sr_pos
[PROOF STATE]
proof (prove)
using this:
0 < sr

goal (1 subgoal):
 1. 0 < c
[PROOF STEP]
unfolding c_def
[PROOF STATE]
proof (prove)
using this:
0 < sr

goal (1 subgoal):
 1. 0 < (sr + 1) ^ N
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < c

goal (1 subgoal):
 1. lt_vec 0 u
[PROOF STEP]
have "lt_vec 0 ?y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lt_vec 0 (pow_A_1 u)
[PROOF STEP]
using Y_pos_main[of ?y] u
[PROOF STATE]
proof (prove)
using this:
pow_A_1 u \<in> pow_A_1 ` X \<Longrightarrow> 0 < pow_A_1 u $h ?i
u \<in> X

goal (1 subgoal):
 1. lt_vec 0 (pow_A_1 u)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lt_vec 0 (pow_A_1 u)

goal (1 subgoal):
 1. lt_vec 0 u
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lt_vec 0 (pow_A_1 u)

goal (1 subgoal):
 1. lt_vec 0 u
[PROOF STEP]
have "?y = A1n *v u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pow_A_1 u = A1n *v u
[PROOF STEP]
unfolding pow_A_1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A1n *v u = A1n *v u
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
pow_A_1 u = A1n *v u

goal (1 subgoal):
 1. lt_vec 0 u
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
pow_A_1 u = A1n *v u

goal (1 subgoal):
 1. lt_vec 0 u
[PROOF STEP]
have "\<dots> = c *s u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A1n *v u = c *s u
[PROOF STEP]
unfolding c_def A1n_def n_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matpow (A + mat 1) n *v u = (sr + 1) ^ n *s u
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. matpow (A + mat 1) 0 *v u = (sr + 1) ^ 0 *s u
 2. \<And>n. matpow (A + mat 1) n *v u = (sr + 1) ^ n *s u \<Longrightarrow> matpow (A + mat 1) (Suc n) *v u = (sr + 1) ^ Suc n *s u
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
matpow (A + mat 1) n *v u = (sr + 1) ^ n *s u

goal (2 subgoals):
 1. matpow (A + mat 1) 0 *v u = (sr + 1) ^ 0 *s u
 2. \<And>n. matpow (A + mat 1) n *v u = (sr + 1) ^ n *s u \<Longrightarrow> matpow (A + mat 1) (Suc n) *v u = (sr + 1) ^ Suc n *s u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
matpow (A + mat 1) n *v u = (sr + 1) ^ n *s u
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
matpow (A + mat 1) n *v u = (sr + 1) ^ n *s u

goal (1 subgoal):
 1. matpow (A + mat 1) (Suc n) *v u = (sr + 1) ^ Suc n *s u
[PROOF STEP]
by (simp add: matrix_vector_mul_assoc[symmetric] algebra_simps vec.scale
          sr_imp_eigen_vector_main[symmetric])
[PROOF STATE]
proof (state)
this:
matpow (A + mat 1) (Suc n) *v u = (sr + 1) ^ Suc n *s u

goal (1 subgoal):
 1. matpow (A + mat 1) 0 *v u = (sr + 1) ^ 0 *s u
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
A1n *v u = c *s u

goal (1 subgoal):
 1. lt_vec 0 u
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
lt_vec 0 (c *s u)
[PROOF STEP]
have lt: "lt_vec 0 (c *s u)"
[PROOF STATE]
proof (prove)
using this:
lt_vec 0 (c *s u)

goal (1 subgoal):
 1. lt_vec 0 (c *s u)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
lt_vec 0 (c *s u)

goal (1 subgoal):
 1. lt_vec 0 u
[PROOF STEP]
have "0 < u $ i" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < u $h i
[PROOF STEP]
using lt[rule_format, of i] c
[PROOF STATE]
proof (prove)
using this:
0 $h i < (c *s u) $h i
0 < c

goal (1 subgoal):
 1. 0 < u $h i
[PROOF STEP]
by simp (metis zero_less_mult_pos)
[PROOF STATE]
proof (state)
this:
0 < u $h ?i

goal (1 subgoal):
 1. lt_vec 0 u
[PROOF STEP]
thus "lt_vec 0 u"
[PROOF STATE]
proof (prove)
using this:
0 < u $h ?i

goal (1 subgoal):
 1. lt_vec 0 u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lt_vec 0 u

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eigen_vector_z_sr: "eigen_vector A z sr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eigen_vector A z sr
[PROOF STEP]
using sr_imp_eigen_vector[OF zX refl]
[PROOF STATE]
proof (prove)
using this:
eigen_vector A z sr

goal (1 subgoal):
 1. eigen_vector A z sr
[PROOF STEP]
by auto


[STATEMENT]
lemma eigen_value_sr: "eigen_value A sr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eigen_value A sr
[PROOF STEP]
using eigen_vector_z_sr
[PROOF STATE]
proof (prove)
using this:
eigen_vector A z sr

goal (1 subgoal):
 1. eigen_value A sr
[PROOF STEP]
unfolding eigen_value_def
[PROOF STATE]
proof (prove)
using this:
eigen_vector A z sr

goal (1 subgoal):
 1. \<exists>v. eigen_vector A v sr
[PROOF STEP]
by auto


[STATEMENT]
lemma norm_v_ge_0: "le_vec 0 (norm_v v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. le_vec 0 (map_vector cmod v)
[PROOF STEP]
by (auto simp: map_vector_def)


[STATEMENT]
lemma norm_v_eq_0: "norm_v v = 0 \<longleftrightarrow> v = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (map_vector cmod v = 0) = (v = 0)
[PROOF STEP]
by (auto simp: map_vector_def vec_eq_iff)


[STATEMENT]
lemma cA_index: "cA $ i $ j = c (A $ i $ j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cA $h i $h j = complex_of_real (A $h i $h j)
[PROOF STEP]
unfolding map_matrix_def map_vector_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>i ia. complex_of_real (A $h i $h ia)) $h i $h j = complex_of_real (A $h i $h j)
[PROOF STEP]
by simp


[STATEMENT]
lemma norm_cA[simp]: "norm (cA $ i $ j) = A $ i $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (cA $h i $h j) = A $h i $h j
[PROOF STEP]
using nonneg[of i j]
[PROOF STATE]
proof (prove)
using this:
0 \<le> A $h i $h j

goal (1 subgoal):
 1. cmod (cA $h i $h j) = A $h i $h j
[PROOF STEP]
by (simp add: cA_index)


[STATEMENT]
lemma evD: "\<alpha> *s v = cA *v v" "v \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> *s v = cA *v v &&& v \<noteq> 0
[PROOF STEP]
using ev[unfolded eigen_vector_def]
[PROOF STATE]
proof (prove)
using this:
v \<noteq> 0 \<and> cA *v v = \<alpha> *s v

goal (1 subgoal):
 1. \<alpha> *s v = cA *v v &&& v \<noteq> 0
[PROOF STEP]
by auto


[STATEMENT]
lemma ev_alpha_norm_v: "norm_v (\<alpha> *s v) = (norm \<alpha> *s norm_v v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_vector cmod (\<alpha> *s v) = cmod \<alpha> *s map_vector cmod v
[PROOF STEP]
by (auto simp: map_vector_def norm_mult vec_eq_iff)


[STATEMENT]
lemma ev_A_norm_v: "norm_v (cA *v v) $ j \<le> (A *v norm_v v) $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_vector cmod (cA *v v) $h j \<le> (A *v map_vector cmod v) $h j
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. map_vector cmod (cA *v v) $h j \<le> (A *v map_vector cmod v) $h j
[PROOF STEP]
have "norm_v (cA *v v) $ j = norm (\<Sum>i\<in>UNIV. cA $ j $ i * v $ i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_vector cmod (cA *v v) $h j = cmod (\<Sum>i\<in>UNIV. cA $h j $h i * v $h i)
[PROOF STEP]
unfolding map_vector_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>i. cmod ((cA *v v) $h i)) $h j = cmod (\<Sum>i\<in>UNIV. cA $h j $h i * v $h i)
[PROOF STEP]
by (simp add: matrix_vector_mult_def)
[PROOF STATE]
proof (state)
this:
map_vector cmod (cA *v v) $h j = cmod (\<Sum>i\<in>UNIV. cA $h j $h i * v $h i)

goal (1 subgoal):
 1. map_vector cmod (cA *v v) $h j \<le> (A *v map_vector cmod v) $h j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map_vector cmod (cA *v v) $h j = cmod (\<Sum>i\<in>UNIV. cA $h j $h i * v $h i)

goal (1 subgoal):
 1. map_vector cmod (cA *v v) $h j \<le> (A *v map_vector cmod v) $h j
[PROOF STEP]
have "\<dots> \<le> (\<Sum>i\<in>UNIV. norm (cA $ j $ i * v $ i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (\<Sum>i\<in>UNIV. cA $h j $h i * v $h i) \<le> (\<Sum>i\<in>UNIV. cmod (cA $h j $h i * v $h i))
[PROOF STEP]
by (rule norm_sum)
[PROOF STATE]
proof (state)
this:
cmod (\<Sum>i\<in>UNIV. cA $h j $h i * v $h i) \<le> (\<Sum>i\<in>UNIV. cmod (cA $h j $h i * v $h i))

goal (1 subgoal):
 1. map_vector cmod (cA *v v) $h j \<le> (A *v map_vector cmod v) $h j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cmod (\<Sum>i\<in>UNIV. cA $h j $h i * v $h i) \<le> (\<Sum>i\<in>UNIV. cmod (cA $h j $h i * v $h i))

goal (1 subgoal):
 1. map_vector cmod (cA *v v) $h j \<le> (A *v map_vector cmod v) $h j
[PROOF STEP]
have "\<dots> = (\<Sum>i\<in>UNIV. A $ j $ i * norm_v v $ i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>UNIV. cmod (cA $h j $h i * v $h i)) = (\<Sum>i\<in>UNIV. A $h j $h i * map_vector cmod v $h i)
[PROOF STEP]
by (rule sum.cong[OF refl], auto simp: norm_mult map_vector_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>UNIV. cmod (cA $h j $h i * v $h i)) = (\<Sum>i\<in>UNIV. A $h j $h i * map_vector cmod v $h i)

goal (1 subgoal):
 1. map_vector cmod (cA *v v) $h j \<le> (A *v map_vector cmod v) $h j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>UNIV. cmod (cA $h j $h i * v $h i)) = (\<Sum>i\<in>UNIV. A $h j $h i * map_vector cmod v $h i)

goal (1 subgoal):
 1. map_vector cmod (cA *v v) $h j \<le> (A *v map_vector cmod v) $h j
[PROOF STEP]
have "\<dots> = (A *v norm_v v) $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>UNIV. A $h j $h i * map_vector cmod v $h i) = (A *v map_vector cmod v) $h j
[PROOF STEP]
by (simp add: matrix_vector_mult_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>UNIV. A $h j $h i * map_vector cmod v $h i) = (A *v map_vector cmod v) $h j

goal (1 subgoal):
 1. map_vector cmod (cA *v v) $h j \<le> (A *v map_vector cmod v) $h j
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
map_vector cmod (cA *v v) $h j \<le> (A *v map_vector cmod v) $h j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
map_vector cmod (cA *v v) $h j \<le> (A *v map_vector cmod v) $h j

goal (1 subgoal):
 1. map_vector cmod (cA *v v) $h j \<le> (A *v map_vector cmod v) $h j
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
map_vector cmod (cA *v v) $h j \<le> (A *v map_vector cmod v) $h j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ev_le_vec: "le_vec (norm \<alpha> *s norm_v v) (A *v norm_v v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. le_vec (cmod \<alpha> *s map_vector cmod v) (A *v map_vector cmod v)
[PROOF STEP]
using arg_cong[OF evD(1), of norm_v, unfolded ev_alpha_norm_v] ev_A_norm_v
[PROOF STATE]
proof (prove)
using this:
cmod \<alpha> *s map_vector cmod v = map_vector cmod (cA *v v)
map_vector cmod (cA *v v) $h ?j \<le> (A *v map_vector cmod v) $h ?j

goal (1 subgoal):
 1. le_vec (cmod \<alpha> *s map_vector cmod v) (A *v map_vector cmod v)
[PROOF STEP]
by auto


[STATEMENT]
lemma norm_v_X: "norm_v v \<in> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_vector cmod v \<in> X
[PROOF STEP]
using norm_v_ge_0[of v] evD(2) norm_v_eq_0[of v]
[PROOF STATE]
proof (prove)
using this:
le_vec 0 (map_vector cmod v)
v \<noteq> 0
(map_vector cmod v = 0) = (v = 0)

goal (1 subgoal):
 1. map_vector cmod v \<in> X
[PROOF STEP]
unfolding X_def
[PROOF STATE]
proof (prove)
using this:
le_vec 0 (map_vector cmod v)
v \<noteq> 0
(map_vector cmod v = 0) = (v = 0)

goal (1 subgoal):
 1. map_vector cmod v \<in> {x. le_vec 0 x \<and> x \<noteq> 0}
[PROOF STEP]
by auto


[STATEMENT]
lemma ev_inequalities: "norm \<alpha> \<le> r (norm_v v)" "r (norm_v v) \<le> sr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod \<alpha> \<le> r (map_vector cmod v) &&& r (map_vector cmod v) \<le> sr
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cmod \<alpha> \<le> r (map_vector cmod v)
 2. r (map_vector cmod v) \<le> sr
[PROOF STEP]
have v: "norm_v v \<in> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_vector cmod v \<in> X
[PROOF STEP]
by (rule norm_v_X)
[PROOF STATE]
proof (state)
this:
map_vector cmod v \<in> X

goal (2 subgoals):
 1. cmod \<alpha> \<le> r (map_vector cmod v)
 2. r (map_vector cmod v) \<le> sr
[PROOF STEP]
from rho_le_x_Ax_imp_rho_le_rx[OF v ev_le_vec]
[PROOF STATE]
proof (chain)
picking this:
cmod \<alpha> \<le> r (map_vector cmod v)
[PROOF STEP]
show "norm \<alpha> \<le> r (norm_v v)"
[PROOF STATE]
proof (prove)
using this:
cmod \<alpha> \<le> r (map_vector cmod v)

goal (1 subgoal):
 1. cmod \<alpha> \<le> r (map_vector cmod v)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
cmod \<alpha> \<le> r (map_vector cmod v)

goal (1 subgoal):
 1. r (map_vector cmod v) \<le> sr
[PROOF STEP]
from sr_max[OF v]
[PROOF STATE]
proof (chain)
picking this:
r (map_vector cmod v) \<le> sr
[PROOF STEP]
show "r (norm_v v) \<le> sr"
[PROOF STATE]
proof (prove)
using this:
r (map_vector cmod v) \<le> sr

goal (1 subgoal):
 1. r (map_vector cmod v) \<le> sr
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
r (map_vector cmod v) \<le> sr

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eigen_vector_norm_sr: "norm \<alpha> \<le> sr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod \<alpha> \<le> sr
[PROOF STEP]
using ev_inequalities
[PROOF STATE]
proof (prove)
using this:
cmod \<alpha> \<le> r (map_vector cmod v)
r (map_vector cmod v) \<le> sr

goal (1 subgoal):
 1. cmod \<alpha> \<le> sr
[PROOF STEP]
by auto


[STATEMENT]
lemma eigen_value_norm_sr: assumes "eigen_value cA \<alpha>"
  shows "norm \<alpha> \<le> sr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod \<alpha> \<le> sr
[PROOF STEP]
using eigen_vector_norm_sr[of _ \<alpha>] assms
[PROOF STATE]
proof (prove)
using this:
eigen_vector cA ?v \<alpha> \<Longrightarrow> cmod \<alpha> \<le> sr
eigen_value cA \<alpha>

goal (1 subgoal):
 1. cmod \<alpha> \<le> sr
[PROOF STEP]
unfolding eigen_value_def
[PROOF STATE]
proof (prove)
using this:
eigen_vector cA ?v \<alpha> \<Longrightarrow> cmod \<alpha> \<le> sr
\<exists>v. eigen_vector cA v \<alpha>

goal (1 subgoal):
 1. cmod \<alpha> \<le> sr
[PROOF STEP]
by auto


[STATEMENT]
lemma eigen_vector_z_sr_c: "eigen_vector cA (map_vector c z) (c sr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eigen_vector cA (map_vector complex_of_real z) (complex_of_real sr)
[PROOF STEP]
unfolding of_real_hom.eigen_vector_hom
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eigen_vector A z sr
[PROOF STEP]
by (rule eigen_vector_z_sr)


[STATEMENT]
lemma eigen_value_sr_c: "eigen_value cA (c sr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eigen_value cA (complex_of_real sr)
[PROOF STEP]
using eigen_vector_z_sr_c
[PROOF STATE]
proof (prove)
using this:
eigen_vector cA (map_vector complex_of_real z) (complex_of_real sr)

goal (1 subgoal):
 1. eigen_value cA (complex_of_real sr)
[PROOF STEP]
unfolding eigen_value_def
[PROOF STATE]
proof (prove)
using this:
eigen_vector cA (map_vector complex_of_real z) (complex_of_real sr)

goal (1 subgoal):
 1. \<exists>v. eigen_vector cA v (complex_of_real sr)
[PROOF STEP]
by auto


[STATEMENT]
lemma w: "transpose A *v w = sr *s w" "lt_vec 0 w" "perron_frobenius.sr (transpose A) = sr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Finite_Cartesian_Product.transpose A *v w = sr *s w &&& lt_vec 0 w &&& perron_frobenius.r (Finite_Cartesian_Product.transpose A) (perron_frobenius.z (Finite_Cartesian_Product.transpose A)) = sr
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. Finite_Cartesian_Product.transpose A *v w = sr *s w
 2. lt_vec 0 w
 3. perron_frobenius.r (Finite_Cartesian_Product.transpose A) (perron_frobenius.z (Finite_Cartesian_Product.transpose A)) = sr
[PROOF STEP]
interpret t: perron_frobenius "transpose A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. perron_frobenius (Finite_Cartesian_Product.transpose A)
[PROOF STEP]
by (rule pf_transpose)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. Finite_Cartesian_Product.transpose A *v w = sr *s w
 2. t.lt_vec 0 w
 3. t.sr = sr
[PROOF STEP]
from eigen_vector_z_sr_c t.eigen_vector_z_sr_c
[PROOF STATE]
proof (chain)
picking this:
eigen_vector cA (map_vector complex_of_real z) (complex_of_real sr)
eigen_vector t.cA (map_vector complex_of_real t.z) (complex_of_real t.sr)
[PROOF STEP]
have ev: "eigen_value cA (c sr)" "eigen_value t.cA (c t.sr)"
[PROOF STATE]
proof (prove)
using this:
eigen_vector cA (map_vector complex_of_real z) (complex_of_real sr)
eigen_vector t.cA (map_vector complex_of_real t.z) (complex_of_real t.sr)

goal (1 subgoal):
 1. eigen_value cA (complex_of_real sr) &&& eigen_value t.cA (complex_of_real t.sr)
[PROOF STEP]
unfolding eigen_value_def
[PROOF STATE]
proof (prove)
using this:
eigen_vector cA (map_vector complex_of_real z) (complex_of_real sr)
eigen_vector t.cA (map_vector complex_of_real t.z) (complex_of_real t.sr)

goal (1 subgoal):
 1. \<exists>v. eigen_vector cA v (complex_of_real sr) &&& \<exists>v. eigen_vector t.cA v (complex_of_real t.sr)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eigen_value cA (complex_of_real sr)
eigen_value t.cA (complex_of_real t.sr)

goal (3 subgoals):
 1. Finite_Cartesian_Product.transpose A *v w = sr *s w
 2. t.lt_vec 0 w
 3. t.sr = sr
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
eigen_value cA (complex_of_real sr)
eigen_value t.cA (complex_of_real t.sr)

goal (3 subgoals):
 1. Finite_Cartesian_Product.transpose A *v w = sr *s w
 2. t.lt_vec 0 w
 3. t.sr = sr
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. Finite_Cartesian_Product.transpose A *v w = sr *s w
 2. t.lt_vec 0 w
 3. t.sr = sr
[PROOF STEP]
have "eigen_value (t.cA) x = eigen_value (transpose cA) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eigen_value t.cA x = eigen_value (Finite_Cartesian_Product.transpose cA) x
[PROOF STEP]
unfolding map_matrix_def map_vector_def transpose_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eigen_value (\<chi>i ia. complex_of_real ((\<chi>i j. A $h j $h i) $h i $h ia)) x = eigen_value (\<chi>i j. (\<chi>i ia. complex_of_real (A $h i $h ia)) $h j $h i) x
[PROOF STEP]
by (auto simp: vec_eq_iff)
[PROOF STATE]
proof (state)
this:
eigen_value t.cA x = eigen_value (Finite_Cartesian_Product.transpose cA) x

goal (3 subgoals):
 1. Finite_Cartesian_Product.transpose A *v w = sr *s w
 2. t.lt_vec 0 w
 3. t.sr = sr
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
eigen_value t.cA x = eigen_value (Finite_Cartesian_Product.transpose cA) x

goal (3 subgoals):
 1. Finite_Cartesian_Product.transpose A *v w = sr *s w
 2. t.lt_vec 0 w
 3. t.sr = sr
[PROOF STEP]
have "\<dots> = eigen_value cA x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eigen_value (Finite_Cartesian_Product.transpose cA) x = eigen_value cA x
[PROOF STEP]
by (rule eigen_value_transpose)
[PROOF STATE]
proof (state)
this:
eigen_value (Finite_Cartesian_Product.transpose cA) x = eigen_value cA x

goal (3 subgoals):
 1. Finite_Cartesian_Product.transpose A *v w = sr *s w
 2. t.lt_vec 0 w
 3. t.sr = sr
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
eigen_value t.cA x = eigen_value cA x
[PROOF STEP]
have "eigen_value (t.cA) x = eigen_value cA x"
[PROOF STATE]
proof (prove)
using this:
eigen_value t.cA x = eigen_value cA x

goal (1 subgoal):
 1. eigen_value t.cA x = eigen_value cA x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
eigen_value t.cA x = eigen_value cA x

goal (3 subgoals):
 1. Finite_Cartesian_Product.transpose A *v w = sr *s w
 2. t.lt_vec 0 w
 3. t.sr = sr
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
eigen_value t.cA ?x2 = eigen_value cA ?x2

goal (3 subgoals):
 1. Finite_Cartesian_Product.transpose A *v w = sr *s w
 2. t.lt_vec 0 w
 3. t.sr = sr
[PROOF STEP]
note ev_id = this
[PROOF STATE]
proof (state)
this:
eigen_value t.cA ?x2 = eigen_value cA ?x2

goal (3 subgoals):
 1. Finite_Cartesian_Product.transpose A *v w = sr *s w
 2. t.lt_vec 0 w
 3. t.sr = sr
[PROOF STEP]
with ev
[PROOF STATE]
proof (chain)
picking this:
eigen_value cA (complex_of_real sr)
eigen_value t.cA (complex_of_real t.sr)
eigen_value t.cA ?x2 = eigen_value cA ?x2
[PROOF STEP]
have ev: "eigen_value t.cA (c sr)" "eigen_value cA (c t.sr)"
[PROOF STATE]
proof (prove)
using this:
eigen_value cA (complex_of_real sr)
eigen_value t.cA (complex_of_real t.sr)
eigen_value t.cA ?x2 = eigen_value cA ?x2

goal (1 subgoal):
 1. eigen_value t.cA (complex_of_real sr) &&& eigen_value cA (complex_of_real t.sr)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eigen_value t.cA (complex_of_real sr)
eigen_value cA (complex_of_real t.sr)

goal (3 subgoals):
 1. Finite_Cartesian_Product.transpose A *v w = sr *s w
 2. t.lt_vec 0 w
 3. t.sr = sr
[PROOF STEP]
from eigen_value_norm_sr[OF ev(2)] t.eigen_value_norm_sr[OF ev(1)]
[PROOF STATE]
proof (chain)
picking this:
cmod (complex_of_real t.sr) \<le> sr
cmod (complex_of_real sr) \<le> t.sr
[PROOF STEP]
show id: "t.sr = sr"
[PROOF STATE]
proof (prove)
using this:
cmod (complex_of_real t.sr) \<le> sr
cmod (complex_of_real sr) \<le> t.sr

goal (1 subgoal):
 1. t.sr = sr
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t.sr = sr

goal (2 subgoals):
 1. Finite_Cartesian_Product.transpose A *v w = sr *s w
 2. t.lt_vec 0 w
[PROOF STEP]
from t.eigen_vector_z_sr[unfolded id, folded w_def]
[PROOF STATE]
proof (chain)
picking this:
eigen_vector (Finite_Cartesian_Product.transpose A) w sr
[PROOF STEP]
show "transpose A *v w = sr *s w"
[PROOF STATE]
proof (prove)
using this:
eigen_vector (Finite_Cartesian_Product.transpose A) w sr

goal (1 subgoal):
 1. Finite_Cartesian_Product.transpose A *v w = sr *s w
[PROOF STEP]
unfolding eigen_vector_def
[PROOF STATE]
proof (prove)
using this:
w \<noteq> 0 \<and> Finite_Cartesian_Product.transpose A *v w = sr *s w

goal (1 subgoal):
 1. Finite_Cartesian_Product.transpose A *v w = sr *s w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Finite_Cartesian_Product.transpose A *v w = sr *s w

goal (1 subgoal):
 1. t.lt_vec 0 w
[PROOF STEP]
from t.z_pos[folded w_def]
[PROOF STATE]
proof (chain)
picking this:
0 < w $h ?i
[PROOF STEP]
show "lt_vec 0 w"
[PROOF STATE]
proof (prove)
using this:
0 < w $h ?i

goal (1 subgoal):
 1. t.lt_vec 0 w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t.lt_vec 0 w

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma c_cmod_id: "a \<in> \<real> \<Longrightarrow> Re a \<ge> 0 \<Longrightarrow> c (cmod a) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> \<real>; 0 \<le> Re a\<rbrakk> \<Longrightarrow> complex_of_real (cmod a) = a
[PROOF STEP]
by (auto simp: Reals_def)