Theory Limits_Higher_Order_Derivatives

section ‹Limits and Higher Order Derivatives›

theory Limits_Higher_Order_Derivatives
  imports "HOL-Analysis.Analysis" 
begin


subsection ‹\(\varepsilon\)--\(\delta\) Characterizations of Limits and Continuity›

lemma tendsto_at_top_epsilon_def:
  "(f ⤏ L) at_top = (∀ ε > 0. ∃N. ∀x ≥ N. ¦(f (x::real)::real) - L¦ < ε)"
    by (simp add: Zfun_def tendsto_Zfun_iff eventually_at_top_linorder)

lemma tendsto_at_bot_epsilon_def:
  "(f ⤏ L) at_bot = (∀ ε > 0. ∃N. ∀x ≤ N. ¦(f (x::real)::real) - L¦ < ε)"
    by (simp add: Zfun_def tendsto_Zfun_iff eventually_at_bot_linorder)

lemma tendsto_inf_at_top_epsilon_def:
  "(g ⤏ ∞) at_top = (∀ ε > 0. ∃N. ∀x ≥ N. (g (x::real)::real) > ε)"
  by (subst tendsto_PInfty', subst Filter.eventually_at_top_linorder, simp)
  
lemma tendsto_inf_at_bot_epsilon_def:
  "(g ⤏ ∞) at_bot = (∀ ε > 0. ∃N. ∀x ≤ N. (g (x::real)::real) > ε)"
  by (subst tendsto_PInfty', subst Filter.eventually_at_bot_linorder, simp)

lemma tendsto_minus_inf_at_top_epsilon_def:
  "(g ⤏ -∞) at_top = (∀ ε < 0. ∃N. ∀x ≥ N. (g (x::real)::real) < ε)"
  by(subst tendsto_MInfty', subst Filter.eventually_at_top_linorder, simp)

lemma tendsto_minus_inf_at_bot_epsilon_def:
  "(g ⤏ -∞) at_bot = (∀ ε < 0. ∃N. ∀x ≤ N. (g (x::real)::real) < ε)"
  by (subst tendsto_MInfty', subst Filter.eventually_at_bot_linorder, simp)

lemma tendsto_at_x_epsilon_def:
  fixes f :: "real ⇒ real" and L :: real and x :: real
  shows "(f ⤏ L) (at x) = (∀ε > 0. ∃δ > 0. ∀y. (y ≠ x ∧ ¦y - x¦ < δ) ⟶ ¦f y - L¦ < ε)"
  unfolding tendsto_def
proof (subst eventually_at, safe)
  text ‹ --- First Direction ---
  We show that the filter definition implies the \(\varepsilon\)--\(\delta\) formulation.›
  fix ε :: real
  assume lim_neigh: "∀S. open S ⟶ L ∈ S ⟶ (∃d>0. ∀xa∈UNIV. xa ≠ x ∧ dist xa x < d ⟶ f xa ∈ S)"
  assume ε_pos: "0 < ε"
  show "∃δ>0. ∀y. y ≠ x ∧ ¦y - x¦ < δ ⟶ ¦f y - L¦ < ε"
  proof -
    text ‹Choose \(S\) as the open ball around \(L\) with radius \(\varepsilon\).›

    have "open (ball L ε)" 
      by simp 
    text ‹Confirm that \(L\) lies in the ball.›
    moreover have "L ∈ ball L ε"
      unfolding ball_def by (simp add: ε_pos)
    text ‹By applying lim\_neigh to the ball, we obtain a suitable \(\delta\).›
    ultimately obtain δ where d_pos: "δ > 0" 
      and δ_prop: "∀y. y ≠ x ∧ dist y x < δ ⟶ f y ∈ ball L ε"
      by (meson UNIV_I lim_neigh)
    text ‹Since \(f(y)\in \mathrm{ball}(L,\varepsilon)\) means \(\lvert f(y)-L\rvert<\varepsilon\), 
          we deduce the \(\varepsilon\)–\(\delta\) condition.›
    hence "∀y. y ≠ x ∧ ¦y - x¦ < δ ⟶ ¦f y - L¦ < ε"
      by (auto simp: ball_def dist_norm)
    thus ?thesis
      using d_pos by blast
  qed
next
  text ‹--- Second Direction ---
     We show that the \(\varepsilon\)--\(\delta\) formulation implies the filter definition.›
  fix S :: "real set"
  assume eps_delta: "∀ε>0. ∃δ>0. ∀y. (y ≠ x ∧ ¦y - x¦ < δ) ⟶ ¦f y - L¦ < ε"
  and S_open: "open S"
  and L_in_S: "L ∈ S"
  text ‹ Since \(S\) is open and contains \(L\), there exists an \(\varepsilon\)-ball
  around \(L\) contained in \(S\).›

  from S_open L_in_S obtain ε where ε_pos: "ε > 0" and ball_sub: "ball L ε ⊆ S"
    by (meson openE)
  text ‹Applying the \(\varepsilon\)--\(\delta\) assumption for this particular \(\varepsilon\)
  yields a \(\delta > 0\) such that for all \(y\), if \(y \neq x\) and
  \(\lvert y - x\rvert < \delta\) then \(\lvert f(y) - L\rvert < \varepsilon\).›

  from eps_delta obtain δ where δ_pos: "δ > 0" 
    and δ_prop: "∀y. (y ≠ x ∧ ¦y - x¦ < δ) ⟶ ¦f y - L¦ < ε"
    using ε_pos by blast
  text ‹ Notice that \(\lvert f(y) - L\rvert < \varepsilon\) is equivalent to
  \(f(y) \in \mathrm{ball}\,L\,\varepsilon\).›

  have "∀y. (y ≠ x ∧ dist y x < δ) ⟶ f y ∈ ball L ε"
    using δ_prop dist_real_def by fastforce
  text ‹Since \(\mathrm{ball}(L,\varepsilon) \subseteq S\),
  for all \(y\) with \(y \neq x\) and \(\mathrm{dist}\,y\,x < \delta\), we have \(f\,y \in S\).›
  hence "∀y. (y ≠ x ∧ dist y x < δ) ⟶ f y ∈ S"
    using ball_sub by blast
  text ‹This gives exactly the existence of some \(d\) (namely \(\delta\)) satisfying the filter condition.›

  thus "∃d>0. ∀y∈UNIV. (y ≠ x ∧ dist y x < d) ⟶ f y ∈ S"
    using δ_pos by blast
qed

lemma continuous_at_eps_delta:
  fixes g :: "real ⇒ real" and y :: real
  shows "continuous (at y) g = (∀ε > 0. ∃δ > 0. ∀x. ¦x - y¦ < δ ⟶ ¦g x - g y¦ < ε)"
proof -
  have "continuous (at y) g = (∀ε > 0. ∃δ > 0. ∀x. (x ≠ y ∧ ¦x - y¦ < δ) ⟶ ¦g x - g y¦ < ε)"
    by (simp add: isCont_def tendsto_at_x_epsilon_def)
  also have "... = (∀ε > 0. ∃δ > 0. ∀x. ¦x - y¦ < δ ⟶ ¦g x - g y¦ < ε)"
    by (metis abs_eq_0 diff_self)
  finally show ?thesis.
qed

lemma tendsto_divide_approaches_const:
  fixes f g :: "real ⇒ real"
  assumes f_lim:"((λx. f (x::real)) ⤏ c) at_top"
      and g_lim: "((λx. g (x::real)) ⤏ ∞) at_top"
    shows "((λx. f (x::real) / g x) ⤏ 0) at_top"
proof(subst tendsto_at_top_epsilon_def, clarify)
  fix ε :: real
  assume ε_pos: "0 < ε"

  obtain M where M_def: "M = abs c + 1" and M_gt_0: "M > 0"
    by simp

  obtain N1 where N1_def: "∀x≥N1. abs (f x - c) < 1"
    using f_lim tendsto_at_top_epsilon_def zero_less_one by blast 

  have f_bound: "∀x≥N1. abs (f x) < M"
    using M_def N1_def by fastforce

  have M_over_ε_gt_0: "M / ε > 0"
    by (simp add: M_gt_0 ε_pos)

  then obtain N2 where N2_def: "∀x≥N2. g x > M / ε"
    using g_lim tendsto_inf_at_top_epsilon_def by blast

  obtain N where "N = max N1 N2" and N_ge_N1: "N ≥ N1" and N_ge_N2: "N ≥ N2"
    by auto 

  show "∃N::real. ∀x≥N. ¦f x / g x - 0¦ < ε"
  proof(intro exI [where x=N], clarify)
    fix x :: real
    assume x_ge_N: " N ≤ x"

    have f_bound_x: "¦f x¦ < M"
      using N_ge_N1 f_bound x_ge_N by auto

    have g_bound_x: "g x > M / ε"
      using N2_def N_ge_N2 x_ge_N by auto 

    have "¦f x / g x¦ = ¦f x¦ / ¦g x¦"
      using abs_divide by blast
    also have "... < M /  ¦g x¦"
      using M_over_ε_gt_0 divide_strict_right_mono f_bound_x g_bound_x by force
    also have  "... < ε"
      by (metis  M_over_ε_gt_0 ε_pos abs_real_def g_bound_x mult.commute order_less_irrefl order_less_trans pos_divide_less_eq)
    finally show "¦f x / g x - 0¦ < ε"
      by linarith
  qed      
qed

lemma tendsto_divide_approaches_const_at_bot:
  fixes f g :: "real ⇒ real"
  assumes f_lim: "((λx. f (x::real)) ⤏ c) at_bot"
      and g_lim: "((λx. g (x::real)) ⤏ ∞) at_bot"
    shows "((λx. f (x::real) / g x) ⤏ 0) at_bot"
proof(subst tendsto_at_bot_epsilon_def, clarify)
  fix ε :: real
  assume ε_pos: "0 < ε"

  obtain M where M_def: "M = abs c + 1" and M_gt_0: "M > 0"
    by simp

  obtain N1 where N1_def: "∀x≤N1. abs (f x - c) < 1"
    using f_lim tendsto_at_bot_epsilon_def zero_less_one by blast 

  have f_bound: "∀x≤N1. abs (f x) < M"
    using M_def N1_def by fastforce

  have M_over_ε_gt_0: "M / ε > 0"
    by (simp add: M_gt_0 ε_pos)

  then obtain N2 where N2_def: "∀x≤N2. g x > M / ε"
    using g_lim tendsto_inf_at_bot_epsilon_def by blast

  obtain N where "N = min N1 N2" and N_le_N1: "N ≤ N1" and N_le_N2: "N ≤ N2"
    by auto 
    
  show "∃N::real. ∀x≤N. ¦f x / g x - 0¦ < ε"
  proof(intro exI [where x=N], clarify)
    fix x :: real
    assume x_le_N: "x ≤ N"

    have f_bound_x: "¦f x¦ < M"
      using N_le_N1 f_bound x_le_N by auto

    have g_bound_x: "g x > M / ε"
      using N2_def N_le_N2 x_le_N by auto 

    have "¦f x / g x¦ = ¦f x¦ / ¦g x¦"
      using abs_divide by blast
    also have "... < M /  ¦g x¦"
      using M_over_ε_gt_0 divide_strict_right_mono f_bound_x g_bound_x by force
    also have  "... < ε"
      by (metis  M_over_ε_gt_0 ε_pos abs_real_def g_bound_x mult.commute order_less_irrefl order_less_trans pos_divide_less_eq)
    finally show "¦f x / g x - 0¦ < ε"
      by linarith
  qed      
qed

lemma equal_limits_diff_zero_at_top:
  assumes f_lim: "(f ⤏ (L1::real)) at_top"
  assumes g_lim: "(g ⤏ (L2::real)) at_top"
  shows "((f - g) ⤏ (L1 - L2)) at_top"
proof -
  have "((λx. f x - g x) ⤏ L1 - L2) at_top"
    by (rule tendsto_diff, rule f_lim, rule g_lim)
  then show ?thesis 
    by (simp add: fun_diff_def)
qed

lemma equal_limits_diff_zero_at_bot:
  assumes f_lim: "(f ⤏ (L1::real)) at_bot"
  assumes g_lim: "(g ⤏ (L2::real)) at_bot"
  shows "((f - g) ⤏ (L1 - L2)) at_bot"
proof -
  have "((λx. f x - g x) ⤏ L1 - L2) at_bot"
    by (rule tendsto_diff, rule f_lim, rule g_lim)
  then show ?thesis 
    by (simp add: fun_diff_def)
qed


subsection ‹Nth Order Derivatives and $C^k(U)$ Smoothness›
fun Nth_derivative :: "nat ⇒ (real ⇒ real) ⇒ (real ⇒ real)" where
  "Nth_derivative 0 f = f " |
  "Nth_derivative (Suc n) f  = deriv (Nth_derivative n f)"

lemma first_derivative_alt_def:
  "Nth_derivative 1 f = deriv f"
  by simp

lemma second_derivative_alt_def:
  "Nth_derivative 2 f  = deriv (deriv f)"
  by (simp add: numeral_2_eq_2)

lemma limit_def_nth_deriv:
  fixes f :: "real ⇒ real" and a :: real and n :: nat
  assumes n_pos: "n > 0"
      and D_last: "DERIV (Nth_derivative (n - 1) f) a :> Nth_derivative n f a"
  shows
    "((λx. (Nth_derivative (n - 1) f x - Nth_derivative (n - 1) f a) / (x - a))
       ⤏ Nth_derivative n f a) (at a)"
  using D_last has_field_derivativeD by blast

definition C_k_on :: "nat ⇒ (real ⇒ real) ⇒ real set ⇒ bool" where
  "C_k_on k f U ≡ 
     (if k = 0 then (open U ∧ continuous_on U f)
      else (open U ∧ (∀n < k. (Nth_derivative n f) differentiable_on U 
                         ∧ continuous_on U (Nth_derivative (Suc n) f))))"

lemma C0_on_def:
  "C_k_on 0 f U ⟷ (open U ∧ continuous_on U f)"
  by (simp add: C_k_on_def)

lemma C1_cont_diff:
  assumes "C_k_on 1 f U"
  shows "f differentiable_on U ∧ continuous_on U (deriv f) ∧ 
         (∀ y  ∈ U. (f has_real_derivative (deriv f) y) (at y))"
  using C_k_on_def DERIV_deriv_iff_real_differentiable assms at_within_open differentiable_on_def by fastforce

lemma C2_cont_diff:
  fixes f :: "real ⇒ real" and U :: "real set"
  assumes "C_k_on 2 f U"
  shows "f differentiable_on U ∧ continuous_on U (deriv f) ∧ 
         (∀y ∈ U. (f has_real_derivative (deriv f) y) (at y)) ∧
         deriv f differentiable_on U ∧ continuous_on U (deriv (deriv f)) ∧
         (∀y ∈ U. (deriv f has_real_derivative (deriv (deriv f)) y) (at y))"
  by (smt (verit, best) C1_cont_diff C_k_on_def Nth_derivative.simps(1,2) One_nat_def assms less_2_cases_iff less_numeral_extra(1) nat_1_add_1 order.asym pos_add_strict)

lemma C2_on_open_U_def2:
  fixes f :: "real ⇒ real"
  assumes openU : "open U"
      and diff_f : "f differentiable_on U"
      and diff_df: "deriv f differentiable_on U"
      and cont_d2f: "continuous_on U (deriv (deriv f))"
  shows "C_k_on 2 f U"
  by (simp add: C_k_on_def cont_d2f diff_df diff_f differentiable_imp_continuous_on less_2_cases_iff openU)

lemma C_k_on_subset:
  assumes "C_k_on k f U"
  assumes open_subset: "open S ∧ S ⊂ U"  
  shows "C_k_on k f S"
  using assms
  by (smt (verit) C_k_on_def continuous_on_subset differentiable_on_eq_differentiable_at dual_order.strict_implies_order subset_eq)


definition smooth_on :: "(real ⇒ real) ⇒ real set ⇒ bool" where
  "smooth_on f U ≡ ∀k. C_k_on k f U"

end