Theory Deriv

(*  Title:      HOL/Deriv.thy
    Author:     Jacques D. Fleuriot, University of Cambridge, 1998
    Author:     Brian Huffman
    Author:     Lawrence C Paulson, 2004
    Author:     Benjamin Porter, 2005
*)

section Differentiation

theory Deriv
  imports Limits
begin

subsection Frechet derivative

definition has_derivative :: "('a::real_normed_vector  'b::real_normed_vector) 
    ('a  'b)  'a filter  bool"  (infix "(has'_derivative)" 50)
  where "(f has_derivative f') F 
    bounded_linear f' 
    ((λy. ((f y - f (Lim F (λx. x))) - f' (y - Lim F (λx. x))) /R norm (y - Lim F (λx. x)))  0) F"

text 
  Usually the filter termF is termat x within s.  term(f has_derivative D)
  (at x within s) means: termD is the derivative of function termf at point termx
  within the set terms. Where terms is used to express left or right sided derivatives. In
  most cases terms is either a variable or termUNIV.


text These are the only cases we'll care about, probably.

lemma has_derivative_within: "(f has_derivative f') (at x within s) 
    bounded_linear f'  ((λy. (1 / norm(y - x)) *R (f y - (f x + f' (y - x))))  0) (at x within s)"
  unfolding has_derivative_def tendsto_iff
  by (subst eventually_Lim_ident_at) (auto simp add: field_simps)

lemma has_derivative_eq_rhs: "(f has_derivative f') F  f' = g'  (f has_derivative g') F"
  by simp

definition has_field_derivative :: "('a::real_normed_field  'a)  'a  'a filter  bool"
    (infix "(has'_field'_derivative)" 50)
  where "(f has_field_derivative D) F  (f has_derivative (*) D) F"

lemma DERIV_cong: "(f has_field_derivative X) F  X = Y  (f has_field_derivative Y) F"
  by simp

definition has_vector_derivative :: "(real  'b::real_normed_vector)  'b  real filter  bool"
    (infix "has'_vector'_derivative" 50)
  where "(f has_vector_derivative f') net  (f has_derivative (λx. x *R f')) net"

lemma has_vector_derivative_eq_rhs:
  "(f has_vector_derivative X) F  X = Y  (f has_vector_derivative Y) F"
  by simp

named_theorems derivative_intros "structural introduction rules for derivatives"
setup 
  let
    val eq_thms = @{thms has_derivative_eq_rhs DERIV_cong has_vector_derivative_eq_rhs}
    fun eq_rule thm = get_first (try (fn eq_thm => eq_thm OF [thm])) eq_thms
  in
    Global_Theory.add_thms_dynamic
      (bindingderivative_eq_intros,
        fn context =>
          Named_Theorems.get (Context.proof_of context) named_theorems‹derivative_intros›
          |> map_filter eq_rule)
  end


text 
  The following syntax is only used as a legacy syntax.

abbreviation (input)
  FDERIV :: "('a::real_normed_vector  'b::real_normed_vector)  'a   ('a  'b)  bool"
  ("(FDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
  where "FDERIV f x :> f'  (f has_derivative f') (at x)"

lemma has_derivative_bounded_linear: "(f has_derivative f') F  bounded_linear f'"
  by (simp add: has_derivative_def)

lemma has_derivative_linear: "(f has_derivative f') F  linear f'"
  using bounded_linear.linear[OF has_derivative_bounded_linear] .

lemma has_derivative_ident[derivative_intros, simp]: "((λx. x) has_derivative (λx. x)) F"
  by (simp add: has_derivative_def)

lemma has_derivative_id [derivative_intros, simp]: "(id has_derivative id) (at a)"
  by (metis eq_id_iff has_derivative_ident)

lemma has_derivative_const[derivative_intros, simp]: "((λx. c) has_derivative (λx. 0)) F"
  by (simp add: has_derivative_def)

lemma (in bounded_linear) bounded_linear: "bounded_linear f" ..

lemma (in bounded_linear) has_derivative:
  "(g has_derivative g') F  ((λx. f (g x)) has_derivative (λx. f (g' x))) F"
  unfolding has_derivative_def
  by (auto simp add: bounded_linear_compose [OF bounded_linear] scaleR diff dest: tendsto)

lemmas has_derivative_scaleR_right [derivative_intros] =
  bounded_linear.has_derivative [OF bounded_linear_scaleR_right]

lemmas has_derivative_scaleR_left [derivative_intros] =
  bounded_linear.has_derivative [OF bounded_linear_scaleR_left]

lemmas has_derivative_mult_right [derivative_intros] =
  bounded_linear.has_derivative [OF bounded_linear_mult_right]

lemmas has_derivative_mult_left [derivative_intros] =
  bounded_linear.has_derivative [OF bounded_linear_mult_left]

lemmas has_derivative_of_real[derivative_intros, simp] = 
  bounded_linear.has_derivative[OF bounded_linear_of_real] 

lemma has_derivative_add[simp, derivative_intros]:
  assumes f: "(f has_derivative f') F"
    and g: "(g has_derivative g') F"
  shows "((λx. f x + g x) has_derivative (λx. f' x + g' x)) F"
  unfolding has_derivative_def
proof safe
  let ?x = "Lim F (λx. x)"
  let ?D = "λf f' y. ((f y - f ?x) - f' (y - ?x)) /R norm (y - ?x)"
  have "((λx. ?D f f' x + ?D g g' x)  (0 + 0)) F"
    using f g by (intro tendsto_add) (auto simp: has_derivative_def)
  then show "(?D (λx. f x + g x) (λx. f' x + g' x)  0) F"
    by (simp add: field_simps scaleR_add_right scaleR_diff_right)
qed (blast intro: bounded_linear_add f g has_derivative_bounded_linear)

lemma has_derivative_sum[simp, derivative_intros]:
  "(i. i  I  (f i has_derivative f' i) F) 
    ((λx. iI. f i x) has_derivative (λx. iI. f' i x)) F"
  by (induct I rule: infinite_finite_induct) simp_all

lemma has_derivative_minus[simp, derivative_intros]:
  "(f has_derivative f') F  ((λx. - f x) has_derivative (λx. - f' x)) F"
  using has_derivative_scaleR_right[of f f' F "-1"] by simp

lemma has_derivative_diff[simp, derivative_intros]:
  "(f has_derivative f') F  (g has_derivative g') F 
    ((λx. f x - g x) has_derivative (λx. f' x - g' x)) F"
  by (simp only: diff_conv_add_uminus has_derivative_add has_derivative_minus)

lemma has_derivative_at_within:
  "(f has_derivative f') (at x within s) 
    (bounded_linear f'  ((λy. ((f y - f x) - f' (y - x)) /R norm (y - x))  0) (at x within s))"
proof (cases "at x within s = bot")
  case True
  then show ?thesis
    by (metis (no_types, lifting) has_derivative_within tendsto_bot)
next
  case False
  then show ?thesis
  by (simp add: Lim_ident_at has_derivative_def)
qed

lemma has_derivative_iff_norm:
  "(f has_derivative f') (at x within s) 
    bounded_linear f'  ((λy. norm ((f y - f x) - f' (y - x)) / norm (y - x))  0) (at x within s)"
  using tendsto_norm_zero_iff[of _ "at x within s", where 'b="'b", symmetric]
  by (simp add: has_derivative_at_within divide_inverse ac_simps)

lemma has_derivative_at:
  "(f has_derivative D) (at x) 
    (bounded_linear D  (λh. norm (f (x + h) - f x - D h) / norm h) 0 0)"
  by (simp add: has_derivative_iff_norm LIM_offset_zero_iff)

lemma field_has_derivative_at:
  fixes x :: "'a::real_normed_field"
  shows "(f has_derivative (*) D) (at x)  (λh. (f (x + h) - f x) / h) 0 D" (is "?lhs = ?rhs")
proof -
  have "?lhs = (λh. norm (f (x + h) - f x - D * h) / norm h) 0  0"
    by (simp add: bounded_linear_mult_right has_derivative_at)
  also have "... = (λy. norm ((f (x + y) - f x - D * y) / y)) 0 0"
    by (simp cong: LIM_cong flip: nonzero_norm_divide)
  also have "... = (λy. norm ((f (x + y) - f x) / y - D / y * y)) 0 0"
    by (simp only: diff_divide_distrib times_divide_eq_left [symmetric])
  also have "... = ?rhs"
    by (simp add: tendsto_norm_zero_iff LIM_zero_iff cong: LIM_cong)
  finally show ?thesis .
qed

lemma has_derivative_iff_Ex:
  "(f has_derivative f') (at x) 
    bounded_linear f'  (e. (h. f (x+h) = f x + f' h + e h)  ((λh. norm (e h) / norm h)  0) (at 0))"
  unfolding has_derivative_at by force

lemma has_derivative_at_within_iff_Ex:
  assumes "x  S" "open S"
  shows "(f has_derivative f') (at x within S) 
         bounded_linear f'  (e. (h. x+h  S  f (x+h) = f x + f' h + e h)  ((λh. norm (e h) / norm h)  0) (at 0))"
    (is "?lhs = ?rhs")
proof safe
  show "bounded_linear f'"
    if "(f has_derivative f') (at x within S)"
    using has_derivative_bounded_linear that by blast
  show "e. (h. x + h  S  f (x + h) = f x + f' h + e h)  (λh. norm (e h) / norm h) 0 0"
    if "(f has_derivative f') (at x within S)"
    by (metis (full_types) assms that has_derivative_iff_Ex at_within_open)
  show "(f has_derivative f') (at x within S)"
    if "bounded_linear f'"
      and eq [rule_format]: "h. x + h  S  f (x + h) = f x + f' h + e h"
      and 0: "(λh. norm (e (h::'a)::'b) / norm h) 0 0"
    for e 
  proof -
    have 1: "f y - f x = f' (y-x) + e (y-x)" if "y  S" for y
      using eq [of "y-x"] that by simp
    have 2: "((λy. norm (e (y-x)) / norm (y - x))  0) (at x within S)"
      by (simp add: "0" assms tendsto_offset_zero_iff)
    have "((λy. norm (f y - f x - f' (y - x)) / norm (y - x))  0) (at x within S)"
      by (simp add: Lim_cong_within 1 2)
    then show ?thesis
      by (simp add: has_derivative_iff_norm bounded_linear f')
  qed
qed

lemma has_derivativeI:
  "bounded_linear f' 
    ((λy. ((f y - f x) - f' (y - x)) /R norm (y - x))  0) (at x within s) 
    (f has_derivative f') (at x within s)"
  by (simp add: has_derivative_at_within)

lemma has_derivativeI_sandwich:
  assumes e: "0 < e"
    and bounded: "bounded_linear f'"
    and sandwich: "(y. y  s  y  x  dist y x < e 
      norm ((f y - f x) - f' (y - x)) / norm (y - x)  H y)"
    and "(H  0) (at x within s)"
  shows "(f has_derivative f') (at x within s)"
  unfolding has_derivative_iff_norm
proof safe
  show "((λy. norm (f y - f x - f' (y - x)) / norm (y - x))  0) (at x within s)"
  proof (rule tendsto_sandwich[where f="λx. 0"])
    show "(H  0) (at x within s)" by fact
    show "eventually (λn. norm (f n - f x - f' (n - x)) / norm (n - x)  H n) (at x within s)"
      unfolding eventually_at using e sandwich by auto
  qed (auto simp: le_divide_eq)
qed fact

lemma has_derivative_subset:
  "(f has_derivative f') (at x within s)  t  s  (f has_derivative f') (at x within t)"
  by (auto simp add: has_derivative_iff_norm intro: tendsto_within_subset)

lemma has_derivative_within_singleton_iff:
  "(f has_derivative g) (at x within {x})  bounded_linear g"
  by (auto intro!: has_derivativeI_sandwich[where e=1] has_derivative_bounded_linear)


subsubsection Limit transformation for derivatives

lemma has_derivative_transform_within:
  assumes "(f has_derivative f') (at x within s)"
    and "0 < d"
    and "x  s"
    and "x'. x'  s; dist x' x < d  f x' = g x'"
  shows "(g has_derivative f') (at x within s)"
  using assms
  unfolding has_derivative_within
  by (force simp add: intro: Lim_transform_within)

lemma has_derivative_transform_within_open:
  assumes "(f has_derivative f') (at x within t)"
    and "open s"
    and "x  s"
    and "x. xs  f x = g x"
  shows "(g has_derivative f') (at x within t)"
  using assms unfolding has_derivative_within
  by (force simp add: intro: Lim_transform_within_open)

lemma has_derivative_transform:
  assumes "x  s" "x. x  s  g x = f x"
  assumes "(f has_derivative f') (at x within s)"
  shows "(g has_derivative f') (at x within s)"
  using assms
  by (intro has_derivative_transform_within[OF _ zero_less_one, where g=g]) auto

lemma has_derivative_transform_eventually:
  assumes "(f has_derivative f') (at x within s)"
    "(F x' in at x within s. f x' = g x')"
  assumes "f x = g x" "x  s"
  shows "(g has_derivative f') (at x within s)"
  using assms
proof -
  from assms(2,3) obtain d where "d > 0" "x'. x'  s  dist x' x < d  f x' = g x'"
    by (force simp: eventually_at)
  from has_derivative_transform_within[OF assms(1) this(1) assms(4) this(2)]
  show ?thesis .
qed

lemma has_field_derivative_transform_within:
  assumes "(f has_field_derivative f') (at a within S)"
    and "0 < d"
    and "a  S"
    and "x. x  S; dist x a < d  f x = g x"
  shows "(g has_field_derivative f') (at a within S)"
  using assms unfolding has_field_derivative_def
  by (metis has_derivative_transform_within)

lemma has_field_derivative_transform_within_open:
  assumes "(f has_field_derivative f') (at a)"
    and "open S" "a  S"
    and "x. x  S  f x = g x"
  shows "(g has_field_derivative f') (at a)"
  using assms unfolding has_field_derivative_def
  by (metis has_derivative_transform_within_open)


subsection Continuity

lemma has_derivative_continuous:
  assumes f: "(f has_derivative f') (at x within s)"
  shows "continuous (at x within s) f"
proof -
  from f interpret F: bounded_linear f'
    by (rule has_derivative_bounded_linear)
  note F.tendsto[tendsto_intros]
  let ?L = "λf. (f  0) (at x within s)"
  have "?L (λy. norm ((f y - f x) - f' (y - x)) / norm (y - x))"
    using f unfolding has_derivative_iff_norm by blast
  then have "?L (λy. norm ((f y - f x) - f' (y - x)) / norm (y - x) * norm (y - x))" (is ?m)
    by (rule tendsto_mult_zero) (auto intro!: tendsto_eq_intros)
  also have "?m  ?L (λy. norm ((f y - f x) - f' (y - x)))"
    by (intro filterlim_cong) (simp_all add: eventually_at_filter)
  finally have "?L (λy. (f y - f x) - f' (y - x))"
    by (rule tendsto_norm_zero_cancel)
  then have "?L (λy. ((f y - f x) - f' (y - x)) + f' (y - x))"
    by (rule tendsto_eq_intros) (auto intro!: tendsto_eq_intros simp: F.zero)
  then have "?L (λy. f y - f x)"
    by simp
  from tendsto_add[OF this tendsto_const, of "f x"] show ?thesis
    by (simp add: continuous_within)
qed


subsection Composition

lemma tendsto_at_iff_tendsto_nhds_within:
  "f x = y  (f  y) (at x within s)  (f  y) (inf (nhds x) (principal s))"
  unfolding tendsto_def eventually_inf_principal eventually_at_filter
  by (intro ext all_cong imp_cong) (auto elim!: eventually_mono)

lemma has_derivative_in_compose:
  assumes f: "(f has_derivative f') (at x within s)"
    and g: "(g has_derivative g') (at (f x) within (f`s))"
  shows "((λx. g (f x)) has_derivative (λx. g' (f' x))) (at x within s)"
proof -
  from f interpret F: bounded_linear f'
    by (rule has_derivative_bounded_linear)
  from g interpret G: bounded_linear g'
    by (rule has_derivative_bounded_linear)
  from F.bounded obtain kF where kF: "x. norm (f' x)  norm x * kF"
    by fast
  from G.bounded obtain kG where kG: "x. norm (g' x)  norm x * kG"
    by fast
  note G.tendsto[tendsto_intros]

  let ?L = "λf. (f  0) (at x within s)"
  let ?D = "λf f' x y. (f y - f x) - f' (y - x)"
  let ?N = "λf f' x y. norm (?D f f' x y) / norm (y - x)"
  let ?gf = "λx. g (f x)" and ?gf' = "λx. g' (f' x)"
  define Nf where "Nf = ?N f f' x"
  define Ng where [abs_def]: "Ng y = ?N g g' (f x) (f y)" for y

  show ?thesis
  proof (rule has_derivativeI_sandwich[of 1])
    show "bounded_linear (λx. g' (f' x))"
      using f g by (blast intro: bounded_linear_compose has_derivative_bounded_linear)
  next
    fix y :: 'a
    assume neq: "y  x"
    have "?N ?gf ?gf' x y = norm (g' (?D f f' x y) + ?D g g' (f x) (f y)) / norm (y - x)"
      by (simp add: G.diff G.add field_simps)
    also have "  norm (g' (?D f f' x y)) / norm (y - x) + Ng y * (norm (f y - f x) / norm (y - x))"
      by (simp add: add_divide_distrib[symmetric] divide_right_mono norm_triangle_ineq G.zero Ng_def)
    also have "  Nf y * kG + Ng y * (Nf y + kF)"
    proof (intro add_mono mult_left_mono)
      have "norm (f y - f x) = norm (?D f f' x y + f' (y - x))"
        by simp
      also have "  norm (?D f f' x y) + norm (f' (y - x))"
        by (rule norm_triangle_ineq)
      also have "  norm (?D f f' x y) + norm (y - x) * kF"
        using kF by (intro add_mono) simp
      finally show "norm (f y - f x) / norm (y - x)  Nf y + kF"
        by (simp add: neq Nf_def field_simps)
    qed (use kG in simp_all add: Ng_def Nf_def neq zero_le_divide_iff field_simps)
    finally show "?N ?gf ?gf' x y  Nf y * kG + Ng y * (Nf y + kF)" .
  next
    have [tendsto_intros]: "?L Nf"
      using f unfolding has_derivative_iff_norm Nf_def ..
    from f have "(f  f x) (at x within s)"
      by (blast intro: has_derivative_continuous continuous_within[THEN iffD1])
    then have f': "LIM x at x within s. f x :> inf (nhds (f x)) (principal (f`s))"
      unfolding filterlim_def
      by (simp add: eventually_filtermap eventually_at_filter le_principal)

    have "((?N g  g' (f x))  0) (at (f x) within f`s)"
      using g unfolding has_derivative_iff_norm ..
    then have g': "((?N g  g' (f x))  0) (inf (nhds (f x)) (principal (f`s)))"
      by (rule tendsto_at_iff_tendsto_nhds_within[THEN iffD1, rotated]) simp

    have [tendsto_intros]: "?L Ng"
      unfolding Ng_def by (rule filterlim_compose[OF g' f'])
    show "((λy. Nf y * kG + Ng y * (Nf y + kF))  0) (at x within s)"
      by (intro tendsto_eq_intros) auto
  qed simp
qed

lemma has_derivative_compose:
  "(f has_derivative f') (at x within s)  (g has_derivative g') (at (f x)) 
  ((λx. g (f x)) has_derivative (λx. g' (f' x))) (at x within s)"
  by (blast intro: has_derivative_in_compose has_derivative_subset)

lemma has_derivative_in_compose2:
  assumes "x. x  t  (g has_derivative g' x) (at x within t)"
  assumes "f ` s  t" "x  s"
  assumes "(f has_derivative f') (at x within s)"
  shows "((λx. g (f x)) has_derivative (λy. g' (f x) (f' y))) (at x within s)"
  using assms
  by (auto intro: has_derivative_subset intro!: has_derivative_in_compose[of f f' x s g])

lemma (in bounded_bilinear) FDERIV:
  assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)"
  shows "((λx. f x ** g x) has_derivative (λh. f x ** g' h + f' h ** g x)) (at x within s)"
proof -
  from bounded_linear.bounded [OF has_derivative_bounded_linear [OF f]]
  obtain KF where norm_F: "x. norm (f' x)  norm x * KF" by fast

  from pos_bounded obtain K
    where K: "0 < K" and norm_prod: "a b. norm (a ** b)  norm a * norm b * K"
    by fast
  let ?D = "λf f' y. f y - f x - f' (y - x)"
  let ?N = "λf f' y. norm (?D f f' y) / norm (y - x)"
  define Ng where "Ng = ?N g g'"
  define Nf where "Nf = ?N f f'"

  let ?fun1 = "λy. norm (f y ** g y - f x ** g x - (f x ** g' (y - x) + f' (y - x) ** g x)) / norm (y - x)"
  let ?fun2 = "λy. norm (f x) * Ng y * K + Nf y * norm (g y) * K + KF * norm (g y - g x) * K"
  let ?F = "at x within s"

  show ?thesis
  proof (rule has_derivativeI_sandwich[of 1])
    show "bounded_linear (λh. f x ** g' h + f' h ** g x)"
      by (intro bounded_linear_add
        bounded_linear_compose [OF bounded_linear_right] bounded_linear_compose [OF bounded_linear_left]
        has_derivative_bounded_linear [OF g] has_derivative_bounded_linear [OF f])
  next
    from g have "(g  g x) ?F"
      by (intro continuous_within[THEN iffD1] has_derivative_continuous)
    moreover from f g have "(Nf  0) ?F" "(Ng  0) ?F"
      by (simp_all add: has_derivative_iff_norm Ng_def Nf_def)
    ultimately have "(?fun2  norm (f x) * 0 * K + 0 * norm (g x) * K + KF * norm (0::'b) * K) ?F"
      by (intro tendsto_intros) (simp_all add: LIM_zero_iff)
    then show "(?fun2  0) ?F"
      by simp
  next
    fix y :: 'd
    assume "y  x"
    have "?fun1 y =
        norm (f x ** ?D g g' y + ?D f f' y ** g y + f' (y - x) ** (g y - g x)) / norm (y - x)"
      by (simp add: diff_left diff_right add_left add_right field_simps)
    also have "  (norm (f x) * norm (?D g g' y) * K + norm (?D f f' y) * norm (g y) * K +
        norm (y - x) * KF * norm (g y - g x) * K) / norm (y - x)"
      by (intro divide_right_mono mult_mono'
                order_trans [OF norm_triangle_ineq add_mono]
                order_trans [OF norm_prod mult_right_mono]
                mult_nonneg_nonneg order_refl norm_ge_zero norm_F
                K [THEN order_less_imp_le])
    also have " = ?fun2 y"
      by (simp add: add_divide_distrib Ng_def Nf_def)
    finally show "?fun1 y  ?fun2 y" .
  qed simp
qed

lemmas has_derivative_mult[simp, derivative_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_mult]
lemmas has_derivative_scaleR[simp, derivative_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_scaleR]

lemma has_derivative_prod[simp, derivative_intros]:
  fixes f :: "'i  'a::real_normed_vector  'b::real_normed_field"
  shows "(i. i  I  (f i has_derivative f' i) (at x within S)) 
    ((λx. iI. f i x) has_derivative (λy. iI. f' i y * (jI - {i}. f j x))) (at x within S)"
proof (induct I rule: infinite_finite_induct)
  case infinite
  then show ?case by simp
next
  case empty
  then show ?case by simp
next
  case (insert i I)
  let ?P = "λy. f i x * (iI. f' i y * (jI - {i}. f j x)) + (f' i y) * (iI. f i x)"
  have "((λx. f i x * (iI. f i x)) has_derivative ?P) (at x within S)"
    using insert by (intro has_derivative_mult) auto
  also have "?P = (λy. i'insert i I. f' i' y * (jinsert i I - {i'}. f j x))"
    using insert(1,2)
    by (auto simp add: sum_distrib_left insert_Diff_if intro!: ext sum.cong)
  finally show ?case
    using insert by simp
qed

lemma has_derivative_power[simp, derivative_intros]:
  fixes f :: "'a :: real_normed_vector  'b :: real_normed_field"
  assumes f: "(f has_derivative f') (at x within S)"
  shows "((λx. f x^n) has_derivative (λy. of_nat n * f' y * f x^(n - 1))) (at x within S)"
  using has_derivative_prod[OF f, of "{..< n}"] by (simp add: prod_constant ac_simps)

lemma has_derivative_inverse':
  fixes x :: "'a::real_normed_div_algebra"
  assumes x: "x  0"
  shows "(inverse has_derivative (λh. - (inverse x * h * inverse x))) (at x within S)"
    (is "(_ has_derivative ?f) _")
proof (rule has_derivativeI_sandwich)
  show "bounded_linear (λh. - (inverse x * h * inverse x))"
    by (simp add: bounded_linear_minus bounded_linear_mult_const bounded_linear_mult_right)
  show "0 < norm x" using x by simp
  have "(inverse  inverse x) (at x within S)"
    using tendsto_inverse tendsto_ident_at x by auto
  then show "((λy. norm (inverse y - inverse x) * norm (inverse x))  0) (at x within S)"
    by (simp add: LIM_zero_iff tendsto_mult_left_zero tendsto_norm_zero)
next
  fix y :: 'a
  assume h: "y  x" "dist y x < norm x"
  then have "y  0" by auto
  have "norm (inverse y - inverse x - ?f (y -x)) / norm (y - x) 
        = norm (- (inverse y * (y - x) * inverse x - inverse x * (y - x) * inverse x)) /
                norm (y - x)"
    by (simp add: y  0 inverse_diff_inverse x)
  also have "... = norm ((inverse y - inverse x) * (y - x) * inverse x) / norm (y - x)"
    by (simp add: left_diff_distrib norm_minus_commute)
  also have "  norm (inverse y - inverse x) * norm (y - x) * norm (inverse x) / norm (y - x)"
    by (simp add: norm_mult)
  also have " = norm (inverse y - inverse x) * norm (inverse x)"
    by simp
  finally show "norm (inverse y - inverse x - ?f (y -x)) / norm (y - x) 
    norm (inverse y - inverse x) * norm (inverse x)" .
qed

lemma has_derivative_inverse[simp, derivative_intros]:
  fixes f :: "_  'a::real_normed_div_algebra"
  assumes x:  "f x  0"
    and f: "(f has_derivative f') (at x within S)"
  shows "((λx. inverse (f x)) has_derivative (λh. - (inverse (f x) * f' h * inverse (f x))))
    (at x within S)"
  using has_derivative_compose[OF f has_derivative_inverse', OF x] .

lemma has_derivative_divide[simp, derivative_intros]:
  fixes f :: "_  'a::real_normed_div_algebra"
  assumes f: "(f has_derivative f') (at x within S)"
    and g: "(g has_derivative g') (at x within S)"
  assumes x: "g x  0"
  shows "((λx. f x / g x) has_derivative
                (λh. - f x * (inverse (g x) * g' h * inverse (g x)) + f' h / g x)) (at x within S)"
  using has_derivative_mult[OF f has_derivative_inverse[OF x g]]
  by (simp add: field_simps)

lemma has_derivative_power_int':
  fixes x :: "'a::real_normed_field"
  assumes x: "x  0"
  shows "((λx. power_int x n) has_derivative (λy. y * (of_int n * power_int x (n - 1)))) (at x within S)"
proof (cases n rule: int_cases4)
  case (nonneg n)
  thus ?thesis using x
    by (cases "n = 0") (auto intro!: derivative_eq_intros simp: field_simps power_int_diff fun_eq_iff
                             simp flip: power_Suc)
next
  case (neg n)
  thus ?thesis using x
    by (auto intro!: derivative_eq_intros simp: field_simps power_int_diff power_int_minus
             simp flip: power_Suc power_Suc2 power_add)
qed

lemma has_derivative_power_int[simp, derivative_intros]:
  fixes f :: "_  'a::real_normed_field"
  assumes x:  "f x  0"
    and f: "(f has_derivative f') (at x within S)"
  shows "((λx. power_int (f x) n) has_derivative (λh. f' h * (of_int n * power_int (f x) (n - 1))))
           (at x within S)"
  using has_derivative_compose[OF f has_derivative_power_int', OF x] .


text Conventional form requires mult-AC laws. Types real and complex only.

lemma has_derivative_divide'[derivative_intros]:
  fixes f :: "_  'a::real_normed_field"
  assumes f: "(f has_derivative f') (at x within S)"
    and g: "(g has_derivative g') (at x within S)"
    and x: "g x  0"
  shows "((λx. f x / g x) has_derivative (λh. (f' h * g x - f x * g' h) / (g x * g x))) (at x within S)"
proof -
  have "f' h / g x - f x * (inverse (g x) * g' h * inverse (g x)) =
      (f' h * g x - f x * g' h) / (g x * g x)" for h
    by (simp add: field_simps x)
  then show ?thesis
    using has_derivative_divide [OF f g] x
    by simp
qed


subsection Uniqueness

text 
This can not generally shown for consthas_derivative, as we need to approach the point from
all directions. There is a proof in Analysis› for euclidean_space›.


lemma has_derivative_at2: "(f has_derivative f') (at x) 
    bounded_linear f'  ((λy. (1 / (norm(y - x))) *R (f y - (f x + f' (y - x))))  0) (at x)"
  using has_derivative_within [of f f' x UNIV]
  by simp

lemma has_derivative_zero_unique:
  assumes "((λx. 0) has_derivative F) (at x)"
  shows "F = (λh. 0)"
proof -
  interpret F: bounded_linear F
    using assms by (rule has_derivative_bounded_linear)
  let ?r = "λh. norm (F h) / norm h"
  have *: "?r 0 0"
    using assms unfolding has_derivative_at by simp
  show "F = (λh. 0)"
  proof
    show "F h = 0" for h
    proof (rule ccontr)
      assume **: "¬ ?thesis"
      then have h: "h  0"
        by (auto simp add: F.zero)
      with ** have "0 < ?r h"
        by simp
      from LIM_D [OF * this] obtain S
        where S: "0 < S" and r: "x. x  0  norm x < S  ?r x < ?r h"
        by auto
      from dense [OF S] obtain t where t: "0 < t  t < S" ..
      let ?x = "scaleR (t / norm h) h"
      have "?x  0" and "norm ?x < S"
        using t h by simp_all
      then have "?r ?x < ?r h"
        by (rule r)
      then show False
        using t h by (simp add: F.scaleR)
    qed
  qed
qed

lemma has_derivative_unique:
  assumes "(f has_derivative F) (at x)"
    and "(f has_derivative F') (at x)"
  shows "F = F'"
proof -
  have "((λx. 0) has_derivative (λh. F h - F' h)) (at x)"
    using has_derivative_diff [OF assms] by simp
  then have "(λh. F h - F' h) = (λh. 0)"
    by (rule has_derivative_zero_unique)
  then show "F = F'"
    unfolding fun_eq_iff right_minus_eq .
qed

lemma has_derivative_Uniq: "1F. (f has_derivative F) (at x)"
  by (simp add: Uniq_def has_derivative_unique)


subsection Differentiability predicate

definition differentiable :: "('a::real_normed_vector  'b::real_normed_vector)  'a filter  bool"
    (infix "differentiable" 50)
  where "f differentiable F  (D. (f has_derivative D) F)"

lemma differentiable_subset:
  "f differentiable (at x within s)  t  s  f differentiable (at x within t)"
  unfolding differentiable_def by (blast intro: has_derivative_subset)

lemmas differentiable_within_subset = differentiable_subset

lemma differentiable_ident [simp, derivative_intros]: "(λx. x) differentiable F"
  unfolding differentiable_def by (blast intro: has_derivative_ident)

lemma differentiable_const [simp, derivative_intros]: "(λz. a) differentiable F"
  unfolding differentiable_def by (blast intro: has_derivative_const)

lemma differentiable_in_compose:
  "f differentiable (at (g x) within (g`s))  g differentiable (at x within s) 
    (λx. f (g x)) differentiable (at x within s)"
  unfolding differentiable_def by (blast intro: has_derivative_in_compose)

lemma differentiable_compose:
  "f differentiable (at (g x))  g differentiable (at x within s) 
    (λx. f (g x)) differentiable (at x within s)"
  by (blast intro: differentiable_in_compose differentiable_subset)

lemma differentiable_add [simp, derivative_intros]:
  "f differentiable F  g differentiable F  (λx. f x + g x) differentiable F"
  unfolding differentiable_def by (blast intro: has_derivative_add)

lemma differentiable_sum[simp, derivative_intros]:
  assumes "finite s" "as. (f a) differentiable net"
  shows "(λx. sum (λa. f a x) s) differentiable net"
proof -
  from bchoice[OF assms(2)[unfolded differentiable_def]]
  show ?thesis
    by (auto intro!: has_derivative_sum simp: differentiable_def)
qed

lemma differentiable_minus [simp, derivative_intros]:
  "f differentiable F  (λx. - f x) differentiable F"
  unfolding differentiable_def by (blast intro: has_derivative_minus)

lemma differentiable_diff [simp, derivative_intros]:
  "f differentiable F  g differentiable F  (λx. f x - g x) differentiable F"
  unfolding differentiable_def by (blast intro: has_derivative_diff)

lemma differentiable_mult [simp, derivative_intros]:
  fixes f g :: "'a::real_normed_vector  'b::real_normed_algebra"
  shows "f differentiable (at x within s)  g differentiable (at x within s) 
    (λx. f x * g x) differentiable (at x within s)"
  unfolding differentiable_def by (blast intro: has_derivative_mult)

lemma differentiable_cmult_left_iff [simp]:
  fixes c::"'a::real_normed_field" 
  shows "(λt. c * q t) differentiable at t  c = 0  (λt. q t) differentiable at t" (is "?lhs = ?rhs")
proof
  assume L: ?lhs
  {assume "c  0"
    then have "q differentiable at t"
      using differentiable_mult [OF differentiable_const L, of concl: "1/c"] by auto
  } then show ?rhs
    by auto
qed auto

lemma differentiable_cmult_right_iff [simp]:
  fixes c::"'a::real_normed_field" 
  shows "(λt. q t * c) differentiable at t  c = 0  (λt. q t) differentiable at t" (is "?lhs = ?rhs")
  by (simp add: mult.commute flip: differentiable_cmult_left_iff)

lemma differentiable_inverse [simp, derivative_intros]:
  fixes f :: "'a::real_normed_vector  'b::real_normed_field"
  shows "f differentiable (at x within s)  f x  0 
    (λx. inverse (f x)) differentiable (at x within s)"
  unfolding differentiable_def by (blast intro: has_derivative_inverse)

lemma differentiable_divide [simp, derivative_intros]:
  fixes f g :: "'a::real_normed_vector  'b::real_normed_field"
  shows "f differentiable (at x within s)  g differentiable (at x within s) 
    g x  0  (λx. f x / g x) differentiable (at x within s)"
  unfolding divide_inverse by simp

lemma differentiable_power [simp, derivative_intros]:
  fixes f g :: "'a::real_normed_vector  'b::real_normed_field"
  shows "f differentiable (at x within s)  (λx. f x ^ n) differentiable (at x within s)"
  unfolding differentiable_def by (blast intro: has_derivative_power)

lemma differentiable_power_int [simp, derivative_intros]:
  fixes f :: "'a::real_normed_vector  'b::real_normed_field"
  shows "f differentiable (at x within s)  f x  0 
           (λx. power_int (f x) n) differentiable (at x within s)"
  unfolding differentiable_def by (blast intro: has_derivative_power_int)

lemma differentiable_scaleR [simp, derivative_intros]:
  "f differentiable (at x within s)  g differentiable (at x within s) 
    (λx. f x *R g x) differentiable (at x within s)"
  unfolding differentiable_def by (blast intro: has_derivative_scaleR)

lemma has_derivative_imp_has_field_derivative:
  "(f has_derivative D) F  (x. x * D' = D x)  (f has_field_derivative D') F"
  unfolding has_field_derivative_def
  by (rule has_derivative_eq_rhs[of f D]) (simp_all add: fun_eq_iff mult.commute)

lemma has_field_derivative_imp_has_derivative:
  "(f has_field_derivative D) F  (f has_derivative (*) D) F"
  by (simp add: has_field_derivative_def)

lemma DERIV_subset:
  "(f has_field_derivative f') (at x within s)  t  s 
    (f has_field_derivative f') (at x within t)"
  by (simp add: has_field_derivative_def has_derivative_subset)

lemma has_field_derivative_at_within:
  "(f has_field_derivative f') (at x)  (f has_field_derivative f') (at x within s)"
  using DERIV_subset by blast

abbreviation (input)
  DERIV :: "('a::real_normed_field  'a)  'a  'a  bool"
    ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
  where "DERIV f x :> D  (f has_field_derivative D) (at x)"

abbreviation has_real_derivative :: "(real  real)  real  real filter  bool"
    (infix "(has'_real'_derivative)" 50)
  where "(f has_real_derivative D) F  (f has_field_derivative D) F"

lemma real_differentiable_def:
  "f differentiable at x within s  (D. (f has_real_derivative D) (at x within s))"
proof safe
  assume "f differentiable at x within s"
  then obtain f' where *: "(f has_derivative f') (at x within s)"
    unfolding differentiable_def by auto
  then obtain c where "f' = ((*) c)"
    by (metis real_bounded_linear has_derivative_bounded_linear mult.commute fun_eq_iff)
  with * show "D. (f has_real_derivative D) (at x within s)"
    unfolding has_field_derivative_def by auto
qed (auto simp: differentiable_def has_field_derivative_def)

lemma real_differentiableE [elim?]:
  assumes f: "f differentiable (at x within s)"
  obtains df where "(f has_real_derivative df) (at x within s)"
  using assms by (auto simp: real_differentiable_def)

lemma has_field_derivative_iff:
  "(f has_field_derivative D) (at x within S) 
    ((λy. (f y - f x) / (y - x))  D) (at x within S)"
proof -
  have "((λy. norm (f y - f x - D * (y - x)) / norm (y - x))  0) (at x within S) 
      = ((λy. (f y - f x) / (y - x) - D)  0) (at x within S)"
    apply (subst tendsto_norm_zero_iff[symmetric], rule filterlim_cong)
      apply (simp_all add: eventually_at_filter field_simps nonzero_norm_divide)
    done
  then show ?thesis
    by (simp add: has_field_derivative_def has_derivative_iff_norm bounded_linear_mult_right LIM_zero_iff)
qed

lemma DERIV_def: "DERIV f x :> D  (λh. (f (x + h) - f x) / h) 0 D"
  unfolding field_has_derivative_at has_field_derivative_def has_field_derivative_iff ..

lemma field_derivative_lim_unique:
  assumes f: "(f has_field_derivative df) (at z)"
      and s: "s  0"  "n. s n  0" 
      and a: "(λn. (f (z + s n) - f z) / s n)  a"
    shows "df = a"
proof (rule ccontr)
  assume "df  a"
  obtain q where qpos: "ε. ε > 0  q ε > 0" 
             and q: "ε y. ε > 0; y  z; dist y z < q ε  dist ((f y - f z) / (y - z)) df < ε"
    using f unfolding LIM_def has_field_derivative_iff by metis
  obtain NA where NA: "ε n. ε > 0; n  NA ε  dist ((f (z + s n) - f z) / s n) a < ε" 
    using a unfolding LIMSEQ_def by metis
  obtain NB where NB: "ε n. ε > 0; n  NB ε  norm (s n) < ε" 
    using s unfolding LIMSEQ_def by (metis norm_conv_dist)
  have df: "ε n. ε > 0  0 < ε; norm (s n) < q ε  dist ((f (z + s n) - f z) / s n) df < ε"
    using add_cancel_left_right add_diff_cancel_left' q s
    by (metis add_diff_cancel_right' dist_diff(1))
  define δ where "δ  dist df a / 2"
  with df  a have "δ > 0" and δ: "δ+δ  dist df a"
    by auto
  define N where "N  max (NA δ) (NB (q δ))"
  then have "norm (s N) < q δ"
    by (simp add: NB δ > 0 qpos)
  then have "dist ((f (z + s N) - f z) / s N) df < δ"
    by (simp add: 0 < δ df)
  moreover have "dist ((f (z + s N) - f z) / s N) a < δ"
    using NA N_def 0 < δ by force
  ultimately have "dist df a < dist df a"
    by (smt (verit, ccfv_SIG) δ dist_commute dist_triangle)
  then show False ..
qed

lemma mult_commute_abs: "(λx. x * c) = (*) c"
  for c :: "'a::ab_semigroup_mult"
  by (simp add: fun_eq_iff mult.commute)

lemma DERIV_compose_FDERIV:
  fixes f::"realreal"
  assumes "DERIV f (g x) :> f'"
  assumes "(g has_derivative g') (at x within s)"
  shows "((λx. f (g x)) has_derivative (λx. g' x * f')) (at x within s)"
  using assms has_derivative_compose[of g g' x s f "(*) f'"]
  by (auto simp: has_field_derivative_def ac_simps)


subsection Vector derivative

lemma has_field_derivative_iff_has_vector_derivative:
  "(f has_field_derivative y) F  (f has_vector_derivative y) F"
  unfolding has_vector_derivative_def has_field_derivative_def real_scaleR_def mult_commute_abs ..

lemma has_field_derivative_subset:
  "(f has_field_derivative y) (at x within s)  t  s 
    (f has_field_derivative y) (at x within t)"
  unfolding has_field_derivative_def by (rule has_derivative_subset)

lemma has_vector_derivative_const[simp, derivative_intros]: "((λx. c) has_vector_derivative 0) net"
  by (auto simp: has_vector_derivative_def)

lemma has_vector_derivative_id[simp, derivative_intros]: "((λx. x) has_vector_derivative 1) net"
  by (auto simp: has_vector_derivative_def)

lemma has_vector_derivative_minus[derivative_intros]:
  "(f has_vector_derivative f') net  ((λx. - f x) has_vector_derivative (- f')) net"
  by (auto simp: has_vector_derivative_def)

lemma has_vector_derivative_add[derivative_intros]:
  "(f has_vector_derivative f') net  (g has_vector_derivative g') net 
    ((λx. f x + g x) has_vector_derivative (f' + g')) net"
  by (auto simp: has_vector_derivative_def scaleR_right_distrib)

lemma has_vector_derivative_sum[derivative_intros]:
  "(i. i  I  (f i has_vector_derivative f' i) net) 
    ((λx. iI. f i x) has_vector_derivative (iI. f' i)) net"
  by (auto simp: has_vector_derivative_def fun_eq_iff scaleR_sum_right intro!: derivative_eq_intros)

lemma has_vector_derivative_diff[derivative_intros]:
  "(f has_vector_derivative f') net  (g has_vector_derivative g') net 
    ((λx. f x - g x) has_vector_derivative (f' - g')) net"
  by (auto simp: has_vector_derivative_def scaleR_diff_right)

lemma has_vector_derivative_add_const:
  "((λt. g t + z) has_vector_derivative f') net = ((λt. g t) has_vector_derivative f') net"
  apply (intro iffI)
   apply (force dest: has_vector_derivative_diff [where g = "λt. z", OF _ has_vector_derivative_const])
  apply (force dest: has_vector_derivative_add [OF _ has_vector_derivative_const])
  done

lemma has_vector_derivative_diff_const:
  "((λt. g t - z) has_vector_derivative f') net = ((λt. g t) has_vector_derivative f') net"
  using has_vector_derivative_add_const [where z = "-z"]
  by simp

lemma (in bounded_linear) has_vector_derivative:
  assumes "(g has_vector_derivative g') F"
  shows "((λx. f (g x)) has_vector_derivative f g') F"
  using has_derivative[OF assms[unfolded has_vector_derivative_def]]
  by (simp add: has_vector_derivative_def scaleR)

lemma (in bounded_bilinear) has_vector_derivative:
  assumes "(f has_vector_derivative f') (at x within s)"
    and "(g has_vector_derivative g') (at x within s)"
  shows "((λx. f x ** g x) has_vector_derivative (f x ** g' + f' ** g x)) (at x within s)"
  using FDERIV[OF assms(1-2)[unfolded has_vector_derivative_def]]
  by (simp add: has_vector_derivative_def scaleR_right scaleR_left scaleR_right_distrib)

lemma has_vector_derivative_scaleR[derivative_intros]:
  "(f has_field_derivative f') (at x within s)  (g has_vector_derivative g') (at x within s) 
    ((λx. f x *R g x) has_vector_derivative (f x *R g' + f' *R g x)) (at x within s)"
  unfolding has_field_derivative_iff_has_vector_derivative
  by (rule bounded_bilinear.has_vector_derivative[OF bounded_bilinear_scaleR])

lemma has_vector_derivative_mult[derivative_intros]:
  "(f has_vector_derivative f') (at x within s)  (g has_vector_derivative g') (at x within s) 
    ((λx. f x * g x) has_vector_derivative (f x * g' + f' * g x)) (at x within s)"
  for f g :: "real  'a::real_normed_algebra"
  by (rule bounded_bilinear.has_vector_derivative[OF bounded_bilinear_mult])

lemma has_vector_derivative_of_real[derivative_intros]:
  "(f has_field_derivative D) F  ((λx. of_real (f x)) has_vector_derivative (of_real D)) F"
  by (rule bounded_linear.has_vector_derivative[OF bounded_linear_of_real])
    (simp add: has_field_derivative_iff_has_vector_derivative)

lemma has_vector_derivative_real_field:
  "(f has_field_derivative f') (at (of_real a))  ((λx. f (of_real x)) has_vector_derivative f') (at a within s)"
  using has_derivative_compose[of of_real of_real a _ f "(*) f'"] 
  by (simp add: scaleR_conv_of_real ac_simps has_vector_derivative_def has_field_derivative_def)

lemma has_vector_derivative_continuous:
  "(f has_vector_derivative D) (at x within s)  continuous (at x within s) f"
  by (auto intro: has_derivative_continuous simp: has_vector_derivative_def)

lemma continuous_on_vector_derivative:
  "(x. x  S  (f has_vector_derivative f' x) (at x within S))  continuous_on S f"
  by (auto simp: continuous_on_eq_continuous_within intro!: has_vector_derivative_continuous)

lemma has_vector_derivative_mult_right[derivative_intros]:
  fixes a :: "'a::real_normed_algebra"
  shows "(f has_vector_derivative x) F  ((λx. a * f x) has_vector_derivative (a * x)) F"
  by (rule bounded_linear.has_vector_derivative[OF bounded_linear_mult_right])

lemma has_vector_derivative_mult_left[derivative_intros]:
  fixes a :: "'a::real_normed_algebra"
  shows "(f has_vector_derivative x) F  ((λx. f x * a) has_vector_derivative (x * a)) F"
  by (rule bounded_linear.has_vector_derivative[OF bounded_linear_mult_left])

lemma has_vector_derivative_divide[derivative_intros]:
  fixes a :: "'a::real_normed_field"
  shows "(f has_vector_derivative x) F  ((λx. f x / a) has_vector_derivative (x / a)) F"
  using has_vector_derivative_mult_left [of f x F "inverse a"]
  by (simp add: field_class.field_divide_inverse)


subsection Derivatives

lemma DERIV_D: "DERIV f x :> D  (λh. (f (x + h) - f x) / h) 0 D"
  by (simp add: DERIV_def)

lemma has_field_derivativeD:
  "(f has_field_derivative D) (at x within S) 
    ((λy. (f y - f x) / (y - x))  D) (at x within S)"
  by (simp add: has_field_derivative_iff)

lemma DERIV_const [simp, derivative_intros]: "((λx. k) has_field_derivative 0) F"
  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_const]) auto

lemma DERIV_ident [simp, derivative_intros]: "((λx. x) has_field_derivative 1) F"
  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_ident]) auto

lemma field_differentiable_add[derivative_intros]:
  "(f has_field_derivative f') F  (g has_field_derivative g') F 
    ((λz. f z + g z) has_field_derivative f' + g') F"
  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_add])
     (auto simp: has_field_derivative_def field_simps mult_commute_abs)

corollary DERIV_add:
  "(f has_field_derivative D) (at x within s)  (g has_field_derivative E) (at x within s) 
    ((λx. f x + g x) has_field_derivative D + E) (at x within s)"
  by (rule field_differentiable_add)

lemma field_differentiable_minus[derivative_intros]:
  "(f has_field_derivative f') F  ((λz. - (f z)) has_field_derivative -f') F"
  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_minus])
     (auto simp: has_field_derivative_def field_simps mult_commute_abs)

corollary DERIV_minus:
  "(f has_field_derivative D) (at x within s) 
    ((λx. - f x) has_field_derivative -D) (at x within s)"
  by (rule field_differentiable_minus)

lemma field_differentiable_diff[derivative_intros]:
  "(f has_field_derivative f') F 
    (g has_field_derivative g') F  ((λz. f z - g z) has_field_derivative f' - g') F"
  by (simp only: diff_conv_add_uminus field_differentiable_add field_differentiable_minus)

corollary DERIV_diff:
  "(f has_field_derivative D) (at x within s) 
    (g has_field_derivative E) (at x within s) 
    ((λx. f x - g x) has_field_derivative D - E) (at x within s)"
  by (rule field_differentiable_diff)

lemma DERIV_continuous: "(f has_field_derivative D) (at x within s)  continuous (at x within s) f"
  by (drule has_derivative_continuous[OF has_field_derivative_imp_has_derivative]) simp

corollary DERIV_isCont: "DERIV f x :> D  isCont f x"
  by (rule DERIV_continuous)

lemma DERIV_atLeastAtMost_imp_continuous_on:
  assumes "x. a  x; x  b  y. DERIV f x :> y"
  shows "continuous_on {a..b} f"
  by (meson DERIV_isCont assms atLeastAtMost_iff continuous_at_imp_continuous_at_within continuous_on_eq_continuous_within)

lemma DERIV_continuous_on:
  "(x. x  s  (f has_field_derivative (D x)) (at x within s))  continuous_on s f"
  unfolding continuous_on_eq_continuous_within
  by (intro continuous_at_imp_continuous_on ballI DERIV_continuous)

lemma DERIV_mult':
  "(f has_field_derivative D) (at x within s)  (g has_field_derivative E) (at x within s) 
    ((λx. f x * g x) has_field_derivative f x * E + D * g x) (at x within s)"
  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_mult])
     (auto simp: field_simps mult_commute_abs dest: has_field_derivative_imp_has_derivative)

lemma DERIV_mult[derivative_intros]:
  "(f has_field_derivative Da) (at x within s)  (g has_field_derivative Db) (at x within s) 
    ((λx. f x * g x) has_field_derivative Da * g x + Db * f x) (at x within s)"
  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_mult])
     (auto simp: field_simps dest: has_field_derivative_imp_has_derivative)

text Derivative of linear multiplication

lemma DERIV_cmult:
  "(f has_field_derivative D) (at x within s) 
    ((λx. c * f x) has_field_derivative c * D) (at x within s)"
  by (drule DERIV_mult' [OF DERIV_const]) simp

lemma DERIV_cmult_right:
  "(f has_field_derivative D) (at x within s) 
    ((λx. f x * c) has_field_derivative D * c) (at x within s)"
  using DERIV_cmult by (auto simp add: ac_simps)

lemma DERIV_cmult_Id [simp]: "((*) c has_field_derivative c) (at x within s)"
  using DERIV_ident [THEN DERIV_cmult, where c = c and x = x] by simp

lemma DERIV_cdivide:
  "(f has_field_derivative D) (at x within s) 
    ((λx. f x / c) has_field_derivative D / c) (at x within s)"
  using DERIV_cmult_right[of f D x s "1 / c"] by simp

lemma DERIV_unique: "DERIV f x :> D  DERIV f x :> E  D = E"
  unfolding DERIV_def by (rule LIM_unique)

lemma DERIV_Uniq: "1D. DERIV f x :> D"
  by (simp add: DERIV_unique Uniq_def)

lemma DERIV_sum[derivative_intros]:
  "( n. n  S  ((λx. f x n) has_field_derivative (f' x n)) F) 
    ((λx. sum (f x) S) has_field_derivative sum (f' x) S) F"
  by (rule has_derivative_imp_has_field_derivative [OF has_derivative_sum])
     (auto simp: sum_distrib_left mult_commute_abs dest: has_field_derivative_imp_has_derivative)

lemma DERIV_inverse'[derivative_intros]:
  assumes "(f has_field_derivative D) (at x within s)"
    and "f x  0"
  shows "((λx. inverse (f x)) has_field_derivative - (inverse (f x) * D * inverse (f x)))
    (at x within s)"
proof -
  have "(f has_derivative (λx. x * D)) = (f has_derivative (*) D)"
    by (rule arg_cong [of "λx. x * D"]) (simp add: fun_eq_iff)
  with assms have "(f has_derivative (λx. x * D)) (at x within s)"
    by (auto dest!: has_field_derivative_imp_has_derivative)
  then show ?thesis using f x  0
    by (auto intro: has_derivative_imp_has_field_derivative has_derivative_inverse)
qed

text Power of -1›

lemma DERIV_inverse:
  "x  0  ((λx. inverse(x)) has_field_derivative - (inverse x ^ Suc (Suc 0))) (at x within s)"
  by (drule DERIV_inverse' [OF DERIV_ident]) simp

text Derivative of inverse

lemma DERIV_inverse_fun:
  "(f has_field_derivative d) (at x within s)  f x  0 
    ((λx. inverse (f x)) has_field_derivative (- (d * inverse(f x ^ Suc (Suc 0))))) (at x within s)"
  by (drule (1) DERIV_inverse') (simp add: ac_simps nonzero_inverse_mult_distrib)

text Derivative of quotient

lemma DERIV_divide[derivative_intros]:
  "(f has_field_derivative D) (at x within s) 
    (g has_field_derivative E) (at x within s)  g x  0 
    ((λx. f x / g x) has_field_derivative (D * g x - f x * E) / (g x * g x)) (at x within s)"
  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_divide])
     (auto dest: has_field_derivative_imp_has_derivative simp: field_simps)

lemma DERIV_quotient:
  "(f has_field_derivative d) (at x within s) 
    (g has_field_derivative e) (at x within s) g x  0 
    ((λy. f y / g y) has_field_derivative (d * g x - (e * f x)) / (g x ^ Suc (Suc 0))) (at x within s)"
  by (drule (2) DERIV_divide) (simp add: mult.commute)

lemma DERIV_power_Suc:
  "(f has_field_derivative D) (at x within s) 
    ((λx. f x ^ Suc n) has_field_derivative (1 + of_nat n) * (D * f x ^ n)) (at x within s)"
  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_power])
     (auto simp: has_field_derivative_def)

lemma DERIV_power[derivative_intros]:
  "(f has_field_derivative D) (at x within s) 
    ((λx. f x ^ n) has_field_derivative of_nat n * (D * f x ^ (n - Suc 0))) (at x within s)"
  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_power])
     (auto simp: has_field_derivative_def)

lemma DERIV_pow: "((λx. x ^ n) has_field_derivative real n * (x ^ (n - Suc 0))) (at x within s)"
  using DERIV_power [OF DERIV_ident] by simp

lemma DERIV_power_int [derivative_intros]:
  assumes [derivative_intros]: "(f has_field_derivative d) (at x within s)" and [simp]: "f x  0"
  shows   "((λx. power_int (f x) n) has_field_derivative
             (of_int n * power_int (f x) (n - 1) * d)) (at x within s)"
proof (cases n rule: int_cases4)
  case (nonneg n)
  thus ?thesis 
    by (cases "n = 0")
       (auto intro!: derivative_eq_intros simp: field_simps power_int_diff
             simp flip: power_Suc power_Suc2 power_add)
next
  case (neg n)
  thus ?thesis
    by (auto intro!: derivative_eq_intros simp: field_simps power_int_diff power_int_minus
             simp flip: power_Suc power_Suc2 power_add)
qed

lemma DERIV_chain': "(f has_field_derivative D) (at x within s)  DERIV g (f x) :> E 
  ((λx. g (f x)) has_field_derivative E * D) (at x within s)"
  using has_derivative_compose[of f "(*) D" x s g "(*) E"]
  by (simp only: has_field_derivative_def mult_commute_abs ac_simps)

corollary DERIV_chain2: "DERIV f (g x) :> Da  (g has_field_derivative Db) (at x within s) 
  ((λx. f (g x)) has_field_derivative Da * Db) (at x within s)"
  by (rule DERIV_chain')

text Standard version

lemma DERIV_chain:
  "DERIV f (g x) :> Da  (g has_field_derivative Db) (at x within s) 
    (f  g has_field_derivative Da * Db) (at x within s)"
  by (drule (1) DERIV_chain', simp add: o_def mult.commute)

lemma DERIV_image_chain:
  "(f has_field_derivative Da) (at (g x) within (g ` s)) 
    (g has_field_derivative Db) (at x within s) 
    (f  g has_field_derivative Da * Db) (at x within s)"
  using has_derivative_in_compose [of g "(*) Db" x s f "(*) Da "]
  by (simp add: has_field_derivative_def o_def mult_commute_abs ac_simps)

(*These two are from HOL Light: HAS_COMPLEX_DERIVATIVE_CHAIN*)
lemma DERIV_chain_s:
  assumes "(x. x  s  DERIV g x :> g'(x))"
    and "DERIV f x :> f'"
    and "f x  s"
  shows "DERIV (λx. g(f x)) x :> f' * g'(f x)"
  by (metis (full_types) DERIV_chain' mult.commute assms)

lemma DERIV_chain3: (*HAS_COMPLEX_DERIVATIVE_CHAIN_UNIV*)
  assumes "(x. DERIV g x :> g'(x))"
    and "DERIV f x :> f'"
  shows "DERIV (λx. g(f x)) x :> f' * g'(f x)"
  by (metis UNIV_I DERIV_chain_s [of UNIV] assms)

text Alternative definition for differentiability

lemma DERIV_LIM_iff:
  fixes f :: "'a::{real_normed_vector,inverse}  'a"
  shows "((λh. (f (a + h) - f a) / h) 0 D) = ((λx. (f x - f a) / (x - a)) a D)" (is "?lhs = ?rhs")
proof
  assume ?lhs
  then have "(λx. (f (a + (x + - a)) - f a) / (x + - a)) 0 - - a D"
    by (rule LIM_offset)
  then show ?rhs
    by simp
next
  assume ?rhs
  then have "(λx. (f (x+a) - f a) / ((x+a) - a)) a-a D"
    by (rule LIM_offset)
  then show ?lhs
    by (simp add: add.commute)
qed

lemma has_field_derivative_cong_ev:
  assumes "x = y"
    and *: "eventually (λx. x  S  f x = g x) (nhds x)"
    and "u = v" "S = t" "x  S"
  shows "(f has_field_derivative u) (at x within S) = (g has_field_derivative v) (at y within t)"
  unfolding has_field_derivative_iff
proof (rule filterlim_cong)
  from assms have "f y = g y"
    by (auto simp: eventually_nhds)
  with * show "F z in at x within S. (f z - f x) / (z - x) = (g z - g y) / (z - y)"
    unfolding eventually_at_filter
    by eventually_elim (auto simp: assms f y = g y)
qed (simp_all add: assms)

lemma has_field_derivative_cong_eventually:
  assumes "eventually (λx. f x = g x) (at x within S)" "f x = g x"
  shows "(f has_field_derivative u) (at x within S) = (g has_field_derivative u) (at x within S)"
  unfolding has_field_derivative_iff
proof (rule tendsto_cong)
  show "F y in at x within S. (f y - f x) / (y - x) = (g y - g x) / (y - x)"
    using assms by (auto elim: eventually_mono)
qed

lemma DERIV_cong_ev:
  "x = y  eventually (λx. f x = g x) (nhds x)  u = v 
    DERIV f x :> u  DERIV g y :> v"
  by (rule has_field_derivative_cong_ev) simp_all

lemma DERIV_mirror: "(DERIV f (- x) :> y)  (DERIV (λx. f (- x)) x :> - y)"
  for f :: "real  real" and x y :: real
  by (simp add: DERIV_def filterlim_at_split filterlim_at_left_to_right
      tendsto_minus_cancel_left field_simps conj_commute)

lemma DERIV_shift:
  "(f has_field_derivative y) (at (x + z)) = ((λx. f (x + z)) has_field_derivative y) (at x)"
  by (simp add: DERIV_def field_simps)

lemma DERIV_at_within_shift_lemma:
  assumes "(f has_field_derivative y) (at (z+x) within (+) z ` S)"
  shows "(f  (+)z has_field_derivative y) (at x within S)"
proof -
  have "((+)z has_field_derivative 1) (at x within S)"
    by (rule derivative_eq_intros | simp)+
  with assms DERIV_image_chain show ?thesis
    by (metis mult.right_neutral)
qed

lemma DERIV_at_within_shift:
  "(f has_field_derivative y) (at (z+x) within (+) z ` S)  
   ((λx. f (z+x)) has_field_derivative y) (at x within S)"   (is "?lhs = ?rhs")
proof
  assume ?lhs then show ?rhs
    using DERIV_at_within_shift_lemma unfolding o_def by blast
next
  have [simp]: "(λx. x - z) ` (+) z ` S = S"
    by force
  assume R: ?rhs
  have "(f  (+) z  (+) (- z) has_field_derivative y) (at (z + x) within (+) z ` S)"
    by (rule DERIV_at_within_shift_lemma) (use R in simp add: o_def)
  then show ?lhs
    by (simp add: o_def)
qed

lemma floor_has_real_derivative:
  fixes f :: "real  'a::{floor_ceiling,order_topology}"
  assumes "isCont f x"
    and "f x  "
  shows "((λx. floor (f x)) has_real_derivative 0) (at x)"
proof (subst DERIV_cong_ev[OF refl _ refl])
  show "((λ_. floor (f x)) has_real_derivative 0) (at x)"
    by simp
  have "F y in at x. f y = f x"
    by (rule eventually_floor_eq[OF assms[unfolded continuous_at]])
  then show "F y in nhds x. real_of_int f y = real_of_int f x"
    unfolding eventually_at_filter
    by eventually_elim auto
qed

lemmas has_derivative_floor[derivative_intros] =
  floor_has_real_derivative[THEN DERIV_compose_FDERIV]

lemma continuous_floor:
  fixes x::real
  shows "x    continuous (at x) (real_of_int  floor)"
  using floor_has_real_derivative [where f=id]
  by (auto simp: o_def has_field_derivative_def intro: has_derivative_continuous)

lemma continuous_frac:
  fixes x::real
  assumes "x  "
  shows "continuous (at x) frac"
proof -
  have "isCont (λx. real_of_int x) x"
    using continuous_floor [OF assms] by (simp add: o_def)
  then have *: "continuous (at x) (λx. x - real_of_int x)"
    by (intro continuous_intros)
  moreover have "F x in nhds x. frac x = x - real_of_int x"
    by (simp add: frac_def)
  ultimately show ?thesis
    by (simp add: LIM_imp_LIM frac_def isCont_def)
qed

text Caratheodory formulation of derivative at a point

lemma CARAT_DERIV:
  "(DERIV f x :> l)  (g. (z. f z - f x = g z * (z - x))  isCont g x  g x = l)"
  (is "?lhs = ?rhs")
proof
  assume ?lhs
  show "g. (z. f z - f x = g z * (z - x))  isCont g x  g x = l"
  proof (intro exI conjI)
    let ?g = "(λz. if z = x then l else (f z - f x) / (z-x))"
    show "z. f z - f x = ?g z * (z - x)"
      by simp
    show "isCont ?g x"
      using ?lhs by (simp add: isCont_iff DERIV_def cong: LIM_equal [rule_format])
    show "?g x = l"
      by simp
  qed
next
  assume ?rhs
  then show ?lhs
    by (auto simp add: isCont_iff DERIV_def cong: LIM_cong)
qed


subsection Local extrema

text If term0 < f' x then termx is Locally Strictly Increasing At The Right.

lemma has_real_derivative_pos_inc_right:
  fixes f :: "real  real"
  assumes der: "(f has_real_derivative l) (at x within S)"
    and l: "0 < l"
  shows "d > 0. h > 0. x + h  S  h < d  f x < f (x + h)"
  using assms
proof -
  from der [THEN has_field_derivativeD, THEN tendstoD, OF l, unfolded eventually_at]
  obtain s where s: "0 < s"
    and all: "xa. xaS  xa  x  dist xa x < s  ¦(f xa - f x) / (xa - x) - l¦ < l"
    by (auto simp: dist_real_def)
  then show ?thesis
  proof (intro exI conjI strip)
    show "0 < s" by (rule s)
  next
    fix h :: real
    assume "0 < h" "h < s" "x + h  S"
    with all [of "x + h"] show "f x < f (x+h)"
    proof (simp add: abs_if dist_real_def pos_less_divide_eq split: if_split_asm)
      assume "¬ (f (x + h) - f x) / h < l" and h: "0 < h"
      with l have "0 < (f (x + h) - f x) / h"
        by arith
      then show "f x < f (x + h)"
        by (simp add: pos_less_divide_eq h)
    qed
  qed
qed

lemma DERIV_pos_inc_right:
  fixes f :: "real  real"
  assumes der: "DERIV f x :> l"
    and l: "0 < l"
  shows "d > 0. h > 0. h <