move SEQ.thy and Lim.thy to Limits.thy
authorhoelzl
Tue Mar 26 12:20:58 2013 +0100 (2013-03-26)
changeset 51526155263089e7b
parent 51525 d3d170a2887f
child 51527 bd62e7ff103b
move SEQ.thy and Lim.thy to Limits.thy
src/HOL/Deriv.thy
src/HOL/Library/Diagonal_Subsequence.thy
src/HOL/Lim.thy
src/HOL/Limits.thy
src/HOL/SEQ.thy
src/HOL/Series.thy
     1.1 --- a/src/HOL/Deriv.thy	Tue Mar 26 12:20:58 2013 +0100
     1.2 +++ b/src/HOL/Deriv.thy	Tue Mar 26 12:20:58 2013 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  header{* Differentiation *}
     1.5  
     1.6  theory Deriv
     1.7 -imports Lim
     1.8 +imports Limits
     1.9  begin
    1.10  
    1.11  text{*Standard Definitions*}
     2.1 --- a/src/HOL/Library/Diagonal_Subsequence.thy	Tue Mar 26 12:20:58 2013 +0100
     2.2 +++ b/src/HOL/Library/Diagonal_Subsequence.thy	Tue Mar 26 12:20:58 2013 +0100
     2.3 @@ -3,7 +3,7 @@
     2.4  header {* Sequence of Properties on Subsequences *}
     2.5  
     2.6  theory Diagonal_Subsequence
     2.7 -imports SEQ
     2.8 +imports Complex_Main
     2.9  begin
    2.10  
    2.11  locale subseqs =
     3.1 --- a/src/HOL/Lim.thy	Tue Mar 26 12:20:58 2013 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,225 +0,0 @@
     3.4 -(*  Title       : Lim.thy
     3.5 -    Author      : Jacques D. Fleuriot
     3.6 -    Copyright   : 1998  University of Cambridge
     3.7 -    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     3.8 -*)
     3.9 -
    3.10 -header{* Limits and Continuity *}
    3.11 -
    3.12 -theory Lim
    3.13 -imports SEQ
    3.14 -begin
    3.15 -
    3.16 -subsection {* Limits of Functions *}
    3.17 -
    3.18 -lemma LIM_eq:
    3.19 -  fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
    3.20 -  shows "f -- a --> L =
    3.21 -     (\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)"
    3.22 -by (simp add: LIM_def dist_norm)
    3.23 -
    3.24 -lemma LIM_I:
    3.25 -  fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
    3.26 -  shows "(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)
    3.27 -      ==> f -- a --> L"
    3.28 -by (simp add: LIM_eq)
    3.29 -
    3.30 -lemma LIM_D:
    3.31 -  fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
    3.32 -  shows "[| f -- a --> L; 0<r |]
    3.33 -      ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r"
    3.34 -by (simp add: LIM_eq)
    3.35 -
    3.36 -lemma LIM_offset:
    3.37 -  fixes a :: "'a::real_normed_vector"
    3.38 -  shows "f -- a --> L \<Longrightarrow> (\<lambda>x. f (x + k)) -- a - k --> L"
    3.39 -apply (rule topological_tendstoI)
    3.40 -apply (drule (2) topological_tendstoD)
    3.41 -apply (simp only: eventually_at dist_norm)
    3.42 -apply (clarify, rule_tac x=d in exI, safe)
    3.43 -apply (drule_tac x="x + k" in spec)
    3.44 -apply (simp add: algebra_simps)
    3.45 -done
    3.46 -
    3.47 -lemma LIM_offset_zero:
    3.48 -  fixes a :: "'a::real_normed_vector"
    3.49 -  shows "f -- a --> L \<Longrightarrow> (\<lambda>h. f (a + h)) -- 0 --> L"
    3.50 -by (drule_tac k="a" in LIM_offset, simp add: add_commute)
    3.51 -
    3.52 -lemma LIM_offset_zero_cancel:
    3.53 -  fixes a :: "'a::real_normed_vector"
    3.54 -  shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L"
    3.55 -by (drule_tac k="- a" in LIM_offset, simp)
    3.56 -
    3.57 -lemma LIM_zero:
    3.58 -  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    3.59 -  shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. f x - l) ---> 0) F"
    3.60 -unfolding tendsto_iff dist_norm by simp
    3.61 -
    3.62 -lemma LIM_zero_cancel:
    3.63 -  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    3.64 -  shows "((\<lambda>x. f x - l) ---> 0) F \<Longrightarrow> (f ---> l) F"
    3.65 -unfolding tendsto_iff dist_norm by simp
    3.66 -
    3.67 -lemma LIM_zero_iff:
    3.68 -  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
    3.69 -  shows "((\<lambda>x. f x - l) ---> 0) F = (f ---> l) F"
    3.70 -unfolding tendsto_iff dist_norm by simp
    3.71 -
    3.72 -lemma LIM_imp_LIM:
    3.73 -  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    3.74 -  fixes g :: "'a::topological_space \<Rightarrow> 'c::real_normed_vector"
    3.75 -  assumes f: "f -- a --> l"
    3.76 -  assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)"
    3.77 -  shows "g -- a --> m"
    3.78 -  by (rule metric_LIM_imp_LIM [OF f],
    3.79 -    simp add: dist_norm le)
    3.80 -
    3.81 -lemma LIM_equal2:
    3.82 -  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
    3.83 -  assumes 1: "0 < R"
    3.84 -  assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < R\<rbrakk> \<Longrightarrow> f x = g x"
    3.85 -  shows "g -- a --> l \<Longrightarrow> f -- a --> l"
    3.86 -by (rule metric_LIM_equal2 [OF 1 2], simp_all add: dist_norm)
    3.87 -
    3.88 -lemma LIM_compose2:
    3.89 -  fixes a :: "'a::real_normed_vector"
    3.90 -  assumes f: "f -- a --> b"
    3.91 -  assumes g: "g -- b --> c"
    3.92 -  assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> b"
    3.93 -  shows "(\<lambda>x. g (f x)) -- a --> c"
    3.94 -by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]])
    3.95 -
    3.96 -lemma real_LIM_sandwich_zero:
    3.97 -  fixes f g :: "'a::topological_space \<Rightarrow> real"
    3.98 -  assumes f: "f -- a --> 0"
    3.99 -  assumes 1: "\<And>x. x \<noteq> a \<Longrightarrow> 0 \<le> g x"
   3.100 -  assumes 2: "\<And>x. x \<noteq> a \<Longrightarrow> g x \<le> f x"
   3.101 -  shows "g -- a --> 0"
   3.102 -proof (rule LIM_imp_LIM [OF f]) (* FIXME: use tendsto_sandwich *)
   3.103 -  fix x assume x: "x \<noteq> a"
   3.104 -  have "norm (g x - 0) = g x" by (simp add: 1 x)
   3.105 -  also have "g x \<le> f x" by (rule 2 [OF x])
   3.106 -  also have "f x \<le> \<bar>f x\<bar>" by (rule abs_ge_self)
   3.107 -  also have "\<bar>f x\<bar> = norm (f x - 0)" by simp
   3.108 -  finally show "norm (g x - 0) \<le> norm (f x - 0)" .
   3.109 -qed
   3.110 -
   3.111 -
   3.112 -subsection {* Continuity *}
   3.113 -
   3.114 -lemma LIM_isCont_iff:
   3.115 -  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
   3.116 -  shows "(f -- a --> f a) = ((\<lambda>h. f (a + h)) -- 0 --> f a)"
   3.117 -by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel])
   3.118 -
   3.119 -lemma isCont_iff:
   3.120 -  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
   3.121 -  shows "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x"
   3.122 -by (simp add: isCont_def LIM_isCont_iff)
   3.123 -
   3.124 -lemma isCont_LIM_compose2:
   3.125 -  fixes a :: "'a::real_normed_vector"
   3.126 -  assumes f [unfolded isCont_def]: "isCont f a"
   3.127 -  assumes g: "g -- f a --> l"
   3.128 -  assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> f a"
   3.129 -  shows "(\<lambda>x. g (f x)) -- a --> l"
   3.130 -by (rule LIM_compose2 [OF f g inj])
   3.131 -
   3.132 -
   3.133 -lemma isCont_norm [simp]:
   3.134 -  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   3.135 -  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a"
   3.136 -  by (fact continuous_norm)
   3.137 -
   3.138 -lemma isCont_rabs [simp]:
   3.139 -  fixes f :: "'a::t2_space \<Rightarrow> real"
   3.140 -  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x\<bar>) a"
   3.141 -  by (fact continuous_rabs)
   3.142 -
   3.143 -lemma isCont_add [simp]:
   3.144 -  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   3.145 -  shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"
   3.146 -  by (fact continuous_add)
   3.147 -
   3.148 -lemma isCont_minus [simp]:
   3.149 -  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   3.150 -  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a"
   3.151 -  by (fact continuous_minus)
   3.152 -
   3.153 -lemma isCont_diff [simp]:
   3.154 -  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   3.155 -  shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a"
   3.156 -  by (fact continuous_diff)
   3.157 -
   3.158 -lemma isCont_mult [simp]:
   3.159 -  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_algebra"
   3.160 -  shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x * g x) a"
   3.161 -  by (fact continuous_mult)
   3.162 -
   3.163 -lemma (in bounded_linear) isCont:
   3.164 -  "isCont g a \<Longrightarrow> isCont (\<lambda>x. f (g x)) a"
   3.165 -  by (fact continuous)
   3.166 -
   3.167 -lemma (in bounded_bilinear) isCont:
   3.168 -  "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
   3.169 -  by (fact continuous)
   3.170 -
   3.171 -lemmas isCont_scaleR [simp] = 
   3.172 -  bounded_bilinear.isCont [OF bounded_bilinear_scaleR]
   3.173 -
   3.174 -lemmas isCont_of_real [simp] =
   3.175 -  bounded_linear.isCont [OF bounded_linear_of_real]
   3.176 -
   3.177 -lemma isCont_power [simp]:
   3.178 -  fixes f :: "'a::t2_space \<Rightarrow> 'b::{power,real_normed_algebra}"
   3.179 -  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
   3.180 -  by (fact continuous_power)
   3.181 -
   3.182 -lemma isCont_setsum [simp]:
   3.183 -  fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::real_normed_vector"
   3.184 -  shows "\<forall>i\<in>A. isCont (f i) a \<Longrightarrow> isCont (\<lambda>x. \<Sum>i\<in>A. f i x) a"
   3.185 -  by (auto intro: continuous_setsum)
   3.186 -
   3.187 -lemmas isCont_intros =
   3.188 -  isCont_ident isCont_const isCont_norm isCont_rabs isCont_add isCont_minus
   3.189 -  isCont_diff isCont_mult isCont_inverse isCont_divide isCont_scaleR
   3.190 -  isCont_of_real isCont_power isCont_sgn isCont_setsum
   3.191 -
   3.192 -subsection {* Uniform Continuity *}
   3.193 -
   3.194 -lemma (in bounded_linear) isUCont: "isUCont f"
   3.195 -unfolding isUCont_def dist_norm
   3.196 -proof (intro allI impI)
   3.197 -  fix r::real assume r: "0 < r"
   3.198 -  obtain K where K: "0 < K" and norm_le: "\<And>x. norm (f x) \<le> norm x * K"
   3.199 -    using pos_bounded by fast
   3.200 -  show "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r"
   3.201 -  proof (rule exI, safe)
   3.202 -    from r K show "0 < r / K" by (rule divide_pos_pos)
   3.203 -  next
   3.204 -    fix x y :: 'a
   3.205 -    assume xy: "norm (x - y) < r / K"
   3.206 -    have "norm (f x - f y) = norm (f (x - y))" by (simp only: diff)
   3.207 -    also have "\<dots> \<le> norm (x - y) * K" by (rule norm_le)
   3.208 -    also from K xy have "\<dots> < r" by (simp only: pos_less_divide_eq)
   3.209 -    finally show "norm (f x - f y) < r" .
   3.210 -  qed
   3.211 -qed
   3.212 -
   3.213 -lemma (in bounded_linear) Cauchy: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
   3.214 -by (rule isUCont [THEN isUCont_Cauchy])
   3.215 -
   3.216 -
   3.217 -lemma LIM_less_bound: 
   3.218 -  fixes f :: "real \<Rightarrow> real"
   3.219 -  assumes ev: "b < x" "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and "isCont f x"
   3.220 -  shows "0 \<le> f x"
   3.221 -proof (rule tendsto_le_const)
   3.222 -  show "(f ---> f x) (at_left x)"
   3.223 -    using `isCont f x` by (simp add: filterlim_at_split isCont_def)
   3.224 -  show "eventually (\<lambda>x. 0 \<le> f x) (at_left x)"
   3.225 -    using ev by (auto simp: eventually_within_less dist_real_def intro!: exI[of _ "x - b"])
   3.226 -qed simp
   3.227 -
   3.228 -end
     4.1 --- a/src/HOL/Limits.thy	Tue Mar 26 12:20:58 2013 +0100
     4.2 +++ b/src/HOL/Limits.thy	Tue Mar 26 12:20:58 2013 +0100
     4.3 @@ -1,13 +1,23 @@
     4.4 -(*  Title       : Limits.thy
     4.5 -    Author      : Brian Huffman
     4.6 +(*  Title:      Limits.thy
     4.7 +    Author:     Brian Huffman
     4.8 +    Author:     Jacques D. Fleuriot, University of Cambridge
     4.9 +    Author:     Lawrence C Paulson
    4.10 +    Author:     Jeremy Avigad
    4.11 +
    4.12  *)
    4.13  
    4.14 -header {* Filters and Limits *}
    4.15 +header {* Limits on Real Vector Spaces *}
    4.16  
    4.17  theory Limits
    4.18  imports Real_Vector_Spaces
    4.19  begin
    4.20  
    4.21 +(* Unfortunately eventually_within was overwritten by Multivariate_Analysis.
    4.22 +   Hence it was references as Limits.eventually_within, but now it is Basic_Topology.eventually_within *)
    4.23 +lemmas eventually_within = eventually_within
    4.24 +
    4.25 +subsection {* Filter going to infinity norm *}
    4.26 +
    4.27  definition at_infinity :: "'a::real_normed_vector filter" where
    4.28    "at_infinity = Abs_filter (\<lambda>P. \<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x)"
    4.29  
    4.30 @@ -1027,9 +1037,616 @@
    4.31  qed simp
    4.32  
    4.33  
    4.34 -(* Unfortunately eventually_within was overwritten by Multivariate_Analysis.
    4.35 -   Hence it was references as Limits.within, but now it is Basic_Topology.eventually_within *)
    4.36 -lemmas eventually_within = eventually_within
    4.37 +subsection {* Limits of Sequences *}
    4.38 +
    4.39 +lemma [trans]: "X=Y ==> Y ----> z ==> X ----> z"
    4.40 +  by simp
    4.41 +
    4.42 +lemma LIMSEQ_iff:
    4.43 +  fixes L :: "'a::real_normed_vector"
    4.44 +  shows "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)"
    4.45 +unfolding LIMSEQ_def dist_norm ..
    4.46 +
    4.47 +lemma LIMSEQ_I:
    4.48 +  fixes L :: "'a::real_normed_vector"
    4.49 +  shows "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r) \<Longrightarrow> X ----> L"
    4.50 +by (simp add: LIMSEQ_iff)
    4.51 +
    4.52 +lemma LIMSEQ_D:
    4.53 +  fixes L :: "'a::real_normed_vector"
    4.54 +  shows "\<lbrakk>X ----> L; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r"
    4.55 +by (simp add: LIMSEQ_iff)
    4.56 +
    4.57 +lemma LIMSEQ_linear: "\<lbrakk> X ----> x ; l > 0 \<rbrakk> \<Longrightarrow> (\<lambda> n. X (n * l)) ----> x"
    4.58 +  unfolding tendsto_def eventually_sequentially
    4.59 +  by (metis div_le_dividend div_mult_self1_is_m le_trans nat_mult_commute)
    4.60 +
    4.61 +lemma Bseq_inverse_lemma:
    4.62 +  fixes x :: "'a::real_normed_div_algebra"
    4.63 +  shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r"
    4.64 +apply (subst nonzero_norm_inverse, clarsimp)
    4.65 +apply (erule (1) le_imp_inverse_le)
    4.66 +done
    4.67 +
    4.68 +lemma Bseq_inverse:
    4.69 +  fixes a :: "'a::real_normed_div_algebra"
    4.70 +  shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> Bseq (\<lambda>n. inverse (X n))"
    4.71 +  by (rule Bfun_inverse)
    4.72 +
    4.73 +lemma LIMSEQ_diff_approach_zero:
    4.74 +  fixes L :: "'a::real_normed_vector"
    4.75 +  shows "g ----> L ==> (%x. f x - g x) ----> 0 ==> f ----> L"
    4.76 +  by (drule (1) tendsto_add, simp)
    4.77 +
    4.78 +lemma LIMSEQ_diff_approach_zero2:
    4.79 +  fixes L :: "'a::real_normed_vector"
    4.80 +  shows "f ----> L ==> (%x. f x - g x) ----> 0 ==> g ----> L"
    4.81 +  by (drule (1) tendsto_diff, simp)
    4.82 +
    4.83 +text{*An unbounded sequence's inverse tends to 0*}
    4.84 +
    4.85 +lemma LIMSEQ_inverse_zero:
    4.86 +  "\<forall>r::real. \<exists>N. \<forall>n\<ge>N. r < X n \<Longrightarrow> (\<lambda>n. inverse (X n)) ----> 0"
    4.87 +  apply (rule filterlim_compose[OF tendsto_inverse_0])
    4.88 +  apply (simp add: filterlim_at_infinity[OF order_refl] eventually_sequentially)
    4.89 +  apply (metis abs_le_D1 linorder_le_cases linorder_not_le)
    4.90 +  done
    4.91 +
    4.92 +text{*The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity*}
    4.93 +
    4.94 +lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----> 0"
    4.95 +  by (metis filterlim_compose tendsto_inverse_0 filterlim_mono order_refl filterlim_Suc
    4.96 +            filterlim_compose[OF filterlim_real_sequentially] at_top_le_at_infinity)
    4.97 +
    4.98 +text{*The sequence @{term "r + 1/n"} tends to @{term r} as @{term n} tends to
    4.99 +infinity is now easily proved*}
   4.100 +
   4.101 +lemma LIMSEQ_inverse_real_of_nat_add:
   4.102 +     "(%n. r + inverse(real(Suc n))) ----> r"
   4.103 +  using tendsto_add [OF tendsto_const LIMSEQ_inverse_real_of_nat] by auto
   4.104 +
   4.105 +lemma LIMSEQ_inverse_real_of_nat_add_minus:
   4.106 +     "(%n. r + -inverse(real(Suc n))) ----> r"
   4.107 +  using tendsto_add [OF tendsto_const tendsto_minus [OF LIMSEQ_inverse_real_of_nat]]
   4.108 +  by auto
   4.109 +
   4.110 +lemma LIMSEQ_inverse_real_of_nat_add_minus_mult:
   4.111 +     "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r"
   4.112 +  using tendsto_mult [OF tendsto_const LIMSEQ_inverse_real_of_nat_add_minus [of 1]]
   4.113 +  by auto
   4.114 +
   4.115 +subsection {* Convergence on sequences *}
   4.116 +
   4.117 +lemma convergent_add:
   4.118 +  fixes X Y :: "nat \<Rightarrow> 'a::real_normed_vector"
   4.119 +  assumes "convergent (\<lambda>n. X n)"
   4.120 +  assumes "convergent (\<lambda>n. Y n)"
   4.121 +  shows "convergent (\<lambda>n. X n + Y n)"
   4.122 +  using assms unfolding convergent_def by (fast intro: tendsto_add)
   4.123 +
   4.124 +lemma convergent_setsum:
   4.125 +  fixes X :: "'a \<Rightarrow> nat \<Rightarrow> 'b::real_normed_vector"
   4.126 +  assumes "\<And>i. i \<in> A \<Longrightarrow> convergent (\<lambda>n. X i n)"
   4.127 +  shows "convergent (\<lambda>n. \<Sum>i\<in>A. X i n)"
   4.128 +proof (cases "finite A")
   4.129 +  case True from this and assms show ?thesis
   4.130 +    by (induct A set: finite) (simp_all add: convergent_const convergent_add)
   4.131 +qed (simp add: convergent_const)
   4.132 +
   4.133 +lemma (in bounded_linear) convergent:
   4.134 +  assumes "convergent (\<lambda>n. X n)"
   4.135 +  shows "convergent (\<lambda>n. f (X n))"
   4.136 +  using assms unfolding convergent_def by (fast intro: tendsto)
   4.137 +
   4.138 +lemma (in bounded_bilinear) convergent:
   4.139 +  assumes "convergent (\<lambda>n. X n)" and "convergent (\<lambda>n. Y n)"
   4.140 +  shows "convergent (\<lambda>n. X n ** Y n)"
   4.141 +  using assms unfolding convergent_def by (fast intro: tendsto)
   4.142 +
   4.143 +lemma convergent_minus_iff:
   4.144 +  fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
   4.145 +  shows "convergent X \<longleftrightarrow> convergent (\<lambda>n. - X n)"
   4.146 +apply (simp add: convergent_def)
   4.147 +apply (auto dest: tendsto_minus)
   4.148 +apply (drule tendsto_minus, auto)
   4.149 +done
   4.150 +
   4.151 +subsection {* Bounded Monotonic Sequences *}
   4.152 +
   4.153 +subsubsection {* Bounded Sequences *}
   4.154 +
   4.155 +lemma BseqI': "(\<And>n. norm (X n) \<le> K) \<Longrightarrow> Bseq X"
   4.156 +  by (intro BfunI) (auto simp: eventually_sequentially)
   4.157 +
   4.158 +lemma BseqI2': "\<forall>n\<ge>N. norm (X n) \<le> K \<Longrightarrow> Bseq X"
   4.159 +  by (intro BfunI) (auto simp: eventually_sequentially)
   4.160 +
   4.161 +lemma Bseq_def: "Bseq X \<longleftrightarrow> (\<exists>K>0. \<forall>n. norm (X n) \<le> K)"
   4.162 +  unfolding Bfun_def eventually_sequentially
   4.163 +proof safe
   4.164 +  fix N K assume "0 < K" "\<forall>n\<ge>N. norm (X n) \<le> K"
   4.165 +  then show "\<exists>K>0. \<forall>n. norm (X n) \<le> K"
   4.166 +    by (intro exI[of _ "max (Max (norm ` X ` {..N})) K"] min_max.less_supI2)
   4.167 +       (auto intro!: imageI not_less[where 'a=nat, THEN iffD1] Max_ge simp: le_max_iff_disj)
   4.168 +qed auto
   4.169 +
   4.170 +lemma BseqE: "\<lbrakk>Bseq X; \<And>K. \<lbrakk>0 < K; \<forall>n. norm (X n) \<le> K\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
   4.171 +unfolding Bseq_def by auto
   4.172 +
   4.173 +lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. norm (X n) \<le> K)"
   4.174 +by (simp add: Bseq_def)
   4.175 +
   4.176 +lemma BseqI: "[| 0 < K; \<forall>n. norm (X n) \<le> K |] ==> Bseq X"
   4.177 +by (auto simp add: Bseq_def)
   4.178 +
   4.179 +lemma lemma_NBseq_def:
   4.180 +  "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
   4.181 +proof safe
   4.182 +  fix K :: real
   4.183 +  from reals_Archimedean2 obtain n :: nat where "K < real n" ..
   4.184 +  then have "K \<le> real (Suc n)" by auto
   4.185 +  moreover assume "\<forall>m. norm (X m) \<le> K"
   4.186 +  ultimately have "\<forall>m. norm (X m) \<le> real (Suc n)"
   4.187 +    by (blast intro: order_trans)
   4.188 +  then show "\<exists>N. \<forall>n. norm (X n) \<le> real (Suc N)" ..
   4.189 +qed (force simp add: real_of_nat_Suc)
   4.190 +
   4.191 +text{* alternative definition for Bseq *}
   4.192 +lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
   4.193 +apply (simp add: Bseq_def)
   4.194 +apply (simp (no_asm) add: lemma_NBseq_def)
   4.195 +done
   4.196 +
   4.197 +lemma lemma_NBseq_def2:
   4.198 +     "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))"
   4.199 +apply (subst lemma_NBseq_def, auto)
   4.200 +apply (rule_tac x = "Suc N" in exI)
   4.201 +apply (rule_tac [2] x = N in exI)
   4.202 +apply (auto simp add: real_of_nat_Suc)
   4.203 + prefer 2 apply (blast intro: order_less_imp_le)
   4.204 +apply (drule_tac x = n in spec, simp)
   4.205 +done
   4.206 +
   4.207 +(* yet another definition for Bseq *)
   4.208 +lemma Bseq_iff1a: "Bseq X = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))"
   4.209 +by (simp add: Bseq_def lemma_NBseq_def2)
   4.210 +
   4.211 +subsubsection{*A Few More Equivalence Theorems for Boundedness*}
   4.212 +
   4.213 +text{*alternative formulation for boundedness*}
   4.214 +lemma Bseq_iff2: "Bseq X = (\<exists>k > 0. \<exists>x. \<forall>n. norm (X(n) + -x) \<le> k)"
   4.215 +apply (unfold Bseq_def, safe)
   4.216 +apply (rule_tac [2] x = "k + norm x" in exI)
   4.217 +apply (rule_tac x = K in exI, simp)
   4.218 +apply (rule exI [where x = 0], auto)
   4.219 +apply (erule order_less_le_trans, simp)
   4.220 +apply (drule_tac x=n in spec, fold diff_minus)
   4.221 +apply (drule order_trans [OF norm_triangle_ineq2])
   4.222 +apply simp
   4.223 +done
   4.224 +
   4.225 +text{*alternative formulation for boundedness*}
   4.226 +lemma Bseq_iff3: "Bseq X = (\<exists>k > 0. \<exists>N. \<forall>n. norm(X(n) + -X(N)) \<le> k)"
   4.227 +apply safe
   4.228 +apply (simp add: Bseq_def, safe)
   4.229 +apply (rule_tac x = "K + norm (X N)" in exI)
   4.230 +apply auto
   4.231 +apply (erule order_less_le_trans, simp)
   4.232 +apply (rule_tac x = N in exI, safe)
   4.233 +apply (drule_tac x = n in spec)
   4.234 +apply (rule order_trans [OF norm_triangle_ineq], simp)
   4.235 +apply (auto simp add: Bseq_iff2)
   4.236 +done
   4.237 +
   4.238 +lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> (K::real)) ==> Bseq f"
   4.239 +apply (simp add: Bseq_def)
   4.240 +apply (rule_tac x = " (\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI, auto)
   4.241 +apply (drule_tac x = n in spec, arith)
   4.242 +done
   4.243 +
   4.244 +subsubsection{*Upper Bounds and Lubs of Bounded Sequences*}
   4.245 +
   4.246 +lemma Bseq_isUb:
   4.247 +  "!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U"
   4.248 +by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff)
   4.249 +
   4.250 +text{* Use completeness of reals (supremum property)
   4.251 +   to show that any bounded sequence has a least upper bound*}
   4.252 +
   4.253 +lemma Bseq_isLub:
   4.254 +  "!!(X::nat=>real). Bseq X ==>
   4.255 +   \<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U"
   4.256 +by (blast intro: reals_complete Bseq_isUb)
   4.257 +
   4.258 +subsubsection{*A Bounded and Monotonic Sequence Converges*}
   4.259 +
   4.260 +(* TODO: delete *)
   4.261 +(* FIXME: one use in NSA/HSEQ.thy *)
   4.262 +lemma Bmonoseq_LIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X ----> L)"
   4.263 +  apply (rule_tac x="X m" in exI)
   4.264 +  apply (rule filterlim_cong[THEN iffD2, OF refl refl _ tendsto_const])
   4.265 +  unfolding eventually_sequentially
   4.266 +  apply blast
   4.267 +  done
   4.268 +
   4.269 +text {* A monotone sequence converges to its least upper bound. *}
   4.270 +
   4.271 +lemma isLub_mono_imp_LIMSEQ:
   4.272 +  fixes X :: "nat \<Rightarrow> real"
   4.273 +  assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use 'range X' *)
   4.274 +  assumes X: "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n"
   4.275 +  shows "X ----> u"
   4.276 +proof (rule LIMSEQ_I)
   4.277 +  have 1: "\<forall>n. X n \<le> u"
   4.278 +    using isLubD2 [OF u] by auto
   4.279 +  have "\<forall>y. (\<forall>n. X n \<le> y) \<longrightarrow> u \<le> y"
   4.280 +    using isLub_le_isUb [OF u] by (auto simp add: isUb_def setle_def)
   4.281 +  hence 2: "\<forall>y<u. \<exists>n. y < X n"
   4.282 +    by (metis not_le)
   4.283 +  fix r :: real assume "0 < r"
   4.284 +  hence "u - r < u" by simp
   4.285 +  hence "\<exists>m. u - r < X m" using 2 by simp
   4.286 +  then obtain m where "u - r < X m" ..
   4.287 +  with X have "\<forall>n\<ge>m. u - r < X n"
   4.288 +    by (fast intro: less_le_trans)
   4.289 +  hence "\<exists>m. \<forall>n\<ge>m. u - r < X n" ..
   4.290 +  thus "\<exists>m. \<forall>n\<ge>m. norm (X n - u) < r"
   4.291 +    using 1 by (simp add: diff_less_eq add_commute)
   4.292 +qed
   4.293 +
   4.294 +text{*A standard proof of the theorem for monotone increasing sequence*}
   4.295 +
   4.296 +lemma Bseq_mono_convergent:
   4.297 +   "Bseq X \<Longrightarrow> \<forall>m. \<forall>n \<ge> m. X m \<le> X n \<Longrightarrow> convergent (X::nat=>real)"
   4.298 +  by (metis Bseq_isLub isLub_mono_imp_LIMSEQ convergentI)
   4.299 +
   4.300 +lemma Bseq_minus_iff: "Bseq (%n. -(X n) :: 'a :: real_normed_vector) = Bseq X"
   4.301 +  by (simp add: Bseq_def)
   4.302 +
   4.303 +text{*Main monotonicity theorem*}
   4.304 +
   4.305 +lemma Bseq_monoseq_convergent: "Bseq X \<Longrightarrow> monoseq X \<Longrightarrow> convergent (X::nat\<Rightarrow>real)"
   4.306 +  by (metis monoseq_iff incseq_def decseq_eq_incseq convergent_minus_iff Bseq_minus_iff
   4.307 +            Bseq_mono_convergent)
   4.308 +
   4.309 +lemma Cauchy_iff:
   4.310 +  fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
   4.311 +  shows "Cauchy X \<longleftrightarrow> (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e)"
   4.312 +  unfolding Cauchy_def dist_norm ..
   4.313 +
   4.314 +lemma CauchyI:
   4.315 +  fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
   4.316 +  shows "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e) \<Longrightarrow> Cauchy X"
   4.317 +by (simp add: Cauchy_iff)
   4.318 +
   4.319 +lemma CauchyD:
   4.320 +  fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
   4.321 +  shows "\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e"
   4.322 +by (simp add: Cauchy_iff)
   4.323 +
   4.324 +lemma Bseq_eq_bounded: "range f \<subseteq> {a .. b::real} \<Longrightarrow> Bseq f"
   4.325 +  apply (simp add: subset_eq)
   4.326 +  apply (rule BseqI'[where K="max (norm a) (norm b)"])
   4.327 +  apply (erule_tac x=n in allE)
   4.328 +  apply auto
   4.329 +  done
   4.330 +
   4.331 +lemma incseq_bounded: "incseq X \<Longrightarrow> \<forall>i. X i \<le> (B::real) \<Longrightarrow> Bseq X"
   4.332 +  by (intro Bseq_eq_bounded[of X "X 0" B]) (auto simp: incseq_def)
   4.333 +
   4.334 +lemma decseq_bounded: "decseq X \<Longrightarrow> \<forall>i. (B::real) \<le> X i \<Longrightarrow> Bseq X"
   4.335 +  by (intro Bseq_eq_bounded[of X B "X 0"]) (auto simp: decseq_def)
   4.336 +
   4.337 +lemma incseq_convergent:
   4.338 +  fixes X :: "nat \<Rightarrow> real"
   4.339 +  assumes "incseq X" and "\<forall>i. X i \<le> B"
   4.340 +  obtains L where "X ----> L" "\<forall>i. X i \<le> L"
   4.341 +proof atomize_elim
   4.342 +  from incseq_bounded[OF assms] `incseq X` Bseq_monoseq_convergent[of X]
   4.343 +  obtain L where "X ----> L"
   4.344 +    by (auto simp: convergent_def monoseq_def incseq_def)
   4.345 +  with `incseq X` show "\<exists>L. X ----> L \<and> (\<forall>i. X i \<le> L)"
   4.346 +    by (auto intro!: exI[of _ L] incseq_le)
   4.347 +qed
   4.348 +
   4.349 +lemma decseq_convergent:
   4.350 +  fixes X :: "nat \<Rightarrow> real"
   4.351 +  assumes "decseq X" and "\<forall>i. B \<le> X i"
   4.352 +  obtains L where "X ----> L" "\<forall>i. L \<le> X i"
   4.353 +proof atomize_elim
   4.354 +  from decseq_bounded[OF assms] `decseq X` Bseq_monoseq_convergent[of X]
   4.355 +  obtain L where "X ----> L"
   4.356 +    by (auto simp: convergent_def monoseq_def decseq_def)
   4.357 +  with `decseq X` show "\<exists>L. X ----> L \<and> (\<forall>i. L \<le> X i)"
   4.358 +    by (auto intro!: exI[of _ L] decseq_le)
   4.359 +qed
   4.360 +
   4.361 +subsubsection {* Cauchy Sequences are Bounded *}
   4.362 +
   4.363 +text{*A Cauchy sequence is bounded -- this is the standard
   4.364 +  proof mechanization rather than the nonstandard proof*}
   4.365 +
   4.366 +lemma lemmaCauchy: "\<forall>n \<ge> M. norm (X M - X n) < (1::real)
   4.367 +          ==>  \<forall>n \<ge> M. norm (X n :: 'a::real_normed_vector) < 1 + norm (X M)"
   4.368 +apply (clarify, drule spec, drule (1) mp)
   4.369 +apply (simp only: norm_minus_commute)
   4.370 +apply (drule order_le_less_trans [OF norm_triangle_ineq2])
   4.371 +apply simp
   4.372 +done
   4.373 +
   4.374 +class banach = real_normed_vector + complete_space
   4.375 +
   4.376 +instance real :: banach by default
   4.377 +
   4.378 +subsection {* Power Sequences *}
   4.379 +
   4.380 +text{*The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term
   4.381 +"x<1"}.  Proof will use (NS) Cauchy equivalence for convergence and
   4.382 +  also fact that bounded and monotonic sequence converges.*}
   4.383 +
   4.384 +lemma Bseq_realpow: "[| 0 \<le> (x::real); x \<le> 1 |] ==> Bseq (%n. x ^ n)"
   4.385 +apply (simp add: Bseq_def)
   4.386 +apply (rule_tac x = 1 in exI)
   4.387 +apply (simp add: power_abs)
   4.388 +apply (auto dest: power_mono)
   4.389 +done
   4.390 +
   4.391 +lemma monoseq_realpow: fixes x :: real shows "[| 0 \<le> x; x \<le> 1 |] ==> monoseq (%n. x ^ n)"
   4.392 +apply (clarify intro!: mono_SucI2)
   4.393 +apply (cut_tac n = n and N = "Suc n" and a = x in power_decreasing, auto)
   4.394 +done
   4.395 +
   4.396 +lemma convergent_realpow:
   4.397 +  "[| 0 \<le> (x::real); x \<le> 1 |] ==> convergent (%n. x ^ n)"
   4.398 +by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow)
   4.399 +
   4.400 +lemma LIMSEQ_inverse_realpow_zero: "1 < (x::real) \<Longrightarrow> (\<lambda>n. inverse (x ^ n)) ----> 0"
   4.401 +  by (rule filterlim_compose[OF tendsto_inverse_0 filterlim_realpow_sequentially_gt1]) simp
   4.402 +
   4.403 +lemma LIMSEQ_realpow_zero:
   4.404 +  "\<lbrakk>0 \<le> (x::real); x < 1\<rbrakk> \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0"
   4.405 +proof cases
   4.406 +  assume "0 \<le> x" and "x \<noteq> 0"
   4.407 +  hence x0: "0 < x" by simp
   4.408 +  assume x1: "x < 1"
   4.409 +  from x0 x1 have "1 < inverse x"
   4.410 +    by (rule one_less_inverse)
   4.411 +  hence "(\<lambda>n. inverse (inverse x ^ n)) ----> 0"
   4.412 +    by (rule LIMSEQ_inverse_realpow_zero)
   4.413 +  thus ?thesis by (simp add: power_inverse)
   4.414 +qed (rule LIMSEQ_imp_Suc, simp add: tendsto_const)
   4.415 +
   4.416 +lemma LIMSEQ_power_zero:
   4.417 +  fixes x :: "'a::{real_normed_algebra_1}"
   4.418 +  shows "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0"
   4.419 +apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero])
   4.420 +apply (simp only: tendsto_Zfun_iff, erule Zfun_le)
   4.421 +apply (simp add: power_abs norm_power_ineq)
   4.422 +done
   4.423 +
   4.424 +lemma LIMSEQ_divide_realpow_zero: "1 < x \<Longrightarrow> (\<lambda>n. a / (x ^ n) :: real) ----> 0"
   4.425 +  by (rule tendsto_divide_0 [OF tendsto_const filterlim_realpow_sequentially_gt1]) simp
   4.426 +
   4.427 +text{*Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}*}
   4.428 +
   4.429 +lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. \<bar>c\<bar> ^ n :: real) ----> 0"
   4.430 +  by (rule LIMSEQ_realpow_zero [OF abs_ge_zero])
   4.431 +
   4.432 +lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. c ^ n :: real) ----> 0"
   4.433 +  by (rule LIMSEQ_power_zero) simp
   4.434 +
   4.435 +
   4.436 +subsection {* Limits of Functions *}
   4.437 +
   4.438 +lemma LIM_eq:
   4.439 +  fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
   4.440 +  shows "f -- a --> L =
   4.441 +     (\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)"
   4.442 +by (simp add: LIM_def dist_norm)
   4.443 +
   4.444 +lemma LIM_I:
   4.445 +  fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
   4.446 +  shows "(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)
   4.447 +      ==> f -- a --> L"
   4.448 +by (simp add: LIM_eq)
   4.449 +
   4.450 +lemma LIM_D:
   4.451 +  fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
   4.452 +  shows "[| f -- a --> L; 0<r |]
   4.453 +      ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r"
   4.454 +by (simp add: LIM_eq)
   4.455 +
   4.456 +lemma LIM_offset:
   4.457 +  fixes a :: "'a::real_normed_vector"
   4.458 +  shows "f -- a --> L \<Longrightarrow> (\<lambda>x. f (x + k)) -- a - k --> L"
   4.459 +apply (rule topological_tendstoI)
   4.460 +apply (drule (2) topological_tendstoD)
   4.461 +apply (simp only: eventually_at dist_norm)
   4.462 +apply (clarify, rule_tac x=d in exI, safe)
   4.463 +apply (drule_tac x="x + k" in spec)
   4.464 +apply (simp add: algebra_simps)
   4.465 +done
   4.466 +
   4.467 +lemma LIM_offset_zero:
   4.468 +  fixes a :: "'a::real_normed_vector"
   4.469 +  shows "f -- a --> L \<Longrightarrow> (\<lambda>h. f (a + h)) -- 0 --> L"
   4.470 +by (drule_tac k="a" in LIM_offset, simp add: add_commute)
   4.471 +
   4.472 +lemma LIM_offset_zero_cancel:
   4.473 +  fixes a :: "'a::real_normed_vector"
   4.474 +  shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L"
   4.475 +by (drule_tac k="- a" in LIM_offset, simp)
   4.476 +
   4.477 +lemma LIM_zero:
   4.478 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   4.479 +  shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. f x - l) ---> 0) F"
   4.480 +unfolding tendsto_iff dist_norm by simp
   4.481 +
   4.482 +lemma LIM_zero_cancel:
   4.483 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   4.484 +  shows "((\<lambda>x. f x - l) ---> 0) F \<Longrightarrow> (f ---> l) F"
   4.485 +unfolding tendsto_iff dist_norm by simp
   4.486 +
   4.487 +lemma LIM_zero_iff:
   4.488 +  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   4.489 +  shows "((\<lambda>x. f x - l) ---> 0) F = (f ---> l) F"
   4.490 +unfolding tendsto_iff dist_norm by simp
   4.491 +
   4.492 +lemma LIM_imp_LIM:
   4.493 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   4.494 +  fixes g :: "'a::topological_space \<Rightarrow> 'c::real_normed_vector"
   4.495 +  assumes f: "f -- a --> l"
   4.496 +  assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)"
   4.497 +  shows "g -- a --> m"
   4.498 +  by (rule metric_LIM_imp_LIM [OF f],
   4.499 +    simp add: dist_norm le)
   4.500 +
   4.501 +lemma LIM_equal2:
   4.502 +  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
   4.503 +  assumes 1: "0 < R"
   4.504 +  assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < R\<rbrakk> \<Longrightarrow> f x = g x"
   4.505 +  shows "g -- a --> l \<Longrightarrow> f -- a --> l"
   4.506 +by (rule metric_LIM_equal2 [OF 1 2], simp_all add: dist_norm)
   4.507 +
   4.508 +lemma LIM_compose2:
   4.509 +  fixes a :: "'a::real_normed_vector"
   4.510 +  assumes f: "f -- a --> b"
   4.511 +  assumes g: "g -- b --> c"
   4.512 +  assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> b"
   4.513 +  shows "(\<lambda>x. g (f x)) -- a --> c"
   4.514 +by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]])
   4.515 +
   4.516 +lemma real_LIM_sandwich_zero:
   4.517 +  fixes f g :: "'a::topological_space \<Rightarrow> real"
   4.518 +  assumes f: "f -- a --> 0"
   4.519 +  assumes 1: "\<And>x. x \<noteq> a \<Longrightarrow> 0 \<le> g x"
   4.520 +  assumes 2: "\<And>x. x \<noteq> a \<Longrightarrow> g x \<le> f x"
   4.521 +  shows "g -- a --> 0"
   4.522 +proof (rule LIM_imp_LIM [OF f]) (* FIXME: use tendsto_sandwich *)
   4.523 +  fix x assume x: "x \<noteq> a"
   4.524 +  have "norm (g x - 0) = g x" by (simp add: 1 x)
   4.525 +  also have "g x \<le> f x" by (rule 2 [OF x])
   4.526 +  also have "f x \<le> \<bar>f x\<bar>" by (rule abs_ge_self)
   4.527 +  also have "\<bar>f x\<bar> = norm (f x - 0)" by simp
   4.528 +  finally show "norm (g x - 0) \<le> norm (f x - 0)" .
   4.529 +qed
   4.530 +
   4.531 +
   4.532 +subsection {* Continuity *}
   4.533 +
   4.534 +lemma LIM_isCont_iff:
   4.535 +  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
   4.536 +  shows "(f -- a --> f a) = ((\<lambda>h. f (a + h)) -- 0 --> f a)"
   4.537 +by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel])
   4.538 +
   4.539 +lemma isCont_iff:
   4.540 +  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
   4.541 +  shows "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x"
   4.542 +by (simp add: isCont_def LIM_isCont_iff)
   4.543 +
   4.544 +lemma isCont_LIM_compose2:
   4.545 +  fixes a :: "'a::real_normed_vector"
   4.546 +  assumes f [unfolded isCont_def]: "isCont f a"
   4.547 +  assumes g: "g -- f a --> l"
   4.548 +  assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> f a"
   4.549 +  shows "(\<lambda>x. g (f x)) -- a --> l"
   4.550 +by (rule LIM_compose2 [OF f g inj])
   4.551 +
   4.552 +
   4.553 +lemma isCont_norm [simp]:
   4.554 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   4.555 +  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a"
   4.556 +  by (fact continuous_norm)
   4.557 +
   4.558 +lemma isCont_rabs [simp]:
   4.559 +  fixes f :: "'a::t2_space \<Rightarrow> real"
   4.560 +  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x\<bar>) a"
   4.561 +  by (fact continuous_rabs)
   4.562 +
   4.563 +lemma isCont_add [simp]:
   4.564 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   4.565 +  shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"
   4.566 +  by (fact continuous_add)
   4.567 +
   4.568 +lemma isCont_minus [simp]:
   4.569 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   4.570 +  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a"
   4.571 +  by (fact continuous_minus)
   4.572 +
   4.573 +lemma isCont_diff [simp]:
   4.574 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   4.575 +  shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a"
   4.576 +  by (fact continuous_diff)
   4.577 +
   4.578 +lemma isCont_mult [simp]:
   4.579 +  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_algebra"
   4.580 +  shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x * g x) a"
   4.581 +  by (fact continuous_mult)
   4.582 +
   4.583 +lemma (in bounded_linear) isCont:
   4.584 +  "isCont g a \<Longrightarrow> isCont (\<lambda>x. f (g x)) a"
   4.585 +  by (fact continuous)
   4.586 +
   4.587 +lemma (in bounded_bilinear) isCont:
   4.588 +  "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
   4.589 +  by (fact continuous)
   4.590 +
   4.591 +lemmas isCont_scaleR [simp] = 
   4.592 +  bounded_bilinear.isCont [OF bounded_bilinear_scaleR]
   4.593 +
   4.594 +lemmas isCont_of_real [simp] =
   4.595 +  bounded_linear.isCont [OF bounded_linear_of_real]
   4.596 +
   4.597 +lemma isCont_power [simp]:
   4.598 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::{power,real_normed_algebra}"
   4.599 +  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
   4.600 +  by (fact continuous_power)
   4.601 +
   4.602 +lemma isCont_setsum [simp]:
   4.603 +  fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::real_normed_vector"
   4.604 +  shows "\<forall>i\<in>A. isCont (f i) a \<Longrightarrow> isCont (\<lambda>x. \<Sum>i\<in>A. f i x) a"
   4.605 +  by (auto intro: continuous_setsum)
   4.606 +
   4.607 +lemmas isCont_intros =
   4.608 +  isCont_ident isCont_const isCont_norm isCont_rabs isCont_add isCont_minus
   4.609 +  isCont_diff isCont_mult isCont_inverse isCont_divide isCont_scaleR
   4.610 +  isCont_of_real isCont_power isCont_sgn isCont_setsum
   4.611 +
   4.612 +subsection {* Uniform Continuity *}
   4.613 +
   4.614 +lemma (in bounded_linear) isUCont: "isUCont f"
   4.615 +unfolding isUCont_def dist_norm
   4.616 +proof (intro allI impI)
   4.617 +  fix r::real assume r: "0 < r"
   4.618 +  obtain K where K: "0 < K" and norm_le: "\<And>x. norm (f x) \<le> norm x * K"
   4.619 +    using pos_bounded by fast
   4.620 +  show "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r"
   4.621 +  proof (rule exI, safe)
   4.622 +    from r K show "0 < r / K" by (rule divide_pos_pos)
   4.623 +  next
   4.624 +    fix x y :: 'a
   4.625 +    assume xy: "norm (x - y) < r / K"
   4.626 +    have "norm (f x - f y) = norm (f (x - y))" by (simp only: diff)
   4.627 +    also have "\<dots> \<le> norm (x - y) * K" by (rule norm_le)
   4.628 +    also from K xy have "\<dots> < r" by (simp only: pos_less_divide_eq)
   4.629 +    finally show "norm (f x - f y) < r" .
   4.630 +  qed
   4.631 +qed
   4.632 +
   4.633 +lemma (in bounded_linear) Cauchy: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
   4.634 +by (rule isUCont [THEN isUCont_Cauchy])
   4.635 +
   4.636 +
   4.637 +lemma LIM_less_bound: 
   4.638 +  fixes f :: "real \<Rightarrow> real"
   4.639 +  assumes ev: "b < x" "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and "isCont f x"
   4.640 +  shows "0 \<le> f x"
   4.641 +proof (rule tendsto_le_const)
   4.642 +  show "(f ---> f x) (at_left x)"
   4.643 +    using `isCont f x` by (simp add: filterlim_at_split isCont_def)
   4.644 +  show "eventually (\<lambda>x. 0 \<le> f x) (at_left x)"
   4.645 +    using ev by (auto simp: eventually_within_less dist_real_def intro!: exI[of _ "x - b"])
   4.646 +qed simp
   4.647  
   4.648  end
   4.649  
     5.1 --- a/src/HOL/SEQ.thy	Tue Mar 26 12:20:58 2013 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,415 +0,0 @@
     5.4 -(*  Title:      HOL/SEQ.thy
     5.5 -    Author:     Jacques D. Fleuriot, University of Cambridge
     5.6 -    Author:     Lawrence C Paulson
     5.7 -    Author:     Jeremy Avigad
     5.8 -    Author:     Brian Huffman
     5.9 -
    5.10 -Convergence of sequences and series.
    5.11 -*)
    5.12 -
    5.13 -header {* Sequences and Convergence *}
    5.14 -
    5.15 -theory SEQ
    5.16 -imports Limits
    5.17 -begin
    5.18 -
    5.19 -subsection {* Limits of Sequences *}
    5.20 -
    5.21 -lemma [trans]: "X=Y ==> Y ----> z ==> X ----> z"
    5.22 -  by simp
    5.23 -
    5.24 -lemma LIMSEQ_iff:
    5.25 -  fixes L :: "'a::real_normed_vector"
    5.26 -  shows "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)"
    5.27 -unfolding LIMSEQ_def dist_norm ..
    5.28 -
    5.29 -lemma LIMSEQ_I:
    5.30 -  fixes L :: "'a::real_normed_vector"
    5.31 -  shows "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r) \<Longrightarrow> X ----> L"
    5.32 -by (simp add: LIMSEQ_iff)
    5.33 -
    5.34 -lemma LIMSEQ_D:
    5.35 -  fixes L :: "'a::real_normed_vector"
    5.36 -  shows "\<lbrakk>X ----> L; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r"
    5.37 -by (simp add: LIMSEQ_iff)
    5.38 -
    5.39 -lemma LIMSEQ_linear: "\<lbrakk> X ----> x ; l > 0 \<rbrakk> \<Longrightarrow> (\<lambda> n. X (n * l)) ----> x"
    5.40 -  unfolding tendsto_def eventually_sequentially
    5.41 -  by (metis div_le_dividend div_mult_self1_is_m le_trans nat_mult_commute)
    5.42 -
    5.43 -lemma Bseq_inverse_lemma:
    5.44 -  fixes x :: "'a::real_normed_div_algebra"
    5.45 -  shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r"
    5.46 -apply (subst nonzero_norm_inverse, clarsimp)
    5.47 -apply (erule (1) le_imp_inverse_le)
    5.48 -done
    5.49 -
    5.50 -lemma Bseq_inverse:
    5.51 -  fixes a :: "'a::real_normed_div_algebra"
    5.52 -  shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> Bseq (\<lambda>n. inverse (X n))"
    5.53 -  by (rule Bfun_inverse)
    5.54 -
    5.55 -lemma LIMSEQ_diff_approach_zero:
    5.56 -  fixes L :: "'a::real_normed_vector"
    5.57 -  shows "g ----> L ==> (%x. f x - g x) ----> 0 ==> f ----> L"
    5.58 -  by (drule (1) tendsto_add, simp)
    5.59 -
    5.60 -lemma LIMSEQ_diff_approach_zero2:
    5.61 -  fixes L :: "'a::real_normed_vector"
    5.62 -  shows "f ----> L ==> (%x. f x - g x) ----> 0 ==> g ----> L"
    5.63 -  by (drule (1) tendsto_diff, simp)
    5.64 -
    5.65 -text{*An unbounded sequence's inverse tends to 0*}
    5.66 -
    5.67 -lemma LIMSEQ_inverse_zero:
    5.68 -  "\<forall>r::real. \<exists>N. \<forall>n\<ge>N. r < X n \<Longrightarrow> (\<lambda>n. inverse (X n)) ----> 0"
    5.69 -  apply (rule filterlim_compose[OF tendsto_inverse_0])
    5.70 -  apply (simp add: filterlim_at_infinity[OF order_refl] eventually_sequentially)
    5.71 -  apply (metis abs_le_D1 linorder_le_cases linorder_not_le)
    5.72 -  done
    5.73 -
    5.74 -text{*The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity*}
    5.75 -
    5.76 -lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----> 0"
    5.77 -  by (metis filterlim_compose tendsto_inverse_0 filterlim_mono order_refl filterlim_Suc
    5.78 -            filterlim_compose[OF filterlim_real_sequentially] at_top_le_at_infinity)
    5.79 -
    5.80 -text{*The sequence @{term "r + 1/n"} tends to @{term r} as @{term n} tends to
    5.81 -infinity is now easily proved*}
    5.82 -
    5.83 -lemma LIMSEQ_inverse_real_of_nat_add:
    5.84 -     "(%n. r + inverse(real(Suc n))) ----> r"
    5.85 -  using tendsto_add [OF tendsto_const LIMSEQ_inverse_real_of_nat] by auto
    5.86 -
    5.87 -lemma LIMSEQ_inverse_real_of_nat_add_minus:
    5.88 -     "(%n. r + -inverse(real(Suc n))) ----> r"
    5.89 -  using tendsto_add [OF tendsto_const tendsto_minus [OF LIMSEQ_inverse_real_of_nat]]
    5.90 -  by auto
    5.91 -
    5.92 -lemma LIMSEQ_inverse_real_of_nat_add_minus_mult:
    5.93 -     "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r"
    5.94 -  using tendsto_mult [OF tendsto_const LIMSEQ_inverse_real_of_nat_add_minus [of 1]]
    5.95 -  by auto
    5.96 -
    5.97 -subsection {* Convergence *}
    5.98 -
    5.99 -lemma convergent_add:
   5.100 -  fixes X Y :: "nat \<Rightarrow> 'a::real_normed_vector"
   5.101 -  assumes "convergent (\<lambda>n. X n)"
   5.102 -  assumes "convergent (\<lambda>n. Y n)"
   5.103 -  shows "convergent (\<lambda>n. X n + Y n)"
   5.104 -  using assms unfolding convergent_def by (fast intro: tendsto_add)
   5.105 -
   5.106 -lemma convergent_setsum:
   5.107 -  fixes X :: "'a \<Rightarrow> nat \<Rightarrow> 'b::real_normed_vector"
   5.108 -  assumes "\<And>i. i \<in> A \<Longrightarrow> convergent (\<lambda>n. X i n)"
   5.109 -  shows "convergent (\<lambda>n. \<Sum>i\<in>A. X i n)"
   5.110 -proof (cases "finite A")
   5.111 -  case True from this and assms show ?thesis
   5.112 -    by (induct A set: finite) (simp_all add: convergent_const convergent_add)
   5.113 -qed (simp add: convergent_const)
   5.114 -
   5.115 -lemma (in bounded_linear) convergent:
   5.116 -  assumes "convergent (\<lambda>n. X n)"
   5.117 -  shows "convergent (\<lambda>n. f (X n))"
   5.118 -  using assms unfolding convergent_def by (fast intro: tendsto)
   5.119 -
   5.120 -lemma (in bounded_bilinear) convergent:
   5.121 -  assumes "convergent (\<lambda>n. X n)" and "convergent (\<lambda>n. Y n)"
   5.122 -  shows "convergent (\<lambda>n. X n ** Y n)"
   5.123 -  using assms unfolding convergent_def by (fast intro: tendsto)
   5.124 -
   5.125 -lemma convergent_minus_iff:
   5.126 -  fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
   5.127 -  shows "convergent X \<longleftrightarrow> convergent (\<lambda>n. - X n)"
   5.128 -apply (simp add: convergent_def)
   5.129 -apply (auto dest: tendsto_minus)
   5.130 -apply (drule tendsto_minus, auto)
   5.131 -done
   5.132 -
   5.133 -
   5.134 -subsection {* Bounded Monotonic Sequences *}
   5.135 -
   5.136 -subsubsection {* Bounded Sequences *}
   5.137 -
   5.138 -lemma BseqI': "(\<And>n. norm (X n) \<le> K) \<Longrightarrow> Bseq X"
   5.139 -  by (intro BfunI) (auto simp: eventually_sequentially)
   5.140 -
   5.141 -lemma BseqI2': "\<forall>n\<ge>N. norm (X n) \<le> K \<Longrightarrow> Bseq X"
   5.142 -  by (intro BfunI) (auto simp: eventually_sequentially)
   5.143 -
   5.144 -lemma Bseq_def: "Bseq X \<longleftrightarrow> (\<exists>K>0. \<forall>n. norm (X n) \<le> K)"
   5.145 -  unfolding Bfun_def eventually_sequentially
   5.146 -proof safe
   5.147 -  fix N K assume "0 < K" "\<forall>n\<ge>N. norm (X n) \<le> K"
   5.148 -  then show "\<exists>K>0. \<forall>n. norm (X n) \<le> K"
   5.149 -    by (intro exI[of _ "max (Max (norm ` X ` {..N})) K"] min_max.less_supI2)
   5.150 -       (auto intro!: imageI not_less[where 'a=nat, THEN iffD1] Max_ge simp: le_max_iff_disj)
   5.151 -qed auto
   5.152 -
   5.153 -lemma BseqE: "\<lbrakk>Bseq X; \<And>K. \<lbrakk>0 < K; \<forall>n. norm (X n) \<le> K\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
   5.154 -unfolding Bseq_def by auto
   5.155 -
   5.156 -lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. norm (X n) \<le> K)"
   5.157 -by (simp add: Bseq_def)
   5.158 -
   5.159 -lemma BseqI: "[| 0 < K; \<forall>n. norm (X n) \<le> K |] ==> Bseq X"
   5.160 -by (auto simp add: Bseq_def)
   5.161 -
   5.162 -lemma lemma_NBseq_def:
   5.163 -  "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
   5.164 -proof safe
   5.165 -  fix K :: real
   5.166 -  from reals_Archimedean2 obtain n :: nat where "K < real n" ..
   5.167 -  then have "K \<le> real (Suc n)" by auto
   5.168 -  moreover assume "\<forall>m. norm (X m) \<le> K"
   5.169 -  ultimately have "\<forall>m. norm (X m) \<le> real (Suc n)"
   5.170 -    by (blast intro: order_trans)
   5.171 -  then show "\<exists>N. \<forall>n. norm (X n) \<le> real (Suc N)" ..
   5.172 -qed (force simp add: real_of_nat_Suc)
   5.173 -
   5.174 -text{* alternative definition for Bseq *}
   5.175 -lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
   5.176 -apply (simp add: Bseq_def)
   5.177 -apply (simp (no_asm) add: lemma_NBseq_def)
   5.178 -done
   5.179 -
   5.180 -lemma lemma_NBseq_def2:
   5.181 -     "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))"
   5.182 -apply (subst lemma_NBseq_def, auto)
   5.183 -apply (rule_tac x = "Suc N" in exI)
   5.184 -apply (rule_tac [2] x = N in exI)
   5.185 -apply (auto simp add: real_of_nat_Suc)
   5.186 - prefer 2 apply (blast intro: order_less_imp_le)
   5.187 -apply (drule_tac x = n in spec, simp)
   5.188 -done
   5.189 -
   5.190 -(* yet another definition for Bseq *)
   5.191 -lemma Bseq_iff1a: "Bseq X = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))"
   5.192 -by (simp add: Bseq_def lemma_NBseq_def2)
   5.193 -
   5.194 -subsubsection{*A Few More Equivalence Theorems for Boundedness*}
   5.195 -
   5.196 -text{*alternative formulation for boundedness*}
   5.197 -lemma Bseq_iff2: "Bseq X = (\<exists>k > 0. \<exists>x. \<forall>n. norm (X(n) + -x) \<le> k)"
   5.198 -apply (unfold Bseq_def, safe)
   5.199 -apply (rule_tac [2] x = "k + norm x" in exI)
   5.200 -apply (rule_tac x = K in exI, simp)
   5.201 -apply (rule exI [where x = 0], auto)
   5.202 -apply (erule order_less_le_trans, simp)
   5.203 -apply (drule_tac x=n in spec, fold diff_minus)
   5.204 -apply (drule order_trans [OF norm_triangle_ineq2])
   5.205 -apply simp
   5.206 -done
   5.207 -
   5.208 -text{*alternative formulation for boundedness*}
   5.209 -lemma Bseq_iff3: "Bseq X = (\<exists>k > 0. \<exists>N. \<forall>n. norm(X(n) + -X(N)) \<le> k)"
   5.210 -apply safe
   5.211 -apply (simp add: Bseq_def, safe)
   5.212 -apply (rule_tac x = "K + norm (X N)" in exI)
   5.213 -apply auto
   5.214 -apply (erule order_less_le_trans, simp)
   5.215 -apply (rule_tac x = N in exI, safe)
   5.216 -apply (drule_tac x = n in spec)
   5.217 -apply (rule order_trans [OF norm_triangle_ineq], simp)
   5.218 -apply (auto simp add: Bseq_iff2)
   5.219 -done
   5.220 -
   5.221 -lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> (K::real)) ==> Bseq f"
   5.222 -apply (simp add: Bseq_def)
   5.223 -apply (rule_tac x = " (\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI, auto)
   5.224 -apply (drule_tac x = n in spec, arith)
   5.225 -done
   5.226 -
   5.227 -subsubsection{*Upper Bounds and Lubs of Bounded Sequences*}
   5.228 -
   5.229 -lemma Bseq_isUb:
   5.230 -  "!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U"
   5.231 -by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff)
   5.232 -
   5.233 -text{* Use completeness of reals (supremum property)
   5.234 -   to show that any bounded sequence has a least upper bound*}
   5.235 -
   5.236 -lemma Bseq_isLub:
   5.237 -  "!!(X::nat=>real). Bseq X ==>
   5.238 -   \<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U"
   5.239 -by (blast intro: reals_complete Bseq_isUb)
   5.240 -
   5.241 -subsubsection{*A Bounded and Monotonic Sequence Converges*}
   5.242 -
   5.243 -(* TODO: delete *)
   5.244 -(* FIXME: one use in NSA/HSEQ.thy *)
   5.245 -lemma Bmonoseq_LIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X ----> L)"
   5.246 -  apply (rule_tac x="X m" in exI)
   5.247 -  apply (rule filterlim_cong[THEN iffD2, OF refl refl _ tendsto_const])
   5.248 -  unfolding eventually_sequentially
   5.249 -  apply blast
   5.250 -  done
   5.251 -
   5.252 -text {* A monotone sequence converges to its least upper bound. *}
   5.253 -
   5.254 -lemma isLub_mono_imp_LIMSEQ:
   5.255 -  fixes X :: "nat \<Rightarrow> real"
   5.256 -  assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use 'range X' *)
   5.257 -  assumes X: "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n"
   5.258 -  shows "X ----> u"
   5.259 -proof (rule LIMSEQ_I)
   5.260 -  have 1: "\<forall>n. X n \<le> u"
   5.261 -    using isLubD2 [OF u] by auto
   5.262 -  have "\<forall>y. (\<forall>n. X n \<le> y) \<longrightarrow> u \<le> y"
   5.263 -    using isLub_le_isUb [OF u] by (auto simp add: isUb_def setle_def)
   5.264 -  hence 2: "\<forall>y<u. \<exists>n. y < X n"
   5.265 -    by (metis not_le)
   5.266 -  fix r :: real assume "0 < r"
   5.267 -  hence "u - r < u" by simp
   5.268 -  hence "\<exists>m. u - r < X m" using 2 by simp
   5.269 -  then obtain m where "u - r < X m" ..
   5.270 -  with X have "\<forall>n\<ge>m. u - r < X n"
   5.271 -    by (fast intro: less_le_trans)
   5.272 -  hence "\<exists>m. \<forall>n\<ge>m. u - r < X n" ..
   5.273 -  thus "\<exists>m. \<forall>n\<ge>m. norm (X n - u) < r"
   5.274 -    using 1 by (simp add: diff_less_eq add_commute)
   5.275 -qed
   5.276 -
   5.277 -text{*A standard proof of the theorem for monotone increasing sequence*}
   5.278 -
   5.279 -lemma Bseq_mono_convergent:
   5.280 -   "Bseq X \<Longrightarrow> \<forall>m. \<forall>n \<ge> m. X m \<le> X n \<Longrightarrow> convergent (X::nat=>real)"
   5.281 -  by (metis Bseq_isLub isLub_mono_imp_LIMSEQ convergentI)
   5.282 -
   5.283 -lemma Bseq_minus_iff: "Bseq (%n. -(X n) :: 'a :: real_normed_vector) = Bseq X"
   5.284 -  by (simp add: Bseq_def)
   5.285 -
   5.286 -text{*Main monotonicity theorem*}
   5.287 -
   5.288 -lemma Bseq_monoseq_convergent: "Bseq X \<Longrightarrow> monoseq X \<Longrightarrow> convergent (X::nat\<Rightarrow>real)"
   5.289 -  by (metis monoseq_iff incseq_def decseq_eq_incseq convergent_minus_iff Bseq_minus_iff
   5.290 -            Bseq_mono_convergent)
   5.291 -
   5.292 -lemma Cauchy_iff:
   5.293 -  fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
   5.294 -  shows "Cauchy X \<longleftrightarrow> (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e)"
   5.295 -  unfolding Cauchy_def dist_norm ..
   5.296 -
   5.297 -lemma CauchyI:
   5.298 -  fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
   5.299 -  shows "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e) \<Longrightarrow> Cauchy X"
   5.300 -by (simp add: Cauchy_iff)
   5.301 -
   5.302 -lemma CauchyD:
   5.303 -  fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
   5.304 -  shows "\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e"
   5.305 -by (simp add: Cauchy_iff)
   5.306 -
   5.307 -lemma Bseq_eq_bounded: "range f \<subseteq> {a .. b::real} \<Longrightarrow> Bseq f"
   5.308 -  apply (simp add: subset_eq)
   5.309 -  apply (rule BseqI'[where K="max (norm a) (norm b)"])
   5.310 -  apply (erule_tac x=n in allE)
   5.311 -  apply auto
   5.312 -  done
   5.313 -
   5.314 -lemma incseq_bounded: "incseq X \<Longrightarrow> \<forall>i. X i \<le> (B::real) \<Longrightarrow> Bseq X"
   5.315 -  by (intro Bseq_eq_bounded[of X "X 0" B]) (auto simp: incseq_def)
   5.316 -
   5.317 -lemma decseq_bounded: "decseq X \<Longrightarrow> \<forall>i. (B::real) \<le> X i \<Longrightarrow> Bseq X"
   5.318 -  by (intro Bseq_eq_bounded[of X B "X 0"]) (auto simp: decseq_def)
   5.319 -
   5.320 -lemma incseq_convergent:
   5.321 -  fixes X :: "nat \<Rightarrow> real"
   5.322 -  assumes "incseq X" and "\<forall>i. X i \<le> B"
   5.323 -  obtains L where "X ----> L" "\<forall>i. X i \<le> L"
   5.324 -proof atomize_elim
   5.325 -  from incseq_bounded[OF assms] `incseq X` Bseq_monoseq_convergent[of X]
   5.326 -  obtain L where "X ----> L"
   5.327 -    by (auto simp: convergent_def monoseq_def incseq_def)
   5.328 -  with `incseq X` show "\<exists>L. X ----> L \<and> (\<forall>i. X i \<le> L)"
   5.329 -    by (auto intro!: exI[of _ L] incseq_le)
   5.330 -qed
   5.331 -
   5.332 -lemma decseq_convergent:
   5.333 -  fixes X :: "nat \<Rightarrow> real"
   5.334 -  assumes "decseq X" and "\<forall>i. B \<le> X i"
   5.335 -  obtains L where "X ----> L" "\<forall>i. L \<le> X i"
   5.336 -proof atomize_elim
   5.337 -  from decseq_bounded[OF assms] `decseq X` Bseq_monoseq_convergent[of X]
   5.338 -  obtain L where "X ----> L"
   5.339 -    by (auto simp: convergent_def monoseq_def decseq_def)
   5.340 -  with `decseq X` show "\<exists>L. X ----> L \<and> (\<forall>i. L \<le> X i)"
   5.341 -    by (auto intro!: exI[of _ L] decseq_le)
   5.342 -qed
   5.343 -
   5.344 -subsubsection {* Cauchy Sequences are Bounded *}
   5.345 -
   5.346 -text{*A Cauchy sequence is bounded -- this is the standard
   5.347 -  proof mechanization rather than the nonstandard proof*}
   5.348 -
   5.349 -lemma lemmaCauchy: "\<forall>n \<ge> M. norm (X M - X n) < (1::real)
   5.350 -          ==>  \<forall>n \<ge> M. norm (X n :: 'a::real_normed_vector) < 1 + norm (X M)"
   5.351 -apply (clarify, drule spec, drule (1) mp)
   5.352 -apply (simp only: norm_minus_commute)
   5.353 -apply (drule order_le_less_trans [OF norm_triangle_ineq2])
   5.354 -apply simp
   5.355 -done
   5.356 -
   5.357 -class banach = real_normed_vector + complete_space
   5.358 -
   5.359 -instance real :: banach by default
   5.360 -
   5.361 -subsection {* Power Sequences *}
   5.362 -
   5.363 -text{*The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term
   5.364 -"x<1"}.  Proof will use (NS) Cauchy equivalence for convergence and
   5.365 -  also fact that bounded and monotonic sequence converges.*}
   5.366 -
   5.367 -lemma Bseq_realpow: "[| 0 \<le> (x::real); x \<le> 1 |] ==> Bseq (%n. x ^ n)"
   5.368 -apply (simp add: Bseq_def)
   5.369 -apply (rule_tac x = 1 in exI)
   5.370 -apply (simp add: power_abs)
   5.371 -apply (auto dest: power_mono)
   5.372 -done
   5.373 -
   5.374 -lemma monoseq_realpow: fixes x :: real shows "[| 0 \<le> x; x \<le> 1 |] ==> monoseq (%n. x ^ n)"
   5.375 -apply (clarify intro!: mono_SucI2)
   5.376 -apply (cut_tac n = n and N = "Suc n" and a = x in power_decreasing, auto)
   5.377 -done
   5.378 -
   5.379 -lemma convergent_realpow:
   5.380 -  "[| 0 \<le> (x::real); x \<le> 1 |] ==> convergent (%n. x ^ n)"
   5.381 -by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow)
   5.382 -
   5.383 -lemma LIMSEQ_inverse_realpow_zero: "1 < (x::real) \<Longrightarrow> (\<lambda>n. inverse (x ^ n)) ----> 0"
   5.384 -  by (rule filterlim_compose[OF tendsto_inverse_0 filterlim_realpow_sequentially_gt1]) simp
   5.385 -
   5.386 -lemma LIMSEQ_realpow_zero:
   5.387 -  "\<lbrakk>0 \<le> (x::real); x < 1\<rbrakk> \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0"
   5.388 -proof cases
   5.389 -  assume "0 \<le> x" and "x \<noteq> 0"
   5.390 -  hence x0: "0 < x" by simp
   5.391 -  assume x1: "x < 1"
   5.392 -  from x0 x1 have "1 < inverse x"
   5.393 -    by (rule one_less_inverse)
   5.394 -  hence "(\<lambda>n. inverse (inverse x ^ n)) ----> 0"
   5.395 -    by (rule LIMSEQ_inverse_realpow_zero)
   5.396 -  thus ?thesis by (simp add: power_inverse)
   5.397 -qed (rule LIMSEQ_imp_Suc, simp add: tendsto_const)
   5.398 -
   5.399 -lemma LIMSEQ_power_zero:
   5.400 -  fixes x :: "'a::{real_normed_algebra_1}"
   5.401 -  shows "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0"
   5.402 -apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero])
   5.403 -apply (simp only: tendsto_Zfun_iff, erule Zfun_le)
   5.404 -apply (simp add: power_abs norm_power_ineq)
   5.405 -done
   5.406 -
   5.407 -lemma LIMSEQ_divide_realpow_zero: "1 < x \<Longrightarrow> (\<lambda>n. a / (x ^ n) :: real) ----> 0"
   5.408 -  by (rule tendsto_divide_0 [OF tendsto_const filterlim_realpow_sequentially_gt1]) simp
   5.409 -
   5.410 -text{*Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}*}
   5.411 -
   5.412 -lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. \<bar>c\<bar> ^ n :: real) ----> 0"
   5.413 -  by (rule LIMSEQ_realpow_zero [OF abs_ge_zero])
   5.414 -
   5.415 -lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. c ^ n :: real) ----> 0"
   5.416 -  by (rule LIMSEQ_power_zero) simp
   5.417 -
   5.418 -end
     6.1 --- a/src/HOL/Series.thy	Tue Mar 26 12:20:58 2013 +0100
     6.2 +++ b/src/HOL/Series.thy	Tue Mar 26 12:20:58 2013 +0100
     6.3 @@ -10,7 +10,7 @@
     6.4  header{*Finite Summation and Infinite Series*}
     6.5  
     6.6  theory Series
     6.7 -imports SEQ Deriv
     6.8 +imports Deriv
     6.9  begin
    6.10  
    6.11  definition