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