author | wenzelm |
Fri, 17 Nov 2006 02:20:03 +0100 | |
changeset 21404 | eb85850d3eb7 |
parent 20898 | 113c9516a2d7 |
child 21841 | 1701f05aa1b0 |
permissions | -rw-r--r-- |
10751 | 1 |
(* Title : HSeries.thy |
2 |
Author : Jacques D. Fleuriot |
|
3 |
Copyright : 1998 University of Cambridge |
|
14413 | 4 |
|
5 |
Converted to Isar and polished by lcp |
|
10751 | 6 |
*) |
7 |
||
14413 | 8 |
header{*Finite Summation and Infinite Series for Hyperreals*} |
10751 | 9 |
|
15131 | 10 |
theory HSeries |
15140 | 11 |
imports Series |
15131 | 12 |
begin |
10751 | 13 |
|
19765 | 14 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20898
diff
changeset
|
15 |
sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal" where |
19765 | 16 |
"sumhr = |
17 |
(%(M,N,f). starfun2 (%m n. setsum f {m..<n}) M N)" |
|
10751 | 18 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20898
diff
changeset
|
19 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20898
diff
changeset
|
20 |
NSsums :: "[nat=>real,real] => bool" (infixr "NSsums" 80) where |
19765 | 21 |
"f NSsums s = (%n. setsum f {0..<n}) ----NS> s" |
10751 | 22 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20898
diff
changeset
|
23 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20898
diff
changeset
|
24 |
NSsummable :: "(nat=>real) => bool" where |
19765 | 25 |
"NSsummable f = (\<exists>s. f NSsums s)" |
10751 | 26 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20898
diff
changeset
|
27 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20898
diff
changeset
|
28 |
NSsuminf :: "(nat=>real) => real" where |
20688 | 29 |
"NSsuminf f = (THE s. f NSsums s)" |
10751 | 30 |
|
14413 | 31 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
32 |
lemma sumhr: |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
33 |
"sumhr(star_n M, star_n N, f) = |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
34 |
star_n (%n. setsum f {M n..<N n})" |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
35 |
by (simp add: sumhr_def starfun2_star_n) |
14413 | 36 |
|
37 |
text{*Base case in definition of @{term sumr}*} |
|
38 |
lemma sumhr_zero [simp]: "sumhr (m,0,f) = 0" |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
39 |
apply (cases m) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
40 |
apply (simp add: star_n_zero_num sumhr symmetric) |
14413 | 41 |
done |
42 |
||
43 |
text{*Recursive case in definition of @{term sumr}*} |
|
44 |
lemma sumhr_if: |
|
45 |
"sumhr(m,n+1,f) = |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
46 |
(if n + 1 \<le> m then 0 else sumhr(m,n,f) + ( *f* f) n)" |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
47 |
apply (cases m, cases n) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
48 |
apply (auto simp add: star_n_one_num sumhr star_n_add star_n_le starfun |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
49 |
star_n_zero_num star_n_eq_iff, ultra+) |
14413 | 50 |
done |
51 |
||
52 |
lemma sumhr_Suc_zero [simp]: "sumhr (n + 1, n, f) = 0" |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
53 |
apply (cases n) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
54 |
apply (simp add: star_n_one_num sumhr star_n_add star_n_zero_num) |
14413 | 55 |
done |
56 |
||
57 |
lemma sumhr_eq_bounds [simp]: "sumhr (n,n,f) = 0" |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
58 |
apply (cases n) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
59 |
apply (simp add: sumhr star_n_zero_num) |
14413 | 60 |
done |
61 |
||
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
62 |
lemma sumhr_Suc [simp]: "sumhr (m,m + 1,f) = ( *f* f) m" |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
63 |
apply (cases m) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
64 |
apply (simp add: sumhr star_n_one_num star_n_add starfun) |
14413 | 65 |
done |
66 |
||
67 |
lemma sumhr_add_lbound_zero [simp]: "sumhr(m+k,k,f) = 0" |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
68 |
apply (cases m, cases k) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
69 |
apply (simp add: sumhr star_n_add star_n_zero_num) |
14413 | 70 |
done |
71 |
||
72 |
lemma sumhr_add: "sumhr (m,n,f) + sumhr(m,n,g) = sumhr(m,n,%i. f i + g i)" |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
73 |
apply (cases m, cases n) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
74 |
apply (simp add: sumhr star_n_add setsum_addf) |
14413 | 75 |
done |
76 |
||
77 |
lemma sumhr_mult: "hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)" |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
78 |
apply (cases m, cases n) |
19279 | 79 |
apply (simp add: sumhr star_of_def star_n_mult setsum_right_distrib) |
14413 | 80 |
done |
81 |
||
82 |
lemma sumhr_split_add: "n < p ==> sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)" |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
83 |
apply (cases n, cases p) |
14413 | 84 |
apply (auto elim!: FreeUltrafilterNat_subset simp |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
85 |
add: star_n_zero_num sumhr star_n_add star_n_less setsum_add_nat_ivl star_n_eq_iff) |
14413 | 86 |
done |
87 |
||
88 |
lemma sumhr_split_diff: "n<p ==> sumhr(0,p,f) - sumhr(0,n,f) = sumhr(n,p,f)" |
|
20898 | 89 |
by (drule_tac f = f in sumhr_split_add [symmetric], simp) |
14413 | 90 |
|
91 |
lemma sumhr_hrabs: "abs(sumhr(m,n,f)) \<le> sumhr(m,n,%i. abs(f i))" |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
92 |
apply (cases n, cases m) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
93 |
apply (simp add: sumhr star_n_le star_n_abs setsum_abs) |
14413 | 94 |
done |
95 |
||
96 |
text{* other general version also needed *} |
|
97 |
lemma sumhr_fun_hypnat_eq: |
|
98 |
"(\<forall>r. m \<le> r & r < n --> f r = g r) --> |
|
99 |
sumhr(hypnat_of_nat m, hypnat_of_nat n, f) = |
|
100 |
sumhr(hypnat_of_nat m, hypnat_of_nat n, g)" |
|
15536 | 101 |
by (fastsimp simp add: sumhr hypnat_of_nat_eq intro:setsum_cong) |
102 |
||
14413 | 103 |
|
15047 | 104 |
lemma sumhr_const: |
105 |
"sumhr(0, n, %i. r) = hypreal_of_hypnat n * hypreal_of_real r" |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
106 |
apply (cases n) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
107 |
apply (simp add: sumhr star_n_zero_num hypreal_of_hypnat |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
108 |
star_of_def star_n_mult real_of_nat_def) |
14413 | 109 |
done |
110 |
||
111 |
lemma sumhr_less_bounds_zero [simp]: "n < m ==> sumhr(m,n,f) = 0" |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
112 |
apply (cases m, cases n) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
113 |
apply (auto elim: FreeUltrafilterNat_subset |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
114 |
simp add: sumhr star_n_less star_n_zero_num star_n_eq_iff) |
14413 | 115 |
done |
116 |
||
117 |
lemma sumhr_minus: "sumhr(m, n, %i. - f i) = - sumhr(m, n, f)" |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
118 |
apply (cases m, cases n) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
119 |
apply (simp add: sumhr star_n_minus setsum_negf) |
14413 | 120 |
done |
121 |
||
122 |
lemma sumhr_shift_bounds: |
|
123 |
"sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) = sumhr(m,n,%i. f(i + k))" |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
124 |
apply (cases m, cases n) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
125 |
apply (simp add: sumhr star_n_add setsum_shift_bounds_nat_ivl hypnat_of_nat_eq) |
14413 | 126 |
done |
127 |
||
128 |
||
129 |
subsection{*Nonstandard Sums*} |
|
130 |
||
131 |
text{*Infinite sums are obtained by summing to some infinite hypernatural |
|
132 |
(such as @{term whn})*} |
|
133 |
lemma sumhr_hypreal_of_hypnat_omega: |
|
134 |
"sumhr(0,whn,%i. 1) = hypreal_of_hypnat whn" |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
135 |
by (simp add: hypnat_omega_def star_n_zero_num sumhr hypreal_of_hypnat |
15047 | 136 |
real_of_nat_def) |
14413 | 137 |
|
138 |
lemma sumhr_hypreal_omega_minus_one: "sumhr(0, whn, %i. 1) = omega - 1" |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
139 |
by (simp add: hypnat_omega_def star_n_zero_num omega_def star_n_one_num |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
140 |
sumhr star_n_diff real_of_nat_def) |
14413 | 141 |
|
142 |
lemma sumhr_minus_one_realpow_zero [simp]: |
|
143 |
"sumhr(0, whn + whn, %i. (-1) ^ (i+1)) = 0" |
|
144 |
by (simp del: realpow_Suc |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
145 |
add: sumhr star_n_add nat_mult_2 [symmetric] star_n_zero_num |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
146 |
star_n_zero_num hypnat_omega_def) |
14413 | 147 |
|
148 |
lemma sumhr_interval_const: |
|
149 |
"(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na |
|
150 |
==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) = |
|
151 |
(hypreal_of_nat (na - m) * hypreal_of_real r)" |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
152 |
by(simp add: sumhr hypreal_of_nat_eq hypnat_of_nat_eq |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
153 |
real_of_nat_def star_of_def star_n_mult cong: setsum_ivl_cong) |
14413 | 154 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
155 |
lemma starfunNat_sumr: "( *f* (%n. setsum f {0..<n})) N = sumhr(0,N,f)" |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
156 |
apply (cases N) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset
|
157 |
apply (simp add: star_n_zero_num starfun sumhr) |
14413 | 158 |
done |
159 |
||
160 |
lemma sumhr_hrabs_approx [simp]: "sumhr(0, M, f) @= sumhr(0, N, f) |
|
161 |
==> abs (sumhr(M, N, f)) @= 0" |
|
162 |
apply (cut_tac x = M and y = N in linorder_less_linear) |
|
163 |
apply (auto simp add: approx_refl) |
|
164 |
apply (drule approx_sym [THEN approx_minus_iff [THEN iffD1]]) |
|
165 |
apply (auto dest: approx_hrabs |
|
166 |
simp add: sumhr_split_diff diff_minus [symmetric]) |
|
167 |
done |
|
168 |
||
169 |
(*---------------------------------------------------------------- |
|
170 |
infinite sums: Standard and NS theorems |
|
171 |
----------------------------------------------------------------*) |
|
172 |
lemma sums_NSsums_iff: "(f sums l) = (f NSsums l)" |
|
173 |
by (simp add: sums_def NSsums_def LIMSEQ_NSLIMSEQ_iff) |
|
174 |
||
175 |
lemma summable_NSsummable_iff: "(summable f) = (NSsummable f)" |
|
176 |
by (simp add: summable_def NSsummable_def sums_NSsums_iff) |
|
177 |
||
178 |
lemma suminf_NSsuminf_iff: "(suminf f) = (NSsuminf f)" |
|
179 |
by (simp add: suminf_def NSsuminf_def sums_NSsums_iff) |
|
180 |
||
181 |
lemma NSsums_NSsummable: "f NSsums l ==> NSsummable f" |
|
182 |
by (simp add: NSsums_def NSsummable_def, blast) |
|
183 |
||
184 |
lemma NSsummable_NSsums: "NSsummable f ==> f NSsums (NSsuminf f)" |
|
20688 | 185 |
apply (simp add: NSsummable_def NSsuminf_def NSsums_def) |
186 |
apply (blast intro: theI NSLIMSEQ_unique) |
|
14413 | 187 |
done |
188 |
||
189 |
lemma NSsums_unique: "f NSsums s ==> (s = NSsuminf f)" |
|
190 |
by (simp add: suminf_NSsuminf_iff [symmetric] sums_NSsums_iff sums_unique) |
|
191 |
||
15539 | 192 |
lemma NSseries_zero: |
193 |
"\<forall>m. n \<le> Suc m --> f(m) = 0 ==> f NSsums (setsum f {0..<n})" |
|
14413 | 194 |
by (simp add: sums_NSsums_iff [symmetric] series_zero) |
195 |
||
196 |
lemma NSsummable_NSCauchy: |
|
197 |
"NSsummable f = |
|
198 |
(\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. abs (sumhr(M,N,f)) @= 0)" |
|
199 |
apply (auto simp add: summable_NSsummable_iff [symmetric] |
|
200 |
summable_convergent_sumr_iff convergent_NSconvergent_iff |
|
201 |
NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_sumr) |
|
202 |
apply (cut_tac x = M and y = N in linorder_less_linear) |
|
203 |
apply (auto simp add: approx_refl) |
|
204 |
apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym]) |
|
205 |
apply (rule_tac [2] approx_minus_iff [THEN iffD2]) |
|
206 |
apply (auto dest: approx_hrabs_zero_cancel |
|
207 |
simp add: sumhr_split_diff diff_minus [symmetric]) |
|
208 |
done |
|
209 |
||
210 |
||
211 |
text{*Terms of a convergent series tend to zero*} |
|
212 |
lemma NSsummable_NSLIMSEQ_zero: "NSsummable f ==> f ----NS> 0" |
|
213 |
apply (auto simp add: NSLIMSEQ_def NSsummable_NSCauchy) |
|
214 |
apply (drule bspec, auto) |
|
215 |
apply (drule_tac x = "N + 1 " in bspec) |
|
216 |
apply (auto intro: HNatInfinite_add_one approx_hrabs_zero_cancel) |
|
217 |
done |
|
218 |
||
219 |
text{*Nonstandard comparison test*} |
|
220 |
lemma NSsummable_comparison_test: |
|
221 |
"[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> g n; NSsummable g |] ==> NSsummable f" |
|
20848 | 222 |
apply (fold summable_NSsummable_iff) |
223 |
apply (rule summable_comparison_test, simp, assumption) |
|
224 |
done |
|
14413 | 225 |
|
226 |
lemma NSsummable_rabs_comparison_test: |
|
227 |
"[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> g n; NSsummable g |] |
|
228 |
==> NSsummable (%k. abs (f k))" |
|
229 |
apply (rule NSsummable_comparison_test) |
|
15543 | 230 |
apply (auto) |
14413 | 231 |
done |
232 |
||
10751 | 233 |
end |