author | wenzelm |
Wed, 17 May 2017 13:47:19 +0200 | |
changeset 65851 | c103358a5559 |
parent 64604 | 2bf8cfc98c4d |
child 66453 | cc19f7ca2ed6 |
permissions | -rw-r--r-- |
62479 | 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. |
|
27468 | 9 |
*) |
10 |
||
61975 | 11 |
section \<open>Sequences and Convergence (Nonstandard)\<close> |
27468 | 12 |
|
13 |
theory HSEQ |
|
63579 | 14 |
imports Limits NatStar |
15 |
abbrevs "--->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S" |
|
27468 | 16 |
begin |
17 |
||
64604 | 18 |
definition NSLIMSEQ :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> bool" |
61970 | 19 |
("((_)/ \<longlonglongrightarrow>\<^sub>N\<^sub>S (_))" [60, 60] 60) where |
61975 | 20 |
\<comment>\<open>Nonstandard definition of convergence of sequence\<close> |
64604 | 21 |
"X \<longlonglongrightarrow>\<^sub>N\<^sub>S L \<longleftrightarrow> (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)" |
27468 | 22 |
|
64604 | 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 |
||
27468 | 27 |
|
64604 | 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> |
|
27468 | 31 |
|
64604 | 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 |
||
27468 | 36 |
|
64604 | 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 |
||
27468 | 41 |
|
61975 | 42 |
subsection \<open>Limits of Sequences\<close> |
27468 | 43 |
|
64604 | 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) |
|
27468 | 49 |
|
64604 | 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) |
|
27468 | 52 |
|
64604 | 53 |
lemma NSLIMSEQ_const: "(\<lambda>n. k) \<longlonglongrightarrow>\<^sub>N\<^sub>S k" |
54 |
by (simp add: NSLIMSEQ_def) |
|
27468 | 55 |
|
64604 | 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) |
|
27468 | 58 |
|
64604 | 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) |
|
27468 | 61 |
|
64604 | 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) |
|
27468 | 65 |
|
64604 | 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) |
|
27468 | 68 |
|
64604 | 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 |
|
27468 | 71 |
|
64604 | 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" |
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
51525
diff
changeset
|
73 |
using NSLIMSEQ_add [of X a "- Y" "- b"] by (simp add: NSLIMSEQ_minus fun_Compl_def) |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
51525
diff
changeset
|
74 |
|
27468 | 75 |
(* FIXME: delete *) |
64604 | 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" |
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
51525
diff
changeset
|
77 |
by (simp add: NSLIMSEQ_diff) |
27468 | 78 |
|
64604 | 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) |
|
27468 | 81 |
|
64604 | 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) |
|
27468 | 85 |
|
64604 | 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) |
|
27468 | 89 |
|
90 |
lemma starfun_hnorm: "\<And>x. hnorm (( *f* f) x) = ( *f* (\<lambda>x. norm (f x))) x" |
|
64604 | 91 |
by transfer simp |
27468 | 92 |
|
61970 | 93 |
lemma NSLIMSEQ_norm: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> (\<lambda>n. norm (X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S norm a" |
64604 | 94 |
by (simp add: NSLIMSEQ_def starfun_hnorm [symmetric] approx_hnorm) |
27468 | 95 |
|
64604 | 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 |
|
27468 | 102 |
|
64604 | 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> |
|
27468 | 109 |
|
64604 | 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 |
|
27468 | 120 |
|
64604 | 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 |
|
27468 | 124 |
|
64604 | 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 |
|
27468 | 128 |
|
64604 | 129 |
text \<open>Shift a convergent series by 1: |
27468 | 130 |
By the equivalence between Cauchiness and convergence and because |
61975 | 131 |
the successor of an infinite hypernatural is also infinite.\<close> |
27468 | 132 |
|
64604 | 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 |
|
27468 | 140 |
|
64604 | 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 |
|
27468 | 148 |
|
64604 | 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 |
||
27468 | 152 |
|
61975 | 153 |
subsubsection \<open>Equivalence of @{term LIMSEQ} and @{term NSLIMSEQ}\<close> |
27468 | 154 |
|
155 |
lemma LIMSEQ_NSLIMSEQ: |
|
64604 | 156 |
assumes X: "X \<longlonglongrightarrow> L" |
157 |
shows "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L" |
|
27468 | 158 |
proof (rule NSLIMSEQ_I) |
64604 | 159 |
fix N |
160 |
assume N: "N \<in> HNatInfinite" |
|
27468 | 161 |
have "starfun X N - star_of L \<in> Infinitesimal" |
162 |
proof (rule InfinitesimalI2) |
|
64604 | 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" |
|
27468 | 167 |
by transfer |
64604 | 168 |
then show "hnorm (starfun X N - star_of L) < star_of r" |
27468 | 169 |
using N by (simp add: star_of_le_HNatInfinite) |
170 |
qed |
|
64604 | 171 |
then show "starfun X N \<approx> star_of L" |
172 |
by (simp only: approx_def) |
|
27468 | 173 |
qed |
174 |
||
175 |
lemma NSLIMSEQ_LIMSEQ: |
|
64604 | 176 |
assumes X: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L" |
177 |
shows "X \<longlonglongrightarrow> L" |
|
27468 | 178 |
proof (rule LIMSEQ_I) |
64604 | 179 |
fix r :: real |
180 |
assume r: "0 < r" |
|
27468 | 181 |
have "\<exists>no. \<forall>n\<ge>no. hnorm (starfun X n - star_of L) < star_of r" |
182 |
proof (intro exI allI impI) |
|
64604 | 183 |
fix n |
184 |
assume "whn \<le> n" |
|
27468 | 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) |
|
64604 | 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" |
|
27468 | 192 |
using r by (rule InfinitesimalD2) |
193 |
qed |
|
64604 | 194 |
then show "\<exists>no. \<forall>n\<ge>no. norm (X n - L) < r" |
27468 | 195 |
by transfer |
196 |
qed |
|
197 |
||
64604 | 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 |
||
27468 | 201 |
|
61975 | 202 |
subsubsection \<open>Derived theorems about @{term NSLIMSEQ}\<close> |
27468 | 203 |
|
64604 | 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) |
|
27468 | 208 |
|
64604 | 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) |
|
27468 | 211 |
|
64604 | 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) |
|
27468 | 219 |
|
64604 | 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) |
|
27468 | 222 |
|
64604 | 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) |
|
27468 | 225 |
|
64604 | 226 |
lemma NSLIMSEQ_inverse_real_of_nat_add_minus: "(\<lambda>n. r + - inverse (real (Suc n))) \<longlonglongrightarrow>\<^sub>N\<^sub>S r" |
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
51525
diff
changeset
|
227 |
using LIMSEQ_inverse_real_of_nat_add_minus by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric]) |
27468 | 228 |
|
229 |
lemma NSLIMSEQ_inverse_real_of_nat_add_minus_mult: |
|
64604 | 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]) |
|
27468 | 233 |
|
234 |
||
61975 | 235 |
subsection \<open>Convergence\<close> |
27468 | 236 |
|
64604 | 237 |
lemma nslimI: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> nslim X = L" |
238 |
by (simp add: nslim_def) (blast intro: NSLIMSEQ_unique) |
|
27468 | 239 |
|
240 |
lemma lim_nslim_iff: "lim X = nslim X" |
|
64604 | 241 |
by (simp add: lim_def nslim_def LIMSEQ_NSLIMSEQ_iff) |
27468 | 242 |
|
64604 | 243 |
lemma NSconvergentD: "NSconvergent X \<Longrightarrow> \<exists>L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L" |
244 |
by (simp add: NSconvergent_def) |
|
27468 | 245 |
|
64604 | 246 |
lemma NSconvergentI: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> NSconvergent X" |
247 |
by (auto simp add: NSconvergent_def) |
|
27468 | 248 |
|
249 |
lemma convergent_NSconvergent_iff: "convergent X = NSconvergent X" |
|
64604 | 250 |
by (simp add: convergent_def NSconvergent_def LIMSEQ_NSLIMSEQ_iff) |
27468 | 251 |
|
64604 | 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) |
|
27468 | 254 |
|
255 |
||
61975 | 256 |
subsection \<open>Bounded Monotonic Sequences\<close> |
27468 | 257 |
|
64604 | 258 |
lemma NSBseqD: "NSBseq X \<Longrightarrow> N \<in> HNatInfinite \<Longrightarrow> ( *f* X) N \<in> HFinite" |
259 |
by (simp add: NSBseq_def) |
|
27468 | 260 |
|
261 |
lemma Standard_subset_HFinite: "Standard \<subseteq> HFinite" |
|
64604 | 262 |
by (auto simp: Standard_def) |
27468 | 263 |
|
264 |
lemma NSBseqD2: "NSBseq X \<Longrightarrow> ( *f* X) N \<in> HFinite" |
|
64604 | 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 |
|
27468 | 270 |
|
64604 | 271 |
lemma NSBseqI: "\<forall>N \<in> HNatInfinite. ( *f* X) N \<in> HFinite \<Longrightarrow> NSBseq X" |
272 |
by (simp add: NSBseq_def) |
|
27468 | 273 |
|
64604 | 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 |
|
27468 | 278 |
assume X: "Bseq X" |
64604 | 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) |
|
27468 | 293 |
qed |
294 |
||
64604 | 295 |
text \<open>The nonstandard definition implies the standard definition.\<close> |
27468 | 296 |
lemma SReal_less_omega: "r \<in> \<real> \<Longrightarrow> r < \<omega>" |
64604 | 297 |
using HInfinite_omega |
298 |
by (simp add: HInfinite_def) (simp add: order_less_imp_le) |
|
27468 | 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" |
|
64604 | 304 |
then have finite: "( *f* X) (( *f* ?n) \<omega>) \<in> HFinite" |
27468 | 305 |
by (rule NSBseqD2) |
306 |
assume "\<not> Bseq X" |
|
64604 | 307 |
then have "\<forall>K>0. \<exists>n. K < norm (X n)" |
27468 | 308 |
by (simp add: Bseq_def linorder_not_le) |
64604 | 309 |
then have "\<forall>K>0. K < norm (X (?n K))" |
27468 | 310 |
by (auto intro: LeastI_ex) |
64604 | 311 |
then have "\<forall>K>0. K < hnorm (( *f* X) (( *f* ?n) K))" |
27468 | 312 |
by transfer |
64604 | 313 |
then have "\<omega> < hnorm (( *f* X) (( *f* ?n) \<omega>))" |
27468 | 314 |
by simp |
64604 | 315 |
then have "\<forall>r\<in>\<real>. r < hnorm (( *f* X) (( *f* ?n) \<omega>))" |
27468 | 316 |
by (simp add: order_less_trans [OF SReal_less_omega]) |
64604 | 317 |
then have "( *f* X) (( *f* ?n) \<omega>) \<in> HInfinite" |
27468 | 318 |
by (simp add: HInfinite_def) |
319 |
with finite show "False" |
|
320 |
by (simp add: HFinite_HInfinite_iff) |
|
321 |
qed |
|
322 |
||
64604 | 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) |
|
27468 | 326 |
|
64604 | 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) |
|
27468 | 333 |
|
64604 | 334 |
text \<open>Standard Version: easily now proved using equivalence of NS and |
335 |
standard definitions.\<close> |
|
27468 | 336 |
|
64604 | 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) |
|
27468 | 340 |
|
341 |
||
64604 | 342 |
subsubsection \<open>Upper Bounds and Lubs of Bounded Sequences\<close> |
27468 | 343 |
|
64604 | 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) |
|
27468 | 346 |
|
64604 | 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 |
||
27468 | 350 |
|
64604 | 351 |
subsubsection \<open>A Bounded and Monotonic Sequence Converges\<close> |
27468 | 352 |
|
64604 | 353 |
text \<open>The best of both worlds: Easier to prove this result as a standard |
27468 | 354 |
theorem and then use equivalence to "transfer" it into the |
61975 | 355 |
equivalent nonstandard form if needed!\<close> |
27468 | 356 |
|
64604 | 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) |
|
27468 | 359 |
|
64604 | 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]) |
|
27468 | 364 |
|
365 |
||
61975 | 366 |
subsection \<open>Cauchy Sequences\<close> |
27468 | 367 |
|
368 |
lemma NSCauchyI: |
|
64604 | 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) |
|
27468 | 371 |
|
372 |
lemma NSCauchyD: |
|
64604 | 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) |
|
27468 | 375 |
|
64604 | 376 |
|
377 |
subsubsection \<open>Equivalence Between NS and Standard\<close> |
|
27468 | 378 |
|
379 |
lemma Cauchy_NSCauchy: |
|
64604 | 380 |
assumes X: "Cauchy X" |
381 |
shows "NSCauchy X" |
|
27468 | 382 |
proof (rule NSCauchyI) |
64604 | 383 |
fix M |
384 |
assume M: "M \<in> HNatInfinite" |
|
385 |
fix N |
|
386 |
assume N: "N \<in> HNatInfinite" |
|
27468 | 387 |
have "starfun X M - starfun X N \<in> Infinitesimal" |
388 |
proof (rule InfinitesimalI2) |
|
64604 | 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" |
|
27468 | 393 |
by transfer |
64604 | 394 |
then show "hnorm (starfun X M - starfun X N) < star_of r" |
27468 | 395 |
using M N by (simp add: star_of_le_HNatInfinite) |
396 |
qed |
|
64604 | 397 |
then show "starfun X M \<approx> starfun X N" |
398 |
by (simp only: approx_def) |
|
27468 | 399 |
qed |
400 |
||
401 |
lemma NSCauchy_Cauchy: |
|
64604 | 402 |
assumes X: "NSCauchy X" |
403 |
shows "Cauchy X" |
|
27468 | 404 |
proof (rule CauchyI) |
64604 | 405 |
fix r :: real |
406 |
assume r: "0 < r" |
|
27468 | 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) |
|
64604 | 409 |
fix M |
410 |
assume "whn \<le> M" |
|
27468 | 411 |
with HNatInfinite_whn have M: "M \<in> HNatInfinite" |
412 |
by (rule HNatInfinite_upward_closed) |
|
64604 | 413 |
fix N |
414 |
assume "whn \<le> N" |
|
27468 | 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) |
|
64604 | 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" |
|
27468 | 422 |
using r by (rule InfinitesimalD2) |
423 |
qed |
|
64604 | 424 |
then show "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. norm (X m - X n) < r" |
27468 | 425 |
by transfer |
426 |
qed |
|
427 |
||
428 |
theorem NSCauchy_Cauchy_iff: "NSCauchy X = Cauchy X" |
|
64604 | 429 |
by (blast intro!: NSCauchy_Cauchy Cauchy_NSCauchy) |
430 |
||
27468 | 431 |
|
61975 | 432 |
subsubsection \<open>Cauchy Sequences are Bounded\<close> |
27468 | 433 |
|
64604 | 434 |
text \<open>A Cauchy sequence is bounded -- nonstandard version.\<close> |
27468 | 435 |
|
64604 | 436 |
lemma NSCauchy_NSBseq: "NSCauchy X \<Longrightarrow> NSBseq X" |
437 |
by (simp add: Cauchy_Bseq Bseq_NSBseq_iff [symmetric] NSCauchy_Cauchy_iff) |
|
438 |
||
27468 | 439 |
|
61975 | 440 |
subsubsection \<open>Cauchy Sequences are Convergent\<close> |
27468 | 441 |
|
64604 | 442 |
text \<open>Equivalence of Cauchy criterion and convergence: |
27468 | 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 |
|
61975 | 450 |
since the NS formulations do not involve existential quantifiers.\<close> |
27468 | 451 |
|
452 |
lemma NSconvergent_NSCauchy: "NSconvergent X \<Longrightarrow> NSCauchy X" |
|
64604 | 453 |
by (simp add: NSconvergent_def NSLIMSEQ_def NSCauchy_def) (auto intro: approx_trans2) |
27468 | 454 |
|
64604 | 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 |
|
27468 | 465 |
|
64604 | 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 |
|
27468 | 471 |
|
64604 | 472 |
lemma NSCauchy_NSconvergent_iff: "NSCauchy X = NSconvergent X" |
473 |
for X :: "nat \<Rightarrow> 'a::banach" |
|
474 |
by (fast intro: NSCauchy_NSconvergent NSconvergent_NSCauchy) |
|
27468 | 475 |
|
476 |
||
61975 | 477 |
subsection \<open>Power Sequences\<close> |
27468 | 478 |
|
64604 | 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 |
|
61975 | 481 |
also fact that bounded and monotonic sequence converges.\<close> |
27468 | 482 |
|
64604 | 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 |
|
27468 | 499 |
|
64604 | 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]) |
|
27468 | 503 |
|
64604 | 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]) |
|
27468 | 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 |