src/HOL/Hyperreal/Lim.thy
author nipkow
Sun Dec 10 07:12:26 2006 +0100 (2006-12-10)
changeset 21733 131dd2a27137
parent 21404 eb85850d3eb7
child 21786 66da6af2b0c9
permissions -rw-r--r--
Modified lattice locale
     1 (*  Title       : Lim.thy
     2     ID          : $Id$
     3     Author      : Jacques D. Fleuriot
     4     Copyright   : 1998  University of Cambridge
     5     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     6 *)
     7 
     8 header{* Limits and Continuity *}
     9 
    10 theory Lim
    11 imports SEQ
    12 begin
    13 
    14 text{*Standard and Nonstandard Definitions*}
    15 
    16 definition
    17   LIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
    18         ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where
    19   "f -- a --> L =
    20      (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x - a) < s
    21         --> norm (f x - L) < r)"
    22 
    23 definition
    24   NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
    25             ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) where
    26   "f -- a --NS> L =
    27     (\<forall>x. (x \<noteq> star_of a & x @= star_of a --> ( *f* f) x @= star_of L))"
    28 
    29 definition
    30   isCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where
    31   "isCont f a = (f -- a --> (f a))"
    32 
    33 definition
    34   isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where
    35     --{*NS definition dispenses with limit notions*}
    36   "isNSCont f a = (\<forall>y. y @= star_of a -->
    37          ( *f* f) y @= star_of (f a))"
    38 
    39 definition
    40   isUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where
    41   "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r)"
    42 
    43 definition
    44   isNSUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where
    45   "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
    46 
    47 
    48 subsection {* Limits of Functions *}
    49 
    50 subsubsection {* Purely standard proofs *}
    51 
    52 lemma LIM_eq:
    53      "f -- a --> L =
    54      (\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)"
    55 by (simp add: LIM_def diff_minus)
    56 
    57 lemma LIM_I:
    58      "(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)
    59       ==> f -- a --> L"
    60 by (simp add: LIM_eq)
    61 
    62 lemma LIM_D:
    63      "[| f -- a --> L; 0<r |]
    64       ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r"
    65 by (simp add: LIM_eq)
    66 
    67 lemma LIM_offset: "f -- a --> L \<Longrightarrow> (\<lambda>x. f (x + k)) -- a - k --> L"
    68 apply (rule LIM_I)
    69 apply (drule_tac r="r" in LIM_D, safe)
    70 apply (rule_tac x="s" in exI, safe)
    71 apply (drule_tac x="x + k" in spec)
    72 apply (simp add: compare_rls)
    73 done
    74 
    75 lemma LIM_offset_zero: "f -- a --> L \<Longrightarrow> (\<lambda>h. f (a + h)) -- 0 --> L"
    76 by (drule_tac k="a" in LIM_offset, simp add: add_commute)
    77 
    78 lemma LIM_offset_zero_cancel: "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L"
    79 by (drule_tac k="- a" in LIM_offset, simp)
    80 
    81 lemma LIM_const [simp]: "(%x. k) -- x --> k"
    82 by (simp add: LIM_def)
    83 
    84 lemma LIM_add:
    85   fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
    86   assumes f: "f -- a --> L" and g: "g -- a --> M"
    87   shows "(%x. f x + g(x)) -- a --> (L + M)"
    88 proof (rule LIM_I)
    89   fix r :: real
    90   assume r: "0 < r"
    91   from LIM_D [OF f half_gt_zero [OF r]]
    92   obtain fs
    93     where fs:    "0 < fs"
    94       and fs_lt: "\<forall>x. x \<noteq> a & norm (x-a) < fs --> norm (f x - L) < r/2"
    95   by blast
    96   from LIM_D [OF g half_gt_zero [OF r]]
    97   obtain gs
    98     where gs:    "0 < gs"
    99       and gs_lt: "\<forall>x. x \<noteq> a & norm (x-a) < gs --> norm (g x - M) < r/2"
   100   by blast
   101   show "\<exists>s>0.\<forall>x. x \<noteq> a \<and> norm (x-a) < s \<longrightarrow> norm (f x + g x - (L + M)) < r"
   102   proof (intro exI conjI strip)
   103     show "0 < min fs gs"  by (simp add: fs gs)
   104     fix x :: 'a
   105     assume "x \<noteq> a \<and> norm (x-a) < min fs gs"
   106     hence "x \<noteq> a \<and> norm (x-a) < fs \<and> norm (x-a) < gs" by simp
   107     with fs_lt gs_lt
   108     have "norm (f x - L) < r/2" and "norm (g x - M) < r/2" by blast+
   109     hence "norm (f x - L) + norm (g x - M) < r" by arith
   110     thus "norm (f x + g x - (L + M)) < r"
   111       by (blast intro: norm_diff_triangle_ineq order_le_less_trans)
   112   qed
   113 qed
   114 
   115 lemma LIM_add_zero:
   116   "\<lbrakk>f -- a --> 0; g -- a --> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. f x + g x) -- a --> 0"
   117 by (drule (1) LIM_add, simp)
   118 
   119 lemma minus_diff_minus:
   120   fixes a b :: "'a::ab_group_add"
   121   shows "(- a) - (- b) = - (a - b)"
   122 by simp
   123 
   124 lemma LIM_minus: "f -- a --> L ==> (%x. -f(x)) -- a --> -L"
   125 by (simp only: LIM_eq minus_diff_minus norm_minus_cancel)
   126 
   127 lemma LIM_add_minus:
   128     "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + -g(x)) -- x --> (l + -m)"
   129 by (intro LIM_add LIM_minus)
   130 
   131 lemma LIM_diff:
   132     "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) - g(x)) -- x --> l-m"
   133 by (simp only: diff_minus LIM_add LIM_minus)
   134 
   135 lemma LIM_zero: "f -- a --> l \<Longrightarrow> (\<lambda>x. f x - l) -- a --> 0"
   136 by (simp add: LIM_def)
   137 
   138 lemma LIM_zero_cancel: "(\<lambda>x. f x - l) -- a --> 0 \<Longrightarrow> f -- a --> l"
   139 by (simp add: LIM_def)
   140 
   141 lemma LIM_zero_iff: "(\<lambda>x. f x - l) -- a --> 0 = f -- a --> l"
   142 by (simp add: LIM_def)
   143 
   144 lemma LIM_imp_LIM:
   145   assumes f: "f -- a --> l"
   146   assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)"
   147   shows "g -- a --> m"
   148 apply (rule LIM_I, drule LIM_D [OF f], safe)
   149 apply (rule_tac x="s" in exI, safe)
   150 apply (drule_tac x="x" in spec, safe)
   151 apply (erule (1) order_le_less_trans [OF le])
   152 done
   153 
   154 lemma LIM_norm: "f -- a --> l \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> norm l"
   155 by (erule LIM_imp_LIM, simp add: norm_triangle_ineq3)
   156 
   157 lemma LIM_norm_zero: "f -- a --> 0 \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> 0"
   158 by (drule LIM_norm, simp)
   159 
   160 lemma LIM_norm_zero_cancel: "(\<lambda>x. norm (f x)) -- a --> 0 \<Longrightarrow> f -- a --> 0"
   161 by (erule LIM_imp_LIM, simp)
   162 
   163 lemma LIM_norm_zero_iff: "(\<lambda>x. norm (f x)) -- a --> 0 = f -- a --> 0"
   164 by (rule iffI [OF LIM_norm_zero_cancel LIM_norm_zero])
   165 
   166 lemma LIM_const_not_eq:
   167   fixes a :: "'a::real_normed_div_algebra"
   168   shows "k \<noteq> L ==> ~ ((%x. k) -- a --> L)"
   169 apply (simp add: LIM_eq)
   170 apply (rule_tac x="norm (k - L)" in exI, simp, safe)
   171 apply (rule_tac x="a + of_real (s/2)" in exI, simp add: norm_of_real)
   172 done
   173 
   174 lemma LIM_const_eq:
   175   fixes a :: "'a::real_normed_div_algebra"
   176   shows "(%x. k) -- a --> L ==> k = L"
   177 apply (rule ccontr)
   178 apply (blast dest: LIM_const_not_eq)
   179 done
   180 
   181 lemma LIM_unique:
   182   fixes a :: "'a::real_normed_div_algebra"
   183   shows "[| f -- a --> L; f -- a --> M |] ==> L = M"
   184 apply (drule LIM_diff, assumption)
   185 apply (auto dest!: LIM_const_eq)
   186 done
   187 
   188 lemma LIM_mult_zero:
   189   fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
   190   assumes f: "f -- a --> 0" and g: "g -- a --> 0"
   191   shows "(%x. f(x) * g(x)) -- a --> 0"
   192 proof (rule LIM_I, simp)
   193   fix r :: real
   194   assume r: "0<r"
   195   from LIM_D [OF f zero_less_one]
   196   obtain fs
   197     where fs:    "0 < fs"
   198       and fs_lt: "\<forall>x. x \<noteq> a & norm (x-a) < fs --> norm (f x) < 1"
   199   by auto
   200   from LIM_D [OF g r]
   201   obtain gs
   202     where gs:    "0 < gs"
   203       and gs_lt: "\<forall>x. x \<noteq> a & norm (x-a) < gs --> norm (g x) < r"
   204   by auto
   205   show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> a \<and> norm (x-a) < s \<longrightarrow> norm (f x * g x) < r)"
   206   proof (intro exI conjI strip)
   207     show "0 < min fs gs"  by (simp add: fs gs)
   208     fix x :: 'a
   209     assume "x \<noteq> a \<and> norm (x-a) < min fs gs"
   210     hence  "x \<noteq> a \<and> norm (x-a) < fs \<and> norm (x-a) < gs" by simp
   211     with fs_lt gs_lt
   212     have "norm (f x) < 1" and "norm (g x) < r" by blast+
   213     hence "norm (f x) * norm (g x) < 1*r"
   214       by (rule mult_strict_mono' [OF _ _ norm_ge_zero norm_ge_zero])
   215     thus "norm (f x * g x) < r"
   216       by (simp add: order_le_less_trans [OF norm_mult_ineq])
   217   qed
   218 qed
   219 
   220 lemma LIM_self: "(%x. x) -- a --> a"
   221 by (auto simp add: LIM_def)
   222 
   223 text{*Limits are equal for functions equal except at limit point*}
   224 lemma LIM_equal:
   225      "[| \<forall>x. x \<noteq> a --> (f x = g x) |] ==> (f -- a --> l) = (g -- a --> l)"
   226 by (simp add: LIM_def)
   227 
   228 lemma LIM_cong:
   229   "\<lbrakk>a = b; \<And>x. x \<noteq> b \<Longrightarrow> f x = g x; l = m\<rbrakk>
   230    \<Longrightarrow> ((\<lambda>x. f x) -- a --> l) = ((\<lambda>x. g x) -- b --> m)"
   231 by (simp add: LIM_def)
   232 
   233 lemma LIM_equal2:
   234   assumes 1: "0 < R"
   235   assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < R\<rbrakk> \<Longrightarrow> f x = g x"
   236   shows "g -- a --> l \<Longrightarrow> f -- a --> l"
   237 apply (unfold LIM_def, safe)
   238 apply (drule_tac x="r" in spec, safe)
   239 apply (rule_tac x="min s R" in exI, safe)
   240 apply (simp add: 1)
   241 apply (simp add: 2)
   242 done
   243 
   244 text{*Two uses in Hyperreal/Transcendental.ML*}
   245 lemma LIM_trans:
   246      "[| (%x. f(x) + -g(x)) -- a --> 0;  g -- a --> l |] ==> f -- a --> l"
   247 apply (drule LIM_add, assumption)
   248 apply (auto simp add: add_assoc)
   249 done
   250 
   251 lemma LIM_compose:
   252   assumes g: "g -- l --> g l"
   253   assumes f: "f -- a --> l"
   254   shows "(\<lambda>x. g (f x)) -- a --> g l"
   255 proof (rule LIM_I)
   256   fix r::real assume r: "0 < r"
   257   obtain s where s: "0 < s"
   258     and less_r: "\<And>y. \<lbrakk>y \<noteq> l; norm (y - l) < s\<rbrakk> \<Longrightarrow> norm (g y - g l) < r"
   259     using LIM_D [OF g r] by fast
   260   obtain t where t: "0 < t"
   261     and less_s: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < t\<rbrakk> \<Longrightarrow> norm (f x - l) < s"
   262     using LIM_D [OF f s] by fast
   263 
   264   show "\<exists>t>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < t \<longrightarrow> norm (g (f x) - g l) < r"
   265   proof (rule exI, safe)
   266     show "0 < t" using t .
   267   next
   268     fix x assume "x \<noteq> a" and "norm (x - a) < t"
   269     hence "norm (f x - l) < s" by (rule less_s)
   270     thus "norm (g (f x) - g l) < r"
   271       using r less_r by (case_tac "f x = l", simp_all)
   272   qed
   273 qed
   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::real_normed_vector \<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 subsubsection {* Bounded Linear Operators *}
   294 
   295 locale bounded_linear = additive +
   296   constrains f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   297   assumes scaleR: "f (scaleR r x) = scaleR r (f x)"
   298   assumes bounded: "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K"
   299 
   300 lemma (in bounded_linear) pos_bounded:
   301   "\<exists>K>0. \<forall>x. norm (f x) \<le> norm x * K"
   302 apply (cut_tac bounded, erule exE)
   303 apply (rule_tac x="max 1 K" in exI, safe)
   304 apply (rule order_less_le_trans [OF zero_less_one le_maxI1])
   305 apply (drule spec, erule order_trans)
   306 apply (rule mult_left_mono [OF le_maxI2 norm_ge_zero])
   307 done
   308 
   309 lemma (in bounded_linear) pos_boundedE:
   310   obtains K where "0 < K" and "\<forall>x. norm (f x) \<le> norm x * K"
   311   using pos_bounded by fast
   312 
   313 lemma (in bounded_linear) cont: "f -- a --> f a"
   314 proof (rule LIM_I)
   315   fix r::real assume r: "0 < r"
   316   obtain K where K: "0 < K" and norm_le: "\<And>x. norm (f x) \<le> norm x * K"
   317     using pos_bounded by fast
   318   show "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (f x - f a) < r"
   319   proof (rule exI, safe)
   320     from r K show "0 < r / K" by (rule divide_pos_pos)
   321   next
   322     fix x assume x: "norm (x - a) < r / K"
   323     have "norm (f x - f a) = norm (f (x - a))" by (simp only: diff)
   324     also have "\<dots> \<le> norm (x - a) * K" by (rule norm_le)
   325     also from K x have "\<dots> < r" by (simp only: pos_less_divide_eq)
   326     finally show "norm (f x - f a) < r" .
   327   qed
   328 qed
   329 
   330 lemma (in bounded_linear) LIM:
   331   "g -- a --> l \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> f l"
   332 by (rule LIM_compose [OF cont])
   333 
   334 lemma (in bounded_linear) LIM_zero:
   335   "g -- a --> 0 \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> 0"
   336 by (drule LIM, simp only: zero)
   337 
   338 subsubsection {* Bounded Bilinear Operators *}
   339 
   340 locale bounded_bilinear =
   341   fixes prod :: "['a::real_normed_vector, 'b::real_normed_vector]
   342                  \<Rightarrow> 'c::real_normed_vector"
   343     (infixl "**" 70)
   344   assumes add_left: "prod (a + a') b = prod a b + prod a' b"
   345   assumes add_right: "prod a (b + b') = prod a b + prod a b'"
   346   assumes scaleR_left: "prod (scaleR r a) b = scaleR r (prod a b)"
   347   assumes scaleR_right: "prod a (scaleR r b) = scaleR r (prod a b)"
   348   assumes bounded: "\<exists>K. \<forall>a b. norm (prod a b) \<le> norm a * norm b * K"
   349 
   350 lemma (in bounded_bilinear) pos_bounded:
   351   "\<exists>K>0. \<forall>a b. norm (a ** b) \<le> norm a * norm b * K"
   352 apply (cut_tac bounded, erule exE)
   353 apply (rule_tac x="max 1 K" in exI, safe)
   354 apply (rule order_less_le_trans [OF zero_less_one le_maxI1])
   355 apply (drule spec, drule spec, erule order_trans)
   356 apply (rule mult_left_mono [OF le_maxI2])
   357 apply (intro mult_nonneg_nonneg norm_ge_zero)
   358 done
   359 
   360 lemma (in bounded_bilinear) additive_right: "additive (\<lambda>b. prod a b)"
   361 by (rule additive.intro, rule add_right)
   362 
   363 lemma (in bounded_bilinear) additive_left: "additive (\<lambda>a. prod a b)"
   364 by (rule additive.intro, rule add_left)
   365 
   366 lemma (in bounded_bilinear) zero_left: "prod 0 b = 0"
   367 by (rule additive.zero [OF additive_left])
   368 
   369 lemma (in bounded_bilinear) zero_right: "prod a 0 = 0"
   370 by (rule additive.zero [OF additive_right])
   371 
   372 lemma (in bounded_bilinear) minus_left: "prod (- a) b = - prod a b"
   373 by (rule additive.minus [OF additive_left])
   374 
   375 lemma (in bounded_bilinear) minus_right: "prod a (- b) = - prod a b"
   376 by (rule additive.minus [OF additive_right])
   377 
   378 lemma (in bounded_bilinear) diff_left:
   379   "prod (a - a') b = prod a b - prod a' b"
   380 by (rule additive.diff [OF additive_left])
   381 
   382 lemma (in bounded_bilinear) diff_right:
   383   "prod a (b - b') = prod a b - prod a b'"
   384 by (rule additive.diff [OF additive_right])
   385 
   386 lemma (in bounded_bilinear) LIM_prod_zero:
   387   assumes f: "f -- a --> 0"
   388   assumes g: "g -- a --> 0"
   389   shows "(\<lambda>x. f x ** g x) -- a --> 0"
   390 proof (rule LIM_I)
   391   fix r::real assume r: "0 < r"
   392   obtain K where K: "0 < K"
   393     and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K"
   394     using pos_bounded by fast
   395   from K have K': "0 < inverse K"
   396     by (rule positive_imp_inverse_positive)
   397   obtain s where s: "0 < s"
   398     and norm_f: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < s\<rbrakk> \<Longrightarrow> norm (f x) < r"
   399     using LIM_D [OF f r] by auto
   400   obtain t where t: "0 < t"
   401     and norm_g: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < t\<rbrakk> \<Longrightarrow> norm (g x) < inverse K"
   402     using LIM_D [OF g K'] by auto
   403   show "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (f x ** g x - 0) < r"
   404   proof (rule exI, safe)
   405     from s t show "0 < min s t" by simp
   406   next
   407     fix x assume x: "x \<noteq> a"
   408     assume "norm (x - a) < min s t"
   409     hence xs: "norm (x - a) < s" and xt: "norm (x - a) < t" by simp_all
   410     from x xs have 1: "norm (f x) < r" by (rule norm_f)
   411     from x xt have 2: "norm (g x) < inverse K" by (rule norm_g)
   412     have "norm (f x ** g x) \<le> norm (f x) * norm (g x) * K" by (rule norm_le)
   413     also from 1 2 K have "\<dots> < r * inverse K * K"
   414       by (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero)
   415     also from K have "r * inverse K * K = r" by simp
   416     finally show "norm (f x ** g x - 0) < r" by simp
   417   qed
   418 qed
   419 
   420 lemma (in bounded_bilinear) bounded_linear_left:
   421   "bounded_linear (\<lambda>a. a ** b)"
   422 apply (unfold_locales)
   423 apply (rule add_left)
   424 apply (rule scaleR_left)
   425 apply (cut_tac bounded, safe)
   426 apply (rule_tac x="norm b * K" in exI)
   427 apply (simp add: mult_ac)
   428 done
   429 
   430 lemma (in bounded_bilinear) bounded_linear_right:
   431   "bounded_linear (\<lambda>b. a ** b)"
   432 apply (unfold_locales)
   433 apply (rule add_right)
   434 apply (rule scaleR_right)
   435 apply (cut_tac bounded, safe)
   436 apply (rule_tac x="norm a * K" in exI)
   437 apply (simp add: mult_ac)
   438 done
   439 
   440 lemma (in bounded_bilinear) LIM_left_zero:
   441   "f -- a --> 0 \<Longrightarrow> (\<lambda>x. f x ** c) -- a --> 0"
   442 by (rule bounded_linear.LIM_zero [OF bounded_linear_left])
   443 
   444 lemma (in bounded_bilinear) LIM_right_zero:
   445   "f -- a --> 0 \<Longrightarrow> (\<lambda>x. c ** f x) -- a --> 0"
   446 by (rule bounded_linear.LIM_zero [OF bounded_linear_right])
   447 
   448 lemma (in bounded_bilinear) prod_diff_prod:
   449   "(x ** y - a ** b) = (x - a) ** (y - b) + (x - a) ** b + a ** (y - b)"
   450 by (simp add: diff_left diff_right)
   451 
   452 lemma (in bounded_bilinear) LIM:
   453   "\<lbrakk>f -- a --> L; g -- a --> M\<rbrakk> \<Longrightarrow> (\<lambda>x. f x ** g x) -- a --> L ** M"
   454 apply (drule LIM_zero)
   455 apply (drule LIM_zero)
   456 apply (rule LIM_zero_cancel)
   457 apply (subst prod_diff_prod)
   458 apply (rule LIM_add_zero)
   459 apply (rule LIM_add_zero)
   460 apply (erule (1) LIM_prod_zero)
   461 apply (erule LIM_left_zero)
   462 apply (erule LIM_right_zero)
   463 done
   464 
   465 interpretation bounded_bilinear_mult:
   466   bounded_bilinear ["op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra"]
   467 apply (rule bounded_bilinear.intro)
   468 apply (rule left_distrib)
   469 apply (rule right_distrib)
   470 apply (rule mult_scaleR_left)
   471 apply (rule mult_scaleR_right)
   472 apply (rule_tac x="1" in exI)
   473 apply (simp add: norm_mult_ineq)
   474 done
   475 
   476 interpretation bounded_bilinear_scaleR:
   477   bounded_bilinear ["scaleR"]
   478 apply (rule bounded_bilinear.intro)
   479 apply (rule scaleR_left_distrib)
   480 apply (rule scaleR_right_distrib)
   481 apply (simp add: real_scaleR_def)
   482 apply (rule scaleR_left_commute)
   483 apply (rule_tac x="1" in exI)
   484 apply (simp add: norm_scaleR)
   485 done
   486 
   487 lemmas LIM_mult = bounded_bilinear_mult.LIM
   488 
   489 lemmas LIM_mult_zero = bounded_bilinear_mult.LIM_prod_zero
   490 
   491 lemmas LIM_mult_left_zero = bounded_bilinear_mult.LIM_left_zero
   492 
   493 lemmas LIM_mult_right_zero = bounded_bilinear_mult.LIM_right_zero
   494 
   495 lemmas LIM_scaleR = bounded_bilinear_scaleR.LIM
   496 
   497 subsubsection {* Purely nonstandard proofs *}
   498 
   499 lemma NSLIM_I:
   500   "(\<And>x. \<lbrakk>x \<noteq> star_of a; x \<approx> star_of a\<rbrakk> \<Longrightarrow> starfun f x \<approx> star_of L)
   501    \<Longrightarrow> f -- a --NS> L"
   502 by (simp add: NSLIM_def)
   503 
   504 lemma NSLIM_D:
   505   "\<lbrakk>f -- a --NS> L; x \<noteq> star_of a; x \<approx> star_of a\<rbrakk>
   506    \<Longrightarrow> starfun f x \<approx> star_of L"
   507 by (simp add: NSLIM_def)
   508 
   509 text{*Proving properties of limits using nonstandard definition.
   510       The properties hold for standard limits as well!*}
   511 
   512 lemma NSLIM_mult:
   513   fixes l m :: "'a::real_normed_algebra"
   514   shows "[| f -- x --NS> l; g -- x --NS> m |]
   515       ==> (%x. f(x) * g(x)) -- x --NS> (l * m)"
   516 by (auto simp add: NSLIM_def intro!: approx_mult_HFinite)
   517 
   518 lemma starfun_scaleR [simp]:
   519   "starfun (\<lambda>x. f x *# g x) = (\<lambda>x. scaleHR (starfun f x) (starfun g x))"
   520 by transfer (rule refl)
   521 
   522 lemma NSLIM_scaleR:
   523   "[| f -- x --NS> l; g -- x --NS> m |]
   524       ==> (%x. f(x) *# g(x)) -- x --NS> (l *# m)"
   525 by (auto simp add: NSLIM_def intro!: approx_scaleR_HFinite)
   526 
   527 lemma NSLIM_add:
   528      "[| f -- x --NS> l; g -- x --NS> m |]
   529       ==> (%x. f(x) + g(x)) -- x --NS> (l + m)"
   530 by (auto simp add: NSLIM_def intro!: approx_add)
   531 
   532 lemma NSLIM_const [simp]: "(%x. k) -- x --NS> k"
   533 by (simp add: NSLIM_def)
   534 
   535 lemma NSLIM_minus: "f -- a --NS> L ==> (%x. -f(x)) -- a --NS> -L"
   536 by (simp add: NSLIM_def)
   537 
   538 lemma NSLIM_add_minus: "[| f -- x --NS> l; g -- x --NS> m |] ==> (%x. f(x) + -g(x)) -- x --NS> (l + -m)"
   539 by (simp only: NSLIM_add NSLIM_minus)
   540 
   541 lemma NSLIM_inverse:
   542   fixes L :: "'a::real_normed_div_algebra"
   543   shows "[| f -- a --NS> L;  L \<noteq> 0 |]
   544       ==> (%x. inverse(f(x))) -- a --NS> (inverse L)"
   545 apply (simp add: NSLIM_def, clarify)
   546 apply (drule spec)
   547 apply (auto simp add: star_of_approx_inverse)
   548 done
   549 
   550 lemma NSLIM_zero:
   551   assumes f: "f -- a --NS> l" shows "(%x. f(x) + -l) -- a --NS> 0"
   552 proof -
   553   have "(\<lambda>x. f x + - l) -- a --NS> l + -l"
   554     by (rule NSLIM_add_minus [OF f NSLIM_const])
   555   thus ?thesis by simp
   556 qed
   557 
   558 lemma NSLIM_zero_cancel: "(%x. f(x) - l) -- x --NS> 0 ==> f -- x --NS> l"
   559 apply (drule_tac g = "%x. l" and m = l in NSLIM_add)
   560 apply (auto simp add: diff_minus add_assoc)
   561 done
   562 
   563 lemma NSLIM_const_not_eq:
   564   fixes a :: real (* TODO: generalize to real_normed_div_algebra *)
   565   shows "k \<noteq> L ==> ~ ((%x. k) -- a --NS> L)"
   566 apply (simp add: NSLIM_def)
   567 apply (rule_tac x="star_of a + epsilon" in exI)
   568 apply (auto intro: Infinitesimal_add_approx_self [THEN approx_sym]
   569             simp add: hypreal_epsilon_not_zero)
   570 done
   571 
   572 lemma NSLIM_not_zero:
   573   fixes a :: real
   574   shows "k \<noteq> 0 ==> ~ ((%x. k) -- a --NS> 0)"
   575 by (rule NSLIM_const_not_eq)
   576 
   577 lemma NSLIM_const_eq:
   578   fixes a :: real
   579   shows "(%x. k) -- a --NS> L ==> k = L"
   580 apply (rule ccontr)
   581 apply (blast dest: NSLIM_const_not_eq)
   582 done
   583 
   584 text{* can actually be proved more easily by unfolding the definition!*}
   585 lemma NSLIM_unique:
   586   fixes a :: real
   587   shows "[| f -- a --NS> L; f -- a --NS> M |] ==> L = M"
   588 apply (drule NSLIM_minus)
   589 apply (drule NSLIM_add, assumption)
   590 apply (auto dest!: NSLIM_const_eq [symmetric])
   591 apply (simp add: diff_def [symmetric])
   592 done
   593 
   594 lemma NSLIM_mult_zero:
   595   fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
   596   shows "[| f -- x --NS> 0; g -- x --NS> 0 |] ==> (%x. f(x)*g(x)) -- x --NS> 0"
   597 by (drule NSLIM_mult, auto)
   598 
   599 lemma NSLIM_self: "(%x. x) -- a --NS> a"
   600 by (simp add: NSLIM_def)
   601 
   602 subsubsection {* Equivalence of @{term LIM} and @{term NSLIM} *}
   603 
   604 lemma LIM_NSLIM:
   605   assumes f: "f -- a --> L" shows "f -- a --NS> L"
   606 proof (rule NSLIM_I)
   607   fix x
   608   assume neq: "x \<noteq> star_of a"
   609   assume approx: "x \<approx> star_of a"
   610   have "starfun f x - star_of L \<in> Infinitesimal"
   611   proof (rule InfinitesimalI2)
   612     fix r::real assume r: "0 < r"
   613     from LIM_D [OF f r]
   614     obtain s where s: "0 < s" and
   615       less_r: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < s\<rbrakk> \<Longrightarrow> norm (f x - L) < r"
   616       by fast
   617     from less_r have less_r':
   618        "\<And>x. \<lbrakk>x \<noteq> star_of a; hnorm (x - star_of a) < star_of s\<rbrakk>
   619         \<Longrightarrow> hnorm (starfun f x - star_of L) < star_of r"
   620       by transfer
   621     from approx have "x - star_of a \<in> Infinitesimal"
   622       by (unfold approx_def)
   623     hence "hnorm (x - star_of a) < star_of s"
   624       using s by (rule InfinitesimalD2)
   625     with neq show "hnorm (starfun f x - star_of L) < star_of r"
   626       by (rule less_r')
   627   qed
   628   thus "starfun f x \<approx> star_of L"
   629     by (unfold approx_def)
   630 qed
   631 
   632 lemma NSLIM_LIM:
   633   assumes f: "f -- a --NS> L" shows "f -- a --> L"
   634 proof (rule LIM_I)
   635   fix r::real assume r: "0 < r"
   636   have "\<exists>s>0. \<forall>x. x \<noteq> star_of a \<and> hnorm (x - star_of a) < s
   637         \<longrightarrow> hnorm (starfun f x - star_of L) < star_of r"
   638   proof (rule exI, safe)
   639     show "0 < epsilon" by (rule hypreal_epsilon_gt_zero)
   640   next
   641     fix x assume neq: "x \<noteq> star_of a"
   642     assume "hnorm (x - star_of a) < epsilon"
   643     with Infinitesimal_epsilon
   644     have "x - star_of a \<in> Infinitesimal"
   645       by (rule hnorm_less_Infinitesimal)
   646     hence "x \<approx> star_of a"
   647       by (unfold approx_def)
   648     with f neq have "starfun f x \<approx> star_of L"
   649       by (rule NSLIM_D)
   650     hence "starfun f x - star_of L \<in> Infinitesimal"
   651       by (unfold approx_def)
   652     thus "hnorm (starfun f x - star_of L) < star_of r"
   653       using r by (rule InfinitesimalD2)
   654   qed
   655   thus "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (f x - L) < r"
   656     by transfer
   657 qed
   658 
   659 theorem LIM_NSLIM_iff: "(f -- x --> L) = (f -- x --NS> L)"
   660 by (blast intro: LIM_NSLIM NSLIM_LIM)
   661 
   662 subsubsection {* Derived theorems about @{term LIM} *}
   663 
   664 lemma LIM_mult2:
   665   fixes l m :: "'a::real_normed_algebra"
   666   shows "[| f -- x --> l; g -- x --> m |]
   667       ==> (%x. f(x) * g(x)) -- x --> (l * m)"
   668 by (simp add: LIM_NSLIM_iff NSLIM_mult)
   669 
   670 lemma LIM_scaleR:
   671   "[| f -- x --> l; g -- x --> m |]
   672       ==> (%x. f(x) *# g(x)) -- x --> (l *# m)"
   673 by (simp add: LIM_NSLIM_iff NSLIM_scaleR)
   674 
   675 lemma LIM_add2:
   676      "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + g(x)) -- x --> (l + m)"
   677 by (simp add: LIM_NSLIM_iff NSLIM_add)
   678 
   679 lemma LIM_const2: "(%x. k) -- x --> k"
   680 by (simp add: LIM_NSLIM_iff)
   681 
   682 lemma LIM_minus2: "f -- a --> L ==> (%x. -f(x)) -- a --> -L"
   683 by (simp add: LIM_NSLIM_iff NSLIM_minus)
   684 
   685 lemma LIM_add_minus2: "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + -g(x)) -- x --> (l + -m)"
   686 by (simp add: LIM_NSLIM_iff NSLIM_add_minus)
   687 
   688 lemma LIM_inverse:
   689   fixes L :: "'a::real_normed_div_algebra"
   690   shows "[| f -- a --> L; L \<noteq> 0 |]
   691       ==> (%x. inverse(f(x))) -- a --> (inverse L)"
   692 by (simp add: LIM_NSLIM_iff NSLIM_inverse)
   693 
   694 lemma LIM_zero2: "f -- a --> l ==> (%x. f(x) + -l) -- a --> 0"
   695 by (simp add: LIM_NSLIM_iff NSLIM_zero)
   696 
   697 lemma LIM_unique2:
   698   fixes a :: real
   699   shows "[| f -- a --> L; f -- a --> M |] ==> L = M"
   700 by (simp add: LIM_NSLIM_iff NSLIM_unique)
   701 
   702 (* we can use the corresponding thm LIM_mult2 *)
   703 (* for standard definition of limit           *)
   704 
   705 lemma LIM_mult_zero2:
   706   fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
   707   shows "[| f -- x --> 0; g -- x --> 0 |] ==> (%x. f(x)*g(x)) -- x --> 0"
   708 by (drule LIM_mult2, auto)
   709 
   710 
   711 subsection {* Continuity *}
   712 
   713 subsubsection {* Purely standard proofs *}
   714 
   715 lemma LIM_isCont_iff: "(f -- a --> f a) = ((\<lambda>h. f (a + h)) -- 0 --> f a)"
   716 by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel])
   717 
   718 lemma isCont_iff: "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x"
   719 by (simp add: isCont_def LIM_isCont_iff)
   720 
   721 lemma isCont_Id: "isCont (\<lambda>x. x) a"
   722   unfolding isCont_def by (rule LIM_self)
   723 
   724 lemma isCont_const [simp]: "isCont (%x. k) a"
   725   unfolding isCont_def by (rule LIM_const)
   726 
   727 lemma isCont_add: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"
   728   unfolding isCont_def by (rule LIM_add)
   729 
   730 lemma isCont_minus: "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a"
   731   unfolding isCont_def by (rule LIM_minus)
   732 
   733 lemma isCont_diff: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a"
   734   unfolding isCont_def by (rule LIM_diff)
   735 
   736 lemma isCont_mult:
   737   fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
   738   shows "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) * g(x)) a"
   739   unfolding isCont_def by (rule LIM_mult)
   740 
   741 lemma isCont_inverse:
   742   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_div_algebra"
   743   shows "[| isCont f x; f x \<noteq> 0 |] ==> isCont (%x. inverse (f x)) x"
   744   unfolding isCont_def by (rule LIM_inverse)
   745 
   746 lemma isCont_LIM_compose:
   747   "\<lbrakk>isCont g l; f -- a --> l\<rbrakk> \<Longrightarrow> (\<lambda>x. g (f x)) -- a --> g l"
   748   unfolding isCont_def by (rule LIM_compose)
   749 
   750 lemma isCont_o2: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. g (f x)) a"
   751   unfolding isCont_def by (rule LIM_compose)
   752 
   753 lemma isCont_o: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (g o f) a"
   754   unfolding o_def by (rule isCont_o2)
   755 
   756 lemma (in bounded_linear) isCont: "isCont f a"
   757   unfolding isCont_def by (rule cont)
   758 
   759 lemma (in bounded_bilinear) isCont:
   760   "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
   761   unfolding isCont_def by (rule LIM)
   762 
   763 lemmas isCont_scaleR = bounded_bilinear_scaleR.isCont
   764 
   765 subsubsection {* Nonstandard proofs *}
   766 
   767 lemma isNSContD: "[| isNSCont f a; y \<approx> hypreal_of_real a |] ==> ( *f* f) y \<approx> hypreal_of_real (f a)"
   768 by (simp add: isNSCont_def)
   769 
   770 lemma isNSCont_NSLIM: "isNSCont f a ==> f -- a --NS> (f a) "
   771 by (simp add: isNSCont_def NSLIM_def)
   772 
   773 lemma NSLIM_isNSCont: "f -- a --NS> (f a) ==> isNSCont f a"
   774 apply (simp add: isNSCont_def NSLIM_def, auto)
   775 apply (case_tac "y = star_of a", auto)
   776 done
   777 
   778 text{*NS continuity can be defined using NS Limit in
   779     similar fashion to standard def of continuity*}
   780 lemma isNSCont_NSLIM_iff: "(isNSCont f a) = (f -- a --NS> (f a))"
   781 by (blast intro: isNSCont_NSLIM NSLIM_isNSCont)
   782 
   783 text{*Hence, NS continuity can be given
   784   in terms of standard limit*}
   785 lemma isNSCont_LIM_iff: "(isNSCont f a) = (f -- a --> (f a))"
   786 by (simp add: LIM_NSLIM_iff isNSCont_NSLIM_iff)
   787 
   788 text{*Moreover, it's trivial now that NS continuity
   789   is equivalent to standard continuity*}
   790 lemma isNSCont_isCont_iff: "(isNSCont f a) = (isCont f a)"
   791 apply (simp add: isCont_def)
   792 apply (rule isNSCont_LIM_iff)
   793 done
   794 
   795 text{*Standard continuity ==> NS continuity*}
   796 lemma isCont_isNSCont: "isCont f a ==> isNSCont f a"
   797 by (erule isNSCont_isCont_iff [THEN iffD2])
   798 
   799 text{*NS continuity ==> Standard continuity*}
   800 lemma isNSCont_isCont: "isNSCont f a ==> isCont f a"
   801 by (erule isNSCont_isCont_iff [THEN iffD1])
   802 
   803 text{*Alternative definition of continuity*}
   804 (* Prove equivalence between NS limits - *)
   805 (* seems easier than using standard def  *)
   806 lemma NSLIM_h_iff: "(f -- a --NS> L) = ((%h. f(a + h)) -- 0 --NS> L)"
   807 apply (simp add: NSLIM_def, auto)
   808 apply (drule_tac x = "star_of a + x" in spec)
   809 apply (drule_tac [2] x = "- star_of a + x" in spec, safe, simp)
   810 apply (erule mem_infmal_iff [THEN iffD2, THEN Infinitesimal_add_approx_self [THEN approx_sym]])
   811 apply (erule_tac [3] approx_minus_iff2 [THEN iffD1])
   812  prefer 2 apply (simp add: add_commute diff_def [symmetric])
   813 apply (rule_tac x = x in star_cases)
   814 apply (rule_tac [2] x = x in star_cases)
   815 apply (auto simp add: starfun star_of_def star_n_minus star_n_add add_assoc approx_refl star_n_zero_num)
   816 done
   817 
   818 lemma NSLIM_isCont_iff: "(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)"
   819 by (rule NSLIM_h_iff)
   820 
   821 lemma isNSCont_minus: "isNSCont f a ==> isNSCont (%x. - f x) a"
   822 by (simp add: isNSCont_def)
   823 
   824 lemma isNSCont_inverse:
   825   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_div_algebra"
   826   shows "[| isNSCont f x; f x \<noteq> 0 |] ==> isNSCont (%x. inverse (f x)) x"
   827 by (auto intro: isCont_inverse simp add: isNSCont_isCont_iff)
   828 
   829 lemma isNSCont_const [simp]: "isNSCont (%x. k) a"
   830 by (simp add: isNSCont_def)
   831 
   832 lemma isNSCont_abs [simp]: "isNSCont abs (a::real)"
   833 apply (simp add: isNSCont_def)
   834 apply (auto intro: approx_hrabs simp add: hypreal_of_real_hrabs [symmetric] starfun_rabs_hrabs)
   835 done
   836 
   837 lemma isCont_abs [simp]: "isCont abs (a::real)"
   838 by (auto simp add: isNSCont_isCont_iff [symmetric])
   839 
   840 
   841 (****************************************************************
   842 (%* Leave as commented until I add topology theory or remove? *%)
   843 (%*------------------------------------------------------------
   844   Elementary topology proof for a characterisation of
   845   continuity now: a function f is continuous if and only
   846   if the inverse image, {x. f(x) \<in> A}, of any open set A
   847   is always an open set
   848  ------------------------------------------------------------*%)
   849 Goal "[| isNSopen A; \<forall>x. isNSCont f x |]
   850                ==> isNSopen {x. f x \<in> A}"
   851 by (auto_tac (claset(),simpset() addsimps [isNSopen_iff1]));
   852 by (dtac (mem_monad_approx RS approx_sym);
   853 by (dres_inst_tac [("x","a")] spec 1);
   854 by (dtac isNSContD 1 THEN assume_tac 1)
   855 by (dtac bspec 1 THEN assume_tac 1)
   856 by (dres_inst_tac [("x","( *f* f) x")] approx_mem_monad2 1);
   857 by (blast_tac (claset() addIs [starfun_mem_starset]);
   858 qed "isNSCont_isNSopen";
   859 
   860 Goalw [isNSCont_def]
   861           "\<forall>A. isNSopen A --> isNSopen {x. f x \<in> A} \
   862 \              ==> isNSCont f x";
   863 by (auto_tac (claset() addSIs [(mem_infmal_iff RS iffD1) RS
   864      (approx_minus_iff RS iffD2)],simpset() addsimps
   865       [Infinitesimal_def,SReal_iff]));
   866 by (dres_inst_tac [("x","{z. abs(z + -f(x)) < ya}")] spec 1);
   867 by (etac (isNSopen_open_interval RSN (2,impE));
   868 by (auto_tac (claset(),simpset() addsimps [isNSopen_def,isNSnbhd_def]));
   869 by (dres_inst_tac [("x","x")] spec 1);
   870 by (auto_tac (claset() addDs [approx_sym RS approx_mem_monad],
   871     simpset() addsimps [hypreal_of_real_zero RS sym,STAR_starfun_rabs_add_minus]));
   872 qed "isNSopen_isNSCont";
   873 
   874 Goal "(\<forall>x. isNSCont f x) = \
   875 \     (\<forall>A. isNSopen A --> isNSopen {x. f(x) \<in> A})";
   876 by (blast_tac (claset() addIs [isNSCont_isNSopen,
   877     isNSopen_isNSCont]);
   878 qed "isNSCont_isNSopen_iff";
   879 
   880 (%*------- Standard version of same theorem --------*%)
   881 Goal "(\<forall>x. isCont f x) = \
   882 \         (\<forall>A. isopen A --> isopen {x. f(x) \<in> A})";
   883 by (auto_tac (claset() addSIs [isNSCont_isNSopen_iff],
   884               simpset() addsimps [isNSopen_isopen_iff RS sym,
   885               isNSCont_isCont_iff RS sym]));
   886 qed "isCont_isopen_iff";
   887 *******************************************************************)
   888 
   889 subsection {* Uniform Continuity *}
   890 
   891 lemma isNSUContD: "[| isNSUCont f; x \<approx> y|] ==> ( *f* f) x \<approx> ( *f* f) y"
   892 by (simp add: isNSUCont_def)
   893 
   894 lemma isUCont_isCont: "isUCont f ==> isCont f x"
   895 by (simp add: isUCont_def isCont_def LIM_def, meson)
   896 
   897 lemma isUCont_isNSUCont:
   898   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   899   assumes f: "isUCont f" shows "isNSUCont f"
   900 proof (unfold isNSUCont_def, safe)
   901   fix x y :: "'a star"
   902   assume approx: "x \<approx> y"
   903   have "starfun f x - starfun f y \<in> Infinitesimal"
   904   proof (rule InfinitesimalI2)
   905     fix r::real assume r: "0 < r"
   906     with f obtain s where s: "0 < s" and
   907       less_r: "\<And>x y. norm (x - y) < s \<Longrightarrow> norm (f x - f y) < r"
   908       by (auto simp add: isUCont_def)
   909     from less_r have less_r':
   910        "\<And>x y. hnorm (x - y) < star_of s
   911         \<Longrightarrow> hnorm (starfun f x - starfun f y) < star_of r"
   912       by transfer
   913     from approx have "x - y \<in> Infinitesimal"
   914       by (unfold approx_def)
   915     hence "hnorm (x - y) < star_of s"
   916       using s by (rule InfinitesimalD2)
   917     thus "hnorm (starfun f x - starfun f y) < star_of r"
   918       by (rule less_r')
   919   qed
   920   thus "starfun f x \<approx> starfun f y"
   921     by (unfold approx_def)
   922 qed
   923 
   924 lemma isNSUCont_isUCont:
   925   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   926   assumes f: "isNSUCont f" shows "isUCont f"
   927 proof (unfold isUCont_def, safe)
   928   fix r::real assume r: "0 < r"
   929   have "\<exists>s>0. \<forall>x y. hnorm (x - y) < s
   930         \<longrightarrow> hnorm (starfun f x - starfun f y) < star_of r"
   931   proof (rule exI, safe)
   932     show "0 < epsilon" by (rule hypreal_epsilon_gt_zero)
   933   next
   934     fix x y :: "'a star"
   935     assume "hnorm (x - y) < epsilon"
   936     with Infinitesimal_epsilon
   937     have "x - y \<in> Infinitesimal"
   938       by (rule hnorm_less_Infinitesimal)
   939     hence "x \<approx> y"
   940       by (unfold approx_def)
   941     with f have "starfun f x \<approx> starfun f y"
   942       by (simp add: isNSUCont_def)
   943     hence "starfun f x - starfun f y \<in> Infinitesimal"
   944       by (unfold approx_def)
   945     thus "hnorm (starfun f x - starfun f y) < star_of r"
   946       using r by (rule InfinitesimalD2)
   947   qed
   948   thus "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r"
   949     by transfer
   950 qed
   951 
   952 subsection {* Relation of LIM and LIMSEQ *}
   953 
   954 lemma LIMSEQ_SEQ_conv1:
   955   fixes a :: "'a::real_normed_vector"
   956   assumes X: "X -- a --> L"
   957   shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
   958 proof (safe intro!: LIMSEQ_I)
   959   fix S :: "nat \<Rightarrow> 'a"
   960   fix r :: real
   961   assume rgz: "0 < r"
   962   assume as: "\<forall>n. S n \<noteq> a"
   963   assume S: "S ----> a"
   964   from LIM_D [OF X rgz] obtain s
   965     where sgz: "0 < s"
   966     and aux: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < s\<rbrakk> \<Longrightarrow> norm (X x - L) < r"
   967     by fast
   968   from LIMSEQ_D [OF S sgz]
   969   obtain no where "\<forall>n\<ge>no. norm (S n - a) < s" by blast
   970   hence "\<forall>n\<ge>no. norm (X (S n) - L) < r" by (simp add: aux as)
   971   thus "\<exists>no. \<forall>n\<ge>no. norm (X (S n) - L) < r" ..
   972 qed
   973 
   974 lemma LIMSEQ_SEQ_conv2:
   975   fixes a :: real
   976   assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
   977   shows "X -- a --> L"
   978 proof (rule ccontr)
   979   assume "\<not> (X -- a --> L)"
   980   hence "\<not> (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x - a) < s --> norm (X x - L) < r)" by (unfold LIM_def)
   981   hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. \<not>(x \<noteq> a \<and> \<bar>x - a\<bar> < s --> norm (X x - L) < r)" by simp
   982   hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x - a\<bar> < s \<and> norm (X x - L) \<ge> r)" by (simp add: linorder_not_less)
   983   then obtain r where rdef: "r > 0 \<and> (\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x - a\<bar> < s \<and> norm (X x - L) \<ge> r))" by auto
   984 
   985   let ?F = "\<lambda>n::nat. SOME x. x\<noteq>a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> norm (X x - L) \<ge> r"
   986   have "\<And>n. \<exists>x. x\<noteq>a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> norm (X x - L) \<ge> r"
   987     using rdef by simp
   988   hence F: "\<And>n. ?F n \<noteq> a \<and> \<bar>?F n - a\<bar> < inverse (real (Suc n)) \<and> norm (X (?F n) - L) \<ge> r"
   989     by (rule someI_ex)
   990   hence F1: "\<And>n. ?F n \<noteq> a"
   991     and F2: "\<And>n. \<bar>?F n - a\<bar> < inverse (real (Suc n))"
   992     and F3: "\<And>n. norm (X (?F n) - L) \<ge> r"
   993     by fast+
   994 
   995   have "?F ----> a"
   996   proof (rule LIMSEQ_I, unfold real_norm_def)
   997       fix e::real
   998       assume "0 < e"
   999         (* choose no such that inverse (real (Suc n)) < e *)
  1000       have "\<exists>no. inverse (real (Suc no)) < e" by (rule reals_Archimedean)
  1001       then obtain m where nodef: "inverse (real (Suc m)) < e" by auto
  1002       show "\<exists>no. \<forall>n. no \<le> n --> \<bar>?F n - a\<bar> < e"
  1003       proof (intro exI allI impI)
  1004         fix n
  1005         assume mlen: "m \<le> n"
  1006         have "\<bar>?F n - a\<bar> < inverse (real (Suc n))"
  1007           by (rule F2)
  1008         also have "inverse (real (Suc n)) \<le> inverse (real (Suc m))"
  1009           by auto
  1010         also from nodef have
  1011           "inverse (real (Suc m)) < e" .
  1012         finally show "\<bar>?F n - a\<bar> < e" .
  1013       qed
  1014   qed
  1015   
  1016   moreover have "\<forall>n. ?F n \<noteq> a"
  1017     by (rule allI) (rule F1)
  1018 
  1019   moreover from prems have "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L" by simp
  1020   ultimately have "(\<lambda>n. X (?F n)) ----> L" by simp
  1021   
  1022   moreover have "\<not> ((\<lambda>n. X (?F n)) ----> L)"
  1023   proof -
  1024     {
  1025       fix no::nat
  1026       obtain n where "n = no + 1" by simp
  1027       then have nolen: "no \<le> n" by simp
  1028         (* We prove this by showing that for any m there is an n\<ge>m such that |X (?F n) - L| \<ge> r *)
  1029       have "norm (X (?F n) - L) \<ge> r"
  1030         by (rule F3)
  1031       with nolen have "\<exists>n. no \<le> n \<and> norm (X (?F n) - L) \<ge> r" by fast
  1032     }
  1033     then have "(\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n) - L) \<ge> r)" by simp
  1034     with rdef have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n) - L) \<ge> e)" by auto
  1035     thus ?thesis by (unfold LIMSEQ_def, auto simp add: linorder_not_less)
  1036   qed
  1037   ultimately show False by simp
  1038 qed
  1039 
  1040 lemma LIMSEQ_SEQ_conv:
  1041   "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::real) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) =
  1042    (X -- a --> L)"
  1043 proof
  1044   assume "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
  1045   show "X -- a --> L" by (rule LIMSEQ_SEQ_conv2)
  1046 next
  1047   assume "(X -- a --> L)"
  1048   show "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L" by (rule LIMSEQ_SEQ_conv1)
  1049 qed
  1050 
  1051 end