[STATEMENT]
lemma pos_rowvector_mult_0: assumes lt: "lt_vec 0 x"
  and 0: "(rowvector x :: real ^ 'n ^ 'n) *v y = 0" (is "?x *v _ = 0") and le: "le_vec 0 y"
shows "y = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y = 0
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y = 0
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y = 0
[PROOF STEP]
assume "y $ i \<noteq> 0"
[PROOF STATE]
proof (state)
this:
y $h i \<noteq> 0

goal (1 subgoal):
 1. y = 0
[PROOF STEP]
with le
[PROOF STATE]
proof (chain)
picking this:
le_vec 0 y
y $h i \<noteq> 0
[PROOF STEP]
have yi: "y $ i > 0"
[PROOF STATE]
proof (prove)
using this:
le_vec 0 y
y $h i \<noteq> 0

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

goal (1 subgoal):
 1. y = 0
[PROOF STEP]
have "0 = (?x *v y) $ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 = (rowvector x *v y) $h i
[PROOF STEP]
unfolding 0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 = 0 $h i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 = (rowvector x *v y) $h i

goal (1 subgoal):
 1. y = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 = (rowvector x *v y) $h i

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

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

goal (1 subgoal):
 1. y = 0
[PROOF STEP]
have "\<dots> > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < (\<Sum>j\<in>UNIV. x $h j * y $h j)
[PROOF STEP]
by (rule sum_pos2[of _ i], insert yi lt le, auto intro!: mult_nonneg_nonneg
        simp: order.strict_iff_order)
[PROOF STATE]
proof (state)
this:
0 < (\<Sum>j\<in>UNIV. x $h j * y $h j)

goal (1 subgoal):
 1. y = 0
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
0 < 0
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
0 < 0

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

goal (1 subgoal):
 1. y = 0
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
y $h ?i2 \<noteq> 0 \<Longrightarrow> False

goal (1 subgoal):
 1. y = 0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
y $h ?i2 \<noteq> 0 \<Longrightarrow> False

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pos_matrix_mult_0: assumes le: "\<And> i j. B $ i $ j \<ge> 0"
  and lt: "lt_vec 0 x"
  and 0: "B *v x = 0"
shows "B = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. B = 0
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. B = 0
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. B = 0
[PROOF STEP]
assume "B $ i $ j \<noteq> 0"
[PROOF STATE]
proof (state)
this:
B $h i $h j \<noteq> 0

goal (1 subgoal):
 1. B = 0
[PROOF STEP]
with le
[PROOF STATE]
proof (chain)
picking this:
0 \<le> B $h ?i $h ?j
B $h i $h j \<noteq> 0
[PROOF STEP]
have gt: "B $ i $ j > 0"
[PROOF STATE]
proof (prove)
using this:
0 \<le> B $h ?i $h ?j
B $h i $h j \<noteq> 0

goal (1 subgoal):
 1. 0 < B $h i $h j
[PROOF STEP]
by (auto simp: order.strict_iff_order)
[PROOF STATE]
proof (state)
this:
0 < B $h i $h j

goal (1 subgoal):
 1. B = 0
[PROOF STEP]
have "0 = (B *v x) $ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 = (B *v x) $h i
[PROOF STEP]
unfolding 0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 = 0 $h i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 = (B *v x) $h i

goal (1 subgoal):
 1. B = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 = (B *v x) $h i

goal (1 subgoal):
 1. B = 0
[PROOF STEP]
have "\<dots> = (\<Sum>j\<in>UNIV. B $ i $ j * x $ j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (B *v x) $h i = (\<Sum>j\<in>UNIV. B $h i $h j * x $h j)
[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 = (\<Sum>j\<in>UNIV. B $h i $h j * x $h j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(B *v x) $h i = (\<Sum>j\<in>UNIV. B $h i $h j * x $h j)

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

goal (1 subgoal):
 1. B = 0
[PROOF STEP]
have "\<dots> > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < (\<Sum>j\<in>UNIV. B $h i $h j * x $h j)
[PROOF STEP]
by (rule sum_pos2[of _ j], insert gt lt le, auto intro!: mult_nonneg_nonneg
        simp: order.strict_iff_order)
[PROOF STATE]
proof (state)
this:
0 < (\<Sum>j\<in>UNIV. B $h i $h j * x $h j)

goal (1 subgoal):
 1. B = 0
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
0 < 0
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
0 < 0

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

goal (1 subgoal):
 1. B = 0
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
B $h ?i2 $h ?j2 \<noteq> 0 \<Longrightarrow> False

goal (1 subgoal):
 1. B = 0
[PROOF STEP]
thus "B = 0"
[PROOF STATE]
proof (prove)
using this:
B $h ?i2 $h ?j2 \<noteq> 0 \<Longrightarrow> False

goal (1 subgoal):
 1. B = 0
[PROOF STEP]
unfolding vec_eq_iff
[PROOF STATE]
proof (prove)
using this:
B $h ?i2 $h ?j2 \<noteq> 0 \<Longrightarrow> False

goal (1 subgoal):
 1. \<forall>i ia. B $h i $h ia = 0 $h i $h ia
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eigen_value_smaller_matrix: assumes B: "\<And> i j. 0 \<le> B $ i $ j \<and> B $ i $ j \<le> A $ i $ j"
  and AB: "A \<noteq> B"
  and ev: "eigen_value (map_matrix c B) sigma"
shows "cmod sigma < sr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod sigma < sr
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cmod sigma < sr
[PROOF STEP]
let ?B = "map_matrix c B"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cmod sigma < sr
[PROOF STEP]
let ?sr = "spectral_radius ?B"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cmod sigma < sr
[PROOF STEP]
define \<sigma> where "\<sigma> = ?sr"
[PROOF STATE]
proof (state)
this:
\<sigma> = HMA_Connect.spectral_radius (HMA_Connect.map_matrix complex_of_real B)

goal (1 subgoal):
 1. cmod sigma < sr
[PROOF STEP]
have "real_non_neg_mat ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_non_neg_mat (HMA_Connect.map_matrix complex_of_real B)
[PROOF STEP]
unfolding real_non_neg_mat_def elements_mat_h_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a\<in>range (\<lambda>(i, y). HMA_Connect.map_matrix complex_of_real B $h i $h y). a \<in> \<real> \<and> 0 \<le> Re a
[PROOF STEP]
by (auto simp: map_matrix_def map_vector_def B)
[PROOF STATE]
proof (state)
this:
real_non_neg_mat (HMA_Connect.map_matrix complex_of_real B)

goal (1 subgoal):
 1. cmod sigma < sr
[PROOF STEP]
from perron_frobenius[OF this, folded \<sigma>_def]
[PROOF STATE]
proof (chain)
picking this:
\<exists>v. eigen_vector (HMA_Connect.map_matrix complex_of_real B) v (complex_of_real \<sigma>) \<and> real_non_neg_vec v
[PROOF STEP]
obtain x where ev_sr: "eigen_vector ?B x (c \<sigma>)"
    and rnn: "real_non_neg_vec x"
[PROOF STATE]
proof (prove)
using this:
\<exists>v. eigen_vector (HMA_Connect.map_matrix complex_of_real B) v (complex_of_real \<sigma>) \<and> real_non_neg_vec v

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>eigen_vector (HMA_Connect.map_matrix complex_of_real B) x (complex_of_real \<sigma>); real_non_neg_vec x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eigen_vector (HMA_Connect.map_matrix complex_of_real B) x (complex_of_real \<sigma>)
real_non_neg_vec x

goal (1 subgoal):
 1. cmod sigma < sr
[PROOF STEP]
define y where "y = norm_v x"
[PROOF STATE]
proof (state)
this:
y = map_vector cmod x

goal (1 subgoal):
 1. cmod sigma < sr
[PROOF STEP]
from rnn
[PROOF STATE]
proof (chain)
picking this:
real_non_neg_vec x
[PROOF STEP]
have xy: "x = map_vector c y"
[PROOF STATE]
proof (prove)
using this:
real_non_neg_vec x

goal (1 subgoal):
 1. x = map_vector complex_of_real y
[PROOF STEP]
unfolding real_non_neg_vec_def vec_elements_h_def y_def
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>range (($h) x). a \<in> \<real> \<and> 0 \<le> Re a

goal (1 subgoal):
 1. x = map_vector complex_of_real (map_vector cmod x)
[PROOF STEP]
by (auto simp: map_vector_def vec_eq_iff c_cmod_id)
[PROOF STATE]
proof (state)
this:
x = map_vector complex_of_real y

goal (1 subgoal):
 1. cmod sigma < sr
[PROOF STEP]
from spectral_radius_max[OF ev, folded \<sigma>_def]
[PROOF STATE]
proof (chain)
picking this:
cmod sigma \<le> \<sigma>
[PROOF STEP]
have sigma_sigma: "cmod sigma \<le> \<sigma>"
[PROOF STATE]
proof (prove)
using this:
cmod sigma \<le> \<sigma>

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

goal (1 subgoal):
 1. cmod sigma < sr
[PROOF STEP]
from ev_sr[unfolded xy of_real_hom.eigen_vector_hom]
[PROOF STATE]
proof (chain)
picking this:
eigen_vector B y \<sigma>
[PROOF STEP]
have ev_B: "eigen_vector B y \<sigma>"
[PROOF STATE]
proof (prove)
using this:
eigen_vector B y \<sigma>

goal (1 subgoal):
 1. eigen_vector B y \<sigma>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
eigen_vector B y \<sigma>

goal (1 subgoal):
 1. cmod sigma < sr
[PROOF STEP]
from ev_B[unfolded eigen_vector_def]
[PROOF STATE]
proof (chain)
picking this:
y \<noteq> 0 \<and> B *v y = \<sigma> *s y
[PROOF STEP]
have ev_B': "B *v y = \<sigma> *s y"
[PROOF STATE]
proof (prove)
using this:
y \<noteq> 0 \<and> B *v y = \<sigma> *s y

goal (1 subgoal):
 1. B *v y = \<sigma> *s y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B *v y = \<sigma> *s y

goal (1 subgoal):
 1. cmod sigma < sr
[PROOF STEP]
have ypos: "y $ i \<ge> 0" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> y $h i
[PROOF STEP]
unfolding y_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> map_vector cmod x $h i
[PROOF STEP]
by (auto simp: map_vector_def)
[PROOF STATE]
proof (state)
this:
0 \<le> y $h ?i

goal (1 subgoal):
 1. cmod sigma < sr
[PROOF STEP]
from ev_B this
[PROOF STATE]
proof (chain)
picking this:
eigen_vector B y \<sigma>
0 \<le> y $h ?i
[PROOF STEP]
have y: "y \<in> X"
[PROOF STATE]
proof (prove)
using this:
eigen_vector B y \<sigma>
0 \<le> y $h ?i

goal (1 subgoal):
 1. y \<in> X
[PROOF STEP]
unfolding eigen_vector_def X_def
[PROOF STATE]
proof (prove)
using this:
y \<noteq> 0 \<and> B *v y = \<sigma> *s y
0 \<le> y $h ?i

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

goal (1 subgoal):
 1. cmod sigma < sr
[PROOF STEP]
have BA: "(B *v y) $ i \<le> (A *v y) $ i" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (B *v y) $h i \<le> (A *v y) $h i
[PROOF STEP]
unfolding matrix_vector_mult_def vec_lambda_beta
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j\<in>UNIV. B $h i $h j * y $h j) \<le> (\<Sum>j\<in>UNIV. A $h i $h j * y $h j)
[PROOF STEP]
by (rule sum_mono, rule mult_right_mono, insert B ypos, auto)
[PROOF STATE]
proof (state)
this:
(B *v y) $h ?i \<le> (A *v y) $h ?i

goal (1 subgoal):
 1. cmod sigma < sr
[PROOF STEP]
hence le_vec: "le_vec (\<sigma> *s y) (A *v y)"
[PROOF STATE]
proof (prove)
using this:
(B *v y) $h ?i \<le> (A *v y) $h ?i

goal (1 subgoal):
 1. le_vec (\<sigma> *s y) (A *v y)
[PROOF STEP]
unfolding ev_B'
[PROOF STATE]
proof (prove)
using this:
(\<sigma> *s y) $h ?i \<le> (A *v y) $h ?i

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

goal (1 subgoal):
 1. cmod sigma < sr
[PROOF STEP]
from rho_le_x_Ax_imp_rho_le_rx[OF y le_vec]
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<le> r y
[PROOF STEP]
have "\<sigma> \<le> r y"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<le> r y

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

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

goal (1 subgoal):
 1. cmod sigma < sr
[PROOF STEP]
have "\<dots> \<le> sr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r y \<le> sr
[PROOF STEP]
using y
[PROOF STATE]
proof (prove)
using this:
y \<in> X

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

goal (1 subgoal):
 1. cmod sigma < sr
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<le> sr
[PROOF STEP]
have sig_le_sr: "\<sigma> \<le> sr"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<le> sr

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

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

goal (1 subgoal):
 1. cmod sigma < sr
[PROOF STEP]
assume "\<sigma> = sr"
[PROOF STATE]
proof (state)
this:
\<sigma> = sr

goal (1 subgoal):
 1. cmod sigma < sr
[PROOF STEP]
hence r_sr: "r y = sr" and sr_sig: "sr = \<sigma>"
[PROOF STATE]
proof (prove)
using this:
\<sigma> = sr

goal (1 subgoal):
 1. r y = sr &&& sr = \<sigma>
[PROOF STEP]
using \<open>\<sigma> \<le> r y\<close> \<open>r y \<le> sr\<close>
[PROOF STATE]
proof (prove)
using this:
\<sigma> = sr
\<sigma> \<le> r y
r y \<le> sr

goal (1 subgoal):
 1. r y = sr &&& sr = \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r y = sr
sr = \<sigma>

goal (1 subgoal):
 1. cmod sigma < sr
[PROOF STEP]
from sr_u_pos[OF y r_sr]
[PROOF STATE]
proof (chain)
picking this:
lt_vec 0 y
[PROOF STEP]
have pos: "lt_vec 0 y"
[PROOF STATE]
proof (prove)
using this:
lt_vec 0 y

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

goal (1 subgoal):
 1. cmod sigma < sr
[PROOF STEP]
from sr_imp_eigen_vector[OF y r_sr]
[PROOF STATE]
proof (chain)
picking this:
eigen_vector A y sr
[PROOF STEP]
have ev': "eigen_vector A y sr"
[PROOF STATE]
proof (prove)
using this:
eigen_vector A y sr

goal (1 subgoal):
 1. eigen_vector A y sr
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
eigen_vector A y sr

goal (1 subgoal):
 1. cmod sigma < sr
[PROOF STEP]
have "(A - B) *v y = A *v y - B *v y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A - B) *v y = A *v y - B *v y
[PROOF STEP]
unfolding matrix_vector_mult_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>i. \<Sum>j\<in>UNIV. (A - B) $h i $h j * y $h j) = (\<chi>i. \<Sum>j\<in>UNIV. A $h i $h j * y $h j) - (\<chi>i. \<Sum>j\<in>UNIV. B $h i $h j * y $h j)
[PROOF STEP]
by (auto simp: vec_eq_iff field_simps sum_subtractf)
[PROOF STATE]
proof (state)
this:
(A - B) *v y = A *v y - B *v y

goal (1 subgoal):
 1. cmod sigma < sr
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(A - B) *v y = A *v y - B *v y

goal (1 subgoal):
 1. cmod sigma < sr
[PROOF STEP]
have "A *v y = sr *s y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *v y = sr *s y
[PROOF STEP]
using ev'[unfolded eigen_vector_def]
[PROOF STATE]
proof (prove)
using this:
y \<noteq> 0 \<and> A *v y = sr *s y

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

goal (1 subgoal):
 1. cmod sigma < sr
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
A *v y = sr *s y

goal (1 subgoal):
 1. cmod sigma < sr
[PROOF STEP]
have "B *v y = sr *s y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B *v y = sr *s y
[PROOF STEP]
unfolding ev_B' sr_sig
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> *s y = \<sigma> *s y
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
B *v y = sr *s y

goal (1 subgoal):
 1. cmod sigma < sr
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(A - B) *v y = sr *s y - sr *s y
[PROOF STEP]
have id: "(A - B) *v y = 0"
[PROOF STATE]
proof (prove)
using this:
(A - B) *v y = sr *s y - sr *s y

goal (1 subgoal):
 1. (A - B) *v y = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(A - B) *v y = 0

goal (1 subgoal):
 1. cmod sigma < sr
[PROOF STEP]
from pos_matrix_mult_0[OF _ pos id] assms(1-2)
[PROOF STATE]
proof (chain)
picking this:
(\<And>i j. 0 \<le> (A - B) $h i $h j) \<Longrightarrow> A - B = 0
0 \<le> B $h ?i $h ?j \<and> B $h ?i $h ?j \<le> A $h ?i $h ?j
A \<noteq> B
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
(\<And>i j. 0 \<le> (A - B) $h i $h j) \<Longrightarrow> A - B = 0
0 \<le> B $h ?i $h ?j \<and> B $h ?i $h ?j \<le> A $h ?i $h ?j
A \<noteq> B

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

goal (1 subgoal):
 1. cmod sigma < sr
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<sigma> = sr \<Longrightarrow> False

goal (1 subgoal):
 1. cmod sigma < sr
[PROOF STEP]
with sig_le_sr sigma_sigma
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<le> sr
cmod sigma \<le> \<sigma>
\<sigma> = sr \<Longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<le> sr
cmod sigma \<le> \<sigma>
\<sigma> = sr \<Longrightarrow> False

goal (1 subgoal):
 1. cmod sigma < sr
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
cmod sigma < sr

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma charpoly_erase_mat_sr: "0 < poly (charpoly (erase_mat A i i)) sr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
let ?A = "erase_mat A i i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
let ?pos = "poly (charpoly ?A) sr"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
from A_nonzero_fixed_j[of i]
[PROOF STATE]
proof (chain)
picking this:
\<exists>ia. A $h ia $h i \<noteq> 0
[PROOF STEP]
obtain k where "A $ k $ i \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>ia. A $h ia $h i \<noteq> 0

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

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
assume "A = ?A"
[PROOF STATE]
proof (state)
this:
A = erase_mat A i i

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
hence "A $ k $ i = ?A $ k $ i"
[PROOF STATE]
proof (prove)
using this:
A = erase_mat A i i

goal (1 subgoal):
 1. A $h k $h i = erase_mat A i i $h k $h i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A $h k $h i = erase_mat A i i $h k $h i

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
A $h k $h i = erase_mat A i i $h k $h i

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
have "?A $ k $ i = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. erase_mat A i i $h k $h i = 0
[PROOF STEP]
by (auto simp: erase_mat_def)
[PROOF STATE]
proof (state)
this:
erase_mat A i i $h k $h i = 0

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
erase_mat A i i $h k $h i = 0

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
have "A $ k $ i \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $h k $h i \<noteq> 0
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
A $h k $h i \<noteq> 0

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
A $h k $h i \<noteq> A $h k $h i
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
A $h k $h i \<noteq> A $h k $h i

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

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
A = erase_mat A i i \<Longrightarrow> False

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
hence AA: "A \<noteq> ?A"
[PROOF STATE]
proof (prove)
using this:
A = erase_mat A i i \<Longrightarrow> False

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

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
have le: "0 \<le> ?A $ i $ j \<and> ?A $ i $ j \<le> A $ i $ j" for i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> erase_mat A i i $h i $h j \<and> erase_mat A i i $h i $h j \<le> A $h i $h j
[PROOF STEP]
by (auto simp: erase_mat_def nonneg)
[PROOF STATE]
proof (state)
this:
0 \<le> erase_mat A i i $h ?i $h ?j \<and> erase_mat A i i $h ?i $h ?j \<le> A $h ?i $h ?j

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
note ev_small = eigen_value_smaller_matrix[OF le AA]
[PROOF STATE]
proof (state)
this:
eigen_value (HMA_Connect.map_matrix complex_of_real (erase_mat A i i)) ?sigma \<Longrightarrow> cmod ?sigma < sr

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
eigen_value (HMA_Connect.map_matrix complex_of_real (erase_mat A i i)) ?sigma \<Longrightarrow> cmod ?sigma < sr

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
fix rho :: real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
assume "eigen_value ?A rho"
[PROOF STATE]
proof (state)
this:
eigen_value (erase_mat A i i) rho

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
hence ev: "eigen_value (map_matrix c ?A) (c rho)"
[PROOF STATE]
proof (prove)
using this:
eigen_value (erase_mat A i i) rho

goal (1 subgoal):
 1. eigen_value (HMA_Connect.map_matrix complex_of_real (erase_mat A i i)) (complex_of_real rho)
[PROOF STEP]
unfolding eigen_value_def
[PROOF STATE]
proof (prove)
using this:
\<exists>v. eigen_vector (erase_mat A i i) v rho

goal (1 subgoal):
 1. \<exists>v. eigen_vector (HMA_Connect.map_matrix complex_of_real (erase_mat A i i)) v (complex_of_real rho)
[PROOF STEP]
using of_real_hom.eigen_vector_hom[of ?A _ rho]
[PROOF STATE]
proof (prove)
using this:
\<exists>v. eigen_vector (erase_mat A i i) v rho
eigen_vector (HMA_Connect.map_matrix of_real (erase_mat A i i)) (map_vector of_real ?v) (of_real rho) = eigen_vector (erase_mat A i i) ?v rho

goal (1 subgoal):
 1. \<exists>v. eigen_vector (HMA_Connect.map_matrix complex_of_real (erase_mat A i i)) v (complex_of_real rho)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eigen_value (HMA_Connect.map_matrix complex_of_real (erase_mat A i i)) (complex_of_real rho)

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
from ev_small[OF this]
[PROOF STATE]
proof (chain)
picking this:
cmod (complex_of_real rho) < sr
[PROOF STEP]
have "abs rho < sr"
[PROOF STATE]
proof (prove)
using this:
cmod (complex_of_real rho) < sr

goal (1 subgoal):
 1. \<bar>rho\<bar> < sr
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>rho\<bar> < sr

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
eigen_value (erase_mat A i i) ?rho2 \<Longrightarrow> \<bar>?rho2\<bar> < sr

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
note ev_small_real = this
[PROOF STATE]
proof (state)
this:
eigen_value (erase_mat A i i) ?rho2 \<Longrightarrow> \<bar>?rho2\<bar> < sr

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
have pos0: "?pos \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly (charpoly (erase_mat A i i)) sr \<noteq> 0
[PROOF STEP]
using ev_small_real[of sr]
[PROOF STATE]
proof (prove)
using this:
eigen_value (erase_mat A i i) sr \<Longrightarrow> \<bar>sr\<bar> < sr

goal (1 subgoal):
 1. poly (charpoly (erase_mat A i i)) sr \<noteq> 0
[PROOF STEP]
by (auto simp: eigen_value_root_charpoly)
[PROOF STATE]
proof (state)
this:
poly (charpoly (erase_mat A i i)) sr \<noteq> 0

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
poly (charpoly (erase_mat A i i)) sr \<noteq> 0

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
define p where "p = charpoly ?A"
[PROOF STATE]
proof (state)
this:
p = charpoly (erase_mat A i i)

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
assume pos: "?pos < 0"
[PROOF STATE]
proof (state)
this:
poly (charpoly (erase_mat A i i)) sr < 0

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
hence neg: "poly p sr < 0"
[PROOF STATE]
proof (prove)
using this:
poly (charpoly (erase_mat A i i)) sr < 0

goal (1 subgoal):
 1. poly p sr < 0
[PROOF STEP]
unfolding p_def
[PROOF STATE]
proof (prove)
using this:
poly (charpoly (erase_mat A i i)) sr < 0

goal (1 subgoal):
 1. poly (charpoly (erase_mat A i i)) sr < 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poly p sr < 0

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
from degree_monic_charpoly[of ?A]
[PROOF STATE]
proof (chain)
picking this:
degree (charpoly (erase_mat A i i)) = CARD('n) \<and> monic (charpoly (erase_mat A i i))
[PROOF STEP]
have mon: "monic p" and deg: "degree p \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
degree (charpoly (erase_mat A i i)) = CARD('n) \<and> monic (charpoly (erase_mat A i i))

goal (1 subgoal):
 1. monic p &&& degree p \<noteq> 0
[PROOF STEP]
unfolding p_def
[PROOF STATE]
proof (prove)
using this:
degree (charpoly (erase_mat A i i)) = CARD('n) \<and> monic (charpoly (erase_mat A i i))

goal (1 subgoal):
 1. monic (charpoly (erase_mat A i i)) &&& degree (charpoly (erase_mat A i i)) \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
monic p
degree p \<noteq> 0

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
let ?f = "poly p"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
have cont: "continuous_on {a..b} ?f" for a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on {a..b} (poly p)
[PROOF STEP]
by (auto intro: continuous_intros)
[PROOF STATE]
proof (state)
this:
continuous_on {?a..?b} (poly p)

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
from pos
[PROOF STATE]
proof (chain)
picking this:
poly (charpoly (erase_mat A i i)) sr < 0
[PROOF STEP]
have le: "?f sr \<le> 0"
[PROOF STATE]
proof (prove)
using this:
poly (charpoly (erase_mat A i i)) sr < 0

goal (1 subgoal):
 1. poly p sr \<le> 0
[PROOF STEP]
by (auto simp: p_def)
[PROOF STATE]
proof (state)
this:
poly p sr \<le> 0

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
from mon
[PROOF STATE]
proof (chain)
picking this:
monic p
[PROOF STEP]
have lc: "lead_coeff p > 0"
[PROOF STATE]
proof (prove)
using this:
monic p

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

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
from poly_pinfty_ge[OF this deg, of 0]
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. \<forall>x\<ge>n. 0 \<le> poly p x
[PROOF STEP]
obtain z where lez: "\<And> x. z \<le> x \<Longrightarrow> 0 \<le> ?f x"
[PROOF STATE]
proof (prove)
using this:
\<exists>n. \<forall>x\<ge>n. 0 \<le> poly p x

goal (1 subgoal):
 1. (\<And>z. (\<And>x. z \<le> x \<Longrightarrow> 0 \<le> poly p x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<le> ?x \<Longrightarrow> 0 \<le> poly p ?x

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
define y where "y = max z sr"
[PROOF STATE]
proof (state)
this:
y = max z sr

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
have yr: "y \<ge> sr" and "y \<ge> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sr \<le> y &&& z \<le> y
[PROOF STEP]
unfolding y_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sr \<le> max z sr &&& z \<le> max z sr
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sr \<le> y
z \<le> y

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
from lez[OF this(2)]
[PROOF STATE]
proof (chain)
picking this:
0 \<le> poly p y
[PROOF STEP]
have y0: "?f y \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
0 \<le> poly p y

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

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
from IVT'[of ?f, OF le y0 yr cont]
[PROOF STATE]
proof (chain)
picking this:
\<exists>x\<ge>sr. x \<le> y \<and> poly p x = 0
[PROOF STEP]
obtain x where ge: "x \<ge> sr" and rt: "?f x = 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>x\<ge>sr. x \<le> y \<and> poly p x = 0

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>sr \<le> x; poly p x = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding p_def
[PROOF STATE]
proof (prove)
using this:
\<exists>x\<ge>sr. x \<le> y \<and> poly (charpoly (erase_mat A i i)) x = 0

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>sr \<le> x; poly (charpoly (erase_mat A i i)) x = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sr \<le> x
poly p x = 0

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
hence "eigen_value ?A x"
[PROOF STATE]
proof (prove)
using this:
sr \<le> x
poly p x = 0

goal (1 subgoal):
 1. eigen_value (erase_mat A i i) x
[PROOF STEP]
unfolding p_def
[PROOF STATE]
proof (prove)
using this:
sr \<le> x
poly (charpoly (erase_mat A i i)) x = 0

goal (1 subgoal):
 1. eigen_value (erase_mat A i i) x
[PROOF STEP]
by (simp add: eigen_value_root_charpoly)
[PROOF STATE]
proof (state)
this:
eigen_value (erase_mat A i i) x

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
from ev_small_real[OF this] ge
[PROOF STATE]
proof (chain)
picking this:
\<bar>x\<bar> < sr
sr \<le> x
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
\<bar>x\<bar> < sr
sr \<le> x

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

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
poly (charpoly (erase_mat A i i)) sr < 0 \<Longrightarrow> False

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
with pos0
[PROOF STATE]
proof (chain)
picking this:
poly (charpoly (erase_mat A i i)) sr \<noteq> 0
poly (charpoly (erase_mat A i i)) sr < 0 \<Longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
poly (charpoly (erase_mat A i i)) sr \<noteq> 0
poly (charpoly (erase_mat A i i)) sr < 0 \<Longrightarrow> False

goal (1 subgoal):
 1. 0 < poly (charpoly (erase_mat A i i)) sr
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
0 < poly (charpoly (erase_mat A i i)) sr

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma multiplicity_sr_1: "order sr (charpoly A) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. order sr (charpoly A) = 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. order sr (charpoly A) = 1
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. order sr (charpoly A) = 1
[PROOF STEP]
assume "poly (pderiv (charpoly A)) sr = 0"
[PROOF STATE]
proof (state)
this:
poly (pderiv (charpoly A)) sr = 0

goal (1 subgoal):
 1. order sr (charpoly A) = 1
[PROOF STEP]
hence "0 = poly (monom 1 1 * pderiv (charpoly A)) sr"
[PROOF STATE]
proof (prove)
using this:
poly (pderiv (charpoly A)) sr = 0

goal (1 subgoal):
 1. 0 = poly (monom 1 1 * pderiv (charpoly A)) sr
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 = poly (monom 1 1 * pderiv (charpoly A)) sr

goal (1 subgoal):
 1. order sr (charpoly A) = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 = poly (monom 1 1 * pderiv (charpoly A)) sr

goal (1 subgoal):
 1. order sr (charpoly A) = 1
[PROOF STEP]
have "\<dots> = sum (\<lambda> i. poly (charpoly (erase_mat A i i)) sr) UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly (monom 1 1 * pderiv (charpoly A)) sr = (\<Sum>i\<in>UNIV. poly (charpoly (erase_mat A i i)) sr)
[PROOF STEP]
unfolding pderiv_char_poly_erase_mat poly_sum
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k\<in>UNIV. poly (charpoly (erase_mat A k k)) sr) = (\<Sum>i\<in>UNIV. poly (charpoly (erase_mat A i i)) sr)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
poly (monom 1 1 * pderiv (charpoly A)) sr = (\<Sum>i\<in>UNIV. poly (charpoly (erase_mat A i i)) sr)

goal (1 subgoal):
 1. order sr (charpoly A) = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
poly (monom 1 1 * pderiv (charpoly A)) sr = (\<Sum>i\<in>UNIV. poly (charpoly (erase_mat A i i)) sr)

goal (1 subgoal):
 1. order sr (charpoly A) = 1
[PROOF STEP]
have "\<dots> > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < (\<Sum>i\<in>UNIV. poly (charpoly (erase_mat A i i)) sr)
[PROOF STEP]
by (rule sum_pos, (force simp: charpoly_erase_mat_sr)+)
[PROOF STATE]
proof (state)
this:
0 < (\<Sum>i\<in>UNIV. poly (charpoly (erase_mat A i i)) sr)

goal (1 subgoal):
 1. order sr (charpoly A) = 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
0 < 0
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
0 < 0

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

goal (1 subgoal):
 1. order sr (charpoly A) = 1
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
poly (pderiv (charpoly A)) sr = 0 \<Longrightarrow> False

goal (1 subgoal):
 1. order sr (charpoly A) = 1
[PROOF STEP]
hence nZ: "poly (pderiv (charpoly A)) sr \<noteq> 0" and nZ': "pderiv (charpoly A) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
poly (pderiv (charpoly A)) sr = 0 \<Longrightarrow> False

goal (1 subgoal):
 1. poly (pderiv (charpoly A)) sr \<noteq> 0 &&& pderiv (charpoly A) \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poly (pderiv (charpoly A)) sr \<noteq> 0
pderiv (charpoly A) \<noteq> 0

goal (1 subgoal):
 1. order sr (charpoly A) = 1
[PROOF STEP]
from eigen_vector_z_sr
[PROOF STATE]
proof (chain)
picking this:
eigen_vector A z sr
[PROOF STEP]
have "eigen_value A 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]
..
[PROOF STATE]
proof (state)
this:
eigen_value A sr

goal (1 subgoal):
 1. order sr (charpoly A) = 1
[PROOF STEP]
from this[unfolded eigen_value_root_charpoly]
[PROOF STATE]
proof (chain)
picking this:
poly (charpoly A) sr = 0
[PROOF STEP]
have "poly (charpoly A) sr = 0"
[PROOF STATE]
proof (prove)
using this:
poly (charpoly A) sr = 0

goal (1 subgoal):
 1. poly (charpoly A) sr = 0
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
poly (charpoly A) sr = 0

goal (1 subgoal):
 1. order sr (charpoly A) = 1
[PROOF STEP]
hence "order sr (charpoly A) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
poly (charpoly A) sr = 0

goal (1 subgoal):
 1. order sr (charpoly A) \<noteq> 0
[PROOF STEP]
unfolding order_root
[PROOF STATE]
proof (prove)
using this:
charpoly A = 0 \<or> order sr (charpoly A) \<noteq> 0

goal (1 subgoal):
 1. order sr (charpoly A) \<noteq> 0
[PROOF STEP]
using nZ'
[PROOF STATE]
proof (prove)
using this:
charpoly A = 0 \<or> order sr (charpoly A) \<noteq> 0
pderiv (charpoly A) \<noteq> 0

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

goal (1 subgoal):
 1. order sr (charpoly A) = 1
[PROOF STEP]
from order_pderiv[OF nZ' this] order_0I[OF nZ]
[PROOF STATE]
proof (chain)
picking this:
order sr (charpoly A) = Suc (order sr (pderiv (charpoly A)))
order sr (pderiv (charpoly A)) = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
order sr (charpoly A) = Suc (order sr (pderiv (charpoly A)))
order sr (pderiv (charpoly A)) = 0

goal (1 subgoal):
 1. order sr (charpoly A) = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
order sr (charpoly A) = 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sr_spectral_radius: "sr = spectral_radius cA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sr = HMA_Connect.spectral_radius cA
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sr = HMA_Connect.spectral_radius cA
[PROOF STEP]
from eigen_vector_z_sr_c
[PROOF STATE]
proof (chain)
picking this:
eigen_vector cA (map_vector complex_of_real z) (complex_of_real sr)
[PROOF STEP]
have "eigen_value cA (c sr)"
[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
[PROOF STATE]
proof (state)
this:
eigen_value cA (complex_of_real sr)

goal (1 subgoal):
 1. sr = HMA_Connect.spectral_radius cA
[PROOF STEP]
from spectral_radius_max[OF this]
[PROOF STATE]
proof (chain)
picking this:
cmod (complex_of_real sr) \<le> HMA_Connect.spectral_radius cA
[PROOF STEP]
have sr: "sr \<le> spectral_radius cA"
[PROOF STATE]
proof (prove)
using this:
cmod (complex_of_real sr) \<le> HMA_Connect.spectral_radius cA

goal (1 subgoal):
 1. sr \<le> HMA_Connect.spectral_radius cA
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sr \<le> HMA_Connect.spectral_radius cA

goal (1 subgoal):
 1. sr = HMA_Connect.spectral_radius cA
[PROOF STEP]
with spectral_radius_ev[of cA] eigen_vector_norm_sr
[PROOF STATE]
proof (chain)
picking this:
\<exists>ev v. eigen_vector cA v ev \<and> cmod ev = HMA_Connect.spectral_radius cA
eigen_vector cA ?v ?\<alpha> \<Longrightarrow> cmod ?\<alpha> \<le> sr
sr \<le> HMA_Connect.spectral_radius cA
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>ev v. eigen_vector cA v ev \<and> cmod ev = HMA_Connect.spectral_radius cA
eigen_vector cA ?v ?\<alpha> \<Longrightarrow> cmod ?\<alpha> \<le> sr
sr \<le> HMA_Connect.spectral_radius cA

goal (1 subgoal):
 1. sr = HMA_Connect.spectral_radius cA
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
sr = HMA_Connect.spectral_radius cA

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma le_vec_A_mu: assumes y: "y \<in> X" and le: "le_vec (A *v y) (mu *s y)"
  shows "sr \<le> mu" "lt_vec 0 y"
  "mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sr \<le> mu &&& lt_vec 0 y &&& (mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. sr \<le> mu
 2. lt_vec 0 y
 3. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
let ?w = "rowvector w"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. sr \<le> mu
 2. lt_vec 0 y
 3. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
let ?w' = "columnvector w"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. sr \<le> mu
 2. lt_vec 0 y
 3. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
have "?w ** A = transpose (transpose (?w ** A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rowvector w ** A = Finite_Cartesian_Product.transpose (Finite_Cartesian_Product.transpose (rowvector w ** A))
[PROOF STEP]
unfolding transpose_transpose
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rowvector w ** A = Finite_Cartesian_Product.transpose (Finite_Cartesian_Product.transpose (rowvector w ** A))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rowvector w ** A = Finite_Cartesian_Product.transpose (Finite_Cartesian_Product.transpose (rowvector w ** A))

goal (3 subgoals):
 1. sr \<le> mu
 2. lt_vec 0 y
 3. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rowvector w ** A = Finite_Cartesian_Product.transpose (Finite_Cartesian_Product.transpose (rowvector w ** A))

goal (3 subgoals):
 1. sr \<le> mu
 2. lt_vec 0 y
 3. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
have "transpose (?w ** A) = transpose A ** transpose ?w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Finite_Cartesian_Product.transpose (rowvector w ** A) = Finite_Cartesian_Product.transpose A ** Finite_Cartesian_Product.transpose (rowvector w)
[PROOF STEP]
by (rule matrix_transpose_mul)
[PROOF STATE]
proof (state)
this:
Finite_Cartesian_Product.transpose (rowvector w ** A) = Finite_Cartesian_Product.transpose A ** Finite_Cartesian_Product.transpose (rowvector w)

goal (3 subgoals):
 1. sr \<le> mu
 2. lt_vec 0 y
 3. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Finite_Cartesian_Product.transpose (rowvector w ** A) = Finite_Cartesian_Product.transpose A ** Finite_Cartesian_Product.transpose (rowvector w)

goal (3 subgoals):
 1. sr \<le> mu
 2. lt_vec 0 y
 3. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
have "transpose ?w = columnvector w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Finite_Cartesian_Product.transpose (rowvector w) = columnvector w
[PROOF STEP]
by (rule transpose_rowvector)
[PROOF STATE]
proof (state)
this:
Finite_Cartesian_Product.transpose (rowvector w) = columnvector w

goal (3 subgoals):
 1. sr \<le> mu
 2. lt_vec 0 y
 3. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Finite_Cartesian_Product.transpose (rowvector w) = columnvector w

goal (3 subgoals):
 1. sr \<le> mu
 2. lt_vec 0 y
 3. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
have "transpose A ** \<dots> = columnvector (transpose A *v w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Finite_Cartesian_Product.transpose A ** columnvector w = columnvector (Finite_Cartesian_Product.transpose A *v w)
[PROOF STEP]
unfolding dot_rowvector_columnvector[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. columnvector (Finite_Cartesian_Product.transpose A *v w) = columnvector (Finite_Cartesian_Product.transpose A *v w)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
Finite_Cartesian_Product.transpose A ** columnvector w = columnvector (Finite_Cartesian_Product.transpose A *v w)

goal (3 subgoals):
 1. sr \<le> mu
 2. lt_vec 0 y
 3. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Finite_Cartesian_Product.transpose A ** columnvector w = columnvector (Finite_Cartesian_Product.transpose A *v w)

goal (3 subgoals):
 1. sr \<le> mu
 2. lt_vec 0 y
 3. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
have "transpose A *v w = sr *s w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Finite_Cartesian_Product.transpose A *v w = sr *s w
[PROOF STEP]
unfolding w
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sr *s w = sr *s w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Finite_Cartesian_Product.transpose A *v w = sr *s w

goal (3 subgoals):
 1. sr \<le> mu
 2. lt_vec 0 y
 3. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Finite_Cartesian_Product.transpose A *v w = sr *s w

goal (3 subgoals):
 1. sr \<le> mu
 2. lt_vec 0 y
 3. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
have "transpose (columnvector \<dots>) = rowvector (sr *s w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Finite_Cartesian_Product.transpose (columnvector (sr *s w)) = rowvector (sr *s w)
[PROOF STEP]
unfolding transpose_def columnvector_def rowvector_def vector_scalar_mult_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>i j. (\<chi>i j. (\<chi>i. sr * w $h i) $h i) $h j $h i) = (\<chi>i. vec_lambda (($h) (\<chi>i. sr * w $h i)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Finite_Cartesian_Product.transpose (columnvector (sr *s w)) = rowvector (sr *s w)

goal (3 subgoals):
 1. sr \<le> mu
 2. lt_vec 0 y
 3. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
rowvector w ** A = rowvector (sr *s w)
[PROOF STEP]
have 1: "?w ** A = rowvector (sr *s w)"
[PROOF STATE]
proof (prove)
using this:
rowvector w ** A = rowvector (sr *s w)

goal (1 subgoal):
 1. rowvector w ** A = rowvector (sr *s w)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
rowvector w ** A = rowvector (sr *s w)

goal (3 subgoals):
 1. sr \<le> mu
 2. lt_vec 0 y
 3. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
have "sr *s (?w *v y) = ?w ** A *v y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sr *s (rowvector w *v y) = rowvector w ** A *v y
[PROOF STEP]
unfolding 1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sr *s (rowvector w *v y) = rowvector (sr *s w) *v y
[PROOF STEP]
by (auto simp: rowvector_def vector_scalar_mult_def matrix_vector_mult_def vec_eq_iff
       sum_distrib_left mult.assoc)
[PROOF STATE]
proof (state)
this:
sr *s (rowvector w *v y) = rowvector w ** A *v y

goal (3 subgoals):
 1. sr \<le> mu
 2. lt_vec 0 y
 3. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sr *s (rowvector w *v y) = rowvector w ** A *v y

goal (3 subgoals):
 1. sr \<le> mu
 2. lt_vec 0 y
 3. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
have "\<dots> = ?w *v (A *v y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rowvector w ** A *v y = rowvector w *v (A *v y)
[PROOF STEP]
by (simp add: matrix_vector_mul_assoc)
[PROOF STATE]
proof (state)
this:
rowvector w ** A *v y = rowvector w *v (A *v y)

goal (3 subgoals):
 1. sr \<le> mu
 2. lt_vec 0 y
 3. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sr *s (rowvector w *v y) = rowvector w *v (A *v y)
[PROOF STEP]
have eq1: "sr *s (rowvector w *v y) = rowvector w *v (A *v y)"
[PROOF STATE]
proof (prove)
using this:
sr *s (rowvector w *v y) = rowvector w *v (A *v y)

goal (1 subgoal):
 1. sr *s (rowvector w *v y) = rowvector w *v (A *v y)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sr *s (rowvector w *v y) = rowvector w *v (A *v y)

goal (3 subgoals):
 1. sr \<le> mu
 2. lt_vec 0 y
 3. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
have "le_vec (rowvector w *v (A *v y)) (?w *v (mu *s y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. le_vec (rowvector w *v (A *v y)) (rowvector w *v (mu *s y))
[PROOF STEP]
by (rule le_vec_mono_left[OF _ le], insert w(2), auto simp: rowvector_def order.strict_iff_order)
[PROOF STATE]
proof (state)
this:
le_vec (rowvector w *v (A *v y)) (rowvector w *v (mu *s y))

goal (3 subgoals):
 1. sr \<le> mu
 2. lt_vec 0 y
 3. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
le_vec (rowvector w *v (A *v y)) (rowvector w *v (mu *s y))

goal (3 subgoals):
 1. sr \<le> mu
 2. lt_vec 0 y
 3. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
have "?w *v (mu *s y) = mu *s (?w *v y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rowvector w *v (mu *s y) = mu *s (rowvector w *v y)
[PROOF STEP]
by (simp add: algebra_simps vec.scale)
[PROOF STATE]
proof (state)
this:
rowvector w *v (mu *s y) = mu *s (rowvector w *v y)

goal (3 subgoals):
 1. sr \<le> mu
 2. lt_vec 0 y
 3. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
le_vec (rowvector w *v (A *v y)) (mu *s (rowvector w *v y))
[PROOF STEP]
have le1: "le_vec (rowvector w *v (A *v y)) (mu *s (?w *v y))"
[PROOF STATE]
proof (prove)
using this:
le_vec (rowvector w *v (A *v y)) (mu *s (rowvector w *v y))

goal (1 subgoal):
 1. le_vec (rowvector w *v (A *v y)) (mu *s (rowvector w *v y))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
le_vec (rowvector w *v (A *v y)) (mu *s (rowvector w *v y))

goal (3 subgoals):
 1. sr \<le> mu
 2. lt_vec 0 y
 3. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
from le1[unfolded eq1[symmetric]]
[PROOF STATE]
proof (chain)
picking this:
le_vec (sr *s (rowvector w *v y)) (mu *s (rowvector w *v y))
[PROOF STEP]
have 2: "le_vec (sr *s (?w *v y)) (mu *s (?w *v y))"
[PROOF STATE]
proof (prove)
using this:
le_vec (sr *s (rowvector w *v y)) (mu *s (rowvector w *v y))

goal (1 subgoal):
 1. le_vec (sr *s (rowvector w *v y)) (mu *s (rowvector w *v y))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
le_vec (sr *s (rowvector w *v y)) (mu *s (rowvector w *v y))

goal (3 subgoals):
 1. sr \<le> mu
 2. lt_vec 0 y
 3. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
le_vec (sr *s (rowvector w *v y)) (mu *s (rowvector w *v y))

goal (3 subgoals):
 1. sr \<le> mu
 2. lt_vec 0 y
 3. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
from y
[PROOF STATE]
proof (chain)
picking this:
y \<in> X
[PROOF STEP]
obtain i where yi: "y $ i > 0" and y: "\<And> j. y $ j \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
y \<in> X

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>0 < y $h i; \<And>j. 0 \<le> y $h j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding X_def
[PROOF STATE]
proof (prove)
using this:
y \<in> {x. le_vec 0 x \<and> x \<noteq> 0}

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>0 < y $h i; \<And>j. 0 \<le> y $h j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: order.strict_iff_order vec_eq_iff)
[PROOF STATE]
proof (state)
this:
0 < y $h i
0 \<le> y $h ?j12

goal (3 subgoals):
 1. sr \<le> mu
 2. lt_vec 0 y
 3. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
from w(2)
[PROOF STATE]
proof (chain)
picking this:
lt_vec 0 w
[PROOF STEP]
have wi: "w $ i > 0" and w: "\<And> j. w $ j \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
lt_vec 0 w

goal (1 subgoal):
 1. 0 < w $h i &&& (\<And>j. 0 \<le> w $h j)
[PROOF STEP]
by (auto simp: order.strict_iff_order)
[PROOF STATE]
proof (state)
this:
0 < w $h i
0 \<le> w $h ?j12

goal (3 subgoals):
 1. sr \<le> mu
 2. lt_vec 0 y
 3. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
have "(?w *v y) $ i > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < (rowvector w *v y) $h i
[PROOF STEP]
using yi y wi w
[PROOF STATE]
proof (prove)
using this:
0 < y $h i
0 \<le> y $h ?j12
0 < w $h i
0 \<le> w $h ?j12

goal (1 subgoal):
 1. 0 < (rowvector w *v y) $h i
[PROOF STEP]
by (auto simp: matrix_vector_mult_def rowvector_def
        intro!: sum_pos2[of _ i] mult_nonneg_nonneg)
[PROOF STATE]
proof (state)
this:
0 < (rowvector w *v y) $h i

goal (3 subgoals):
 1. sr \<le> mu
 2. lt_vec 0 y
 3. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < (rowvector w *v y) $h i

goal (3 subgoals):
 1. sr \<le> mu
 2. lt_vec 0 y
 3. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
from 2[rule_format, of i]
[PROOF STATE]
proof (chain)
picking this:
(sr *s (rowvector w *v y)) $h i \<le> (mu *s (rowvector w *v y)) $h i
[PROOF STEP]
have "sr * (?w *v y) $ i \<le> mu * (?w *v y) $ i"
[PROOF STATE]
proof (prove)
using this:
(sr *s (rowvector w *v y)) $h i \<le> (mu *s (rowvector w *v y)) $h i

goal (1 subgoal):
 1. sr * (rowvector w *v y) $h i \<le> mu * (rowvector w *v y) $h i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sr * (rowvector w *v y) $h i \<le> mu * (rowvector w *v y) $h i

goal (3 subgoals):
 1. sr \<le> mu
 2. lt_vec 0 y
 3. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 < (rowvector w *v y) $h i
sr * (rowvector w *v y) $h i \<le> mu * (rowvector w *v y) $h i
[PROOF STEP]
have "sr \<le> mu"
[PROOF STATE]
proof (prove)
using this:
0 < (rowvector w *v y) $h i
sr * (rowvector w *v y) $h i \<le> mu * (rowvector w *v y) $h i

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

goal (3 subgoals):
 1. sr \<le> mu
 2. lt_vec 0 y
 3. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
sr \<le> mu

goal (3 subgoals):
 1. sr \<le> mu
 2. lt_vec 0 y
 3. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
thus *: "sr \<le> mu"
[PROOF STATE]
proof (prove)
using this:
sr \<le> mu

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

goal (2 subgoals):
 1. lt_vec 0 y
 2. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
define cc where "cc = (mu + 1)^ N"
[PROOF STATE]
proof (state)
this:
cc = (mu + 1) ^ N

goal (2 subgoals):
 1. lt_vec 0 y
 2. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
define n where "n = N"
[PROOF STATE]
proof (state)
this:
n = N

goal (2 subgoals):
 1. lt_vec 0 y
 2. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
from * sr_pos
[PROOF STATE]
proof (chain)
picking this:
sr \<le> mu
0 < sr
[PROOF STEP]
have mu: "mu \<ge> 0" "mu > 0"
[PROOF STATE]
proof (prove)
using this:
sr \<le> mu
0 < sr

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

goal (2 subgoals):
 1. lt_vec 0 y
 2. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
hence cc: "cc > 0"
[PROOF STATE]
proof (prove)
using this:
0 \<le> mu
0 < mu

goal (1 subgoal):
 1. 0 < cc
[PROOF STEP]
unfolding cc_def
[PROOF STATE]
proof (prove)
using this:
0 \<le> mu
0 < mu

goal (1 subgoal):
 1. 0 < (mu + 1) ^ N
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < cc

goal (2 subgoals):
 1. lt_vec 0 y
 2. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
from y
[PROOF STATE]
proof (chain)
picking this:
y \<in> X
[PROOF STEP]
have "pow_A_1 y \<in> pow_A_1 ` X"
[PROOF STATE]
proof (prove)
using this:
y \<in> X

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

goal (2 subgoals):
 1. lt_vec 0 y
 2. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
from Y_pos_main[OF this]
[PROOF STATE]
proof (chain)
picking this:
0 < pow_A_1 y $h ?i
[PROOF STEP]
have lt: "0 < (A1n *v y) $ i" for i
[PROOF STATE]
proof (prove)
using this:
0 < pow_A_1 y $h ?i

goal (1 subgoal):
 1. 0 < (A1n *v y) $h i
[PROOF STEP]
by (simp add: pow_A_1_def)
[PROOF STATE]
proof (state)
this:
0 < (A1n *v y) $h ?i12

goal (2 subgoals):
 1. lt_vec 0 y
 2. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
have le: "le_vec (A1n *v y) (cc *s y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. le_vec (A1n *v y) (cc *s y)
[PROOF STEP]
unfolding cc_def A1n_def n_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. le_vec (matpow (A + mat 1) n *v y) ((mu + 1) ^ n *s y)
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. le_vec (matpow (A + mat 1) 0 *v y) ((mu + 1) ^ 0 *s y)
 2. \<And>n. le_vec (matpow (A + mat 1) n *v y) ((mu + 1) ^ n *s y) \<Longrightarrow> le_vec (matpow (A + mat 1) (Suc n) *v y) ((mu + 1) ^ Suc n *s y)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
le_vec (matpow (A + mat 1) n *v y) ((mu + 1) ^ n *s y)

goal (2 subgoals):
 1. le_vec (matpow (A + mat 1) 0 *v y) ((mu + 1) ^ 0 *s y)
 2. \<And>n. le_vec (matpow (A + mat 1) n *v y) ((mu + 1) ^ n *s y) \<Longrightarrow> le_vec (matpow (A + mat 1) (Suc n) *v y) ((mu + 1) ^ Suc n *s y)
[PROOF STEP]
let ?An = "matpow (A + mat 1) n"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. le_vec (matpow (A + mat 1) 0 *v y) ((mu + 1) ^ 0 *s y)
 2. \<And>n. le_vec (matpow (A + mat 1) n *v y) ((mu + 1) ^ n *s y) \<Longrightarrow> le_vec (matpow (A + mat 1) (Suc n) *v y) ((mu + 1) ^ Suc n *s y)
[PROOF STEP]
let ?mu = "(mu + 1)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. le_vec (matpow (A + mat 1) 0 *v y) ((mu + 1) ^ 0 *s y)
 2. \<And>n. le_vec (matpow (A + mat 1) n *v y) ((mu + 1) ^ n *s y) \<Longrightarrow> le_vec (matpow (A + mat 1) (Suc n) *v y) ((mu + 1) ^ Suc n *s y)
[PROOF STEP]
have id': "matpow (A + mat 1) (Suc n) *v y = A *v (?An *v y) + ?An *v y" (is "?a = ?b + ?c")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matpow (A + mat 1) (Suc n) *v y = A *v (matpow (A + mat 1) n *v y) + matpow (A + mat 1) n *v y
[PROOF STEP]
by (simp add: matrix_add_ldistrib matrix_mul_rid matrix_add_vect_distrib matpow_1_commute
       matrix_vector_mul_assoc[symmetric])
[PROOF STATE]
proof (state)
this:
matpow (A + mat 1) (Suc n) *v y = A *v (matpow (A + mat 1) n *v y) + matpow (A + mat 1) n *v y

goal (2 subgoals):
 1. le_vec (matpow (A + mat 1) 0 *v y) ((mu + 1) ^ 0 *s y)
 2. \<And>n. le_vec (matpow (A + mat 1) n *v y) ((mu + 1) ^ n *s y) \<Longrightarrow> le_vec (matpow (A + mat 1) (Suc n) *v y) ((mu + 1) ^ Suc n *s y)
[PROOF STEP]
have "le_vec ?b (?mu^n *s (A *v y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. le_vec (A *v (matpow (A + mat 1) n *v y)) ((mu + 1) ^ n *s (A *v y))
[PROOF STEP]
using le_vec_mono_left[OF nonneg Suc]
[PROOF STATE]
proof (prove)
using this:
le_vec (A *v (matpow (A + mat 1) n *v y)) (A *v ((mu + 1) ^ n *s y))

goal (1 subgoal):
 1. le_vec (A *v (matpow (A + mat 1) n *v y)) ((mu + 1) ^ n *s (A *v y))
[PROOF STEP]
by (simp add: algebra_simps vec.scale)
[PROOF STATE]
proof (state)
this:
le_vec (A *v (matpow (A + mat 1) n *v y)) ((mu + 1) ^ n *s (A *v y))

goal (2 subgoals):
 1. le_vec (matpow (A + mat 1) 0 *v y) ((mu + 1) ^ 0 *s y)
 2. \<And>n. le_vec (matpow (A + mat 1) n *v y) ((mu + 1) ^ n *s y) \<Longrightarrow> le_vec (matpow (A + mat 1) (Suc n) *v y) ((mu + 1) ^ Suc n *s y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
le_vec (A *v (matpow (A + mat 1) n *v y)) ((mu + 1) ^ n *s (A *v y))

goal (2 subgoals):
 1. le_vec (matpow (A + mat 1) 0 *v y) ((mu + 1) ^ 0 *s y)
 2. \<And>n. le_vec (matpow (A + mat 1) n *v y) ((mu + 1) ^ n *s y) \<Longrightarrow> le_vec (matpow (A + mat 1) (Suc n) *v y) ((mu + 1) ^ Suc n *s y)
[PROOF STEP]
have "le_vec (?mu^n *s (A *v y)) (?mu^n *s (mu *s y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. le_vec ((mu + 1) ^ n *s (A *v y)) ((mu + 1) ^ n *s (mu *s y))
[PROOF STEP]
using le mu
[PROOF STATE]
proof (prove)
using this:
le_vec (A *v y) (mu *s y)
0 \<le> mu
0 < mu

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

goal (2 subgoals):
 1. le_vec (matpow (A + mat 1) 0 *v y) ((mu + 1) ^ 0 *s y)
 2. \<And>n. le_vec (matpow (A + mat 1) n *v y) ((mu + 1) ^ n *s y) \<Longrightarrow> le_vec (matpow (A + mat 1) (Suc n) *v y) ((mu + 1) ^ Suc n *s y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
le_vec ((mu + 1) ^ n *s (A *v y)) ((mu + 1) ^ n *s (mu *s y))

goal (2 subgoals):
 1. le_vec (matpow (A + mat 1) 0 *v y) ((mu + 1) ^ 0 *s y)
 2. \<And>n. le_vec (matpow (A + mat 1) n *v y) ((mu + 1) ^ n *s y) \<Longrightarrow> le_vec (matpow (A + mat 1) (Suc n) *v y) ((mu + 1) ^ Suc n *s y)
[PROOF STEP]
have id: "?mu^n *s (mu *s y) = (?mu^n * mu) *s y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mu + 1) ^ n *s (mu *s y) = (mu + 1) ^ n * mu *s y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(mu + 1) ^ n *s (mu *s y) = (mu + 1) ^ n * mu *s y

goal (2 subgoals):
 1. le_vec (matpow (A + mat 1) 0 *v y) ((mu + 1) ^ 0 *s y)
 2. \<And>n. le_vec (matpow (A + mat 1) n *v y) ((mu + 1) ^ n *s y) \<Longrightarrow> le_vec (matpow (A + mat 1) (Suc n) *v y) ((mu + 1) ^ Suc n *s y)
[PROOF STEP]
from le_vec_trans[OF calculation[unfolded id]]
[PROOF STATE]
proof (chain)
picking this:
le_vec (A *v (matpow (A + mat 1) n *v y)) ((mu + 1) ^ n * mu *s y)
[PROOF STEP]
have le1: "le_vec ?b ((?mu^n * mu) *s y)"
[PROOF STATE]
proof (prove)
using this:
le_vec (A *v (matpow (A + mat 1) n *v y)) ((mu + 1) ^ n * mu *s y)

goal (1 subgoal):
 1. le_vec (A *v (matpow (A + mat 1) n *v y)) ((mu + 1) ^ n * mu *s y)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
le_vec (A *v (matpow (A + mat 1) n *v y)) ((mu + 1) ^ n * mu *s y)

goal (2 subgoals):
 1. le_vec (matpow (A + mat 1) 0 *v y) ((mu + 1) ^ 0 *s y)
 2. \<And>n. le_vec (matpow (A + mat 1) n *v y) ((mu + 1) ^ n *s y) \<Longrightarrow> le_vec (matpow (A + mat 1) (Suc n) *v y) ((mu + 1) ^ Suc n *s y)
[PROOF STEP]
from Suc
[PROOF STATE]
proof (chain)
picking this:
le_vec (matpow (A + mat 1) n *v y) ((mu + 1) ^ n *s y)
[PROOF STEP]
have le2: "le_vec ?c ((mu + 1) ^ n *s y)"
[PROOF STATE]
proof (prove)
using this:
le_vec (matpow (A + mat 1) n *v y) ((mu + 1) ^ n *s y)

goal (1 subgoal):
 1. le_vec (matpow (A + mat 1) n *v y) ((mu + 1) ^ n *s y)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
le_vec (matpow (A + mat 1) n *v y) ((mu + 1) ^ n *s y)

goal (2 subgoals):
 1. le_vec (matpow (A + mat 1) 0 *v y) ((mu + 1) ^ 0 *s y)
 2. \<And>n. le_vec (matpow (A + mat 1) n *v y) ((mu + 1) ^ n *s y) \<Longrightarrow> le_vec (matpow (A + mat 1) (Suc n) *v y) ((mu + 1) ^ Suc n *s y)
[PROOF STEP]
have le: "le_vec ?a ((?mu^n * mu) *s y + ?mu^n *s y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. le_vec (matpow (A + mat 1) (Suc n) *v y) ((mu + 1) ^ n * mu *s y + (mu + 1) ^ n *s y)
[PROOF STEP]
unfolding id'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. le_vec (A *v (matpow (A + mat 1) n *v y) + matpow (A + mat 1) n *v y) ((mu + 1) ^ n * mu *s y + (mu + 1) ^ n *s y)
[PROOF STEP]
using add_mono[OF le1[rule_format] le2[rule_format]]
[PROOF STATE]
proof (prove)
using this:
(A *v (matpow (A + mat 1) n *v y)) $h ?i2 + (matpow (A + mat 1) n *v y) $h ?i1 \<le> ((mu + 1) ^ n * mu *s y) $h ?i2 + ((mu + 1) ^ n *s y) $h ?i1

goal (1 subgoal):
 1. le_vec (A *v (matpow (A + mat 1) n *v y) + matpow (A + mat 1) n *v y) ((mu + 1) ^ n * mu *s y + (mu + 1) ^ n *s y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
le_vec (matpow (A + mat 1) (Suc n) *v y) ((mu + 1) ^ n * mu *s y + (mu + 1) ^ n *s y)

goal (2 subgoals):
 1. le_vec (matpow (A + mat 1) 0 *v y) ((mu + 1) ^ 0 *s y)
 2. \<And>n. le_vec (matpow (A + mat 1) n *v y) ((mu + 1) ^ n *s y) \<Longrightarrow> le_vec (matpow (A + mat 1) (Suc n) *v y) ((mu + 1) ^ Suc n *s y)
[PROOF STEP]
have id'': "(?mu^n * mu) *s y + ?mu^n *s y = ?mu^Suc n *s y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mu + 1) ^ n * mu *s y + (mu + 1) ^ n *s y = (mu + 1) ^ Suc n *s y
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
(mu + 1) ^ n * mu *s y + (mu + 1) ^ n *s y = (mu + 1) ^ Suc n *s y

goal (2 subgoals):
 1. le_vec (matpow (A + mat 1) 0 *v y) ((mu + 1) ^ 0 *s y)
 2. \<And>n. le_vec (matpow (A + mat 1) n *v y) ((mu + 1) ^ n *s y) \<Longrightarrow> le_vec (matpow (A + mat 1) (Suc n) *v y) ((mu + 1) ^ Suc n *s y)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. le_vec (matpow (A + mat 1) (Suc n) *v y) ((mu + 1) ^ Suc n *s y)
[PROOF STEP]
using le
[PROOF STATE]
proof (prove)
using this:
le_vec (matpow (A + mat 1) (Suc n) *v y) ((mu + 1) ^ n * mu *s y + (mu + 1) ^ n *s y)

goal (1 subgoal):
 1. le_vec (matpow (A + mat 1) (Suc n) *v y) ((mu + 1) ^ Suc n *s y)
[PROOF STEP]
unfolding id''
[PROOF STATE]
proof (prove)
using this:
le_vec (matpow (A + mat 1) (Suc n) *v y) ((mu + 1) ^ Suc n *s y)

goal (1 subgoal):
 1. le_vec (matpow (A + mat 1) (Suc n) *v y) ((mu + 1) ^ Suc n *s y)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
le_vec (matpow (A + mat 1) (Suc n) *v y) ((mu + 1) ^ Suc n *s y)

goal (1 subgoal):
 1. le_vec (matpow (A + mat 1) 0 *v y) ((mu + 1) ^ 0 *s y)
[PROOF STEP]
qed (simp add: matrix_vector_mul_lid)
[PROOF STATE]
proof (state)
this:
le_vec (A1n *v y) (cc *s y)

goal (2 subgoals):
 1. lt_vec 0 y
 2. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
have lt: "0 < cc * y $ i" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < cc * y $h i
[PROOF STEP]
using lt[of i] le[rule_format, of i]
[PROOF STATE]
proof (prove)
using this:
0 < (A1n *v y) $h i
(A1n *v y) $h i \<le> (cc *s y) $h i

goal (1 subgoal):
 1. 0 < cc * y $h i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < cc * y $h ?i12

goal (2 subgoals):
 1. lt_vec 0 y
 2. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
have "y $ i > 0" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < y $h i
[PROOF STEP]
using lt[of i] cc
[PROOF STATE]
proof (prove)
using this:
0 < cc * y $h i
0 < cc

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

goal (2 subgoals):
 1. lt_vec 0 y
 2. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
thus "lt_vec 0 y"
[PROOF STATE]
proof (prove)
using this:
0 < y $h ?i12

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

goal (1 subgoal):
 1. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
assume **: "mu = sr \<or> A *v y = mu *s y"
[PROOF STATE]
proof (state)
this:
mu = sr \<or> A *v y = mu *s y

goal (1 subgoal):
 1. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
mu = sr \<or> A *v y = mu *s y

goal (1 subgoal):
 1. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
assume "A *v y = mu *s y"
[PROOF STATE]
proof (state)
this:
A *v y = mu *s y

goal (1 subgoal):
 1. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
with y
[PROOF STATE]
proof (chain)
picking this:
y \<in> X
A *v y = mu *s y
[PROOF STEP]
have "eigen_vector A y mu"
[PROOF STATE]
proof (prove)
using this:
y \<in> X
A *v y = mu *s y

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

goal (1 subgoal):
 1. y \<noteq> 0 \<and> A *v y = mu *s y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eigen_vector A y mu

goal (1 subgoal):
 1. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
hence "eigen_vector cA (map_vector c y) (c mu)"
[PROOF STATE]
proof (prove)
using this:
eigen_vector A y mu

goal (1 subgoal):
 1. eigen_vector cA (map_vector complex_of_real y) (complex_of_real mu)
[PROOF STEP]
unfolding of_real_hom.eigen_vector_hom
[PROOF STATE]
proof (prove)
using this:
eigen_vector A y mu

goal (1 subgoal):
 1. eigen_vector A y mu
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
eigen_vector cA (map_vector complex_of_real y) (complex_of_real mu)

goal (1 subgoal):
 1. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
from eigen_vector_norm_sr[OF this] *
[PROOF STATE]
proof (chain)
picking this:
cmod (complex_of_real mu) \<le> sr
sr \<le> mu
[PROOF STEP]
have "mu = sr"
[PROOF STATE]
proof (prove)
using this:
cmod (complex_of_real mu) \<le> sr
sr \<le> mu

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

goal (1 subgoal):
 1. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
A *v y = mu *s y \<Longrightarrow> mu = sr

goal (1 subgoal):
 1. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
with **
[PROOF STATE]
proof (chain)
picking this:
mu = sr \<or> A *v y = mu *s y
A *v y = mu *s y \<Longrightarrow> mu = sr
[PROOF STEP]
have mu_sr: "mu = sr"
[PROOF STATE]
proof (prove)
using this:
mu = sr \<or> A *v y = mu *s y
A *v y = mu *s y \<Longrightarrow> mu = sr

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

goal (1 subgoal):
 1. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
from eq1[folded vector_smult_distrib]
[PROOF STATE]
proof (chain)
picking this:
rowvector w *v (sr *s y) = rowvector w *v (A *v y)
[PROOF STEP]
have 0: "?w *v (sr *s y - A *v y) = 0"
[PROOF STATE]
proof (prove)
using this:
rowvector w *v (sr *s y) = rowvector w *v (A *v y)

goal (1 subgoal):
 1. rowvector w *v (sr *s y - A *v y) = 0
[PROOF STEP]
unfolding matrix_vector_right_distrib_diff
[PROOF STATE]
proof (prove)
using this:
rowvector w *v (sr *s y) = rowvector w *v (A *v y)

goal (1 subgoal):
 1. rowvector w *v (sr *s y) - rowvector w *v (A *v y) = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rowvector w *v (sr *s y - A *v y) = 0

goal (1 subgoal):
 1. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
have le0: "le_vec 0 (sr *s y - A *v y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. le_vec 0 (sr *s y - A *v y)
[PROOF STEP]
using assms(2)[unfolded mu_sr]
[PROOF STATE]
proof (prove)
using this:
le_vec (A *v y) (sr *s y)

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

goal (1 subgoal):
 1. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
have "sr *s y - A *v y = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sr *s y - A *v y = 0
[PROOF STEP]
using pos_rowvector_mult_0[OF w(2) 0 le0]
[PROOF STATE]
proof (prove)
using this:
sr *s y - A *v y = 0

goal (1 subgoal):
 1. sr *s y - A *v y = 0
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sr *s y - A *v y = 0

goal (1 subgoal):
 1. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
hence ev_y: "A *v y = sr *s y"
[PROOF STATE]
proof (prove)
using this:
sr *s y - A *v y = 0

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

goal (1 subgoal):
 1. mu = sr \<or> A *v y = mu *s y \<Longrightarrow> mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
show "mu = sr \<and> A *v y = mu *s y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
using ev_y mu_sr
[PROOF STATE]
proof (prove)
using this:
A *v y = sr *s y
mu = sr

goal (1 subgoal):
 1. mu = sr \<and> A *v y = mu *s y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mu = sr \<and> A *v y = mu *s y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nonnegative_eigenvector_has_ev_sr: assumes "eigen_vector A v mu" and le: "le_vec 0 v"
  shows "mu = sr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mu = sr
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mu = sr
[PROOF STEP]
from assms(1)[unfolded eigen_vector_def]
[PROOF STATE]
proof (chain)
picking this:
v \<noteq> 0 \<and> A *v v = mu *s v
[PROOF STEP]
have v: "v \<noteq> 0" and ev: "A *v v = mu *s v"
[PROOF STATE]
proof (prove)
using this:
v \<noteq> 0 \<and> A *v v = mu *s v

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

goal (1 subgoal):
 1. mu = sr
[PROOF STEP]
from le v
[PROOF STATE]
proof (chain)
picking this:
le_vec 0 v
v \<noteq> 0
[PROOF STEP]
have v: "v \<in> X"
[PROOF STATE]
proof (prove)
using this:
le_vec 0 v
v \<noteq> 0

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

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

goal (1 subgoal):
 1. mu = sr
[PROOF STEP]
from ev
[PROOF STATE]
proof (chain)
picking this:
A *v v = mu *s v
[PROOF STEP]
have "le_vec (A *v v) (mu *s v)"
[PROOF STATE]
proof (prove)
using this:
A *v v = mu *s v

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

goal (1 subgoal):
 1. mu = sr
[PROOF STEP]
from le_vec_A_mu[OF v this] ev
[PROOF STATE]
proof (chain)
picking this:
sr \<le> mu
lt_vec 0 v
mu = sr \<or> A *v v = mu *s v \<Longrightarrow> mu = sr \<and> A *v v = mu *s v
A *v v = mu *s v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sr \<le> mu
lt_vec 0 v
mu = sr \<or> A *v v = mu *s v \<Longrightarrow> mu = sr \<and> A *v v = mu *s v
A *v v = mu *s v

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

goal:
No subgoals!
[PROOF STEP]
qed