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