Theory HSeries

(*  Title:      HOL/Nonstandard_Analysis/HSeries.thy
    Author:     Jacques D. Fleuriot
    Copyright:  1998  University of Cambridge

Converted to Isar and polished by lcp
*)

section Finite Summation and Infinite Series for Hyperreals

theory HSeries
  imports HSEQ
begin

definition sumhr :: "hypnat × hypnat × (nat  real)  hypreal"
  where "sumhr = (λ(M,N,f). starfun2 (λm n. sum f {m..<n}) M N)"

definition NSsums :: "(nat  real)  real  bool"  (infixr "NSsums" 80)
  where "f NSsums s = (λn. sum f {..<n}) NS s"

definition NSsummable :: "(nat  real)  bool"
  where "NSsummable f  (s. f NSsums s)"

definition NSsuminf :: "(nat  real)  real"
  where "NSsuminf f = (THE s. f NSsums s)"

lemma sumhr_app: "sumhr (M, N, f) = ( *f2* (λm n. sum f {m..<n})) M N"
  by (simp add: sumhr_def)

text Base case in definition of termsumr.
lemma sumhr_zero [simp]: "m. sumhr (m, 0, f) = 0"
  unfolding sumhr_app by transfer simp

text Recursive case in definition of termsumr.
lemma sumhr_if:
  "m n. sumhr (m, n + 1, f) = (if n + 1  m then 0 else sumhr (m, n, f) + ( *f* f) n)"
  unfolding sumhr_app by transfer simp

lemma sumhr_Suc_zero [simp]: "n. sumhr (n + 1, n, f) = 0"
  unfolding sumhr_app by transfer simp

lemma sumhr_eq_bounds [simp]: "n. sumhr (n, n, f) = 0"
  unfolding sumhr_app by transfer simp

lemma sumhr_Suc [simp]: "m. sumhr (m, m + 1, f) = ( *f* f) m"
  unfolding sumhr_app by transfer simp

lemma sumhr_add_lbound_zero [simp]: "k m. sumhr (m + k, k, f) = 0"
  unfolding sumhr_app by transfer simp

lemma sumhr_add: "m n. sumhr (m, n, f) + sumhr (m, n, g) = sumhr (m, n, λi. f i + g i)"
  unfolding sumhr_app by transfer (rule sum.distrib [symmetric])

lemma sumhr_mult: "m n. hypreal_of_real r * sumhr (m, n, f) = sumhr (m, n, λn. r * f n)"
  unfolding sumhr_app by transfer (rule sum_distrib_left)

lemma sumhr_split_add: "n p. n < p  sumhr (0, n, f) + sumhr (n, p, f) = sumhr (0, p, f)"
  unfolding sumhr_app by transfer (simp add: sum.atLeastLessThan_concat)

lemma sumhr_split_diff: "n < p  sumhr (0, p, f) - sumhr (0, n, f) = sumhr (n, p, f)"
  by (drule sumhr_split_add [symmetric, where f = f]) simp

lemma sumhr_hrabs: "m n. ¦sumhr (m, n, f)¦  sumhr (m, n, λi. ¦f i¦)"
  unfolding sumhr_app by transfer (rule sum_abs)

text Other general version also needed.
lemma sumhr_fun_hypnat_eq:
  "(r. m  r  r < n  f r = g r) 
    sumhr (hypnat_of_nat m, hypnat_of_nat n, f) =
    sumhr (hypnat_of_nat m, hypnat_of_nat n, g)"
  unfolding sumhr_app by transfer simp

lemma sumhr_const: "n. sumhr (0, n, λi. r) = hypreal_of_hypnat n * hypreal_of_real r"
  unfolding sumhr_app by transfer simp

lemma sumhr_less_bounds_zero [simp]: "m n. n < m  sumhr (m, n, f) = 0"
  unfolding sumhr_app by transfer simp

lemma sumhr_minus: "m n. sumhr (m, n, λi. - f i) = - sumhr (m, n, f)"
  unfolding sumhr_app by transfer (rule sum_negf)

lemma sumhr_shift_bounds:
  "m n. sumhr (m + hypnat_of_nat k, n + hypnat_of_nat k, f) =
    sumhr (m, n, λi. f (i + k))"
  unfolding sumhr_app by transfer (rule sum.shift_bounds_nat_ivl)


subsection Nonstandard Sums

text Infinite sums are obtained by summing to some infinite hypernatural
  (such as termwhn).
lemma sumhr_hypreal_of_hypnat_omega: "sumhr (0, whn, λi. 1) = hypreal_of_hypnat whn"
  by (simp add: sumhr_const)

lemma whn_eq_ωm1: "hypreal_of_hypnat whn = ω - 1"
  unfolding star_class_defs omega_def hypnat_omega_def of_hypnat_def star_of_def
  by (simp add: starfun_star_n starfun2_star_n)

lemma sumhr_hypreal_omega_minus_one: "sumhr(0, whn, λi. 1) = ω - 1"
  by (simp add: sumhr_const whn_eq_ωm1)

lemma sumhr_minus_one_realpow_zero [simp]: "N. sumhr (0, N + N, λi. (-1) ^ (i + 1)) = 0"
  unfolding sumhr_app
  by transfer (induct_tac N, auto)

lemma sumhr_interval_const:
  "(n. m  Suc n  f n = r)  m  na 
    sumhr (hypnat_of_nat m, hypnat_of_nat na, f) = hypreal_of_nat (na - m) * hypreal_of_real r"
  unfolding sumhr_app by transfer simp

lemma starfunNat_sumr: "N. ( *f* (λn. sum f {0..<n})) N = sumhr (0, N, f)"
  unfolding sumhr_app by transfer (rule refl)

lemma sumhr_hrabs_approx [simp]: "sumhr (0, M, f)  sumhr (0, N, f)  ¦sumhr (M, N, f)¦  0"
  using linorder_less_linear [where x = M and y = N]
  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)


subsection Infinite sums: Standard and NS theorems

lemma sums_NSsums_iff: "f sums l  f NSsums l"
  by (simp add: sums_def NSsums_def LIMSEQ_NSLIMSEQ_iff)

lemma summable_NSsummable_iff: "summable f  NSsummable f"
  by (simp add: summable_def NSsummable_def sums_NSsums_iff)

lemma suminf_NSsuminf_iff: "suminf f = NSsuminf f"
  by (simp add: suminf_def NSsuminf_def sums_NSsums_iff)

lemma NSsums_NSsummable: "f NSsums l  NSsummable f"
  unfolding NSsums_def NSsummable_def by blast

lemma NSsummable_NSsums: "NSsummable f  f NSsums (NSsuminf f)"
  unfolding NSsummable_def NSsuminf_def NSsums_def
  by (blast intro: theI NSLIMSEQ_unique)

lemma NSsums_unique: "f NSsums s  s = NSsuminf f"
  by (simp add: suminf_NSsuminf_iff [symmetric] sums_NSsums_iff sums_unique)

lemma NSseries_zero: "m. n  Suc m  f m = 0  f NSsums (sum f {..<n})"
  by (auto simp add: sums_NSsums_iff [symmetric] not_le[symmetric] intro!: sums_finite)

lemma NSsummable_NSCauchy:
  "NSsummable f  (M  HNatInfinite. N  HNatInfinite. ¦sumhr (M, N, f)¦  0)" (is "?L=?R")
proof -
  have "?L = (MHNatInfinite. NHNatInfinite. sumhr (0, M, f)  sumhr (0, N, f))"
    by (auto simp add: summable_iff_convergent convergent_NSconvergent_iff NSCauchy_def starfunNat_sumr 
        simp flip: NSCauchy_NSconvergent_iff summable_NSsummable_iff atLeast0LessThan)
  also have "...  ?R"
    by (metis approx_hrabs_zero_cancel approx_minus_iff approx_refl approx_sym linorder_less_linear sumhr_hrabs_approx sumhr_split_diff)
  finally show ?thesis .
qed

text Terms of a convergent series tend to zero.
lemma NSsummable_NSLIMSEQ_zero: "NSsummable f  f NS 0"
  by (metis HNatInfinite_add NSLIMSEQ_def NSsummable_NSCauchy approx_hrabs_zero_cancel star_of_zero sumhr_Suc)

text Nonstandard comparison test.
lemma NSsummable_comparison_test: "N. n. N  n  ¦f n¦  g n  NSsummable g  NSsummable f"
  by (metis real_norm_def summable_NSsummable_iff summable_comparison_test)

lemma NSsummable_rabs_comparison_test:
  "N. n. N  n  ¦f n¦  g n  NSsummable g  NSsummable (λk. ¦f k¦)"
  by (rule NSsummable_comparison_test) auto

end