|
1 (* Title: HOL/Nonstandard_Analysis/HSeries.thy |
|
2 Author: Jacques D. Fleuriot |
|
3 Copyright: 1998 University of Cambridge |
|
4 |
|
5 Converted to Isar and polished by lcp |
|
6 *) |
|
7 |
|
8 section\<open>Finite Summation and Infinite Series for Hyperreals\<close> |
|
9 |
|
10 theory HSeries |
|
11 imports HSEQ |
|
12 begin |
|
13 |
|
14 definition |
|
15 sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal" where |
|
16 "sumhr = |
|
17 (%(M,N,f). starfun2 (%m n. setsum f {m..<n}) M N)" |
|
18 |
|
19 definition |
|
20 NSsums :: "[nat=>real,real] => bool" (infixr "NSsums" 80) where |
|
21 "f NSsums s = (%n. setsum f {..<n}) \<longlonglongrightarrow>\<^sub>N\<^sub>S s" |
|
22 |
|
23 definition |
|
24 NSsummable :: "(nat=>real) => bool" where |
|
25 "NSsummable f = (\<exists>s. f NSsums s)" |
|
26 |
|
27 definition |
|
28 NSsuminf :: "(nat=>real) => real" where |
|
29 "NSsuminf f = (THE s. f NSsums s)" |
|
30 |
|
31 lemma sumhr_app: "sumhr(M,N,f) = ( *f2* (\<lambda>m n. setsum f {m..<n})) M N" |
|
32 by (simp add: sumhr_def) |
|
33 |
|
34 text\<open>Base case in definition of @{term sumr}\<close> |
|
35 lemma sumhr_zero [simp]: "!!m. sumhr (m,0,f) = 0" |
|
36 unfolding sumhr_app by transfer simp |
|
37 |
|
38 text\<open>Recursive case in definition of @{term sumr}\<close> |
|
39 lemma sumhr_if: |
|
40 "!!m n. sumhr(m,n+1,f) = |
|
41 (if n + 1 \<le> m then 0 else sumhr(m,n,f) + ( *f* f) n)" |
|
42 unfolding sumhr_app by transfer simp |
|
43 |
|
44 lemma sumhr_Suc_zero [simp]: "!!n. sumhr (n + 1, n, f) = 0" |
|
45 unfolding sumhr_app by transfer simp |
|
46 |
|
47 lemma sumhr_eq_bounds [simp]: "!!n. sumhr (n,n,f) = 0" |
|
48 unfolding sumhr_app by transfer simp |
|
49 |
|
50 lemma sumhr_Suc [simp]: "!!m. sumhr (m,m + 1,f) = ( *f* f) m" |
|
51 unfolding sumhr_app by transfer simp |
|
52 |
|
53 lemma sumhr_add_lbound_zero [simp]: "!!k m. sumhr(m+k,k,f) = 0" |
|
54 unfolding sumhr_app by transfer simp |
|
55 |
|
56 lemma sumhr_add: |
|
57 "!!m n. sumhr (m,n,f) + sumhr(m,n,g) = sumhr(m,n,%i. f i + g i)" |
|
58 unfolding sumhr_app by transfer (rule setsum.distrib [symmetric]) |
|
59 |
|
60 lemma sumhr_mult: |
|
61 "!!m n. hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)" |
|
62 unfolding sumhr_app by transfer (rule setsum_right_distrib) |
|
63 |
|
64 lemma sumhr_split_add: |
|
65 "!!n p. n < p ==> sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)" |
|
66 unfolding sumhr_app by transfer (simp add: setsum_add_nat_ivl) |
|
67 |
|
68 lemma sumhr_split_diff: "n<p ==> sumhr(0,p,f) - sumhr(0,n,f) = sumhr(n,p,f)" |
|
69 by (drule_tac f = f in sumhr_split_add [symmetric], simp) |
|
70 |
|
71 lemma sumhr_hrabs: "!!m n. \<bar>sumhr(m,n,f)\<bar> \<le> sumhr(m,n,%i. \<bar>f i\<bar>)" |
|
72 unfolding sumhr_app by transfer (rule setsum_abs) |
|
73 |
|
74 text\<open>other general version also needed\<close> |
|
75 lemma sumhr_fun_hypnat_eq: |
|
76 "(\<forall>r. m \<le> r & r < n --> f r = g r) --> |
|
77 sumhr(hypnat_of_nat m, hypnat_of_nat n, f) = |
|
78 sumhr(hypnat_of_nat m, hypnat_of_nat n, g)" |
|
79 unfolding sumhr_app by transfer simp |
|
80 |
|
81 lemma sumhr_const: |
|
82 "!!n. sumhr(0, n, %i. r) = hypreal_of_hypnat n * hypreal_of_real r" |
|
83 unfolding sumhr_app by transfer simp |
|
84 |
|
85 lemma sumhr_less_bounds_zero [simp]: "!!m n. n < m ==> sumhr(m,n,f) = 0" |
|
86 unfolding sumhr_app by transfer simp |
|
87 |
|
88 lemma sumhr_minus: "!!m n. sumhr(m, n, %i. - f i) = - sumhr(m, n, f)" |
|
89 unfolding sumhr_app by transfer (rule setsum_negf) |
|
90 |
|
91 lemma sumhr_shift_bounds: |
|
92 "!!m n. sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) = |
|
93 sumhr(m,n,%i. f(i + k))" |
|
94 unfolding sumhr_app by transfer (rule setsum_shift_bounds_nat_ivl) |
|
95 |
|
96 |
|
97 subsection\<open>Nonstandard Sums\<close> |
|
98 |
|
99 text\<open>Infinite sums are obtained by summing to some infinite hypernatural |
|
100 (such as @{term whn})\<close> |
|
101 lemma sumhr_hypreal_of_hypnat_omega: |
|
102 "sumhr(0,whn,%i. 1) = hypreal_of_hypnat whn" |
|
103 by (simp add: sumhr_const) |
|
104 |
|
105 lemma sumhr_hypreal_omega_minus_one: "sumhr(0, whn, %i. 1) = \<omega> - 1" |
|
106 apply (simp add: sumhr_const) |
|
107 (* FIXME: need lemma: hypreal_of_hypnat whn = \<omega> - 1 *) |
|
108 (* maybe define \<omega> = hypreal_of_hypnat whn + 1 *) |
|
109 apply (unfold star_class_defs omega_def hypnat_omega_def |
|
110 of_hypnat_def star_of_def) |
|
111 apply (simp add: starfun_star_n starfun2_star_n) |
|
112 done |
|
113 |
|
114 lemma sumhr_minus_one_realpow_zero [simp]: |
|
115 "!!N. sumhr(0, N + N, %i. (-1) ^ (i+1)) = 0" |
|
116 unfolding sumhr_app |
|
117 apply transfer |
|
118 apply (simp del: power_Suc add: mult_2 [symmetric]) |
|
119 apply (induct_tac N) |
|
120 apply simp_all |
|
121 done |
|
122 |
|
123 lemma sumhr_interval_const: |
|
124 "(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na |
|
125 ==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) = |
|
126 (hypreal_of_nat (na - m) * hypreal_of_real r)" |
|
127 unfolding sumhr_app by transfer simp |
|
128 |
|
129 lemma starfunNat_sumr: "!!N. ( *f* (%n. setsum f {0..<n})) N = sumhr(0,N,f)" |
|
130 unfolding sumhr_app by transfer (rule refl) |
|
131 |
|
132 lemma sumhr_hrabs_approx [simp]: "sumhr(0, M, f) \<approx> sumhr(0, N, f) |
|
133 ==> \<bar>sumhr(M, N, f)\<bar> \<approx> 0" |
|
134 apply (cut_tac x = M and y = N in linorder_less_linear) |
|
135 apply (auto simp add: approx_refl) |
|
136 apply (drule approx_sym [THEN approx_minus_iff [THEN iffD1]]) |
|
137 apply (auto dest: approx_hrabs |
|
138 simp add: sumhr_split_diff) |
|
139 done |
|
140 |
|
141 (*---------------------------------------------------------------- |
|
142 infinite sums: Standard and NS theorems |
|
143 ----------------------------------------------------------------*) |
|
144 lemma sums_NSsums_iff: "(f sums l) = (f NSsums l)" |
|
145 by (simp add: sums_def NSsums_def LIMSEQ_NSLIMSEQ_iff) |
|
146 |
|
147 lemma summable_NSsummable_iff: "(summable f) = (NSsummable f)" |
|
148 by (simp add: summable_def NSsummable_def sums_NSsums_iff) |
|
149 |
|
150 lemma suminf_NSsuminf_iff: "(suminf f) = (NSsuminf f)" |
|
151 by (simp add: suminf_def NSsuminf_def sums_NSsums_iff) |
|
152 |
|
153 lemma NSsums_NSsummable: "f NSsums l ==> NSsummable f" |
|
154 by (simp add: NSsums_def NSsummable_def, blast) |
|
155 |
|
156 lemma NSsummable_NSsums: "NSsummable f ==> f NSsums (NSsuminf f)" |
|
157 apply (simp add: NSsummable_def NSsuminf_def NSsums_def) |
|
158 apply (blast intro: theI NSLIMSEQ_unique) |
|
159 done |
|
160 |
|
161 lemma NSsums_unique: "f NSsums s ==> (s = NSsuminf f)" |
|
162 by (simp add: suminf_NSsuminf_iff [symmetric] sums_NSsums_iff sums_unique) |
|
163 |
|
164 lemma NSseries_zero: |
|
165 "\<forall>m. n \<le> Suc m --> f(m) = 0 ==> f NSsums (setsum f {..<n})" |
|
166 by (auto simp add: sums_NSsums_iff [symmetric] not_le[symmetric] intro!: sums_finite) |
|
167 |
|
168 lemma NSsummable_NSCauchy: |
|
169 "NSsummable f = |
|
170 (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. \<bar>sumhr(M,N,f)\<bar> \<approx> 0)" |
|
171 apply (auto simp add: summable_NSsummable_iff [symmetric] |
|
172 summable_iff_convergent convergent_NSconvergent_iff atLeast0LessThan[symmetric] |
|
173 NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_sumr) |
|
174 apply (cut_tac x = M and y = N in linorder_less_linear) |
|
175 apply auto |
|
176 apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym]) |
|
177 apply (rule_tac [2] approx_minus_iff [THEN iffD2]) |
|
178 apply (auto dest: approx_hrabs_zero_cancel |
|
179 simp add: sumhr_split_diff atLeast0LessThan[symmetric]) |
|
180 done |
|
181 |
|
182 text\<open>Terms of a convergent series tend to zero\<close> |
|
183 lemma NSsummable_NSLIMSEQ_zero: "NSsummable f ==> f \<longlonglongrightarrow>\<^sub>N\<^sub>S 0" |
|
184 apply (auto simp add: NSLIMSEQ_def NSsummable_NSCauchy) |
|
185 apply (drule bspec, auto) |
|
186 apply (drule_tac x = "N + 1 " in bspec) |
|
187 apply (auto intro: HNatInfinite_add_one approx_hrabs_zero_cancel) |
|
188 done |
|
189 |
|
190 text\<open>Nonstandard comparison test\<close> |
|
191 lemma NSsummable_comparison_test: |
|
192 "[| \<exists>N. \<forall>n. N \<le> n --> \<bar>f n\<bar> \<le> g n; NSsummable g |] ==> NSsummable f" |
|
193 apply (fold summable_NSsummable_iff) |
|
194 apply (rule summable_comparison_test, simp, assumption) |
|
195 done |
|
196 |
|
197 lemma NSsummable_rabs_comparison_test: |
|
198 "[| \<exists>N. \<forall>n. N \<le> n --> \<bar>f n\<bar> \<le> g n; NSsummable g |] |
|
199 ==> NSsummable (%k. \<bar>f k\<bar>)" |
|
200 apply (rule NSsummable_comparison_test) |
|
201 apply (auto) |
|
202 done |
|
203 |
|
204 end |