Derivative_Lib.thy

section \<open> Derivatives: extra laws and tactics \<close>

theory Derivative_Lib
  imports
  "Differential_Dynamic_Logic.Lib"
  "HOL-Eisbach.Eisbach"
  "HOL-Decision_Procs.Approximation"
begin

subsection \<open> Properties of filters \<close>

lemma filtermap_within_range_minus: "filtermap (\<lambda> x. x - n::real) (at y within {x..<y}) = (at (y - n) within ({x-n..<y-n}))"
  by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_shift[symmetric])

lemma filtermap_within_range_plus: "filtermap (\<lambda> x. x + n::real) (at y within {x..<y}) = (at (y + n) within ({x+n..<y+n}))"
  using filtermap_within_range_minus[of "-n"] by simp

lemma filter_upto_contract:
  "\<lbrakk> (x::real) \<le> y; y < z \<rbrakk> \<Longrightarrow> (at z within {x..<z}) = (at z within {y..<z})"
  by (rule at_within_nhd[of _ "{y<..<z+1}"], auto)

subsection \<open> Topological Spaces \<close>
  
instantiation unit :: t2_space
begin
  definition open_unit :: "unit set \<Rightarrow> bool" where "open_unit = (\<lambda> _. True)"
  instance by (intro_classes, simp_all add: open_unit_def)
end
 
subsection \<open> Extra derivative rules \<close>

lemma has_vector_derivative_Pair [derivative_intros]:
  "\<lbrakk> (f has_vector_derivative f') (at x within s); (g has_vector_derivative g') (at x within s) \<rbrakk> \<Longrightarrow>
      ((\<lambda> x. (f x, g x)) has_vector_derivative (f', g')) (at x within s)"
  by (auto intro: has_derivative_Pair simp add: has_vector_derivative_def)

lemma has_vector_derivative_power[simp, derivative_intros]:
  fixes f :: "real \<Rightarrow> 'a :: real_normed_field"
  assumes f: "(f has_vector_derivative f') (at x within s)"
  shows "((\<lambda>x. f x^n) has_vector_derivative (of_nat n * f' * f x^(n - 1))) (at x within s)"
  using assms
  apply (simp add: has_vector_derivative_def)
  apply (subst has_derivative_eq_rhs)
  apply (rule has_derivative_power)
  apply (auto)
done

lemma has_vector_derivative_divide[simp, derivative_intros]:
  fixes f :: "real \<Rightarrow> 'a :: real_normed_div_algebra"
  assumes f: "(f has_vector_derivative f') (at x within s)"
      and g: "(g has_vector_derivative g') (at x within s)"
  assumes x: "g x \<noteq> 0"
  shows "((\<lambda>x. f x / g x) has_vector_derivative
                (- f x * (inverse (g x) * g' * inverse (g x)) + f' / g x)) (at x within s)"
  using assms
  apply (simp add: has_vector_derivative_def)
  apply (subst has_derivative_eq_rhs)
  apply (rule has_derivative_divide)
  apply (auto simp add: divide_inverse real_vector.scale_right_diff_distrib)
done

lemma Pair_has_vector_derivative:
  assumes "(f has_vector_derivative f') (at x within s)"
    "(g has_vector_derivative g') (at x within s)"
  shows "((\<lambda>x. (f x, g x)) has_vector_derivative (f', g')) (at x within s)"
  using assms
  by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros)
  
lemma has_vector_derivative_fst:
  assumes "((\<lambda>x. (f x, g x)) has_vector_derivative (f', g')) (at x within s)"
  shows "(f has_vector_derivative f') (at x within s)"
  using assms
  by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros dest: has_derivative_fst)

lemma has_vector_derivative_fst' [derivative_intros]:
  assumes "(f has_vector_derivative (f', g')) (at x within s)"
  shows "(fst \<circ> f has_vector_derivative f') (at x within s)"
proof -
  have "(\<lambda> x. (fst (f x), snd (f x))) = f"
    by (simp)
  with assms have "((\<lambda> x. (fst (f x), snd (f x))) has_vector_derivative (f', g')) (at x within s)"
    by (simp)
  thus ?thesis
    by (drule_tac has_vector_derivative_fst, simp add: comp_def)
qed
    
lemma has_vector_derivative_snd:
  assumes "((\<lambda>x. (f x, g x)) has_vector_derivative (f', g')) (at x within s)"
  shows "(g has_vector_derivative g') (at x within s)"
  using assms
  by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros dest: has_derivative_snd)

lemma has_vector_derivative_snd'' [derivative_intros]:
  assumes "(f has_vector_derivative (f', g')) (at x within s)"
  shows "(snd \<circ> f has_vector_derivative g') (at x within s)"
proof -
  have "(\<lambda> x. (fst (f x), snd (f x))) = f"
    by (simp)
  with assms have "((\<lambda> x. (fst (f x), snd (f x))) has_vector_derivative (f', g')) (at x within s)"
    by (simp)
  thus ?thesis
    by (drule_tac has_vector_derivative_snd, simp add: comp_def)
qed

lemma Pair_has_vector_derivative_iff:
  "((\<lambda>x. (f x, g x)) has_vector_derivative (f', g')) (at x within s) \<longleftrightarrow>
   (f has_vector_derivative f') (at x within s) \<and> (g has_vector_derivative g') (at x within s)"
  using Pair_has_vector_derivative has_vector_derivative_fst has_vector_derivative_snd by blast
  
text \<open> The next four rules allow us to prove derivatives when the function is equivalent to
  another a function when approach from the left or right. \<close>
 
lemma has_derivative_left_point:
  fixes f g :: "real \<Rightarrow> real"
  assumes "(f has_derivative f') (at x within s)" "x \<in> s" "x < y" "\<forall>x'<y. f x' = g x'"
  shows "(g has_derivative f') (at x within s)"
  apply (rule has_derivative_transform_within[of f f' x s "y-x" g])
  apply (simp_all add: assms dist_real_def)
done
  
lemma has_derivative_right_point:
  fixes f g :: "real \<Rightarrow> real"
  assumes "(f has_derivative f') (at x within s)" "x \<in> s" "x > y" "\<forall>x'>y. f x' = g x'"
  shows "(g has_derivative f') (at x within s)"
  apply (rule has_derivative_transform_within[of f f' x s "x-y" g])
  apply (simp_all add: assms dist_real_def)
done
  
lemma has_vector_derivative_left_point:
  fixes f g :: "real \<Rightarrow> real"
  assumes "(f has_vector_derivative f') (at x within s)" "x \<in> s" "x < y" "\<forall>x'<y. f x' = g x'"
  shows "(g has_vector_derivative f') (at x within s)"
  using assms
  apply (simp add: has_vector_derivative_def)
  apply (rule_tac y="y" and f="f" in has_derivative_left_point)
  apply (auto simp add: assms)
done

lemma has_vector_derivative_right_point:
  fixes f g :: "real \<Rightarrow> real"
  assumes "(f has_vector_derivative f') (at x within s)" "x \<in> s" "x > y" "\<forall>x'>y. f x' = g x'"
  shows "(g has_vector_derivative f') (at x within s)"
  using assms
  apply (simp add: has_vector_derivative_def)
  apply (rule_tac y="y" and f="f" in has_derivative_right_point)
  apply (auto simp add: assms)
done

method prove_vec_deriv = 
  (simp add: has_vector_derivative_def, 
   subst has_derivative_eq_rhs, 
   force intro: derivative_intros; 
   auto simp add: field_simps)

lemma has_vector_derivative_sqrt[derivative_intros]:
  fixes f :: "real \<Rightarrow> real"    
  assumes f: "(f has_vector_derivative f') (at x within s)"
  assumes "f x > 0"
  shows "((\<lambda>x. sqrt(f x)) has_vector_derivative (f' * 1/(2 * sqrt(f x)))) (at x within s)"
  using assms unfolding divide_inverse by prove_vec_deriv

lemma has_vector_derivative_sin[derivative_intros]:
  fixes f :: "real \<Rightarrow> real"    
  assumes f: "(f has_vector_derivative f') (at x within s)"
  shows "((\<lambda>x. sin(f x)) has_vector_derivative (f' * cos(f x))) (at x within s)"
  using assms by prove_vec_deriv
  
lemma has_vector_derivative_cos[derivative_intros]:
  fixes f :: "real \<Rightarrow> real"    
  assumes f: "(f has_vector_derivative f') (at x within s)"
  shows "((\<lambda>x. cos(f x)) has_vector_derivative (f' * - sin(f x))) (at x within s)"
  using assms by prove_vec_deriv

lemma has_vector_derivative_exp[derivative_intros]:
  fixes f :: "real \<Rightarrow> real"    
  assumes f: "(f has_vector_derivative f') (at x within s)"
  shows "((\<lambda>x. exp(f x)) has_vector_derivative (f' * exp(f x))) (at x within s)"
  using assms by prove_vec_deriv

lemma has_vector_derivative_ln[derivative_intros]:
  fixes f :: "real \<Rightarrow> real"    
  assumes f: "(f has_vector_derivative f') (at x within s)" "0 < f x"
  shows "((\<lambda>x. ln(f x)) has_vector_derivative (f' * inverse(f x))) (at x within s)"
  using assms by prove_vec_deriv

lemma has_vector_derivative_powr[derivative_intros]:
  fixes f :: "real \<Rightarrow> real" and g :: "real \<Rightarrow> real"
  assumes
    "(g has_vector_derivative g') (at x within X)"
    "(f has_vector_derivative f') (at x within X)"
    "0 < g x" "x \<in> X"
  shows "((\<lambda>x. g x powr f x) has_vector_derivative (g x powr f x * (f' * ln (g x) + g' * f x / g x))) (at x within X)"
  using assms by prove_vec_deriv

lemma max_simps [simp]: 
  "(y::real) < max x y \<longleftrightarrow> y < x" 
  "x < max x y \<longleftrightarrow> x < y"
  "max x y = y \<longleftrightarrow> x \<le> y"
  by auto
    
lemma min_simps [simp]:
  "min (x::real) y < x \<longleftrightarrow> y < x"
  "min x y < y \<longleftrightarrow> x < y"
  by auto

text \<open> These laws seem helpful for discharging real conjectures. \<close>

lemma real_sqrt_pow2_combine [simp]: "x > 0 \<Longrightarrow> sqrt x * (sqrt x * n) = x * n"
  by simp                                                                          

declare power2_eq_square [field_simps]

subsection \<open> Calculating derivatives \<close>

text \<open> We set up some nice syntax for taking derivatives by calculation, and prove associated
  theorems based on the Multivariate Analysis package. \<close>

notation frechet_derivative ("\<partial>")
notation vector_derivative ("\<partial>\<^sub>v")

lemma vector_derivative_chain_frechet: 
  fixes g :: "'a::ordered_euclidean_space \<Rightarrow> 'b::ordered_euclidean_space"
  assumes "f differentiable (at x)" "g differentiable (at (f x))"
  shows "\<partial>\<^sub>v (g \<circ> f) (at x) = \<partial> g (at (f x)) (\<partial>\<^sub>v f (at x))"
proof -
  have "(g has_derivative \<partial> g (at (f x))) (at (f x))"
    using assms(2) frechet_derivative_works by blast
  hence 1:"(g has_derivative \<partial> g (at (f x))) (at (f x) within range f)"
    by (simp add: has_derivative_at_withinI)
  from 1 assms show ?thesis
    by (auto intro: vector_derivative_chain_within simp add: at_eq_bot_iff)
qed

lemma frechet_derivative_const: "\<partial> (\<lambda> x. k) (at t) = (\<lambda> x. 0)"
  by (metis frechet_derivative_at has_derivative_const)

lemma frechet_derivative_Pair:
  assumes "f differentiable at t" "g differentiable at t"
  shows "\<partial> (\<lambda>x. (f x, g x)) (at t) = (\<lambda>x. (\<partial> f (at t) x, \<partial> g (at t) x))"
  by (metis (no_types) assms(1) assms(2) frechet_derivative_at frechet_derivative_works has_derivative_Pair)

lemma frechet_derivative_split:
  "\<partial> (\<lambda> (x, y). f x y) (at t) = \<partial> (\<lambda> p. f (fst p) (snd p)) (at t)"
  by (simp add: case_prod_beta')

lemma frechet_derivative_fst: "frechet_derivative fst (at t) = fst"
  by (metis bounded_linear_fst bounded_linear_imp_has_derivative frechet_derivative_at)

lemma frechet_derivative_snd: "frechet_derivative snd (at t) = snd"
  by (metis bounded_linear_imp_has_derivative bounded_linear_snd frechet_derivative_at)

lemma frechet_derivative_vec:
  fixes f :: "'i::finite \<Rightarrow> 'a::{real_normed_vector} \<Rightarrow> 'b::real_normed_vector"
  assumes "\<And> i. (f i) differentiable (at t)"
  shows "frechet_derivative (\<lambda> x. (\<chi> i. f i x)) (at t) = (\<lambda> x. (\<chi> i. frechet_derivative (f i) (at t) x))"
proof -
  have "((\<lambda>a. \<chi> i. f i a) has_derivative (\<lambda>a. \<chi> i. \<partial> (f i) (at t) a)) (at t)"
    by (metis (no_types) assms frechet_derivative_works has_derivative_vec)
  then show ?thesis
    by (metis (no_types) frechet_derivative_at)
qed

lemma differentiable_vec:
  fixes f :: "'i::finite \<Rightarrow> 'a::{real_normed_vector} \<Rightarrow> 'b::real_normed_vector"
  assumes "\<And> i. (f i) differentiable (at t)"
  shows "(\<lambda> x. \<chi> i. f i x) differentiable (at t)"
proof -
  have "\<forall>A i. (f i has_derivative \<partial> (f i) (at t)) (at t within A)"
    by (metis (no_types) assms differentiable_def frechet_derivative_at has_derivative_at_withinI)
  then have "\<forall>A. ((\<lambda>a. \<chi> i. f i a) has_derivative (\<lambda>a. \<chi> i. \<partial> (f i) (at t) a)) (at t within A)"
    by (simp add: has_derivative_vec)
  then show ?thesis
    using differentiable_def by blast
qed

lemma frechet_derivative_plus:
  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
  assumes "f differentiable (at t)" "g differentiable (at t)"
  shows "\<partial> (\<lambda> x. f x + g x) (at t) = (\<lambda> x. \<partial> f (at t) x + \<partial> g (at t) x)"
proof -
  have "((\<lambda>x. f x + g x) has_derivative (\<lambda>x. \<partial> f (at t) x + \<partial> g (at t) x)) (at t)"
    using assms(1) assms(2) frechet_derivative_works has_derivative_add by blast
  thus ?thesis
    using frechet_derivative_at by force
qed

lemma frechet_derivative_uminus:
  assumes "f differentiable (at t)"
  shows "\<partial> (\<lambda> x. - f x) (at t) = (\<lambda>x. - \<partial> f (at t) x)"
proof -
  have "((\<lambda>x. - f x) has_derivative (\<lambda>x. - \<partial> f (at t) x)) (at t)"
    using assms frechet_derivative_works has_derivative_minus by blast
  thus ?thesis
    using frechet_derivative_at by force
qed

lemma frechet_derivative_minus:
  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
  assumes "f differentiable (at t)" "g differentiable (at t)"
  shows "\<partial> (\<lambda> x. f x - g x) (at t) = (\<lambda> x. \<partial> f (at t) x - \<partial> g (at t) x)"
proof -
  have "((\<lambda>x. f x - g x) has_derivative (\<lambda>x. \<partial> f (at t) x - \<partial> g (at t) x)) (at t)"
    using assms(1) assms(2) frechet_derivative_works has_derivative_diff by blast
  thus ?thesis
    using frechet_derivative_at by force
qed

lemma frechet_derivative_mult:
  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
  assumes "f differentiable (at t)" "g differentiable (at t)"
  shows "\<partial> (\<lambda> x. f x * g x) (at t) = 
         (\<lambda> x. f t * \<partial> g (at t) x + \<partial> f (at t) x * g t)"
proof -
  have "((\<lambda>x. f x * g x) has_derivative (\<lambda> x. f t * \<partial> g (at t) x + \<partial> f (at t) x * g t)) (at t)"
    using assms(1) assms(2) frechet_derivative_works has_derivative_mult by blast
  thus ?thesis
    using frechet_derivative_at by force
qed

lemma frechet_derivative_scaleR:
  fixes g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
  assumes "f differentiable (at t)" "g differentiable (at t)"
  shows "\<partial> (\<lambda> x. f x *\<^sub>R g x) (at t) = 
         (\<lambda> x. f t *\<^sub>R \<partial> g (at t) x + \<partial> f (at t) x *\<^sub>R g t)"
proof -
  have "((\<lambda>x. f x *\<^sub>R g x) has_derivative (\<lambda> x. f t *\<^sub>R \<partial> g (at t) x + \<partial> f (at t) x *\<^sub>R g t)) (at t)"
  proof -
    have "(f has_derivative \<partial> f (at t)) (at t)"
      by (meson assms(1) frechet_derivative_works)
    then show ?thesis
      using assms(2) frechet_derivative_works has_derivative_scaleR by blast
  qed

  thus ?thesis
    using frechet_derivative_at by force
qed

lemma frechet_derivative_inner:
  fixes g :: "'a::{real_inner,real_normed_vector} \<Rightarrow> 'b::{real_inner,real_normed_vector}"
  assumes "f differentiable (at t)" "g differentiable (at t)"
  shows "\<partial> (\<lambda> x. f x \<bullet> g x) (at t) = 
         (\<lambda> x. f t \<bullet> \<partial> g (at t) x + \<partial> f (at t) x \<bullet> g t)"
proof -
  have "((\<lambda>x. f x \<bullet> g x) has_derivative (\<lambda> x. f t \<bullet> \<partial> g (at t) x + \<partial> f (at t) x \<bullet> g t)) (at t)"
  proof -
    have "(f has_derivative \<partial> f (at t)) (at t)"
      by (meson assms(1) frechet_derivative_works)
    then show ?thesis
      using assms(2) frechet_derivative_works has_derivative_inner by blast
  qed

  thus ?thesis
    using frechet_derivative_at by force
qed

lemma frechet_derivative_inverse: 
  fixes f :: "_ \<Rightarrow> (_::real_normed_div_algebra)"
  assumes "f differentiable at t" "f t \<noteq> 0"
  shows "\<partial> (\<lambda>x. inverse (f x)) (at t) = (\<lambda>x. - (inverse (f t) * \<partial> f (at t) x * inverse (f t)))"
proof -
  obtain f' where f':"(f has_derivative f') (at t)"
    using assms differentiable_def by blast
  have fd: "frechet_derivative f (at t) = f'"
    using f' frechet_derivative_at by auto

  from has_derivative_compose[OF f' has_derivative_inverse']
  have "((\<lambda>x. inverse (f x)) has_derivative (\<lambda>x. - (inverse (f t) * \<partial> f (at t) x * inverse (f t)))) (at t)"
    by (simp add: fd assms(2))

  thus ?thesis
    using frechet_derivative_at by force
qed

lemma frechet_derivative_divide:
  fixes f :: "_ \<Rightarrow> (_::real_normed_field)"
  assumes "f differentiable at t" "g differentiable at t" "g t \<noteq> 0"
  shows "\<partial> (\<lambda>x. f x / g x) (at t) = (\<lambda>x. \<partial> f (at t) x / g t - f t * (\<partial> g (at t) x / (g t)\<^sup>2))"
  by (simp add: divide_inverse frechet_derivative_mult frechet_derivative_inverse assms 
                power2_eq_square mult.assoc vector_space_over_itself.scale_left_commute)

lemma frechet_derivative_norm:
  fixes f :: "'a::{real_inner} \<Rightarrow> 'b::{real_inner}"
  assumes "f differentiable (at t)" "f t \<noteq> 0"
  shows "\<partial> (\<lambda> x. norm (f x)) (at t) = (\<lambda> x. \<partial> f (at t) x \<bullet> sgn (f t))"
proof -
  have "(norm \<circ> f has_derivative ((\<lambda> x. x \<bullet> sgn (f t)) \<circ> \<partial> f (at t))) (at t)"
    using assms(1) assms(2) diff_chain_at frechet_derivative_works has_derivative_norm by blast
  thus ?thesis
    by (metis assms differentiable_def frechet_derivative_at has_derivative_compose has_derivative_norm)
qed

lemma frechet_derivative_power:
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_field"
  assumes "f differentiable (at t)"
  shows "\<partial> (\<lambda> x. f x ^ n) (at t) = (\<lambda>y. of_nat n * \<partial> f (at t) y * f t ^ (n - 1))"
  using assms has_derivative_power[of f "\<partial> f (at t)" t UNIV n] frechet_derivative_at
  by (fastforce simp add: frechet_derivative_works)

lemma frechet_derivative_powr:
  fixes f :: "'a::{banach, real_normed_algebra_1} \<Rightarrow> real"
  assumes "f differentiable (at t)" "g differentiable (at t)" "0 < f t"
  shows "\<partial> (\<lambda> x. f x powr g x) (at t) = (\<lambda>h. f t powr g t * (\<partial> g (at t) h * ln (f t) + \<partial> f (at t) h * g t / f t))"
  using assms has_derivative_powr[of f "\<partial> f (at t)" t UNIV g "\<partial> g (at t)"] frechet_derivative_at
  by (fastforce simp add: frechet_derivative_works)

lemma frechet_derivative_ln:
  fixes f :: "'a::{banach, real_normed_algebra_1} \<Rightarrow> real"
  assumes "f differentiable (at t)" "0 < f t"
  shows "\<partial> (\<lambda> x. ln (f x)) (at t) = (\<lambda> x. \<partial> f (at t) x * inverse (f t))"
  by (metis assms(1) assms(2) frechet_derivative_at frechet_derivative_works has_derivative_ln)

lemma frechet_derivative_sin:
  fixes f :: "'a::{real_normed_vector} \<Rightarrow> real"
  assumes "f differentiable (at t)"
  shows "\<partial> (\<lambda> x. sin (f x)) (at t) = (\<lambda> x. \<partial> f (at t) x * cos (f t))"
  by (metis assms frechet_derivative_at frechet_derivative_works has_derivative_sin)

lemma frechet_derivative_cos:
  fixes f :: "'a::{real_normed_vector} \<Rightarrow> real"
  assumes "f differentiable (at t)"
  shows "\<partial> (\<lambda> x. cos (f x)) (at t) = (\<lambda> x. \<partial> f (at t) x * - sin (f t))"
  by (metis assms frechet_derivative_at frechet_derivative_works has_derivative_cos)

end