src/HOL/Lim.thy
author huffman
Wed Aug 17 11:06:39 2011 -0700 (2011-08-17)
changeset 44251 d101ed3177b6
parent 44233 aa74ce315bae
child 44253 c073a0bd8458
permissions -rw-r--r--
add lemma metric_tendsto_imp_tendsto
     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 proof (rule topological_tendstoI)
   258   fix C assume C: "open C" "c \<in> C"
   259   obtain B where B: "open B" "b \<in> B"
   260     and gC: "\<And>y. y \<in> B \<Longrightarrow> y \<noteq> b \<Longrightarrow> g y \<in> C"
   261     using topological_tendstoD [OF g C]
   262     unfolding eventually_at_topological by fast
   263   obtain A where A: "open A" "a \<in> A"
   264     and fB: "\<And>x. x \<in> A \<Longrightarrow> x \<noteq> a \<Longrightarrow> f x \<in> B"
   265     using topological_tendstoD [OF f B]
   266     unfolding eventually_at_topological by fast
   267   have "eventually (\<lambda>x. f x \<noteq> b \<longrightarrow> g (f x) \<in> C) (at a)"
   268   unfolding eventually_at_topological
   269   proof (intro exI conjI ballI impI)
   270     show "open A" and "a \<in> A" using A .
   271   next
   272     fix x assume "x \<in> A" and "x \<noteq> a" and "f x \<noteq> b"
   273     then show "g (f x) \<in> C" by (simp add: gC fB)
   274   qed
   275   with inj show "eventually (\<lambda>x. g (f x) \<in> C) (at a)"
   276     by (rule eventually_rev_mp)
   277 qed
   278 
   279 lemma metric_LIM_compose2:
   280   assumes f: "f -- a --> b"
   281   assumes g: "g -- b --> c"
   282   assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> b"
   283   shows "(\<lambda>x. g (f x)) -- a --> c"
   284 using f g inj [folded eventually_at]
   285 by (rule LIM_compose_eventually)
   286 
   287 lemma LIM_compose2:
   288   fixes a :: "'a::real_normed_vector"
   289   assumes f: "f -- a --> b"
   290   assumes g: "g -- b --> c"
   291   assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> b"
   292   shows "(\<lambda>x. g (f x)) -- a --> c"
   293 by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]])
   294 
   295 lemma LIM_o: "\<lbrakk>g -- l --> g l; f -- a --> l\<rbrakk> \<Longrightarrow> (g \<circ> f) -- a --> g l"
   296 unfolding o_def by (rule LIM_compose)
   297 
   298 lemma real_LIM_sandwich_zero:
   299   fixes f g :: "'a::topological_space \<Rightarrow> real"
   300   assumes f: "f -- a --> 0"
   301   assumes 1: "\<And>x. x \<noteq> a \<Longrightarrow> 0 \<le> g x"
   302   assumes 2: "\<And>x. x \<noteq> a \<Longrightarrow> g x \<le> f x"
   303   shows "g -- a --> 0"
   304 proof (rule LIM_imp_LIM [OF f])
   305   fix x assume x: "x \<noteq> a"
   306   have "norm (g x - 0) = g x" by (simp add: 1 x)
   307   also have "g x \<le> f x" by (rule 2 [OF x])
   308   also have "f x \<le> \<bar>f x\<bar>" by (rule abs_ge_self)
   309   also have "\<bar>f x\<bar> = norm (f x - 0)" by simp
   310   finally show "norm (g x - 0) \<le> norm (f x - 0)" .
   311 qed
   312 
   313 text {* Bounded Linear Operators *}
   314 
   315 lemma (in bounded_linear) LIM:
   316   "g -- a --> l \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> f l"
   317 by (rule tendsto)
   318 
   319 lemma (in bounded_linear) LIM_zero:
   320   "g -- a --> 0 \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> 0"
   321   by (rule tendsto_zero)
   322 
   323 text {* Bounded Bilinear Operators *}
   324 
   325 lemma (in bounded_bilinear) LIM:
   326   "\<lbrakk>f -- a --> L; g -- a --> M\<rbrakk> \<Longrightarrow> (\<lambda>x. f x ** g x) -- a --> L ** M"
   327 by (rule tendsto)
   328 
   329 lemma (in bounded_bilinear) LIM_prod_zero:
   330   fixes a :: "'d::metric_space"
   331   assumes f: "f -- a --> 0"
   332   assumes g: "g -- a --> 0"
   333   shows "(\<lambda>x. f x ** g x) -- a --> 0"
   334   using f g by (rule tendsto_zero)
   335 
   336 lemma (in bounded_bilinear) LIM_left_zero:
   337   "f -- a --> 0 \<Longrightarrow> (\<lambda>x. f x ** c) -- a --> 0"
   338   by (rule tendsto_left_zero)
   339 
   340 lemma (in bounded_bilinear) LIM_right_zero:
   341   "f -- a --> 0 \<Longrightarrow> (\<lambda>x. c ** f x) -- a --> 0"
   342   by (rule tendsto_right_zero)
   343 
   344 lemmas LIM_mult = mult.LIM
   345 
   346 lemmas LIM_mult_zero = mult.LIM_prod_zero
   347 
   348 lemmas LIM_mult_left_zero = mult.LIM_left_zero
   349 
   350 lemmas LIM_mult_right_zero = mult.LIM_right_zero
   351 
   352 lemmas LIM_scaleR = scaleR.LIM
   353 
   354 lemmas LIM_of_real = of_real.LIM
   355 
   356 lemma LIM_power:
   357   fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}"
   358   assumes f: "f -- a --> l"
   359   shows "(\<lambda>x. f x ^ n) -- a --> l ^ n"
   360   using assms by (rule tendsto_power)
   361 
   362 lemma LIM_inverse:
   363   fixes L :: "'a::real_normed_div_algebra"
   364   shows "\<lbrakk>f -- a --> L; L \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. inverse (f x)) -- a --> inverse L"
   365 by (rule tendsto_inverse)
   366 
   367 lemma LIM_inverse_fun:
   368   assumes a: "a \<noteq> (0::'a::real_normed_div_algebra)"
   369   shows "inverse -- a --> inverse a"
   370 by (rule LIM_inverse [OF LIM_ident a])
   371 
   372 lemma LIM_sgn:
   373   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   374   shows "\<lbrakk>f -- a --> l; l \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. sgn (f x)) -- a --> sgn l"
   375   by (rule tendsto_sgn)
   376 
   377 
   378 subsection {* Continuity *}
   379 
   380 lemma LIM_isCont_iff:
   381   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
   382   shows "(f -- a --> f a) = ((\<lambda>h. f (a + h)) -- 0 --> f a)"
   383 by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel])
   384 
   385 lemma isCont_iff:
   386   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
   387   shows "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x"
   388 by (simp add: isCont_def LIM_isCont_iff)
   389 
   390 lemma isCont_ident [simp]: "isCont (\<lambda>x. x) a"
   391   unfolding isCont_def by (rule LIM_ident)
   392 
   393 lemma isCont_const [simp]: "isCont (\<lambda>x. k) a"
   394   unfolding isCont_def by (rule LIM_const)
   395 
   396 lemma isCont_norm [simp]:
   397   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   398   shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a"
   399   unfolding isCont_def by (rule LIM_norm)
   400 
   401 lemma isCont_rabs [simp]:
   402   fixes f :: "'a::topological_space \<Rightarrow> real"
   403   shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x\<bar>) a"
   404   unfolding isCont_def by (rule LIM_rabs)
   405 
   406 lemma isCont_add [simp]:
   407   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   408   shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"
   409   unfolding isCont_def by (rule LIM_add)
   410 
   411 lemma isCont_minus [simp]:
   412   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   413   shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a"
   414   unfolding isCont_def by (rule LIM_minus)
   415 
   416 lemma isCont_diff [simp]:
   417   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   418   shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a"
   419   unfolding isCont_def by (rule LIM_diff)
   420 
   421 lemma isCont_mult [simp]:
   422   fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra"
   423   shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x * g x) a"
   424   unfolding isCont_def by (rule LIM_mult)
   425 
   426 lemma isCont_inverse [simp]:
   427   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra"
   428   shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. inverse (f x)) a"
   429   unfolding isCont_def by (rule LIM_inverse)
   430 
   431 lemma isCont_divide [simp]:
   432   fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_field"
   433   shows "\<lbrakk>isCont f a; isCont g a; g a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x / g x) a"
   434   unfolding isCont_def by (rule tendsto_divide)
   435 
   436 lemma isCont_LIM_compose:
   437   "\<lbrakk>isCont g l; f -- a --> l\<rbrakk> \<Longrightarrow> (\<lambda>x. g (f x)) -- a --> g l"
   438   unfolding isCont_def by (rule LIM_compose)
   439 
   440 lemma metric_isCont_LIM_compose2:
   441   assumes f [unfolded isCont_def]: "isCont f a"
   442   assumes g: "g -- f a --> l"
   443   assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> f a"
   444   shows "(\<lambda>x. g (f x)) -- a --> l"
   445 by (rule metric_LIM_compose2 [OF f g inj])
   446 
   447 lemma isCont_LIM_compose2:
   448   fixes a :: "'a::real_normed_vector"
   449   assumes f [unfolded isCont_def]: "isCont f a"
   450   assumes g: "g -- f a --> l"
   451   assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> f a"
   452   shows "(\<lambda>x. g (f x)) -- a --> l"
   453 by (rule LIM_compose2 [OF f g inj])
   454 
   455 lemma isCont_o2: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. g (f x)) a"
   456   unfolding isCont_def by (rule LIM_compose)
   457 
   458 lemma isCont_o: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (g o f) a"
   459   unfolding o_def by (rule isCont_o2)
   460 
   461 lemma (in bounded_linear) isCont:
   462   "isCont g a \<Longrightarrow> isCont (\<lambda>x. f (g x)) a"
   463   unfolding isCont_def by (rule LIM)
   464 
   465 lemma (in bounded_bilinear) isCont:
   466   "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
   467   unfolding isCont_def by (rule LIM)
   468 
   469 lemmas isCont_scaleR [simp] = scaleR.isCont
   470 
   471 lemma isCont_of_real [simp]:
   472   "isCont f a \<Longrightarrow> isCont (\<lambda>x. of_real (f x)::'b::real_normed_algebra_1) a"
   473   by (rule of_real.isCont)
   474 
   475 lemma isCont_power [simp]:
   476   fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}"
   477   shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
   478   unfolding isCont_def by (rule LIM_power)
   479 
   480 lemma isCont_sgn [simp]:
   481   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   482   shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. sgn (f x)) a"
   483   unfolding isCont_def by (rule LIM_sgn)
   484 
   485 lemma isCont_setsum [simp]:
   486   fixes f :: "'a \<Rightarrow> 'b::topological_space \<Rightarrow> 'c::real_normed_vector"
   487   fixes A :: "'a set"
   488   shows "\<forall>i\<in>A. isCont (f i) a \<Longrightarrow> isCont (\<lambda>x. \<Sum>i\<in>A. f i x) a"
   489   unfolding isCont_def by (simp add: tendsto_setsum)
   490 
   491 lemmas isCont_intros =
   492   isCont_ident isCont_const isCont_norm isCont_rabs isCont_add isCont_minus
   493   isCont_diff isCont_mult isCont_inverse isCont_divide isCont_scaleR
   494   isCont_of_real isCont_power isCont_sgn isCont_setsum
   495 
   496 lemma LIM_less_bound: fixes f :: "real \<Rightarrow> real" assumes "b < x"
   497   and all_le: "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and isCont: "isCont f x"
   498   shows "0 \<le> f x"
   499 proof (rule ccontr)
   500   assume "\<not> 0 \<le> f x" hence "f x < 0" by auto
   501   hence "0 < - f x / 2" by auto
   502   from isCont[unfolded isCont_def, THEN LIM_D, OF this]
   503   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
   504 
   505   let ?x = "x - min (s / 2) ((x - b) / 2)"
   506   have "?x < x" and "\<bar> ?x - x \<bar> < s"
   507     using `b < x` and `0 < s` by auto
   508   have "b < ?x"
   509   proof (cases "s < x - b")
   510     case True thus ?thesis using `0 < s` by auto
   511   next
   512     case False hence "s / 2 \<ge> (x - b) / 2" by auto
   513     hence "?x = (x + b) / 2" by (simp add: field_simps min_max.inf_absorb2)
   514     thus ?thesis using `b < x` by auto
   515   qed
   516   hence "0 \<le> f ?x" using all_le `?x < x` by auto
   517   moreover have "\<bar>f ?x - f x\<bar> < - f x / 2"
   518     using s_D[OF _ `\<bar> ?x - x \<bar> < s`] `?x < x` by auto
   519   hence "f ?x - f x < - f x / 2" by auto
   520   hence "f ?x < f x / 2" by auto
   521   hence "f ?x < 0" using `f x < 0` by auto
   522   thus False using `0 \<le> f ?x` by auto
   523 qed
   524 
   525 
   526 subsection {* Uniform Continuity *}
   527 
   528 lemma isUCont_isCont: "isUCont f ==> isCont f x"
   529 by (simp add: isUCont_def isCont_def LIM_def, force)
   530 
   531 lemma isUCont_Cauchy:
   532   "\<lbrakk>isUCont f; Cauchy X\<rbrakk> \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
   533 unfolding isUCont_def
   534 apply (rule metric_CauchyI)
   535 apply (drule_tac x=e in spec, safe)
   536 apply (drule_tac e=s in metric_CauchyD, safe)
   537 apply (rule_tac x=M in exI, simp)
   538 done
   539 
   540 lemma (in bounded_linear) isUCont: "isUCont f"
   541 unfolding isUCont_def dist_norm
   542 proof (intro allI impI)
   543   fix r::real assume r: "0 < r"
   544   obtain K where K: "0 < K" and norm_le: "\<And>x. norm (f x) \<le> norm x * K"
   545     using pos_bounded by fast
   546   show "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r"
   547   proof (rule exI, safe)
   548     from r K show "0 < r / K" by (rule divide_pos_pos)
   549   next
   550     fix x y :: 'a
   551     assume xy: "norm (x - y) < r / K"
   552     have "norm (f x - f y) = norm (f (x - y))" by (simp only: diff)
   553     also have "\<dots> \<le> norm (x - y) * K" by (rule norm_le)
   554     also from K xy have "\<dots> < r" by (simp only: pos_less_divide_eq)
   555     finally show "norm (f x - f y) < r" .
   556   qed
   557 qed
   558 
   559 lemma (in bounded_linear) Cauchy: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
   560 by (rule isUCont [THEN isUCont_Cauchy])
   561 
   562 
   563 subsection {* Relation of LIM and LIMSEQ *}
   564 
   565 lemma LIMSEQ_SEQ_conv1:
   566   fixes a :: "'a::metric_space" and L :: "'b::metric_space"
   567   assumes X: "X -- a --> L"
   568   shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
   569 proof (safe intro!: metric_LIMSEQ_I)
   570   fix S :: "nat \<Rightarrow> 'a"
   571   fix r :: real
   572   assume rgz: "0 < r"
   573   assume as: "\<forall>n. S n \<noteq> a"
   574   assume S: "S ----> a"
   575   from metric_LIM_D [OF X rgz] obtain s
   576     where sgz: "0 < s"
   577     and aux: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < s\<rbrakk> \<Longrightarrow> dist (X x) L < r"
   578     by fast
   579   from metric_LIMSEQ_D [OF S sgz]
   580   obtain no where "\<forall>n\<ge>no. dist (S n) a < s" by blast
   581   hence "\<forall>n\<ge>no. dist (X (S n)) L < r" by (simp add: aux as)
   582   thus "\<exists>no. \<forall>n\<ge>no. dist (X (S n)) L < r" ..
   583 qed
   584 
   585 
   586 lemma LIMSEQ_SEQ_conv2:
   587   fixes a :: real and L :: "'a::metric_space"
   588   assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
   589   shows "X -- a --> L"
   590 proof (rule ccontr)
   591   assume "\<not> (X -- a --> L)"
   592   hence "\<not> (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x - a) < s --> dist (X x) L < r)"
   593     unfolding LIM_def dist_norm .
   594   hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. \<not>(x \<noteq> a \<and> \<bar>x - a\<bar> < s --> dist (X x) L < r)" by simp
   595   hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x - a\<bar> < s \<and> dist (X x) L \<ge> r)" by (simp add: not_less)
   596   then obtain r where rdef: "r > 0 \<and> (\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x - a\<bar> < s \<and> dist (X x) L \<ge> r))" by auto
   597 
   598   let ?F = "\<lambda>n::nat. SOME x. x\<noteq>a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> dist (X x) L \<ge> r"
   599   have "\<And>n. \<exists>x. x\<noteq>a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> dist (X x) L \<ge> r"
   600     using rdef by simp
   601   hence F: "\<And>n. ?F n \<noteq> a \<and> \<bar>?F n - a\<bar> < inverse (real (Suc n)) \<and> dist (X (?F n)) L \<ge> r"
   602     by (rule someI_ex)
   603   hence F1: "\<And>n. ?F n \<noteq> a"
   604     and F2: "\<And>n. \<bar>?F n - a\<bar> < inverse (real (Suc n))"
   605     and F3: "\<And>n. dist (X (?F n)) L \<ge> r"
   606     by fast+
   607 
   608   have "?F ----> a"
   609   proof (rule LIMSEQ_I, unfold real_norm_def)
   610       fix e::real
   611       assume "0 < e"
   612         (* choose no such that inverse (real (Suc n)) < e *)
   613       then have "\<exists>no. inverse (real (Suc no)) < e" by (rule reals_Archimedean)
   614       then obtain m where nodef: "inverse (real (Suc m)) < e" by auto
   615       show "\<exists>no. \<forall>n. no \<le> n --> \<bar>?F n - a\<bar> < e"
   616       proof (intro exI allI impI)
   617         fix n
   618         assume mlen: "m \<le> n"
   619         have "\<bar>?F n - a\<bar> < inverse (real (Suc n))"
   620           by (rule F2)
   621         also have "inverse (real (Suc n)) \<le> inverse (real (Suc m))"
   622           using mlen by auto
   623         also from nodef have
   624           "inverse (real (Suc m)) < e" .
   625         finally show "\<bar>?F n - a\<bar> < e" .
   626       qed
   627   qed
   628   
   629   moreover have "\<forall>n. ?F n \<noteq> a"
   630     by (rule allI) (rule F1)
   631 
   632   moreover note `\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L`
   633   ultimately have "(\<lambda>n. X (?F n)) ----> L" by simp
   634   
   635   moreover have "\<not> ((\<lambda>n. X (?F n)) ----> L)"
   636   proof -
   637     {
   638       fix no::nat
   639       obtain n where "n = no + 1" by simp
   640       then have nolen: "no \<le> n" by simp
   641         (* We prove this by showing that for any m there is an n\<ge>m such that |X (?F n) - L| \<ge> r *)
   642       have "dist (X (?F n)) L \<ge> r"
   643         by (rule F3)
   644       with nolen have "\<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> r" by fast
   645     }
   646     then have "(\<forall>no. \<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> r)" by simp
   647     with rdef have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> e)" by auto
   648     thus ?thesis by (unfold LIMSEQ_def, auto simp add: not_less)
   649   qed
   650   ultimately show False by simp
   651 qed
   652 
   653 lemma LIMSEQ_SEQ_conv:
   654   "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::real) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) =
   655    (X -- a --> (L::'a::metric_space))"
   656 proof
   657   assume "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
   658   thus "X -- a --> L" by (rule LIMSEQ_SEQ_conv2)
   659 next
   660   assume "(X -- a --> L)"
   661   thus "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L" by (rule LIMSEQ_SEQ_conv1)
   662 qed
   663 
   664 end