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