src/HOL/NSA/HSeries.thy
author huffman
Fri Mar 30 11:16:35 2012 +0200 (2012-03-30)
changeset 47217 501b9bbd0d6e
parent 37765 26bdfb7b680b
child 51525 d3d170a2887f
permissions -rw-r--r--
removed redundant nat-specific copies of theorems
     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 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 {0..<n}) ----NS> 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{*Base case in definition of @{term sumr}*}
    35 lemma sumhr_zero [simp]: "!!m. sumhr (m,0,f) = 0"
    36 unfolding sumhr_app by transfer simp
    37 
    38 text{*Recursive case in definition of @{term sumr}*}
    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_addf [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. abs(sumhr(m,n,f)) \<le> sumhr(m,n,%i. abs(f i))"
    72 unfolding sumhr_app by transfer (rule setsum_abs)
    73 
    74 text{* other general version also needed *}
    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 add: real_of_nat_def)
    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{*Nonstandard Sums*}
    98 
    99 text{*Infinite sums are obtained by summing to some infinite hypernatural
   100  (such as @{term whn})*}
   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 real_of_nat_def)
   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 by transfer (simp del: power_Suc add: mult_2 [symmetric])
   118 
   119 lemma sumhr_interval_const:
   120      "(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na  
   121       ==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) =  
   122           (hypreal_of_nat (na - m) * hypreal_of_real r)"
   123 unfolding sumhr_app by transfer simp
   124 
   125 lemma starfunNat_sumr: "!!N. ( *f* (%n. setsum f {0..<n})) N = sumhr(0,N,f)"
   126 unfolding sumhr_app by transfer (rule refl)
   127 
   128 lemma sumhr_hrabs_approx [simp]: "sumhr(0, M, f) @= sumhr(0, N, f)  
   129       ==> abs (sumhr(M, N, f)) @= 0"
   130 apply (cut_tac x = M and y = N in linorder_less_linear)
   131 apply (auto simp add: approx_refl)
   132 apply (drule approx_sym [THEN approx_minus_iff [THEN iffD1]])
   133 apply (auto dest: approx_hrabs 
   134             simp add: sumhr_split_diff diff_minus [symmetric])
   135 done
   136 
   137 (*----------------------------------------------------------------
   138       infinite sums: Standard and NS theorems
   139  ----------------------------------------------------------------*)
   140 lemma sums_NSsums_iff: "(f sums l) = (f NSsums l)"
   141 by (simp add: sums_def NSsums_def LIMSEQ_NSLIMSEQ_iff)
   142 
   143 lemma summable_NSsummable_iff: "(summable f) = (NSsummable f)"
   144 by (simp add: summable_def NSsummable_def sums_NSsums_iff)
   145 
   146 lemma suminf_NSsuminf_iff: "(suminf f) = (NSsuminf f)"
   147 by (simp add: suminf_def NSsuminf_def sums_NSsums_iff)
   148 
   149 lemma NSsums_NSsummable: "f NSsums l ==> NSsummable f"
   150 by (simp add: NSsums_def NSsummable_def, blast)
   151 
   152 lemma NSsummable_NSsums: "NSsummable f ==> f NSsums (NSsuminf f)"
   153 apply (simp add: NSsummable_def NSsuminf_def NSsums_def)
   154 apply (blast intro: theI NSLIMSEQ_unique)
   155 done
   156 
   157 lemma NSsums_unique: "f NSsums s ==> (s = NSsuminf f)"
   158 by (simp add: suminf_NSsuminf_iff [symmetric] sums_NSsums_iff sums_unique)
   159 
   160 lemma NSseries_zero:
   161   "\<forall>m. n \<le> Suc m --> f(m) = 0 ==> f NSsums (setsum f {0..<n})"
   162 by (simp add: sums_NSsums_iff [symmetric] series_zero)
   163 
   164 lemma NSsummable_NSCauchy:
   165      "NSsummable f =  
   166       (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. abs (sumhr(M,N,f)) @= 0)"
   167 apply (auto simp add: summable_NSsummable_iff [symmetric] 
   168        summable_convergent_sumr_iff convergent_NSconvergent_iff 
   169        NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_sumr)
   170 apply (cut_tac x = M and y = N in linorder_less_linear)
   171 apply (auto simp add: approx_refl)
   172 apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])
   173 apply (rule_tac [2] approx_minus_iff [THEN iffD2])
   174 apply (auto dest: approx_hrabs_zero_cancel 
   175             simp add: sumhr_split_diff diff_minus [symmetric])
   176 done
   177 
   178 
   179 text{*Terms of a convergent series tend to zero*}
   180 lemma NSsummable_NSLIMSEQ_zero: "NSsummable f ==> f ----NS> 0"
   181 apply (auto simp add: NSLIMSEQ_def NSsummable_NSCauchy)
   182 apply (drule bspec, auto)
   183 apply (drule_tac x = "N + 1 " in bspec)
   184 apply (auto intro: HNatInfinite_add_one approx_hrabs_zero_cancel)
   185 done
   186 
   187 text{*Nonstandard comparison test*}
   188 lemma NSsummable_comparison_test:
   189      "[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> g n; NSsummable g |] ==> NSsummable f"
   190 apply (fold summable_NSsummable_iff)
   191 apply (rule summable_comparison_test, simp, assumption)
   192 done
   193 
   194 lemma NSsummable_rabs_comparison_test:
   195      "[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> g n; NSsummable g |]
   196       ==> NSsummable (%k. abs (f k))"
   197 apply (rule NSsummable_comparison_test)
   198 apply (auto)
   199 done
   200 
   201 end