Theory HLim

(*  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 "--->" = "─→NS"
begin

text Nonstandard Definitions.

definition NSLIM :: "('a::real_normed_vector  'b::real_normed_vector)  'a  'b  bool"
    ("((_)/ (_)/NS (_))" [60, 0, 60] 60)
  where "f aNS 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 aNS L"
  by (simp add: NSLIM_def)

lemma NSLIM_D: "f aNS L  x  star_of a  x  star_of a  starfun f x  star_of L"
  by (simp add: NSLIM_def)

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

lemma NSLIM_mult: "f xNS l  g xNS m  (λx. f x * g x) xNS (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 xNS l  g xNS m  (λx. f x *R g x) xNS (l *R m)"
  by (auto simp add: NSLIM_def intro!: approx_scaleR_HFinite)

lemma NSLIM_add: "f xNS l  g xNS m  (λx. f x + g x) xNS (l + m)"
  by (auto simp add: NSLIM_def intro!: approx_add)

lemma NSLIM_const [simp]: "(λx. k) xNS k"
  by (simp add: NSLIM_def)

lemma NSLIM_minus: "f aNS L  (λx. - f x) aNS -L"
  by (simp add: NSLIM_def)

lemma NSLIM_diff: "f xNS l  g xNS m  (λx. f x - g x) xNS (l - m)"
  by (simp only: NSLIM_add NSLIM_minus diff_conv_add_uminus)

lemma NSLIM_add_minus: "f xNS l  g xNS m  (λx. f x + - g x) xNS (l + -m)"
  by (simp only: NSLIM_add NSLIM_minus)

lemma NSLIM_inverse: "f aNS L  L  0  (λx. inverse (f x)) aNS (inverse L)"
  for L :: "'a::real_normed_div_algebra"
  unfolding NSLIM_def by (metis (no_types) star_of_approx_inverse star_of_simps(6) starfun_inverse)

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

lemma NSLIM_zero_cancel: 
  assumes "(λx. f x - l) xNS 0"
  shows "f xNS l"
proof -
  have "(λx. f x - l + l) xNS 0 + l"
    by (fast intro: assms NSLIM_const NSLIM_add)
  then show ?thesis
    by simp
qed

lemma NSLIM_const_eq:
  fixes a :: "'a::real_normed_algebra_1"
  assumes "(λx. k) aNS l"
  shows "k = l"
proof -
  have "¬ (λx. k) aNS l" if "k  l"
  proof -
    have "star_of a + of_hypreal ε  star_of a"
      by (simp add: approx_def)
    then show ?thesis
      using epsilon_not_zero that by (force simp add: NSLIM_def)
  qed
  with assms show ?thesis by metis
qed

lemma NSLIM_unique: "f aNS l  f aNS 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 xNS 0  g xNS 0  (λx. f x * g x) xNS 0"
  for f g :: "'a::real_normed_vector  'b::real_normed_algebra"
  by (drule NSLIM_mult) auto

lemma NSLIM_self: "(λx. x) aNS a"
  by (simp add: NSLIM_def)


subsubsection Equivalence of termfilterlim and termNSLIM

lemma LIM_NSLIM:
  assumes f: "f a L"
  shows "f aNS 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 aNS 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 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 xNS 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)"
  by (simp add: isNSCont_def)

lemma isNSCont_NSLIM: "isNSCont f a  f aNS (f a)"
  by (simp add: isNSCont_def NSLIM_def)

lemma NSLIM_isNSCont: "f aNS (f a)  isNSCont f a"
  by (force simp add: isNSCont_def NSLIM_def)

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 aNS (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))"
  by (simp add: LIM_NSLIM_iff isNSCont_NSLIM_iff)

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_at0_iff: "f aNS L  (λh. f (a + h)) 0NS L"
proof
  assume "f aNS L"
  then show "(λh. f (a + h)) 0NS L"
    by (simp add: NSLIM_def) (metis (no_types) add_cancel_left_right approx_add_left_iff starfun_lambda_cancel)
next
  assume *: "(λh. f (a + h)) 0NS L"
  show "f aNS L"
  proof (clarsimp simp: NSLIM_def)
    fix x
    assume "x  star_of a" "x  star_of a"
    then have "(*f* (λh. f (a + h))) (- star_of a + x)  star_of L"
      by (metis (no_types, lifting) "*" NSLIM_D add.right_neutral add_minus_cancel approx_minus_iff2 star_zero_def)
    then show "(*f* f) x  star_of L"
      by (simp add: starfun_lambda_cancel)
  qed
qed

lemma isNSCont_minus: "isNSCont f a  isNSCont (λx. - f x) a"
  by (simp add: isNSCont_def)

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"
  by (simp add: isNSCont_def)

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"
  by (simp add: isNSUCont_def)

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 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"
      by (simp add: isNSUCont_def)
    then have "starfun f x - starfun f y  Infinitesimal"
      by (unfold approx_def)
    then show "hnorm (starfun f x - starfun f y) < star_of r"
      using r by (rule InfinitesimalD2)
  qed
  then show "s>0. x y. norm (x - y) < s  norm (f x - f y) < r"
    by transfer
qed

end