1.1 --- a/src/HOL/Deriv.thy Mon Dec 03 18:19:11 2012 +0100
1.2 +++ b/src/HOL/Deriv.thy Mon Dec 03 18:19:12 2012 +0100
1.3 @@ -76,7 +76,7 @@
1.4 lemma DERIV_mult_lemma:
1.5 fixes a b c d :: "'a::real_field"
1.6 shows "(a * b - c * d) / h = a * ((b - d) / h) + ((a - c) / h) * d"
1.7 -by (simp add: diff_minus add_divide_distrib [symmetric] ring_distribs)
1.8 + by (simp add: field_simps diff_divide_distrib)
1.9
1.10 lemma DERIV_mult':
1.11 assumes f: "DERIV f x :> D"
1.12 @@ -97,15 +97,12 @@
1.13 qed
1.14
1.15 lemma DERIV_mult:
1.16 - "[| DERIV f x :> Da; DERIV g x :> Db |]
1.17 - ==> DERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))"
1.18 -by (drule (1) DERIV_mult', simp only: mult_commute add_commute)
1.19 + "DERIV f x :> Da \<Longrightarrow> DERIV g x :> Db \<Longrightarrow> DERIV (\<lambda>x. f x * g x) x :> Da * g x + Db * f x"
1.20 + by (drule (1) DERIV_mult', simp only: mult_commute add_commute)
1.21
1.22 lemma DERIV_unique:
1.23 - "[| DERIV f x :> D; DERIV f x :> E |] ==> D = E"
1.24 -apply (simp add: deriv_def)
1.25 -apply (blast intro: LIM_unique)
1.26 -done
1.27 + "DERIV f x :> D \<Longrightarrow> DERIV f x :> E \<Longrightarrow> D = E"
1.28 + unfolding deriv_def by (rule LIM_unique)
1.29
1.30 text{*Differentiation of finite sum*}
1.31
2.1 --- a/src/HOL/Lim.thy Mon Dec 03 18:19:11 2012 +0100
2.2 +++ b/src/HOL/Lim.thy Mon Dec 03 18:19:12 2012 +0100
2.3 @@ -323,36 +323,6 @@
2.4 isCont_diff isCont_mult isCont_inverse isCont_divide isCont_scaleR
2.5 isCont_of_real isCont_power isCont_sgn isCont_setsum
2.6
2.7 -lemma LIM_less_bound: fixes f :: "real \<Rightarrow> real" assumes "b < x"
2.8 - and all_le: "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and isCont: "isCont f x"
2.9 - shows "0 \<le> f x"
2.10 -proof (rule ccontr)
2.11 - assume "\<not> 0 \<le> f x" hence "f x < 0" by auto
2.12 - hence "0 < - f x / 2" by auto
2.13 - from isCont[unfolded isCont_def, THEN LIM_D, OF this]
2.14 - obtain s where "s > 0" and s_D: "\<And>x'. \<lbrakk> x' \<noteq> x ; \<bar> x' - x \<bar> < s \<rbrakk> \<Longrightarrow> \<bar> f x' - f x \<bar> < - f x / 2" by auto
2.15 -
2.16 - let ?x = "x - min (s / 2) ((x - b) / 2)"
2.17 - have "?x < x" and "\<bar> ?x - x \<bar> < s"
2.18 - using `b < x` and `0 < s` by auto
2.19 - have "b < ?x"
2.20 - proof (cases "s < x - b")
2.21 - case True thus ?thesis using `0 < s` by auto
2.22 - next
2.23 - case False hence "s / 2 \<ge> (x - b) / 2" by auto
2.24 - hence "?x = (x + b) / 2" by (simp add: field_simps min_max.inf_absorb2)
2.25 - thus ?thesis using `b < x` by auto
2.26 - qed
2.27 - hence "0 \<le> f ?x" using all_le `?x < x` by auto
2.28 - moreover have "\<bar>f ?x - f x\<bar> < - f x / 2"
2.29 - using s_D[OF _ `\<bar> ?x - x \<bar> < s`] `?x < x` by auto
2.30 - hence "f ?x - f x < - f x / 2" by auto
2.31 - hence "f ?x < f x / 2" by auto
2.32 - hence "f ?x < 0" using `f x < 0` by auto
2.33 - thus False using `0 \<le> f ?x` by auto
2.34 -qed
2.35 -
2.36 -
2.37 subsection {* Uniform Continuity *}
2.38
2.39 lemma isUCont_isCont: "isUCont f ==> isCont f x"
2.40 @@ -442,4 +412,15 @@
2.41 (X -- a --> (L::'b::topological_space))"
2.42 using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 ..
2.43
2.44 +lemma LIM_less_bound:
2.45 + fixes f :: "real \<Rightarrow> real"
2.46 + assumes ev: "b < x" "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and "isCont f x"
2.47 + shows "0 \<le> f x"
2.48 +proof (rule tendsto_le_const)
2.49 + show "(f ---> f x) (at_left x)"
2.50 + using `isCont f x` by (simp add: filterlim_at_split isCont_def)
2.51 + show "eventually (\<lambda>x. 0 \<le> f x) (at_left x)"
2.52 + using ev by (auto simp: eventually_within_less dist_real_def intro!: exI[of _ "x - b"])
2.53 +qed simp
2.54 +
2.55 end
3.1 --- a/src/HOL/Limits.thy Mon Dec 03 18:19:11 2012 +0100
3.2 +++ b/src/HOL/Limits.thy Mon Dec 03 18:19:12 2012 +0100
3.3 @@ -463,6 +463,22 @@
3.4 lemma at_neq_bot [simp]: "at (a::'a::perfect_space) \<noteq> bot"
3.5 by (simp add: at_eq_bot_iff not_open_singleton)
3.6
3.7 +lemma trivial_limit_at_left_real [simp]: (* maybe generalize type *)
3.8 + "\<not> trivial_limit (at_left (x::real))"
3.9 + unfolding trivial_limit_def eventually_within_le
3.10 + apply clarsimp
3.11 + apply (rule_tac x="x - d/2" in bexI)
3.12 + apply (auto simp: dist_real_def)
3.13 + done
3.14 +
3.15 +lemma trivial_limit_at_right_real [simp]: (* maybe generalize type *)
3.16 + "\<not> trivial_limit (at_right (x::real))"
3.17 + unfolding trivial_limit_def eventually_within_le
3.18 + apply clarsimp
3.19 + apply (rule_tac x="x + d/2" in bexI)
3.20 + apply (auto simp: dist_real_def)
3.21 + done
3.22 +
3.23 lemma eventually_at_infinity:
3.24 "eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. b \<le> norm x \<longrightarrow> P x)"
3.25 unfolding at_infinity_def
3.26 @@ -713,6 +729,9 @@
3.27 "filterlim f F F1 \<Longrightarrow> filterlim f F F2 \<Longrightarrow> filterlim f F (sup F1 F2)"
3.28 unfolding filterlim_def filtermap_sup by auto
3.29
3.30 +lemma filterlim_Suc: "filterlim Suc sequentially sequentially"
3.31 + by (simp add: filterlim_iff eventually_sequentially) (metis le_Suc_eq)
3.32 +
3.33 abbreviation (in topological_space)
3.34 tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr "--->" 55) where
3.35 "(f ---> l) F \<equiv> filterlim f (nhds l) F"
3.36 @@ -1027,6 +1046,30 @@
3.37 by (simp add: tendsto_const)
3.38 qed
3.39
3.40 +lemma tendsto_le_const:
3.41 + fixes f :: "_ \<Rightarrow> real"
3.42 + assumes F: "\<not> trivial_limit F"
3.43 + assumes x: "(f ---> x) F" and a: "eventually (\<lambda>x. a \<le> f x) F"
3.44 + shows "a \<le> x"
3.45 +proof (rule ccontr)
3.46 + assume "\<not> a \<le> x"
3.47 + with x have "eventually (\<lambda>x. f x < a) F"
3.48 + by (auto simp add: tendsto_def elim!: allE[of _ "{..< a}"])
3.49 + with a have "eventually (\<lambda>x. False) F"
3.50 + by eventually_elim auto
3.51 + with F show False
3.52 + by (simp add: eventually_False)
3.53 +qed
3.54 +
3.55 +lemma tendsto_le:
3.56 + fixes f g :: "_ \<Rightarrow> real"
3.57 + assumes F: "\<not> trivial_limit F"
3.58 + assumes x: "(f ---> x) F" and y: "(g ---> y) F"
3.59 + assumes ev: "eventually (\<lambda>x. g x \<le> f x) F"
3.60 + shows "y \<le> x"
3.61 + using tendsto_le_const[OF F tendsto_diff[OF x y], of 0] ev
3.62 + by (simp add: sign_simps)
3.63 +
3.64 subsubsection {* Inverse and division *}
3.65
3.66 lemma (in bounded_bilinear) Zfun_prod_Bfun:
3.67 @@ -1382,6 +1425,44 @@
3.68 by eventually_elim simp
3.69 qed
3.70
3.71 +lemma tendsto_divide_0:
3.72 + fixes f :: "_ \<Rightarrow> 'a\<Colon>{real_normed_div_algebra, division_ring_inverse_zero}"
3.73 + assumes f: "(f ---> c) F"
3.74 + assumes g: "LIM x F. g x :> at_infinity"
3.75 + shows "((\<lambda>x. f x / g x) ---> 0) F"
3.76 + using tendsto_mult[OF f filterlim_compose[OF tendsto_inverse_0 g]] by (simp add: divide_inverse)
3.77 +
3.78 +lemma linear_plus_1_le_power:
3.79 + fixes x :: real
3.80 + assumes x: "0 \<le> x"
3.81 + shows "real n * x + 1 \<le> (x + 1) ^ n"
3.82 +proof (induct n)
3.83 + case (Suc n)
3.84 + have "real (Suc n) * x + 1 \<le> (x + 1) * (real n * x + 1)"
3.85 + by (simp add: field_simps real_of_nat_Suc mult_nonneg_nonneg x)
3.86 + also have "\<dots> \<le> (x + 1)^Suc n"
3.87 + using Suc x by (simp add: mult_left_mono)
3.88 + finally show ?case .
3.89 +qed simp
3.90 +
3.91 +lemma filterlim_realpow_sequentially_gt1:
3.92 + fixes x :: "'a :: real_normed_div_algebra"
3.93 + assumes x[arith]: "1 < norm x"
3.94 + shows "LIM n sequentially. x ^ n :> at_infinity"
3.95 +proof (intro filterlim_at_infinity[THEN iffD2] allI impI)
3.96 + fix y :: real assume "0 < y"
3.97 + have "0 < norm x - 1" by simp
3.98 + then obtain N::nat where "y < real N * (norm x - 1)" by (blast dest: reals_Archimedean3)
3.99 + also have "\<dots> \<le> real N * (norm x - 1) + 1" by simp
3.100 + also have "\<dots> \<le> (norm x - 1 + 1) ^ N" by (rule linear_plus_1_le_power) simp
3.101 + also have "\<dots> = norm x ^ N" by simp
3.102 + finally have "\<forall>n\<ge>N. y \<le> norm x ^ n"
3.103 + by (metis order_less_le_trans power_increasing order_less_imp_le x)
3.104 + then show "eventually (\<lambda>n. y \<le> norm (x ^ n)) sequentially"
3.105 + unfolding eventually_sequentially
3.106 + by (auto simp: norm_power)
3.107 +qed simp
3.108 +
3.109 subsection {* Relate @{const at}, @{const at_left} and @{const at_right} *}
3.110
3.111 text {*
4.1 --- a/src/HOL/SEQ.thy Mon Dec 03 18:19:11 2012 +0100
4.2 +++ b/src/HOL/SEQ.thy Mon Dec 03 18:19:12 2012 +0100
4.3 @@ -171,6 +171,9 @@
4.4 thus ?case by arith
4.5 qed
4.6
4.7 +lemma filterlim_subseq: "subseq f \<Longrightarrow> filterlim f sequentially sequentially"
4.8 + unfolding filterlim_iff eventually_sequentially by (metis le_trans seq_suble)
4.9 +
4.10 lemma subseq_o: "subseq r \<Longrightarrow> subseq s \<Longrightarrow> subseq (r \<circ> s)"
4.11 unfolding subseq_def by simp
4.12
4.13 @@ -357,36 +360,23 @@
4.14
4.15 lemma increasing_LIMSEQ:
4.16 fixes f :: "nat \<Rightarrow> real"
4.17 - assumes inc: "!!n. f n \<le> f (Suc n)"
4.18 - and bdd: "!!n. f n \<le> l"
4.19 - and en: "!!e. 0 < e \<Longrightarrow> \<exists>n. l \<le> f n + e"
4.20 + assumes inc: "\<And>n. f n \<le> f (Suc n)"
4.21 + and bdd: "\<And>n. f n \<le> l"
4.22 + and en: "\<And>e. 0 < e \<Longrightarrow> \<exists>n. l \<le> f n + e"
4.23 shows "f ----> l"
4.24 -proof (auto simp add: LIMSEQ_def)
4.25 - fix e :: real
4.26 - assume e: "0 < e"
4.27 - then obtain N where "l \<le> f N + e/2"
4.28 - by (metis half_gt_zero e en that)
4.29 - hence N: "l < f N + e" using e
4.30 - by simp
4.31 - { fix k
4.32 - have [simp]: "!!n. \<bar>f n - l\<bar> = l - f n"
4.33 - by (simp add: bdd)
4.34 - have "\<bar>f (N+k) - l\<bar> < e"
4.35 - proof (induct k)
4.36 - case 0 show ?case using N
4.37 - by simp
4.38 - next
4.39 - case (Suc k) thus ?case using N inc [of "N+k"]
4.40 - by simp
4.41 - qed
4.42 - } note 1 = this
4.43 - { fix n
4.44 - have "N \<le> n \<Longrightarrow> \<bar>f n - l\<bar> < e" using 1 [of "n-N"]
4.45 - by simp
4.46 - } note [intro] = this
4.47 - show " \<exists>no. \<forall>n\<ge>no. dist (f n) l < e"
4.48 - by (auto simp add: dist_real_def)
4.49 - qed
4.50 + unfolding LIMSEQ_def
4.51 +proof safe
4.52 + fix r :: real assume "0 < r"
4.53 + with bdd en[of "r / 2"] obtain n where n: "dist (f n) l \<le> r / 2"
4.54 + by (auto simp add: field_simps dist_real_def)
4.55 + { fix N assume "n \<le> N"
4.56 + then have "dist (f N) l \<le> dist (f n) l"
4.57 + using incseq_SucI[of f] inc bdd by (auto dest!: incseqD simp: dist_real_def)
4.58 + then have "dist (f N) l < r"
4.59 + using `0 < r` n by simp }
4.60 + with `0 < r` show "\<exists>no. \<forall>n\<ge>no. dist (f n) l < r"
4.61 + by (auto simp add: LIMSEQ_def field_simps intro!: exI[of _ n])
4.62 +qed
4.63
4.64 lemma Bseq_inverse_lemma:
4.65 fixes x :: "'a::real_normed_div_algebra"
4.66 @@ -414,24 +404,16 @@
4.67
4.68 lemma LIMSEQ_inverse_zero:
4.69 "\<forall>r::real. \<exists>N. \<forall>n\<ge>N. r < X n \<Longrightarrow> (\<lambda>n. inverse (X n)) ----> 0"
4.70 -apply (rule LIMSEQ_I)
4.71 -apply (drule_tac x="inverse r" in spec, safe)
4.72 -apply (rule_tac x="N" in exI, safe)
4.73 -apply (drule_tac x="n" in spec, safe)
4.74 -apply (frule positive_imp_inverse_positive)
4.75 -apply (frule (1) less_imp_inverse_less)
4.76 -apply (subgoal_tac "0 < X n", simp)
4.77 -apply (erule (1) order_less_trans)
4.78 -done
4.79 + apply (rule filterlim_compose[OF tendsto_inverse_0])
4.80 + apply (simp add: filterlim_at_infinity[OF order_refl] eventually_sequentially)
4.81 + apply (metis abs_le_D1 linorder_le_cases linorder_not_le)
4.82 + done
4.83
4.84 text{*The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity*}
4.85
4.86 lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----> 0"
4.87 -apply (rule LIMSEQ_inverse_zero, safe)
4.88 -apply (cut_tac x = r in reals_Archimedean2)
4.89 -apply (safe, rule_tac x = n in exI)
4.90 -apply (auto simp add: real_of_nat_Suc)
4.91 -done
4.92 + by (metis filterlim_compose tendsto_inverse_0 filterlim_mono order_refl filterlim_Suc
4.93 + filterlim_compose[OF filterlim_real_sequentially] at_top_le_at_infinity)
4.94
4.95 text{*The sequence @{term "r + 1/n"} tends to @{term r} as @{term n} tends to
4.96 infinity is now easily proved*}
4.97 @@ -442,41 +424,25 @@
4.98
4.99 lemma LIMSEQ_inverse_real_of_nat_add_minus:
4.100 "(%n. r + -inverse(real(Suc n))) ----> r"
4.101 - using tendsto_add [OF tendsto_const
4.102 - tendsto_minus [OF LIMSEQ_inverse_real_of_nat]] by auto
4.103 + using tendsto_add [OF tendsto_const tendsto_minus [OF LIMSEQ_inverse_real_of_nat]]
4.104 + by auto
4.105
4.106 lemma LIMSEQ_inverse_real_of_nat_add_minus_mult:
4.107 "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r"
4.108 - using tendsto_mult [OF tendsto_const
4.109 - LIMSEQ_inverse_real_of_nat_add_minus [of 1]]
4.110 + using tendsto_mult [OF tendsto_const LIMSEQ_inverse_real_of_nat_add_minus [of 1]]
4.111 by auto
4.112
4.113 lemma LIMSEQ_le_const:
4.114 "\<lbrakk>X ----> (x::real); \<exists>N. \<forall>n\<ge>N. a \<le> X n\<rbrakk> \<Longrightarrow> a \<le> x"
4.115 -apply (rule ccontr, simp only: linorder_not_le)
4.116 -apply (drule_tac r="a - x" in LIMSEQ_D, simp)
4.117 -apply clarsimp
4.118 -apply (drule_tac x="max N no" in spec, drule mp, rule le_maxI1)
4.119 -apply (drule_tac x="max N no" in spec, drule mp, rule le_maxI2)
4.120 -apply simp
4.121 -done
4.122 + using tendsto_le_const[of sequentially X x a] by (simp add: eventually_sequentially)
4.123 +
4.124 +lemma LIMSEQ_le:
4.125 + "\<lbrakk>X ----> x; Y ----> y; \<exists>N. \<forall>n\<ge>N. X n \<le> Y n\<rbrakk> \<Longrightarrow> x \<le> (y::real)"
4.126 + using tendsto_le[of sequentially Y y X x] by (simp add: eventually_sequentially)
4.127
4.128 lemma LIMSEQ_le_const2:
4.129 "\<lbrakk>X ----> (x::real); \<exists>N. \<forall>n\<ge>N. X n \<le> a\<rbrakk> \<Longrightarrow> x \<le> a"
4.130 -apply (subgoal_tac "- a \<le> - x", simp)
4.131 -apply (rule LIMSEQ_le_const)
4.132 -apply (erule tendsto_minus)
4.133 -apply simp
4.134 -done
4.135 -
4.136 -lemma LIMSEQ_le:
4.137 - "\<lbrakk>X ----> x; Y ----> y; \<exists>N. \<forall>n\<ge>N. X n \<le> Y n\<rbrakk> \<Longrightarrow> x \<le> (y::real)"
4.138 -apply (subgoal_tac "0 \<le> y - x", simp)
4.139 -apply (rule LIMSEQ_le_const)
4.140 -apply (erule (1) tendsto_diff)
4.141 -apply (simp add: le_diff_eq)
4.142 -done
4.143 -
4.144 + by (rule LIMSEQ_le[of X x "\<lambda>n. a"]) (auto simp: tendsto_const)
4.145
4.146 subsection {* Convergence *}
4.147
4.148 @@ -531,88 +497,17 @@
4.149 apply (drule tendsto_minus, auto)
4.150 done
4.151
4.152 -lemma lim_le:
4.153 - fixes x :: real
4.154 - assumes f: "convergent f" and fn_le: "!!n. f n \<le> x"
4.155 - shows "lim f \<le> x"
4.156 -proof (rule classical)
4.157 - assume "\<not> lim f \<le> x"
4.158 - hence 0: "0 < lim f - x" by arith
4.159 - have 1: "f----> lim f"
4.160 - by (metis convergent_LIMSEQ_iff f)
4.161 - thus ?thesis
4.162 - proof (simp add: LIMSEQ_iff)
4.163 - assume "\<forall>r>0. \<exists>no. \<forall>n\<ge>no. \<bar>f n - lim f\<bar> < r"
4.164 - hence "\<exists>no. \<forall>n\<ge>no. \<bar>f n - lim f\<bar> < lim f - x"
4.165 - by (metis 0)
4.166 - from this obtain no where "\<forall>n\<ge>no. \<bar>f n - lim f\<bar> < lim f - x"
4.167 - by blast
4.168 - thus "lim f \<le> x"
4.169 - by (metis 1 LIMSEQ_le_const2 fn_le)
4.170 - qed
4.171 -qed
4.172 +lemma lim_le: "convergent f \<Longrightarrow> (\<And>n. f n \<le> (x::real)) \<Longrightarrow> lim f \<le> x"
4.173 + using LIMSEQ_le_const2[of f "lim f" x] by (simp add: convergent_LIMSEQ_iff)
4.174
4.175 lemma monoseq_le:
4.176 - fixes a :: "nat \<Rightarrow> real"
4.177 - assumes "monoseq a" and "a ----> x"
4.178 - shows "((\<forall> n. a n \<le> x) \<and> (\<forall>m. \<forall>n\<ge>m. a m \<le> a n)) \<or>
4.179 - ((\<forall> n. x \<le> a n) \<and> (\<forall>m. \<forall>n\<ge>m. a n \<le> a m))"
4.180 -proof -
4.181 - { fix x n fix a :: "nat \<Rightarrow> real"
4.182 - assume "a ----> x" and "\<forall> m. \<forall> n \<ge> m. a m \<le> a n"
4.183 - hence monotone: "\<And> m n. m \<le> n \<Longrightarrow> a m \<le> a n" by auto
4.184 - have "a n \<le> x"
4.185 - proof (rule ccontr)
4.186 - assume "\<not> a n \<le> x" hence "x < a n" by auto
4.187 - hence "0 < a n - x" by auto
4.188 - from `a ----> x`[THEN LIMSEQ_D, OF this]
4.189 - obtain no where "\<And>n'. no \<le> n' \<Longrightarrow> norm (a n' - x) < a n - x" by blast
4.190 - hence "norm (a (max no n) - x) < a n - x" by auto
4.191 - moreover
4.192 - { fix n' have "n \<le> n' \<Longrightarrow> x < a n'" using monotone[where m=n and n=n'] and `x < a n` by auto }
4.193 - hence "x < a (max no n)" by auto
4.194 - ultimately
4.195 - have "a (max no n) < a n" by auto
4.196 - with monotone[where m=n and n="max no n"]
4.197 - show False by (auto simp:max_def split:split_if_asm)
4.198 - qed
4.199 - } note top_down = this
4.200 - { fix x n m fix a :: "nat \<Rightarrow> real"
4.201 - assume "a ----> x" and "monoseq a" and "a m < x"
4.202 - have "a n \<le> x \<and> (\<forall> m. \<forall> n \<ge> m. a m \<le> a n)"
4.203 - proof (cases "\<forall> m. \<forall> n \<ge> m. a m \<le> a n")
4.204 - case True with top_down and `a ----> x` show ?thesis by auto
4.205 - next
4.206 - case False with `monoseq a`[unfolded monoseq_def] have "\<forall> m. \<forall> n \<ge> m. - a m \<le> - a n" by auto
4.207 - hence "- a m \<le> - x" using top_down[OF tendsto_minus[OF `a ----> x`]] by blast
4.208 - hence False using `a m < x` by auto
4.209 - thus ?thesis ..
4.210 - qed
4.211 - } note when_decided = this
4.212 -
4.213 - show ?thesis
4.214 - proof (cases "\<exists> m. a m \<noteq> x")
4.215 - case True then obtain m where "a m \<noteq> x" by auto
4.216 - show ?thesis
4.217 - proof (cases "a m < x")
4.218 - case True with when_decided[OF `a ----> x` `monoseq a`, where m2=m]
4.219 - show ?thesis by blast
4.220 - next
4.221 - case False hence "- a m < - x" using `a m \<noteq> x` by auto
4.222 - with when_decided[OF tendsto_minus[OF `a ----> x`] monoseq_minus[OF `monoseq a`], where m2=m]
4.223 - show ?thesis by auto
4.224 - qed
4.225 - qed auto
4.226 -qed
4.227 + "monoseq a \<Longrightarrow> a ----> (x::real) \<Longrightarrow>
4.228 + ((\<forall> n. a n \<le> x) \<and> (\<forall>m. \<forall>n\<ge>m. a m \<le> a n)) \<or> ((\<forall> n. x \<le> a n) \<and> (\<forall>m. \<forall>n\<ge>m. a n \<le> a m))"
4.229 + by (metis LIMSEQ_le_const LIMSEQ_le_const2 decseq_def incseq_def monoseq_iff)
4.230
4.231 lemma LIMSEQ_subseq_LIMSEQ:
4.232 "\<lbrakk> X ----> L; subseq f \<rbrakk> \<Longrightarrow> (X o f) ----> L"
4.233 -apply (rule topological_tendstoI)
4.234 -apply (drule (2) topological_tendstoD)
4.235 -apply (simp only: eventually_sequentially)
4.236 -apply (clarify, rule_tac x=N in exI, clarsimp)
4.237 -apply (blast intro: seq_suble le_trans dest!: spec)
4.238 -done
4.239 + unfolding comp_def by (rule filterlim_compose[of X, OF _ filterlim_subseq])
4.240
4.241 lemma convergent_subseq_convergent:
4.242 "\<lbrakk>convergent X; subseq f\<rbrakk> \<Longrightarrow> convergent (X o f)"
4.243 @@ -630,27 +525,16 @@
4.244 by (auto simp add: Bseq_def)
4.245
4.246 lemma lemma_NBseq_def:
4.247 - "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) =
4.248 - (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
4.249 -proof auto
4.250 + "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
4.251 +proof safe
4.252 fix K :: real
4.253 from reals_Archimedean2 obtain n :: nat where "K < real n" ..
4.254 then have "K \<le> real (Suc n)" by auto
4.255 - assume "\<forall>m. norm (X m) \<le> K"
4.256 - have "\<forall>m. norm (X m) \<le> real (Suc n)"
4.257 - proof
4.258 - fix m :: 'a
4.259 - from `\<forall>m. norm (X m) \<le> K` have "norm (X m) \<le> K" ..
4.260 - with `K \<le> real (Suc n)` show "norm (X m) \<le> real (Suc n)" by auto
4.261 - qed
4.262 + moreover assume "\<forall>m. norm (X m) \<le> K"
4.263 + ultimately have "\<forall>m. norm (X m) \<le> real (Suc n)"
4.264 + by (blast intro: order_trans)
4.265 then show "\<exists>N. \<forall>n. norm (X n) \<le> real (Suc N)" ..
4.266 -next
4.267 - fix N :: nat
4.268 - have "real (Suc N) > 0" by (simp add: real_of_nat_Suc)
4.269 - moreover assume "\<forall>n. norm (X n) \<le> real (Suc N)"
4.270 - ultimately show "\<exists>K>0. \<forall>n. norm (X n) \<le> K" by blast
4.271 -qed
4.272 -
4.273 +qed (force simp add: real_of_nat_Suc)
4.274
4.275 text{* alternative definition for Bseq *}
4.276 lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
4.277 @@ -672,6 +556,39 @@
4.278 lemma Bseq_iff1a: "Bseq X = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))"
4.279 by (simp add: Bseq_def lemma_NBseq_def2)
4.280
4.281 +subsubsection{*A Few More Equivalence Theorems for Boundedness*}
4.282 +
4.283 +text{*alternative formulation for boundedness*}
4.284 +lemma Bseq_iff2: "Bseq X = (\<exists>k > 0. \<exists>x. \<forall>n. norm (X(n) + -x) \<le> k)"
4.285 +apply (unfold Bseq_def, safe)
4.286 +apply (rule_tac [2] x = "k + norm x" in exI)
4.287 +apply (rule_tac x = K in exI, simp)
4.288 +apply (rule exI [where x = 0], auto)
4.289 +apply (erule order_less_le_trans, simp)
4.290 +apply (drule_tac x=n in spec, fold diff_minus)
4.291 +apply (drule order_trans [OF norm_triangle_ineq2])
4.292 +apply simp
4.293 +done
4.294 +
4.295 +text{*alternative formulation for boundedness*}
4.296 +lemma Bseq_iff3: "Bseq X = (\<exists>k > 0. \<exists>N. \<forall>n. norm(X(n) + -X(N)) \<le> k)"
4.297 +apply safe
4.298 +apply (simp add: Bseq_def, safe)
4.299 +apply (rule_tac x = "K + norm (X N)" in exI)
4.300 +apply auto
4.301 +apply (erule order_less_le_trans, simp)
4.302 +apply (rule_tac x = N in exI, safe)
4.303 +apply (drule_tac x = n in spec)
4.304 +apply (rule order_trans [OF norm_triangle_ineq], simp)
4.305 +apply (auto simp add: Bseq_iff2)
4.306 +done
4.307 +
4.308 +lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> (K::real)) ==> Bseq f"
4.309 +apply (simp add: Bseq_def)
4.310 +apply (rule_tac x = " (\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI, auto)
4.311 +apply (drule_tac x = n in spec, arith)
4.312 +done
4.313 +
4.314 subsubsection{*Upper Bounds and Lubs of Bounded Sequences*}
4.315
4.316 lemma Bseq_isUb:
4.317 @@ -725,115 +642,43 @@
4.318 text{*A standard proof of the theorem for monotone increasing sequence*}
4.319
4.320 lemma Bseq_mono_convergent:
4.321 - "[| Bseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> convergent (X::nat=>real)"
4.322 -proof -
4.323 - assume "Bseq X"
4.324 - then obtain u where u: "isLub UNIV {x. \<exists>n. X n = x} u"
4.325 - using Bseq_isLub by fast
4.326 - assume "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n"
4.327 - with u have "X ----> u"
4.328 - by (rule isLub_mono_imp_LIMSEQ)
4.329 - thus "convergent X"
4.330 - by (rule convergentI)
4.331 -qed
4.332 + "Bseq X \<Longrightarrow> \<forall>m. \<forall>n \<ge> m. X m \<le> X n \<Longrightarrow> convergent (X::nat=>real)"
4.333 + by (metis Bseq_isLub isLub_mono_imp_LIMSEQ convergentI)
4.334
4.335 lemma Bseq_minus_iff: "Bseq (%n. -(X n)) = Bseq X"
4.336 -by (simp add: Bseq_def)
4.337 + by (simp add: Bseq_def)
4.338
4.339 text{*Main monotonicity theorem*}
4.340 -lemma Bseq_monoseq_convergent: "[| Bseq X; monoseq X |] ==> convergent (X::nat\<Rightarrow>real)"
4.341 -apply (simp add: monoseq_def, safe)
4.342 -apply (rule_tac [2] convergent_minus_iff [THEN ssubst])
4.343 -apply (drule_tac [2] Bseq_minus_iff [THEN ssubst])
4.344 -apply (auto intro!: Bseq_mono_convergent)
4.345 -done
4.346 +
4.347 +lemma Bseq_monoseq_convergent: "Bseq X \<Longrightarrow> monoseq X \<Longrightarrow> convergent (X::nat\<Rightarrow>real)"
4.348 + by (metis monoseq_iff incseq_def decseq_eq_incseq convergent_minus_iff Bseq_minus_iff
4.349 + Bseq_mono_convergent)
4.350
4.351 subsubsection{*Increasing and Decreasing Series*}
4.352
4.353 -lemma incseq_le:
4.354 - fixes X :: "nat \<Rightarrow> real"
4.355 - assumes inc: "incseq X" and lim: "X ----> L" shows "X n \<le> L"
4.356 - using monoseq_le [OF incseq_imp_monoseq [OF inc] lim]
4.357 -proof
4.358 - assume "(\<forall>n. X n \<le> L) \<and> (\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n)"
4.359 - thus ?thesis by simp
4.360 -next
4.361 - assume "(\<forall>n. L \<le> X n) \<and> (\<forall>m n. m \<le> n \<longrightarrow> X n \<le> X m)"
4.362 - hence const: "(!!m n. m \<le> n \<Longrightarrow> X n = X m)" using inc
4.363 - by (auto simp add: incseq_def intro: order_antisym)
4.364 - have X: "!!n. X n = X 0"
4.365 - by (blast intro: const [of 0])
4.366 - have "X = (\<lambda>n. X 0)"
4.367 - by (blast intro: X)
4.368 - hence "L = X 0" using tendsto_const [of "X 0" sequentially]
4.369 - by (auto intro: LIMSEQ_unique lim)
4.370 - thus ?thesis
4.371 - by (blast intro: eq_refl X)
4.372 -qed
4.373 +lemma incseq_le: "incseq X \<Longrightarrow> X ----> L \<Longrightarrow> X n \<le> (L::real)"
4.374 + by (metis incseq_def LIMSEQ_le_const)
4.375
4.376 -lemma decseq_le:
4.377 - fixes X :: "nat \<Rightarrow> real" assumes dec: "decseq X" and lim: "X ----> L" shows "L \<le> X n"
4.378 -proof -
4.379 - have inc: "incseq (\<lambda>n. - X n)" using dec
4.380 - by (simp add: decseq_eq_incseq)
4.381 - have "- X n \<le> - L"
4.382 - by (blast intro: incseq_le [OF inc] tendsto_minus lim)
4.383 - thus ?thesis
4.384 - by simp
4.385 -qed
4.386 -
4.387 -subsubsection{*A Few More Equivalence Theorems for Boundedness*}
4.388 -
4.389 -text{*alternative formulation for boundedness*}
4.390 -lemma Bseq_iff2: "Bseq X = (\<exists>k > 0. \<exists>x. \<forall>n. norm (X(n) + -x) \<le> k)"
4.391 -apply (unfold Bseq_def, safe)
4.392 -apply (rule_tac [2] x = "k + norm x" in exI)
4.393 -apply (rule_tac x = K in exI, simp)
4.394 -apply (rule exI [where x = 0], auto)
4.395 -apply (erule order_less_le_trans, simp)
4.396 -apply (drule_tac x=n in spec, fold diff_minus)
4.397 -apply (drule order_trans [OF norm_triangle_ineq2])
4.398 -apply simp
4.399 -done
4.400 -
4.401 -text{*alternative formulation for boundedness*}
4.402 -lemma Bseq_iff3: "Bseq X = (\<exists>k > 0. \<exists>N. \<forall>n. norm(X(n) + -X(N)) \<le> k)"
4.403 -apply safe
4.404 -apply (simp add: Bseq_def, safe)
4.405 -apply (rule_tac x = "K + norm (X N)" in exI)
4.406 -apply auto
4.407 -apply (erule order_less_le_trans, simp)
4.408 -apply (rule_tac x = N in exI, safe)
4.409 -apply (drule_tac x = n in spec)
4.410 -apply (rule order_trans [OF norm_triangle_ineq], simp)
4.411 -apply (auto simp add: Bseq_iff2)
4.412 -done
4.413 -
4.414 -lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> (K::real)) ==> Bseq f"
4.415 -apply (simp add: Bseq_def)
4.416 -apply (rule_tac x = " (\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI, auto)
4.417 -apply (drule_tac x = n in spec, arith)
4.418 -done
4.419 -
4.420 +lemma decseq_le: "decseq X \<Longrightarrow> X ----> L \<Longrightarrow> (L::real) \<le> X n"
4.421 + by (metis decseq_def LIMSEQ_le_const2)
4.422
4.423 subsection {* Cauchy Sequences *}
4.424
4.425 lemma metric_CauchyI:
4.426 "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X"
4.427 -by (simp add: Cauchy_def)
4.428 + by (simp add: Cauchy_def)
4.429
4.430 lemma metric_CauchyD:
4.431 - "\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e"
4.432 -by (simp add: Cauchy_def)
4.433 + "Cauchy X \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e"
4.434 + by (simp add: Cauchy_def)
4.435
4.436 lemma Cauchy_iff:
4.437 fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
4.438 shows "Cauchy X \<longleftrightarrow> (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e)"
4.439 -unfolding Cauchy_def dist_norm ..
4.440 + unfolding Cauchy_def dist_norm ..
4.441
4.442 lemma Cauchy_iff2:
4.443 - "Cauchy X =
4.444 - (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m - X n\<bar> < inverse(real (Suc j))))"
4.445 + "Cauchy X = (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m - X n\<bar> < inverse(real (Suc j))))"
4.446 apply (simp add: Cauchy_iff, auto)
4.447 apply (drule reals_Archimedean, safe)
4.448 apply (drule_tac x = n in spec, auto)
4.449 @@ -934,24 +779,17 @@
4.450 lemma isUb_UNIV_I: "(\<And>y. y \<in> S \<Longrightarrow> y \<le> u) \<Longrightarrow> isUb UNIV S u"
4.451 by (simp add: isUbI setleI)
4.452
4.453 -locale real_Cauchy =
4.454 +lemma real_Cauchy_convergent:
4.455 fixes X :: "nat \<Rightarrow> real"
4.456 assumes X: "Cauchy X"
4.457 - fixes S :: "real set"
4.458 - defines S_def: "S \<equiv> {x::real. \<exists>N. \<forall>n\<ge>N. x < X n}"
4.459 + shows "convergent X"
4.460 +proof -
4.461 + def S \<equiv> "{x::real. \<exists>N. \<forall>n\<ge>N. x < X n}"
4.462 + then have mem_S: "\<And>N x. \<forall>n\<ge>N. x < X n \<Longrightarrow> x \<in> S" by auto
4.463
4.464 -lemma real_CauchyI:
4.465 - assumes "Cauchy X"
4.466 - shows "real_Cauchy X"
4.467 - proof qed (fact assms)
4.468 -
4.469 -lemma (in real_Cauchy) mem_S: "\<forall>n\<ge>N. x < X n \<Longrightarrow> x \<in> S"
4.470 -by (unfold S_def, auto)
4.471 -
4.472 -lemma (in real_Cauchy) bound_isUb:
4.473 - assumes N: "\<forall>n\<ge>N. X n < x"
4.474 - shows "isUb UNIV S x"
4.475 -proof (rule isUb_UNIV_I)
4.476 + { fix N x assume N: "\<forall>n\<ge>N. X n < x"
4.477 + have "isUb UNIV S x"
4.478 + proof (rule isUb_UNIV_I)
4.479 fix y::real assume "y \<in> S"
4.480 hence "\<exists>M. \<forall>n\<ge>M. y < X n"
4.481 by (simp add: S_def)
4.482 @@ -960,10 +798,11 @@
4.483 also have "\<dots> < x" using N by simp
4.484 finally show "y \<le> x"
4.485 by (rule order_less_imp_le)
4.486 -qed
4.487 + qed }
4.488 + note bound_isUb = this
4.489
4.490 -lemma (in real_Cauchy) isLub_ex: "\<exists>u. isLub UNIV S u"
4.491 -proof (rule reals_complete)
4.492 + have "\<exists>u. isLub UNIV S u"
4.493 + proof (rule reals_complete)
4.494 obtain N where "\<forall>m\<ge>N. \<forall>n\<ge>N. norm (X m - X n) < 1"
4.495 using CauchyD [OF X zero_less_one] by auto
4.496 hence N: "\<forall>n\<ge>N. norm (X n - X N) < 1" by simp
4.497 @@ -980,12 +819,10 @@
4.498 thus "isUb UNIV S (X N + 1)"
4.499 by (rule bound_isUb)
4.500 qed
4.501 -qed
4.502 -
4.503 -lemma (in real_Cauchy) isLub_imp_LIMSEQ:
4.504 - assumes x: "isLub UNIV S x"
4.505 - shows "X ----> x"
4.506 -proof (rule LIMSEQ_I)
4.507 + qed
4.508 + then obtain x where x: "isLub UNIV S x" ..
4.509 + have "X ----> x"
4.510 + proof (rule LIMSEQ_I)
4.511 fix r::real assume "0 < r"
4.512 hence r: "0 < r/2" by simp
4.513 obtain N where "\<forall>n\<ge>N. \<forall>m\<ge>N. norm (X n - X m) < r/2"
4.514 @@ -1009,26 +846,12 @@
4.515 thus "norm (X n - x) < r" using 1 2
4.516 by (simp add: abs_diff_less_iff)
4.517 qed
4.518 + qed
4.519 + then show ?thesis unfolding convergent_def by auto
4.520 qed
4.521
4.522 -lemma (in real_Cauchy) LIMSEQ_ex: "\<exists>x. X ----> x"
4.523 -proof -
4.524 - obtain x where "isLub UNIV S x"
4.525 - using isLub_ex by fast
4.526 - hence "X ----> x"
4.527 - by (rule isLub_imp_LIMSEQ)
4.528 - thus ?thesis ..
4.529 -qed
4.530 -
4.531 -lemma real_Cauchy_convergent:
4.532 - fixes X :: "nat \<Rightarrow> real"
4.533 - shows "Cauchy X \<Longrightarrow> convergent X"
4.534 -unfolding convergent_def
4.535 -by (rule real_Cauchy.LIMSEQ_ex)
4.536 - (rule real_CauchyI)
4.537 -
4.538 instance real :: banach
4.539 -by intro_classes (rule real_Cauchy_convergent)
4.540 + by intro_classes (rule real_Cauchy_convergent)
4.541
4.542
4.543 subsection {* Power Sequences *}
4.544 @@ -1053,53 +876,12 @@
4.545 "[| 0 \<le> (x::real); x \<le> 1 |] ==> convergent (%n. x ^ n)"
4.546 by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow)
4.547
4.548 -lemma LIMSEQ_inverse_realpow_zero_lemma:
4.549 - fixes x :: real
4.550 - assumes x: "0 \<le> x"
4.551 - shows "real n * x + 1 \<le> (x + 1) ^ n"
4.552 -apply (induct n)
4.553 -apply simp
4.554 -apply simp
4.555 -apply (rule order_trans)
4.556 -prefer 2
4.557 -apply (erule mult_left_mono)
4.558 -apply (rule add_increasing [OF x], simp)
4.559 -apply (simp add: real_of_nat_Suc)
4.560 -apply (simp add: ring_distribs)
4.561 -apply (simp add: mult_nonneg_nonneg x)
4.562 -done
4.563 -
4.564 -lemma LIMSEQ_inverse_realpow_zero:
4.565 - "1 < (x::real) \<Longrightarrow> (\<lambda>n. inverse (x ^ n)) ----> 0"
4.566 -proof (rule LIMSEQ_inverse_zero [rule_format])
4.567 - fix y :: real
4.568 - assume x: "1 < x"
4.569 - hence "0 < x - 1" by simp
4.570 - hence "\<forall>y. \<exists>N::nat. y < real N * (x - 1)"
4.571 - by (rule reals_Archimedean3)
4.572 - hence "\<exists>N::nat. y < real N * (x - 1)" ..
4.573 - then obtain N::nat where "y < real N * (x - 1)" ..
4.574 - also have "\<dots> \<le> real N * (x - 1) + 1" by simp
4.575 - also have "\<dots> \<le> (x - 1 + 1) ^ N"
4.576 - by (rule LIMSEQ_inverse_realpow_zero_lemma, cut_tac x, simp)
4.577 - also have "\<dots> = x ^ N" by simp
4.578 - finally have "y < x ^ N" .
4.579 - hence "\<forall>n\<ge>N. y < x ^ n"
4.580 - apply clarify
4.581 - apply (erule order_less_le_trans)
4.582 - apply (erule power_increasing)
4.583 - apply (rule order_less_imp_le [OF x])
4.584 - done
4.585 - thus "\<exists>N. \<forall>n\<ge>N. y < x ^ n" ..
4.586 -qed
4.587 +lemma LIMSEQ_inverse_realpow_zero: "1 < (x::real) \<Longrightarrow> (\<lambda>n. inverse (x ^ n)) ----> 0"
4.588 + by (rule filterlim_compose[OF tendsto_inverse_0 filterlim_realpow_sequentially_gt1]) simp
4.589
4.590 lemma LIMSEQ_realpow_zero:
4.591 "\<lbrakk>0 \<le> (x::real); x < 1\<rbrakk> \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0"
4.592 -proof (cases)
4.593 - assume "x = 0"
4.594 - hence "(\<lambda>n. x ^ Suc n) ----> 0" by (simp add: tendsto_const)
4.595 - thus ?thesis by (rule LIMSEQ_imp_Suc)
4.596 -next
4.597 +proof cases
4.598 assume "0 \<le> x" and "x \<noteq> 0"
4.599 hence x0: "0 < x" by simp
4.600 assume x1: "x < 1"
4.601 @@ -1108,7 +890,7 @@
4.602 hence "(\<lambda>n. inverse (inverse x ^ n)) ----> 0"
4.603 by (rule LIMSEQ_inverse_realpow_zero)
4.604 thus ?thesis by (simp add: power_inverse)
4.605 -qed
4.606 +qed (rule LIMSEQ_imp_Suc, simp add: tendsto_const)
4.607
4.608 lemma LIMSEQ_power_zero:
4.609 fixes x :: "'a::{real_normed_algebra_1}"
4.610 @@ -1118,22 +900,15 @@
4.611 apply (simp add: power_abs norm_power_ineq)
4.612 done
4.613
4.614 -lemma LIMSEQ_divide_realpow_zero:
4.615 - "1 < (x::real) ==> (%n. a / (x ^ n)) ----> 0"
4.616 -using tendsto_mult [OF tendsto_const [of a]
4.617 - LIMSEQ_realpow_zero [of "inverse x"]]
4.618 -apply (auto simp add: divide_inverse power_inverse)
4.619 -apply (simp add: inverse_eq_divide pos_divide_less_eq)
4.620 -done
4.621 +lemma LIMSEQ_divide_realpow_zero: "1 < x \<Longrightarrow> (\<lambda>n. a / (x ^ n) :: real) ----> 0"
4.622 + by (rule tendsto_divide_0 [OF tendsto_const filterlim_realpow_sequentially_gt1]) simp
4.623
4.624 text{*Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}*}
4.625
4.626 -lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < (1::real) ==> (%n. \<bar>c\<bar> ^ n) ----> 0"
4.627 -by (rule LIMSEQ_realpow_zero [OF abs_ge_zero])
4.628 +lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. \<bar>c\<bar> ^ n :: real) ----> 0"
4.629 + by (rule LIMSEQ_realpow_zero [OF abs_ge_zero])
4.630
4.631 -lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < (1::real) ==> (%n. c ^ n) ----> 0"
4.632 -apply (rule tendsto_rabs_zero_cancel)
4.633 -apply (auto intro: LIMSEQ_rabs_realpow_zero simp add: power_abs)
4.634 -done
4.635 +lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. c ^ n :: real) ----> 0"
4.636 + by (rule LIMSEQ_power_zero) simp
4.637
4.638 end
5.1 --- a/src/HOL/Series.thy Mon Dec 03 18:19:11 2012 +0100
5.2 +++ b/src/HOL/Series.thy Mon Dec 03 18:19:12 2012 +0100
5.3 @@ -650,6 +650,7 @@
5.4 lemma rabs_ratiotest_lemma: "[| c \<le> 0; abs x \<le> c * abs y |] ==> x = (0::real)"
5.5 by (erule norm_ratiotest_lemma, simp)
5.6
5.7 +(* TODO: MOVE *)
5.8 lemma le_Suc_ex: "(k::nat) \<le> l ==> (\<exists>n. l = k + n)"
5.9 apply (drule le_imp_less_or_eq)
5.10 apply (auto dest: less_imp_Suc_add)