src/HOL/Limits.thy
changeset 51531 f415febf4234
parent 51529 2d2f59e6055a
child 51641 cd05e9fcc63d
     1.1 --- a/src/HOL/Limits.thy	Tue Mar 26 12:21:00 2013 +0100
     1.2 +++ b/src/HOL/Limits.thy	Tue Mar 26 12:21:01 2013 +0100
     1.3 @@ -57,7 +57,21 @@
     1.4    "at_bot \<le> (at_infinity :: real filter)"
     1.5    unfolding at_infinity_eq_at_top_bot by simp
     1.6  
     1.7 -subsection {* Boundedness *}
     1.8 +subsubsection {* Boundedness *}
     1.9 +
    1.10 +definition Bfun :: "('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'a filter \<Rightarrow> bool" where
    1.11 +  Bfun_metric_def: "Bfun f F = (\<exists>y. \<exists>K>0. eventually (\<lambda>x. dist (f x) y \<le> K) F)"
    1.12 +
    1.13 +abbreviation Bseq :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where
    1.14 +  "Bseq X \<equiv> Bfun X sequentially"
    1.15 +
    1.16 +lemma Bseq_conv_Bfun: "Bseq X \<longleftrightarrow> Bfun X sequentially" ..
    1.17 +
    1.18 +lemma Bseq_ignore_initial_segment: "Bseq X \<Longrightarrow> Bseq (\<lambda>n. X (n + k))"
    1.19 +  unfolding Bfun_metric_def by (subst eventually_sequentially_seg)
    1.20 +
    1.21 +lemma Bseq_offset: "Bseq (\<lambda>n. X (n + k)) \<Longrightarrow> Bseq X"
    1.22 +  unfolding Bfun_metric_def by (subst (asm) eventually_sequentially_seg)
    1.23  
    1.24  lemma Bfun_def:
    1.25    "Bfun f F \<longleftrightarrow> (\<exists>K>0. eventually (\<lambda>x. norm (f x) \<le> K) F)"
    1.26 @@ -87,6 +101,154 @@
    1.27    obtains B where "0 < B" and "eventually (\<lambda>x. norm (f x) \<le> B) F"
    1.28  using assms unfolding Bfun_def by fast
    1.29  
    1.30 +lemma Cauchy_Bseq: "Cauchy X \<Longrightarrow> Bseq X"
    1.31 +  unfolding Cauchy_def Bfun_metric_def eventually_sequentially
    1.32 +  apply (erule_tac x=1 in allE)
    1.33 +  apply simp
    1.34 +  apply safe
    1.35 +  apply (rule_tac x="X M" in exI)
    1.36 +  apply (rule_tac x=1 in exI)
    1.37 +  apply (erule_tac x=M in allE)
    1.38 +  apply simp
    1.39 +  apply (rule_tac x=M in exI)
    1.40 +  apply (auto simp: dist_commute)
    1.41 +  done
    1.42 +
    1.43 +
    1.44 +subsubsection {* Bounded Sequences *}
    1.45 +
    1.46 +lemma BseqI': "(\<And>n. norm (X n) \<le> K) \<Longrightarrow> Bseq X"
    1.47 +  by (intro BfunI) (auto simp: eventually_sequentially)
    1.48 +
    1.49 +lemma BseqI2': "\<forall>n\<ge>N. norm (X n) \<le> K \<Longrightarrow> Bseq X"
    1.50 +  by (intro BfunI) (auto simp: eventually_sequentially)
    1.51 +
    1.52 +lemma Bseq_def: "Bseq X \<longleftrightarrow> (\<exists>K>0. \<forall>n. norm (X n) \<le> K)"
    1.53 +  unfolding Bfun_def eventually_sequentially
    1.54 +proof safe
    1.55 +  fix N K assume "0 < K" "\<forall>n\<ge>N. norm (X n) \<le> K"
    1.56 +  then show "\<exists>K>0. \<forall>n. norm (X n) \<le> K"
    1.57 +    by (intro exI[of _ "max (Max (norm ` X ` {..N})) K"] min_max.less_supI2)
    1.58 +       (auto intro!: imageI not_less[where 'a=nat, THEN iffD1] Max_ge simp: le_max_iff_disj)
    1.59 +qed auto
    1.60 +
    1.61 +lemma BseqE: "\<lbrakk>Bseq X; \<And>K. \<lbrakk>0 < K; \<forall>n. norm (X n) \<le> K\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
    1.62 +unfolding Bseq_def by auto
    1.63 +
    1.64 +lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. norm (X n) \<le> K)"
    1.65 +by (simp add: Bseq_def)
    1.66 +
    1.67 +lemma BseqI: "[| 0 < K; \<forall>n. norm (X n) \<le> K |] ==> Bseq X"
    1.68 +by (auto simp add: Bseq_def)
    1.69 +
    1.70 +lemma lemma_NBseq_def:
    1.71 +  "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
    1.72 +proof safe
    1.73 +  fix K :: real
    1.74 +  from reals_Archimedean2 obtain n :: nat where "K < real n" ..
    1.75 +  then have "K \<le> real (Suc n)" by auto
    1.76 +  moreover assume "\<forall>m. norm (X m) \<le> K"
    1.77 +  ultimately have "\<forall>m. norm (X m) \<le> real (Suc n)"
    1.78 +    by (blast intro: order_trans)
    1.79 +  then show "\<exists>N. \<forall>n. norm (X n) \<le> real (Suc N)" ..
    1.80 +qed (force simp add: real_of_nat_Suc)
    1.81 +
    1.82 +text{* alternative definition for Bseq *}
    1.83 +lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
    1.84 +apply (simp add: Bseq_def)
    1.85 +apply (simp (no_asm) add: lemma_NBseq_def)
    1.86 +done
    1.87 +
    1.88 +lemma lemma_NBseq_def2:
    1.89 +     "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))"
    1.90 +apply (subst lemma_NBseq_def, auto)
    1.91 +apply (rule_tac x = "Suc N" in exI)
    1.92 +apply (rule_tac [2] x = N in exI)
    1.93 +apply (auto simp add: real_of_nat_Suc)
    1.94 + prefer 2 apply (blast intro: order_less_imp_le)
    1.95 +apply (drule_tac x = n in spec, simp)
    1.96 +done
    1.97 +
    1.98 +(* yet another definition for Bseq *)
    1.99 +lemma Bseq_iff1a: "Bseq X = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))"
   1.100 +by (simp add: Bseq_def lemma_NBseq_def2)
   1.101 +
   1.102 +subsubsection{*A Few More Equivalence Theorems for Boundedness*}
   1.103 +
   1.104 +text{*alternative formulation for boundedness*}
   1.105 +lemma Bseq_iff2: "Bseq X = (\<exists>k > 0. \<exists>x. \<forall>n. norm (X(n) + -x) \<le> k)"
   1.106 +apply (unfold Bseq_def, safe)
   1.107 +apply (rule_tac [2] x = "k + norm x" in exI)
   1.108 +apply (rule_tac x = K in exI, simp)
   1.109 +apply (rule exI [where x = 0], auto)
   1.110 +apply (erule order_less_le_trans, simp)
   1.111 +apply (drule_tac x=n in spec, fold diff_minus)
   1.112 +apply (drule order_trans [OF norm_triangle_ineq2])
   1.113 +apply simp
   1.114 +done
   1.115 +
   1.116 +text{*alternative formulation for boundedness*}
   1.117 +lemma Bseq_iff3: "Bseq X = (\<exists>k > 0. \<exists>N. \<forall>n. norm(X(n) + -X(N)) \<le> k)"
   1.118 +apply safe
   1.119 +apply (simp add: Bseq_def, safe)
   1.120 +apply (rule_tac x = "K + norm (X N)" in exI)
   1.121 +apply auto
   1.122 +apply (erule order_less_le_trans, simp)
   1.123 +apply (rule_tac x = N in exI, safe)
   1.124 +apply (drule_tac x = n in spec)
   1.125 +apply (rule order_trans [OF norm_triangle_ineq], simp)
   1.126 +apply (auto simp add: Bseq_iff2)
   1.127 +done
   1.128 +
   1.129 +lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> (K::real)) ==> Bseq f"
   1.130 +apply (simp add: Bseq_def)
   1.131 +apply (rule_tac x = " (\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI, auto)
   1.132 +apply (drule_tac x = n in spec, arith)
   1.133 +done
   1.134 +
   1.135 +subsubsection{*Upper Bounds and Lubs of Bounded Sequences*}
   1.136 +
   1.137 +lemma Bseq_isUb:
   1.138 +  "!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U"
   1.139 +by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff)
   1.140 +
   1.141 +text{* Use completeness of reals (supremum property)
   1.142 +   to show that any bounded sequence has a least upper bound*}
   1.143 +
   1.144 +lemma Bseq_isLub:
   1.145 +  "!!(X::nat=>real). Bseq X ==>
   1.146 +   \<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U"
   1.147 +by (blast intro: reals_complete Bseq_isUb)
   1.148 +
   1.149 +lemma Bseq_minus_iff: "Bseq (%n. -(X n) :: 'a :: real_normed_vector) = Bseq X"
   1.150 +  by (simp add: Bseq_def)
   1.151 +
   1.152 +lemma Bseq_eq_bounded: "range f \<subseteq> {a .. b::real} \<Longrightarrow> Bseq f"
   1.153 +  apply (simp add: subset_eq)
   1.154 +  apply (rule BseqI'[where K="max (norm a) (norm b)"])
   1.155 +  apply (erule_tac x=n in allE)
   1.156 +  apply auto
   1.157 +  done
   1.158 +
   1.159 +lemma incseq_bounded: "incseq X \<Longrightarrow> \<forall>i. X i \<le> (B::real) \<Longrightarrow> Bseq X"
   1.160 +  by (intro Bseq_eq_bounded[of X "X 0" B]) (auto simp: incseq_def)
   1.161 +
   1.162 +lemma decseq_bounded: "decseq X \<Longrightarrow> \<forall>i. (B::real) \<le> X i \<Longrightarrow> Bseq X"
   1.163 +  by (intro Bseq_eq_bounded[of X B "X 0"]) (auto simp: decseq_def)
   1.164 +
   1.165 +subsection {* Bounded Monotonic Sequences *}
   1.166 +
   1.167 +subsubsection{*A Bounded and Monotonic Sequence Converges*}
   1.168 +
   1.169 +(* TODO: delete *)
   1.170 +(* FIXME: one use in NSA/HSEQ.thy *)
   1.171 +lemma Bmonoseq_LIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X ----> L)"
   1.172 +  apply (rule_tac x="X m" in exI)
   1.173 +  apply (rule filterlim_cong[THEN iffD2, OF refl refl _ tendsto_const])
   1.174 +  unfolding eventually_sequentially
   1.175 +  apply blast
   1.176 +  done
   1.177 +
   1.178  subsection {* Convergence to Zero *}
   1.179  
   1.180  definition Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool"
   1.181 @@ -242,6 +404,37 @@
   1.182  
   1.183  subsubsection {* Distance and norms *}
   1.184  
   1.185 +lemma tendsto_dist [tendsto_intros]:
   1.186 +  fixes l m :: "'a :: metric_space"
   1.187 +  assumes f: "(f ---> l) F" and g: "(g ---> m) F"
   1.188 +  shows "((\<lambda>x. dist (f x) (g x)) ---> dist l m) F"
   1.189 +proof (rule tendstoI)
   1.190 +  fix e :: real assume "0 < e"
   1.191 +  hence e2: "0 < e/2" by simp
   1.192 +  from tendstoD [OF f e2] tendstoD [OF g e2]
   1.193 +  show "eventually (\<lambda>x. dist (dist (f x) (g x)) (dist l m) < e) F"
   1.194 +  proof (eventually_elim)
   1.195 +    case (elim x)
   1.196 +    then show "dist (dist (f x) (g x)) (dist l m) < e"
   1.197 +      unfolding dist_real_def
   1.198 +      using dist_triangle2 [of "f x" "g x" "l"]
   1.199 +      using dist_triangle2 [of "g x" "l" "m"]
   1.200 +      using dist_triangle3 [of "l" "m" "f x"]
   1.201 +      using dist_triangle [of "f x" "m" "g x"]
   1.202 +      by arith
   1.203 +  qed
   1.204 +qed
   1.205 +
   1.206 +lemma continuous_dist[continuous_intros]:
   1.207 +  fixes f g :: "_ \<Rightarrow> 'a :: metric_space"
   1.208 +  shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. dist (f x) (g x))"
   1.209 +  unfolding continuous_def by (rule tendsto_dist)
   1.210 +
   1.211 +lemma continuous_on_dist[continuous_on_intros]:
   1.212 +  fixes f g :: "_ \<Rightarrow> 'a :: metric_space"
   1.213 +  shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. dist (f x) (g x))"
   1.214 +  unfolding continuous_on_def by (auto intro: tendsto_dist)
   1.215 +
   1.216  lemma tendsto_norm [tendsto_intros]:
   1.217    "(f ---> a) F \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> norm a) F"
   1.218    unfolding norm_conv_dist by (intro tendsto_intros)
   1.219 @@ -1152,123 +1345,6 @@
   1.220  apply (drule tendsto_minus, auto)
   1.221  done
   1.222  
   1.223 -subsection {* Bounded Monotonic Sequences *}
   1.224 -
   1.225 -subsubsection {* Bounded Sequences *}
   1.226 -
   1.227 -lemma BseqI': "(\<And>n. norm (X n) \<le> K) \<Longrightarrow> Bseq X"
   1.228 -  by (intro BfunI) (auto simp: eventually_sequentially)
   1.229 -
   1.230 -lemma BseqI2': "\<forall>n\<ge>N. norm (X n) \<le> K \<Longrightarrow> Bseq X"
   1.231 -  by (intro BfunI) (auto simp: eventually_sequentially)
   1.232 -
   1.233 -lemma Bseq_def: "Bseq X \<longleftrightarrow> (\<exists>K>0. \<forall>n. norm (X n) \<le> K)"
   1.234 -  unfolding Bfun_def eventually_sequentially
   1.235 -proof safe
   1.236 -  fix N K assume "0 < K" "\<forall>n\<ge>N. norm (X n) \<le> K"
   1.237 -  then show "\<exists>K>0. \<forall>n. norm (X n) \<le> K"
   1.238 -    by (intro exI[of _ "max (Max (norm ` X ` {..N})) K"] min_max.less_supI2)
   1.239 -       (auto intro!: imageI not_less[where 'a=nat, THEN iffD1] Max_ge simp: le_max_iff_disj)
   1.240 -qed auto
   1.241 -
   1.242 -lemma BseqE: "\<lbrakk>Bseq X; \<And>K. \<lbrakk>0 < K; \<forall>n. norm (X n) \<le> K\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
   1.243 -unfolding Bseq_def by auto
   1.244 -
   1.245 -lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. norm (X n) \<le> K)"
   1.246 -by (simp add: Bseq_def)
   1.247 -
   1.248 -lemma BseqI: "[| 0 < K; \<forall>n. norm (X n) \<le> K |] ==> Bseq X"
   1.249 -by (auto simp add: Bseq_def)
   1.250 -
   1.251 -lemma lemma_NBseq_def:
   1.252 -  "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
   1.253 -proof safe
   1.254 -  fix K :: real
   1.255 -  from reals_Archimedean2 obtain n :: nat where "K < real n" ..
   1.256 -  then have "K \<le> real (Suc n)" by auto
   1.257 -  moreover assume "\<forall>m. norm (X m) \<le> K"
   1.258 -  ultimately have "\<forall>m. norm (X m) \<le> real (Suc n)"
   1.259 -    by (blast intro: order_trans)
   1.260 -  then show "\<exists>N. \<forall>n. norm (X n) \<le> real (Suc N)" ..
   1.261 -qed (force simp add: real_of_nat_Suc)
   1.262 -
   1.263 -text{* alternative definition for Bseq *}
   1.264 -lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
   1.265 -apply (simp add: Bseq_def)
   1.266 -apply (simp (no_asm) add: lemma_NBseq_def)
   1.267 -done
   1.268 -
   1.269 -lemma lemma_NBseq_def2:
   1.270 -     "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))"
   1.271 -apply (subst lemma_NBseq_def, auto)
   1.272 -apply (rule_tac x = "Suc N" in exI)
   1.273 -apply (rule_tac [2] x = N in exI)
   1.274 -apply (auto simp add: real_of_nat_Suc)
   1.275 - prefer 2 apply (blast intro: order_less_imp_le)
   1.276 -apply (drule_tac x = n in spec, simp)
   1.277 -done
   1.278 -
   1.279 -(* yet another definition for Bseq *)
   1.280 -lemma Bseq_iff1a: "Bseq X = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))"
   1.281 -by (simp add: Bseq_def lemma_NBseq_def2)
   1.282 -
   1.283 -subsubsection{*A Few More Equivalence Theorems for Boundedness*}
   1.284 -
   1.285 -text{*alternative formulation for boundedness*}
   1.286 -lemma Bseq_iff2: "Bseq X = (\<exists>k > 0. \<exists>x. \<forall>n. norm (X(n) + -x) \<le> k)"
   1.287 -apply (unfold Bseq_def, safe)
   1.288 -apply (rule_tac [2] x = "k + norm x" in exI)
   1.289 -apply (rule_tac x = K in exI, simp)
   1.290 -apply (rule exI [where x = 0], auto)
   1.291 -apply (erule order_less_le_trans, simp)
   1.292 -apply (drule_tac x=n in spec, fold diff_minus)
   1.293 -apply (drule order_trans [OF norm_triangle_ineq2])
   1.294 -apply simp
   1.295 -done
   1.296 -
   1.297 -text{*alternative formulation for boundedness*}
   1.298 -lemma Bseq_iff3: "Bseq X = (\<exists>k > 0. \<exists>N. \<forall>n. norm(X(n) + -X(N)) \<le> k)"
   1.299 -apply safe
   1.300 -apply (simp add: Bseq_def, safe)
   1.301 -apply (rule_tac x = "K + norm (X N)" in exI)
   1.302 -apply auto
   1.303 -apply (erule order_less_le_trans, simp)
   1.304 -apply (rule_tac x = N in exI, safe)
   1.305 -apply (drule_tac x = n in spec)
   1.306 -apply (rule order_trans [OF norm_triangle_ineq], simp)
   1.307 -apply (auto simp add: Bseq_iff2)
   1.308 -done
   1.309 -
   1.310 -lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> (K::real)) ==> Bseq f"
   1.311 -apply (simp add: Bseq_def)
   1.312 -apply (rule_tac x = " (\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI, auto)
   1.313 -apply (drule_tac x = n in spec, arith)
   1.314 -done
   1.315 -
   1.316 -subsubsection{*Upper Bounds and Lubs of Bounded Sequences*}
   1.317 -
   1.318 -lemma Bseq_isUb:
   1.319 -  "!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U"
   1.320 -by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff)
   1.321 -
   1.322 -text{* Use completeness of reals (supremum property)
   1.323 -   to show that any bounded sequence has a least upper bound*}
   1.324 -
   1.325 -lemma Bseq_isLub:
   1.326 -  "!!(X::nat=>real). Bseq X ==>
   1.327 -   \<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U"
   1.328 -by (blast intro: reals_complete Bseq_isUb)
   1.329 -
   1.330 -subsubsection{*A Bounded and Monotonic Sequence Converges*}
   1.331 -
   1.332 -(* TODO: delete *)
   1.333 -(* FIXME: one use in NSA/HSEQ.thy *)
   1.334 -lemma Bmonoseq_LIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X ----> L)"
   1.335 -  apply (rule_tac x="X m" in exI)
   1.336 -  apply (rule filterlim_cong[THEN iffD2, OF refl refl _ tendsto_const])
   1.337 -  unfolding eventually_sequentially
   1.338 -  apply blast
   1.339 -  done
   1.340  
   1.341  text {* A monotone sequence converges to its least upper bound. *}
   1.342  
   1.343 @@ -1301,9 +1377,6 @@
   1.344     "Bseq X \<Longrightarrow> \<forall>m. \<forall>n \<ge> m. X m \<le> X n \<Longrightarrow> convergent (X::nat=>real)"
   1.345    by (metis Bseq_isLub isLub_mono_imp_LIMSEQ convergentI)
   1.346  
   1.347 -lemma Bseq_minus_iff: "Bseq (%n. -(X n) :: 'a :: real_normed_vector) = Bseq X"
   1.348 -  by (simp add: Bseq_def)
   1.349 -
   1.350  text{*Main monotonicity theorem*}
   1.351  
   1.352  lemma Bseq_monoseq_convergent: "Bseq X \<Longrightarrow> monoseq X \<Longrightarrow> convergent (X::nat\<Rightarrow>real)"
   1.353 @@ -1325,19 +1398,6 @@
   1.354    shows "\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e"
   1.355  by (simp add: Cauchy_iff)
   1.356  
   1.357 -lemma Bseq_eq_bounded: "range f \<subseteq> {a .. b::real} \<Longrightarrow> Bseq f"
   1.358 -  apply (simp add: subset_eq)
   1.359 -  apply (rule BseqI'[where K="max (norm a) (norm b)"])
   1.360 -  apply (erule_tac x=n in allE)
   1.361 -  apply auto
   1.362 -  done
   1.363 -
   1.364 -lemma incseq_bounded: "incseq X \<Longrightarrow> \<forall>i. X i \<le> (B::real) \<Longrightarrow> Bseq X"
   1.365 -  by (intro Bseq_eq_bounded[of X "X 0" B]) (auto simp: incseq_def)
   1.366 -
   1.367 -lemma decseq_bounded: "decseq X \<Longrightarrow> \<forall>i. (B::real) \<le> X i \<Longrightarrow> Bseq X"
   1.368 -  by (intro Bseq_eq_bounded[of X B "X 0"]) (auto simp: decseq_def)
   1.369 -
   1.370  lemma incseq_convergent:
   1.371    fixes X :: "nat \<Rightarrow> real"
   1.372    assumes "incseq X" and "\<forall>i. X i \<le> B"
   1.373 @@ -1375,10 +1435,6 @@
   1.374  apply simp
   1.375  done
   1.376  
   1.377 -class banach = real_normed_vector + complete_space
   1.378 -
   1.379 -instance real :: banach by default
   1.380 -
   1.381  subsection {* Power Sequences *}
   1.382  
   1.383  text{*The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term
   1.384 @@ -1615,6 +1671,22 @@
   1.385  
   1.386  subsection {* Uniform Continuity *}
   1.387  
   1.388 +definition
   1.389 +  isUCont :: "['a::metric_space \<Rightarrow> 'b::metric_space] \<Rightarrow> bool" where
   1.390 +  "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. dist x y < s \<longrightarrow> dist (f x) (f y) < r)"
   1.391 +
   1.392 +lemma isUCont_isCont: "isUCont f ==> isCont f x"
   1.393 +by (simp add: isUCont_def isCont_def LIM_def, force)
   1.394 +
   1.395 +lemma isUCont_Cauchy:
   1.396 +  "\<lbrakk>isUCont f; Cauchy X\<rbrakk> \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
   1.397 +unfolding isUCont_def
   1.398 +apply (rule metric_CauchyI)
   1.399 +apply (drule_tac x=e in spec, safe)
   1.400 +apply (drule_tac e=s in metric_CauchyD, safe)
   1.401 +apply (rule_tac x=M in exI, simp)
   1.402 +done
   1.403 +
   1.404  lemma (in bounded_linear) isUCont: "isUCont f"
   1.405  unfolding isUCont_def dist_norm
   1.406  proof (intro allI impI)
   1.407 @@ -1637,7 +1709,6 @@
   1.408  lemma (in bounded_linear) Cauchy: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
   1.409  by (rule isUCont [THEN isUCont_Cauchy])
   1.410  
   1.411 -
   1.412  lemma LIM_less_bound: 
   1.413    fixes f :: "real \<Rightarrow> real"
   1.414    assumes ev: "b < x" "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and "isCont f x"
   1.415 @@ -1878,5 +1949,6 @@
   1.416    fixes f :: "real \<Rightarrow> real"
   1.417    shows "f -- c --> l \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> \<exists>r. 0 < r \<and> (\<forall>x. x \<noteq> c \<and> \<bar>c - x\<bar> < r \<longrightarrow> f x \<noteq> 0)"
   1.418    using LIM_fun_gt_zero[of f l c] LIM_fun_less_zero[of f l c] by (auto simp add: neq_iff)
   1.419 +
   1.420  end
   1.421