src/HOL/Nonstandard_Analysis/HSEQ.thy
 author wenzelm Sat Nov 04 19:17:19 2017 +0100 (19 months ago) changeset 67006 b1278ed3cd46 parent 66453 cc19f7ca2ed6 child 67443 3abf6a722518 permissions -rw-r--r--
prefer main entry points of HOL;
```     1 (*  Title:      HOL/Nonstandard_Analysis/HSEQ.thy
```
```     2     Author:     Jacques D. Fleuriot
```
```     3     Copyright:  1998  University of Cambridge
```
```     4
```
```     5 Convergence of sequences and series.
```
```     6
```
```     7 Conversion to Isar and new proofs by Lawrence C Paulson, 2004
```
```     8 Additional contributions by Jeremy Avigad and Brian Huffman.
```
```     9 *)
```
```    10
```
```    11 section \<open>Sequences and Convergence (Nonstandard)\<close>
```
```    12
```
```    13 theory HSEQ
```
```    14   imports Complex_Main NatStar
```
```    15   abbrevs "--->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S"
```
```    16 begin
```
```    17
```
```    18 definition NSLIMSEQ :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> bool"
```
```    19     ("((_)/ \<longlonglongrightarrow>\<^sub>N\<^sub>S (_))" [60, 60] 60) where
```
```    20     \<comment>\<open>Nonstandard definition of convergence of sequence\<close>
```
```    21   "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L \<longleftrightarrow> (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
```
```    22
```
```    23 definition nslim :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> 'a"
```
```    24   where "nslim X = (THE L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
```
```    25   \<comment> \<open>Nonstandard definition of limit using choice operator\<close>
```
```    26
```
```    27
```
```    28 definition NSconvergent :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> bool"
```
```    29   where "NSconvergent X \<longleftrightarrow> (\<exists>L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
```
```    30   \<comment> \<open>Nonstandard definition of convergence\<close>
```
```    31
```
```    32 definition NSBseq :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> bool"
```
```    33   where "NSBseq X \<longleftrightarrow> (\<forall>N \<in> HNatInfinite. ( *f* X) N \<in> HFinite)"
```
```    34   \<comment> \<open>Nonstandard definition for bounded sequence\<close>
```
```    35
```
```    36
```
```    37 definition NSCauchy :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> bool"
```
```    38   where "NSCauchy X \<longleftrightarrow> (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
```
```    39   \<comment> \<open>Nonstandard definition\<close>
```
```    40
```
```    41
```
```    42 subsection \<open>Limits of Sequences\<close>
```
```    43
```
```    44 lemma NSLIMSEQ_iff: "(X \<longlonglongrightarrow>\<^sub>N\<^sub>S L) \<longleftrightarrow> (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
```
```    45   by (simp add: NSLIMSEQ_def)
```
```    46
```
```    47 lemma NSLIMSEQ_I: "(\<And>N. N \<in> HNatInfinite \<Longrightarrow> starfun X N \<approx> star_of L) \<Longrightarrow> X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
```
```    48   by (simp add: NSLIMSEQ_def)
```
```    49
```
```    50 lemma NSLIMSEQ_D: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> N \<in> HNatInfinite \<Longrightarrow> starfun X N \<approx> star_of L"
```
```    51   by (simp add: NSLIMSEQ_def)
```
```    52
```
```    53 lemma NSLIMSEQ_const: "(\<lambda>n. k) \<longlonglongrightarrow>\<^sub>N\<^sub>S k"
```
```    54   by (simp add: NSLIMSEQ_def)
```
```    55
```
```    56 lemma NSLIMSEQ_add: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b \<Longrightarrow> (\<lambda>n. X n + Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a + b"
```
```    57   by (auto intro: approx_add simp add: NSLIMSEQ_def)
```
```    58
```
```    59 lemma NSLIMSEQ_add_const: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> (\<lambda>n. f n + b) \<longlonglongrightarrow>\<^sub>N\<^sub>S a + b"
```
```    60   by (simp only: NSLIMSEQ_add NSLIMSEQ_const)
```
```    61
```
```    62 lemma NSLIMSEQ_mult: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b \<Longrightarrow> (\<lambda>n. X n * Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a * b"
```
```    63   for a b :: "'a::real_normed_algebra"
```
```    64   by (auto intro!: approx_mult_HFinite simp add: NSLIMSEQ_def)
```
```    65
```
```    66 lemma NSLIMSEQ_minus: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> (\<lambda>n. - X n) \<longlonglongrightarrow>\<^sub>N\<^sub>S - a"
```
```    67   by (auto simp add: NSLIMSEQ_def)
```
```    68
```
```    69 lemma NSLIMSEQ_minus_cancel: "(\<lambda>n. - X n) \<longlonglongrightarrow>\<^sub>N\<^sub>S -a \<Longrightarrow> X \<longlonglongrightarrow>\<^sub>N\<^sub>S a"
```
```    70   by (drule NSLIMSEQ_minus) simp
```
```    71
```
```    72 lemma NSLIMSEQ_diff: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b \<Longrightarrow> (\<lambda>n. X n - Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a - b"
```
```    73   using NSLIMSEQ_add [of X a "- Y" "- b"] by (simp add: NSLIMSEQ_minus fun_Compl_def)
```
```    74
```
```    75 (* FIXME: delete *)
```
```    76 lemma NSLIMSEQ_add_minus: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b \<Longrightarrow> (\<lambda>n. X n + - Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a + - b"
```
```    77   by (simp add: NSLIMSEQ_diff)
```
```    78
```
```    79 lemma NSLIMSEQ_diff_const: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> (\<lambda>n. f n - b) \<longlonglongrightarrow>\<^sub>N\<^sub>S a - b"
```
```    80   by (simp add: NSLIMSEQ_diff NSLIMSEQ_const)
```
```    81
```
```    82 lemma NSLIMSEQ_inverse: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> (\<lambda>n. inverse (X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S inverse a"
```
```    83   for a :: "'a::real_normed_div_algebra"
```
```    84   by (simp add: NSLIMSEQ_def star_of_approx_inverse)
```
```    85
```
```    86 lemma NSLIMSEQ_mult_inverse: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> (\<lambda>n. X n / Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a / b"
```
```    87   for a b :: "'a::real_normed_field"
```
```    88   by (simp add: NSLIMSEQ_mult NSLIMSEQ_inverse divide_inverse)
```
```    89
```
```    90 lemma starfun_hnorm: "\<And>x. hnorm (( *f* f) x) = ( *f* (\<lambda>x. norm (f x))) x"
```
```    91   by transfer simp
```
```    92
```
```    93 lemma NSLIMSEQ_norm: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> (\<lambda>n. norm (X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S norm a"
```
```    94   by (simp add: NSLIMSEQ_def starfun_hnorm [symmetric] approx_hnorm)
```
```    95
```
```    96 text \<open>Uniqueness of limit.\<close>
```
```    97 lemma NSLIMSEQ_unique: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> X \<longlonglongrightarrow>\<^sub>N\<^sub>S b \<Longrightarrow> a = b"
```
```    98   apply (simp add: NSLIMSEQ_def)
```
```    99   apply (drule HNatInfinite_whn [THEN [2] bspec])+
```
```   100   apply (auto dest: approx_trans3)
```
```   101   done
```
```   102
```
```   103 lemma NSLIMSEQ_pow [rule_format]: "(X \<longlonglongrightarrow>\<^sub>N\<^sub>S a) \<longrightarrow> ((\<lambda>n. (X n) ^ m) \<longlonglongrightarrow>\<^sub>N\<^sub>S a ^ m)"
```
```   104   for a :: "'a::{real_normed_algebra,power}"
```
```   105   by (induct m) (auto intro: NSLIMSEQ_mult NSLIMSEQ_const)
```
```   106
```
```   107 text \<open>We can now try and derive a few properties of sequences,
```
```   108   starting with the limit comparison property for sequences.\<close>
```
```   109
```
```   110 lemma NSLIMSEQ_le: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S l \<Longrightarrow> g \<longlonglongrightarrow>\<^sub>N\<^sub>S m \<Longrightarrow> \<exists>N. \<forall>n \<ge> N. f n \<le> g n \<Longrightarrow> l \<le> m"
```
```   111   for l m :: real
```
```   112   apply (simp add: NSLIMSEQ_def, safe)
```
```   113   apply (drule starfun_le_mono)
```
```   114   apply (drule HNatInfinite_whn [THEN [2] bspec])+
```
```   115   apply (drule_tac x = whn in spec)
```
```   116   apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+
```
```   117   apply clarify
```
```   118   apply (auto intro: hypreal_of_real_le_add_Infininitesimal_cancel2)
```
```   119   done
```
```   120
```
```   121 lemma NSLIMSEQ_le_const: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S r \<Longrightarrow> \<forall>n. a \<le> X n \<Longrightarrow> a \<le> r"
```
```   122   for a r :: real
```
```   123   by (erule NSLIMSEQ_le [OF NSLIMSEQ_const]) auto
```
```   124
```
```   125 lemma NSLIMSEQ_le_const2: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S r \<Longrightarrow> \<forall>n. X n \<le> a \<Longrightarrow> r \<le> a"
```
```   126   for a r :: real
```
```   127   by (erule NSLIMSEQ_le [OF _ NSLIMSEQ_const]) auto
```
```   128
```
```   129 text \<open>Shift a convergent series by 1:
```
```   130   By the equivalence between Cauchiness and convergence and because
```
```   131   the successor of an infinite hypernatural is also infinite.\<close>
```
```   132
```
```   133 lemma NSLIMSEQ_Suc: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S l \<Longrightarrow> (\<lambda>n. f(Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l"
```
```   134   apply (unfold NSLIMSEQ_def)
```
```   135   apply safe
```
```   136   apply (drule_tac x="N + 1" in bspec)
```
```   137    apply (erule HNatInfinite_add)
```
```   138   apply (simp add: starfun_shift_one)
```
```   139   done
```
```   140
```
```   141 lemma NSLIMSEQ_imp_Suc: "(\<lambda>n. f(Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l \<Longrightarrow> f \<longlonglongrightarrow>\<^sub>N\<^sub>S l"
```
```   142   apply (unfold NSLIMSEQ_def)
```
```   143   apply safe
```
```   144   apply (drule_tac x="N - 1" in bspec)
```
```   145    apply (erule Nats_1 [THEN [2] HNatInfinite_diff])
```
```   146   apply (simp add: starfun_shift_one one_le_HNatInfinite)
```
```   147   done
```
```   148
```
```   149 lemma NSLIMSEQ_Suc_iff: "(\<lambda>n. f (Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l \<longleftrightarrow> f \<longlonglongrightarrow>\<^sub>N\<^sub>S l"
```
```   150   by (blast intro: NSLIMSEQ_imp_Suc NSLIMSEQ_Suc)
```
```   151
```
```   152
```
```   153 subsubsection \<open>Equivalence of @{term LIMSEQ} and @{term NSLIMSEQ}\<close>
```
```   154
```
```   155 lemma LIMSEQ_NSLIMSEQ:
```
```   156   assumes X: "X \<longlonglongrightarrow> L"
```
```   157   shows "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
```
```   158 proof (rule NSLIMSEQ_I)
```
```   159   fix N
```
```   160   assume N: "N \<in> HNatInfinite"
```
```   161   have "starfun X N - star_of L \<in> Infinitesimal"
```
```   162   proof (rule InfinitesimalI2)
```
```   163     fix r :: real
```
```   164     assume r: "0 < r"
```
```   165     from LIMSEQ_D [OF X r] obtain no where "\<forall>n\<ge>no. norm (X n - L) < r" ..
```
```   166     then have "\<forall>n\<ge>star_of no. hnorm (starfun X n - star_of L) < star_of r"
```
```   167       by transfer
```
```   168     then show "hnorm (starfun X N - star_of L) < star_of r"
```
```   169       using N by (simp add: star_of_le_HNatInfinite)
```
```   170   qed
```
```   171   then show "starfun X N \<approx> star_of L"
```
```   172     by (simp only: approx_def)
```
```   173 qed
```
```   174
```
```   175 lemma NSLIMSEQ_LIMSEQ:
```
```   176   assumes X: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
```
```   177   shows "X \<longlonglongrightarrow> L"
```
```   178 proof (rule LIMSEQ_I)
```
```   179   fix r :: real
```
```   180   assume r: "0 < r"
```
```   181   have "\<exists>no. \<forall>n\<ge>no. hnorm (starfun X n - star_of L) < star_of r"
```
```   182   proof (intro exI allI impI)
```
```   183     fix n
```
```   184     assume "whn \<le> n"
```
```   185     with HNatInfinite_whn have "n \<in> HNatInfinite"
```
```   186       by (rule HNatInfinite_upward_closed)
```
```   187     with X have "starfun X n \<approx> star_of L"
```
```   188       by (rule NSLIMSEQ_D)
```
```   189     then have "starfun X n - star_of L \<in> Infinitesimal"
```
```   190       by (simp only: approx_def)
```
```   191     then show "hnorm (starfun X n - star_of L) < star_of r"
```
```   192       using r by (rule InfinitesimalD2)
```
```   193   qed
```
```   194   then show "\<exists>no. \<forall>n\<ge>no. norm (X n - L) < r"
```
```   195     by transfer
```
```   196 qed
```
```   197
```
```   198 theorem LIMSEQ_NSLIMSEQ_iff: "f \<longlonglongrightarrow> L \<longleftrightarrow> f \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
```
```   199   by (blast intro: LIMSEQ_NSLIMSEQ NSLIMSEQ_LIMSEQ)
```
```   200
```
```   201
```
```   202 subsubsection \<open>Derived theorems about @{term NSLIMSEQ}\<close>
```
```   203
```
```   204 text \<open>We prove the NS version from the standard one, since the NS proof
```
```   205   seems more complicated than the standard one above!\<close>
```
```   206 lemma NSLIMSEQ_norm_zero: "(\<lambda>n. norm (X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0 \<longleftrightarrow> X \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
```
```   207   by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] tendsto_norm_zero_iff)
```
```   208
```
```   209 lemma NSLIMSEQ_rabs_zero: "(\<lambda>n. \<bar>f n\<bar>) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0 \<longleftrightarrow> f \<longlonglongrightarrow>\<^sub>N\<^sub>S (0::real)"
```
```   210   by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] tendsto_rabs_zero_iff)
```
```   211
```
```   212 text \<open>Generalization to other limits.\<close>
```
```   213 lemma NSLIMSEQ_imp_rabs: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S l \<Longrightarrow> (\<lambda>n. \<bar>f n\<bar>) \<longlonglongrightarrow>\<^sub>N\<^sub>S \<bar>l\<bar>"
```
```   214   for l :: real
```
```   215   by (simp add: NSLIMSEQ_def) (auto intro: approx_hrabs simp add: starfun_abs)
```
```   216
```
```   217 lemma NSLIMSEQ_inverse_zero: "\<forall>y::real. \<exists>N. \<forall>n \<ge> N. y < f n \<Longrightarrow> (\<lambda>n. inverse (f n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
```
```   218   by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_zero)
```
```   219
```
```   220 lemma NSLIMSEQ_inverse_real_of_nat: "(\<lambda>n. inverse (real (Suc n))) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
```
```   221   by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat del: of_nat_Suc)
```
```   222
```
```   223 lemma NSLIMSEQ_inverse_real_of_nat_add: "(\<lambda>n. r + inverse (real (Suc n))) \<longlonglongrightarrow>\<^sub>N\<^sub>S r"
```
```   224   by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add del: of_nat_Suc)
```
```   225
```
```   226 lemma NSLIMSEQ_inverse_real_of_nat_add_minus: "(\<lambda>n. r + - inverse (real (Suc n))) \<longlonglongrightarrow>\<^sub>N\<^sub>S r"
```
```   227   using LIMSEQ_inverse_real_of_nat_add_minus by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric])
```
```   228
```
```   229 lemma NSLIMSEQ_inverse_real_of_nat_add_minus_mult:
```
```   230   "(\<lambda>n. r * (1 + - inverse (real (Suc n)))) \<longlonglongrightarrow>\<^sub>N\<^sub>S r"
```
```   231   using LIMSEQ_inverse_real_of_nat_add_minus_mult
```
```   232   by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric])
```
```   233
```
```   234
```
```   235 subsection \<open>Convergence\<close>
```
```   236
```
```   237 lemma nslimI: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> nslim X = L"
```
```   238   by (simp add: nslim_def) (blast intro: NSLIMSEQ_unique)
```
```   239
```
```   240 lemma lim_nslim_iff: "lim X = nslim X"
```
```   241   by (simp add: lim_def nslim_def LIMSEQ_NSLIMSEQ_iff)
```
```   242
```
```   243 lemma NSconvergentD: "NSconvergent X \<Longrightarrow> \<exists>L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
```
```   244   by (simp add: NSconvergent_def)
```
```   245
```
```   246 lemma NSconvergentI: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> NSconvergent X"
```
```   247   by (auto simp add: NSconvergent_def)
```
```   248
```
```   249 lemma convergent_NSconvergent_iff: "convergent X = NSconvergent X"
```
```   250   by (simp add: convergent_def NSconvergent_def LIMSEQ_NSLIMSEQ_iff)
```
```   251
```
```   252 lemma NSconvergent_NSLIMSEQ_iff: "NSconvergent X \<longleftrightarrow> X \<longlonglongrightarrow>\<^sub>N\<^sub>S nslim X"
```
```   253   by (auto intro: theI NSLIMSEQ_unique simp add: NSconvergent_def nslim_def)
```
```   254
```
```   255
```
```   256 subsection \<open>Bounded Monotonic Sequences\<close>
```
```   257
```
```   258 lemma NSBseqD: "NSBseq X \<Longrightarrow> N \<in> HNatInfinite \<Longrightarrow> ( *f* X) N \<in> HFinite"
```
```   259   by (simp add: NSBseq_def)
```
```   260
```
```   261 lemma Standard_subset_HFinite: "Standard \<subseteq> HFinite"
```
```   262   by (auto simp: Standard_def)
```
```   263
```
```   264 lemma NSBseqD2: "NSBseq X \<Longrightarrow> ( *f* X) N \<in> HFinite"
```
```   265   apply (cases "N \<in> HNatInfinite")
```
```   266    apply (erule (1) NSBseqD)
```
```   267   apply (rule subsetD [OF Standard_subset_HFinite])
```
```   268   apply (simp add: HNatInfinite_def Nats_eq_Standard)
```
```   269   done
```
```   270
```
```   271 lemma NSBseqI: "\<forall>N \<in> HNatInfinite. ( *f* X) N \<in> HFinite \<Longrightarrow> NSBseq X"
```
```   272   by (simp add: NSBseq_def)
```
```   273
```
```   274 text \<open>The standard definition implies the nonstandard definition.\<close>
```
```   275 lemma Bseq_NSBseq: "Bseq X \<Longrightarrow> NSBseq X"
```
```   276   unfolding NSBseq_def
```
```   277 proof safe
```
```   278   assume X: "Bseq X"
```
```   279   fix N
```
```   280   assume N: "N \<in> HNatInfinite"
```
```   281   from BseqD [OF X] obtain K where "\<forall>n. norm (X n) \<le> K"
```
```   282     by fast
```
```   283   then have "\<forall>N. hnorm (starfun X N) \<le> star_of K"
```
```   284     by transfer
```
```   285   then have "hnorm (starfun X N) \<le> star_of K"
```
```   286     by simp
```
```   287   also have "star_of K < star_of (K + 1)"
```
```   288     by simp
```
```   289   finally have "\<exists>x\<in>Reals. hnorm (starfun X N) < x"
```
```   290     by (rule bexI) simp
```
```   291   then show "starfun X N \<in> HFinite"
```
```   292     by (simp add: HFinite_def)
```
```   293 qed
```
```   294
```
```   295 text \<open>The nonstandard definition implies the standard definition.\<close>
```
```   296 lemma SReal_less_omega: "r \<in> \<real> \<Longrightarrow> r < \<omega>"
```
```   297   using HInfinite_omega
```
```   298   by (simp add: HInfinite_def) (simp add: order_less_imp_le)
```
```   299
```
```   300 lemma NSBseq_Bseq: "NSBseq X \<Longrightarrow> Bseq X"
```
```   301 proof (rule ccontr)
```
```   302   let ?n = "\<lambda>K. LEAST n. K < norm (X n)"
```
```   303   assume "NSBseq X"
```
```   304   then have finite: "( *f* X) (( *f* ?n) \<omega>) \<in> HFinite"
```
```   305     by (rule NSBseqD2)
```
```   306   assume "\<not> Bseq X"
```
```   307   then have "\<forall>K>0. \<exists>n. K < norm (X n)"
```
```   308     by (simp add: Bseq_def linorder_not_le)
```
```   309   then have "\<forall>K>0. K < norm (X (?n K))"
```
```   310     by (auto intro: LeastI_ex)
```
```   311   then have "\<forall>K>0. K < hnorm (( *f* X) (( *f* ?n) K))"
```
```   312     by transfer
```
```   313   then have "\<omega> < hnorm (( *f* X) (( *f* ?n) \<omega>))"
```
```   314     by simp
```
```   315   then have "\<forall>r\<in>\<real>. r < hnorm (( *f* X) (( *f* ?n) \<omega>))"
```
```   316     by (simp add: order_less_trans [OF SReal_less_omega])
```
```   317   then have "( *f* X) (( *f* ?n) \<omega>) \<in> HInfinite"
```
```   318     by (simp add: HInfinite_def)
```
```   319   with finite show "False"
```
```   320     by (simp add: HFinite_HInfinite_iff)
```
```   321 qed
```
```   322
```
```   323 text \<open>Equivalence of nonstandard and standard definitions for a bounded sequence.\<close>
```
```   324 lemma Bseq_NSBseq_iff: "Bseq X = NSBseq X"
```
```   325   by (blast intro!: NSBseq_Bseq Bseq_NSBseq)
```
```   326
```
```   327 text \<open>A convergent sequence is bounded:
```
```   328   Boundedness as a necessary condition for convergence.
```
```   329   The nonstandard version has no existential, as usual.\<close>
```
```   330 lemma NSconvergent_NSBseq: "NSconvergent X \<Longrightarrow> NSBseq X"
```
```   331   by (simp add: NSconvergent_def NSBseq_def NSLIMSEQ_def)
```
```   332     (blast intro: HFinite_star_of approx_sym approx_HFinite)
```
```   333
```
```   334 text \<open>Standard Version: easily now proved using equivalence of NS and
```
```   335  standard definitions.\<close>
```
```   336
```
```   337 lemma convergent_Bseq: "convergent X \<Longrightarrow> Bseq X"
```
```   338   for X :: "nat \<Rightarrow> 'b::real_normed_vector"
```
```   339   by (simp add: NSconvergent_NSBseq convergent_NSconvergent_iff Bseq_NSBseq_iff)
```
```   340
```
```   341
```
```   342 subsubsection \<open>Upper Bounds and Lubs of Bounded Sequences\<close>
```
```   343
```
```   344 lemma NSBseq_isUb: "NSBseq X \<Longrightarrow> \<exists>U::real. isUb UNIV {x. \<exists>n. X n = x} U"
```
```   345   by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isUb)
```
```   346
```
```   347 lemma NSBseq_isLub: "NSBseq X \<Longrightarrow> \<exists>U::real. isLub UNIV {x. \<exists>n. X n = x} U"
```
```   348   by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isLub)
```
```   349
```
```   350
```
```   351 subsubsection \<open>A Bounded and Monotonic Sequence Converges\<close>
```
```   352
```
```   353 text \<open>The best of both worlds: Easier to prove this result as a standard
```
```   354    theorem and then use equivalence to "transfer" it into the
```
```   355    equivalent nonstandard form if needed!\<close>
```
```   356
```
```   357 lemma Bmonoseq_NSLIMSEQ: "\<forall>n \<ge> m. X n = X m \<Longrightarrow> \<exists>L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
```
```   358   by (auto dest!: Bmonoseq_LIMSEQ simp add: LIMSEQ_NSLIMSEQ_iff)
```
```   359
```
```   360 lemma NSBseq_mono_NSconvergent: "NSBseq X \<Longrightarrow> \<forall>m. \<forall>n \<ge> m. X m \<le> X n \<Longrightarrow> NSconvergent X"
```
```   361   for X :: "nat \<Rightarrow> real"
```
```   362   by (auto intro: Bseq_mono_convergent
```
```   363       simp: convergent_NSconvergent_iff [symmetric] Bseq_NSBseq_iff [symmetric])
```
```   364
```
```   365
```
```   366 subsection \<open>Cauchy Sequences\<close>
```
```   367
```
```   368 lemma NSCauchyI:
```
```   369   "(\<And>M N. M \<in> HNatInfinite \<Longrightarrow> N \<in> HNatInfinite \<Longrightarrow> starfun X M \<approx> starfun X N) \<Longrightarrow> NSCauchy X"
```
```   370   by (simp add: NSCauchy_def)
```
```   371
```
```   372 lemma NSCauchyD:
```
```   373   "NSCauchy X \<Longrightarrow> M \<in> HNatInfinite \<Longrightarrow> N \<in> HNatInfinite \<Longrightarrow> starfun X M \<approx> starfun X N"
```
```   374   by (simp add: NSCauchy_def)
```
```   375
```
```   376
```
```   377 subsubsection \<open>Equivalence Between NS and Standard\<close>
```
```   378
```
```   379 lemma Cauchy_NSCauchy:
```
```   380   assumes X: "Cauchy X"
```
```   381   shows "NSCauchy X"
```
```   382 proof (rule NSCauchyI)
```
```   383   fix M
```
```   384   assume M: "M \<in> HNatInfinite"
```
```   385   fix N
```
```   386   assume N: "N \<in> HNatInfinite"
```
```   387   have "starfun X M - starfun X N \<in> Infinitesimal"
```
```   388   proof (rule InfinitesimalI2)
```
```   389     fix r :: real
```
```   390     assume r: "0 < r"
```
```   391     from CauchyD [OF X r] obtain k where "\<forall>m\<ge>k. \<forall>n\<ge>k. norm (X m - X n) < r" ..
```
```   392     then have "\<forall>m\<ge>star_of k. \<forall>n\<ge>star_of k. hnorm (starfun X m - starfun X n) < star_of r"
```
```   393       by transfer
```
```   394     then show "hnorm (starfun X M - starfun X N) < star_of r"
```
```   395       using M N by (simp add: star_of_le_HNatInfinite)
```
```   396   qed
```
```   397   then show "starfun X M \<approx> starfun X N"
```
```   398     by (simp only: approx_def)
```
```   399 qed
```
```   400
```
```   401 lemma NSCauchy_Cauchy:
```
```   402   assumes X: "NSCauchy X"
```
```   403   shows "Cauchy X"
```
```   404 proof (rule CauchyI)
```
```   405   fix r :: real
```
```   406   assume r: "0 < r"
```
```   407   have "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. hnorm (starfun X m - starfun X n) < star_of r"
```
```   408   proof (intro exI allI impI)
```
```   409     fix M
```
```   410     assume "whn \<le> M"
```
```   411     with HNatInfinite_whn have M: "M \<in> HNatInfinite"
```
```   412       by (rule HNatInfinite_upward_closed)
```
```   413     fix N
```
```   414     assume "whn \<le> N"
```
```   415     with HNatInfinite_whn have N: "N \<in> HNatInfinite"
```
```   416       by (rule HNatInfinite_upward_closed)
```
```   417     from X M N have "starfun X M \<approx> starfun X N"
```
```   418       by (rule NSCauchyD)
```
```   419     then have "starfun X M - starfun X N \<in> Infinitesimal"
```
```   420       by (simp only: approx_def)
```
```   421     then show "hnorm (starfun X M - starfun X N) < star_of r"
```
```   422       using r by (rule InfinitesimalD2)
```
```   423   qed
```
```   424   then show "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. norm (X m - X n) < r"
```
```   425     by transfer
```
```   426 qed
```
```   427
```
```   428 theorem NSCauchy_Cauchy_iff: "NSCauchy X = Cauchy X"
```
```   429   by (blast intro!: NSCauchy_Cauchy Cauchy_NSCauchy)
```
```   430
```
```   431
```
```   432 subsubsection \<open>Cauchy Sequences are Bounded\<close>
```
```   433
```
```   434 text \<open>A Cauchy sequence is bounded -- nonstandard version.\<close>
```
```   435
```
```   436 lemma NSCauchy_NSBseq: "NSCauchy X \<Longrightarrow> NSBseq X"
```
```   437   by (simp add: Cauchy_Bseq Bseq_NSBseq_iff [symmetric] NSCauchy_Cauchy_iff)
```
```   438
```
```   439
```
```   440 subsubsection \<open>Cauchy Sequences are Convergent\<close>
```
```   441
```
```   442 text \<open>Equivalence of Cauchy criterion and convergence:
```
```   443   We will prove this using our NS formulation which provides a
```
```   444   much easier proof than using the standard definition. We do not
```
```   445   need to use properties of subsequences such as boundedness,
```
```   446   monotonicity etc... Compare with Harrison's corresponding proof
```
```   447   in HOL which is much longer and more complicated. Of course, we do
```
```   448   not have problems which he encountered with guessing the right
```
```   449   instantiations for his 'espsilon-delta' proof(s) in this case
```
```   450   since the NS formulations do not involve existential quantifiers.\<close>
```
```   451
```
```   452 lemma NSconvergent_NSCauchy: "NSconvergent X \<Longrightarrow> NSCauchy X"
```
```   453   by (simp add: NSconvergent_def NSLIMSEQ_def NSCauchy_def) (auto intro: approx_trans2)
```
```   454
```
```   455 lemma real_NSCauchy_NSconvergent: "NSCauchy X \<Longrightarrow> NSconvergent X"
```
```   456   for X :: "nat \<Rightarrow> real"
```
```   457   apply (simp add: NSconvergent_def NSLIMSEQ_def)
```
```   458   apply (frule NSCauchy_NSBseq)
```
```   459   apply (simp add: NSBseq_def NSCauchy_def)
```
```   460   apply (drule HNatInfinite_whn [THEN [2] bspec])
```
```   461   apply (drule HNatInfinite_whn [THEN [2] bspec])
```
```   462   apply (auto dest!: st_part_Ex simp add: SReal_iff)
```
```   463   apply (blast intro: approx_trans3)
```
```   464   done
```
```   465
```
```   466 lemma NSCauchy_NSconvergent: "NSCauchy X \<Longrightarrow> NSconvergent X"
```
```   467   for X :: "nat \<Rightarrow> 'a::banach"
```
```   468   apply (drule NSCauchy_Cauchy [THEN Cauchy_convergent])
```
```   469   apply (erule convergent_NSconvergent_iff [THEN iffD1])
```
```   470   done
```
```   471
```
```   472 lemma NSCauchy_NSconvergent_iff: "NSCauchy X = NSconvergent X"
```
```   473   for X :: "nat \<Rightarrow> 'a::banach"
```
```   474   by (fast intro: NSCauchy_NSconvergent NSconvergent_NSCauchy)
```
```   475
```
```   476
```
```   477 subsection \<open>Power Sequences\<close>
```
```   478
```
```   479 text \<open>The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term
```
```   480   "x<1"}.  Proof will use (NS) Cauchy equivalence for convergence and
```
```   481   also fact that bounded and monotonic sequence converges.\<close>
```
```   482
```
```   483 text \<open>We now use NS criterion to bring proof of theorem through.\<close>
```
```   484 lemma NSLIMSEQ_realpow_zero: "0 \<le> x \<Longrightarrow> x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
```
```   485   for x :: real
```
```   486   apply (simp add: NSLIMSEQ_def)
```
```   487   apply (auto dest!: convergent_realpow simp add: convergent_NSconvergent_iff)
```
```   488   apply (frule NSconvergentD)
```
```   489   apply (auto simp add: NSLIMSEQ_def NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfun_pow)
```
```   490   apply (frule HNatInfinite_add_one)
```
```   491   apply (drule bspec, assumption)
```
```   492   apply (drule bspec, assumption)
```
```   493   apply (drule_tac x = "N + 1" in bspec, assumption)
```
```   494   apply (simp add: hyperpow_add)
```
```   495   apply (drule approx_mult_subst_star_of, assumption)
```
```   496   apply (drule approx_trans3, assumption)
```
```   497   apply (auto simp del: star_of_mult simp add: star_of_mult [symmetric])
```
```   498   done
```
```   499
```
```   500 lemma NSLIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. \<bar>c\<bar> ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
```
```   501   for c :: real
```
```   502   by (simp add: LIMSEQ_rabs_realpow_zero LIMSEQ_NSLIMSEQ_iff [symmetric])
```
```   503
```
```   504 lemma NSLIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. c ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
```
```   505   for c :: real
```
```   506   by (simp add: LIMSEQ_rabs_realpow_zero2 LIMSEQ_NSLIMSEQ_iff [symmetric])
```
```   507
```
```   508 (***---------------------------------------------------------------
```
```   509     Theorems proved by Harrison in HOL that we do not need
```
```   510     in order to prove equivalence between Cauchy criterion
```
```   511     and convergence:
```
```   512  -- Show that every sequence contains a monotonic subsequence
```
```   513 Goal "\<exists>f. subseq f & monoseq (%n. s (f n))"
```
```   514  -- Show that a subsequence of a bounded sequence is bounded
```
```   515 Goal "Bseq X ==> Bseq (%n. X (f n))";
```
```   516  -- Show we can take subsequential terms arbitrarily far
```
```   517     up a sequence
```
```   518 Goal "subseq f ==> n \<le> f(n)";
```
```   519 Goal "subseq f ==> \<exists>n. N1 \<le> n & N2 \<le> f(n)";
```
```   520  ---------------------------------------------------------------***)
```
```   521
```
```   522 end
```