# Theory HSeries

theory HSeries
imports HSEQ
```(*  Title:      HOL/Nonstandard_Analysis/HSeries.thy
Author:     Jacques D. Fleuriot

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}) ⇢⇩N⇩S 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"

text ‹Base case in definition of @{term sumr}.›
lemma sumhr_zero [simp]: "⋀m. sumhr (m, 0, f) = 0"
unfolding sumhr_app by transfer simp

text ‹Recursive case in definition of @{term sumr}.›
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)"

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 @{term whn}).›
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"
(* FIXME: need lemma: hypreal_of_hypnat whn = ω - 1 *)
(* maybe define ω = hypreal_of_hypnat whn + 1 *)
apply (unfold star_class_defs omega_def hypnat_omega_def of_hypnat_def star_of_def)
done

lemma sumhr_minus_one_realpow_zero [simp]: "⋀N. sumhr (0, N + N, λi. (-1) ^ (i + 1)) = 0"
unfolding sumhr_app
apply transfer
apply (simp del: power_Suc add: mult_2 [symmetric])
apply (induct_tac N)
apply simp_all
done

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]
apply auto
apply (drule approx_sym [THEN approx_minus_iff [THEN iffD1]])
apply (auto dest: approx_hrabs simp add: sumhr_split_diff)
done

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)"
apply (auto simp add: summable_NSsummable_iff [symmetric]
summable_iff_convergent convergent_NSconvergent_iff atLeast0LessThan[symmetric]
NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_sumr)
apply (cut_tac x = M and y = N in linorder_less_linear)
apply auto
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: sumhr_split_diff atLeast0LessThan[symmetric])
done

text ‹Terms of a convergent series tend to zero.›
lemma NSsummable_NSLIMSEQ_zero: "NSsummable f ⟹ f ⇢⇩N⇩S 0"
apply (auto simp add: NSLIMSEQ_def NSsummable_NSCauchy)
apply (drule bspec)
apply auto
apply (drule_tac x = "N + 1 " in bspec)
done

text ‹Nonstandard comparison test.›
lemma NSsummable_comparison_test: "∃N. ∀n. N ≤ n ⟶ ¦f n¦ ≤ g n ⟹ NSsummable g ⟹ NSsummable f"
apply (fold summable_NSsummable_iff)
apply (rule summable_comparison_test, simp, assumption)
done

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
```