# Theory HSEQ

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

Convergence of sequences and series.

Conversion to Isar and new proofs by Lawrence C Paulson, 2004
*)

section ‹Sequences and Convergence (Nonstandard)›

theory HSEQ
imports Complex_Main NatStar
abbrevs "--->" = "⇢⇩N⇩S"
begin

definition NSLIMSEQ :: "(nat ⇒ 'a::real_normed_vector) ⇒ 'a ⇒ bool"
("((_)/ ⇢⇩N⇩S (_))" [60, 60] 60) where
― ‹Nonstandard definition of convergence of sequence›
"X ⇢⇩N⇩S L ⟷ (∀N ∈ HNatInfinite. ( *f* X) N ≈ star_of L)"

definition nslim :: "(nat ⇒ 'a::real_normed_vector) ⇒ 'a"
where "nslim X = (THE L. X ⇢⇩N⇩S L)"
― ‹Nonstandard definition of limit using choice operator›

definition NSconvergent :: "(nat ⇒ 'a::real_normed_vector) ⇒ bool"
where "NSconvergent X ⟷ (∃L. X ⇢⇩N⇩S L)"
― ‹Nonstandard definition of convergence›

definition NSBseq :: "(nat ⇒ 'a::real_normed_vector) ⇒ bool"
where "NSBseq X ⟷ (∀N ∈ HNatInfinite. ( *f* X) N ∈ HFinite)"
― ‹Nonstandard definition for bounded sequence›

definition NSCauchy :: "(nat ⇒ 'a::real_normed_vector) ⇒ bool"
where "NSCauchy X ⟷ (∀M ∈ HNatInfinite. ∀N ∈ HNatInfinite. ( *f* X) M ≈ ( *f* X) N)"
― ‹Nonstandard definition›

subsection ‹Limits of Sequences›

lemma NSLIMSEQ_iff: "(X ⇢⇩N⇩S L) ⟷ (∀N ∈ HNatInfinite. ( *f* X) N ≈ star_of L)"

lemma NSLIMSEQ_I: "(⋀N. N ∈ HNatInfinite ⟹ starfun X N ≈ star_of L) ⟹ X ⇢⇩N⇩S L"

lemma NSLIMSEQ_D: "X ⇢⇩N⇩S L ⟹ N ∈ HNatInfinite ⟹ starfun X N ≈ star_of L"

lemma NSLIMSEQ_const: "(λn. k) ⇢⇩N⇩S k"

lemma NSLIMSEQ_add: "X ⇢⇩N⇩S a ⟹ Y ⇢⇩N⇩S b ⟹ (λn. X n + Y n) ⇢⇩N⇩S a + b"

lemma NSLIMSEQ_add_const: "f ⇢⇩N⇩S a ⟹ (λn. f n + b) ⇢⇩N⇩S a + b"

lemma NSLIMSEQ_mult: "X ⇢⇩N⇩S a ⟹ Y ⇢⇩N⇩S b ⟹ (λn. X n * Y n) ⇢⇩N⇩S a * b"
for a b :: "'a::real_normed_algebra"
by (auto intro!: approx_mult_HFinite simp add: NSLIMSEQ_def)

lemma NSLIMSEQ_minus: "X ⇢⇩N⇩S a ⟹ (λn. - X n) ⇢⇩N⇩S - a"

lemma NSLIMSEQ_minus_cancel: "(λn. - X n) ⇢⇩N⇩S -a ⟹ X ⇢⇩N⇩S a"
by (drule NSLIMSEQ_minus) simp

lemma NSLIMSEQ_diff: "X ⇢⇩N⇩S a ⟹ Y ⇢⇩N⇩S b ⟹ (λn. X n - Y n) ⇢⇩N⇩S a - b"
using NSLIMSEQ_add [of X a "- Y" "- b"] by (simp add: NSLIMSEQ_minus fun_Compl_def)

(* FIXME: delete *)
lemma NSLIMSEQ_add_minus: "X ⇢⇩N⇩S a ⟹ Y ⇢⇩N⇩S b ⟹ (λn. X n + - Y n) ⇢⇩N⇩S a + - b"

lemma NSLIMSEQ_diff_const: "f ⇢⇩N⇩S a ⟹ (λn. f n - b) ⇢⇩N⇩S a - b"

lemma NSLIMSEQ_inverse: "X ⇢⇩N⇩S a ⟹ a ≠ 0 ⟹ (λn. inverse (X n)) ⇢⇩N⇩S inverse a"
for a :: "'a::real_normed_div_algebra"

lemma NSLIMSEQ_mult_inverse: "X ⇢⇩N⇩S a ⟹ Y ⇢⇩N⇩S b ⟹ b ≠ 0 ⟹ (λn. X n / Y n) ⇢⇩N⇩S a / b"
for a b :: "'a::real_normed_field"
by (simp add: NSLIMSEQ_mult NSLIMSEQ_inverse divide_inverse)

lemma starfun_hnorm: "⋀x. hnorm (( *f* f) x) = ( *f* (λx. norm (f x))) x"
by transfer simp

lemma NSLIMSEQ_norm: "X ⇢⇩N⇩S a ⟹ (λn. norm (X n)) ⇢⇩N⇩S norm a"
by (simp add: NSLIMSEQ_def starfun_hnorm [symmetric] approx_hnorm)

text ‹Uniqueness of limit.›
lemma NSLIMSEQ_unique: "X ⇢⇩N⇩S a ⟹ X ⇢⇩N⇩S b ⟹ a = b"
apply (drule HNatInfinite_whn [THEN [2] bspec])+
apply (auto dest: approx_trans3)
done

lemma NSLIMSEQ_pow [rule_format]: "(X ⇢⇩N⇩S a) ⟶ ((λn. (X n) ^ m) ⇢⇩N⇩S a ^ m)"
for a :: "'a::{real_normed_algebra,power}"
by (induct m) (auto intro: NSLIMSEQ_mult NSLIMSEQ_const)

text ‹We can now try and derive a few properties of sequences,
starting with the limit comparison property for sequences.›

lemma NSLIMSEQ_le: "f ⇢⇩N⇩S l ⟹ g ⇢⇩N⇩S m ⟹ ∃N. ∀n ≥ N. f n ≤ g n ⟹ l ≤ m"
for l m :: real
apply (drule starfun_le_mono)
apply (drule HNatInfinite_whn [THEN [2] bspec])+
apply (drule_tac x = whn in spec)
apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+
apply clarify
done

lemma NSLIMSEQ_le_const: "X ⇢⇩N⇩S r ⟹ ∀n. a ≤ X n ⟹ a ≤ r"
for a r :: real
by (erule NSLIMSEQ_le [OF NSLIMSEQ_const]) auto

lemma NSLIMSEQ_le_const2: "X ⇢⇩N⇩S r ⟹ ∀n. X n ≤ a ⟹ r ≤ a"
for a r :: real
by (erule NSLIMSEQ_le [OF _ NSLIMSEQ_const]) auto

text ‹Shift a convergent series by 1:
By the equivalence between Cauchiness and convergence and because
the successor of an infinite hypernatural is also infinite.›

lemma NSLIMSEQ_Suc: "f ⇢⇩N⇩S l ⟹ (λn. f(Suc n)) ⇢⇩N⇩S l"
apply (unfold NSLIMSEQ_def)
apply safe
apply (drule_tac x="N + 1" in bspec)
done

lemma NSLIMSEQ_imp_Suc: "(λn. f(Suc n)) ⇢⇩N⇩S l ⟹ f ⇢⇩N⇩S l"
apply (unfold NSLIMSEQ_def)
apply safe
apply (drule_tac x="N - 1" in bspec)
apply (erule Nats_1 [THEN [2] HNatInfinite_diff])
done

lemma NSLIMSEQ_Suc_iff: "(λn. f (Suc n)) ⇢⇩N⇩S l ⟷ f ⇢⇩N⇩S l"
by (blast intro: NSLIMSEQ_imp_Suc NSLIMSEQ_Suc)

subsubsection ‹Equivalence of @{term LIMSEQ} and @{term NSLIMSEQ}›

lemma LIMSEQ_NSLIMSEQ:
assumes X: "X ⇢ L"
shows "X ⇢⇩N⇩S L"
proof (rule NSLIMSEQ_I)
fix N
assume N: "N ∈ HNatInfinite"
have "starfun X N - star_of L ∈ Infinitesimal"
proof (rule InfinitesimalI2)
fix r :: real
assume r: "0 < r"
from LIMSEQ_D [OF X r] obtain no where "∀n≥no. norm (X n - L) < r" ..
then have "∀n≥star_of no. hnorm (starfun X n - star_of L) < star_of r"
by transfer
then show "hnorm (starfun X N - star_of L) < star_of r"
using N by (simp add: star_of_le_HNatInfinite)
qed
then show "starfun X N ≈ star_of L"
by (simp only: approx_def)
qed

lemma NSLIMSEQ_LIMSEQ:
assumes X: "X ⇢⇩N⇩S L"
shows "X ⇢ L"
proof (rule LIMSEQ_I)
fix r :: real
assume r: "0 < r"
have "∃no. ∀n≥no. hnorm (starfun X n - star_of L) < star_of r"
proof (intro exI allI impI)
fix n
assume "whn ≤ n"
with HNatInfinite_whn have "n ∈ HNatInfinite"
by (rule HNatInfinite_upward_closed)
with X have "starfun X n ≈ star_of L"
by (rule NSLIMSEQ_D)
then have "starfun X n - star_of L ∈ Infinitesimal"
by (simp only: approx_def)
then show "hnorm (starfun X n - star_of L) < star_of r"
using r by (rule InfinitesimalD2)
qed
then show "∃no. ∀n≥no. norm (X n - L) < r"
by transfer
qed

theorem LIMSEQ_NSLIMSEQ_iff: "f ⇢ L ⟷ f ⇢⇩N⇩S L"
by (blast intro: LIMSEQ_NSLIMSEQ NSLIMSEQ_LIMSEQ)

subsubsection ‹Derived theorems about @{term NSLIMSEQ}›

text ‹We prove the NS version from the standard one, since the NS proof
seems more complicated than the standard one above!›
lemma NSLIMSEQ_norm_zero: "(λn. norm (X n)) ⇢⇩N⇩S 0 ⟷ X ⇢⇩N⇩S 0"
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] tendsto_norm_zero_iff)

lemma NSLIMSEQ_rabs_zero: "(λn. ¦f n¦) ⇢⇩N⇩S 0 ⟷ f ⇢⇩N⇩S (0::real)"
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] tendsto_rabs_zero_iff)

text ‹Generalization to other limits.›
lemma NSLIMSEQ_imp_rabs: "f ⇢⇩N⇩S l ⟹ (λn. ¦f n¦) ⇢⇩N⇩S ¦l¦"
for l :: real

lemma NSLIMSEQ_inverse_zero: "∀y::real. ∃N. ∀n ≥ N. y < f n ⟹ (λn. inverse (f n)) ⇢⇩N⇩S 0"
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_zero)

lemma NSLIMSEQ_inverse_real_of_nat: "(λn. inverse (real (Suc n))) ⇢⇩N⇩S 0"
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat del: of_nat_Suc)

lemma NSLIMSEQ_inverse_real_of_nat_add: "(λn. r + inverse (real (Suc n))) ⇢⇩N⇩S r"

lemma NSLIMSEQ_inverse_real_of_nat_add_minus: "(λn. r + - inverse (real (Suc n))) ⇢⇩N⇩S r"

"(λn. r * (1 + - inverse (real (Suc n)))) ⇢⇩N⇩S r"

subsection ‹Convergence›

lemma nslimI: "X ⇢⇩N⇩S L ⟹ nslim X = L"
by (simp add: nslim_def) (blast intro: NSLIMSEQ_unique)

lemma lim_nslim_iff: "lim X = nslim X"
by (simp add: lim_def nslim_def LIMSEQ_NSLIMSEQ_iff)

lemma NSconvergentD: "NSconvergent X ⟹ ∃L. X ⇢⇩N⇩S L"

lemma NSconvergentI: "X ⇢⇩N⇩S L ⟹ NSconvergent X"

lemma convergent_NSconvergent_iff: "convergent X = NSconvergent X"
by (simp add: convergent_def NSconvergent_def LIMSEQ_NSLIMSEQ_iff)

lemma NSconvergent_NSLIMSEQ_iff: "NSconvergent X ⟷ X ⇢⇩N⇩S nslim X"
by (auto intro: theI NSLIMSEQ_unique simp add: NSconvergent_def nslim_def)

subsection ‹Bounded Monotonic Sequences›

lemma NSBseqD: "NSBseq X ⟹ N ∈ HNatInfinite ⟹ ( *f* X) N ∈ HFinite"

lemma Standard_subset_HFinite: "Standard ⊆ HFinite"
by (auto simp: Standard_def)

lemma NSBseqD2: "NSBseq X ⟹ ( *f* X) N ∈ HFinite"
apply (cases "N ∈ HNatInfinite")
apply (erule (1) NSBseqD)
apply (rule subsetD [OF Standard_subset_HFinite])
done

lemma NSBseqI: "∀N ∈ HNatInfinite. ( *f* X) N ∈ HFinite ⟹ NSBseq X"

text ‹The standard definition implies the nonstandard definition.›
lemma Bseq_NSBseq: "Bseq X ⟹ NSBseq X"
unfolding NSBseq_def
proof safe
assume X: "Bseq X"
fix N
assume N: "N ∈ HNatInfinite"
from BseqD [OF X] obtain K where "∀n. norm (X n) ≤ K"
by fast
then have "∀N. hnorm (starfun X N) ≤ star_of K"
by transfer
then have "hnorm (starfun X N) ≤ star_of K"
by simp
also have "star_of K < star_of (K + 1)"
by simp
finally have "∃x∈Reals. hnorm (starfun X N) < x"
by (rule bexI) simp
then show "starfun X N ∈ HFinite"
qed

text ‹The nonstandard definition implies the standard definition.›
lemma SReal_less_omega: "r ∈ ℝ ⟹ r < ω"
using HInfinite_omega

lemma NSBseq_Bseq: "NSBseq X ⟹ Bseq X"
proof (rule ccontr)
let ?n = "λK. LEAST n. K < norm (X n)"
assume "NSBseq X"
then have finite: "( *f* X) (( *f* ?n) ω) ∈ HFinite"
by (rule NSBseqD2)
assume "¬ Bseq X"
then have "∀K>0. ∃n. K < norm (X n)"
then have "∀K>0. K < norm (X (?n K))"
by (auto intro: LeastI_ex)
then have "∀K>0. K < hnorm (( *f* X) (( *f* ?n) K))"
by transfer
then have "ω < hnorm (( *f* X) (( *f* ?n) ω))"
by simp
then have "∀r∈ℝ. r < hnorm (( *f* X) (( *f* ?n) ω))"
by (simp add: order_less_trans [OF SReal_less_omega])
then have "( *f* X) (( *f* ?n) ω) ∈ HInfinite"
with finite show "False"
qed

text ‹Equivalence of nonstandard and standard definitions for a bounded sequence.›
lemma Bseq_NSBseq_iff: "Bseq X = NSBseq X"
by (blast intro!: NSBseq_Bseq Bseq_NSBseq)

text ‹A convergent sequence is bounded:
Boundedness as a necessary condition for convergence.
The nonstandard version has no existential, as usual.›
lemma NSconvergent_NSBseq: "NSconvergent X ⟹ NSBseq X"
by (simp add: NSconvergent_def NSBseq_def NSLIMSEQ_def)
(blast intro: HFinite_star_of approx_sym approx_HFinite)

text ‹Standard Version: easily now proved using equivalence of NS and
standard definitions.›

lemma convergent_Bseq: "convergent X ⟹ Bseq X"
for X :: "nat ⇒ 'b::real_normed_vector"
by (simp add: NSconvergent_NSBseq convergent_NSconvergent_iff Bseq_NSBseq_iff)

subsubsection ‹Upper Bounds and Lubs of Bounded Sequences›

lemma NSBseq_isUb: "NSBseq X ⟹ ∃U::real. isUb UNIV {x. ∃n. X n = x} U"
by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isUb)

lemma NSBseq_isLub: "NSBseq X ⟹ ∃U::real. isLub UNIV {x. ∃n. X n = x} U"
by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isLub)

subsubsection ‹A Bounded and Monotonic Sequence Converges›

text ‹The best of both worlds: Easier to prove this result as a standard
theorem and then use equivalence to "transfer" it into the
equivalent nonstandard form if needed!›

lemma Bmonoseq_NSLIMSEQ: "∀⇩F k in sequentially. X k = X m ⟹ X ⇢⇩N⇩S X m"
unfolding LIMSEQ_NSLIMSEQ_iff[symmetric]
by (simp add: eventually_mono eventually_nhds_x_imp_x filterlim_iff)

lemma NSBseq_mono_NSconvergent: "NSBseq X ⟹ ∀m. ∀n ≥ m. X m ≤ X n ⟹ NSconvergent X"
for X :: "nat ⇒ real"
by (auto intro: Bseq_mono_convergent
simp: convergent_NSconvergent_iff [symmetric] Bseq_NSBseq_iff [symmetric])

subsection ‹Cauchy Sequences›

lemma NSCauchyI:
"(⋀M N. M ∈ HNatInfinite ⟹ N ∈ HNatInfinite ⟹ starfun X M ≈ starfun X N) ⟹ NSCauchy X"

lemma NSCauchyD:
"NSCauchy X ⟹ M ∈ HNatInfinite ⟹ N ∈ HNatInfinite ⟹ starfun X M ≈ starfun X N"

subsubsection ‹Equivalence Between NS and Standard›

lemma Cauchy_NSCauchy:
assumes X: "Cauchy X"
shows "NSCauchy X"
proof (rule NSCauchyI)
fix M
assume M: "M ∈ HNatInfinite"
fix N
assume N: "N ∈ HNatInfinite"
have "starfun X M - starfun X N ∈ Infinitesimal"
proof (rule InfinitesimalI2)
fix r :: real
assume r: "0 < r"
from CauchyD [OF X r] obtain k where "∀m≥k. ∀n≥k. norm (X m - X n) < r" ..
then have "∀m≥star_of k. ∀n≥star_of k. hnorm (starfun X m - starfun X n) < star_of r"
by transfer
then show "hnorm (starfun X M - starfun X N) < star_of r"
using M N by (simp add: star_of_le_HNatInfinite)
qed
then show "starfun X M ≈ starfun X N"
by (simp only: approx_def)
qed

lemma NSCauchy_Cauchy:
assumes X: "NSCauchy X"
shows "Cauchy X"
proof (rule CauchyI)
fix r :: real
assume r: "0 < r"
have "∃k. ∀m≥k. ∀n≥k. hnorm (starfun X m - starfun X n) < star_of r"
proof (intro exI allI impI)
fix M
assume "whn ≤ M"
with HNatInfinite_whn have M: "M ∈ HNatInfinite"
by (rule HNatInfinite_upward_closed)
fix N
assume "whn ≤ N"
with HNatInfinite_whn have N: "N ∈ HNatInfinite"
by (rule HNatInfinite_upward_closed)
from X M N have "starfun X M ≈ starfun X N"
by (rule NSCauchyD)
then have "starfun X M - starfun X N ∈ Infinitesimal"
by (simp only: approx_def)
then show "hnorm (starfun X M - starfun X N) < star_of r"
using r by (rule InfinitesimalD2)
qed
then show "∃k. ∀m≥k. ∀n≥k. norm (X m - X n) < r"
by transfer
qed

theorem NSCauchy_Cauchy_iff: "NSCauchy X = Cauchy X"
by (blast intro!: NSCauchy_Cauchy Cauchy_NSCauchy)

subsubsection ‹Cauchy Sequences are Bounded›

text ‹A Cauchy sequence is bounded -- nonstandard version.›

lemma NSCauchy_NSBseq: "NSCauchy X ⟹ NSBseq X"
by (simp add: Cauchy_Bseq Bseq_NSBseq_iff [symmetric] NSCauchy_Cauchy_iff)

subsubsection ‹Cauchy Sequences are Convergent›

text ‹Equivalence of Cauchy criterion and convergence:
We will prove this using our NS formulation which provides a
much easier proof than using the standard definition. We do not
need to use properties of subsequences such as boundedness,
monotonicity etc... Compare with Harrison's corresponding proof
in HOL which is much longer and more complicated. Of course, we do
not have problems which he encountered with guessing the right
instantiations for his 'espsilon-delta' proof(s) in this case
since the NS formulations do not involve existential quantifiers.›

lemma NSconvergent_NSCauchy: "NSconvergent X ⟹ NSCauchy X"
by (simp add: NSconvergent_def NSLIMSEQ_def NSCauchy_def) (auto intro: approx_trans2)

lemma real_NSCauchy_NSconvergent:
fixes X :: "nat ⇒ real"
assumes "NSCauchy X" shows "NSconvergent X"
unfolding NSconvergent_def NSLIMSEQ_def
proof -
have "( *f* X) whn ∈ HFinite"
by (simp add: NSBseqD2 NSCauchy_NSBseq assms)
moreover have "∀N∈HNatInfinite. ( *f* X) whn ≈ ( *f* X) N"
using HNatInfinite_whn NSCauchy_def assms by blast
ultimately show "∃L. ∀N∈HNatInfinite. ( *f* X) N ≈ hypreal_of_real L"
by (force dest!: st_part_Ex simp add: SReal_iff intro: approx_trans3)
qed

lemma NSCauchy_NSconvergent: "NSCauchy X ⟹ NSconvergent X"
for X :: "nat ⇒ 'a::banach"
using Cauchy_convergent NSCauchy_Cauchy convergent_NSconvergent_iff by auto

lemma NSCauchy_NSconvergent_iff: "NSCauchy X = NSconvergent X"
for X :: "nat ⇒ 'a::banach"
by (fast intro: NSCauchy_NSconvergent NSconvergent_NSCauchy)

subsection ‹Power Sequences›

text ‹The sequence @{term "x^n"} tends to 0 if @{term "0≤x"} and @{term
"x<1"}.  Proof will use (NS) Cauchy equivalence for convergence and
also fact that bounded and monotonic sequence converges.›

text ‹We now use NS criterion to bring proof of theorem through.›
lemma NSLIMSEQ_realpow_zero:
fixes x :: real
assumes "0 ≤ x" "x < 1" shows "(λn. x ^ n) ⇢⇩N⇩S 0"
proof -
have "( *f* (^) x) N ≈ 0"
if N: "N ∈ HNatInfinite" and x: "NSconvergent ((^) x)" for N
proof -
have "hypreal_of_real x pow N ≈ hypreal_of_real x pow (N + 1)"
by (metis HNatInfinite_add N NSCauchy_NSconvergent_iff NSCauchy_def starfun_pow x)
moreover obtain L where L: "hypreal_of_real x pow N ≈ hypreal_of_real L"
using NSconvergentD [OF x] N by (auto simp add: NSLIMSEQ_def starfun_pow)
ultimately have "hypreal_of_real x pow N ≈ hypreal_of_real L * hypreal_of_real x"
then have "hypreal_of_real L ≈ hypreal_of_real L * hypreal_of_real x"
using L approx_trans3 by blast
then show ?thesis
by (metis L ‹x < 1› hyperpow_def less_irrefl mult.right_neutral mult_left_cancel star_of_approx_iff star_of_mult star_of_simps(9) starfun2_star_of)
qed
with assms show ?thesis
by (force dest!: convergent_realpow simp add: NSLIMSEQ_def convergent_NSconvergent_iff)
qed

lemma NSLIMSEQ_abs_realpow_zero: "¦c¦ < 1 ⟹ (λn. ¦c¦ ^ n) ⇢⇩N⇩S 0"
for c :: real
by (simp add: LIMSEQ_abs_realpow_zero LIMSEQ_NSLIMSEQ_iff [symmetric])

lemma NSLIMSEQ_abs_realpow_zero2: "¦c¦ < 1 ⟹ (λn. c ^ n) ⇢⇩N⇩S 0"
for c :: real
by (simp add: LIMSEQ_abs_realpow_zero2 LIMSEQ_NSLIMSEQ_iff [symmetric])

end
```