[STATEMENT]
lemma eventually_subadditiveI:
  assumes "\<And>m n. m > N0 \<Longrightarrow> n > N0 \<Longrightarrow> u (m+n) \<le> u m + u n"
  shows "eventually_subadditive u N0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eventually_subadditive u N0
[PROOF STEP]
unfolding eventually_subadditive_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m>N0. \<forall>n>N0. u (m + n) \<le> u m + u n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>N0 < ?m; N0 < ?n\<rbrakk> \<Longrightarrow> u (?m + ?n) \<le> u ?m + u ?n

goal (1 subgoal):
 1. \<forall>m>N0. \<forall>n>N0. u (m + n) \<le> u m + u n
[PROOF STEP]
by auto


[STATEMENT]
lemma subadditive_imp_eventually_subadditive:
  assumes "subadditive u"
  shows "eventually_subadditive u 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eventually_subadditive u 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
subadditive u

goal (1 subgoal):
 1. eventually_subadditive u 0
[PROOF STEP]
unfolding subadditive_def eventually_subadditive_def
[PROOF STATE]
proof (prove)
using this:
\<forall>m n. u (m + n) \<le> u m + u n

goal (1 subgoal):
 1. \<forall>m>0. \<forall>n>0. u (m + n) \<le> u m + u n
[PROOF STEP]
by auto


[STATEMENT]
lemma eventually_subadditive_ineq:
  assumes "eventually_subadditive u N0" "e>0" "n>N0"
  shows "\<exists>N>N0. \<forall>m\<ge>N. u m/m < u n/n + e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>N>N0. \<forall>m\<ge>N. u m / real m < u n / real n + e
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>N>N0. \<forall>m\<ge>N. u m / real m < u n / real n + e
[PROOF STEP]
have ineq_rec: "u(a*n+r) \<le> a * u n + u r" if "n>N0" "r>N0" for a n r
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u (a * n + r) \<le> real a * u n + u r
[PROOF STEP]
proof (induct a)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. u (0 * n + r) \<le> real 0 * u n + u r
 2. \<And>a. u (a * n + r) \<le> real a * u n + u r \<Longrightarrow> u (Suc a * n + r) \<le> real (Suc a) * u n + u r
[PROOF STEP]
case (Suc a)
[PROOF STATE]
proof (state)
this:
u (a * n + r) \<le> real a * u n + u r

goal (2 subgoals):
 1. u (0 * n + r) \<le> real 0 * u n + u r
 2. \<And>a. u (a * n + r) \<le> real a * u n + u r \<Longrightarrow> u (Suc a * n + r) \<le> real (Suc a) * u n + u r
[PROOF STEP]
have "a*n+r>N0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N0 < a * n + r
[PROOF STEP]
using \<open>r>N0\<close>
[PROOF STATE]
proof (prove)
using this:
N0 < r

goal (1 subgoal):
 1. N0 < a * n + r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
N0 < a * n + r

goal (2 subgoals):
 1. u (0 * n + r) \<le> real 0 * u n + u r
 2. \<And>a. u (a * n + r) \<le> real a * u n + u r \<Longrightarrow> u (Suc a * n + r) \<le> real (Suc a) * u n + u r
[PROOF STEP]
have "u((Suc a)*n+r) = u(a*n+r+n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u (Suc a * n + r) = u (a * n + r + n)
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
u (Suc a * n + r) = u (a * n + r + n)

goal (2 subgoals):
 1. u (0 * n + r) \<le> real 0 * u n + u r
 2. \<And>a. u (a * n + r) \<le> real a * u n + u r \<Longrightarrow> u (Suc a * n + r) \<le> real (Suc a) * u n + u r
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
u (Suc a * n + r) = u (a * n + r + n)

goal (2 subgoals):
 1. u (0 * n + r) \<le> real 0 * u n + u r
 2. \<And>a. u (a * n + r) \<le> real a * u n + u r \<Longrightarrow> u (Suc a * n + r) \<le> real (Suc a) * u n + u r
[PROOF STEP]
have "... \<le> u(a*n+r)+u n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u (a * n + r + n) \<le> u (a * n + r) + u n
[PROOF STEP]
using assms \<open>n>N0\<close> \<open>a*n+r>N0\<close> eventually_subadditive_def
[PROOF STATE]
proof (prove)
using this:
eventually_subadditive u N0
0 < e
N0 < n
N0 < n
N0 < a * n + r
eventually_subadditive ?u ?N0.0 = (\<forall>m>?N0.0. \<forall>n>?N0.0. ?u (m + n) \<le> ?u m + ?u n)

goal (1 subgoal):
 1. u (a * n + r + n) \<le> u (a * n + r) + u n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
u (a * n + r + n) \<le> u (a * n + r) + u n

goal (2 subgoals):
 1. u (0 * n + r) \<le> real 0 * u n + u r
 2. \<And>a. u (a * n + r) \<le> real a * u n + u r \<Longrightarrow> u (Suc a * n + r) \<le> real (Suc a) * u n + u r
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
u (a * n + r + n) \<le> u (a * n + r) + u n

goal (2 subgoals):
 1. u (0 * n + r) \<le> real 0 * u n + u r
 2. \<And>a. u (a * n + r) \<le> real a * u n + u r \<Longrightarrow> u (Suc a * n + r) \<le> real (Suc a) * u n + u r
[PROOF STEP]
have "... \<le> a*u n + u r + u n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u (a * n + r) + u n \<le> real a * u n + u r + u n
[PROOF STEP]
by (simp add: Suc.hyps)
[PROOF STATE]
proof (state)
this:
u (a * n + r) + u n \<le> real a * u n + u r + u n

goal (2 subgoals):
 1. u (0 * n + r) \<le> real 0 * u n + u r
 2. \<And>a. u (a * n + r) \<le> real a * u n + u r \<Longrightarrow> u (Suc a * n + r) \<le> real (Suc a) * u n + u r
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
u (a * n + r) + u n \<le> real a * u n + u r + u n

goal (2 subgoals):
 1. u (0 * n + r) \<le> real 0 * u n + u r
 2. \<And>a. u (a * n + r) \<le> real a * u n + u r \<Longrightarrow> u (Suc a * n + r) \<le> real (Suc a) * u n + u r
[PROOF STEP]
have "... = (Suc a) * u n + u r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real a * u n + u r + u n = real (Suc a) * u n + u r
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
real a * u n + u r + u n = real (Suc a) * u n + u r

goal (2 subgoals):
 1. u (0 * n + r) \<le> real 0 * u n + u r
 2. \<And>a. u (a * n + r) \<le> real a * u n + u r \<Longrightarrow> u (Suc a * n + r) \<le> real (Suc a) * u n + u r
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
u (Suc a * n + r) \<le> real (Suc a) * u n + u r
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
u (Suc a * n + r) \<le> real (Suc a) * u n + u r

goal (1 subgoal):
 1. u (Suc a * n + r) \<le> real (Suc a) * u n + u r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
u (Suc a * n + r) \<le> real (Suc a) * u n + u r

goal (1 subgoal):
 1. u (0 * n + r) \<le> real 0 * u n + u r
[PROOF STEP]
qed (simp)
[PROOF STATE]
proof (state)
this:
\<lbrakk>N0 < ?n; N0 < ?r\<rbrakk> \<Longrightarrow> u (?a * ?n + ?r) \<le> real ?a * u ?n + u ?r

goal (1 subgoal):
 1. \<exists>N>N0. \<forall>m\<ge>N. u m / real m < u n / real n + e
[PROOF STEP]
have "n>0" "real n > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n &&& 0 < real n
[PROOF STEP]
using \<open>n>N0\<close>
[PROOF STATE]
proof (prove)
using this:
N0 < n

goal (1 subgoal):
 1. 0 < n &&& 0 < real n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < n
0 < real n

goal (1 subgoal):
 1. \<exists>N>N0. \<forall>m\<ge>N. u m / real m < u n / real n + e
[PROOF STEP]
define C where "C = Max {abs(u i) |i. i\<le>2*n}"
[PROOF STATE]
proof (state)
this:
C = Max {\<bar>u i\<bar> |i. i \<le> 2 * n}

goal (1 subgoal):
 1. \<exists>N>N0. \<forall>m\<ge>N. u m / real m < u n / real n + e
[PROOF STEP]
have ineq_C: "abs(u i) \<le> C" if "i \<le> 2 * n" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>u i\<bar> \<le> C
[PROOF STEP]
unfolding C_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>u i\<bar> \<le> Max {\<bar>u i\<bar> |i. i \<le> 2 * n}
[PROOF STEP]
by (intro Max_ge, auto simp add: that)
[PROOF STATE]
proof (state)
this:
?i \<le> 2 * n \<Longrightarrow> \<bar>u ?i\<bar> \<le> C

goal (1 subgoal):
 1. \<exists>N>N0. \<forall>m\<ge>N. u m / real m < u n / real n + e
[PROOF STEP]
have ineq_all_m: "u m/m \<le> u n/n + 3*C/m" if "m\<ge>n" for m
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u m / real m \<le> u n / real n + 3 * C / real m
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u m / real m \<le> u n / real n + 3 * C / real m
[PROOF STEP]
have "real m>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < real m
[PROOF STEP]
using \<open>m\<ge>n\<close> \<open>0 < real n\<close>
[PROOF STATE]
proof (prove)
using this:
n \<le> m
0 < real n

goal (1 subgoal):
 1. 0 < real m
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
0 < real m

goal (1 subgoal):
 1. u m / real m \<le> u n / real n + 3 * C / real m
[PROOF STEP]
obtain a0 r0 where "r0<n" "m = a0*n+r0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r0 a0. \<lbrakk>r0 < n; m = a0 * n + r0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>0 < n\<close> mod_div_decomp mod_less_divisor
[PROOF STATE]
proof (prove)
using this:
0 < n
(\<And>q r. \<lbrakk>q = ?a div ?b; r = ?a mod ?b; ?a = q * ?b + r\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
0 < ?n \<Longrightarrow> ?m mod ?n < ?n

goal (1 subgoal):
 1. (\<And>r0 a0. \<lbrakk>r0 < n; m = a0 * n + r0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r0 < n
m = a0 * n + r0

goal (1 subgoal):
 1. u m / real m \<le> u n / real n + 3 * C / real m
[PROOF STEP]
define a where "a = a0-1"
[PROOF STATE]
proof (state)
this:
a = a0 - 1

goal (1 subgoal):
 1. u m / real m \<le> u n / real n + 3 * C / real m
[PROOF STEP]
define r where "r = r0+n"
[PROOF STATE]
proof (state)
this:
r = r0 + n

goal (1 subgoal):
 1. u m / real m \<le> u n / real n + 3 * C / real m
[PROOF STEP]
have "r<2*n" "r\<ge>n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r < 2 * n &&& n \<le> r
[PROOF STEP]
unfolding r_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r0 + n < 2 * n &&& n \<le> r0 + n
[PROOF STEP]
by (auto simp add: \<open>r0<n\<close>)
[PROOF STATE]
proof (state)
this:
r < 2 * n
n \<le> r

goal (1 subgoal):
 1. u m / real m \<le> u n / real n + 3 * C / real m
[PROOF STEP]
have "a0>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < a0
[PROOF STEP]
using \<open>m = a0*n + r0\<close> \<open>n \<le> m\<close> \<open>r0 < n\<close> not_le
[PROOF STATE]
proof (prove)
using this:
m = a0 * n + r0
n \<le> m
r0 < n
(\<not> ?x \<le> ?y) = (?y < ?x)

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

goal (1 subgoal):
 1. u m / real m \<le> u n / real n + 3 * C / real m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < a0
[PROOF STEP]
have "m = a * n + r"
[PROOF STATE]
proof (prove)
using this:
0 < a0

goal (1 subgoal):
 1. m = a * n + r
[PROOF STEP]
using a_def r_def \<open>m = a0*n+r0\<close> mult_eq_if
[PROOF STATE]
proof (prove)
using this:
0 < a0
a = a0 - 1
r = r0 + n
m = a0 * n + r0
?m * ?n = (if ?m = 0 then 0 else ?n + (?m - 1) * ?n)

goal (1 subgoal):
 1. m = a * n + r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m = a * n + r

goal (1 subgoal):
 1. u m / real m \<le> u n / real n + 3 * C / real m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m = a * n + r
[PROOF STEP]
have real_eq: "-r = real n * a - m"
[PROOF STATE]
proof (prove)
using this:
m = a * n + r

goal (1 subgoal):
 1. real_of_int (- int r) = real n * real a - real m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real_of_int (- int r) = real n * real a - real m

goal (1 subgoal):
 1. u m / real m \<le> u n / real n + 3 * C / real m
[PROOF STEP]
have "r>N0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N0 < r
[PROOF STEP]
using \<open>r\<ge>n\<close> \<open>n>N0\<close>
[PROOF STATE]
proof (prove)
using this:
n \<le> r
N0 < n

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

goal (1 subgoal):
 1. u m / real m \<le> u n / real n + 3 * C / real m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
N0 < r
[PROOF STEP]
have "u m \<le> a * u n + u r"
[PROOF STATE]
proof (prove)
using this:
N0 < r

goal (1 subgoal):
 1. u m \<le> real a * u n + u r
[PROOF STEP]
using ineq_rec \<open>m = a*n+r\<close> \<open>n>N0\<close>
[PROOF STATE]
proof (prove)
using this:
N0 < r
\<lbrakk>N0 < ?n; N0 < ?r\<rbrakk> \<Longrightarrow> u (?a * ?n + ?r) \<le> real ?a * u ?n + u ?r
m = a * n + r
N0 < n

goal (1 subgoal):
 1. u m \<le> real a * u n + u r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
u m \<le> real a * u n + u r

goal (1 subgoal):
 1. u m / real m \<le> u n / real n + 3 * C / real m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u m \<le> real a * u n + u r
[PROOF STEP]
have "n * u m \<le> n * (a * u n + u r)"
[PROOF STATE]
proof (prove)
using this:
u m \<le> real a * u n + u r

goal (1 subgoal):
 1. real n * u m \<le> real n * (real a * u n + u r)
[PROOF STEP]
using \<open>real n>0\<close>
[PROOF STATE]
proof (prove)
using this:
u m \<le> real a * u n + u r
0 < real n

goal (1 subgoal):
 1. real n * u m \<le> real n * (real a * u n + u r)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real n * u m \<le> real n * (real a * u n + u r)

goal (1 subgoal):
 1. u m / real m \<le> u n / real n + 3 * C / real m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
real n * u m \<le> real n * (real a * u n + u r)
[PROOF STEP]
have "n * u m - m * u n \<le> -r * u n + n * u r"
[PROOF STATE]
proof (prove)
using this:
real n * u m \<le> real n * (real a * u n + u r)

goal (1 subgoal):
 1. real n * u m - real m * u n \<le> real_of_int (- int r) * u n + real n * u r
[PROOF STEP]
unfolding real_eq
[PROOF STATE]
proof (prove)
using this:
real n * u m \<le> real n * (real a * u n + u r)

goal (1 subgoal):
 1. real n * u m - real m * u n \<le> (real n * real a - real m) * u n + real n * u r
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
real n * u m - real m * u n \<le> real_of_int (- int r) * u n + real n * u r

goal (1 subgoal):
 1. u m / real m \<le> u n / real n + 3 * C / real m
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real n * u m - real m * u n \<le> real_of_int (- int r) * u n + real n * u r

goal (1 subgoal):
 1. u m / real m \<le> u n / real n + 3 * C / real m
[PROOF STEP]
have "... \<le> r * abs(u n) + n * abs(u r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (- int r) * u n + real n * u r \<le> real r * \<bar>u n\<bar> + real n * \<bar>u r\<bar>
[PROOF STEP]
apply (intro add_mono mult_left_mono)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. real_of_int (- int r) * u n \<le> real r * \<bar>u n\<bar>
 2. u r \<le> \<bar>u r\<bar>
 3. 0 \<le> real n
[PROOF STEP]
using real_0_le_add_iff
[PROOF STATE]
proof (prove)
using this:
(0 \<le> ?x + ?y) = (- ?x \<le> ?y)

goal (3 subgoals):
 1. real_of_int (- int r) * u n \<le> real r * \<bar>u n\<bar>
 2. u r \<le> \<bar>u r\<bar>
 3. 0 \<le> real n
[PROOF STEP]
by fastforce+
[PROOF STATE]
proof (state)
this:
real_of_int (- int r) * u n + real n * u r \<le> real r * \<bar>u n\<bar> + real n * \<bar>u r\<bar>

goal (1 subgoal):
 1. u m / real m \<le> u n / real n + 3 * C / real m
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real_of_int (- int r) * u n + real n * u r \<le> real r * \<bar>u n\<bar> + real n * \<bar>u r\<bar>

goal (1 subgoal):
 1. u m / real m \<le> u n / real n + 3 * C / real m
[PROOF STEP]
have "... \<le> (2 * n) * C + n * C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real r * \<bar>u n\<bar> + real n * \<bar>u r\<bar> \<le> real (2 * n) * C + real n * C
[PROOF STEP]
apply (intro add_mono mult_mono ineq_C)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. real r \<le> real (2 * n)
 2. n \<le> 2 * n
 3. 0 \<le> real (2 * n)
 4. 0 \<le> \<bar>u n\<bar>
 5. real n \<le> real n
 6. r \<le> 2 * n
 7. 0 \<le> real n
 8. 0 \<le> \<bar>u r\<bar>
[PROOF STEP]
using less_imp_le[OF \<open>r < 2 * n\<close>]
[PROOF STATE]
proof (prove)
using this:
r \<le> 2 * n

goal (8 subgoals):
 1. real r \<le> real (2 * n)
 2. n \<le> 2 * n
 3. 0 \<le> real (2 * n)
 4. 0 \<le> \<bar>u n\<bar>
 5. real n \<le> real n
 6. r \<le> 2 * n
 7. 0 \<le> real n
 8. 0 \<le> \<bar>u r\<bar>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real r * \<bar>u n\<bar> + real n * \<bar>u r\<bar> \<le> real (2 * n) * C + real n * C

goal (1 subgoal):
 1. u m / real m \<le> u n / real n + 3 * C / real m
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
real n * u m - real m * u n \<le> real (2 * n) * C + real n * C
[PROOF STEP]
have "n * u m - m * u n \<le> 3*C*n"
[PROOF STATE]
proof (prove)
using this:
real n * u m - real m * u n \<le> real (2 * n) * C + real n * C

goal (1 subgoal):
 1. real n * u m - real m * u n \<le> 3 * C * real n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real n * u m - real m * u n \<le> 3 * C * real n

goal (1 subgoal):
 1. u m / real m \<le> u n / real n + 3 * C / real m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
real n * u m - real m * u n \<le> 3 * C * real n
[PROOF STEP]
show "u m/m \<le> u n/n + 3*C/m"
[PROOF STATE]
proof (prove)
using this:
real n * u m - real m * u n \<le> 3 * C * real n

goal (1 subgoal):
 1. u m / real m \<le> u n / real n + 3 * C / real m
[PROOF STEP]
using \<open>0 < real n\<close> \<open>0 < real m\<close>
[PROOF STATE]
proof (prove)
using this:
real n * u m - real m * u n \<le> 3 * C * real n
0 < real n
0 < real m

goal (1 subgoal):
 1. u m / real m \<le> u n / real n + 3 * C / real m
[PROOF STEP]
by (simp add: divide_simps mult.commute)
[PROOF STATE]
proof (state)
this:
u m / real m \<le> u n / real n + 3 * C / real m

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n \<le> ?m \<Longrightarrow> u ?m / real ?m \<le> u n / real n + 3 * C / real ?m

goal (1 subgoal):
 1. \<exists>N>N0. \<forall>m\<ge>N. u m / real m < u n / real n + e
[PROOF STEP]
obtain M::nat where M: "M \<ge> 3 * C / e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>M. 3 * C / e \<le> real M \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using real_nat_ceiling_ge
[PROOF STATE]
proof (prove)
using this:
?x \<le> real (nat \<lceil>?x\<rceil>)

goal (1 subgoal):
 1. (\<And>M. 3 * C / e \<le> real M \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
3 * C / e \<le> real M

goal (1 subgoal):
 1. \<exists>N>N0. \<forall>m\<ge>N. u m / real m < u n / real n + e
[PROOF STEP]
define N where "N = M + n + N0 + 1"
[PROOF STATE]
proof (state)
this:
N = M + n + N0 + 1

goal (1 subgoal):
 1. \<exists>N>N0. \<forall>m\<ge>N. u m / real m < u n / real n + e
[PROOF STEP]
have "N > 3 * C / e" "N \<ge> n" "N > N0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 3 * C / e < real N &&& n \<le> N &&& N0 < N
[PROOF STEP]
unfolding N_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 3 * C / e < real (M + n + N0 + 1) &&& n \<le> M + n + N0 + 1 &&& N0 < M + n + N0 + 1
[PROOF STEP]
using M
[PROOF STATE]
proof (prove)
using this:
3 * C / e \<le> real M

goal (1 subgoal):
 1. 3 * C / e < real (M + n + N0 + 1) &&& n \<le> M + n + N0 + 1 &&& N0 < M + n + N0 + 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
3 * C / e < real N
n \<le> N
N0 < N

goal (1 subgoal):
 1. \<exists>N>N0. \<forall>m\<ge>N. u m / real m < u n / real n + e
[PROOF STEP]
have "u m/m < u n/n + e" if "m \<ge> N" for m
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u m / real m < u n / real n + e
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u m / real m < u n / real n + e
[PROOF STEP]
have "3 * C / m < e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 3 * C / real m < e
[PROOF STEP]
using that \<open>N > 3 * C / e\<close> \<open>e > 0\<close>
[PROOF STATE]
proof (prove)
using this:
N \<le> m
3 * C / e < real N
0 < e

goal (1 subgoal):
 1. 3 * C / real m < e
[PROOF STEP]
apply (auto simp add: algebra_simps divide_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>N \<le> m; C * 3 < e * real N; 0 < e; 0 < m\<rbrakk> \<Longrightarrow> C * 3 < e * real m
[PROOF STEP]
by (meson le_less_trans linorder_not_le mult_less_cancel_left_pos of_nat_less_iff)
[PROOF STATE]
proof (state)
this:
3 * C / real m < e

goal (1 subgoal):
 1. u m / real m < u n / real n + e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
3 * C / real m < e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
3 * C / real m < e

goal (1 subgoal):
 1. u m / real m < u n / real n + e
[PROOF STEP]
using ineq_all_m[of m] \<open>n \<le> N\<close> \<open>N \<le> m\<close>
[PROOF STATE]
proof (prove)
using this:
3 * C / real m < e
n \<le> m \<Longrightarrow> u m / real m \<le> u n / real n + 3 * C / real m
n \<le> N
N \<le> m

goal (1 subgoal):
 1. u m / real m < u n / real n + e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u m / real m < u n / real n + e

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
N \<le> ?m \<Longrightarrow> u ?m / real ?m < u n / real n + e

goal (1 subgoal):
 1. \<exists>N>N0. \<forall>m\<ge>N. u m / real m < u n / real n + e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
N \<le> ?m \<Longrightarrow> u ?m / real ?m < u n / real n + e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
N \<le> ?m \<Longrightarrow> u ?m / real ?m < u n / real n + e

goal (1 subgoal):
 1. \<exists>N>N0. \<forall>m\<ge>N. u m / real m < u n / real n + e
[PROOF STEP]
using \<open>N0 < N\<close>
[PROOF STATE]
proof (prove)
using this:
N \<le> ?m \<Longrightarrow> u ?m / real ?m < u n / real n + e
N0 < N

goal (1 subgoal):
 1. \<exists>N>N0. \<forall>m\<ge>N. u m / real m < u n / real n + e
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>N>N0. \<forall>m\<ge>N. u m / real m < u n / real n + e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subadditive_converges_ereal':
  assumes "eventually_subadditive u N0"
  shows "(\<lambda>m. ereal(u m/m)) \<longlonglongrightarrow> Inf {ereal(u n/n) | n. n>N0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>m. ereal (u m / real m)) \<longlonglongrightarrow> Inf {ereal (u n / real n) |n. N0 < n}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>m. ereal (u m / real m)) \<longlonglongrightarrow> Inf {ereal (u n / real n) |n. N0 < n}
[PROOF STEP]
define v where "v = (\<lambda>m. ereal(u m/m))"
[PROOF STATE]
proof (state)
this:
v = (\<lambda>m. ereal (u m / real m))

goal (1 subgoal):
 1. (\<lambda>m. ereal (u m / real m)) \<longlonglongrightarrow> Inf {ereal (u n / real n) |n. N0 < n}
[PROOF STEP]
define V where "V = {v n | n. n>N0}"
[PROOF STATE]
proof (state)
this:
V = {v n |n. N0 < n}

goal (1 subgoal):
 1. (\<lambda>m. ereal (u m / real m)) \<longlonglongrightarrow> Inf {ereal (u n / real n) |n. N0 < n}
[PROOF STEP]
define l where "l = Inf V"
[PROOF STATE]
proof (state)
this:
l = Inf V

goal (1 subgoal):
 1. (\<lambda>m. ereal (u m / real m)) \<longlonglongrightarrow> Inf {ereal (u n / real n) |n. N0 < n}
[PROOF STEP]
have "\<And>t. t\<in>V \<Longrightarrow> t\<ge>l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. t \<in> V \<Longrightarrow> l \<le> t
[PROOF STEP]
by (simp add: Inf_lower l_def)
[PROOF STATE]
proof (state)
this:
?t \<in> V \<Longrightarrow> l \<le> ?t

goal (1 subgoal):
 1. (\<lambda>m. ereal (u m / real m)) \<longlonglongrightarrow> Inf {ereal (u n / real n) |n. N0 < n}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?t \<in> V \<Longrightarrow> l \<le> ?t
[PROOF STEP]
have "v n \<ge> l" if "n > N0" for n
[PROOF STATE]
proof (prove)
using this:
?t \<in> V \<Longrightarrow> l \<le> ?t

goal (1 subgoal):
 1. l \<le> v n
[PROOF STEP]
using V_def that
[PROOF STATE]
proof (prove)
using this:
?t \<in> V \<Longrightarrow> l \<le> ?t
V = {v n |n. N0 < n}
N0 < n

goal (1 subgoal):
 1. l \<le> v n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
N0 < ?n \<Longrightarrow> l \<le> v ?n

goal (1 subgoal):
 1. (\<lambda>m. ereal (u m / real m)) \<longlonglongrightarrow> Inf {ereal (u n / real n) |n. N0 < n}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
N0 < ?n \<Longrightarrow> l \<le> v ?n
[PROOF STEP]
have lower: "eventually (\<lambda>n. a < v n) sequentially" if "a < l" for a
[PROOF STATE]
proof (prove)
using this:
N0 < ?n \<Longrightarrow> l \<le> v ?n

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. a < v n
[PROOF STEP]
by (meson that dual_order.strict_trans1 eventually_at_top_dense)
[PROOF STATE]
proof (state)
this:
?a < l \<Longrightarrow> \<forall>\<^sub>F n in sequentially. ?a < v n

goal (1 subgoal):
 1. (\<lambda>m. ereal (u m / real m)) \<longlonglongrightarrow> Inf {ereal (u n / real n) |n. N0 < n}
[PROOF STEP]
have upper: "eventually (\<lambda>n. a > v n) sequentially" if "a > l" for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. v n < a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. v n < a
[PROOF STEP]
obtain t where "t\<in>V" "t<a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t. \<lbrakk>t \<in> V; t < a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis \<open>a>l\<close> Inf_greatest l_def not_le)
[PROOF STATE]
proof (state)
this:
t \<in> V
t < a

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. v n < a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<in> V
t < a
[PROOF STEP]
obtain e::real where "e>0" "t+e < a"
[PROOF STATE]
proof (prove)
using this:
t \<in> V
t < a

goal (1 subgoal):
 1. (\<And>e. \<lbrakk>0 < e; t + ereal e < a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson ereal_le_epsilon2 leD le_less_linear)
[PROOF STATE]
proof (state)
this:
0 < e
t + ereal e < a

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. v n < a
[PROOF STEP]
obtain n where "n>N0" "t = u n/n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. \<lbrakk>N0 < n; t = ereal (u n / real n)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using V_def v_def \<open>t \<in> V\<close>
[PROOF STATE]
proof (prove)
using this:
V = {v n |n. N0 < n}
v = (\<lambda>m. ereal (u m / real m))
t \<in> V

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>N0 < n; t = ereal (u n / real n)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
N0 < n
t = ereal (u n / real n)

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. v n < a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
N0 < n
t = ereal (u n / real n)
[PROOF STEP]
have "u n/n + e < a"
[PROOF STATE]
proof (prove)
using this:
N0 < n
t = ereal (u n / real n)

goal (1 subgoal):
 1. ereal (u n / real n + e) < a
[PROOF STEP]
using \<open>t+e < a\<close>
[PROOF STATE]
proof (prove)
using this:
N0 < n
t = ereal (u n / real n)
t + ereal e < a

goal (1 subgoal):
 1. ereal (u n / real n + e) < a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ereal (u n / real n + e) < a

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. v n < a
[PROOF STEP]
obtain N where "\<forall>m\<ge>N. u m/m < u n/n + e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>N. \<forall>m\<ge>N. u m / real m < u n / real n + e \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eventually_subadditive_ineq[OF assms] \<open>0 < e\<close> \<open>N0 < n\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < ?e; N0 < ?n\<rbrakk> \<Longrightarrow> \<exists>N>N0. \<forall>m\<ge>N. u m / real m < u ?n / real ?n + ?e
0 < e
N0 < n

goal (1 subgoal):
 1. (\<And>N. \<forall>m\<ge>N. u m / real m < u n / real n + e \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>m\<ge>N. u m / real m < u n / real n + e

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. v n < a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>m\<ge>N. u m / real m < u n / real n + e
[PROOF STEP]
have "u m/m < a" if "m \<ge> N" for m
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<ge>N. u m / real m < u n / real n + e

goal (1 subgoal):
 1. ereal (u m / real m) < a
[PROOF STEP]
using that \<open>u n/n + e < a\<close> less_ereal.simps(1) less_trans
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<ge>N. u m / real m < u n / real n + e
N \<le> m
ereal (u n / real n + e) < a
(ereal ?x < ereal ?y) = (?x < ?y)
\<lbrakk>?x < ?y; ?y < ?z\<rbrakk> \<Longrightarrow> ?x < ?z

goal (1 subgoal):
 1. ereal (u m / real m) < a
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
N \<le> ?m \<Longrightarrow> ereal (u ?m / real ?m) < a

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. v n < a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
N \<le> ?m \<Longrightarrow> ereal (u ?m / real ?m) < a
[PROOF STEP]
have "v m< a" if "m \<ge> N" for m
[PROOF STATE]
proof (prove)
using this:
N \<le> ?m \<Longrightarrow> ereal (u ?m / real ?m) < a

goal (1 subgoal):
 1. v m < a
[PROOF STEP]
using v_def that
[PROOF STATE]
proof (prove)
using this:
N \<le> ?m \<Longrightarrow> ereal (u ?m / real ?m) < a
v = (\<lambda>m. ereal (u m / real m))
N \<le> m

goal (1 subgoal):
 1. v m < a
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
N \<le> ?m \<Longrightarrow> v ?m < a

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. v n < a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
N \<le> ?m \<Longrightarrow> v ?m < a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
N \<le> ?m \<Longrightarrow> v ?m < a

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. v n < a
[PROOF STEP]
using eventually_at_top_linorder
[PROOF STATE]
proof (prove)
using this:
N \<le> ?m \<Longrightarrow> v ?m < a
eventually ?P at_top = (\<exists>N. \<forall>n\<ge>N. ?P n)

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. v n < a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. v n < a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
l < ?a \<Longrightarrow> \<forall>\<^sub>F n in sequentially. v n < ?a

goal (1 subgoal):
 1. (\<lambda>m. ereal (u m / real m)) \<longlonglongrightarrow> Inf {ereal (u n / real n) |n. N0 < n}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>m. ereal (u m / real m)) \<longlonglongrightarrow> Inf {ereal (u n / real n) |n. N0 < n}
[PROOF STEP]
using lower upper
[PROOF STATE]
proof (prove)
using this:
?a < l \<Longrightarrow> \<forall>\<^sub>F n in sequentially. ?a < v n
l < ?a \<Longrightarrow> \<forall>\<^sub>F n in sequentially. v n < ?a

goal (1 subgoal):
 1. (\<lambda>m. ereal (u m / real m)) \<longlonglongrightarrow> Inf {ereal (u n / real n) |n. N0 < n}
[PROOF STEP]
unfolding V_def l_def v_def
[PROOF STATE]
proof (prove)
using this:
?a < Inf {ereal (u n / real n) |n. N0 < n} \<Longrightarrow> \<forall>\<^sub>F n in sequentially. ?a < ereal (u n / real n)
Inf {ereal (u n / real n) |n. N0 < n} < ?a \<Longrightarrow> \<forall>\<^sub>F n in sequentially. ereal (u n / real n) < ?a

goal (1 subgoal):
 1. (\<lambda>m. ereal (u m / real m)) \<longlonglongrightarrow> Inf {ereal (u n / real n) |n. N0 < n}
[PROOF STEP]
by (simp add: order_tendsto_iff)
[PROOF STATE]
proof (state)
this:
(\<lambda>m. ereal (u m / real m)) \<longlonglongrightarrow> Inf {ereal (u n / real n) |n. N0 < n}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subadditive_converges_ereal:
  assumes "subadditive u"
  shows "(\<lambda>m. ereal(u m/m)) \<longlonglongrightarrow> Inf {ereal(u n/n) | n. n>0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>m. ereal (u m / real m)) \<longlonglongrightarrow> Inf {ereal (u n / real n) |n. 0 < n}
[PROOF STEP]
by (rule subadditive_converges_ereal'[OF subadditive_imp_eventually_subadditive[OF assms]])


[STATEMENT]
lemma subadditive_converges_bounded':
  assumes "eventually_subadditive u N0"
          "bdd_below {u n/n | n. n>N0}"
  shows "(\<lambda>n. u n/n) \<longlonglongrightarrow> Inf {u n/n | n. n>N0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. u n / real n) \<longlonglongrightarrow> Inf {u n / real n |n. N0 < n}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>n. u n / real n) \<longlonglongrightarrow> Inf {u n / real n |n. N0 < n}
[PROOF STEP]
have *: "(\<lambda>n. ereal(u n /n)) \<longlonglongrightarrow> Inf {ereal(u n/n)|n. n > N0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. ereal (u n / real n)) \<longlonglongrightarrow> Inf {ereal (u n / real n) |n. N0 < n}
[PROOF STEP]
by (simp add: assms(1) subadditive_converges_ereal')
[PROOF STATE]
proof (state)
this:
(\<lambda>n. ereal (u n / real n)) \<longlonglongrightarrow> Inf {ereal (u n / real n) |n. N0 < n}

goal (1 subgoal):
 1. (\<lambda>n. u n / real n) \<longlonglongrightarrow> Inf {u n / real n |n. N0 < n}
[PROOF STEP]
define V where "V = {u n/n | n. n>N0}"
[PROOF STATE]
proof (state)
this:
V = {u n / real n |n. N0 < n}

goal (1 subgoal):
 1. (\<lambda>n. u n / real n) \<longlonglongrightarrow> Inf {u n / real n |n. N0 < n}
[PROOF STEP]
have a: "bdd_below V" "V\<noteq>{}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_below V &&& V \<noteq> {}
[PROOF STEP]
by (auto simp add: V_def assms(2))
[PROOF STATE]
proof (state)
this:
bdd_below V
V \<noteq> {}

goal (1 subgoal):
 1. (\<lambda>n. u n / real n) \<longlonglongrightarrow> Inf {u n / real n |n. N0 < n}
[PROOF STEP]
have "Inf {ereal(t)| t. t\<in>V} = ereal(Inf V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inf {ereal t |t. t \<in> V} = ereal (Inf V)
[PROOF STEP]
by (subst ereal_Inf'[OF a], simp add: Setcompr_eq_image)
[PROOF STATE]
proof (state)
this:
Inf {ereal t |t. t \<in> V} = ereal (Inf V)

goal (1 subgoal):
 1. (\<lambda>n. u n / real n) \<longlonglongrightarrow> Inf {u n / real n |n. N0 < n}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Inf {ereal t |t. t \<in> V} = ereal (Inf V)

goal (1 subgoal):
 1. (\<lambda>n. u n / real n) \<longlonglongrightarrow> Inf {u n / real n |n. N0 < n}
[PROOF STEP]
have "{ereal(t)| t. t\<in>V} = {ereal(u n/n)|n. n > N0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {ereal t |t. t \<in> V} = {ereal (u n / real n) |n. N0 < n}
[PROOF STEP]
using V_def
[PROOF STATE]
proof (prove)
using this:
V = {u n / real n |n. N0 < n}

goal (1 subgoal):
 1. {ereal t |t. t \<in> V} = {ereal (u n / real n) |n. N0 < n}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{ereal t |t. t \<in> V} = {ereal (u n / real n) |n. N0 < n}

goal (1 subgoal):
 1. (\<lambda>n. u n / real n) \<longlonglongrightarrow> Inf {u n / real n |n. N0 < n}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Inf {ereal t |t. t \<in> V} = ereal (Inf V)
{ereal t |t. t \<in> V} = {ereal (u n / real n) |n. N0 < n}
[PROOF STEP]
have "Inf {ereal(u n/n)|n. n > N0} = ereal(Inf {u n/n |n. n > N0})"
[PROOF STATE]
proof (prove)
using this:
Inf {ereal t |t. t \<in> V} = ereal (Inf V)
{ereal t |t. t \<in> V} = {ereal (u n / real n) |n. N0 < n}

goal (1 subgoal):
 1. Inf {ereal (u n / real n) |n. N0 < n} = ereal (Inf {u n / real n |n. N0 < n})
[PROOF STEP]
using V_def
[PROOF STATE]
proof (prove)
using this:
Inf {ereal t |t. t \<in> V} = ereal (Inf V)
{ereal t |t. t \<in> V} = {ereal (u n / real n) |n. N0 < n}
V = {u n / real n |n. N0 < n}

goal (1 subgoal):
 1. Inf {ereal (u n / real n) |n. N0 < n} = ereal (Inf {u n / real n |n. N0 < n})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Inf {ereal (u n / real n) |n. N0 < n} = ereal (Inf {u n / real n |n. N0 < n})

goal (1 subgoal):
 1. (\<lambda>n. u n / real n) \<longlonglongrightarrow> Inf {u n / real n |n. N0 < n}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Inf {ereal (u n / real n) |n. N0 < n} = ereal (Inf {u n / real n |n. N0 < n})
[PROOF STEP]
have "(\<lambda>n. ereal(u n /n)) \<longlonglongrightarrow> ereal(Inf {u n/n | n. n>N0})"
[PROOF STATE]
proof (prove)
using this:
Inf {ereal (u n / real n) |n. N0 < n} = ereal (Inf {u n / real n |n. N0 < n})

goal (1 subgoal):
 1. (\<lambda>n. ereal (u n / real n)) \<longlonglongrightarrow> ereal (Inf {u n / real n |n. N0 < n})
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
Inf {ereal (u n / real n) |n. N0 < n} = ereal (Inf {u n / real n |n. N0 < n})
(\<lambda>n. ereal (u n / real n)) \<longlonglongrightarrow> Inf {ereal (u n / real n) |n. N0 < n}

goal (1 subgoal):
 1. (\<lambda>n. ereal (u n / real n)) \<longlonglongrightarrow> ereal (Inf {u n / real n |n. N0 < n})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. ereal (u n / real n)) \<longlonglongrightarrow> ereal (Inf {u n / real n |n. N0 < n})

goal (1 subgoal):
 1. (\<lambda>n. u n / real n) \<longlonglongrightarrow> Inf {u n / real n |n. N0 < n}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. ereal (u n / real n)) \<longlonglongrightarrow> ereal (Inf {u n / real n |n. N0 < n})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. ereal (u n / real n)) \<longlonglongrightarrow> ereal (Inf {u n / real n |n. N0 < n})

goal (1 subgoal):
 1. (\<lambda>n. u n / real n) \<longlonglongrightarrow> Inf {u n / real n |n. N0 < n}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>n. u n / real n) \<longlonglongrightarrow> Inf {u n / real n |n. N0 < n}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subadditive_converges_bounded:
  assumes "subadditive u"
          "bdd_below {u n/n | n. n>0}"
  shows "(\<lambda>n. u n/n) \<longlonglongrightarrow> Inf {u n/n | n. n>0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. u n / real n) \<longlonglongrightarrow> Inf {u n / real n |n. 0 < n}
[PROOF STEP]
by (rule subadditive_converges_bounded'[OF subadditive_imp_eventually_subadditive[OF assms(1)] assms(2)])


[STATEMENT]
lemma subadditive_converges_bounded'':
  assumes "subadditive u"
          "\<And>n. n > 0 \<Longrightarrow> u n \<ge> n * (a::real)"
  shows "\<exists>l. (\<lambda>n. u n / n) \<longlonglongrightarrow> l \<and> (\<forall>n>0. u n \<ge> n * l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l. (\<lambda>n. u n / real n) \<longlonglongrightarrow> l \<and> (\<forall>n>0. real n * l \<le> u n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>l. (\<lambda>n. u n / real n) \<longlonglongrightarrow> l \<and> (\<forall>n>0. real n * l \<le> u n)
[PROOF STEP]
have B: "bdd_below {u n/n | n. n>0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_below {u n / real n |n. 0 < n}
[PROOF STEP]
apply (rule bdd_belowI[of _ a])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {u n / real n |n. 0 < n} \<Longrightarrow> a \<le> x
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
0 < ?n \<Longrightarrow> real ?n * a \<le> u ?n

goal (1 subgoal):
 1. \<And>x. x \<in> {u n / real n |n. 0 < n} \<Longrightarrow> a \<le> x
[PROOF STEP]
apply (auto simp add: divide_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x n. \<lbrakk>\<And>n. 0 < n \<Longrightarrow> real n * a \<le> u n; x * real n = u n; 0 < n\<rbrakk> \<Longrightarrow> a \<le> x
[PROOF STEP]
apply (metis mult.commute mult_left_le_imp_le of_nat_0_less_iff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
bdd_below {u n / real n |n. 0 < n}

goal (1 subgoal):
 1. \<exists>l. (\<lambda>n. u n / real n) \<longlonglongrightarrow> l \<and> (\<forall>n>0. real n * l \<le> u n)
[PROOF STEP]
define l where "l = Inf {u n/n | n. n>0}"
[PROOF STATE]
proof (state)
this:
l = Inf {u n / real n |n. 0 < n}

goal (1 subgoal):
 1. \<exists>l. (\<lambda>n. u n / real n) \<longlonglongrightarrow> l \<and> (\<forall>n>0. real n * l \<le> u n)
[PROOF STEP]
have *: "u n / n \<ge> l" if "n > 0" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<le> u n / real n
[PROOF STEP]
unfolding l_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inf {u n / real n |n. 0 < n} \<le> u n / real n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. Inf {u n / real n |n. 0 < n} \<le> u n / real n
[PROOF STEP]
by (auto intro!: cInf_lower[OF _ B])
[PROOF STATE]
proof (state)
this:
0 < ?n \<Longrightarrow> l \<le> u ?n / real ?n

goal (1 subgoal):
 1. \<exists>l. (\<lambda>n. u n / real n) \<longlonglongrightarrow> l \<and> (\<forall>n>0. real n * l \<le> u n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l. (\<lambda>n. u n / real n) \<longlonglongrightarrow> l \<and> (\<forall>n>0. real n * l \<le> u n)
[PROOF STEP]
apply (rule exI[of _ l], auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<lambda>n. u n / real n) \<longlonglongrightarrow> l
 2. \<And>n. 0 < n \<Longrightarrow> real n * l \<le> u n
[PROOF STEP]
using subadditive_converges_bounded[OF assms(1) B]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. u n / real n) \<longlonglongrightarrow> Inf {u n / real n |n. 0 < n}

goal (2 subgoals):
 1. (\<lambda>n. u n / real n) \<longlonglongrightarrow> l
 2. \<And>n. 0 < n \<Longrightarrow> real n * l \<le> u n
[PROOF STEP]
apply (simp add: l_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. 0 < n \<Longrightarrow> real n * l \<le> u n
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
0 < ?n \<Longrightarrow> l \<le> u ?n / real ?n

goal (1 subgoal):
 1. \<And>n. 0 < n \<Longrightarrow> real n * l \<le> u n
[PROOF STEP]
by (simp add: divide_simps algebra_simps)
[PROOF STATE]
proof (state)
this:
\<exists>l. (\<lambda>n. u n / real n) \<longlonglongrightarrow> l \<and> (\<forall>n>0. real n * l \<le> u n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subadditive_converges_unbounded':
  assumes "eventually_subadditive u N0"
          "\<not> (bdd_below {u n/n | n. n>N0})"
  shows "(\<lambda>n. ereal(u n/n)) \<longlonglongrightarrow> -\<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. ereal (u n / real n)) \<longlonglongrightarrow> - \<infinity>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>n. ereal (u n / real n)) \<longlonglongrightarrow> - \<infinity>
[PROOF STEP]
have *: "(\<lambda>n. ereal(u n /n)) \<longlonglongrightarrow> Inf {ereal(u n/n)|n. n > N0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. ereal (u n / real n)) \<longlonglongrightarrow> Inf {ereal (u n / real n) |n. N0 < n}
[PROOF STEP]
by (simp add: assms(1) subadditive_converges_ereal')
[PROOF STATE]
proof (state)
this:
(\<lambda>n. ereal (u n / real n)) \<longlonglongrightarrow> Inf {ereal (u n / real n) |n. N0 < n}

goal (1 subgoal):
 1. (\<lambda>n. ereal (u n / real n)) \<longlonglongrightarrow> - \<infinity>
[PROOF STEP]
define V where "V = {u n/n | n. n>N0}"
[PROOF STATE]
proof (state)
this:
V = {u n / real n |n. N0 < n}

goal (1 subgoal):
 1. (\<lambda>n. ereal (u n / real n)) \<longlonglongrightarrow> - \<infinity>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
V = {u n / real n |n. N0 < n}
[PROOF STEP]
have "\<not> bdd_below V"
[PROOF STATE]
proof (prove)
using this:
V = {u n / real n |n. N0 < n}

goal (1 subgoal):
 1. \<not> bdd_below V
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
V = {u n / real n |n. N0 < n}
eventually_subadditive u N0
\<not> bdd_below {u n / real n |n. N0 < n}

goal (1 subgoal):
 1. \<not> bdd_below V
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> bdd_below V

goal (1 subgoal):
 1. (\<lambda>n. ereal (u n / real n)) \<longlonglongrightarrow> - \<infinity>
[PROOF STEP]
have "Inf {ereal(t) | t. t\<in>V} = -\<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inf {ereal t |t. t \<in> V} = - \<infinity>
[PROOF STEP]
by (rule ereal_bot, metis (mono_tags, lifting) \<open>\<not> bdd_below V\<close> bdd_below_def
        leI Inf_lower2 ereal_less_eq(3) le_less mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
Inf {ereal t |t. t \<in> V} = - \<infinity>

goal (1 subgoal):
 1. (\<lambda>n. ereal (u n / real n)) \<longlonglongrightarrow> - \<infinity>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Inf {ereal t |t. t \<in> V} = - \<infinity>

goal (1 subgoal):
 1. (\<lambda>n. ereal (u n / real n)) \<longlonglongrightarrow> - \<infinity>
[PROOF STEP]
have "{ereal(t)| t. t\<in>V} = {ereal(u n/n)|n. n > N0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {ereal t |t. t \<in> V} = {ereal (u n / real n) |n. N0 < n}
[PROOF STEP]
using V_def
[PROOF STATE]
proof (prove)
using this:
V = {u n / real n |n. N0 < n}

goal (1 subgoal):
 1. {ereal t |t. t \<in> V} = {ereal (u n / real n) |n. N0 < n}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{ereal t |t. t \<in> V} = {ereal (u n / real n) |n. N0 < n}

goal (1 subgoal):
 1. (\<lambda>n. ereal (u n / real n)) \<longlonglongrightarrow> - \<infinity>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Inf {ereal t |t. t \<in> V} = - \<infinity>
{ereal t |t. t \<in> V} = {ereal (u n / real n) |n. N0 < n}
[PROOF STEP]
have "Inf {ereal(u n/n)|n. n > N0} = -\<infinity>"
[PROOF STATE]
proof (prove)
using this:
Inf {ereal t |t. t \<in> V} = - \<infinity>
{ereal t |t. t \<in> V} = {ereal (u n / real n) |n. N0 < n}

goal (1 subgoal):
 1. Inf {ereal (u n / real n) |n. N0 < n} = - \<infinity>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Inf {ereal (u n / real n) |n. N0 < n} = - \<infinity>

goal (1 subgoal):
 1. (\<lambda>n. ereal (u n / real n)) \<longlonglongrightarrow> - \<infinity>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Inf {ereal (u n / real n) |n. N0 < n} = - \<infinity>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Inf {ereal (u n / real n) |n. N0 < n} = - \<infinity>

goal (1 subgoal):
 1. (\<lambda>n. ereal (u n / real n)) \<longlonglongrightarrow> - \<infinity>
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
Inf {ereal (u n / real n) |n. N0 < n} = - \<infinity>
(\<lambda>n. ereal (u n / real n)) \<longlonglongrightarrow> Inf {ereal (u n / real n) |n. N0 < n}

goal (1 subgoal):
 1. (\<lambda>n. ereal (u n / real n)) \<longlonglongrightarrow> - \<infinity>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>n. ereal (u n / real n)) \<longlonglongrightarrow> - \<infinity>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subadditive_converges_unbounded:
  assumes "subadditive u"
          "\<not> (bdd_below {u n/n | n. n>0})"
  shows "(\<lambda>n. ereal(u n/n)) \<longlonglongrightarrow> -\<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. ereal (u n / real n)) \<longlonglongrightarrow> - \<infinity>
[PROOF STEP]
by (rule subadditive_converges_unbounded'[OF subadditive_imp_eventually_subadditive[OF assms(1)] assms(2)])


[STATEMENT]
lemma subadditive_of_superadditive:
  assumes "superadditive u"
  shows "subadditive (\<lambda>n. -u n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subadditive (\<lambda>n. - u n)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
superadditive u

goal (1 subgoal):
 1. subadditive (\<lambda>n. - u n)
[PROOF STEP]
unfolding superadditive_def subadditive_def
[PROOF STATE]
proof (prove)
using this:
\<forall>m n. u m + u n \<le> u (m + n)

goal (1 subgoal):
 1. \<forall>m n. - u (m + n) \<le> - u m + - u n
[PROOF STEP]
by (auto simp add: algebra_simps)


[STATEMENT]
lemma superadditive_un_ge_nu1:
  assumes "superadditive u"
          "n > 0"
  shows "u n \<ge> n * u 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real n * u 1 \<le> u n
[PROOF STEP]
using subadditive_un_le_nu1[OF subadditive_of_superadditive[OF assms(1)] assms(2)]
[PROOF STATE]
proof (prove)
using this:
- u n \<le> real n * - u 1

goal (1 subgoal):
 1. real n * u 1 \<le> u n
[PROOF STEP]
by auto


[STATEMENT]
lemma superadditive_converges_bounded'':
  assumes "superadditive u"
          "\<And>n. n > 0 \<Longrightarrow> u n \<le> n * (a::real)"
  shows "\<exists>l. (\<lambda>n. u n / n) \<longlonglongrightarrow> l \<and> (\<forall>n>0. u n \<le> n * l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l. (\<lambda>n. u n / real n) \<longlonglongrightarrow> l \<and> (\<forall>n>0. u n \<le> real n * l)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>l. (\<lambda>n. u n / real n) \<longlonglongrightarrow> l \<and> (\<forall>n>0. u n \<le> real n * l)
[PROOF STEP]
have "\<exists>l. (\<lambda>n. -u n / n) \<longlonglongrightarrow> l \<and> (\<forall>n>0. -u n \<ge> n * l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l. (\<lambda>n. - u n / real n) \<longlonglongrightarrow> l \<and> (\<forall>n>0. real n * l \<le> - u n)
[PROOF STEP]
apply (rule subadditive_converges_bounded''[OF subadditive_of_superadditive[OF assms(1)], of "-a"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. 0 < n \<Longrightarrow> real n * - a \<le> - u n
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
0 < ?n \<Longrightarrow> u ?n \<le> real ?n * a

goal (1 subgoal):
 1. \<And>n. 0 < n \<Longrightarrow> real n * - a \<le> - u n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>l. (\<lambda>n. - u n / real n) \<longlonglongrightarrow> l \<and> (\<forall>n>0. real n * l \<le> - u n)

goal (1 subgoal):
 1. \<exists>l. (\<lambda>n. u n / real n) \<longlonglongrightarrow> l \<and> (\<forall>n>0. u n \<le> real n * l)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l. (\<lambda>n. - u n / real n) \<longlonglongrightarrow> l \<and> (\<forall>n>0. real n * l \<le> - u n)
[PROOF STEP]
obtain l where l: "(\<lambda>n. -u n / n) \<longlonglongrightarrow> l" "(\<forall>n>0. -u n \<ge> n * l)"
[PROOF STATE]
proof (prove)
using this:
\<exists>l. (\<lambda>n. - u n / real n) \<longlonglongrightarrow> l \<and> (\<forall>n>0. real n * l \<le> - u n)

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>(\<lambda>n. - u n / real n) \<longlonglongrightarrow> l; \<forall>n>0. real n * l \<le> - u n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<lambda>n. - u n / real n) \<longlonglongrightarrow> l
\<forall>n>0. real n * l \<le> - u n

goal (1 subgoal):
 1. \<exists>l. (\<lambda>n. u n / real n) \<longlonglongrightarrow> l \<and> (\<forall>n>0. u n \<le> real n * l)
[PROOF STEP]
have "(\<lambda>n. -((-u n)/n)) \<longlonglongrightarrow> -l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. - (- u n / real n)) \<longlonglongrightarrow> - l
[PROOF STEP]
by (intro tendsto_intros l)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. - (- u n / real n)) \<longlonglongrightarrow> - l

goal (1 subgoal):
 1. \<exists>l. (\<lambda>n. u n / real n) \<longlonglongrightarrow> l \<and> (\<forall>n>0. u n \<le> real n * l)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>n. - (- u n / real n)) \<longlonglongrightarrow> - l

goal (1 subgoal):
 1. \<exists>l. (\<lambda>n. u n / real n) \<longlonglongrightarrow> l \<and> (\<forall>n>0. u n \<le> real n * l)
[PROOF STEP]
have "\<forall>n>0. u n \<le> n * (-l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n>0. u n \<le> real n * - l
[PROOF STEP]
using l(2)
[PROOF STATE]
proof (prove)
using this:
\<forall>n>0. real n * l \<le> - u n

goal (1 subgoal):
 1. \<forall>n>0. u n \<le> real n * - l
[PROOF STEP]
by (auto simp add: algebra_simps) (metis minus_equation_iff neg_le_iff_le)
[PROOF STATE]
proof (state)
this:
\<forall>n>0. u n \<le> real n * - l

goal (1 subgoal):
 1. \<exists>l. (\<lambda>n. u n / real n) \<longlonglongrightarrow> l \<and> (\<forall>n>0. u n \<le> real n * l)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. - (- u n / real n)) \<longlonglongrightarrow> - l
\<forall>n>0. u n \<le> real n * - l
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. - (- u n / real n)) \<longlonglongrightarrow> - l
\<forall>n>0. u n \<le> real n * - l

goal (1 subgoal):
 1. \<exists>l. (\<lambda>n. u n / real n) \<longlonglongrightarrow> l \<and> (\<forall>n>0. u n \<le> real n * l)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>l. (\<lambda>n. u n / real n) \<longlonglongrightarrow> l \<and> (\<forall>n>0. u n \<le> real n * l)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma almost_additive_converges:
  fixes u::"nat \<Rightarrow> real"
  assumes "\<And>m n. abs(u(m+n) - u m - u n) \<le> C"
  shows "convergent (\<lambda>n. u n/n)"
        "abs(u k - k * lim (\<lambda>n. u n / n)) \<le> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convergent (\<lambda>n. u n / real n) &&& \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. convergent (\<lambda>n. u n / real n)
 2. \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
have "(abs (u 0)) \<le> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>u 0\<bar> \<le> C
[PROOF STEP]
using assms[of 0 0]
[PROOF STATE]
proof (prove)
using this:
\<bar>u (0 + 0) - u 0 - u 0\<bar> \<le> C

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

goal (2 subgoals):
 1. convergent (\<lambda>n. u n / real n)
 2. \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<bar>u 0\<bar> \<le> C
[PROOF STEP]
have "C \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
\<bar>u 0\<bar> \<le> C

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

goal (2 subgoals):
 1. convergent (\<lambda>n. u n / real n)
 2. \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
define v where "v = (\<lambda>n. u n + C)"
[PROOF STATE]
proof (state)
this:
v = (\<lambda>n. u n + C)

goal (2 subgoals):
 1. convergent (\<lambda>n. u n / real n)
 2. \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
have "subadditive v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subadditive v
[PROOF STEP]
unfolding subadditive_def v_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m n. u (m + n) + C \<le> u m + C + (u n + C)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<bar>u (?m + ?n) - u ?m - u ?n\<bar> \<le> C

goal (1 subgoal):
 1. \<forall>m n. u (m + n) + C \<le> u m + C + (u n + C)
[PROOF STEP]
by (auto simp add: algebra_simps abs_diff_le_iff)
[PROOF STATE]
proof (state)
this:
subadditive v

goal (2 subgoals):
 1. convergent (\<lambda>n. u n / real n)
 2. \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
subadditive v
[PROOF STEP]
have vle: "v n \<le> n * v 1" if "n > 0" for n
[PROOF STATE]
proof (prove)
using this:
subadditive v

goal (1 subgoal):
 1. v n \<le> real n * v 1
[PROOF STEP]
using subadditive_un_le_nu1 that
[PROOF STATE]
proof (prove)
using this:
subadditive v
\<lbrakk>subadditive ?u; 0 < ?n\<rbrakk> \<Longrightarrow> ?u ?n \<le> real ?n * ?u 1
0 < n

goal (1 subgoal):
 1. v n \<le> real n * v 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < ?n \<Longrightarrow> v ?n \<le> real ?n * v 1

goal (2 subgoals):
 1. convergent (\<lambda>n. u n / real n)
 2. \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
define w where "w = (\<lambda>n. u n - C)"
[PROOF STATE]
proof (state)
this:
w = (\<lambda>n. u n - C)

goal (2 subgoals):
 1. convergent (\<lambda>n. u n / real n)
 2. \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
have "superadditive w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. superadditive w
[PROOF STEP]
unfolding superadditive_def w_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m n. u m - C + (u n - C) \<le> u (m + n) - C
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<bar>u (?m + ?n) - u ?m - u ?n\<bar> \<le> C

goal (1 subgoal):
 1. \<forall>m n. u m - C + (u n - C) \<le> u (m + n) - C
[PROOF STEP]
by (auto simp add: algebra_simps abs_diff_le_iff)
[PROOF STATE]
proof (state)
this:
superadditive w

goal (2 subgoals):
 1. convergent (\<lambda>n. u n / real n)
 2. \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
superadditive w
[PROOF STEP]
have wge: "w n \<ge> n * w 1" if "n > 0" for n
[PROOF STATE]
proof (prove)
using this:
superadditive w

goal (1 subgoal):
 1. real n * w 1 \<le> w n
[PROOF STEP]
using superadditive_un_ge_nu1 that
[PROOF STATE]
proof (prove)
using this:
superadditive w
\<lbrakk>superadditive ?u; 0 < ?n\<rbrakk> \<Longrightarrow> real ?n * ?u 1 \<le> ?u ?n
0 < n

goal (1 subgoal):
 1. real n * w 1 \<le> w n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < ?n \<Longrightarrow> real ?n * w 1 \<le> w ?n

goal (2 subgoals):
 1. convergent (\<lambda>n. u n / real n)
 2. \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
have I: "v n \<ge> w n" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w n \<le> v n
[PROOF STEP]
unfolding v_def w_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u n - C \<le> u n + C
[PROOF STEP]
using \<open>C \<ge> 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 \<le> C

goal (1 subgoal):
 1. u n - C \<le> u n + C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w ?n \<le> v ?n

goal (2 subgoals):
 1. convergent (\<lambda>n. u n / real n)
 2. \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w ?n \<le> v ?n
[PROOF STEP]
have *: "v n \<ge> n * w 1" if "n > 0" for n
[PROOF STATE]
proof (prove)
using this:
w ?n \<le> v ?n

goal (1 subgoal):
 1. real n * w 1 \<le> v n
[PROOF STEP]
using order_trans[OF wge[OF that]]
[PROOF STATE]
proof (prove)
using this:
w ?n \<le> v ?n
w n \<le> ?z \<Longrightarrow> real n * w 1 \<le> ?z

goal (1 subgoal):
 1. real n * w 1 \<le> v n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < ?n \<Longrightarrow> real ?n * w 1 \<le> v ?n

goal (2 subgoals):
 1. convergent (\<lambda>n. u n / real n)
 2. \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < ?n \<Longrightarrow> real ?n * w 1 \<le> v ?n
[PROOF STEP]
obtain lv where lv: "(\<lambda>n. v n/n) \<longlonglongrightarrow> lv" "\<And>n. n > 0 \<Longrightarrow> v n \<ge> n * lv"
[PROOF STATE]
proof (prove)
using this:
0 < ?n \<Longrightarrow> real ?n * w 1 \<le> v ?n

goal (1 subgoal):
 1. (\<And>lv. \<lbrakk>(\<lambda>n. v n / real n) \<longlonglongrightarrow> lv; \<And>n. 0 < n \<Longrightarrow> real n * lv \<le> v n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using subadditive_converges_bounded''[OF \<open>subadditive v\<close> *]
[PROOF STATE]
proof (prove)
using this:
0 < ?n \<Longrightarrow> real ?n * w 1 \<le> v ?n
(\<And>n. 0 < n \<Longrightarrow> 0 < n) \<Longrightarrow> \<exists>l. (\<lambda>n. v n / real n) \<longlonglongrightarrow> l \<and> (\<forall>n>0. real n * l \<le> v n)

goal (1 subgoal):
 1. (\<And>lv. \<lbrakk>(\<lambda>n. v n / real n) \<longlonglongrightarrow> lv; \<And>n. 0 < n \<Longrightarrow> real n * lv \<le> v n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. v n / real n) \<longlonglongrightarrow> lv
0 < ?n \<Longrightarrow> real ?n * lv \<le> v ?n

goal (2 subgoals):
 1. convergent (\<lambda>n. u n / real n)
 2. \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
have *: "w n \<le> n * v 1" if "n > 0" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w n \<le> real n * v 1
[PROOF STEP]
using order_trans[OF _ vle[OF that]] I
[PROOF STATE]
proof (prove)
using this:
?x \<le> v n \<Longrightarrow> ?x \<le> real n * v 1
w ?n \<le> v ?n

goal (1 subgoal):
 1. w n \<le> real n * v 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < ?n \<Longrightarrow> w ?n \<le> real ?n * v 1

goal (2 subgoals):
 1. convergent (\<lambda>n. u n / real n)
 2. \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < ?n \<Longrightarrow> w ?n \<le> real ?n * v 1
[PROOF STEP]
obtain lw where lw: "(\<lambda>n. w n/n) \<longlonglongrightarrow> lw" "\<And>n. n > 0 \<Longrightarrow> w n \<le> n * lw"
[PROOF STATE]
proof (prove)
using this:
0 < ?n \<Longrightarrow> w ?n \<le> real ?n * v 1

goal (1 subgoal):
 1. (\<And>lw. \<lbrakk>(\<lambda>n. w n / real n) \<longlonglongrightarrow> lw; \<And>n. 0 < n \<Longrightarrow> w n \<le> real n * lw\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using superadditive_converges_bounded''[OF \<open>superadditive w\<close> *]
[PROOF STATE]
proof (prove)
using this:
0 < ?n \<Longrightarrow> w ?n \<le> real ?n * v 1
(\<And>n. 0 < n \<Longrightarrow> 0 < n) \<Longrightarrow> \<exists>l. (\<lambda>n. w n / real n) \<longlonglongrightarrow> l \<and> (\<forall>n>0. w n \<le> real n * l)

goal (1 subgoal):
 1. (\<And>lw. \<lbrakk>(\<lambda>n. w n / real n) \<longlonglongrightarrow> lw; \<And>n. 0 < n \<Longrightarrow> w n \<le> real n * lw\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. w n / real n) \<longlonglongrightarrow> lw
0 < ?n \<Longrightarrow> w ?n \<le> real ?n * lw

goal (2 subgoals):
 1. convergent (\<lambda>n. u n / real n)
 2. \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
have *: "v n/n = w n /n + 2*C*(1/n)" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v n / real n = w n / real n + 2 * C * (1 / real n)
[PROOF STEP]
unfolding v_def w_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u n + C) / real n = (u n - C) / real n + 2 * C * (1 / real n)
[PROOF STEP]
by (auto simp add: algebra_simps divide_simps)
[PROOF STATE]
proof (state)
this:
v ?n / real ?n = w ?n / real ?n + 2 * C * (1 / real ?n)

goal (2 subgoals):
 1. convergent (\<lambda>n. u n / real n)
 2. \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
have "(\<lambda>n. w n /n + 2*C*(1/n)) \<longlonglongrightarrow> lw + 2*C*0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. w n / real n + 2 * C * (1 / real n)) \<longlonglongrightarrow> lw + 2 * C * 0
[PROOF STEP]
by (intro tendsto_add tendsto_mult lim_1_over_n lw, auto)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. w n / real n + 2 * C * (1 / real n)) \<longlonglongrightarrow> lw + 2 * C * 0

goal (2 subgoals):
 1. convergent (\<lambda>n. u n / real n)
 2. \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. w n / real n + 2 * C * (1 / real n)) \<longlonglongrightarrow> lw + 2 * C * 0
[PROOF STEP]
have "lw = lv"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. w n / real n + 2 * C * (1 / real n)) \<longlonglongrightarrow> lw + 2 * C * 0

goal (1 subgoal):
 1. lw = lv
[PROOF STEP]
unfolding *[symmetric]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. v n / real n) \<longlonglongrightarrow> lw + 2 * C * 0

goal (1 subgoal):
 1. lw = lv
[PROOF STEP]
using lv(1) LIMSEQ_unique
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. v n / real n) \<longlonglongrightarrow> lw + 2 * C * 0
(\<lambda>n. v n / real n) \<longlonglongrightarrow> lv
\<lbrakk>?X \<longlonglongrightarrow> ?a; ?X \<longlonglongrightarrow> ?b\<rbrakk> \<Longrightarrow> ?a = ?b

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

goal (2 subgoals):
 1. convergent (\<lambda>n. u n / real n)
 2. \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
have *: "u n/n = w n /n + C*(1/n)" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u n / real n = w n / real n + C * (1 / real n)
[PROOF STEP]
unfolding w_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u n / real n = (u n - C) / real n + C * (1 / real n)
[PROOF STEP]
by (auto simp add: algebra_simps divide_simps)
[PROOF STATE]
proof (state)
this:
u ?n / real ?n = w ?n / real ?n + C * (1 / real ?n)

goal (2 subgoals):
 1. convergent (\<lambda>n. u n / real n)
 2. \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
have "(\<lambda>n. u n /n) \<longlonglongrightarrow> lw + C*0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. u n / real n) \<longlonglongrightarrow> lw + C * 0
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. w n / real n + C * (1 / real n)) \<longlonglongrightarrow> lw + C * 0
[PROOF STEP]
by (intro tendsto_add tendsto_mult lim_1_over_n lw, auto)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. u n / real n) \<longlonglongrightarrow> lw + C * 0

goal (2 subgoals):
 1. convergent (\<lambda>n. u n / real n)
 2. \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. u n / real n) \<longlonglongrightarrow> lw + C * 0
[PROOF STEP]
have lu: "convergent (\<lambda>n. u n/n)" "lim (\<lambda>n. u n/n) = lw"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. u n / real n) \<longlonglongrightarrow> lw + C * 0

goal (1 subgoal):
 1. convergent (\<lambda>n. u n / real n) &&& lim (\<lambda>n. u n / real n) = lw
[PROOF STEP]
by (auto simp add: convergentI limI)
[PROOF STATE]
proof (state)
this:
convergent (\<lambda>n. u n / real n)
lim (\<lambda>n. u n / real n) = lw

goal (2 subgoals):
 1. convergent (\<lambda>n. u n / real n)
 2. \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
convergent (\<lambda>n. u n / real n)
lim (\<lambda>n. u n / real n) = lw
[PROOF STEP]
show "convergent (\<lambda>n. u n/n)"
[PROOF STATE]
proof (prove)
using this:
convergent (\<lambda>n. u n / real n)
lim (\<lambda>n. u n / real n) = lw

goal (1 subgoal):
 1. convergent (\<lambda>n. u n / real n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
convergent (\<lambda>n. u n / real n)

goal (1 subgoal):
 1. \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
show "abs(u k - k * lim (\<lambda>n. u n / n)) \<le> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
proof (cases "k>0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < k \<Longrightarrow> \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
 2. \<not> 0 < k \<Longrightarrow> \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> 0 < k

goal (2 subgoals):
 1. 0 < k \<Longrightarrow> \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
 2. \<not> 0 < k \<Longrightarrow> \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> 0 < k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> 0 < k

goal (1 subgoal):
 1. \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
using assms[of 0 0]
[PROOF STATE]
proof (prove)
using this:
\<not> 0 < k
\<bar>u (0 + 0) - u 0 - u 0\<bar> \<le> C

goal (1 subgoal):
 1. \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C

goal (1 subgoal):
 1. 0 < k \<Longrightarrow> \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
0 < k

goal (1 subgoal):
 1. 0 < k \<Longrightarrow> \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
have "u k - k * lim (\<lambda>n. u n/n) = v k - C - k * lv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u k - real k * lim (\<lambda>n. u n / real n) = v k - C - real k * lv
[PROOF STEP]
unfolding lu(2) \<open>lw = lv\<close> v_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u k - real k * lv = u k + C - C - real k * lv
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u k - real k * lim (\<lambda>n. u n / real n) = v k - C - real k * lv

goal (1 subgoal):
 1. 0 < k \<Longrightarrow> \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
u k - real k * lim (\<lambda>n. u n / real n) = v k - C - real k * lv

goal (1 subgoal):
 1. 0 < k \<Longrightarrow> \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
have "... \<ge> -C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - C \<le> v k - C - real k * lv
[PROOF STEP]
using lv(2)[OF True]
[PROOF STATE]
proof (prove)
using this:
real k * lv \<le> v k

goal (1 subgoal):
 1. - C \<le> v k - C - real k * lv
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
- C \<le> v k - C - real k * lv

goal (1 subgoal):
 1. 0 < k \<Longrightarrow> \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
- C \<le> u k - real k * lim (\<lambda>n. u n / real n)
[PROOF STEP]
have A: "u k - k * lim (\<lambda>n. u n/n) \<ge> - C"
[PROOF STATE]
proof (prove)
using this:
- C \<le> u k - real k * lim (\<lambda>n. u n / real n)

goal (1 subgoal):
 1. - C \<le> u k - real k * lim (\<lambda>n. u n / real n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
- C \<le> u k - real k * lim (\<lambda>n. u n / real n)

goal (1 subgoal):
 1. 0 < k \<Longrightarrow> \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
have "u k - k * lim (\<lambda>n. u n/n) = w k + C - k * lw"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u k - real k * lim (\<lambda>n. u n / real n) = w k + C - real k * lw
[PROOF STEP]
unfolding lu(2) w_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u k - real k * lw = u k - C + C - real k * lw
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u k - real k * lim (\<lambda>n. u n / real n) = w k + C - real k * lw

goal (1 subgoal):
 1. 0 < k \<Longrightarrow> \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
u k - real k * lim (\<lambda>n. u n / real n) = w k + C - real k * lw

goal (1 subgoal):
 1. 0 < k \<Longrightarrow> \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
have "... \<le> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w k + C - real k * lw \<le> C
[PROOF STEP]
using lw(2)[OF True]
[PROOF STATE]
proof (prove)
using this:
w k \<le> real k * lw

goal (1 subgoal):
 1. w k + C - real k * lw \<le> C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w k + C - real k * lw \<le> C

goal (1 subgoal):
 1. 0 < k \<Longrightarrow> \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
u k - real k * lim (\<lambda>n. u n / real n) \<le> C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
u k - real k * lim (\<lambda>n. u n / real n) \<le> C

goal (1 subgoal):
 1. \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
u k - real k * lim (\<lambda>n. u n / real n) \<le> C
- C \<le> u k - real k * lim (\<lambda>n. u n / real n)

goal (1 subgoal):
 1. \<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<bar>u k - real k * lim (\<lambda>n. u n / real n)\<bar> \<le> C

goal:
No subgoals!
[PROOF STEP]
qed