SSL Deriv.thy Interaktion und
PortierbarkeitIsabelle

(*  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 \<open>Differentiation\<close>

theory Deriv
  imports Limits
begin

subsection \<open>Frechet derivative\<close>

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' \
    ((\<lambda>y. ((f y - f (Lim F (\<lambda>x. x))) - f' (y - Lim F (\<lambda>x. x))) /\<^sub>R norm (y - Lim F (\<lambda>x. x))) \<longlongrightarrow> 0) F"

text \<open>
  Usually the filter \<^term>\<open>F\<close> is \<^term>\<open>at x within s\<close>.  \<^term>\<open>(f has_derivative D)
  (at x within s)\<close> means: \<^term>\<open>D\<close> is the derivative of function \<^term>\<open>f\<close> at point \<^term>\<open>x\<close>
  within the set \<^term>\<open>s\<close>. Where \<^term>\<open>s\<close> is used to express left or right sided derivatives. In
  most cases \<^term>\<open>s\<close> is either a variable or \<^term>\<open>UNIV\<close>.
\<close>

text \<open>These are the only cases we'll care about, probably.\<close>

lemma has_derivative_within: "(f has_derivative f') (at x within s) \
    bounded_linear f' \ ((\y. (1 / norm(y - x)) *\<^sub>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 \<open>(has'_field'_derivative)\<close> 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 \<open>has'_vector'_derivative\<close> 50)
  where "(f has_vector_derivative f') net \ (f has_derivative (\x. x *\<^sub>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 \<open>
  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
      (\<^binding>\<open>derivative_eq_intros\<close>,
        fn context =>
          Named_Theorems.get (Context.proof_of context) \<^named_theorems>\<open>derivative_intros\<close>
          |> map_filter eq_rule)
  end
\<close>

text \<open>
  The following syntax is only used as a legacy syntax.
\<close>
abbreviation (input)
  FDERIV :: "('a::real_normed_vector \ 'b::real_normed_vector) \ 'a \ ('a \ 'b) \ bool"
  (\<open>(\<open>notation=\<open>mixfix FDERIV\<close>\<close>FDERIV (_)/ (_)/ :> (_))\<close> [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) F"
  by (metis eq_id_iff has_derivative_ident)

lemma shift_has_derivative_id: "((+) d has_derivative (\x. x)) F"
  using has_derivative_def by fastforce

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)

lemma has_derivative_bot [intro]: "bounded_linear f' \ (f has_derivative f') bot"
  by (auto simp: has_derivative_def)

lemma has_field_derivative_bot [simp, intro]: "(f has_field_derivative f') bot"
  by (auto simp: has_field_derivative_def intro!: has_derivative_bot bounded_linear_mult_right)

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)) /\<^sub>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) \
    ((\<lambda>x. \<Sum>i\<in>I. f i x) has_derivative (\<lambda>x. \<Sum>i\<in>I. 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 \
    ((\<lambda>x. f x - g x) has_derivative (\<lambda>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)) /\<^sub>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 \<and> (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) \<midarrow>0\<rightarrow> 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 \<open>bounded_linear f'\<close>)
  qed
qed

lemma has_derivativeI:
  "bounded_linear f' \
    ((\<lambda>y. ((f y - f x) - f' (y - x)) /\<^sub>R norm (y - x)) \<longlongrightarrow> 0) (at x within s) \<Longrightarrow>
    (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 \<open>Limit transformation for derivatives\<close>

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. x\s \ 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)"
    "(\\<^sub>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 \<open>Continuity\<close>

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 \<open>Composition\<close>

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 \<open>simp_all add: Ng_def Nf_def neq zero_le_divide_iff field_simps\<close>)
    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)) \<longlongrightarrow> 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)) \
  ((\<lambda>x. g (f x)) has_derivative (\<lambda>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)) \
    ((\<lambda>x. \<Prod>i\<in>I. f i x) has_derivative (\<lambda>y. \<Sum>i\<in>I. f' i y * (\<Prod>j\<in>I - {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 * (\i\I. f' i y * (\j\I - {i}. f j x)) + (f' i y) * (\i\I. f i x)"
  have "((\x. f i x * (\i\I. 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 * (\j\insert 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: \<open>y \<noteq> 0\<close> 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
                (\<lambda>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 \<open>Conventional form requires mult-AC laws. Types real and complex only.\<close>

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 \<open>Uniqueness\<close>

text \<open>
This can not generally shown for \<^const>\<open>has_derivative\<close>, as we need to approach the point from
all directions. There is a proof in \<open>Analysis\<close> for \<open>euclidean_space\<close>.
\<close>

lemma has_derivative_at2: "(f has_derivative f') (at x) \
    bounded_linear f' \ ((\y. (1 / (norm(y - x))) *\<^sub>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: "\\<^sub>\\<^sub>1F. (f has_derivative F) (at x)"
  by (simp add: Uniq_def has_derivative_unique)

subsection \<open>Differentiability predicate\<close>

definition differentiable :: "('a::real_normed_vector \ 'b::real_normed_vector) \ 'a filter \ bool"
    (infix \<open>differentiable\<close> 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) \
    (\<lambda>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) \
    (\<lambda>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" "\a\s. (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) \
    (\<lambda>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 \
    (\<lambda>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 \<noteq> 0 \<Longrightarrow> (\<lambda>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 \
           (\<lambda>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) \
    (\<lambda>x. f x *\<^sub>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"
    (\<open>(\<open>notation=\<open>mixfix DERIV\<close>\<close>DERIV (_)/ (_)/ :> (_))\<close> [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 \<open>(has'_real'_derivative)\<close> 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) \
    ((\<lambda>y. (f y - f x) / (y - x)) \<longlongrightarrow> D) (at x within S)"
proof -
  have "((\y. norm (f y - f x - D * (y - x)) / norm (y - x)) \ 0) (at x within S)
      = ((\<lambda>y. (f y - f x) / (y - x) - D) \<longlongrightarrow> 0) (at x within S)"
    by (smt (verit, best) Lim_cong_within divide_diff_eq_iff norm_divide right_minus_eq tendsto_norm_zero_iff)
  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 has_field_derivative_unique:
  assumes "(f has_field_derivative f'1) (at x within A)"
  assumes "(f has_field_derivative f'2) (at x within A)"
  assumes "at x within A \ bot"
  shows   "f'1 = f'2"
  using assms unfolding has_field_derivative_iff using tendsto_unique by blast

text \<open>due to Christian Pardillo Laursen, replacing a proper epsilon-delta horror\<close>
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 -
  have "((\k. (f (z + k) - f z) / k) \ df) (at 0)"
    using f by (simp add: DERIV_def)
  with s have "((\n. (f (z + s n) - f z) / s n) \ df)"
    by (simp flip: LIMSEQ_SEQ_conv)
  then show ?thesis
    using a by (rule LIMSEQ_unique)
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::"real\real"
  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 \<open>Vector derivative\<close>

text \<open>It's for real derivatives only, and not obviously generalisable to field derivatives\<close>
lemma has_real_derivative_iff_has_vector_derivative:
  "(f has_real_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)"
  by (fact DERIV_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 \
    ((\<lambda>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) \
    ((\<lambda>x. \<Sum>i\<in>I. f i x) has_vector_derivative (\<Sum>i\<in>I. 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 \
    ((\<lambda>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) \
    ((\<lambda>x. f x *\<^sub>R g x) has_vector_derivative (f x *\<^sub>R g' + f' *\<^sub>R g x)) (at x within s)"
  unfolding has_real_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) \
    ((\<lambda>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_real_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 \<open>Derivatives\<close>

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) \
    ((\<lambda>y. (f y - f x) / (y - x)) \<longlongrightarrow> 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 \
    ((\<lambda>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) \
    ((\<lambda>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) \
    ((\<lambda>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) \<Longrightarrow>
    ((\<lambda>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) \
    ((\<lambda>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) \
    ((\<lambda>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 \<open>Derivative of linear multiplication\<close>

lemma DERIV_cmult:
  "(f has_field_derivative D) (at x within s) \
    ((\<lambda>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) \
    ((\<lambda>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) \
    ((\<lambda>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: "\\<^sub>\\<^sub>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' n)) F) \
    ((\<lambda>x. sum (f x) S) has_field_derivative sum f' 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 \<open>f x \<noteq> 0\<close>
    by (auto intro: has_derivative_imp_has_field_derivative has_derivative_inverse)
qed

text \<open>Power of \<open>-1\<close>\<close>

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 \<open>Derivative of inverse\<close>

lemma DERIV_inverse_fun:
  "(f has_field_derivative d) (at x within s) \ f x \ 0 \
    ((\<lambda>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 \<open>Derivative of quotient\<close>

lemma DERIV_divide[derivative_intros]:
  "(f has_field_derivative D) (at x within s) \
    (g has_field_derivative E) (at x within s) \<Longrightarrow> g x \<noteq> 0 \<Longrightarrow>
    ((\<lambda>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)\<Longrightarrow> g x \<noteq> 0 \<Longrightarrow>
    ((\<lambda>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) \
    ((\<lambda>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) \
    ((\<lambda>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 "n \ 0 \ 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"; cases "f x = 0")
       (auto intro!: derivative_eq_intros simp: field_simps power_int_diff
                     power_diff power_int_0_left_if)
next
  case (neg n)
  thus ?thesis using assms(2)
    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 \
  ((\<lambda>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) \
  ((\<lambda>x. f (g x)) has_field_derivative Da * Db) (at x within s)"
  by (rule DERIV_chain')

text \<open>Derivative of a finite product\<close>

lemma has_field_derivative_prod:
  assumes "\x. x \ A \ (f x has_field_derivative f' x) (at z)"
  shows   "((\u. \x\A. f x u) has_field_derivative (\x\A. f' x * (\y\A-{x}. f y z))) (at z)"
  using assms
proof (induction A rule: infinite_finite_induct)
  case (insert x A)
  have eq: "insert x A - {y} = insert x (A - {y})" if "y \ A" for y
    using insert.hyps that by auto
  show ?case
    using insert.hyps
    by (auto intro!: derivative_eq_intros insert.prems insert.IH sum.cong
             simp: sum_distrib_left sum_distrib_right eq)
qed auto

lemma has_field_derivative_prod':
  assumes "\x. x \ A \ f x z \ 0"
  assumes "\x. x \ A \ (f x has_field_derivative f' x) (at z)"
  defines "P \ (\A u. \x\A. f x u)"
  shows   "(P A has_field_derivative (P A z * (\x\A. f' x / f x z))) (at z)"
proof (cases "finite A")
  case True
  note [derivative_intros] = has_field_derivative_prod
  show ?thesis using assms True
    by (auto intro!: derivative_eq_intros
             simp: prod_diff1 sum_distrib_left sum_distrib_right mult_ac)
qed (auto simp: P_def)

text \<open>Standard version\<close>

lemma DERIV_chain:
  "DERIV f (g x) :> Da \ (g has_field_derivative Db) (at x within s) \
    (f \<circ> 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) \<Longrightarrow>
    (f \<circ> 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 \<open>Alternative definition for differentiability\<close>

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 "\\<^sub>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 \<open>f y = g y\<close>)
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 "\\<^sub>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 \<longleftrightarrow> 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) \
   ((\<lambda>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 \<open>simp add: o_def\<close>)
  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 "\\<^sub>F y in at x. \f y\ = \f x\"
    by (rule eventually_floor_eq[OF assms[unfolded continuous_at]])
  then show "\\<^sub>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 "\\<^sub>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 \<open>Caratheodory formulation of derivative at a point\<close>

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 \<open>?lhs\<close> 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 \<open>Local extrema\<close>

text \<open>If \<^term>\<open>0 < f' x\<close> then \<^term>\<open>x\<close> is Locally Strictly Increasing At The Right.\<close>

--> --------------------

--> maximum size reached

--> --------------------

quality96%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.25Bemerkung: Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.

SSL Deriv.thy Interaktion und PortierbarkeitIsabelle

Haftungshinweis

Bemerkung:

SSL Deriv.thy Interaktion und
PortierbarkeitIsabelle