src/HOL/Lim.thy
author huffman
Fri Aug 26 08:12:38 2011 -0700 (2011-08-26)
changeset 44532 a2e9b39df938
parent 44314 dbad46932536
child 44568 e6f291cb5810
permissions -rw-r--r--
add lemma sequentially_imp_eventually_within;
rename LIMSEQ_SEQ_conv2_lemma to sequentially_imp_eventually_at;
     1 (*  Title       : Lim.thy
     2     Author      : Jacques D. Fleuriot
     3     Copyright   : 1998  University of Cambridge
     4     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     5 *)
     6 
     7 header{* Limits and Continuity *}
     8 
     9 theory Lim
    10 imports SEQ
    11 begin
    12 
    13 text{*Standard Definitions*}
    14 
    15 abbreviation
    16   LIM :: "['a::topological_space \<Rightarrow> 'b::topological_space, 'a, 'b] \<Rightarrow> bool"
    17         ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where
    18   "f -- a --> L \<equiv> (f ---> L) (at a)"
    19 
    20 definition
    21   isCont :: "['a::topological_space \<Rightarrow> 'b::topological_space, 'a] \<Rightarrow> bool" where
    22   "isCont f a = (f -- a --> (f a))"
    23 
    24 definition
    25   isUCont :: "['a::metric_space \<Rightarrow> 'b::metric_space] \<Rightarrow> bool" where
    26   "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. dist x y < s \<longrightarrow> dist (f x) (f y) < r)"
    27 
    28 subsection {* Limits of Functions *}
    29 
    30 lemma LIM_def: "f -- a --> L =
    31      (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & dist x a < s
    32         --> dist (f x) L < r)"
    33 unfolding tendsto_iff eventually_at ..
    34 
    35 lemma metric_LIM_I:
    36   "(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r)
    37     \<Longrightarrow> f -- a --> L"
    38 by (simp add: LIM_def)
    39 
    40 lemma metric_LIM_D:
    41   "\<lbrakk>f -- a --> L; 0 < r\<rbrakk>
    42     \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r"
    43 by (simp add: LIM_def)
    44 
    45 lemma LIM_eq:
    46   fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
    47   shows "f -- a --> L =
    48      (\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)"
    49 by (simp add: LIM_def dist_norm)
    50 
    51 lemma LIM_I:
    52   fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
    53   shows "(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)
    54       ==> f -- a --> L"
    55 by (simp add: LIM_eq)
    56 
    57 lemma LIM_D:
    58   fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
    59   shows "[| f -- a --> L; 0<r |]
    60       ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r"
    61 by (simp add: LIM_eq)
    62 
    63 lemma LIM_offset:
    64   fixes a :: "'a::real_normed_vector"
    65   shows "f -- a --> L \<Longrightarrow> (\<lambda>x. f (x + k)) -- a - k --> L"
    66 apply (rule topological_tendstoI)
    67 apply (drule (2) topological_tendstoD)
    68 apply (simp only: eventually_at dist_norm)
    69 apply (clarify, rule_tac x=d in exI, safe)
    70 apply (drule_tac x="x + k" in spec)
    71 apply (simp add: algebra_simps)
    72 done
    73 
    74 lemma LIM_offset_zero:
    75   fixes a :: "'a::real_normed_vector"
    76   shows "f -- a --> L \<Longrightarrow> (\<lambda>h. f (a + h)) -- 0 --> L"
    77 by (drule_tac k="a" in LIM_offset, simp add: add_commute)
    78 
    79 lemma LIM_offset_zero_cancel:
    80   fixes a :: "'a::real_normed_vector"
    81   shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L"
    82 by (drule_tac k="- a" in LIM_offset, simp)
    83 
    84 lemma LIM_cong_limit: "\<lbrakk> f -- x --> L ; K = L \<rbrakk> \<Longrightarrow> f -- x --> K" by simp
    85 
    86 lemma LIM_zero:
    87   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    88   shows "f -- a --> l \<Longrightarrow> (\<lambda>x. f x - l) -- a --> 0"
    89 unfolding tendsto_iff dist_norm by simp
    90 
    91 lemma LIM_zero_cancel:
    92   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    93   shows "(\<lambda>x. f x - l) -- a --> 0 \<Longrightarrow> f -- a --> l"
    94 unfolding tendsto_iff dist_norm by simp
    95 
    96 lemma LIM_zero_iff:
    97   fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
    98   shows "(\<lambda>x. f x - l) -- a --> 0 = f -- a --> l"
    99 unfolding tendsto_iff dist_norm by simp
   100 
   101 lemma metric_LIM_imp_LIM:
   102   assumes f: "f -- a --> l"
   103   assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> dist (g x) m \<le> dist (f x) l"
   104   shows "g -- a --> m"
   105   by (rule metric_tendsto_imp_tendsto [OF f],
   106     auto simp add: eventually_at_topological le)
   107 
   108 lemma LIM_imp_LIM:
   109   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   110   fixes g :: "'a::topological_space \<Rightarrow> 'c::real_normed_vector"
   111   assumes f: "f -- a --> l"
   112   assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)"
   113   shows "g -- a --> m"
   114   by (rule metric_LIM_imp_LIM [OF f],
   115     simp add: dist_norm le)
   116 
   117 lemma trivial_limit_at:
   118   fixes a :: "'a::real_normed_algebra_1"
   119   shows "\<not> trivial_limit (at a)"  -- {* TODO: find a more appropriate class *}
   120 unfolding trivial_limit_def
   121 unfolding eventually_at dist_norm
   122 by (clarsimp, rule_tac x="a + of_real (d/2)" in exI, simp)
   123 
   124 lemma LIM_const_not_eq:
   125   fixes a :: "'a::real_normed_algebra_1"
   126   fixes k L :: "'b::t2_space"
   127   shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --> L"
   128 by (simp add: tendsto_const_iff trivial_limit_at)
   129 
   130 lemmas LIM_not_zero = LIM_const_not_eq [where L = 0]
   131 
   132 lemma LIM_const_eq:
   133   fixes a :: "'a::real_normed_algebra_1"
   134   fixes k L :: "'b::t2_space"
   135   shows "(\<lambda>x. k) -- a --> L \<Longrightarrow> k = L"
   136   by (simp add: tendsto_const_iff trivial_limit_at)
   137 
   138 lemma LIM_unique:
   139   fixes a :: "'a::real_normed_algebra_1" -- {* TODO: find a more appropriate class *}
   140   fixes L M :: "'b::t2_space"
   141   shows "\<lbrakk>f -- a --> L; f -- a --> M\<rbrakk> \<Longrightarrow> L = M"
   142   using trivial_limit_at by (rule tendsto_unique)
   143 
   144 text{*Limits are equal for functions equal except at limit point*}
   145 lemma LIM_equal:
   146      "[| \<forall>x. x \<noteq> a --> (f x = g x) |] ==> (f -- a --> l) = (g -- a --> l)"
   147 unfolding tendsto_def eventually_at_topological by simp
   148 
   149 lemma LIM_cong:
   150   "\<lbrakk>a = b; \<And>x. x \<noteq> b \<Longrightarrow> f x = g x; l = m\<rbrakk>
   151    \<Longrightarrow> ((\<lambda>x. f x) -- a --> l) = ((\<lambda>x. g x) -- b --> m)"
   152 by (simp add: LIM_equal)
   153 
   154 lemma metric_LIM_equal2:
   155   assumes 1: "0 < R"
   156   assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < R\<rbrakk> \<Longrightarrow> f x = g x"
   157   shows "g -- a --> l \<Longrightarrow> f -- a --> l"
   158 apply (rule topological_tendstoI)
   159 apply (drule (2) topological_tendstoD)
   160 apply (simp add: eventually_at, safe)
   161 apply (rule_tac x="min d R" in exI, safe)
   162 apply (simp add: 1)
   163 apply (simp add: 2)
   164 done
   165 
   166 lemma LIM_equal2:
   167   fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
   168   assumes 1: "0 < R"
   169   assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < R\<rbrakk> \<Longrightarrow> f x = g x"
   170   shows "g -- a --> l \<Longrightarrow> f -- a --> l"
   171 by (rule metric_LIM_equal2 [OF 1 2], simp_all add: dist_norm)
   172 
   173 lemma LIM_compose_eventually:
   174   assumes f: "f -- a --> b"
   175   assumes g: "g -- b --> c"
   176   assumes inj: "eventually (\<lambda>x. f x \<noteq> b) (at a)"
   177   shows "(\<lambda>x. g (f x)) -- a --> c"
   178   using g f inj by (rule tendsto_compose_eventually)
   179 
   180 lemma metric_LIM_compose2:
   181   assumes f: "f -- a --> b"
   182   assumes g: "g -- b --> c"
   183   assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> b"
   184   shows "(\<lambda>x. g (f x)) -- a --> c"
   185   using g f inj [folded eventually_at]
   186   by (rule tendsto_compose_eventually)
   187 
   188 lemma LIM_compose2:
   189   fixes a :: "'a::real_normed_vector"
   190   assumes f: "f -- a --> b"
   191   assumes g: "g -- b --> c"
   192   assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> b"
   193   shows "(\<lambda>x. g (f x)) -- a --> c"
   194 by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]])
   195 
   196 lemma LIM_o: "\<lbrakk>g -- l --> g l; f -- a --> l\<rbrakk> \<Longrightarrow> (g \<circ> f) -- a --> g l"
   197   unfolding o_def by (rule tendsto_compose)
   198 
   199 lemma real_LIM_sandwich_zero:
   200   fixes f g :: "'a::topological_space \<Rightarrow> real"
   201   assumes f: "f -- a --> 0"
   202   assumes 1: "\<And>x. x \<noteq> a \<Longrightarrow> 0 \<le> g x"
   203   assumes 2: "\<And>x. x \<noteq> a \<Longrightarrow> g x \<le> f x"
   204   shows "g -- a --> 0"
   205 proof (rule LIM_imp_LIM [OF f])
   206   fix x assume x: "x \<noteq> a"
   207   have "norm (g x - 0) = g x" by (simp add: 1 x)
   208   also have "g x \<le> f x" by (rule 2 [OF x])
   209   also have "f x \<le> \<bar>f x\<bar>" by (rule abs_ge_self)
   210   also have "\<bar>f x\<bar> = norm (f x - 0)" by simp
   211   finally show "norm (g x - 0) \<le> norm (f x - 0)" .
   212 qed
   213 
   214 text {* Bounded Linear Operators *}
   215 
   216 lemma (in bounded_linear) LIM:
   217   "g -- a --> l \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> f l"
   218 by (rule tendsto)
   219 
   220 lemma (in bounded_linear) LIM_zero:
   221   "g -- a --> 0 \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> 0"
   222   by (rule tendsto_zero)
   223 
   224 text {* Bounded Bilinear Operators *}
   225 
   226 lemma (in bounded_bilinear) LIM:
   227   "\<lbrakk>f -- a --> L; g -- a --> M\<rbrakk> \<Longrightarrow> (\<lambda>x. f x ** g x) -- a --> L ** M"
   228 by (rule tendsto)
   229 
   230 lemma (in bounded_bilinear) LIM_prod_zero:
   231   fixes a :: "'d::metric_space"
   232   assumes f: "f -- a --> 0"
   233   assumes g: "g -- a --> 0"
   234   shows "(\<lambda>x. f x ** g x) -- a --> 0"
   235   using f g by (rule tendsto_zero)
   236 
   237 lemma (in bounded_bilinear) LIM_left_zero:
   238   "f -- a --> 0 \<Longrightarrow> (\<lambda>x. f x ** c) -- a --> 0"
   239   by (rule tendsto_left_zero)
   240 
   241 lemma (in bounded_bilinear) LIM_right_zero:
   242   "f -- a --> 0 \<Longrightarrow> (\<lambda>x. c ** f x) -- a --> 0"
   243   by (rule tendsto_right_zero)
   244 
   245 lemmas LIM_mult_zero =
   246   bounded_bilinear.LIM_prod_zero [OF bounded_bilinear_mult]
   247 
   248 lemmas LIM_mult_left_zero =
   249   bounded_bilinear.LIM_left_zero [OF bounded_bilinear_mult]
   250 
   251 lemmas LIM_mult_right_zero =
   252   bounded_bilinear.LIM_right_zero [OF bounded_bilinear_mult]
   253 
   254 lemma LIM_inverse_fun:
   255   assumes a: "a \<noteq> (0::'a::real_normed_div_algebra)"
   256   shows "inverse -- a --> inverse a"
   257   by (rule tendsto_inverse [OF tendsto_ident_at a])
   258 
   259 
   260 subsection {* Continuity *}
   261 
   262 lemma LIM_isCont_iff:
   263   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
   264   shows "(f -- a --> f a) = ((\<lambda>h. f (a + h)) -- 0 --> f a)"
   265 by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel])
   266 
   267 lemma isCont_iff:
   268   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
   269   shows "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x"
   270 by (simp add: isCont_def LIM_isCont_iff)
   271 
   272 lemma isCont_ident [simp]: "isCont (\<lambda>x. x) a"
   273   unfolding isCont_def by (rule tendsto_ident_at)
   274 
   275 lemma isCont_const [simp]: "isCont (\<lambda>x. k) a"
   276   unfolding isCont_def by (rule tendsto_const)
   277 
   278 lemma isCont_norm [simp]:
   279   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   280   shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a"
   281   unfolding isCont_def by (rule tendsto_norm)
   282 
   283 lemma isCont_rabs [simp]:
   284   fixes f :: "'a::topological_space \<Rightarrow> real"
   285   shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x\<bar>) a"
   286   unfolding isCont_def by (rule tendsto_rabs)
   287 
   288 lemma isCont_add [simp]:
   289   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   290   shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"
   291   unfolding isCont_def by (rule tendsto_add)
   292 
   293 lemma isCont_minus [simp]:
   294   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   295   shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a"
   296   unfolding isCont_def by (rule tendsto_minus)
   297 
   298 lemma isCont_diff [simp]:
   299   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   300   shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a"
   301   unfolding isCont_def by (rule tendsto_diff)
   302 
   303 lemma isCont_mult [simp]:
   304   fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra"
   305   shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x * g x) a"
   306   unfolding isCont_def by (rule tendsto_mult)
   307 
   308 lemma isCont_inverse [simp]:
   309   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra"
   310   shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. inverse (f x)) a"
   311   unfolding isCont_def by (rule tendsto_inverse)
   312 
   313 lemma isCont_divide [simp]:
   314   fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_field"
   315   shows "\<lbrakk>isCont f a; isCont g a; g a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x / g x) a"
   316   unfolding isCont_def by (rule tendsto_divide)
   317 
   318 lemma isCont_tendsto_compose:
   319   "\<lbrakk>isCont g l; (f ---> l) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. g (f x)) ---> g l) F"
   320   unfolding isCont_def by (rule tendsto_compose)
   321 
   322 lemma metric_isCont_LIM_compose2:
   323   assumes f [unfolded isCont_def]: "isCont f a"
   324   assumes g: "g -- f a --> l"
   325   assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> f a"
   326   shows "(\<lambda>x. g (f x)) -- a --> l"
   327 by (rule metric_LIM_compose2 [OF f g inj])
   328 
   329 lemma isCont_LIM_compose2:
   330   fixes a :: "'a::real_normed_vector"
   331   assumes f [unfolded isCont_def]: "isCont f a"
   332   assumes g: "g -- f a --> l"
   333   assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> f a"
   334   shows "(\<lambda>x. g (f x)) -- a --> l"
   335 by (rule LIM_compose2 [OF f g inj])
   336 
   337 lemma isCont_o2: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. g (f x)) a"
   338   unfolding isCont_def by (rule tendsto_compose)
   339 
   340 lemma isCont_o: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (g o f) a"
   341   unfolding o_def by (rule isCont_o2)
   342 
   343 lemma (in bounded_linear) isCont:
   344   "isCont g a \<Longrightarrow> isCont (\<lambda>x. f (g x)) a"
   345   unfolding isCont_def by (rule tendsto)
   346 
   347 lemma (in bounded_bilinear) isCont:
   348   "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
   349   unfolding isCont_def by (rule tendsto)
   350 
   351 lemmas isCont_scaleR [simp] =
   352   bounded_bilinear.isCont [OF bounded_bilinear_scaleR]
   353 
   354 lemmas isCont_of_real [simp] =
   355   bounded_linear.isCont [OF bounded_linear_of_real]
   356 
   357 lemma isCont_power [simp]:
   358   fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}"
   359   shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
   360   unfolding isCont_def by (rule tendsto_power)
   361 
   362 lemma isCont_sgn [simp]:
   363   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   364   shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. sgn (f x)) a"
   365   unfolding isCont_def by (rule tendsto_sgn)
   366 
   367 lemma isCont_setsum [simp]:
   368   fixes f :: "'a \<Rightarrow> 'b::topological_space \<Rightarrow> 'c::real_normed_vector"
   369   fixes A :: "'a set"
   370   shows "\<forall>i\<in>A. isCont (f i) a \<Longrightarrow> isCont (\<lambda>x. \<Sum>i\<in>A. f i x) a"
   371   unfolding isCont_def by (simp add: tendsto_setsum)
   372 
   373 lemmas isCont_intros =
   374   isCont_ident isCont_const isCont_norm isCont_rabs isCont_add isCont_minus
   375   isCont_diff isCont_mult isCont_inverse isCont_divide isCont_scaleR
   376   isCont_of_real isCont_power isCont_sgn isCont_setsum
   377 
   378 lemma LIM_less_bound: fixes f :: "real \<Rightarrow> real" assumes "b < x"
   379   and all_le: "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and isCont: "isCont f x"
   380   shows "0 \<le> f x"
   381 proof (rule ccontr)
   382   assume "\<not> 0 \<le> f x" hence "f x < 0" by auto
   383   hence "0 < - f x / 2" by auto
   384   from isCont[unfolded isCont_def, THEN LIM_D, OF this]
   385   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
   386 
   387   let ?x = "x - min (s / 2) ((x - b) / 2)"
   388   have "?x < x" and "\<bar> ?x - x \<bar> < s"
   389     using `b < x` and `0 < s` by auto
   390   have "b < ?x"
   391   proof (cases "s < x - b")
   392     case True thus ?thesis using `0 < s` by auto
   393   next
   394     case False hence "s / 2 \<ge> (x - b) / 2" by auto
   395     hence "?x = (x + b) / 2" by (simp add: field_simps min_max.inf_absorb2)
   396     thus ?thesis using `b < x` by auto
   397   qed
   398   hence "0 \<le> f ?x" using all_le `?x < x` by auto
   399   moreover have "\<bar>f ?x - f x\<bar> < - f x / 2"
   400     using s_D[OF _ `\<bar> ?x - x \<bar> < s`] `?x < x` by auto
   401   hence "f ?x - f x < - f x / 2" by auto
   402   hence "f ?x < f x / 2" by auto
   403   hence "f ?x < 0" using `f x < 0` by auto
   404   thus False using `0 \<le> f ?x` by auto
   405 qed
   406 
   407 
   408 subsection {* Uniform Continuity *}
   409 
   410 lemma isUCont_isCont: "isUCont f ==> isCont f x"
   411 by (simp add: isUCont_def isCont_def LIM_def, force)
   412 
   413 lemma isUCont_Cauchy:
   414   "\<lbrakk>isUCont f; Cauchy X\<rbrakk> \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
   415 unfolding isUCont_def
   416 apply (rule metric_CauchyI)
   417 apply (drule_tac x=e in spec, safe)
   418 apply (drule_tac e=s in metric_CauchyD, safe)
   419 apply (rule_tac x=M in exI, simp)
   420 done
   421 
   422 lemma (in bounded_linear) isUCont: "isUCont f"
   423 unfolding isUCont_def dist_norm
   424 proof (intro allI impI)
   425   fix r::real assume r: "0 < r"
   426   obtain K where K: "0 < K" and norm_le: "\<And>x. norm (f x) \<le> norm x * K"
   427     using pos_bounded by fast
   428   show "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r"
   429   proof (rule exI, safe)
   430     from r K show "0 < r / K" by (rule divide_pos_pos)
   431   next
   432     fix x y :: 'a
   433     assume xy: "norm (x - y) < r / K"
   434     have "norm (f x - f y) = norm (f (x - y))" by (simp only: diff)
   435     also have "\<dots> \<le> norm (x - y) * K" by (rule norm_le)
   436     also from K xy have "\<dots> < r" by (simp only: pos_less_divide_eq)
   437     finally show "norm (f x - f y) < r" .
   438   qed
   439 qed
   440 
   441 lemma (in bounded_linear) Cauchy: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
   442 by (rule isUCont [THEN isUCont_Cauchy])
   443 
   444 
   445 subsection {* Relation of LIM and LIMSEQ *}
   446 
   447 lemma sequentially_imp_eventually_within:
   448   fixes a :: "'a::metric_space"
   449   assumes "\<forall>f. (\<forall>n. f n \<in> s \<and> f n \<noteq> a) \<and> f ----> a \<longrightarrow>
   450     eventually (\<lambda>n. P (f n)) sequentially"
   451   shows "eventually P (at a within s)"
   452 proof (rule ccontr)
   453   let ?I = "\<lambda>n. inverse (real (Suc n))"
   454   def F \<equiv> "\<lambda>n::nat. SOME x. x \<in> s \<and> x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x"
   455   assume "\<not> eventually P (at a within s)"
   456   hence P: "\<forall>d>0. \<exists>x. x \<in> s \<and> x \<noteq> a \<and> dist x a < d \<and> \<not> P x"
   457     unfolding Limits.eventually_within Limits.eventually_at by fast
   458   hence "\<And>n. \<exists>x. x \<in> s \<and> x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x" by simp
   459   hence F: "\<And>n. F n \<in> s \<and> F n \<noteq> a \<and> dist (F n) a < ?I n \<and> \<not> P (F n)"
   460     unfolding F_def by (rule someI_ex)
   461   hence F0: "\<forall>n. F n \<in> s" and F1: "\<forall>n. F n \<noteq> a"
   462     and F2: "\<forall>n. dist (F n) a < ?I n" and F3: "\<forall>n. \<not> P (F n)"
   463     by fast+
   464   from LIMSEQ_inverse_real_of_nat have "F ----> a"
   465     by (rule metric_tendsto_imp_tendsto,
   466       simp add: dist_norm F2 less_imp_le)
   467   hence "eventually (\<lambda>n. P (F n)) sequentially"
   468     using assms F0 F1 by simp
   469   thus "False" by (simp add: F3)
   470 qed
   471 
   472 lemma sequentially_imp_eventually_at:
   473   fixes a :: "'a::metric_space"
   474   assumes "\<forall>f. (\<forall>n. f n \<noteq> a) \<and> f ----> a \<longrightarrow>
   475     eventually (\<lambda>n. P (f n)) sequentially"
   476   shows "eventually P (at a)"
   477   using assms sequentially_imp_eventually_within [where s=UNIV]
   478   unfolding within_UNIV by simp
   479 
   480 lemma LIMSEQ_SEQ_conv1:
   481   fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
   482   assumes f: "f -- a --> l"
   483   shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"
   484   using tendsto_compose_eventually [OF f, where F=sequentially] by simp
   485 
   486 lemma LIMSEQ_SEQ_conv2:
   487   fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
   488   assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"
   489   shows "f -- a --> l"
   490   using assms unfolding tendsto_def [where l=l]
   491   by (simp add: sequentially_imp_eventually_at)
   492 
   493 lemma LIMSEQ_SEQ_conv:
   494   "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::'a::metric_space) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) =
   495    (X -- a --> (L::'b::topological_space))"
   496   using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 ..
   497 
   498 subsection {* Legacy theorem names *}
   499 
   500 lemmas LIM_ident [simp] = tendsto_ident_at
   501 lemmas LIM_const [simp] = tendsto_const [where F="at x", standard]
   502 lemmas LIM_add = tendsto_add [where F="at x", standard]
   503 lemmas LIM_add_zero = tendsto_add_zero [where F="at x", standard]
   504 lemmas LIM_minus = tendsto_minus [where F="at x", standard]
   505 lemmas LIM_diff = tendsto_diff [where F="at x", standard]
   506 lemmas LIM_norm = tendsto_norm [where F="at x", standard]
   507 lemmas LIM_norm_zero = tendsto_norm_zero [where F="at x", standard]
   508 lemmas LIM_norm_zero_cancel = tendsto_norm_zero_cancel [where F="at x", standard]
   509 lemmas LIM_norm_zero_iff = tendsto_norm_zero_iff [where F="at x", standard]
   510 lemmas LIM_rabs = tendsto_rabs [where F="at x", standard]
   511 lemmas LIM_rabs_zero = tendsto_rabs_zero [where F="at x", standard]
   512 lemmas LIM_rabs_zero_cancel = tendsto_rabs_zero_cancel [where F="at x", standard]
   513 lemmas LIM_rabs_zero_iff = tendsto_rabs_zero_iff [where F="at x", standard]
   514 lemmas LIM_compose = tendsto_compose [where F="at x", standard]
   515 lemmas LIM_mult = tendsto_mult [where F="at x", standard]
   516 lemmas LIM_scaleR = tendsto_scaleR [where F="at x", standard]
   517 lemmas LIM_of_real = tendsto_of_real [where F="at x", standard]
   518 lemmas LIM_power = tendsto_power [where F="at x", standard]
   519 lemmas LIM_inverse = tendsto_inverse [where F="at x", standard]
   520 lemmas LIM_sgn = tendsto_sgn [where F="at x", standard]
   521 lemmas isCont_LIM_compose = isCont_tendsto_compose [where F="at x", standard]
   522 
   523 end