src/HOL/Hyperreal/HSeries.thy
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 15131 c69542757a4d
child 15536 3ce1cb7a24f0
permissions -rw-r--r--
import -> imports
     1 (*  Title       : 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 header{*Finite Summation and Infinite Series for Hyperreals*}
     9 
    10 theory HSeries
    11 imports Series
    12 begin
    13 
    14 constdefs 
    15   sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal"
    16    "sumhr p == 
    17       (%(M,N,f). Abs_hypreal(\<Union>X \<in> Rep_hypnat(M). \<Union>Y \<in> Rep_hypnat(N).  
    18                              hyprel ``{%n::nat. sumr (X n) (Y n) f})) p"
    19 
    20   NSsums  :: "[nat=>real,real] => bool"     (infixr "NSsums" 80)
    21    "f NSsums s  == (%n. sumr 0 n f) ----NS> s"
    22 
    23   NSsummable :: "(nat=>real) => bool"
    24    "NSsummable f == (\<exists>s. f NSsums s)"
    25 
    26   NSsuminf   :: "(nat=>real) => real"
    27    "NSsuminf f == (@s. f NSsums s)"
    28 
    29 
    30 lemma sumhr: 
    31      "sumhr(Abs_hypnat(hypnatrel``{%n. M n}),  
    32             Abs_hypnat(hypnatrel``{%n. N n}), f) =  
    33       Abs_hypreal(hyprel `` {%n. sumr (M n) (N n) f})"
    34 apply (simp add: sumhr_def)
    35 apply (rule arg_cong [where f = Abs_hypreal]) 
    36 apply (auto, ultra)
    37 done
    38 
    39 text{*Base case in definition of @{term sumr}*}
    40 lemma sumhr_zero [simp]: "sumhr (m,0,f) = 0"
    41 apply (cases m)
    42 apply (simp add: hypnat_zero_def sumhr symmetric hypreal_zero_def)
    43 done
    44 
    45 text{*Recursive case in definition of @{term sumr}*}
    46 lemma sumhr_if: 
    47      "sumhr(m,n+1,f) = 
    48       (if n + 1 \<le> m then 0 else sumhr(m,n,f) + ( *fNat* f) n)"
    49 apply (cases m, cases n)
    50 apply (auto simp add: hypnat_one_def sumhr hypnat_add hypnat_le starfunNat
    51            hypreal_add hypreal_zero_def,   ultra+)
    52 done
    53 
    54 lemma sumhr_Suc_zero [simp]: "sumhr (n + 1, n, f) = 0"
    55 apply (cases n)
    56 apply (simp add: hypnat_one_def sumhr hypnat_add hypreal_zero_def)
    57 done
    58 
    59 lemma sumhr_eq_bounds [simp]: "sumhr (n,n,f) = 0"
    60 apply (cases n)
    61 apply (simp add: sumhr hypreal_zero_def)
    62 done
    63 
    64 lemma sumhr_Suc [simp]: "sumhr (m,m + 1,f) = ( *fNat* f) m"
    65 apply (cases m)
    66 apply (simp add: sumhr hypnat_one_def  hypnat_add starfunNat)
    67 done
    68 
    69 lemma sumhr_add_lbound_zero [simp]: "sumhr(m+k,k,f) = 0"
    70 apply (cases m, cases k)
    71 apply (simp add: sumhr hypnat_add hypreal_zero_def)
    72 done
    73 
    74 lemma sumhr_add: "sumhr (m,n,f) + sumhr(m,n,g) = sumhr(m,n,%i. f i + g i)"
    75 apply (cases m, cases n)
    76 apply (simp add: sumhr hypreal_add sumr_add)
    77 done
    78 
    79 lemma sumhr_mult: "hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)"
    80 apply (cases m, cases n)
    81 apply (simp add: sumhr hypreal_of_real_def hypreal_mult sumr_mult)
    82 done
    83 
    84 lemma sumhr_split_add: "n < p ==> sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)"
    85 apply (cases n, cases p)
    86 apply (auto elim!: FreeUltrafilterNat_subset simp 
    87             add: hypnat_zero_def sumhr hypreal_add hypnat_less sumr_split_add)
    88 done
    89 
    90 lemma sumhr_split_diff: "n<p ==> sumhr(0,p,f) - sumhr(0,n,f) = sumhr(n,p,f)"
    91 by (drule_tac f1 = f in sumhr_split_add [symmetric], simp)
    92 
    93 lemma sumhr_hrabs: "abs(sumhr(m,n,f)) \<le> sumhr(m,n,%i. abs(f i))"
    94 apply (cases n, cases m)
    95 apply (simp add: sumhr hypreal_le hypreal_hrabs sumr_rabs)
    96 done
    97 
    98 text{* other general version also needed *}
    99 lemma sumhr_fun_hypnat_eq:
   100    "(\<forall>r. m \<le> r & r < n --> f r = g r) -->  
   101       sumhr(hypnat_of_nat m, hypnat_of_nat n, f) =  
   102       sumhr(hypnat_of_nat m, hypnat_of_nat n, g)"
   103 apply (safe, drule sumr_fun_eq)
   104 apply (simp add: sumhr hypnat_of_nat_eq)
   105 done
   106 
   107 lemma sumhr_const:
   108      "sumhr(0, n, %i. r) = hypreal_of_hypnat n * hypreal_of_real r"
   109 apply (cases n)
   110 apply (simp add: sumhr hypnat_zero_def hypreal_of_real_def hypreal_of_hypnat 
   111                  hypreal_mult real_of_nat_def)
   112 done
   113 
   114 lemma sumhr_less_bounds_zero [simp]: "n < m ==> sumhr(m,n,f) = 0"
   115 apply (cases m, cases n)
   116 apply (auto elim: FreeUltrafilterNat_subset 
   117             simp add: sumhr hypnat_less hypreal_zero_def)
   118 done
   119 
   120 lemma sumhr_minus: "sumhr(m, n, %i. - f i) = - sumhr(m, n, f)"
   121 apply (cases m, cases n)
   122 apply (simp add: sumhr hypreal_minus sumr_minus)
   123 done
   124 
   125 lemma sumhr_shift_bounds:
   126      "sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) = sumhr(m,n,%i. f(i + k))"
   127 apply (cases m, cases n)
   128 apply (simp add: sumhr hypnat_add sumr_shift_bounds hypnat_of_nat_eq)
   129 done
   130 
   131 
   132 subsection{*Nonstandard Sums*}
   133 
   134 text{*Infinite sums are obtained by summing to some infinite hypernatural
   135  (such as @{term whn})*}
   136 lemma sumhr_hypreal_of_hypnat_omega: 
   137       "sumhr(0,whn,%i. 1) = hypreal_of_hypnat whn"
   138 by (simp add: hypnat_omega_def hypnat_zero_def sumhr hypreal_of_hypnat
   139               real_of_nat_def)
   140 
   141 lemma sumhr_hypreal_omega_minus_one: "sumhr(0, whn, %i. 1) = omega - 1"
   142 by (simp add: hypnat_omega_def hypnat_zero_def omega_def hypreal_one_def
   143               sumhr hypreal_diff real_of_nat_def)
   144 
   145 lemma sumhr_minus_one_realpow_zero [simp]: 
   146      "sumhr(0, whn + whn, %i. (-1) ^ (i+1)) = 0"
   147 by (simp del: realpow_Suc 
   148          add: sumhr hypnat_add nat_mult_2 [symmetric] hypreal_zero_def 
   149               hypnat_zero_def hypnat_omega_def)
   150 
   151 lemma sumhr_interval_const:
   152      "(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na  
   153       ==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) =  
   154           (hypreal_of_nat (na - m) * hypreal_of_real r)"
   155 by (auto dest!: sumr_interval_const 
   156          simp add: hypreal_of_real_def sumhr hypreal_of_nat_eq 
   157                    hypnat_of_nat_eq hypreal_of_real_def hypreal_mult)
   158 
   159 lemma starfunNat_sumr: "( *fNat* (%n. sumr 0 n f)) N = sumhr(0,N,f)"
   160 apply (cases N)
   161 apply (simp add: hypnat_zero_def starfunNat sumhr)
   162 done
   163 
   164 lemma sumhr_hrabs_approx [simp]: "sumhr(0, M, f) @= sumhr(0, N, f)  
   165       ==> abs (sumhr(M, N, f)) @= 0"
   166 apply (cut_tac x = M and y = N in linorder_less_linear)
   167 apply (auto simp add: approx_refl)
   168 apply (drule approx_sym [THEN approx_minus_iff [THEN iffD1]])
   169 apply (auto dest: approx_hrabs 
   170             simp add: sumhr_split_diff diff_minus [symmetric])
   171 done
   172 
   173 (*----------------------------------------------------------------
   174       infinite sums: Standard and NS theorems
   175  ----------------------------------------------------------------*)
   176 lemma sums_NSsums_iff: "(f sums l) = (f NSsums l)"
   177 by (simp add: sums_def NSsums_def LIMSEQ_NSLIMSEQ_iff)
   178 
   179 lemma summable_NSsummable_iff: "(summable f) = (NSsummable f)"
   180 by (simp add: summable_def NSsummable_def sums_NSsums_iff)
   181 
   182 lemma suminf_NSsuminf_iff: "(suminf f) = (NSsuminf f)"
   183 by (simp add: suminf_def NSsuminf_def sums_NSsums_iff)
   184 
   185 lemma NSsums_NSsummable: "f NSsums l ==> NSsummable f"
   186 by (simp add: NSsums_def NSsummable_def, blast)
   187 
   188 lemma NSsummable_NSsums: "NSsummable f ==> f NSsums (NSsuminf f)"
   189 apply (simp add: NSsummable_def NSsuminf_def)
   190 apply (blast intro: someI2)
   191 done
   192 
   193 lemma NSsums_unique: "f NSsums s ==> (s = NSsuminf f)"
   194 by (simp add: suminf_NSsuminf_iff [symmetric] sums_NSsums_iff sums_unique)
   195 
   196 lemma NSseries_zero: "\<forall>m. n \<le> Suc m --> f(m) = 0 ==> f NSsums (sumr 0 n f)"
   197 by (simp add: sums_NSsums_iff [symmetric] series_zero)
   198 
   199 lemma NSsummable_NSCauchy:
   200      "NSsummable f =  
   201       (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. abs (sumhr(M,N,f)) @= 0)"
   202 apply (auto simp add: summable_NSsummable_iff [symmetric] 
   203        summable_convergent_sumr_iff convergent_NSconvergent_iff 
   204        NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_sumr)
   205 apply (cut_tac x = M and y = N in linorder_less_linear)
   206 apply (auto simp add: approx_refl)
   207 apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])
   208 apply (rule_tac [2] approx_minus_iff [THEN iffD2])
   209 apply (auto dest: approx_hrabs_zero_cancel 
   210             simp add: sumhr_split_diff diff_minus [symmetric])
   211 done
   212 
   213 
   214 text{*Terms of a convergent series tend to zero*}
   215 lemma NSsummable_NSLIMSEQ_zero: "NSsummable f ==> f ----NS> 0"
   216 apply (auto simp add: NSLIMSEQ_def NSsummable_NSCauchy)
   217 apply (drule bspec, auto)
   218 apply (drule_tac x = "N + 1 " in bspec)
   219 apply (auto intro: HNatInfinite_add_one approx_hrabs_zero_cancel)
   220 done
   221 
   222 text{* Easy to prove stsandard case now *}
   223 lemma summable_LIMSEQ_zero: "summable f ==> f ----> 0"
   224 by (simp add: summable_NSsummable_iff LIMSEQ_NSLIMSEQ_iff NSsummable_NSLIMSEQ_zero)
   225 
   226 text{*Nonstandard comparison test*}
   227 lemma NSsummable_comparison_test:
   228      "[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> g n; NSsummable g |] ==> NSsummable f"
   229 by (auto intro: summable_comparison_test 
   230          simp add: summable_NSsummable_iff [symmetric])
   231 
   232 lemma NSsummable_rabs_comparison_test:
   233      "[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> g n; NSsummable g |]
   234       ==> NSsummable (%k. abs (f k))"
   235 apply (rule NSsummable_comparison_test)
   236 apply (auto simp add: abs_idempotent)
   237 done
   238 
   239 ML
   240 {*
   241 val sumhr = thm "sumhr";
   242 val sumhr_zero = thm "sumhr_zero";
   243 val sumhr_if = thm "sumhr_if";
   244 val sumhr_Suc_zero = thm "sumhr_Suc_zero";
   245 val sumhr_eq_bounds = thm "sumhr_eq_bounds";
   246 val sumhr_Suc = thm "sumhr_Suc";
   247 val sumhr_add_lbound_zero = thm "sumhr_add_lbound_zero";
   248 val sumhr_add = thm "sumhr_add";
   249 val sumhr_mult = thm "sumhr_mult";
   250 val sumhr_split_add = thm "sumhr_split_add";
   251 val sumhr_split_diff = thm "sumhr_split_diff";
   252 val sumhr_hrabs = thm "sumhr_hrabs";
   253 val sumhr_fun_hypnat_eq = thm "sumhr_fun_hypnat_eq";
   254 val sumhr_less_bounds_zero = thm "sumhr_less_bounds_zero";
   255 val sumhr_minus = thm "sumhr_minus";
   256 val sumhr_shift_bounds = thm "sumhr_shift_bounds";
   257 val sumhr_hypreal_of_hypnat_omega = thm "sumhr_hypreal_of_hypnat_omega";
   258 val sumhr_hypreal_omega_minus_one = thm "sumhr_hypreal_omega_minus_one";
   259 val sumhr_minus_one_realpow_zero = thm "sumhr_minus_one_realpow_zero";
   260 val sumhr_interval_const = thm "sumhr_interval_const";
   261 val starfunNat_sumr = thm "starfunNat_sumr";
   262 val sumhr_hrabs_approx = thm "sumhr_hrabs_approx";
   263 val sums_NSsums_iff = thm "sums_NSsums_iff";
   264 val summable_NSsummable_iff = thm "summable_NSsummable_iff";
   265 val suminf_NSsuminf_iff = thm "suminf_NSsuminf_iff";
   266 val NSsums_NSsummable = thm "NSsums_NSsummable";
   267 val NSsummable_NSsums = thm "NSsummable_NSsums";
   268 val NSsums_unique = thm "NSsums_unique";
   269 val NSseries_zero = thm "NSseries_zero";
   270 val NSsummable_NSCauchy = thm "NSsummable_NSCauchy";
   271 val NSsummable_NSLIMSEQ_zero = thm "NSsummable_NSLIMSEQ_zero";
   272 val summable_LIMSEQ_zero = thm "summable_LIMSEQ_zero";
   273 val NSsummable_comparison_test = thm "NSsummable_comparison_test";
   274 val NSsummable_rabs_comparison_test = thm "NSsummable_rabs_comparison_test";
   275 *}
   276 
   277 end