Theory Auxilary_Facts

section ‹Auxiliary Facts›

theory Auxilary_Facts
  imports
    "Sigmoid_Universal_Approximation.Limits_Higher_Order_Derivatives"   
begin

subsection ‹Differentiation Lemmas›

lemma has_derivative_imp:
  fixes f :: "real ⇒ real"
  assumes "(f has_derivative f') (at x)"
  shows "f differentiable (at x) ∧ deriv f x = f' 1"
proof safe
  show "f differentiable at x"
    by (meson assms differentiableI)
  then show "deriv f x = f' 1"
    by (metis DERIV_deriv_iff_real_differentiable assms has_derivative_unique 
        has_field_derivative_imp_has_derivative mult.comm_neutral)
qed

lemma DERIV_inverse_func:
  assumes "x ≠ 0"
  shows "DERIV (λw. 1 / w) x :> -1 / x^2"
proof -
  have "inverse = (/) (1::'a)"
    using inverse_eq_divide by auto
  then show ?thesis
    by (metis (no_types) DERIV_inverse assms divide_minus_left numeral_2_eq_2 power_one_over)
qed

lemma power_rule:
  fixes z :: real  and  n :: nat
  shows "deriv (λx. x ^ n) z = (if n = 0 then 0 else real n * z ^ (n - 1))"
  by(subst deriv_pow, simp_all)


subsubsection ‹Transfer Lemmas›

― ‹The following pair of results are similar to @{thm has_field_derivative_transform_within_open}  
    and @{thm has_derivative_at_within}, but more applicable to the Euclidean setting.›

lemma has_derivative_transfer_on_ball:
  fixes f g :: "real ⇒ real"
  assumes eps_gt0: "0 < ε"
  assumes eq_on_ball: "∀y. y ∈ ball x ε ⟶ f y = g y"
  assumes f_has_deriv: "(f has_derivative D) (at x)"
  shows "(g has_derivative D) (at x)"
proof -
  from f_has_deriv
  have lim: "((λy. (f y - f x - D (y - x)) / ¦y - x¦) ⤏ 0) (at x)"
    unfolding has_derivative_def
    by (simp add: divide_inverse_commute)
  
  ― ‹Using @{thm Lim_transform_within_open}, we switch from \(f\) to \(g\) in the difference quotient.›
  from assms(1,2) lim have "((λy. (g y - f x - D (y - x)) / ¦y - x¦) ⤏ 0) (at x)"
    by (subst Lim_transform_within_open
          [where f = "λxa. (f xa - f x - D (xa - x)) / ¦xa - x¦" and s = "ball x ε"], simp_all)
 ― ‹Then we replace \(f(x)\) by \(g(x)\) using the assumption \texttt{eq\_on\_ball}.›

  then have "((λy. (g y - g x - D (y - x)) / ¦y - x¦) ⤏ 0) (at x)"
    by (simp add: assms(1) eq_on_ball)
  thus ?thesis
    using assms centre_in_ball has_derivative_transform_within_open by blast
qed

corollary field_differentiable_transfer_on_ball:
  fixes f g :: "real ⇒ real"
  assumes "0 < ε"
  assumes eq_on_ball: "∀y. y ∈ ball x ε ⟶ f y = g y"
  assumes f_diff: "f field_differentiable at x"
  shows "g field_differentiable at x"
proof -
  from f_diff obtain d
    where f_has_real_deriv: "(f has_real_derivative d) (at x)"
    by (auto simp: field_differentiable_def)

  have "(g has_real_derivative d) (at x)"
    by (meson Elementary_Metric_Spaces.open_ball assms(1,2) centre_in_ball f_has_real_deriv has_field_derivative_transform_within_open)
  thus ?thesis
    unfolding field_differentiable_def
    by blast
qed

subsection ‹Trigonometric Contraction›

lemma cos_contractive:
  fixes x y :: real
  shows "¦cos x - cos y¦ ≤ ¦x - y¦"
proof -
  have "¦cos x - cos y¦ = ¦-2 * sin ((x + y) / 2) * sin ((x - y) / 2)¦"
    by (smt (verit) cos_diff_cos mult_minus_left)
  also have "... ≤ ¦sin ((x + y) / 2)¦ * (2* ¦sin ((x - y) / 2)¦)"
    by (subst abs_mult, force)
  also have "... ≤ 2 * ¦sin ((x - y) / 2)¦"
  proof - 
    have "¦sin ((x + y) / 2)¦ ≤ 1"
      using abs_sin_le_one by blast
    then have "¦sin ((x + y) / 2)¦ * (2* ¦sin ((x - y) / 2)¦) ≤ 1 * (2* ¦sin ((x - y) / 2)¦)"
      by(rule mult_right_mono, simp)
    then show ?thesis
      by linarith
  qed
  also have "... ≤ 2 * ¦(x - y) / 2¦"
    using abs_sin_le_one by (smt (verit, del_insts) abs_sin_x_le_abs_x)
  also have "... = ¦x - y¦"
    by simp
  finally show ?thesis.
qed

lemma sin_contractive:
  fixes x y :: real
  shows "¦sin x - sin y¦ ≤ ¦x - y¦"
proof -
  have "¦sin x - sin y¦ = ¦2 * cos ((x + y) / 2) * sin ((x - y) / 2)¦"
    by (metis (no_types) mult.assoc mult.commute sin_diff_sin)    
  also have "... ≤ ¦cos ((x + y) / 2)¦ * (2 * ¦sin ((x - y) / 2)¦)"
    by (subst abs_mult, force)
  also have "... ≤ 2 * ¦sin ((x - y) / 2)¦"
  proof -
    have "¦cos ((x + y) / 2)¦ ≤ 1"
      using abs_cos_le_one by blast
    then have "¦cos ((x + y) / 2)¦ * (2 * ¦sin ((x - y) / 2)¦) ≤ 1 * (2 * ¦sin ((x - y) / 2)¦)"
      by (rule mult_right_mono, simp)
    then show ?thesis
      by linarith
  qed
  also have "... ≤ 2 * ¦(x - y) / 2¦"
    using abs_sin_le_one by (smt (verit, del_insts) abs_sin_x_le_abs_x)
  also have "... = ¦x - y¦"
    by simp
  finally show ?thesis.
qed

subsection ‹Algebraic Factorizations›

lemma biquadrate_diff_biquadrate_factored:    
  fixes x y::real
  shows "y^4 - x^4 = (y - x) * (y^3 + y^2 * x + y * x^2 + x^3)"
proof -
    have "y^4 - x^4 = (y^2 - x^2) * (y^2 + x^2)"
      by (metis mult.commute numeral_Bit0 power_add square_diff_square_factored) 
    also have "... = (y - x) * (y + x) * (y^2 + x^2)"
      by (simp add: power2_eq_square square_diff_square_factored)
    also have "... = (y - x) * (y^3 + y^2 * x + y * x^2 + x^3)"
      by (simp add: distrib_left mult.commute power2_eq_square power3_eq_cube)  
    finally show ?thesis.
qed

subsection ‹Specific Trigonometric Values›

lemma sin_5pi_div_4: "sin (5 * pi / 4) = - (sqrt 2 / 2)" 
proof -
  have "5 * pi / 4 = pi + pi / 4"
    by simp
  moreover have "sin (pi + x) = - sin x" for x
    by (simp add: sin_add)
  ultimately show ?thesis
    using sin_45 by presburger
qed

lemma cos_5pi_div_4: "cos (5 * pi / 4) = - (sqrt 2 / 2)"
proof -
  have "5 * pi / 4 = pi + pi / 4"
    by simp
  moreover have "cos (pi + x) = - cos x" for x
    by (simp add: cos_add)
  moreover have "cos (pi / 4) = sqrt 2 / 2"
    by (simp add: real_div_sqrt cos_45)
  ultimately show ?thesis
    by presburger
qed

subsection ‹Local Sign Preservation of Continuous Functions›

subsubsection ‹Local Positivity›

lemma cont_at_pos_imp_loc_pos:
  fixes g :: "real ⇒ real" and x :: real
  assumes "continuous (at x) g" and "g x > 0"
  shows "∃δ > 0. ∀y. ¦y - x¦ < δ ⟶ g y > 0"
proof -
  from assms obtain δ where δ_pos: "δ > 0"
    and "∀y. ¦y - x¦ < δ ⟶ ¦g y - g x¦ < (g x)/2"
    using continuous_at_eps_delta half_gt_zero by blast
  then have "∀y. ¦y - x¦ < δ ⟶ g y > 0"
    by (smt (verit, best) field_sum_of_halves)
  then show ?thesis
    using δ_pos by blast
qed

lemma cont_at_pos_imp_loc_pos':
  fixes g :: "real ⇒ real" and x :: real
  assumes "continuous (at x) g" and "g x > 0"
  shows "∃Δ > 0. ∀δ. 0 < δ ∧ δ ≤ Δ ⟶ (∀y. ¦y - x¦ < δ ⟶ g y > 0)"
proof -
  from assms obtain δ where δ_pos: "δ > 0" and H: "∀y. ¦y - x¦ < δ ⟶ g y > 0"
    using cont_at_pos_imp_loc_pos by blast
  have "∀δ' ≤ δ. ∀y. ¦y - x¦ < δ' ⟶ g y > 0"
  proof clarify
    fix δ' y :: real
    assume "δ' ≤ δ" and "¦y - x¦ < δ'"
    thus "g y > 0" by (auto simp: H)
  qed
  then show ?thesis
    using δ_pos by blast
qed

subsubsection ‹Local Negativity›

lemma cont_at_neg_imp_loc_neg:
  fixes g :: "real ⇒ real" and x :: real
  assumes "continuous (at x) g" and "g x < 0"
  shows "∃δ > 0. ∀y. ¦y - x¦ < δ ⟶ g y < 0"
proof -
  from assms obtain δ where δ_pos: "δ > 0"
    and "∀y. ¦y - x¦ < δ ⟶ ¦g y - g x¦ < -(g x)/2"
    by (metis continuous_at_eps_delta half_gt_zero neg_0_less_iff_less)
  then have "∀y. ¦y - x¦ < δ ⟶ - g y > 0"
    by (smt (verit, best) field_sum_of_halves)
  then show ?thesis
    using δ_pos neg_0_less_iff_less by blast
qed

lemma cont_at_neg_imp_loc_neg':
  fixes g :: "real ⇒ real" and x :: real
  assumes "continuous (at x) g" and "g x < 0"
  shows "∃Δ > 0. ∀δ. 0 < δ ∧ δ ≤ Δ ⟶ (∀y. ¦y - x¦ < δ ⟶ g y < 0)"
proof -
  from assms obtain δ where δ_pos: "δ > 0"
    and H: "∀y. ¦y - x¦ < δ ⟶ -(g y) > 0"
    by (smt (verit) cont_at_neg_imp_loc_neg)
  have "∀δ' ≤ δ. ∀y. ¦y - x¦ < δ' ⟶ -(g y) > 0"
  proof clarify
    fix δ' y :: real
    assume "δ' ≤ δ" and "¦y - x¦ < δ'"
    then show "-(g y) > 0"
      using H by auto 
  qed
  then show ?thesis
    using δ_pos neg_0_less_iff_less by blast
qed

end