src/HOL/Lim.thy
author huffman
Fri Aug 19 14:17:28 2011 -0700 (2011-08-19)
changeset 44311 42c5cbf68052
parent 44310 ba3d031b5dbb
child 44312 471ff02a8574
permissions -rw-r--r--
Transcendental.thy: add tendsto_intros lemmas;
new isCont theorems;
simplify some proofs.
     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_const [simp]: "(%x. k) -- x --> k"
    85 by (rule tendsto_const)
    86 
    87 lemma LIM_cong_limit: "\<lbrakk> f -- x --> L ; K = L \<rbrakk> \<Longrightarrow> f -- x --> K" by simp
    88 
    89 lemma LIM_add:
    90   fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    91   assumes f: "f -- a --> L" and g: "g -- a --> M"
    92   shows "(\<lambda>x. f x + g x) -- a --> (L + M)"
    93 using assms by (rule tendsto_add)
    94 
    95 lemma LIM_add_zero:
    96   fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    97   shows "\<lbrakk>f -- a --> 0; g -- a --> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. f x + g x) -- a --> 0"
    98   by (rule tendsto_add_zero)
    99 
   100 lemma LIM_minus:
   101   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   102   shows "f -- a --> L \<Longrightarrow> (\<lambda>x. - f x) -- a --> - L"
   103 by (rule tendsto_minus)
   104 
   105 (* TODO: delete *)
   106 lemma LIM_add_minus:
   107   fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   108   shows "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + -g(x)) -- x --> (l + -m)"
   109 by (intro LIM_add LIM_minus)
   110 
   111 lemma LIM_diff:
   112   fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   113   shows "\<lbrakk>f -- x --> l; g -- x --> m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x - g x) -- x --> l - m"
   114 by (rule tendsto_diff)
   115 
   116 lemma LIM_zero:
   117   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   118   shows "f -- a --> l \<Longrightarrow> (\<lambda>x. f x - l) -- a --> 0"
   119 unfolding tendsto_iff dist_norm by simp
   120 
   121 lemma LIM_zero_cancel:
   122   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   123   shows "(\<lambda>x. f x - l) -- a --> 0 \<Longrightarrow> f -- a --> l"
   124 unfolding tendsto_iff dist_norm by simp
   125 
   126 lemma LIM_zero_iff:
   127   fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   128   shows "(\<lambda>x. f x - l) -- a --> 0 = f -- a --> l"
   129 unfolding tendsto_iff dist_norm by simp
   130 
   131 lemma metric_LIM_imp_LIM:
   132   assumes f: "f -- a --> l"
   133   assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> dist (g x) m \<le> dist (f x) l"
   134   shows "g -- a --> m"
   135   by (rule metric_tendsto_imp_tendsto [OF f],
   136     auto simp add: eventually_at_topological le)
   137 
   138 lemma LIM_imp_LIM:
   139   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   140   fixes g :: "'a::topological_space \<Rightarrow> 'c::real_normed_vector"
   141   assumes f: "f -- a --> l"
   142   assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)"
   143   shows "g -- a --> m"
   144   by (rule metric_LIM_imp_LIM [OF f],
   145     simp add: dist_norm le)
   146 
   147 lemma LIM_norm:
   148   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   149   shows "f -- a --> l \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> norm l"
   150 by (rule tendsto_norm)
   151 
   152 lemma LIM_norm_zero:
   153   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   154   shows "f -- a --> 0 \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> 0"
   155 by (rule tendsto_norm_zero)
   156 
   157 lemma LIM_norm_zero_cancel:
   158   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   159   shows "(\<lambda>x. norm (f x)) -- a --> 0 \<Longrightarrow> f -- a --> 0"
   160 by (rule tendsto_norm_zero_cancel)
   161 
   162 lemma LIM_norm_zero_iff:
   163   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   164   shows "(\<lambda>x. norm (f x)) -- a --> 0 = f -- a --> 0"
   165 by (rule tendsto_norm_zero_iff)
   166 
   167 lemma LIM_rabs: "f -- a --> (l::real) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>) -- a --> \<bar>l\<bar>"
   168   by (rule tendsto_rabs)
   169 
   170 lemma LIM_rabs_zero: "f -- a --> (0::real) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>) -- a --> 0"
   171   by (rule tendsto_rabs_zero)
   172 
   173 lemma LIM_rabs_zero_cancel: "(\<lambda>x. \<bar>f x\<bar>) -- a --> (0::real) \<Longrightarrow> f -- a --> 0"
   174   by (rule tendsto_rabs_zero_cancel)
   175 
   176 lemma LIM_rabs_zero_iff: "(\<lambda>x. \<bar>f x\<bar>) -- a --> (0::real) = f -- a --> 0"
   177   by (rule tendsto_rabs_zero_iff)
   178 
   179 lemma trivial_limit_at:
   180   fixes a :: "'a::real_normed_algebra_1"
   181   shows "\<not> trivial_limit (at a)"  -- {* TODO: find a more appropriate class *}
   182 unfolding trivial_limit_def
   183 unfolding eventually_at dist_norm
   184 by (clarsimp, rule_tac x="a + of_real (d/2)" in exI, simp)
   185 
   186 lemma LIM_const_not_eq:
   187   fixes a :: "'a::real_normed_algebra_1"
   188   fixes k L :: "'b::t2_space"
   189   shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --> L"
   190 by (simp add: tendsto_const_iff trivial_limit_at)
   191 
   192 lemmas LIM_not_zero = LIM_const_not_eq [where L = 0]
   193 
   194 lemma LIM_const_eq:
   195   fixes a :: "'a::real_normed_algebra_1"
   196   fixes k L :: "'b::t2_space"
   197   shows "(\<lambda>x. k) -- a --> L \<Longrightarrow> k = L"
   198   by (simp add: tendsto_const_iff trivial_limit_at)
   199 
   200 lemma LIM_unique:
   201   fixes a :: "'a::real_normed_algebra_1" -- {* TODO: find a more appropriate class *}
   202   fixes L M :: "'b::t2_space"
   203   shows "\<lbrakk>f -- a --> L; f -- a --> M\<rbrakk> \<Longrightarrow> L = M"
   204   using trivial_limit_at by (rule tendsto_unique)
   205 
   206 lemma LIM_ident [simp]: "(\<lambda>x. x) -- a --> a"
   207 by (rule tendsto_ident_at)
   208 
   209 text{*Limits are equal for functions equal except at limit point*}
   210 lemma LIM_equal:
   211      "[| \<forall>x. x \<noteq> a --> (f x = g x) |] ==> (f -- a --> l) = (g -- a --> l)"
   212 unfolding tendsto_def eventually_at_topological by simp
   213 
   214 lemma LIM_cong:
   215   "\<lbrakk>a = b; \<And>x. x \<noteq> b \<Longrightarrow> f x = g x; l = m\<rbrakk>
   216    \<Longrightarrow> ((\<lambda>x. f x) -- a --> l) = ((\<lambda>x. g x) -- b --> m)"
   217 by (simp add: LIM_equal)
   218 
   219 lemma metric_LIM_equal2:
   220   assumes 1: "0 < R"
   221   assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < R\<rbrakk> \<Longrightarrow> f x = g x"
   222   shows "g -- a --> l \<Longrightarrow> f -- a --> l"
   223 apply (rule topological_tendstoI)
   224 apply (drule (2) topological_tendstoD)
   225 apply (simp add: eventually_at, safe)
   226 apply (rule_tac x="min d R" in exI, safe)
   227 apply (simp add: 1)
   228 apply (simp add: 2)
   229 done
   230 
   231 lemma LIM_equal2:
   232   fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
   233   assumes 1: "0 < R"
   234   assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < R\<rbrakk> \<Longrightarrow> f x = g x"
   235   shows "g -- a --> l \<Longrightarrow> f -- a --> l"
   236 by (rule metric_LIM_equal2 [OF 1 2], simp_all add: dist_norm)
   237 
   238 text{*Two uses in Transcendental.ML*} (* BH: no longer true; delete? *)
   239 lemma LIM_trans:
   240   fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   241   shows "[| (%x. f(x) + -g(x)) -- a --> 0;  g -- a --> l |] ==> f -- a --> l"
   242 apply (drule LIM_add, assumption)
   243 apply (auto simp add: add_assoc)
   244 done
   245 
   246 lemma LIM_compose:
   247   assumes g: "g -- l --> g l"
   248   assumes f: "f -- a --> l"
   249   shows "(\<lambda>x. g (f x)) -- a --> g l"
   250   using assms by (rule tendsto_compose)
   251 
   252 lemma LIM_compose_eventually:
   253   assumes f: "f -- a --> b"
   254   assumes g: "g -- b --> c"
   255   assumes inj: "eventually (\<lambda>x. f x \<noteq> b) (at a)"
   256   shows "(\<lambda>x. g (f x)) -- a --> c"
   257   using g f inj by (rule tendsto_compose_eventually)
   258 
   259 lemma metric_LIM_compose2:
   260   assumes f: "f -- a --> b"
   261   assumes g: "g -- b --> c"
   262   assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> b"
   263   shows "(\<lambda>x. g (f x)) -- a --> c"
   264 using f g inj [folded eventually_at]
   265 by (rule LIM_compose_eventually)
   266 
   267 lemma LIM_compose2:
   268   fixes a :: "'a::real_normed_vector"
   269   assumes f: "f -- a --> b"
   270   assumes g: "g -- b --> c"
   271   assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> b"
   272   shows "(\<lambda>x. g (f x)) -- a --> c"
   273 by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]])
   274 
   275 lemma LIM_o: "\<lbrakk>g -- l --> g l; f -- a --> l\<rbrakk> \<Longrightarrow> (g \<circ> f) -- a --> g l"
   276 unfolding o_def by (rule LIM_compose)
   277 
   278 lemma real_LIM_sandwich_zero:
   279   fixes f g :: "'a::topological_space \<Rightarrow> real"
   280   assumes f: "f -- a --> 0"
   281   assumes 1: "\<And>x. x \<noteq> a \<Longrightarrow> 0 \<le> g x"
   282   assumes 2: "\<And>x. x \<noteq> a \<Longrightarrow> g x \<le> f x"
   283   shows "g -- a --> 0"
   284 proof (rule LIM_imp_LIM [OF f])
   285   fix x assume x: "x \<noteq> a"
   286   have "norm (g x - 0) = g x" by (simp add: 1 x)
   287   also have "g x \<le> f x" by (rule 2 [OF x])
   288   also have "f x \<le> \<bar>f x\<bar>" by (rule abs_ge_self)
   289   also have "\<bar>f x\<bar> = norm (f x - 0)" by simp
   290   finally show "norm (g x - 0) \<le> norm (f x - 0)" .
   291 qed
   292 
   293 text {* Bounded Linear Operators *}
   294 
   295 lemma (in bounded_linear) LIM:
   296   "g -- a --> l \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> f l"
   297 by (rule tendsto)
   298 
   299 lemma (in bounded_linear) LIM_zero:
   300   "g -- a --> 0 \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> 0"
   301   by (rule tendsto_zero)
   302 
   303 text {* Bounded Bilinear Operators *}
   304 
   305 lemma (in bounded_bilinear) LIM:
   306   "\<lbrakk>f -- a --> L; g -- a --> M\<rbrakk> \<Longrightarrow> (\<lambda>x. f x ** g x) -- a --> L ** M"
   307 by (rule tendsto)
   308 
   309 lemma (in bounded_bilinear) LIM_prod_zero:
   310   fixes a :: "'d::metric_space"
   311   assumes f: "f -- a --> 0"
   312   assumes g: "g -- a --> 0"
   313   shows "(\<lambda>x. f x ** g x) -- a --> 0"
   314   using f g by (rule tendsto_zero)
   315 
   316 lemma (in bounded_bilinear) LIM_left_zero:
   317   "f -- a --> 0 \<Longrightarrow> (\<lambda>x. f x ** c) -- a --> 0"
   318   by (rule tendsto_left_zero)
   319 
   320 lemma (in bounded_bilinear) LIM_right_zero:
   321   "f -- a --> 0 \<Longrightarrow> (\<lambda>x. c ** f x) -- a --> 0"
   322   by (rule tendsto_right_zero)
   323 
   324 lemmas LIM_mult =
   325   bounded_bilinear.LIM [OF bounded_bilinear_mult]
   326 
   327 lemmas LIM_mult_zero =
   328   bounded_bilinear.LIM_prod_zero [OF bounded_bilinear_mult]
   329 
   330 lemmas LIM_mult_left_zero =
   331   bounded_bilinear.LIM_left_zero [OF bounded_bilinear_mult]
   332 
   333 lemmas LIM_mult_right_zero =
   334   bounded_bilinear.LIM_right_zero [OF bounded_bilinear_mult]
   335 
   336 lemmas LIM_scaleR =
   337   bounded_bilinear.LIM [OF bounded_bilinear_scaleR]
   338 
   339 lemmas LIM_of_real =
   340   bounded_linear.LIM [OF bounded_linear_of_real]
   341 
   342 lemma LIM_power:
   343   fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}"
   344   assumes f: "f -- a --> l"
   345   shows "(\<lambda>x. f x ^ n) -- a --> l ^ n"
   346   using assms by (rule tendsto_power)
   347 
   348 lemma LIM_inverse:
   349   fixes L :: "'a::real_normed_div_algebra"
   350   shows "\<lbrakk>f -- a --> L; L \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. inverse (f x)) -- a --> inverse L"
   351 by (rule tendsto_inverse)
   352 
   353 lemma LIM_inverse_fun:
   354   assumes a: "a \<noteq> (0::'a::real_normed_div_algebra)"
   355   shows "inverse -- a --> inverse a"
   356 by (rule LIM_inverse [OF LIM_ident a])
   357 
   358 lemma LIM_sgn:
   359   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   360   shows "\<lbrakk>f -- a --> l; l \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. sgn (f x)) -- a --> sgn l"
   361   by (rule tendsto_sgn)
   362 
   363 
   364 subsection {* Continuity *}
   365 
   366 lemma LIM_isCont_iff:
   367   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
   368   shows "(f -- a --> f a) = ((\<lambda>h. f (a + h)) -- 0 --> f a)"
   369 by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel])
   370 
   371 lemma isCont_iff:
   372   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
   373   shows "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x"
   374 by (simp add: isCont_def LIM_isCont_iff)
   375 
   376 lemma isCont_ident [simp]: "isCont (\<lambda>x. x) a"
   377   unfolding isCont_def by (rule LIM_ident)
   378 
   379 lemma isCont_const [simp]: "isCont (\<lambda>x. k) a"
   380   unfolding isCont_def by (rule LIM_const)
   381 
   382 lemma isCont_norm [simp]:
   383   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   384   shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a"
   385   unfolding isCont_def by (rule LIM_norm)
   386 
   387 lemma isCont_rabs [simp]:
   388   fixes f :: "'a::topological_space \<Rightarrow> real"
   389   shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x\<bar>) a"
   390   unfolding isCont_def by (rule LIM_rabs)
   391 
   392 lemma isCont_add [simp]:
   393   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   394   shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"
   395   unfolding isCont_def by (rule LIM_add)
   396 
   397 lemma isCont_minus [simp]:
   398   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   399   shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a"
   400   unfolding isCont_def by (rule LIM_minus)
   401 
   402 lemma isCont_diff [simp]:
   403   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   404   shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a"
   405   unfolding isCont_def by (rule LIM_diff)
   406 
   407 lemma isCont_mult [simp]:
   408   fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra"
   409   shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x * g x) a"
   410   unfolding isCont_def by (rule LIM_mult)
   411 
   412 lemma isCont_inverse [simp]:
   413   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra"
   414   shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. inverse (f x)) a"
   415   unfolding isCont_def by (rule LIM_inverse)
   416 
   417 lemma isCont_divide [simp]:
   418   fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_field"
   419   shows "\<lbrakk>isCont f a; isCont g a; g a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x / g x) a"
   420   unfolding isCont_def by (rule tendsto_divide)
   421 
   422 lemma isCont_tendsto_compose:
   423   "\<lbrakk>isCont g l; (f ---> l) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. g (f x)) ---> g l) F"
   424   unfolding isCont_def by (rule tendsto_compose)
   425 
   426 lemma isCont_LIM_compose:
   427   "\<lbrakk>isCont g l; f -- a --> l\<rbrakk> \<Longrightarrow> (\<lambda>x. g (f x)) -- a --> g l"
   428   by (rule isCont_tendsto_compose) (* TODO: delete? *)
   429 
   430 lemma metric_isCont_LIM_compose2:
   431   assumes f [unfolded isCont_def]: "isCont f a"
   432   assumes g: "g -- f a --> l"
   433   assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> f a"
   434   shows "(\<lambda>x. g (f x)) -- a --> l"
   435 by (rule metric_LIM_compose2 [OF f g inj])
   436 
   437 lemma isCont_LIM_compose2:
   438   fixes a :: "'a::real_normed_vector"
   439   assumes f [unfolded isCont_def]: "isCont f a"
   440   assumes g: "g -- f a --> l"
   441   assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> f a"
   442   shows "(\<lambda>x. g (f x)) -- a --> l"
   443 by (rule LIM_compose2 [OF f g inj])
   444 
   445 lemma isCont_o2: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. g (f x)) a"
   446   unfolding isCont_def by (rule LIM_compose)
   447 
   448 lemma isCont_o: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (g o f) a"
   449   unfolding o_def by (rule isCont_o2)
   450 
   451 lemma (in bounded_linear) isCont:
   452   "isCont g a \<Longrightarrow> isCont (\<lambda>x. f (g x)) a"
   453   unfolding isCont_def by (rule LIM)
   454 
   455 lemma (in bounded_bilinear) isCont:
   456   "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
   457   unfolding isCont_def by (rule LIM)
   458 
   459 lemmas isCont_scaleR [simp] =
   460   bounded_bilinear.isCont [OF bounded_bilinear_scaleR]
   461 
   462 lemmas isCont_of_real [simp] =
   463   bounded_linear.isCont [OF bounded_linear_of_real]
   464 
   465 lemma isCont_power [simp]:
   466   fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}"
   467   shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
   468   unfolding isCont_def by (rule LIM_power)
   469 
   470 lemma isCont_sgn [simp]:
   471   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   472   shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. sgn (f x)) a"
   473   unfolding isCont_def by (rule LIM_sgn)
   474 
   475 lemma isCont_setsum [simp]:
   476   fixes f :: "'a \<Rightarrow> 'b::topological_space \<Rightarrow> 'c::real_normed_vector"
   477   fixes A :: "'a set"
   478   shows "\<forall>i\<in>A. isCont (f i) a \<Longrightarrow> isCont (\<lambda>x. \<Sum>i\<in>A. f i x) a"
   479   unfolding isCont_def by (simp add: tendsto_setsum)
   480 
   481 lemmas isCont_intros =
   482   isCont_ident isCont_const isCont_norm isCont_rabs isCont_add isCont_minus
   483   isCont_diff isCont_mult isCont_inverse isCont_divide isCont_scaleR
   484   isCont_of_real isCont_power isCont_sgn isCont_setsum
   485 
   486 lemma LIM_less_bound: fixes f :: "real \<Rightarrow> real" assumes "b < x"
   487   and all_le: "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and isCont: "isCont f x"
   488   shows "0 \<le> f x"
   489 proof (rule ccontr)
   490   assume "\<not> 0 \<le> f x" hence "f x < 0" by auto
   491   hence "0 < - f x / 2" by auto
   492   from isCont[unfolded isCont_def, THEN LIM_D, OF this]
   493   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
   494 
   495   let ?x = "x - min (s / 2) ((x - b) / 2)"
   496   have "?x < x" and "\<bar> ?x - x \<bar> < s"
   497     using `b < x` and `0 < s` by auto
   498   have "b < ?x"
   499   proof (cases "s < x - b")
   500     case True thus ?thesis using `0 < s` by auto
   501   next
   502     case False hence "s / 2 \<ge> (x - b) / 2" by auto
   503     hence "?x = (x + b) / 2" by (simp add: field_simps min_max.inf_absorb2)
   504     thus ?thesis using `b < x` by auto
   505   qed
   506   hence "0 \<le> f ?x" using all_le `?x < x` by auto
   507   moreover have "\<bar>f ?x - f x\<bar> < - f x / 2"
   508     using s_D[OF _ `\<bar> ?x - x \<bar> < s`] `?x < x` by auto
   509   hence "f ?x - f x < - f x / 2" by auto
   510   hence "f ?x < f x / 2" by auto
   511   hence "f ?x < 0" using `f x < 0` by auto
   512   thus False using `0 \<le> f ?x` by auto
   513 qed
   514 
   515 
   516 subsection {* Uniform Continuity *}
   517 
   518 lemma isUCont_isCont: "isUCont f ==> isCont f x"
   519 by (simp add: isUCont_def isCont_def LIM_def, force)
   520 
   521 lemma isUCont_Cauchy:
   522   "\<lbrakk>isUCont f; Cauchy X\<rbrakk> \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
   523 unfolding isUCont_def
   524 apply (rule metric_CauchyI)
   525 apply (drule_tac x=e in spec, safe)
   526 apply (drule_tac e=s in metric_CauchyD, safe)
   527 apply (rule_tac x=M in exI, simp)
   528 done
   529 
   530 lemma (in bounded_linear) isUCont: "isUCont f"
   531 unfolding isUCont_def dist_norm
   532 proof (intro allI impI)
   533   fix r::real assume r: "0 < r"
   534   obtain K where K: "0 < K" and norm_le: "\<And>x. norm (f x) \<le> norm x * K"
   535     using pos_bounded by fast
   536   show "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r"
   537   proof (rule exI, safe)
   538     from r K show "0 < r / K" by (rule divide_pos_pos)
   539   next
   540     fix x y :: 'a
   541     assume xy: "norm (x - y) < r / K"
   542     have "norm (f x - f y) = norm (f (x - y))" by (simp only: diff)
   543     also have "\<dots> \<le> norm (x - y) * K" by (rule norm_le)
   544     also from K xy have "\<dots> < r" by (simp only: pos_less_divide_eq)
   545     finally show "norm (f x - f y) < r" .
   546   qed
   547 qed
   548 
   549 lemma (in bounded_linear) Cauchy: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
   550 by (rule isUCont [THEN isUCont_Cauchy])
   551 
   552 
   553 subsection {* Relation of LIM and LIMSEQ *}
   554 
   555 lemma LIMSEQ_SEQ_conv1:
   556   fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
   557   assumes f: "f -- a --> l"
   558   shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"
   559   using tendsto_compose_eventually [OF f, where F=sequentially] by simp
   560 
   561 lemma LIMSEQ_SEQ_conv2_lemma:
   562   fixes a :: "'a::metric_space"
   563   assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> eventually (\<lambda>x. P (S x)) sequentially"
   564   shows "eventually P (at a)"
   565 proof (rule ccontr)
   566   let ?I = "\<lambda>n. inverse (real (Suc n))"
   567   let ?F = "\<lambda>n::nat. SOME x. x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x"
   568   assume "\<not> eventually P (at a)"
   569   hence P: "\<forall>d>0. \<exists>x. x \<noteq> a \<and> dist x a < d \<and> \<not> P x"
   570     unfolding eventually_at by simp
   571   hence "\<And>n. \<exists>x. x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x" by simp
   572   hence F: "\<And>n. ?F n \<noteq> a \<and> dist (?F n) a < ?I n \<and> \<not> P (?F n)"
   573     by (rule someI_ex)
   574   hence F1: "\<And>n. ?F n \<noteq> a"
   575     and F2: "\<And>n. dist (?F n) a < ?I n"
   576     and F3: "\<And>n. \<not> P (?F n)"
   577     by fast+
   578   have "?F ----> a"
   579     using LIMSEQ_inverse_real_of_nat
   580     by (rule metric_tendsto_imp_tendsto,
   581       simp add: dist_norm F2 [THEN less_imp_le])
   582   moreover have "\<forall>n. ?F n \<noteq> a"
   583     by (rule allI) (rule F1)
   584   ultimately have "eventually (\<lambda>n. P (?F n)) sequentially"
   585     using assms by simp
   586   thus "False" by (simp add: F3)
   587 qed
   588 
   589 lemma LIMSEQ_SEQ_conv2:
   590   fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
   591   assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"
   592   shows "f -- a --> l"
   593   using assms unfolding tendsto_def [where l=l]
   594   by (simp add: LIMSEQ_SEQ_conv2_lemma)
   595 
   596 lemma LIMSEQ_SEQ_conv:
   597   "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::'a::metric_space) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) =
   598    (X -- a --> (L::'b::topological_space))"
   599   using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 ..
   600 
   601 end