src/HOL/Nonstandard_Analysis/HLim.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 64604 2bf8cfc98c4d
child 66827 c94531b5007d
permissions -rw-r--r--
executable domain membership checks
     1 (*  Title:      HOL/Nonstandard_Analysis/HLim.thy
     2     Author:     Jacques D. Fleuriot, University of Cambridge
     3     Author:     Lawrence C Paulson
     4 *)
     5 
     6 section \<open>Limits and Continuity (Nonstandard)\<close>
     7 
     8 theory HLim
     9   imports Star
    10   abbrevs "--->" = "\<midarrow>\<rightarrow>\<^sub>N\<^sub>S"
    11 begin
    12 
    13 text \<open>Nonstandard Definitions.\<close>
    14 
    15 definition NSLIM :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
    16     ("((_)/ \<midarrow>(_)/\<rightarrow>\<^sub>N\<^sub>S (_))" [60, 0, 60] 60)
    17   where "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L \<longleftrightarrow> (\<forall>x. x \<noteq> star_of a \<and> x \<approx> star_of a \<longrightarrow> ( *f* f) x \<approx> star_of L)"
    18 
    19 definition isNSCont :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> bool"
    20   where  \<comment> \<open>NS definition dispenses with limit notions\<close>
    21     "isNSCont f a \<longleftrightarrow> (\<forall>y. y \<approx> star_of a \<longrightarrow> ( *f* f) y \<approx> star_of (f a))"
    22 
    23 definition isNSUCont :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> bool"
    24   where "isNSUCont f \<longleftrightarrow> (\<forall>x y. x \<approx> y \<longrightarrow> ( *f* f) x \<approx> ( *f* f) y)"
    25 
    26 
    27 subsection \<open>Limits of Functions\<close>
    28 
    29 lemma NSLIM_I: "(\<And>x. x \<noteq> star_of a \<Longrightarrow> x \<approx> star_of a \<Longrightarrow> starfun f x \<approx> star_of L) \<Longrightarrow> f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L"
    30   by (simp add: NSLIM_def)
    31 
    32 lemma NSLIM_D: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> x \<noteq> star_of a \<Longrightarrow> x \<approx> star_of a \<Longrightarrow> starfun f x \<approx> star_of L"
    33   by (simp add: NSLIM_def)
    34 
    35 text \<open>Proving properties of limits using nonstandard definition.
    36   The properties hold for standard limits as well!\<close>
    37 
    38 lemma NSLIM_mult: "f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l \<Longrightarrow> g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S m \<Longrightarrow> (\<lambda>x. f x * g x) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S (l * m)"
    39   for l m :: "'a::real_normed_algebra"
    40   by (auto simp add: NSLIM_def intro!: approx_mult_HFinite)
    41 
    42 lemma starfun_scaleR [simp]: "starfun (\<lambda>x. f x *\<^sub>R g x) = (\<lambda>x. scaleHR (starfun f x) (starfun g x))"
    43   by transfer (rule refl)
    44 
    45 lemma NSLIM_scaleR: "f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l \<Longrightarrow> g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S m \<Longrightarrow> (\<lambda>x. f x *\<^sub>R g x) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S (l *\<^sub>R m)"
    46   by (auto simp add: NSLIM_def intro!: approx_scaleR_HFinite)
    47 
    48 lemma NSLIM_add: "f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l \<Longrightarrow> g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S m \<Longrightarrow> (\<lambda>x. f x + g x) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S (l + m)"
    49   by (auto simp add: NSLIM_def intro!: approx_add)
    50 
    51 lemma NSLIM_const [simp]: "(\<lambda>x. k) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S k"
    52   by (simp add: NSLIM_def)
    53 
    54 lemma NSLIM_minus: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> (\<lambda>x. - f x) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S -L"
    55   by (simp add: NSLIM_def)
    56 
    57 lemma NSLIM_diff: "f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l \<Longrightarrow> g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S m \<Longrightarrow> (\<lambda>x. f x - g x) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S (l - m)"
    58   by (simp only: NSLIM_add NSLIM_minus diff_conv_add_uminus)
    59 
    60 lemma NSLIM_add_minus: "f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l \<Longrightarrow> g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S m \<Longrightarrow> (\<lambda>x. f x + - g x) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S (l + -m)"
    61   by (simp only: NSLIM_add NSLIM_minus)
    62 
    63 lemma NSLIM_inverse: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> L \<noteq> 0 \<Longrightarrow> (\<lambda>x. inverse (f x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S (inverse L)"
    64   for L :: "'a::real_normed_div_algebra"
    65   apply (simp add: NSLIM_def, clarify)
    66   apply (drule spec)
    67   apply (auto simp add: star_of_approx_inverse)
    68   done
    69 
    70 lemma NSLIM_zero:
    71   assumes f: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S l"
    72   shows "(\<lambda>x. f(x) - l) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S 0"
    73 proof -
    74   have "(\<lambda>x. f x - l) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S l - l"
    75     by (rule NSLIM_diff [OF f NSLIM_const])
    76   then show ?thesis by simp
    77 qed
    78 
    79 lemma NSLIM_zero_cancel: "(\<lambda>x. f x - l) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0 \<Longrightarrow> f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l"
    80   apply (drule_tac g = "\<lambda>x. l" and m = l in NSLIM_add)
    81    apply (auto simp add: add.assoc)
    82   done
    83 
    84 lemma NSLIM_const_not_eq: "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L"
    85   for a :: "'a::real_normed_algebra_1"
    86   apply (simp add: NSLIM_def)
    87   apply (rule_tac x="star_of a + of_hypreal \<epsilon>" in exI)
    88   apply (simp add: hypreal_epsilon_not_zero approx_def)
    89   done
    90 
    91 lemma NSLIM_not_zero: "k \<noteq> 0 \<Longrightarrow> \<not> (\<lambda>x. k) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S 0"
    92   for a :: "'a::real_normed_algebra_1"
    93   by (rule NSLIM_const_not_eq)
    94 
    95 lemma NSLIM_const_eq: "(\<lambda>x. k) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> k = L"
    96   for a :: "'a::real_normed_algebra_1"
    97   by (rule ccontr) (blast dest: NSLIM_const_not_eq)
    98 
    99 lemma NSLIM_unique: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S M \<Longrightarrow> L = M"
   100   for a :: "'a::real_normed_algebra_1"
   101   by (drule (1) NSLIM_diff) (auto dest!: NSLIM_const_eq)
   102 
   103 lemma NSLIM_mult_zero: "f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0 \<Longrightarrow> g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0 \<Longrightarrow> (\<lambda>x. f x * g x) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0"
   104   for f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
   105   by (drule NSLIM_mult) auto
   106 
   107 lemma NSLIM_self: "(\<lambda>x. x) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S a"
   108   by (simp add: NSLIM_def)
   109 
   110 
   111 subsubsection \<open>Equivalence of @{term filterlim} and @{term NSLIM}\<close>
   112 
   113 lemma LIM_NSLIM:
   114   assumes f: "f \<midarrow>a\<rightarrow> L"
   115   shows "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L"
   116 proof (rule NSLIM_I)
   117   fix x
   118   assume neq: "x \<noteq> star_of a"
   119   assume approx: "x \<approx> star_of a"
   120   have "starfun f x - star_of L \<in> Infinitesimal"
   121   proof (rule InfinitesimalI2)
   122     fix r :: real
   123     assume r: "0 < r"
   124     from LIM_D [OF f r] obtain s
   125       where s: "0 < s" and less_r: "\<And>x. x \<noteq> a \<Longrightarrow> norm (x - a) < s \<Longrightarrow> norm (f x - L) < r"
   126       by fast
   127     from less_r have less_r':
   128       "\<And>x. x \<noteq> star_of a \<Longrightarrow> hnorm (x - star_of a) < star_of s \<Longrightarrow>
   129         hnorm (starfun f x - star_of L) < star_of r"
   130       by transfer
   131     from approx have "x - star_of a \<in> Infinitesimal"
   132       by (simp only: approx_def)
   133     then have "hnorm (x - star_of a) < star_of s"
   134       using s by (rule InfinitesimalD2)
   135     with neq show "hnorm (starfun f x - star_of L) < star_of r"
   136       by (rule less_r')
   137   qed
   138   then show "starfun f x \<approx> star_of L"
   139     by (unfold approx_def)
   140 qed
   141 
   142 lemma NSLIM_LIM:
   143   assumes f: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L"
   144   shows "f \<midarrow>a\<rightarrow> L"
   145 proof (rule LIM_I)
   146   fix r :: real
   147   assume r: "0 < r"
   148   have "\<exists>s>0. \<forall>x. x \<noteq> star_of a \<and> hnorm (x - star_of a) < s \<longrightarrow>
   149     hnorm (starfun f x - star_of L) < star_of r"
   150   proof (rule exI, safe)
   151     show "0 < \<epsilon>"
   152       by (rule hypreal_epsilon_gt_zero)
   153   next
   154     fix x
   155     assume neq: "x \<noteq> star_of a"
   156     assume "hnorm (x - star_of a) < \<epsilon>"
   157     with Infinitesimal_epsilon have "x - star_of a \<in> Infinitesimal"
   158       by (rule hnorm_less_Infinitesimal)
   159     then have "x \<approx> star_of a"
   160       by (unfold approx_def)
   161     with f neq have "starfun f x \<approx> star_of L"
   162       by (rule NSLIM_D)
   163     then have "starfun f x - star_of L \<in> Infinitesimal"
   164       by (unfold approx_def)
   165     then show "hnorm (starfun f x - star_of L) < star_of r"
   166       using r by (rule InfinitesimalD2)
   167   qed
   168   then show "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (f x - L) < r"
   169     by transfer
   170 qed
   171 
   172 theorem LIM_NSLIM_iff: "f \<midarrow>x\<rightarrow> L \<longleftrightarrow> f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S L"
   173   by (blast intro: LIM_NSLIM NSLIM_LIM)
   174 
   175 
   176 subsection \<open>Continuity\<close>
   177 
   178 lemma isNSContD: "isNSCont f a \<Longrightarrow> y \<approx> star_of a \<Longrightarrow> ( *f* f) y \<approx> star_of (f a)"
   179   by (simp add: isNSCont_def)
   180 
   181 lemma isNSCont_NSLIM: "isNSCont f a \<Longrightarrow> f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S (f a)"
   182   by (simp add: isNSCont_def NSLIM_def)
   183 
   184 lemma NSLIM_isNSCont: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S (f a) \<Longrightarrow> isNSCont f a"
   185   apply (auto simp add: isNSCont_def NSLIM_def)
   186   apply (case_tac "y = star_of a")
   187    apply auto
   188   done
   189 
   190 text \<open>NS continuity can be defined using NS Limit in
   191   similar fashion to standard definition of continuity.\<close>
   192 lemma isNSCont_NSLIM_iff: "isNSCont f a \<longleftrightarrow> f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S (f a)"
   193   by (blast intro: isNSCont_NSLIM NSLIM_isNSCont)
   194 
   195 text \<open>Hence, NS continuity can be given in terms of standard limit.\<close>
   196 lemma isNSCont_LIM_iff: "(isNSCont f a) = (f \<midarrow>a\<rightarrow> (f a))"
   197   by (simp add: LIM_NSLIM_iff isNSCont_NSLIM_iff)
   198 
   199 text \<open>Moreover, it's trivial now that NS continuity
   200   is equivalent to standard continuity.\<close>
   201 lemma isNSCont_isCont_iff: "isNSCont f a \<longleftrightarrow> isCont f a"
   202   by (simp add: isCont_def) (rule isNSCont_LIM_iff)
   203 
   204 text \<open>Standard continuity \<open>\<Longrightarrow>\<close> NS continuity.\<close>
   205 lemma isCont_isNSCont: "isCont f a \<Longrightarrow> isNSCont f a"
   206   by (erule isNSCont_isCont_iff [THEN iffD2])
   207 
   208 text \<open>NS continuity \<open>\<Longrightarrow>\<close> Standard continuity.\<close>
   209 lemma isNSCont_isCont: "isNSCont f a \<Longrightarrow> isCont f a"
   210   by (erule isNSCont_isCont_iff [THEN iffD1])
   211 
   212 
   213 text \<open>Alternative definition of continuity.\<close>
   214 
   215 text \<open>Prove equivalence between NS limits --
   216   seems easier than using standard definition.\<close>
   217 lemma NSLIM_h_iff: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L \<longleftrightarrow> (\<lambda>h. f (a + h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S L"
   218   apply (simp add: NSLIM_def, auto)
   219    apply (drule_tac x = "star_of a + x" in spec)
   220    apply (drule_tac [2] x = "- star_of a + x" in spec, safe, simp)
   221       apply (erule mem_infmal_iff [THEN iffD2, THEN Infinitesimal_add_approx_self [THEN approx_sym]])
   222      apply (erule_tac [3] approx_minus_iff2 [THEN iffD1])
   223     prefer 2 apply (simp add: add.commute)
   224    apply (rule_tac x = x in star_cases)
   225    apply (rule_tac [2] x = x in star_cases)
   226    apply (auto simp add: starfun star_of_def star_n_minus star_n_add add.assoc star_n_zero_num)
   227   done
   228 
   229 lemma NSLIM_isCont_iff: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S f a \<longleftrightarrow> (\<lambda>h. f (a + h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S f a"
   230   by (fact NSLIM_h_iff)
   231 
   232 lemma isNSCont_minus: "isNSCont f a \<Longrightarrow> isNSCont (\<lambda>x. - f x) a"
   233   by (simp add: isNSCont_def)
   234 
   235 lemma isNSCont_inverse: "isNSCont f x \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> isNSCont (\<lambda>x. inverse (f x)) x"
   236   for f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_div_algebra"
   237   by (auto intro: isCont_inverse simp add: isNSCont_isCont_iff)
   238 
   239 lemma isNSCont_const [simp]: "isNSCont (\<lambda>x. k) a"
   240   by (simp add: isNSCont_def)
   241 
   242 lemma isNSCont_abs [simp]: "isNSCont abs a"
   243   for a :: real
   244   by (auto simp: isNSCont_def intro: approx_hrabs simp: starfun_rabs_hrabs)
   245 
   246 
   247 subsection \<open>Uniform Continuity\<close>
   248 
   249 lemma isNSUContD: "isNSUCont f \<Longrightarrow> x \<approx> y \<Longrightarrow> ( *f* f) x \<approx> ( *f* f) y"
   250   by (simp add: isNSUCont_def)
   251 
   252 lemma isUCont_isNSUCont:
   253   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   254   assumes f: "isUCont f"
   255   shows "isNSUCont f"
   256   unfolding isNSUCont_def
   257 proof safe
   258   fix x y :: "'a star"
   259   assume approx: "x \<approx> y"
   260   have "starfun f x - starfun f y \<in> Infinitesimal"
   261   proof (rule InfinitesimalI2)
   262     fix r :: real
   263     assume r: "0 < r"
   264     with f obtain s where s: "0 < s"
   265       and less_r: "\<And>x y. norm (x - y) < s \<Longrightarrow> norm (f x - f y) < r"
   266       by (auto simp add: isUCont_def dist_norm)
   267     from less_r have less_r':
   268       "\<And>x y. hnorm (x - y) < star_of s \<Longrightarrow> hnorm (starfun f x - starfun f y) < star_of r"
   269       by transfer
   270     from approx have "x - y \<in> Infinitesimal"
   271       by (unfold approx_def)
   272     then have "hnorm (x - y) < star_of s"
   273       using s by (rule InfinitesimalD2)
   274     then show "hnorm (starfun f x - starfun f y) < star_of r"
   275       by (rule less_r')
   276   qed
   277   then show "starfun f x \<approx> starfun f y"
   278     by (unfold approx_def)
   279 qed
   280 
   281 lemma isNSUCont_isUCont:
   282   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   283   assumes f: "isNSUCont f"
   284   shows "isUCont f"
   285   unfolding isUCont_def dist_norm
   286 proof safe
   287   fix r :: real
   288   assume r: "0 < r"
   289   have "\<exists>s>0. \<forall>x y. hnorm (x - y) < s \<longrightarrow> hnorm (starfun f x - starfun f y) < star_of r"
   290   proof (rule exI, safe)
   291     show "0 < \<epsilon>"
   292       by (rule hypreal_epsilon_gt_zero)
   293   next
   294     fix x y :: "'a star"
   295     assume "hnorm (x - y) < \<epsilon>"
   296     with Infinitesimal_epsilon have "x - y \<in> Infinitesimal"
   297       by (rule hnorm_less_Infinitesimal)
   298     then have "x \<approx> y"
   299       by (unfold approx_def)
   300     with f have "starfun f x \<approx> starfun f y"
   301       by (simp add: isNSUCont_def)
   302     then have "starfun f x - starfun f y \<in> Infinitesimal"
   303       by (unfold approx_def)
   304     then show "hnorm (starfun f x - starfun f y) < star_of r"
   305       using r by (rule InfinitesimalD2)
   306   qed
   307   then show "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r"
   308     by transfer
   309 qed
   310 
   311 end