# Theory HLim

theory HLim
imports Star
```(*  Title:      HOL/Nonstandard_Analysis/HLim.thy
Author:     Jacques D. Fleuriot, University of Cambridge
Author:     Lawrence C Paulson
*)

section ‹Limits and Continuity (Nonstandard)›

theory HLim
imports Star
abbrevs "--->" = "─\007→⇩N⇩S"
begin

text ‹Nonstandard Definitions.›

definition NSLIM :: "('a::real_normed_vector ⇒ 'b::real_normed_vector) ⇒ 'a ⇒ 'b ⇒ bool"
("((_)/ ─(_)/→⇩N⇩S (_))" [60, 0, 60] 60)
where "f ─a→⇩N⇩S L ⟷ (∀x. x ≠ star_of a ∧ x ≈ star_of a ⟶ ( *f* f) x ≈ star_of L)"

definition isNSCont :: "('a::real_normed_vector ⇒ 'b::real_normed_vector) ⇒ 'a ⇒ bool"
where  ― ‹NS definition dispenses with limit notions›
"isNSCont f a ⟷ (∀y. y ≈ star_of a ⟶ ( *f* f) y ≈ star_of (f a))"

definition isNSUCont :: "('a::real_normed_vector ⇒ 'b::real_normed_vector) ⇒ bool"
where "isNSUCont f ⟷ (∀x y. x ≈ y ⟶ ( *f* f) x ≈ ( *f* f) y)"

subsection ‹Limits of Functions›

lemma NSLIM_I: "(⋀x. x ≠ star_of a ⟹ x ≈ star_of a ⟹ starfun f x ≈ star_of L) ⟹ f ─a→⇩N⇩S L"

lemma NSLIM_D: "f ─a→⇩N⇩S L ⟹ x ≠ star_of a ⟹ x ≈ star_of a ⟹ starfun f x ≈ star_of L"

text ‹Proving properties of limits using nonstandard definition.
The properties hold for standard limits as well!›

lemma NSLIM_mult: "f ─x→⇩N⇩S l ⟹ g ─x→⇩N⇩S m ⟹ (λx. f x * g x) ─x→⇩N⇩S (l * m)"
for l m :: "'a::real_normed_algebra"
by (auto simp add: NSLIM_def intro!: approx_mult_HFinite)

lemma starfun_scaleR [simp]: "starfun (λx. f x *⇩R g x) = (λx. scaleHR (starfun f x) (starfun g x))"
by transfer (rule refl)

lemma NSLIM_scaleR: "f ─x→⇩N⇩S l ⟹ g ─x→⇩N⇩S m ⟹ (λx. f x *⇩R g x) ─x→⇩N⇩S (l *⇩R m)"
by (auto simp add: NSLIM_def intro!: approx_scaleR_HFinite)

lemma NSLIM_add: "f ─x→⇩N⇩S l ⟹ g ─x→⇩N⇩S m ⟹ (λx. f x + g x) ─x→⇩N⇩S (l + m)"

lemma NSLIM_const [simp]: "(λx. k) ─x→⇩N⇩S k"

lemma NSLIM_minus: "f ─a→⇩N⇩S L ⟹ (λx. - f x) ─a→⇩N⇩S -L"

lemma NSLIM_diff: "f ─x→⇩N⇩S l ⟹ g ─x→⇩N⇩S m ⟹ (λx. f x - g x) ─x→⇩N⇩S (l - m)"

lemma NSLIM_add_minus: "f ─x→⇩N⇩S l ⟹ g ─x→⇩N⇩S m ⟹ (λx. f x + - g x) ─x→⇩N⇩S (l + -m)"

lemma NSLIM_inverse: "f ─a→⇩N⇩S L ⟹ L ≠ 0 ⟹ (λx. inverse (f x)) ─a→⇩N⇩S (inverse L)"
for L :: "'a::real_normed_div_algebra"
apply (drule spec)
done

lemma NSLIM_zero:
assumes f: "f ─a→⇩N⇩S l"
shows "(λx. f(x) - l) ─a→⇩N⇩S 0"
proof -
have "(λx. f x - l) ─a→⇩N⇩S l - l"
by (rule NSLIM_diff [OF f NSLIM_const])
then show ?thesis by simp
qed

lemma NSLIM_zero_cancel: "(λx. f x - l) ─x→⇩N⇩S 0 ⟹ f ─x→⇩N⇩S l"
apply (drule_tac g = "λx. l" and m = l in NSLIM_add)
done

lemma NSLIM_const_not_eq: "k ≠ L ⟹ ¬ (λx. k) ─a→⇩N⇩S L"
for a :: "'a::real_normed_algebra_1"
apply (rule_tac x="star_of a + of_hypreal ε" in exI)
done

lemma NSLIM_not_zero: "k ≠ 0 ⟹ ¬ (λx. k) ─a→⇩N⇩S 0"
for a :: "'a::real_normed_algebra_1"
by (rule NSLIM_const_not_eq)

lemma NSLIM_const_eq: "(λx. k) ─a→⇩N⇩S L ⟹ k = L"
for a :: "'a::real_normed_algebra_1"
by (rule ccontr) (blast dest: NSLIM_const_not_eq)

lemma NSLIM_unique: "f ─a→⇩N⇩S L ⟹ f ─a→⇩N⇩S M ⟹ L = M"
for a :: "'a::real_normed_algebra_1"
by (drule (1) NSLIM_diff) (auto dest!: NSLIM_const_eq)

lemma NSLIM_mult_zero: "f ─x→⇩N⇩S 0 ⟹ g ─x→⇩N⇩S 0 ⟹ (λx. f x * g x) ─x→⇩N⇩S 0"
for f g :: "'a::real_normed_vector ⇒ 'b::real_normed_algebra"
by (drule NSLIM_mult) auto

lemma NSLIM_self: "(λx. x) ─a→⇩N⇩S a"

subsubsection ‹Equivalence of @{term filterlim} and @{term NSLIM}›

lemma LIM_NSLIM:
assumes f: "f ─a→ L"
shows "f ─a→⇩N⇩S L"
proof (rule NSLIM_I)
fix x
assume neq: "x ≠ star_of a"
assume approx: "x ≈ star_of a"
have "starfun f x - star_of L ∈ Infinitesimal"
proof (rule InfinitesimalI2)
fix r :: real
assume r: "0 < r"
from LIM_D [OF f r] obtain s
where s: "0 < s" and less_r: "⋀x. x ≠ a ⟹ norm (x - a) < s ⟹ norm (f x - L) < r"
by fast
from less_r have less_r':
"⋀x. x ≠ star_of a ⟹ hnorm (x - star_of a) < star_of s ⟹
hnorm (starfun f x - star_of L) < star_of r"
by transfer
from approx have "x - star_of a ∈ Infinitesimal"
by (simp only: approx_def)
then have "hnorm (x - star_of a) < star_of s"
using s by (rule InfinitesimalD2)
with neq show "hnorm (starfun f x - star_of L) < star_of r"
by (rule less_r')
qed
then show "starfun f x ≈ star_of L"
by (unfold approx_def)
qed

lemma NSLIM_LIM:
assumes f: "f ─a→⇩N⇩S L"
shows "f ─a→ L"
proof (rule LIM_I)
fix r :: real
assume r: "0 < r"
have "∃s>0. ∀x. x ≠ star_of a ∧ hnorm (x - star_of a) < s ⟶
hnorm (starfun f x - star_of L) < star_of r"
proof (rule exI, safe)
show "0 < ε"
by (rule hypreal_epsilon_gt_zero)
next
fix x
assume neq: "x ≠ star_of a"
assume "hnorm (x - star_of a) < ε"
with Infinitesimal_epsilon have "x - star_of a ∈ Infinitesimal"
by (rule hnorm_less_Infinitesimal)
then have "x ≈ star_of a"
by (unfold approx_def)
with f neq have "starfun f x ≈ star_of L"
by (rule NSLIM_D)
then have "starfun f x - star_of L ∈ Infinitesimal"
by (unfold approx_def)
then show "hnorm (starfun f x - star_of L) < star_of r"
using r by (rule InfinitesimalD2)
qed
then show "∃s>0. ∀x. x ≠ a ∧ norm (x - a) < s ⟶ norm (f x - L) < r"
by transfer
qed

theorem LIM_NSLIM_iff: "f ─x→ L ⟷ f ─x→⇩N⇩S L"
by (blast intro: LIM_NSLIM NSLIM_LIM)

subsection ‹Continuity›

lemma isNSContD: "isNSCont f a ⟹ y ≈ star_of a ⟹ ( *f* f) y ≈ star_of (f a)"

lemma isNSCont_NSLIM: "isNSCont f a ⟹ f ─a→⇩N⇩S (f a)"

lemma NSLIM_isNSCont: "f ─a→⇩N⇩S (f a) ⟹ isNSCont f a"
apply (auto simp add: isNSCont_def NSLIM_def)
apply (case_tac "y = star_of a")
apply auto
done

text ‹NS continuity can be defined using NS Limit in
similar fashion to standard definition of continuity.›
lemma isNSCont_NSLIM_iff: "isNSCont f a ⟷ f ─a→⇩N⇩S (f a)"
by (blast intro: isNSCont_NSLIM NSLIM_isNSCont)

text ‹Hence, NS continuity can be given in terms of standard limit.›
lemma isNSCont_LIM_iff: "(isNSCont f a) = (f ─a→ (f a))"

text ‹Moreover, it's trivial now that NS continuity
is equivalent to standard continuity.›
lemma isNSCont_isCont_iff: "isNSCont f a ⟷ isCont f a"
by (simp add: isCont_def) (rule isNSCont_LIM_iff)

text ‹Standard continuity ‹⟹› NS continuity.›
lemma isCont_isNSCont: "isCont f a ⟹ isNSCont f a"
by (erule isNSCont_isCont_iff [THEN iffD2])

text ‹NS continuity ‹⟹› Standard continuity.›
lemma isNSCont_isCont: "isNSCont f a ⟹ isCont f a"
by (erule isNSCont_isCont_iff [THEN iffD1])

text ‹Alternative definition of continuity.›

text ‹Prove equivalence between NS limits --
seems easier than using standard definition.›
lemma NSLIM_h_iff: "f ─a→⇩N⇩S L ⟷ (λh. f (a + h)) ─0→⇩N⇩S L"
apply (drule_tac x = "star_of a + x" in spec)
apply (drule_tac [2] x = "- star_of a + x" in spec, safe, simp)
apply (erule mem_infmal_iff [THEN iffD2, THEN Infinitesimal_add_approx_self [THEN approx_sym]])
apply (erule_tac [3] approx_minus_iff2 [THEN iffD1])
apply (rule_tac x = x in star_cases)
apply (rule_tac [2] x = x in star_cases)
done

lemma NSLIM_isCont_iff: "f ─a→⇩N⇩S f a ⟷ (λh. f (a + h)) ─0→⇩N⇩S f a"
by (fact NSLIM_h_iff)

lemma isNSCont_minus: "isNSCont f a ⟹ isNSCont (λx. - f x) a"

lemma isNSCont_inverse: "isNSCont f x ⟹ f x ≠ 0 ⟹ isNSCont (λx. inverse (f x)) x"
for f :: "'a::real_normed_vector ⇒ 'b::real_normed_div_algebra"
using NSLIM_inverse NSLIM_isNSCont isNSCont_NSLIM by blast

lemma isNSCont_const [simp]: "isNSCont (λx. k) a"

lemma isNSCont_abs [simp]: "isNSCont abs a"
for a :: real
by (auto simp: isNSCont_def intro: approx_hrabs simp: starfun_rabs_hrabs)

subsection ‹Uniform Continuity›

lemma isNSUContD: "isNSUCont f ⟹ x ≈ y ⟹ ( *f* f) x ≈ ( *f* f) y"

lemma isUCont_isNSUCont:
fixes f :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
assumes f: "isUCont f"
shows "isNSUCont f"
unfolding isNSUCont_def
proof safe
fix x y :: "'a star"
assume approx: "x ≈ y"
have "starfun f x - starfun f y ∈ Infinitesimal"
proof (rule InfinitesimalI2)
fix r :: real
assume r: "0 < r"
with f obtain s where s: "0 < s"
and less_r: "⋀x y. norm (x - y) < s ⟹ norm (f x - f y) < r"
by (auto simp add: isUCont_def dist_norm)
from less_r have less_r':
"⋀x y. hnorm (x - y) < star_of s ⟹ hnorm (starfun f x - starfun f y) < star_of r"
by transfer
from approx have "x - y ∈ Infinitesimal"
by (unfold approx_def)
then have "hnorm (x - y) < star_of s"
using s by (rule InfinitesimalD2)
then show "hnorm (starfun f x - starfun f y) < star_of r"
by (rule less_r')
qed
then show "starfun f x ≈ starfun f y"
by (unfold approx_def)
qed

lemma isNSUCont_isUCont:
fixes f :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
assumes f: "isNSUCont f"
shows "isUCont f"
unfolding isUCont_def dist_norm
proof safe
fix r :: real
assume r: "0 < r"
have "∃s>0. ∀x y. hnorm (x - y) < s ⟶ hnorm (starfun f x - starfun f y) < star_of r"
proof (rule exI, safe)
show "0 < ε"
by (rule hypreal_epsilon_gt_zero)
next
fix x y :: "'a star"
assume "hnorm (x - y) < ε"
with Infinitesimal_epsilon have "x - y ∈ Infinitesimal"
by (rule hnorm_less_Infinitesimal)
then have "x ≈ y"
by (unfold approx_def)
with f have "starfun f x ≈ starfun f y"