Theory Star
section ‹Star-Transforms in Non-Standard Analysis›
theory Star
imports NSA
begin
definition
starset_n :: "(nat ⇒ 'a set) ⇒ 'a star set" ("*sn* _" [80] 80)
where "*sn* As = Iset (star_n As)"
definition InternalSets :: "'a star set set"
where "InternalSets = {X. ∃As. X = *sn* As}"
definition
is_starext :: "('a star ⇒ 'a star) ⇒ ('a ⇒ 'a) ⇒ bool"
where "is_starext F f ⟷
(∀x y. ∃X ∈ Rep_star x. ∃Y ∈ Rep_star y. y = F x ⟷ eventually (λn. Y n = f(X n)) 𝒰)"
definition
starfun_n :: "(nat ⇒ 'a ⇒ 'b) ⇒ 'a star ⇒ 'b star" ("*fn* _" [80] 80)
where "*fn* F = Ifun (star_n F)"
definition InternalFuns :: "('a star => 'b star) set"
where "InternalFuns = {X. ∃F. X = *fn* F}"
subsection ‹Preamble - Pulling ‹∃› over ‹∀››
text ‹This proof does not need AC and was suggested by the
referee for the JCM Paper: let ‹f x› be least ‹y› such
that ‹Q x y›.›
lemma no_choice: "∀x. ∃y. Q x y ⟹ ∃f :: 'a ⇒ nat. ∀x. Q x (f x)"
by (rule exI [where x = "λx. LEAST y. Q x y"]) (blast intro: LeastI)
subsection ‹Properties of the Star-transform Applied to Sets of Reals›
lemma STAR_star_of_image_subset: "star_of ` A ⊆ *s* A"
by auto
lemma STAR_hypreal_of_real_Int: "*s* X ∩ ℝ = hypreal_of_real ` X"
by (auto simp add: SReal_def)
lemma STAR_star_of_Int: "*s* X ∩ Standard = star_of ` X"
by (auto simp add: Standard_def)
lemma lemma_not_hyprealA: "x ∉ hypreal_of_real ` A ⟹ ∀y ∈ A. x ≠ hypreal_of_real y"
by auto
lemma lemma_not_starA: "x ∉ star_of ` A ⟹ ∀y ∈ A. x ≠ star_of y"
by auto
lemma STAR_real_seq_to_hypreal: "∀n. (X n) ∉ M ⟹ star_n X ∉ *s* M"
by (simp add: starset_def star_of_def Iset_star_n FreeUltrafilterNat.proper)
lemma STAR_singleton: "*s* {x} = {star_of x}"
by simp
lemma STAR_not_mem: "x ∉ F ⟹ star_of x ∉ *s* F"
by transfer
lemma STAR_subset_closed: "x ∈ *s* A ⟹ A ⊆ B ⟹ x ∈ *s* B"
by (erule rev_subsetD) simp
text ‹Nonstandard extension of a set (defined using a constant
sequence) as a special case of an internal set.›
lemma starset_n_starset: "∀n. As n = A ⟹ *sn* As = *s* A"
by (drule fun_eq_iff [THEN iffD2]) (simp add: starset_n_def starset_def star_of_def)
subsection ‹Theorems about nonstandard extensions of functions›
text ‹Nonstandard extension of a function (defined using a
constant sequence) as a special case of an internal function.›
lemma starfun_n_starfun: "F = (λn. f) ⟹ *fn* F = *f* f"
by (simp add: starfun_n_def starfun_def star_of_def)
text ‹Prove that ‹abs› for hypreal is a nonstandard extension of abs for real w/o
use of congruence property (proved after this for general
nonstandard extensions of real valued functions).
Proof now Uses the ultrafilter tactic!›
lemma hrabs_is_starext_rabs: "is_starext abs abs"
proof -
have "∃f∈Rep_star (star_n h). ∃g∈Rep_star (star_n k). (star_n k = ¦star_n h¦) = (∀⇩F n in 𝒰. (g n::'a) = ¦f n¦)"
for x y :: "'a star" and h k
by (metis (full_types) Rep_star_star_n star_n_abs star_n_eq_iff)
then show ?thesis
unfolding is_starext_def by (metis star_cases)
qed
text ‹Nonstandard extension of functions.›
lemma starfun: "( *f* f) (star_n X) = star_n (λn. f (X n))"
by (rule starfun_star_n)
lemma starfun_if_eq: "⋀w. w ≠ star_of x ⟹ ( *f* (λz. if z = x then a else g z)) w = ( *f* g) w"
by transfer simp
text ‹Multiplication: ‹( *f) x ( *g) = *(f x g)››
lemma starfun_mult: "⋀x. ( *f* f) x * ( *f* g) x = ( *f* (λx. f x * g x)) x"
by transfer (rule refl)
declare starfun_mult [symmetric, simp]
text ‹Addition: ‹( *f) + ( *g) = *(f + g)››
lemma starfun_add: "⋀x. ( *f* f) x + ( *f* g) x = ( *f* (λx. f x + g x)) x"
by transfer (rule refl)
declare starfun_add [symmetric, simp]
text ‹Subtraction: ‹( *f) + -( *g) = *(f + -g)››
lemma starfun_minus: "⋀x. - ( *f* f) x = ( *f* (λx. - f x)) x"
by transfer (rule refl)
declare starfun_minus [symmetric, simp]
lemma starfun_add_minus: "⋀x. ( *f* f) x + -( *f* g) x = ( *f* (λx. f x + -g x)) x"
by transfer (rule refl)
declare starfun_add_minus [symmetric, simp]
lemma starfun_diff: "⋀x. ( *f* f) x - ( *f* g) x = ( *f* (λx. f x - g x)) x"
by transfer (rule refl)
declare starfun_diff [symmetric, simp]
text ‹Composition: ‹( *f) ∘ ( *g) = *(f ∘ g)››
lemma starfun_o2: "(λx. ( *f* f) (( *f* g) x)) = *f* (λx. f (g x))"
by transfer (rule refl)
lemma starfun_o: "( *f* f) ∘ ( *f* g) = ( *f* (f ∘ g))"
by (transfer o_def) (rule refl)
text ‹NS extension of constant function.›
lemma starfun_const_fun [simp]: "⋀x. ( *f* (λx. k)) x = star_of k"
by transfer (rule refl)
text ‹The NS extension of the identity function.›
lemma starfun_Id [simp]: "⋀x. ( *f* (λx. x)) x = x"
by transfer (rule refl)
text ‹The Star-function is a (nonstandard) extension of the function.›
lemma is_starext_starfun: "is_starext ( *f* f) f"
proof -
have "∃X∈Rep_star x. ∃Y∈Rep_star y. (y = (*f* f) x) = (∀⇩F n in 𝒰. Y n = f (X n))"
for x y
by (metis (mono_tags) Rep_star_star_n star_cases star_n_eq_iff starfun_star_n)
then show ?thesis
by (auto simp: is_starext_def)
qed
text ‹Any nonstandard extension is in fact the Star-function.›
lemma is_starfun_starext:
assumes "is_starext F f"
shows "F = *f* f"
proof -
have "F x = (*f* f) x"
if "∀x y. ∃X∈Rep_star x. ∃Y∈Rep_star y. (y = F x) = (∀⇩F n in 𝒰. Y n = f (X n))" for x
by (metis that mem_Rep_star_iff star_n_eq_iff starfun_star_n)
with assms show ?thesis
by (force simp add: is_starext_def)
qed
lemma is_starext_starfun_iff: "is_starext F f ⟷ F = *f* f"
by (blast intro: is_starfun_starext is_starext_starfun)
text ‹Extended function has same solution as its standard version
for real arguments. i.e they are the same for all real arguments.›
lemma starfun_eq: "( *f* f) (star_of a) = star_of (f a)"
by (rule starfun_star_of)
lemma starfun_approx: "( *f* f) (star_of a) ≈ star_of (f a)"
by simp
text ‹Useful for NS definition of derivatives.›
lemma starfun_lambda_cancel: "⋀x'. ( *f* (λh. f (x + h))) x' = ( *f* f) (star_of x + x')"
by transfer (rule refl)
lemma starfun_lambda_cancel2: "( *f* (λh. f (g (x + h)))) x' = ( *f* (f ∘ g)) (star_of x + x')"
unfolding o_def by (rule starfun_lambda_cancel)
lemma starfun_mult_HFinite_approx:
"( *f* f) x ≈ l ⟹ ( *f* g) x ≈ m ⟹ l ∈ HFinite ⟹ m ∈ HFinite ⟹
( *f* (λx. f x * g x)) x ≈ l * m"
for l m :: "'a::real_normed_algebra star"
using approx_mult_HFinite by auto
lemma starfun_add_approx: "( *f* f) x ≈ l ⟹ ( *f* g) x ≈ m ⟹ ( *f* (%x. f x + g x)) x ≈ l + m"
by (auto intro: approx_add)
text ‹Examples: ‹hrabs› is nonstandard extension of ‹rabs›,
‹inverse› is nonstandard extension of ‹inverse›.›
text ‹Can be proved easily using theorem ‹starfun› and
properties of ultrafilter as for inverse below we
use the theorem we proved above instead.›
lemma starfun_rabs_hrabs: "*f* abs = abs"
by (simp only: star_abs_def)
lemma starfun_inverse_inverse [simp]: "( *f* inverse) x = inverse x"
by (simp only: star_inverse_def)
lemma starfun_inverse: "⋀x. inverse (( *f* f) x) = ( *f* (λx. inverse (f x))) x"
by transfer (rule refl)
declare starfun_inverse [symmetric, simp]
lemma starfun_divide: "⋀x. ( *f* f) x / ( *f* g) x = ( *f* (λx. f x / g x)) x"
by transfer (rule refl)
declare starfun_divide [symmetric, simp]
lemma starfun_inverse2: "⋀x. inverse (( *f* f) x) = ( *f* (λx. inverse (f x))) x"
by transfer (rule refl)
text ‹General lemma/theorem needed for proofs in elementary topology of the reals.›
lemma starfun_mem_starset: "⋀x. ( *f* f) x ∈ *s* A ⟹ x ∈ *s* {x. f x ∈ A}"
by transfer simp
text ‹Alternative definition for ‹hrabs› with ‹rabs› function applied
entrywise to equivalence class representative.
This is easily proved using @{thm [source] starfun} and ns extension thm.›
lemma hypreal_hrabs: "¦star_n X¦ = star_n (λn. ¦X n¦)"
by (simp only: starfun_rabs_hrabs [symmetric] starfun)
text ‹Nonstandard extension of set through nonstandard extension
of ‹rabs› function i.e. ‹hrabs›. A more general result should be
where we replace ‹rabs› by some arbitrary function ‹f› and ‹hrabs›
by its NS extenson. See second NS set extension below.›
lemma STAR_rabs_add_minus: "*s* {x. ¦x + - y¦ < r} = {x. ¦x + -star_of y¦ < star_of r}"
by transfer (rule refl)
lemma STAR_starfun_rabs_add_minus:
"*s* {x. ¦f x + - y¦ < r} = {x. ¦( *f* f) x + -star_of y¦ < star_of r}"
by transfer (rule refl)
text ‹Another characterization of Infinitesimal and one of ‹≈› relation.
In this theory since ‹hypreal_hrabs› proved here. Maybe move both theorems??›
lemma Infinitesimal_FreeUltrafilterNat_iff2:
"star_n X ∈ Infinitesimal ⟷ (∀m. eventually (λn. norm (X n) < inverse (real (Suc m))) 𝒰)"
by (simp add: Infinitesimal_hypreal_of_nat_iff star_of_def hnorm_def
star_of_nat_def starfun_star_n star_n_inverse star_n_less)
lemma HNatInfinite_inverse_Infinitesimal [simp]:
assumes "n ∈ HNatInfinite"
shows "inverse (hypreal_of_hypnat n) ∈ Infinitesimal"
proof (cases n)
case (star_n X)
then have *: "⋀k. ∀⇩F n in 𝒰. k < X n"
using HNatInfinite_FreeUltrafilterNat assms by blast
have "∀⇩F n in 𝒰. inverse (real (X n)) < inverse (1 + real m)" for m
using * [of "Suc m"] by (auto elim!: eventually_mono)
then show ?thesis
using star_n by (auto simp: of_hypnat_def starfun_star_n star_n_inverse Infinitesimal_FreeUltrafilterNat_iff2)
qed
lemma approx_FreeUltrafilterNat_iff:
"star_n X ≈ star_n Y ⟷ (∀r>0. eventually (λn. norm (X n - Y n) < r) 𝒰)"
(is "?lhs = ?rhs")
proof -
have "?lhs = (star_n X - star_n Y ≈ 0)"
using approx_minus_iff by blast
also have "... = ?rhs"
by (metis (full_types) Infinitesimal_FreeUltrafilterNat_iff mem_infmal_iff star_n_diff)
finally show ?thesis .
qed
lemma approx_FreeUltrafilterNat_iff2:
"star_n X ≈ star_n Y ⟷ (∀m. eventually (λn. norm (X n - Y n) < inverse (real (Suc m))) 𝒰)"
(is "?lhs = ?rhs")
proof -
have "?lhs = (star_n X - star_n Y ≈ 0)"
using approx_minus_iff by blast
also have "... = ?rhs"
by (metis (full_types) Infinitesimal_FreeUltrafilterNat_iff2 mem_infmal_iff star_n_diff)
finally show ?thesis .
qed
lemma inj_starfun: "inj starfun"
proof (rule inj_onI)
show "φ = ψ" if eq: "*f* φ = *f* ψ" for φ ψ :: "'a ⇒ 'b"
proof (rule ext, rule ccontr)
show False
if "φ x ≠ ψ x" for x
by (metis eq that star_of_inject starfun_eq)
qed
qed
end