src/HOL/NSA/HSeries.thy
author huffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 47220 52426c62b5d0
parent 47217 501b9bbd0d6e
child 51525 d3d170a2887f
permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
huffman@27468
     1
(*  Title       : HSeries.thy
huffman@27468
     2
    Author      : Jacques D. Fleuriot
huffman@27468
     3
    Copyright   : 1998  University of Cambridge
huffman@27468
     4
huffman@27468
     5
Converted to Isar and polished by lcp    
huffman@27468
     6
*) 
huffman@27468
     7
huffman@27468
     8
header{*Finite Summation and Infinite Series for Hyperreals*}
huffman@27468
     9
huffman@27468
    10
theory HSeries
huffman@27468
    11
imports Series HSEQ
huffman@27468
    12
begin
huffman@27468
    13
huffman@27468
    14
definition
huffman@27468
    15
  sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal" where
haftmann@37765
    16
  "sumhr = 
huffman@27468
    17
      (%(M,N,f). starfun2 (%m n. setsum f {m..<n}) M N)"
huffman@27468
    18
huffman@27468
    19
definition
huffman@27468
    20
  NSsums  :: "[nat=>real,real] => bool"     (infixr "NSsums" 80) where
huffman@27468
    21
  "f NSsums s = (%n. setsum f {0..<n}) ----NS> s"
huffman@27468
    22
huffman@27468
    23
definition
huffman@27468
    24
  NSsummable :: "(nat=>real) => bool" where
haftmann@37765
    25
  "NSsummable f = (\<exists>s. f NSsums s)"
huffman@27468
    26
huffman@27468
    27
definition
huffman@27468
    28
  NSsuminf   :: "(nat=>real) => real" where
huffman@27468
    29
  "NSsuminf f = (THE s. f NSsums s)"
huffman@27468
    30
huffman@27468
    31
lemma sumhr_app: "sumhr(M,N,f) = ( *f2* (\<lambda>m n. setsum f {m..<n})) M N"
huffman@27468
    32
by (simp add: sumhr_def)
huffman@27468
    33
huffman@27468
    34
text{*Base case in definition of @{term sumr}*}
huffman@27468
    35
lemma sumhr_zero [simp]: "!!m. sumhr (m,0,f) = 0"
huffman@27468
    36
unfolding sumhr_app by transfer simp
huffman@27468
    37
huffman@27468
    38
text{*Recursive case in definition of @{term sumr}*}
huffman@27468
    39
lemma sumhr_if: 
huffman@27468
    40
     "!!m n. sumhr(m,n+1,f) = 
huffman@27468
    41
      (if n + 1 \<le> m then 0 else sumhr(m,n,f) + ( *f* f) n)"
huffman@27468
    42
unfolding sumhr_app by transfer simp
huffman@27468
    43
huffman@27468
    44
lemma sumhr_Suc_zero [simp]: "!!n. sumhr (n + 1, n, f) = 0"
huffman@27468
    45
unfolding sumhr_app by transfer simp
huffman@27468
    46
huffman@27468
    47
lemma sumhr_eq_bounds [simp]: "!!n. sumhr (n,n,f) = 0"
huffman@27468
    48
unfolding sumhr_app by transfer simp
huffman@27468
    49
huffman@27468
    50
lemma sumhr_Suc [simp]: "!!m. sumhr (m,m + 1,f) = ( *f* f) m"
huffman@27468
    51
unfolding sumhr_app by transfer simp
huffman@27468
    52
huffman@27468
    53
lemma sumhr_add_lbound_zero [simp]: "!!k m. sumhr(m+k,k,f) = 0"
huffman@27468
    54
unfolding sumhr_app by transfer simp
huffman@27468
    55
huffman@27468
    56
lemma sumhr_add:
huffman@27468
    57
  "!!m n. sumhr (m,n,f) + sumhr(m,n,g) = sumhr(m,n,%i. f i + g i)"
huffman@27468
    58
unfolding sumhr_app by transfer (rule setsum_addf [symmetric])
huffman@27468
    59
huffman@27468
    60
lemma sumhr_mult:
huffman@27468
    61
  "!!m n. hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)"
huffman@27468
    62
unfolding sumhr_app by transfer (rule setsum_right_distrib)
huffman@27468
    63
huffman@27468
    64
lemma sumhr_split_add:
huffman@27468
    65
  "!!n p. n < p ==> sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)"
huffman@27468
    66
unfolding sumhr_app by transfer (simp add: setsum_add_nat_ivl)
huffman@27468
    67
huffman@27468
    68
lemma sumhr_split_diff: "n<p ==> sumhr(0,p,f) - sumhr(0,n,f) = sumhr(n,p,f)"
huffman@27468
    69
by (drule_tac f = f in sumhr_split_add [symmetric], simp)
huffman@27468
    70
huffman@27468
    71
lemma sumhr_hrabs: "!!m n. abs(sumhr(m,n,f)) \<le> sumhr(m,n,%i. abs(f i))"
huffman@27468
    72
unfolding sumhr_app by transfer (rule setsum_abs)
huffman@27468
    73
huffman@27468
    74
text{* other general version also needed *}
huffman@27468
    75
lemma sumhr_fun_hypnat_eq:
huffman@27468
    76
   "(\<forall>r. m \<le> r & r < n --> f r = g r) -->  
huffman@27468
    77
      sumhr(hypnat_of_nat m, hypnat_of_nat n, f) =  
huffman@27468
    78
      sumhr(hypnat_of_nat m, hypnat_of_nat n, g)"
huffman@27468
    79
unfolding sumhr_app by transfer simp
huffman@27468
    80
huffman@27468
    81
lemma sumhr_const:
huffman@27468
    82
     "!!n. sumhr(0, n, %i. r) = hypreal_of_hypnat n * hypreal_of_real r"
huffman@27468
    83
unfolding sumhr_app by transfer (simp add: real_of_nat_def)
huffman@27468
    84
huffman@27468
    85
lemma sumhr_less_bounds_zero [simp]: "!!m n. n < m ==> sumhr(m,n,f) = 0"
huffman@27468
    86
unfolding sumhr_app by transfer simp
huffman@27468
    87
huffman@27468
    88
lemma sumhr_minus: "!!m n. sumhr(m, n, %i. - f i) = - sumhr(m, n, f)"
huffman@27468
    89
unfolding sumhr_app by transfer (rule setsum_negf)
huffman@27468
    90
huffman@27468
    91
lemma sumhr_shift_bounds:
huffman@27468
    92
  "!!m n. sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) =
huffman@27468
    93
          sumhr(m,n,%i. f(i + k))"
huffman@27468
    94
unfolding sumhr_app by transfer (rule setsum_shift_bounds_nat_ivl)
huffman@27468
    95
huffman@27468
    96
huffman@27468
    97
subsection{*Nonstandard Sums*}
huffman@27468
    98
huffman@27468
    99
text{*Infinite sums are obtained by summing to some infinite hypernatural
huffman@27468
   100
 (such as @{term whn})*}
huffman@27468
   101
lemma sumhr_hypreal_of_hypnat_omega: 
huffman@27468
   102
      "sumhr(0,whn,%i. 1) = hypreal_of_hypnat whn"
huffman@27468
   103
by (simp add: sumhr_const)
huffman@27468
   104
huffman@27468
   105
lemma sumhr_hypreal_omega_minus_one: "sumhr(0, whn, %i. 1) = omega - 1"
huffman@27468
   106
apply (simp add: sumhr_const)
huffman@27468
   107
(* FIXME: need lemma: hypreal_of_hypnat whn = omega - 1 *)
huffman@27468
   108
(* maybe define omega = hypreal_of_hypnat whn + 1 *)
huffman@27468
   109
apply (unfold star_class_defs omega_def hypnat_omega_def
huffman@27468
   110
              of_hypnat_def star_of_def)
huffman@27468
   111
apply (simp add: starfun_star_n starfun2_star_n real_of_nat_def)
huffman@27468
   112
done
huffman@27468
   113
huffman@27468
   114
lemma sumhr_minus_one_realpow_zero [simp]: 
huffman@27468
   115
     "!!N. sumhr(0, N + N, %i. (-1) ^ (i+1)) = 0"
huffman@27468
   116
unfolding sumhr_app
huffman@47217
   117
by transfer (simp del: power_Suc add: mult_2 [symmetric])
huffman@27468
   118
huffman@27468
   119
lemma sumhr_interval_const:
huffman@27468
   120
     "(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na  
huffman@27468
   121
      ==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) =  
huffman@27468
   122
          (hypreal_of_nat (na - m) * hypreal_of_real r)"
huffman@27468
   123
unfolding sumhr_app by transfer simp
huffman@27468
   124
huffman@27468
   125
lemma starfunNat_sumr: "!!N. ( *f* (%n. setsum f {0..<n})) N = sumhr(0,N,f)"
huffman@27468
   126
unfolding sumhr_app by transfer (rule refl)
huffman@27468
   127
huffman@27468
   128
lemma sumhr_hrabs_approx [simp]: "sumhr(0, M, f) @= sumhr(0, N, f)  
huffman@27468
   129
      ==> abs (sumhr(M, N, f)) @= 0"
huffman@27468
   130
apply (cut_tac x = M and y = N in linorder_less_linear)
huffman@27468
   131
apply (auto simp add: approx_refl)
huffman@27468
   132
apply (drule approx_sym [THEN approx_minus_iff [THEN iffD1]])
huffman@27468
   133
apply (auto dest: approx_hrabs 
huffman@27468
   134
            simp add: sumhr_split_diff diff_minus [symmetric])
huffman@27468
   135
done
huffman@27468
   136
huffman@27468
   137
(*----------------------------------------------------------------
huffman@27468
   138
      infinite sums: Standard and NS theorems
huffman@27468
   139
 ----------------------------------------------------------------*)
huffman@27468
   140
lemma sums_NSsums_iff: "(f sums l) = (f NSsums l)"
huffman@27468
   141
by (simp add: sums_def NSsums_def LIMSEQ_NSLIMSEQ_iff)
huffman@27468
   142
huffman@27468
   143
lemma summable_NSsummable_iff: "(summable f) = (NSsummable f)"
huffman@27468
   144
by (simp add: summable_def NSsummable_def sums_NSsums_iff)
huffman@27468
   145
huffman@27468
   146
lemma suminf_NSsuminf_iff: "(suminf f) = (NSsuminf f)"
huffman@27468
   147
by (simp add: suminf_def NSsuminf_def sums_NSsums_iff)
huffman@27468
   148
huffman@27468
   149
lemma NSsums_NSsummable: "f NSsums l ==> NSsummable f"
huffman@27468
   150
by (simp add: NSsums_def NSsummable_def, blast)
huffman@27468
   151
huffman@27468
   152
lemma NSsummable_NSsums: "NSsummable f ==> f NSsums (NSsuminf f)"
huffman@27468
   153
apply (simp add: NSsummable_def NSsuminf_def NSsums_def)
huffman@27468
   154
apply (blast intro: theI NSLIMSEQ_unique)
huffman@27468
   155
done
huffman@27468
   156
huffman@27468
   157
lemma NSsums_unique: "f NSsums s ==> (s = NSsuminf f)"
huffman@27468
   158
by (simp add: suminf_NSsuminf_iff [symmetric] sums_NSsums_iff sums_unique)
huffman@27468
   159
huffman@27468
   160
lemma NSseries_zero:
huffman@27468
   161
  "\<forall>m. n \<le> Suc m --> f(m) = 0 ==> f NSsums (setsum f {0..<n})"
huffman@27468
   162
by (simp add: sums_NSsums_iff [symmetric] series_zero)
huffman@27468
   163
huffman@27468
   164
lemma NSsummable_NSCauchy:
huffman@27468
   165
     "NSsummable f =  
huffman@27468
   166
      (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. abs (sumhr(M,N,f)) @= 0)"
huffman@27468
   167
apply (auto simp add: summable_NSsummable_iff [symmetric] 
huffman@27468
   168
       summable_convergent_sumr_iff convergent_NSconvergent_iff 
huffman@27468
   169
       NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_sumr)
huffman@27468
   170
apply (cut_tac x = M and y = N in linorder_less_linear)
huffman@27468
   171
apply (auto simp add: approx_refl)
huffman@27468
   172
apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])
huffman@27468
   173
apply (rule_tac [2] approx_minus_iff [THEN iffD2])
huffman@27468
   174
apply (auto dest: approx_hrabs_zero_cancel 
huffman@27468
   175
            simp add: sumhr_split_diff diff_minus [symmetric])
huffman@27468
   176
done
huffman@27468
   177
huffman@27468
   178
huffman@27468
   179
text{*Terms of a convergent series tend to zero*}
huffman@27468
   180
lemma NSsummable_NSLIMSEQ_zero: "NSsummable f ==> f ----NS> 0"
huffman@27468
   181
apply (auto simp add: NSLIMSEQ_def NSsummable_NSCauchy)
huffman@27468
   182
apply (drule bspec, auto)
huffman@27468
   183
apply (drule_tac x = "N + 1 " in bspec)
huffman@27468
   184
apply (auto intro: HNatInfinite_add_one approx_hrabs_zero_cancel)
huffman@27468
   185
done
huffman@27468
   186
huffman@27468
   187
text{*Nonstandard comparison test*}
huffman@27468
   188
lemma NSsummable_comparison_test:
huffman@27468
   189
     "[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> g n; NSsummable g |] ==> NSsummable f"
huffman@27468
   190
apply (fold summable_NSsummable_iff)
huffman@27468
   191
apply (rule summable_comparison_test, simp, assumption)
huffman@27468
   192
done
huffman@27468
   193
huffman@27468
   194
lemma NSsummable_rabs_comparison_test:
huffman@27468
   195
     "[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> g n; NSsummable g |]
huffman@27468
   196
      ==> NSsummable (%k. abs (f k))"
huffman@27468
   197
apply (rule NSsummable_comparison_test)
huffman@27468
   198
apply (auto)
huffman@27468
   199
done
huffman@27468
   200
huffman@27468
   201
end