src/HOL/Lim.thy
author huffman
Thu Aug 18 13:36:58 2011 -0700 (2011-08-18)
changeset 44282 f0de18b62d63
parent 44254 336dd390e4a4
child 44310 ba3d031b5dbb
permissions -rw-r--r--
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
     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_LIM_compose:
   423   "\<lbrakk>isCont g l; f -- a --> l\<rbrakk> \<Longrightarrow> (\<lambda>x. g (f x)) -- a --> g l"
   424   unfolding isCont_def by (rule LIM_compose)
   425 
   426 lemma metric_isCont_LIM_compose2:
   427   assumes f [unfolded isCont_def]: "isCont f a"
   428   assumes g: "g -- f a --> l"
   429   assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> f a"
   430   shows "(\<lambda>x. g (f x)) -- a --> l"
   431 by (rule metric_LIM_compose2 [OF f g inj])
   432 
   433 lemma isCont_LIM_compose2:
   434   fixes a :: "'a::real_normed_vector"
   435   assumes f [unfolded isCont_def]: "isCont f a"
   436   assumes g: "g -- f a --> l"
   437   assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> f a"
   438   shows "(\<lambda>x. g (f x)) -- a --> l"
   439 by (rule LIM_compose2 [OF f g inj])
   440 
   441 lemma isCont_o2: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. g (f x)) a"
   442   unfolding isCont_def by (rule LIM_compose)
   443 
   444 lemma isCont_o: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (g o f) a"
   445   unfolding o_def by (rule isCont_o2)
   446 
   447 lemma (in bounded_linear) isCont:
   448   "isCont g a \<Longrightarrow> isCont (\<lambda>x. f (g x)) a"
   449   unfolding isCont_def by (rule LIM)
   450 
   451 lemma (in bounded_bilinear) isCont:
   452   "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
   453   unfolding isCont_def by (rule LIM)
   454 
   455 lemmas isCont_scaleR [simp] =
   456   bounded_bilinear.isCont [OF bounded_bilinear_scaleR]
   457 
   458 lemmas isCont_of_real [simp] =
   459   bounded_linear.isCont [OF bounded_linear_of_real]
   460 
   461 lemma isCont_power [simp]:
   462   fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}"
   463   shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
   464   unfolding isCont_def by (rule LIM_power)
   465 
   466 lemma isCont_sgn [simp]:
   467   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   468   shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. sgn (f x)) a"
   469   unfolding isCont_def by (rule LIM_sgn)
   470 
   471 lemma isCont_setsum [simp]:
   472   fixes f :: "'a \<Rightarrow> 'b::topological_space \<Rightarrow> 'c::real_normed_vector"
   473   fixes A :: "'a set"
   474   shows "\<forall>i\<in>A. isCont (f i) a \<Longrightarrow> isCont (\<lambda>x. \<Sum>i\<in>A. f i x) a"
   475   unfolding isCont_def by (simp add: tendsto_setsum)
   476 
   477 lemmas isCont_intros =
   478   isCont_ident isCont_const isCont_norm isCont_rabs isCont_add isCont_minus
   479   isCont_diff isCont_mult isCont_inverse isCont_divide isCont_scaleR
   480   isCont_of_real isCont_power isCont_sgn isCont_setsum
   481 
   482 lemma LIM_less_bound: fixes f :: "real \<Rightarrow> real" assumes "b < x"
   483   and all_le: "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and isCont: "isCont f x"
   484   shows "0 \<le> f x"
   485 proof (rule ccontr)
   486   assume "\<not> 0 \<le> f x" hence "f x < 0" by auto
   487   hence "0 < - f x / 2" by auto
   488   from isCont[unfolded isCont_def, THEN LIM_D, OF this]
   489   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
   490 
   491   let ?x = "x - min (s / 2) ((x - b) / 2)"
   492   have "?x < x" and "\<bar> ?x - x \<bar> < s"
   493     using `b < x` and `0 < s` by auto
   494   have "b < ?x"
   495   proof (cases "s < x - b")
   496     case True thus ?thesis using `0 < s` by auto
   497   next
   498     case False hence "s / 2 \<ge> (x - b) / 2" by auto
   499     hence "?x = (x + b) / 2" by (simp add: field_simps min_max.inf_absorb2)
   500     thus ?thesis using `b < x` by auto
   501   qed
   502   hence "0 \<le> f ?x" using all_le `?x < x` by auto
   503   moreover have "\<bar>f ?x - f x\<bar> < - f x / 2"
   504     using s_D[OF _ `\<bar> ?x - x \<bar> < s`] `?x < x` by auto
   505   hence "f ?x - f x < - f x / 2" by auto
   506   hence "f ?x < f x / 2" by auto
   507   hence "f ?x < 0" using `f x < 0` by auto
   508   thus False using `0 \<le> f ?x` by auto
   509 qed
   510 
   511 
   512 subsection {* Uniform Continuity *}
   513 
   514 lemma isUCont_isCont: "isUCont f ==> isCont f x"
   515 by (simp add: isUCont_def isCont_def LIM_def, force)
   516 
   517 lemma isUCont_Cauchy:
   518   "\<lbrakk>isUCont f; Cauchy X\<rbrakk> \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
   519 unfolding isUCont_def
   520 apply (rule metric_CauchyI)
   521 apply (drule_tac x=e in spec, safe)
   522 apply (drule_tac e=s in metric_CauchyD, safe)
   523 apply (rule_tac x=M in exI, simp)
   524 done
   525 
   526 lemma (in bounded_linear) isUCont: "isUCont f"
   527 unfolding isUCont_def dist_norm
   528 proof (intro allI impI)
   529   fix r::real assume r: "0 < r"
   530   obtain K where K: "0 < K" and norm_le: "\<And>x. norm (f x) \<le> norm x * K"
   531     using pos_bounded by fast
   532   show "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r"
   533   proof (rule exI, safe)
   534     from r K show "0 < r / K" by (rule divide_pos_pos)
   535   next
   536     fix x y :: 'a
   537     assume xy: "norm (x - y) < r / K"
   538     have "norm (f x - f y) = norm (f (x - y))" by (simp only: diff)
   539     also have "\<dots> \<le> norm (x - y) * K" by (rule norm_le)
   540     also from K xy have "\<dots> < r" by (simp only: pos_less_divide_eq)
   541     finally show "norm (f x - f y) < r" .
   542   qed
   543 qed
   544 
   545 lemma (in bounded_linear) Cauchy: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
   546 by (rule isUCont [THEN isUCont_Cauchy])
   547 
   548 
   549 subsection {* Relation of LIM and LIMSEQ *}
   550 
   551 lemma LIMSEQ_SEQ_conv1:
   552   fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
   553   assumes f: "f -- a --> l"
   554   shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"
   555   using tendsto_compose_eventually [OF f, where F=sequentially] by simp
   556 
   557 lemma LIMSEQ_SEQ_conv2_lemma:
   558   fixes a :: "'a::metric_space"
   559   assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> eventually (\<lambda>x. P (S x)) sequentially"
   560   shows "eventually P (at a)"
   561 proof (rule ccontr)
   562   let ?I = "\<lambda>n. inverse (real (Suc n))"
   563   let ?F = "\<lambda>n::nat. SOME x. x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x"
   564   assume "\<not> eventually P (at a)"
   565   hence P: "\<forall>d>0. \<exists>x. x \<noteq> a \<and> dist x a < d \<and> \<not> P x"
   566     unfolding eventually_at by simp
   567   hence "\<And>n. \<exists>x. x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x" by simp
   568   hence F: "\<And>n. ?F n \<noteq> a \<and> dist (?F n) a < ?I n \<and> \<not> P (?F n)"
   569     by (rule someI_ex)
   570   hence F1: "\<And>n. ?F n \<noteq> a"
   571     and F2: "\<And>n. dist (?F n) a < ?I n"
   572     and F3: "\<And>n. \<not> P (?F n)"
   573     by fast+
   574   have "?F ----> a"
   575     using LIMSEQ_inverse_real_of_nat
   576     by (rule metric_tendsto_imp_tendsto,
   577       simp add: dist_norm F2 [THEN less_imp_le])
   578   moreover have "\<forall>n. ?F n \<noteq> a"
   579     by (rule allI) (rule F1)
   580   ultimately have "eventually (\<lambda>n. P (?F n)) sequentially"
   581     using assms by simp
   582   thus "False" by (simp add: F3)
   583 qed
   584 
   585 lemma LIMSEQ_SEQ_conv2:
   586   fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
   587   assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"
   588   shows "f -- a --> l"
   589   using assms unfolding tendsto_def [where l=l]
   590   by (simp add: LIMSEQ_SEQ_conv2_lemma)
   591 
   592 lemma LIMSEQ_SEQ_conv:
   593   "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::'a::metric_space) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) =
   594    (X -- a --> (L::'b::topological_space))"
   595   using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 ..
   596 
   597 end