# Theory HSeries

Up to index of Isabelle/HOL/HOL-Complex

theory HSeries
imports Series
begin

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

    Converted to Isar and polished by lcp
    *)

    header{*Finite Summation and Infinite Series for Hyperreals*}

    theory HSeries
    imports Series
    begin

    constdefs
      sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal"
       "sumhr ==
          %(M,N,f). starfun2 (%m n. setsum f {m..<n}) M N"

      NSsums  :: "[nat=>real,real] => bool"     (infixr "NSsums" 80)
       "f NSsums s  == (%n. setsum f {0..<n}) ----NS> s"

      NSsummable :: "(nat=>real) => bool"
       "NSsummable f == (∃s. f NSsums s)"

      NSsuminf   :: "(nat=>real) => real"
       "NSsuminf f == (@s. f NSsums s)"

    lemma sumhr:
         "sumhr(star_n M, star_n N, f) =
          star_n (%n. setsum f {M n..<N n})"
    by (simp add: sumhr_def starfun2_star_n)

    text{*Base case in definition of @{term sumr}*}
    lemma sumhr_zero [simp]: "sumhr (m,0,f) = 0"
    apply (cases m)
    apply (simp add: star_n_zero_num sumhr symmetric)
    done

    text{*Recursive case in definition of @{term sumr}*}
    lemma sumhr_if:
         "sumhr(m,n+1,f) =
          (if n + 1 ≤ m then 0 else sumhr(m,n,f) + ( *f* f) n)"
    apply (cases m, cases n)
    apply (auto simp add: star_n_one_num sumhr star_n_add star_n_le starfun
               star_n_zero_num star_n_eq_iff, ultra+)
    done

    lemma sumhr_Suc_zero [simp]: "sumhr (n + 1, n, f) = 0"
    apply (cases n)
    apply (simp add: star_n_one_num sumhr star_n_add star_n_zero_num)
    done

    lemma sumhr_eq_bounds [simp]: "sumhr (n,n,f) = 0"
    apply (cases n)
    apply (simp add: sumhr star_n_zero_num)
    done

    lemma sumhr_Suc [simp]: "sumhr (m,m + 1,f) = ( *f* f) m"
    apply (cases m)
    apply (simp add: sumhr star_n_one_num star_n_add starfun)
    done

    lemma sumhr_add_lbound_zero [simp]: "sumhr(m+k,k,f) = 0"
    apply (cases m, cases k)
    apply (simp add: sumhr star_n_add star_n_zero_num)
    done

    lemma sumhr_add: "sumhr (m,n,f) + sumhr(m,n,g) = sumhr(m,n,%i. f i + g i)"
    apply (cases m, cases n)
    apply (simp add: sumhr star_n_add setsum_addf)
    done

    lemma sumhr_mult: "hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)"
    apply (cases m, cases n)
    apply (simp add: sumhr star_of_def star_n_mult setsum_mult)
    done

    lemma sumhr_split_add: "n < p ==> sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)"
    apply (cases n, cases p)
    apply (auto elim!: FreeUltrafilterNat_subset simp
                add: star_n_zero_num sumhr star_n_add star_n_less setsum_add_nat_ivl star_n_eq_iff)
    done

    lemma sumhr_split_diff: "n<p ==> sumhr(0,p,f) - sumhr(0,n,f) = sumhr(n,p,f)"
    by (drule_tac f1 = f in sumhr_split_add [symmetric], simp)

    lemma sumhr_hrabs: "abs(sumhr(m,n,f)) ≤ sumhr(m,n,%i. abs(f i))"
    apply (cases n, cases m)
    apply (simp add: sumhr star_n_le star_n_abs setsum_abs)
    done

    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)"
    by (fastsimp simp add: sumhr hypnat_of_nat_eq intro:setsum_cong)

    lemma sumhr_const:
         "sumhr(0, n, %i. r) = hypreal_of_hypnat n * hypreal_of_real r"
    apply (cases n)
    apply (simp add: sumhr star_n_zero_num hypreal_of_hypnat
                     star_of_def star_n_mult real_of_nat_def)
    done

    lemma sumhr_less_bounds_zero [simp]: "n < m ==> sumhr(m,n,f) = 0"
    apply (cases m, cases n)
    apply (auto elim: FreeUltrafilterNat_subset
                simp add: sumhr star_n_less star_n_zero_num star_n_eq_iff)
    done

    lemma sumhr_minus: "sumhr(m, n, %i. - f i) = - sumhr(m, n, f)"
    apply (cases m, cases n)
    apply (simp add: sumhr star_n_minus setsum_negf)
    done

    lemma sumhr_shift_bounds:
         "sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) = sumhr(m,n,%i. f(i + k))"
    apply (cases m, cases n)
    apply (simp add: sumhr star_n_add setsum_shift_bounds_nat_ivl hypnat_of_nat_eq)
    done

    subsection{*Nonstandard Sums*}

    text{*Infinite sums are obtained by summing to some infinite hypernatural
     (such as @{term whn})*}
    lemma sumhr_hypreal_of_hypnat_omega:
          "sumhr(0,whn,%i. 1) = hypreal_of_hypnat whn"
    by (simp add: hypnat_omega_def star_n_zero_num sumhr hypreal_of_hypnat
                  real_of_nat_def)

    lemma sumhr_hypreal_omega_minus_one: "sumhr(0, whn, %i. 1) = omega - 1"
    by (simp add: hypnat_omega_def star_n_zero_num omega_def star_n_one_num
                  sumhr star_n_diff real_of_nat_def)

    lemma sumhr_minus_one_realpow_zero [simp]:
         "sumhr(0, whn + whn, %i. (-1) ^ (i+1)) = 0"
    by (simp del: realpow_Suc
             add: sumhr star_n_add nat_mult_2 [symmetric] star_n_zero_num
                  star_n_zero_num hypnat_omega_def)

    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)"
    by(simp add: sumhr hypreal_of_nat_eq hypnat_of_nat_eq
                 real_of_nat_def star_of_def star_n_mult cong: setsum_ivl_cong)

    lemma starfunNat_sumr: "( *f* (%n. setsum f {0..<n})) N = sumhr(0,N,f)"
    apply (cases N)
    apply (simp add: star_n_zero_num starfun sumhr)
    done

    lemma sumhr_hrabs_approx [simp]: "sumhr(0, M, f) @= sumhr(0, N, f)
          ==> abs (sumhr(M, N, f)) @= 0"
    apply (cut_tac x = M and y = N in linorder_less_linear)
    apply (auto simp add: approx_refl)
    apply (drule approx_sym [THEN approx_minus_iff [THEN iffD1]])
    apply (auto dest: approx_hrabs
                simp add: sumhr_split_diff diff_minus [symmetric])
    done

    (*----------------------------------------------------------------
          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"
    by (simp add: NSsums_def NSsummable_def, blast)

    lemma NSsummable_NSsums: "NSsummable f ==> f NSsums (NSsuminf f)"
    apply (simp add: NSsummable_def NSsuminf_def)
    apply (blast intro: someI2)
    done

    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 (setsum f {0..<n})"
    by (simp add: sums_NSsums_iff [symmetric] series_zero)

    lemma NSsummable_NSCauchy:
         "NSsummable f =
          (∀M ∈ HNatInfinite. ∀N ∈ HNatInfinite. abs (sumhr(M,N,f)) @= 0)"
    apply (auto simp add: summable_NSsummable_iff [symmetric]
           summable_convergent_sumr_iff convergent_NSconvergent_iff
           NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_sumr)
    apply (cut_tac x = M and y = N in linorder_less_linear)
    apply (auto simp add: approx_refl)
    apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])
    apply (rule_tac [2] approx_minus_iff [THEN iffD2])
    apply (auto dest: approx_hrabs_zero_cancel
                simp add: sumhr_split_diff diff_minus [symmetric])
    done

    text{*Terms of a convergent series tend to zero*}
    lemma NSsummable_NSLIMSEQ_zero: "NSsummable f ==> f ----NS> 0"
    apply (auto simp add: NSLIMSEQ_def NSsummable_NSCauchy)
    apply (drule bspec, auto)
    apply (drule_tac x = "N + 1 " in bspec)
    apply (auto intro: HNatInfinite_add_one approx_hrabs_zero_cancel)
    done

    text{* Easy to prove stsandard case now *}
    lemma summable_LIMSEQ_zero: "summable f ==> f ----> 0"
    by (simp add: summable_NSsummable_iff LIMSEQ_NSLIMSEQ_iff NSsummable_NSLIMSEQ_zero)

    text{*Nonstandard comparison test*}
    lemma NSsummable_comparison_test:
         "[| ∃N. ∀n. N ≤ n --> abs(f n) ≤ g n; NSsummable g |] ==> NSsummable f"
    by (auto intro: summable_comparison_test
             simp add: summable_NSsummable_iff [symmetric])

    lemma NSsummable_rabs_comparison_test:
         "[| ∃N. ∀n. N ≤ n --> abs(f n) ≤ g n; NSsummable g |]
          ==> NSsummable (%k. abs (f k))"
    apply (rule NSsummable_comparison_test)
    apply (auto)
    done

    ML
    {*
    val sumhr = thm "sumhr";
    val sumhr_zero = thm "sumhr_zero";
    val sumhr_if = thm "sumhr_if";
    val sumhr_Suc_zero = thm "sumhr_Suc_zero";
    val sumhr_eq_bounds = thm "sumhr_eq_bounds";
    val sumhr_Suc = thm "sumhr_Suc";
    val sumhr_add_lbound_zero = thm "sumhr_add_lbound_zero";
    val sumhr_add = thm "sumhr_add";
    val sumhr_mult = thm "sumhr_mult";
    val sumhr_split_add = thm "sumhr_split_add";
    val sumhr_split_diff = thm "sumhr_split_diff";
    val sumhr_hrabs = thm "sumhr_hrabs";
    val sumhr_fun_hypnat_eq = thm "sumhr_fun_hypnat_eq";
    val sumhr_less_bounds_zero = thm "sumhr_less_bounds_zero";
    val sumhr_minus = thm "sumhr_minus";
    val sumhr_shift_bounds = thm "sumhr_shift_bounds";
    val sumhr_hypreal_of_hypnat_omega = thm "sumhr_hypreal_of_hypnat_omega";
    val sumhr_hypreal_omega_minus_one = thm "sumhr_hypreal_omega_minus_one";
    val sumhr_minus_one_realpow_zero = thm "sumhr_minus_one_realpow_zero";
    val sumhr_interval_const = thm "sumhr_interval_const";
    val starfunNat_sumr = thm "starfunNat_sumr";
    val sumhr_hrabs_approx = thm "sumhr_hrabs_approx";
    val sums_NSsums_iff = thm "sums_NSsums_iff";
    val summable_NSsummable_iff = thm "summable_NSsummable_iff";
    val suminf_NSsuminf_iff = thm "suminf_NSsuminf_iff";
    val NSsums_NSsummable = thm "NSsums_NSsummable";
    val NSsummable_NSsums = thm "NSsummable_NSsums";
    val NSsums_unique = thm "NSsums_unique";
    val NSseries_zero = thm "NSseries_zero";
    val NSsummable_NSCauchy = thm "NSsummable_NSCauchy";
    val NSsummable_NSLIMSEQ_zero = thm "NSsummable_NSLIMSEQ_zero";
    val summable_LIMSEQ_zero = thm "summable_LIMSEQ_zero";
    val NSsummable_comparison_test = thm "NSsummable_comparison_test";
    val NSsummable_rabs_comparison_test = thm "NSsummable_rabs_comparison_test";
    *}

    end

lemma sumhr:

      sumhr (star_n M, star_n N, f) = star_n (%n. setsum f {M n..<N n})

lemma sumhr_zero:

      sumhr (m, 0, f) = 0

lemma sumhr_if:

      sumhr (m, n + 1, f) = (if n + 1 ≤ m then 0 else sumhr (m, n, f) + (*f* f) n)

lemma sumhr_Suc_zero:

      sumhr (n + 1, n, f) = 0

lemma sumhr_eq_bounds:

      sumhr (n, n, f) = 0

lemma sumhr_Suc:

      sumhr (m, m + 1, f) = (*f* f) m

lemma sumhr_add_lbound_zero:

      sumhr (m + k, k, f) = 0

lemma sumhr_add:

      sumhr (m, n, f) + sumhr (m, n, g) = sumhr (m, n, %i. f i + g i)

lemma sumhr_mult:

      star_of r * sumhr (m, n, f) = sumhr (m, n, %n. r * f n)

lemma sumhr_split_add:

      n < p ==> sumhr (0, n, f) + sumhr (n, p, f) = sumhr (0, p, f)

lemma sumhr_split_diff:

      n < p ==> sumhr (0, p, f) - sumhr (0, n, f) = sumhr (n, p, f)

lemma sumhr_hrabs:

      ¦sumhr (m, n, f)¦ ≤ sumhr (m, n, %i. ¦f i¦)

lemma sumhr_fun_hypnat_eq:

      (∀r. m ≤ r ∧ r < n --> f r = g r) -->
      sumhr (star_of m, star_of n, f) = sumhr (star_of m, star_of n, g)

lemma sumhr_const:

      sumhr (0, n, %i. r) = hypreal_of_hypnat n * star_of r

lemma sumhr_less_bounds_zero:

      n < m ==> sumhr (m, n, f) = 0

lemma sumhr_minus:

      sumhr (m, n, %i. - f i) = - sumhr (m, n, f)

lemma sumhr_shift_bounds:

      sumhr (m + star_of k, n + star_of k, f) = sumhr (m, n, %i. f (i + k))

### Nonstandard Sums

lemma sumhr_hypreal_of_hypnat_omega:

      sumhr (0, whn, %i. 1) = hypreal_of_hypnat whn

lemma sumhr_hypreal_omega_minus_one:

      sumhr (0, whn, %i. 1) = ω - 1

lemma sumhr_minus_one_realpow_zero:

      sumhr (0, whn + whn, %i. -1 ^ (i + 1)) = 0

lemma sumhr_interval_const:

      (∀n. m ≤ Suc n --> f n = r) ∧ m ≤ na
      ==> sumhr (star_of m, star_of na, f) = hypreal_of_nat (na - m) * star_of r

lemma starfunNat_sumr:

      (*f* (%n. setsum f {0..<n})) N = sumhr (0, N, f)

lemma sumhr_hrabs_approx:

      sumhr (0, M, f) ≈ sumhr (0, N, f) ==> ¦sumhr (M, N, f)¦ ≈ 0

lemma sums_NSsums_iff:

      f sums l = f NSsums l

lemma summable_NSsummable_iff:

      summable f = NSsummable f

lemma suminf_NSsuminf_iff:

      suminf f = NSsuminf f

lemma NSsums_NSsummable:

      f NSsums l ==> NSsummable f

lemma NSsummable_NSsums:

      NSsummable f ==> f NSsums NSsuminf f

lemma NSsums_unique:

      f NSsums s ==> s = NSsuminf f

lemma NSseries_zero:

      ∀m. n ≤ Suc m --> f m = 0 ==> f NSsums setsum f {0..<n}

lemma NSsummable_NSCauchy:

      NSsummable f = (∀M∈HNatInfinite. ∀N∈HNatInfinite. ¦sumhr (M, N, f)¦ ≈ 0)

lemma NSsummable_NSLIMSEQ_zero:

      NSsummable f ==> f ----NS> 0

lemma summable_LIMSEQ_zero:

      summable f ==> f ----> 0

lemma NSsummable_comparison_test:

      [| ∃N. ∀n. N ≤ n --> ¦f n¦ ≤ g n; NSsummable g |] ==> NSsummable f

lemma NSsummable_rabs_comparison_test:

      [| ∃N. ∀n. N ≤ n --> ¦f n¦ ≤ g n; NSsummable g |] ==> NSsummable (%k. ¦f k¦)