Quelle Derivative.thy Sprache: Isabelle

(*  Title:      HOL/Analysis/Derivative.thy
    Author:     John Harrison
    Author:     Robert Himmelmann, TU Muenchen (translation from HOL Light); tidied by LCP
*)

section \<open>Derivative\<close>

theory Derivative
  imports
    Bounded_Linear_Function
    Line_Segment
    Convex_Euclidean_Space
begin

declare bounded_linear_inner_left [intro]

declare has_derivative_bounded_linear[dest]

subsection \<open>Derivatives\<close>

lemma has_derivative_add_const:
  "(f has_derivative f') net \ ((\x. f x + c) has_derivative f') net"
  by (intro derivative_eq_intros) auto

subsection\<^marker>\<open>tag unimportant\<close> \<open>Derivative with composed bilinear function\<close>

text \<open>More explicit epsilon-delta forms.\<close>

proposition has_derivative_within':
  "(f has_derivative f')(at x within s) \
    bounded_linear f' \
    (\<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. 0 < norm (x' - x) \<and> norm (x' - x) < d \<longrightarrow>
      norm (f x' - f x - f'(x' - x)) / norm (x' - x) < e)"
  unfolding has_derivative_within Lim_within dist_norm
  by (simp add: diff_diff_eq)

lemma has_derivative_at':
  "(f has_derivative f') (at x)
   \<longleftrightarrow> bounded_linear f' \<and>
       (\<forall>e>0. \<exists>d>0. \<forall>x'. 0 < norm (x' - x) \<and> norm (x' - x) < d \<longrightarrow>
        norm (f x' - f x - f'(x' - x)) / norm (x' - x) < e)"
  using has_derivative_within' [of f f' x UNIV] by simp

lemma has_derivative_componentwise_within:
   "(f has_derivative f') (at a within S) \
    (\<forall>i \<in> Basis. ((\<lambda>x. f x \<bullet> i) has_derivative (\<lambda>x. f' x \<bullet> i)) (at a within S))"
  apply (simp add: has_derivative_within)
  apply (subst tendsto_componentwise_iff)
  apply (simp add: ball_conj_distrib  inner_diff_left inner_left_distrib flip: bounded_linear_componentwise_iff)
  done

lemma has_derivative_at_withinI:
  "(f has_derivative f') (at x) \ (f has_derivative f') (at x within s)"
  unfolding has_derivative_within' has_derivative_at'
  by blast

lemma has_derivative_right:
  fixes f :: "real \ real"
    and y :: "real"
  shows "(f has_derivative ((*) y)) (at x within ({x <..} \ I)) \
         ((\<lambda>t. (f x - f t) / (x - t)) \<longlongrightarrow> y) (at x within ({x <..} \<inter> I))"
proof -
  have "((\t. (f t - (f x + y * (t - x))) / \t - x\) \ 0) (at x within ({x<..} \ I)) \
    ((\<lambda>t. (f t - f x) / (t - x) - y) \<longlongrightarrow> 0) (at x within ({x<..} \<inter> I))"
    by (intro Lim_cong_within) (auto simp add: diff_divide_distrib add_divide_distrib)
  also have "\ \ ((\t. (f t - f x) / (t - x)) \ y) (at x within ({x<..} \ I))"
    by (simp add: Lim_null[symmetric])
  also have "\ \ ((\t. (f x - f t) / (x - t)) \ y) (at x within ({x<..} \ I))"
    by (intro Lim_cong_within) (simp_all add: field_simps)
  finally show ?thesis
    by (simp add: bounded_linear_mult_right has_derivative_within)
qed

subsubsection \<open>Caratheodory characterization\<close>

lemma DERIV_caratheodory_within:
  "(f has_field_derivative l) (at x within S) \
   (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> continuous (at x within S) g \<and> g x = l)"
      (is "?lhs = ?rhs")
proof
  assume ?lhs
  show ?rhs
  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 "continuous (at x within S) ?g" using \<open>?lhs\<close>
      by (auto simp add: continuous_within has_field_derivative_iff cong: Lim_cong_within)
    show "?g x = l" by simp
  qed
next
  assume ?rhs
  then obtain g where
    "(\z. f z - f x = g z * (z-x))" and "continuous (at x within S) g" and "g x = l" by blast
  thus ?lhs
    by (auto simp add: continuous_within has_field_derivative_iff cong: Lim_cong_within)
qed

subsection \<open>Differentiability\<close>

definition\<^marker>\<open>tag important\<close>
  differentiable_on :: "('a::real_normed_vector \ 'b::real_normed_vector) \ 'a set \ bool"
    (infix \<open>differentiable'_on\<close> 50)
  where "f differentiable_on s \ (\x\s. f differentiable (at x within s))"

lemma differentiableI: "(f has_derivative f') net \ f differentiable net"
  unfolding differentiable_def
  by auto

lemma differentiable_onD: "\f differentiable_on S; x \ S\ \ f differentiable (at x within S)"
  using differentiable_on_def by blast

lemma differentiable_at_withinI: "f differentiable (at x) \ f differentiable (at x within s)"
  unfolding differentiable_def
  using has_derivative_at_withinI
  by blast

lemma differentiable_at_imp_differentiable_on:
  "(\x. x \ s \ f differentiable at x) \ f differentiable_on s"
  by (metis differentiable_at_withinI differentiable_on_def)

corollary\<^marker>\<open>tag unimportant\<close> differentiable_iff_scaleR:
  fixes f :: "real \ 'a::real_normed_vector"
  shows "f differentiable F \ (\d. (f has_derivative (\x. x *\<^sub>R d)) F)"
  by (auto simp: differentiable_def dest: has_derivative_linear linear_imp_scaleR)

lemma differentiable_on_eq_differentiable_at:
  "open s \ f differentiable_on s \ (\x\s. f differentiable at x)"
  unfolding differentiable_on_def
  by (metis at_within_interior interior_open)

lemma differentiable_transform_within:
  assumes "f differentiable (at x within s)"
    and "0 < d"
    and "x \ s"
    and "\x'. \x'\s; dist x' x < d\ \ f x' = g x'"
  shows "g differentiable (at x within s)"
   using assms has_derivative_transform_within unfolding differentiable_def
   by blast

lemma differentiable_on_ident [simp, derivative_intros]: "(\x. x) differentiable_on S"
  by (simp add: differentiable_at_imp_differentiable_on)

lemma differentiable_on_id [simp, derivative_intros]: "id differentiable_on S"
  by (simp add: id_def)

lemma differentiable_on_const [simp, derivative_intros]: "(\z. c) differentiable_on S"
  by (simp add: differentiable_on_def)

lemma differentiable_on_mult [simp, derivative_intros]:
  fixes f :: "'M::real_normed_vector \ 'a::real_normed_algebra"
  shows "\f differentiable_on S; g differentiable_on S\ \ (\z. f z * g z) differentiable_on S"
  unfolding differentiable_on_def differentiable_def
  using differentiable_def differentiable_mult by blast

lemma differentiable_on_compose:
   "\g differentiable_on S; f differentiable_on (g ` S)\ \ (\x. f (g x)) differentiable_on S"
by (simp add: differentiable_in_compose differentiable_on_def)

lemma bounded_linear_imp_differentiable_on: "bounded_linear f \ f differentiable_on S"
  by (simp add: differentiable_on_def bounded_linear_imp_differentiable)

lemma linear_imp_differentiable_on:
  fixes f :: "'a::euclidean_space \ 'b::real_normed_vector"
  shows "linear f \ f differentiable_on S"
  by (simp add: differentiable_on_def linear_imp_differentiable)

lemma differentiable_on_minus [simp, derivative_intros]:
  "f differentiable_on S \ (\z. -(f z)) differentiable_on S"
  by (simp add: differentiable_on_def)

lemma differentiable_on_add [simp, derivative_intros]:
  "\f differentiable_on S; g differentiable_on S\ \ (\z. f z + g z) differentiable_on S"
  by (simp add: differentiable_on_def)

lemma differentiable_on_diff [simp, derivative_intros]:
  "\f differentiable_on S; g differentiable_on S\ \ (\z. f z - g z) differentiable_on S"
  by (simp add: differentiable_on_def)

lemma differentiable_on_inverse [simp, derivative_intros]:
  fixes f :: "'a :: real_normed_vector \ 'b :: real_normed_field"
  shows "f differentiable_on S \ (\x. x \ S \ f x \ 0) \ (\x. inverse (f x)) differentiable_on S"
  by (simp add: differentiable_on_def)

lemma differentiable_on_scaleR [derivative_intros, simp]:
  "\f differentiable_on S; g differentiable_on S\ \ (\x. f x *\<^sub>R g x) differentiable_on S"
  unfolding differentiable_on_def
  by (blast intro: differentiable_scaleR)

lemma has_derivative_sqnorm_at [derivative_intros, simp]:
  "((\x. (norm x)\<^sup>2) has_derivative (\x. 2 *\<^sub>R (a \ x))) (at a)"
  using bounded_bilinear.FDERIV  [of "(\)" id id a _ id id]
  by (auto simp: inner_commute dot_square_norm bounded_bilinear_inner)

lemma differentiable_sqnorm_at [derivative_intros, simp]:
  fixes a :: "'a :: {real_normed_vector,real_inner}"
  shows "(\x. (norm x)\<^sup>2) differentiable (at a)"
  by (force simp add: differentiable_def intro: has_derivative_sqnorm_at)

lemma differentiable_on_sqnorm [derivative_intros, simp]:
  fixes S :: "'a :: {real_normed_vector,real_inner} set"
  shows "(\x. (norm x)\<^sup>2) differentiable_on S"
  by (simp add: differentiable_at_imp_differentiable_on)

lemma differentiable_norm_at [derivative_intros, simp]:
  fixes a :: "'a :: {real_normed_vector,real_inner}"
  shows "a \ 0 \ norm differentiable (at a)"
  using differentiableI has_derivative_norm by blast

lemma differentiable_on_norm [derivative_intros, simp]:
  fixes S :: "'a :: {real_normed_vector,real_inner} set"
  shows "0 \ S \ norm differentiable_on S"
  by (metis differentiable_at_imp_differentiable_on differentiable_norm_at)

subsection \<open>Frechet derivative and Jacobian matrix\<close>

definition "frechet_derivative f net = (SOME f'. (f has_derivative f') net)"

proposition frechet_derivative_works:
  "f differentiable net \ (f has_derivative (frechet_derivative f net)) net"
  unfolding frechet_derivative_def differentiable_def
  unfolding some_eq_ex[of "\ f' . (f has_derivative f') net"] ..

lemma linear_frechet_derivative: "f differentiable net \ linear (frechet_derivative f net)"
  unfolding frechet_derivative_works has_derivative_def
  by (auto intro: bounded_linear.linear)

lemma frechet_derivative_const [simp]: "frechet_derivative (\x. c) (at a) = (\x. 0)"
  using differentiable_const frechet_derivative_works has_derivative_const has_derivative_unique by blast

lemma frechet_derivative_id [simp]: "frechet_derivative id (at a) = id"
  using differentiable_def frechet_derivative_works has_derivative_id has_derivative_unique by blast

lemma frechet_derivative_ident [simp]: "frechet_derivative (\x. x) (at a) = (\x. x)"
  by (metis eq_id_iff frechet_derivative_id)

subsection \<open>Differentiability implies continuity\<close>

proposition differentiable_imp_continuous_within:
  "f differentiable (at x within s) \ continuous (at x within s) f"
  by (auto simp: differentiable_def intro: has_derivative_continuous)

lemma differentiable_imp_continuous_on:
  "f differentiable_on s \ continuous_on s f"
  unfolding differentiable_on_def continuous_on_eq_continuous_within
  using differentiable_imp_continuous_within by blast

lemma differentiable_on_subset:
  "f differentiable_on t \ s \ t \ f differentiable_on s"
  unfolding differentiable_on_def
  using differentiable_within_subset
  by blast

lemma differentiable_on_empty: "f differentiable_on {}"
  unfolding differentiable_on_def
  by auto

lemma has_derivative_continuous_on:
  "(\x. x \ s \ (f has_derivative f' x) (at x within s)) \ continuous_on s f"
  by (auto intro!: differentiable_imp_continuous_on differentiableI simp: differentiable_on_def)

text \<open>Results about neighborhoods filter.\<close>

lemma eventually_nhds_metric_le:
  "eventually P (nhds a) = (\d>0. \x. dist x a \ d \ P x)"
  unfolding eventually_nhds_metric by (safe, rule_tac x="d / 2" in exI, auto)

lemma le_nhds: "F \ nhds a \ (\S. open S \ a \ S \ eventually (\x. x \ S) F)"
  unfolding le_filter_def eventually_nhds by (fast elim: eventually_mono)

lemma le_nhds_metric: "F \ nhds a \ (\e>0. eventually (\x. dist x a < e) F)"
  unfolding le_filter_def eventually_nhds_metric by (fast elim: eventually_mono)

lemma le_nhds_metric_le: "F \ nhds a \ (\e>0. eventually (\x. dist x a \ e) F)"
  unfolding le_filter_def eventually_nhds_metric_le by (fast elim: eventually_mono)

text \<open>Several results are easier using a "multiplied-out" variant.
(I got this idea from Dieudonne's proof of the chain rule).\

lemma has_derivative_within_alt:
  "(f has_derivative f') (at x within s) \ bounded_linear f' \
    (\<forall>e>0. \<exists>d>0. \<forall>y\<in>s. norm(y - x) < d \<longrightarrow> norm (f y - f x - f' (y - x)) \<le> e * norm (y - x))"
  unfolding has_derivative_within filterlim_def le_nhds_metric_le eventually_filtermap
    eventually_at dist_norm diff_diff_eq
  by (force simp add: linear_0 bounded_linear.linear pos_divide_le_eq)

lemma has_derivative_within_alt2:
  "(f has_derivative f') (at x within s) \ bounded_linear f' \
    (\<forall>e>0. eventually (\<lambda>y. norm (f y - f x - f' (y - x)) \<le> e * norm (y - x)) (at x within s))"
  unfolding has_derivative_within filterlim_def le_nhds_metric_le eventually_filtermap
    eventually_at dist_norm diff_diff_eq
  by (force simp add: linear_0 bounded_linear.linear pos_divide_le_eq)

lemma has_derivative_at_alt:
  "(f has_derivative f') (at x) \
    bounded_linear f' \
    (\<forall>e>0. \<exists>d>0. \<forall>y. norm(y - x) < d \<longrightarrow> norm (f y - f x - f'(y - x)) \<le> e * norm (y - x))"
  using has_derivative_within_alt[where s=UNIV]
  by simp

subsection \<open>The chain rule\<close>

proposition diff_chain_within[derivative_intros]:
  assumes "(f has_derivative f') (at x within s)"
    and "(g has_derivative g') (at (f x) within (f ` s))"
  shows "((g \ f) has_derivative (g' \ f'))(at x within s)"
  using has_derivative_in_compose[OF assms]
  by (simp add: comp_def)

lemma diff_chain_at[derivative_intros]:
  "(f has_derivative f') (at x) \
    (g has_derivative g') (at (f x)) \ ((g \ f) has_derivative (g' \ f')) (at x)"
  by (meson diff_chain_within has_derivative_at_withinI)

lemma has_vector_derivative_shift: "(f has_vector_derivative D x) (at x)
           \<Longrightarrow> ((+) d \<circ> f has_vector_derivative D x) (at x)"
  using diff_chain_at [OF _ shift_has_derivative_id]
  by (simp add: has_derivative_iff_Ex has_vector_derivative_def)

lemma has_vector_derivative_within_open:
  "a \ S \ open S \
    (f has_vector_derivative f') (at a within S) \ (f has_vector_derivative f') (at a)"
  by (simp only: at_within_interior interior_open)

lemma field_vector_diff_chain_within:
assumes Df: "(f has_vector_derivative f') (at x within S)"
     and Dg: "(g has_field_derivative g') (at (f x) within f ` S)"
shows "((g \ f) has_vector_derivative (f' * g')) (at x within S)"
using diff_chain_within[OF Df[unfolded has_vector_derivative_def]
                       Dg [unfolded has_field_derivative_def]]
by (auto simp: o_def mult.commute has_vector_derivative_def)

lemma vector_derivative_diff_chain_within:
  assumes Df: "(f has_vector_derivative f') (at x within S)"
     and Dg: "(g has_derivative g') (at (f x) within f`S)"
  shows "((g \ f) has_vector_derivative (g' f')) (at x within S)"
using diff_chain_within[OF Df[unfolded has_vector_derivative_def] Dg]
  linear.scaleR[OF has_derivative_linear[OF Dg]]
  unfolding has_vector_derivative_def o_def
  by (auto simp: o_def mult.commute has_vector_derivative_def)

subsection\<^marker>\<open>tag unimportant\<close> \<open>Composition rules stated just for differentiability\<close>

lemma differentiable_chain_at:
  "f differentiable (at x) \
    g differentiable (at (f x)) \<Longrightarrow> (g \<circ> f) differentiable (at x)"
  unfolding differentiable_def
  by (meson diff_chain_at)

lemma differentiable_chain_within:
  "f differentiable (at x within S) \
    g differentiable (at(f x) within (f ` S)) \<Longrightarrow> (g \<circ> f) differentiable (at x within S)"
  unfolding differentiable_def
  by (meson diff_chain_within)

subsection \<open>Uniqueness of derivative\<close>

text\<^marker>\<open>tag important\<close> \<open>
The general result is a bit messy because we need approachability of the
limit point from any direction. But OK for nontrivial intervals etc.
\<close>

proposition frechet_derivative_unique_within:
  fixes f :: "'a::euclidean_space \ 'b::real_normed_vector"
  assumes 1: "(f has_derivative f') (at x within S)"
    and 2: "(f has_derivative f'') (at x within S)"
    and S: "\i e. \i\Basis; e>0\ \ \d. 0 < \d\ \ \d\ < e \ (x + d *\<^sub>R i) \ S"
  shows "f' = f''"
proof -
  note as = assms(1,2)[unfolded has_derivative_def]
  then interpret f': bounded_linear f' by auto
  from as interpret f'': bounded_linear f'' by auto
  have "x islimpt S" unfolding islimpt_approachable
  proof (intro allI impI)
    fix e :: real
    assume "e > 0"
    obtain d where "0 < \d\" and "\d\ < e" and "x + d *\<^sub>R (SOME i. i \ Basis) \ S"
      using assms(3) SOME_Basis \<open>e>0\<close> by blast
    then show "\x'\S. x' \ x \ dist x' x < e"
      by (rule_tac x="x + d *\<^sub>R (SOME i. i \ Basis)" in bexI) (auto simp: dist_norm SOME_Basis nonzero_Basis) qed
  then have *: "netlimit (at x within S) = x"
    by (simp add: Lim_ident_at trivial_limit_within)
  show ?thesis
  proof (rule linear_eq_stdbasis)
    show "linear f'" "linear f''"
      unfolding linear_conv_bounded_linear using as by auto
  next
    fix i :: 'a
    assume i: "i \ Basis"
    define e where "e = norm (f' i - f'' i)"
    show "f' i = f'' i"
    proof (rule ccontr)
      assume "f' i \ f'' i"
      then have "e > 0"
        unfolding e_def by auto
      obtain d where d:
        "0 < d"
        "(\y. y\S \ 0 < dist y x \ dist y x < d \
          dist ((f y - f x - f' (y - x)) /\<^sub>R norm (y - x) -
              (f y - f x - f'' (y - x)) /\<^sub>R norm (y - x)) (0 - 0) < e)"
        using tendsto_diff [OF as(1,2)[THEN conjunct2]]
        unfolding * Lim_within
        using \<open>e>0\<close> by blast
      obtain c where c: "0 < \c\" "\c\ < d \ x + c *\<^sub>R i \ S"
        using assms(3) i d(1) by blast
      have *: "norm (- ((1 / \c\) *\<^sub>R f' (c *\<^sub>R i)) + (1 / \c\) *\<^sub>R f'' (c *\<^sub>R i)) =
        norm ((1 / \<bar>c\<bar>) *\<^sub>R (- (f' (c *\<^sub>R i)) + f'' (c *\<^sub>R i)))"
        unfolding scaleR_right_distrib by auto
      also have "\ = norm ((1 / \c\) *\<^sub>R (c *\<^sub>R (- (f' i) + f'' i)))"
        unfolding f'.scaleR f''.scaleR
        unfolding scaleR_right_distrib scaleR_minus_right
        by auto
      also have "\ = e"
        unfolding e_def
        using c(1)
        using norm_minus_cancel[of "f' i - f'' i"]
        by auto
      finally show False
        using c
        using d(2)[of "x + c *\<^sub>R i"]
        unfolding dist_norm
        unfolding f'.scaleR f''.scaleR f'.add f''.add f'.diff f''.diff
          scaleR_scaleR scaleR_right_diff_distrib scaleR_right_distrib
        using i
        by (auto simp: inverse_eq_divide)
    qed
  qed
qed

proposition frechet_derivative_unique_within_closed_interval:
  fixes f::"'a::euclidean_space \ 'b::real_normed_vector"
  assumes ab: "\i. i\Basis \ a\i < b\i"
    and x: "x \ cbox a b"
    and "(f has_derivative f' ) (at x within cbox a b)"
    and "(f has_derivative f'') (at x within cbox a b)"
  shows "f' = f''"
proof (rule frechet_derivative_unique_within)
  fix e :: real
  fix i :: 'a
  assume "e > 0" and i: "i \ Basis"
  then show "\d. 0 < \d\ \ \d\ < e \ x + d *\<^sub>R i \ cbox a b"
  proof (cases "x\i = a\i")
    case True
    with ab[of i] \<open>e>0\<close> x i show ?thesis
      by (rule_tac x="(min (b\i - a\i) e) / 2" in exI)
         (auto simp add: mem_box field_simps inner_simps inner_Basis)
  next
    case False
    moreover have "a \ i < x \ i"
      using False i mem_box(2) x by force
    moreover {
      have "a \ i * 2 + min (x \ i - a \ i) e \ a\i *2 + x\i - a\i"
        by auto
      also have "\ = a\i + x\i"
        by auto
      also have "\ \ 2 * (x\i)"
        using \<open>a \<bullet> i < x \<bullet> i\<close> by auto
      finally have "a \ i * 2 + min (x \ i - a \ i) e \ x \ i * 2"
        by auto
    }
    moreover have "min (x \ i - a \ i) e \ 0"
      by (simp add: \<open>0 < e\<close> \<open>a \<bullet> i < x \<bullet> i\<close> less_eq_real_def)
    then have "x \ i * 2 \ b \ i * 2 + min (x \ i - a \ i) e"
      using i mem_box(2) x by force
    ultimately show ?thesis
    using ab[of i] \<open>e>0\<close> x i
      by (rule_tac x="- (min (x\i - a\i) e) / 2" in exI)
         (auto simp add: mem_box field_simps inner_simps inner_Basis)
  qed
qed (use assms in auto)

lemma frechet_derivative_unique_within_open_interval:
  fixes f::"'a::euclidean_space \ 'b::real_normed_vector"
  assumes x: "x \ box a b"
    and f: "(f has_derivative f' ) (at x within box a b)" "(f has_derivative f'') (at x within box a b)"
  shows "f' = f''"
  by (metis at_within_open assms has_derivative_unique open_box)

lemma frechet_derivative_at:
  "(f has_derivative f') (at x) \ f' = frechet_derivative f (at x)"
  using differentiable_def frechet_derivative_works has_derivative_unique by blast

lemma frechet_derivative_compose:
  "frechet_derivative (f o g) (at x) = frechet_derivative (f) (at (g x)) o frechet_derivative g (at x)"
  if "g differentiable at x" "f differentiable at (g x)"
  by (metis diff_chain_at frechet_derivative_at frechet_derivative_works that)

lemma frechet_derivative_within_cbox:
  fixes f :: "'a::euclidean_space \ 'b::real_normed_vector"
  assumes "\i. i\Basis \ a\i < b\i"
    and "x \ cbox a b"
    and "(f has_derivative f') (at x within cbox a b)"
  shows "frechet_derivative f (at x within cbox a b) = f'"
  using assms
  by (metis Derivative.differentiableI frechet_derivative_unique_within_closed_interval frechet_derivative_works)

lemma frechet_derivative_transform_within_open:
  "frechet_derivative f (at x) = frechet_derivative g (at x)"
  if "f differentiable at x" "open X" "x \ X" "\x. x \ X \ f x = g x"
  by (meson frechet_derivative_at frechet_derivative_works has_derivative_transform_within_open that)

subsection \<open>Derivatives of local minima and maxima are zero\<close>

lemma has_derivative_local_min:
  fixes f :: "'a::real_normed_vector \ real"
  assumes deriv: "(f has_derivative f') (at x)"
  assumes min: "eventually (\y. f x \ f y) (at x)"
  shows "f' = (\h. 0)"
proof
  fix h :: 'a
  interpret f': bounded_linear f'
    using deriv by (rule has_derivative_bounded_linear)
  show "f' h = 0"
  proof (cases "h = 0")
    case False
    from min obtain d where d1: "0 < d" and d2: "\y\ball x d. f x \ f y"
      unfolding eventually_at by (force simp: dist_commute)
    have "FDERIV (\r. x + r *\<^sub>R h) 0 :> (\r. r *\<^sub>R h)"
      by (intro derivative_eq_intros) auto
    then have "FDERIV (\r. f (x + r *\<^sub>R h)) 0 :> (\k. f' (k *\<^sub>R h))"
      by (rule has_derivative_compose, simp add: deriv)
    then have "DERIV (\r. f (x + r *\<^sub>R h)) 0 :> f' h"
      unfolding has_field_derivative_def by (simp add: f'.scaleR mult_commute_abs)
    moreover have "0 < d / norm h" using d1 and \<open>h \<noteq> 0\<close> by simp
    moreover have "\y. \0 - y\ < d / norm h \ f (x + 0 *\<^sub>R h) \ f (x + y *\<^sub>R h)"
      using \<open>h \<noteq> 0\<close> by (auto simp add: d2 dist_norm pos_less_divide_eq)
    ultimately show "f' h = 0"
      by (rule DERIV_local_min)
  qed simp
qed

lemma has_derivative_local_max:
  fixes f :: "'a::real_normed_vector \ real"
  assumes "(f has_derivative f') (at x)"
  assumes "eventually (\y. f y \ f x) (at x)"
  shows "f' = (\h. 0)"
  using has_derivative_local_min [of "\x. - f x" "\h. - f' h" "x"]
  using assms unfolding fun_eq_iff by simp

lemma differential_zero_maxmin:
  fixes f::"'a::real_normed_vector \ real"
  assumes "x \ S"
    and "open S"
    and deriv: "(f has_derivative f') (at x)"
    and mono: "(\y\S. f y \ f x) \ (\y\S. f x \ f y)"
  shows "f' = (\v. 0)"
  using mono
proof
  assume "\y\S. f y \ f x"
  with \<open>x \<in> S\<close> and \<open>open S\<close> have "eventually (\<lambda>y. f y \<le> f x) (at x)"
    unfolding eventually_at_topological by auto
  with deriv show ?thesis
    by (rule has_derivative_local_max)
next
  assume "\y\S. f x \ f y"
  with \<open>x \<in> S\<close> and \<open>open S\<close> have "eventually (\<lambda>y. f x \<le> f y) (at x)"
    unfolding eventually_at_topological by auto
  with deriv show ?thesis
    by (rule has_derivative_local_min)
qed

lemma differential_zero_maxmin_component:
  fixes f :: "'a::euclidean_space \ 'b::euclidean_space"
  assumes k: "k \ Basis"
    and ball: "0 < e" "(\y \ ball x e. (f y)\k \ (f x)\k) \ (\y\ball x e. (f x)\k \ (f y)\k)"
    and diff: "f differentiable (at x)"
  shows "(\j\Basis. (frechet_derivative f (at x) j \ k) *\<^sub>R j) = (0::'a)" (is "?D k = 0")
proof -
  let ?f' = "frechet_derivative f (at x)"
  have "x \ ball x e" using \0 < e\ by simp
  moreover have "open (ball x e)" by simp
  moreover have "((\x. f x \ k) has_derivative (\h. ?f' h \ k)) (at x)"
    using bounded_linear_inner_left diff[unfolded frechet_derivative_works]
    by (rule bounded_linear.has_derivative)
  ultimately have "(\h. frechet_derivative f (at x) h \ k) = (\v. 0)"
    using ball(2) by (rule differential_zero_maxmin)
  then show ?thesis
    unfolding fun_eq_iff by simp
qed

subsection \<open>One-dimensional mean value theorem\<close>

lemma mvt_simple:
  fixes f :: "real \ real"
  assumes "a < b"
    and derf: "\x. \a \ x; x \ b\ \ (f has_derivative f' x) (at x within {a..b})"
  shows "\x\{a<..
proof (rule mvt)
  have "f differentiable_on {a..b}"
    using derf unfolding differentiable_on_def differentiable_def by force
  then show "continuous_on {a..b} f"
    by (rule differentiable_imp_continuous_on)
  show "(f has_derivative f' x) (at x)" if "a < x" "x < b" for x
    by (metis at_within_Icc_at derf leI order.asym that)
qed (use assms in auto)

lemma mvt_very_simple:
  fixes f :: "real \ real"
  assumes "a \ b"
    and derf: "\x. \a \ x; x \ b\ \ (f has_derivative f' x) (at x within {a..b})"
  shows "\x\{a..b}. f b - f a = f' x (b - a)"
proof (cases "a = b")
  interpret bounded_linear "f' b"
    using assms by auto
  case True
  then show ?thesis
    by force
next
  case False
  then show ?thesis
    using mvt_simple[OF _ derf]
    by (metis \<open>a \<le> b\<close> atLeastAtMost_iff dual_order.order_iff_strict greaterThanLessThan_iff)
qed

text \<open>A nice generalization (see Havin's proof of 5.19 from Rudin's book).\<close>

lemma mvt_general:
  fixes f :: "real \ 'a::real_inner"
  assumes "a < b"
    and contf: "continuous_on {a..b} f"
    and derf: "\x. \a < x; x < b\ \ (f has_derivative f' x) (at x)"
  shows "\x\{a<.. norm (f' x (b - a))"
proof -
  have "\x\{a<.. f b - (f b - f a) \ f a = (f b - f a) \ f' x (b - a)"
    apply (rule mvt [OF \<open>a < b\<close>, where f = "\<lambda>x. (f b - f a) \<bullet> f x"])
    apply (intro continuous_intros contf)
    using derf apply (auto intro: has_derivative_inner_right)
    done
  then obtain x where x: "x \ {a<..
    "(f b - f a) \ f b - (f b - f a) \ f a = (f b - f a) \ f' x (b - a)" ..
  show ?thesis
  proof (cases "f a = f b")
    case False
    have "norm (f b - f a) * norm (f b - f a) = (norm (f b - f a))\<^sup>2"
      by (simp add: power2_eq_square)
    also have "\ = (f b - f a) \ (f b - f a)"
      unfolding power2_norm_eq_inner ..
    also have "\ = (f b - f a) \ f' x (b - a)"
      using x(2) by (simp only: inner_diff_right)
    also have "\ \ norm (f b - f a) * norm (f' x (b - a))"
      by (rule norm_cauchy_schwarz)
    finally show ?thesis
      using False x(1)
      by (auto simp add: mult_left_cancel)
  next
    case True
    then show ?thesis
      using \<open>a < b\<close> by (rule_tac x="(a + b) /2" in bexI) auto
  qed
qed

subsection \<open>More general bound theorems\<close>

proposition differentiable_bound_general:
  fixes f :: "real \ 'a::real_normed_vector"
  assumes "a < b"
    and f_cont: "continuous_on {a..b} f"
    and phi_cont: "continuous_on {a..b} \"
    and f': "\x. a < x \ x < b \ (f has_vector_derivative f' x) (at x)"
    and phi': "\x. a < x \ x < b \ (\ has_vector_derivative \' x) (at x)"
    and bnd: "\x. a < x \ x < b \ norm (f' x) \ \' x"
  shows "norm (f b - f a) \ \ b - \ a"
proof -
  {
    fix x assume x: "a < x" "x < b"
    have "0 \ norm (f' x)" by simp
    also have "\ \ \' x" using x by (auto intro!: bnd)
    finally have "0 \ \' x" .
  } note phi'_nonneg = this
  note f_tendsto = assms(2)[simplified continuous_on_def, rule_format]
  note phi_tendsto = assms(3)[simplified continuous_on_def, rule_format]
  {
    fix e::real assume "e > 0"
    define e2 where "e2 = e / 2"
    with \<open>e > 0\<close> have "e2 > 0" by simp
    let ?le = "\x1. norm (f x1 - f a) \ \ x1 - \ a + e * (x1 - a) + e"
    define A where "A = {x2. a \ x2 \ x2 \ b \ (\x1\{a ..< x2}. ?le x1)}"
    have A_subset: "A \ {a..b}" by (auto simp: A_def)
    {
      fix x2
      assume a: "a \ x2" "x2 \ b" and le: "\x1\{a..
      have "?le x2" using \<open>e > 0\<close>
      proof cases
        assume "x2 \ a" with a have "a < x2" by simp
        have "at x2 within {a <.. bot"
          using \<open>a < x2\<close>
          by (auto simp: trivial_limit_within islimpt_in_closure)
        moreover
        have "((\x1. (\ x1 - \ a) + e * (x1 - a) + e) \ (\ x2 - \ a) + e * (x2 - a) + e) (at x2 within {a <..
          "((\x1. norm (f x1 - f a)) \ norm (f x2 - f a)) (at x2 within {a <..
          using a
          by (auto intro!: tendsto_eq_intros f_tendsto phi_tendsto
            intro: tendsto_within_subset[where S="{a..b}"])
        moreover
        have "eventually (\x. x > a) (at x2 within {a <..
          by (auto simp: eventually_at_filter)
        hence "eventually ?le (at x2 within {a <..
          unfolding eventually_at_filter
          by eventually_elim (insert le, auto)
        ultimately
        show ?thesis
          by (rule tendsto_le)
      qed simp
    } note le_cont = this
    have "a \ A"
      using assms by (auto simp: A_def)
    hence [simp]: "A \ {}" by auto
    have A_ivl: "\x1 x2. x2 \ A \ x1 \ {a ..x2} \ x1 \ A"
      by (simp add: A_def)
    have [simp]: "bdd_above A" by (auto simp: A_def)
    define y where "y = Sup A"
    have "y \ b"
      unfolding y_def
      by (simp add: cSup_le_iff) (simp add: A_def)
     have leI: "\x x1. a \ x1 \ x \ A \ x1 < x \ ?le x1"
       by (auto simp: A_def intro!: le_cont)
    have y_all_le: "\x1\{a..
      by (auto simp: y_def less_cSup_iff leI)
    have "a \ y"
      by (metis \<open>a \<in> A\<close> \<open>bdd_above A\<close> cSup_upper y_def)
    have "y \ A"
      using y_all_le \<open>a \<le> y\<close> \<open>y \<le> b\<close>
      by (auto simp: A_def)
    hence "A = {a .. y}"
      using A_subset by (auto simp: subset_iff y_def cSup_upper intro: A_ivl)
    from le_cont[OF \<open>a \<le> y\<close> \<open>y \<le> b\<close> y_all_le] have le_y: "?le y" .
    have "y = b"
    proof (cases "a = y")
      case True
      with \<open>a < b\<close> have "y < b" by simp
      with \<open>a = y\<close> f_cont phi_cont \<open>e2 > 0\<close>
      have 1: "\\<^sub>F x in at y within {y..b}. dist (f x) (f y) < e2"
       and 2: "\\<^sub>F x in at y within {y..b}. dist (\ x) (\ y) < e2"
        by (auto simp: continuous_on_def tendsto_iff)
      have 3: "eventually (\x. y < x) (at y within {y..b})"
        by (auto simp: eventually_at_filter)
      have 4: "eventually (\x::real. x < b) (at y within {y..b})"
        using _ \<open>y < b\<close>
        by (rule order_tendstoD) (auto intro!: tendsto_eq_intros)
      from 1 2 3 4
      have eventually_le: "eventually (\x. ?le x) (at y within {y .. b})"
      proof eventually_elim
        case (elim x1)
        have "norm (f x1 - f a) = norm (f x1 - f y)"
          by (simp add: \<open>a = y\<close>)
        also have "norm (f x1 - f y) \ e2"
          using elim \<open>a = y\<close> by (auto simp : dist_norm intro!:  less_imp_le)
        also have "\ \ e2 + (\ x1 - \ a + e2 + e * (x1 - a))"
          using \<open>0 < e\<close> elim
          by (intro add_increasing2[OF add_nonneg_nonneg order.refl])
            (auto simp: \<open>a = y\<close> dist_norm intro!: mult_nonneg_nonneg)
        also have "\ = \ x1 - \ a + e * (x1 - a) + e"
          by (simp add: e2_def)
        finally show "?le x1" .
      qed
      from this[unfolded eventually_at_topological] \<open>?le y\<close>
      obtain S where S: "open S" "y \ S" "\x. x\S \ x \ {y..b} \ ?le x"
        by metis
      from \<open>open S\<close> obtain d where d: "\<And>x. dist x y < d \<Longrightarrow> x \<in> S" "d > 0"
        by (force simp: dist_commute open_dist ball_def dest!: bspec[OF _ \<open>y \<in> S\<close>])
      define d' where "d' = min b (y + (d/2))"
      have "d' \ A"
        unfolding A_def
      proof safe
        show "a \ d'" using \a = y\ \0 < d\ \y < b\ by (simp add: d'_def)
        show "d' \ b" by (simp add: d'_def)
        fix x1
        assume "x1 \ {a..
        hence "x1 \ S" "x1 \ {y..b}"
          by (auto simp: \<open>a = y\<close> d'_def dist_real_def intro!: d )
        thus "?le x1"
          by (rule S)
      qed
      hence "d' \ y"
        unfolding y_def
        by (rule cSup_upper) simp
      then show "y = b" using \<open>d > 0\<close> \<open>y < b\<close>
        by (simp add: d'_def)
    next
      case False
      with \<open>a \<le> y\<close> have "a < y" by simp
      show "y = b"
      proof (rule ccontr)
        assume "y \ b"
        hence "y < b" using \<open>y \<le> b\<close> by simp
        let ?F = "at y within {y..
        from f' phi'
        have "(f has_vector_derivative f' y) ?F"
          and "(\ has_vector_derivative \' y) ?F"
          using \<open>a < y\<close> \<open>y < b\<close>
          by (auto simp add: at_within_open[of _ "{a<..] has_vector_derivative_def
            intro!: has_derivative_subset[where s="{a<.. and t="{y..])
        hence "\\<^sub>F x1 in ?F. norm (f x1 - f y - (x1 - y) *\<^sub>R f' y) \ e2 * \x1 - y\"
            "\\<^sub>F x1 in ?F. norm (\ x1 - \ y - (x1 - y) *\<^sub>R \' y) \ e2 * \x1 - y\"
          using \<open>e2 > 0\<close>
          by (auto simp: has_derivative_within_alt2 has_vector_derivative_def)
        moreover
        have "\\<^sub>F x1 in ?F. y \ x1" "\\<^sub>F x1 in ?F. x1 < b"
          by (auto simp: eventually_at_filter)
        ultimately
        have "\\<^sub>F x1 in ?F. norm (f x1 - f y) \ (\ x1 - \ y) + e * \x1 - y\"
          (is "\\<^sub>F x1 in ?F. ?le' x1")
        proof eventually_elim
          case (elim x1)
          from norm_triangle_ineq2[THEN order_trans, OF elim(1)]
          have "norm (f x1 - f y) \ norm (f' y) * \x1 - y\ + e2 * \x1 - y\"
            by (simp add: ac_simps)
          also have "norm (f' y) \ \' y" using bnd \a < y\ \y < b\ by simp
          also have "\' y * \x1 - y\ \ \ x1 - \ y + e2 * \x1 - y\"
            using elim by (simp add: ac_simps)
          finally
          have "norm (f x1 - f y) \ \ x1 - \ y + e2 * \x1 - y\ + e2 * \x1 - y\"
            by (auto simp: mult_right_mono)
          thus ?case by (simp add: e2_def)
        qed
        moreover have "?le' y" by simp
        ultimately obtain S
        where S: "open S" "y \ S" "\x. x\S \ x \ {y.. ?le' x"
          unfolding eventually_at_topological
          by metis
        from \<open>open S\<close> obtain d where d: "\<And>x. dist x y < d \<Longrightarrow> x \<in> S" "d > 0"
          by (force simp: dist_commute open_dist ball_def dest!: bspec[OF _ \<open>y \<in> S\<close>])
        define d' where "d' = min ((y + b)/2) (y + (d/2))"
        have "d' \ A"
          unfolding A_def
        proof safe
          show "a \ d'" using \a < y\ \0 < d\ \y < b\ by (simp add: d'_def)
          show "d' \ b" using \y < b\ by (simp add: d'_def min_def)
          fix x1
          assume x1: "x1 \ {a..
          show "?le x1"
          proof (cases "x1 < y")
            case True
            then show ?thesis
              using \<open>y \<in> A\<close> local.leI x1 by auto
          next
            case False
            hence x1': "x1 \ S" "x1 \ {y..
              by (auto simp: d'_def dist_real_def intro!: d)
            have "norm (f x1 - f a) \ norm (f x1 - f y) + norm (f y - f a)"
              by (rule order_trans[OF _ norm_triangle_ineq]) simp
            also note S(3)[OF x1']
            also note le_y
            finally show "?le x1"
              using False by (auto simp: algebra_simps)
          qed
        qed
        hence "d' \ y"
          unfolding y_def by (rule cSup_upper) simp
        thus False using \<open>d > 0\<close> \<open>y < b\<close>
          by (simp add: d'_def min_def split: if_split_asm)
      qed
    qed
    with le_y have "norm (f b - f a) \ \ b - \ a + e * (b - a + 1)"
      by (simp add: algebra_simps)
  } note * = this
  show ?thesis
  proof (rule field_le_epsilon)
    fix e::real assume "e > 0"
    then show "norm (f b - f a) \ \ b - \ a + e"
      using *[of "e / (b - a + 1)"] \<open>a < b\<close> by simp
  qed
qed

lemma differentiable_bound:
  fixes f :: "'a::real_normed_vector \ 'b::real_normed_vector"
  assumes "convex S"
    and derf: "\x. x\S \ (f has_derivative f' x) (at x within S)"
    and B: "\x. x \ S \ onorm (f' x) \ B"
    and x: "x \ S"
    and y: "y \ S"
  shows "norm (f x - f y) \ B * norm (x - y)"
proof -
  let ?p = "\u. x + u *\<^sub>R (y - x)"
  let ?\<phi> = "\<lambda>h. h * B * norm (x - y)"
  have *: "x + u *\<^sub>R (y - x) \ S" if "u \ {0..1}" for u
  proof -
    have "u *\<^sub>R y = u *\<^sub>R (y - x) + u *\<^sub>R x"
      by (simp add: scale_right_diff_distrib)
    then show "x + u *\<^sub>R (y - x) \ S"
      using that \<open>convex S\<close> x y by (simp add: convex_alt)
        (metis pth_b(2) pth_c(1) scaleR_collapse)
  qed
  have "\z. z \ (\u. x + u *\<^sub>R (y - x)) ` {0..1} \
          (f has_derivative f' z) (at z within (\u. x + u *\<^sub>R (y - x)) ` {0..1})"
    by (auto intro: * has_derivative_subset [OF derf])
  then have "continuous_on (?p ` {0..1}) f"
    unfolding continuous_on_eq_continuous_within
    by (meson has_derivative_continuous)
  with * have 1: "continuous_on {0 .. 1} (f \ ?p)"
    by (intro continuous_intros)+
  {
    fix u::real assume u: "u \{0 <..< 1}"
    let ?u = "?p u"
    interpret linear "(f' ?u)"
      using u by (auto intro!: has_derivative_linear derf *)
    have "(f \ ?p has_derivative (f' ?u) \ (\u. 0 + u *\<^sub>R (y - x))) (at u within box 0 1)"
      by (intro derivative_intros has_derivative_subset [OF derf]) (use u * in auto)
    hence "((f \ ?p) has_vector_derivative f' ?u (y - x)) (at u)"
      by (simp add: at_within_open[OF u open_greaterThanLessThan] scaleR has_vector_derivative_def o_def)
  } note 2 = this
  have 3: "continuous_on {0..1} ?\"
    by (rule continuous_intros)+
  have 4: "(?\ has_vector_derivative B * norm (x - y)) (at u)" for u
    by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros)
  {
    fix u::real assume u: "u \{0 <..< 1}"
    let ?u = "?p u"
    interpret bounded_linear "(f' ?u)"
      using u by (auto intro!: has_derivative_bounded_linear derf *)
    have "norm (f' ?u (y - x)) \ onorm (f' ?u) * norm (y - x)"
      by (rule onorm) (rule bounded_linear)
    also have "onorm (f' ?u) \ B"
      using u by (auto intro!: assms(3)[rule_format] *)
    finally have "norm ((f' ?u) (y - x)) \ B * norm (x - y)"
      by (simp add: mult_right_mono norm_minus_commute)
  } note 5 = this
  have "norm (f x - f y) = norm ((f \ (\u. x + u *\<^sub>R (y - x))) 1 - (f \ (\u. x + u *\<^sub>R (y - x))) 0)"
    by (auto simp add: norm_minus_commute)
  also
  from differentiable_bound_general[OF zero_less_one 1, OF 3 2 4 5]
  have "norm ((f \ ?p) 1 - (f \ ?p) 0) \ B * norm (x - y)"
    by simp
  finally show ?thesis .
qed

lemma field_differentiable_bound:
  fixes S :: "'a::real_normed_field set"
  assumes cvs: "convex S"
      and df:  "\z. z \ S \ (f has_field_derivative f' z) (at z within S)"
      and dn:  "\z. z \ S \ norm (f' z) \ B"
      and "x \ S" "y \ S"
    shows "norm(f x - f y) \ B * norm(x - y)"
proof (rule differentiable_bound [OF cvs])
  show "\x. x \ S \ (f has_derivative (*) (f' x)) (at x within S)"
    by (simp add: df has_field_derivative_imp_has_derivative)
  show "\x. x \ S \ onorm ((*) (f' x)) \ B"
    by (metis (no_types, opaque_lifting) dn norm_mult onorm_le order.refl order_trans)
qed (use assms in auto)

lemma
  differentiable_bound_segment:
  fixes f::"'a::real_normed_vector \ 'b::real_normed_vector"
  assumes "\t. t \ {0..1} \ x0 + t *\<^sub>R a \ G"
  assumes f': "\x. x \ G \ (f has_derivative f' x) (at x within G)"
  assumes B: "\x. x \ {0..1} \ onorm (f' (x0 + x *\<^sub>R a)) \ B"
  shows "norm (f (x0 + a) - f x0) \ norm a * B"
proof -
  let ?G = "(\x. x0 + x *\<^sub>R a) ` {0..1}"
  have "?G = (+) x0 ` (\x. x *\<^sub>R a) ` {0..1}" by auto
  also have "convex \"
    by (intro convex_translation convex_scaled convex_real_interval)
  finally have "convex ?G" .
  moreover have "?G \ G" "x0 \ ?G" "x0 + a \ ?G" using assms by (auto intro: image_eqI[where x=1])
  ultimately show ?thesis
    using has_derivative_subset[OF f' \?G \ G\] B
      differentiable_bound[of "(\x. x0 + x *\<^sub>R a) ` {0..1}" f f' B "x0 + a" x0]
    by (force simp: ac_simps)
qed

lemma differentiable_bound_linearization:
  fixes f::"'a::real_normed_vector \ 'b::real_normed_vector"
  assumes S: "\t. t \ {0..1} \ a + t *\<^sub>R (b - a) \ S"
  assumes f'[derivative_intros]: "\x. x \ S \ (f has_derivative f' x) (at x within S)"
  assumes B: "\x. x \ S \ onorm (f' x - f' x0) \ B"
  assumes "x0 \ S"
  shows "norm (f b - f a - f' x0 (b - a)) \ norm (b - a) * B"
proof -
  define g where [abs_def]: "g x = f x - f' x0 x" for x
  have g: "\x. x \ S \ (g has_derivative (\i. f' x i - f' x0 i)) (at x within S)"
    unfolding g_def using assms
    by (auto intro!: derivative_eq_intros
      bounded_linear.has_derivative[OF has_derivative_bounded_linear, OF f'])
  from B have "\x\{0..1}. onorm (\i. f' (a + x *\<^sub>R (b - a)) i - f' x0 i) \ B"
    using assms by (auto simp: fun_diff_def)
  with differentiable_bound_segment[OF S g] \<open>x0 \<in> S\<close>
  show ?thesis
    by (simp add: g_def field_simps linear_diff[OF has_derivative_linear[OF f']])
qed

lemma vector_differentiable_bound_linearization:
  fixes f::"real \ 'b::real_normed_vector"
  assumes f': "\x. x \ S \ (f has_vector_derivative f' x) (at x within S)"
  assumes "closed_segment a b \ S"
  assumes B: "\x. x \ S \ norm (f' x - f' x0) \ B"
  assumes "x0 \ S"
  shows "norm (f b - f a - (b - a) *\<^sub>R f' x0) \ norm (b - a) * B"
  using assms
  by (intro differentiable_bound_linearization[of a b S f "\x h. h *\<^sub>R f' x" x0 B])
    (force simp: closed_segment_real_eq has_vector_derivative_def
      scaleR_diff_right[symmetric] mult.commute[of B]
      intro!: onorm_le mult_left_mono)+

text \<open>In particular.\<close>

lemma has_derivative_zero_constant:
  fixes f :: "'a::real_normed_vector \ 'b::real_normed_vector"
  assumes "convex s"
    and "\x. x \ s \ (f has_derivative (\h. 0)) (at x within s)"
  shows "\c. \x\s. f x = c"
proof -
  { fix x y assume "x \ s" "y \ s"
    then have "norm (f x - f y) \ 0 * norm (x - y)"
      using assms by (intro differentiable_bound[of s]) (auto simp: onorm_zero)
    then have "f x = f y"
      by simp }
  then show ?thesis
    by metis
qed

lemma has_field_derivative_zero_constant:
  assumes "convex s" "\x. x \ s \ (f has_field_derivative 0) (at x within s)"
  shows   "\c. \x\s. f (x) = (c :: 'a :: real_normed_field)"
proof (rule has_derivative_zero_constant)
  have A: "(*) 0 = (\_. 0 :: 'a)" by (intro ext) simp
  fix x assume "x \ s" thus "(f has_derivative (\h. 0)) (at x within s)"
    using assms(2)[of x] by (simp add: has_field_derivative_def A)
qed fact

lemma
  has_vector_derivative_zero_constant:
  assumes "convex s"
  assumes "\x. x \ s \ (f has_vector_derivative 0) (at x within s)"
  obtains c where "\x. x \ s \ f x = c"
  using has_derivative_zero_constant[of s f] assms
  by (auto simp: has_vector_derivative_def)

lemma has_derivative_zero_unique:
  fixes f :: "'a::real_normed_vector \ 'b::real_normed_vector"
  assumes "convex s"
    and "\x. x \ s \ (f has_derivative (\h. 0)) (at x within s)"
    and "x \ s" "y \ s"
  shows "f x = f y"
  using has_derivative_zero_constant[OF assms(1,2)] assms(3-) by force

lemma has_derivative_zero_unique_connected:
  fixes f :: "'a::real_normed_vector \ 'b::real_normed_vector"
  assumes "open s" "connected s"
  assumes f: "\x. x \ s \ (f has_derivative (\x. 0)) (at x)"
  assumes "x \ s" "y \ s"
  shows "f x = f y"
proof (rule connected_local_const[where f=f, OF \<open>connected s\<close> \<open>x\<in>s\<close> \<open>y\<in>s\<close>])
  show "\a\s. eventually (\b. f a = f b) (at a within s)"
  proof
    fix a assume "a \ s"
    with \<open>open s\<close> obtain e where "0 < e" "ball a e \<subseteq> s"
      by (rule openE)
    then have "\c. \x\ball a e. f x = c"
      by (intro has_derivative_zero_constant)
         (auto simp: at_within_open[OF _ open_ball] f)
    with \<open>0<e\<close> have "\<forall>x\<in>ball a e. f a = f x"
      by auto
    then show "eventually (\b. f a = f b) (at a within s)"
      using \<open>0<e\<close> unfolding eventually_at_topological
      by (intro exI[of _ "ball a e"]) auto
  qed
qed

subsection \<open>Differentiability of inverse function (most basic form)\<close>

lemma has_derivative_inverse_basic:
  fixes f :: "'a::real_normed_vector \ 'b::real_normed_vector"
  assumes derf: "(f has_derivative f') (at (g y))"
    and ling': "bounded_linear g'"
    and "g' \ f' = id"
    and contg: "continuous (at y) g"
    and "open T"
    and "y \ T"
    and fg: "\z. z \ T \ f (g z) = z"
  shows "(g has_derivative g') (at y)"
proof -
  interpret f': bounded_linear f'
    using assms unfolding has_derivative_def by auto
  interpret g': bounded_linear g'
    using assms by auto
  obtain C where C: "0 < C" "\x. norm (g' x) \ norm x * C"
    using bounded_linear.pos_bounded[OF assms(2)] by blast
  have lem1: "\e>0. \d>0. \z.
    norm (z - y) < d \<longrightarrow> norm (g z - g y - g'(z - y)) \<le> e * norm (g z - g y)"
  proof (intro allI impI)
    fix e :: real
    assume "e > 0"
    with C(1) have *: "e / C > 0" by auto
    obtain d0 where  "0 < d0" and d0:
        "\u. norm (u - g y) < d0 \ norm (f u - f (g y) - f' (u - g y)) \ e / C * norm (u - g y)"
      using derf * unfolding has_derivative_at_alt by blast
    obtain d1 where "0 < d1" and d1: "\x. \0 < dist x y; dist x y < d1\ \ dist (g x) (g y) < d0"
      using contg \<open>0 < d0\<close> unfolding continuous_at Lim_at by blast
    obtain d2 where "0 < d2" and d2: "\u. dist u y < d2 \ u \ T"
      using \<open>open T\<close> \<open>y \<in> T\<close> unfolding open_dist by blast
    obtain d where d: "0 < d" "d < d1" "d < d2"
      using field_lbound_gt_zero[OF \<open>0 < d1\<close> \<open>0 < d2\<close>] by blast
    show "\d>0. \z. norm (z - y) < d \ norm (g z - g y - g' (z - y)) \ e * norm (g z - g y)"
    proof (intro exI allI impI conjI)
      fix z
      assume as: "norm (z - y) < d"
      then have "z \ T"
        using d2 d unfolding dist_norm by auto
      have "norm (g z - g y - g' (z - y)) \ norm (g' (f (g z) - y - f' (g z - g y)))"
        unfolding g'.diff f'.diff
        unfolding assms(3)[unfolded o_def id_def, THEN fun_cong] fg[OF \<open>z\<in>T\<close>]
        by (simp add: norm_minus_commute)
      also have "\ \ norm (f (g z) - y - f' (g z - g y)) * C"
        by (rule C(2))
      also have "\ \ (e / C) * norm (g z - g y) * C"
      proof -
        have "norm (g z - g y) < d0"
          by (metis as cancel_comm_monoid_add_class.diff_cancel d(2) \<open>0 < d0\<close> d1 diff_gt_0_iff_gt diff_strict_mono dist_norm dist_self zero_less_dist_iff)
        then show ?thesis
          by (metis C(1) \<open>y \<in> T\<close> d0 fg mult_le_cancel_right_pos)
      qed
      also have "\ \ e * norm (g z - g y)"
        using C by (auto simp add: field_simps)
      finally show "norm (g z - g y - g' (z - y)) \ e * norm (g z - g y)"
        by simp
    qed (use d in auto)
  qed
  have *: "(0::real) < 1 / 2"
    by auto
  obtain d where "0 < d" and d:
      "\z. norm (z - y) < d \ norm (g z - g y - g' (z - y)) \ 1/2 * norm (g z - g y)"
    using lem1 * by blast
  define B where "B = C * 2"
  have "B > 0"
    unfolding B_def using C by auto
  have lem2: "norm (g z - g y) \ B * norm (z - y)" if z: "norm(z - y) < d" for z
  proof -
    have "norm (g z - g y) \ norm(g' (z - y)) + norm ((g z - g y) - g'(z - y))"
      by (rule norm_triangle_sub)
    also have "\ \ norm (g' (z - y)) + 1 / 2 * norm (g z - g y)"
      by (rule add_left_mono) (use d z in auto)
    also have "\ \ norm (z - y) * C + 1 / 2 * norm (g z - g y)"
      by (rule add_right_mono) (use C in auto)
    finally show "norm (g z - g y) \ B * norm (z - y)"
      unfolding B_def
      by (auto simp add: field_simps)
  qed
  show ?thesis
    unfolding has_derivative_at_alt
  proof (intro conjI assms allI impI)
    fix e :: real
    assume "e > 0"
    then have *: "e / B > 0" by (metis \<open>B > 0\<close> divide_pos_pos)
    obtain d' where "0 < d'" and d':
        "\z. norm (z - y) < d' \ norm (g z - g y - g' (z - y)) \ e / B * norm (g z - g y)"
      using lem1 * by blast
    obtain k where k: "0 < k" "k < d" "k < d'"
      using field_lbound_gt_zero[OF \<open>0 < d\<close> \<open>0 < d'\<close>] by blast
    show "\d>0. \ya. norm (ya - y) < d \ norm (g ya - g y - g' (ya - y)) \ e * norm (ya - y)"
    proof (intro exI allI impI conjI)
      fix z
      assume as: "norm (z - y) < k"
      then have "norm (g z - g y - g' (z - y)) \ e / B * norm(g z - g y)"
        using d' k by auto
      also have "\ \ e * norm (z - y)"
        unfolding times_divide_eq_left pos_divide_le_eq[OF \<open>B>0\<close>]
        using lem2[of z] k as \<open>e > 0\<close>
        by (auto simp add: field_simps)
      finally show "norm (g z - g y - g' (z - y)) \ e * norm (z - y)"
        by simp
    qed (use k in auto)
  qed
qed

text\<^marker>\<open>tag unimportant\<close>\<open>Inverse function theorem for complex derivatives\<close>
lemma has_field_derivative_inverse_basic:
  shows "DERIV f (g y) :> f' \
        f' \ 0 \
        continuous (at y) g \<Longrightarrow>
        open t \<Longrightarrow>
        y \<in> t \<Longrightarrow>
        (\<And>z. z \<in> t \<Longrightarrow> f (g z) = z)
        \<Longrightarrow> DERIV g y :> inverse (f')"
  unfolding has_field_derivative_def
  by (rule has_derivative_inverse_basic) (auto simp: bounded_linear_mult_right)

text \<open>Simply rewrite that based on the domain point x.\<close>

lemma has_derivative_inverse_basic_x:
  fixes f :: "'a::real_normed_vector \ 'b::real_normed_vector"
  assumes "(f has_derivative f') (at x)"
    and "bounded_linear g'"
    and "g' \ f' = id"
    and "continuous (at (f x)) g"
    and "g (f x) = x"
    and "open T"
    and "f x \ T"
    and "\y. y \ T \ f (g y) = y"
  shows "(g has_derivative g') (at (f x))"
  by (rule has_derivative_inverse_basic) (use assms in auto)

text \<open>This is the version in Dieudonne', assuming continuity of f and g.\<close>

lemma has_derivative_inverse_dieudonne:
  fixes f :: "'a::real_normed_vector \ 'b::real_normed_vector"
  assumes "open S"
    and fS: "open (f ` S)"
    and A: "continuous_on S f" "continuous_on (f ` S) g"
           "\x. x \ S \ g (f x) = x" "x \ S"
    and B: "(f has_derivative f') (at x)" "bounded_linear g'" "g' \ f' = id"
  shows "(g has_derivative g') (at (f x))"
  using A fS continuous_on_eq_continuous_at
  by (intro has_derivative_inverse_basic_x[OF B _ _ fS]) force+

text \<open>Here's the simplest way of not assuming much about g.\<close>

proposition has_derivative_inverse:
  fixes f :: "'a::real_normed_vector \ 'b::real_normed_vector"
  assumes "compact S"
    and "x \ S"
    and fx: "f x \ interior (f ` S)"
    and "continuous_on S f"
    and gf: "\y. y \ S \ g (f y) = y"
    and B: "(f has_derivative f') (at x)" "bounded_linear g'" "g' \ f' = id"
  shows "(g has_derivative g') (at (f x))"
proof -
  have *: "\y. y \ interior (f ` S) \ f (g y) = y"
    by (metis gf image_iff interior_subset subsetCE)
  show ?thesis
    using assms * continuous_on_interior continuous_on_inv fx
    by (intro has_derivative_inverse_basic_x[OF B, where T = "interior (f`S)"]) blast+
qed

text \<open>Invertible derivative continuous at a point implies local
injectivity. It's only for this we need continuity of the derivative,
except of course if we want the fact that the inverse derivative is
also continuous. So if we know for some other reason that the inverse
function exists, it's OK.\

proposition has_derivative_locally_injective:
  fixes f :: "'n::euclidean_space \ 'm::euclidean_space"
  assumes "a \ S"
      and "open S"
      and bling: "bounded_linear g'"
      and "g' \ f' a = id"
      and derf: "\x. x \ S \ (f has_derivative f' x) (at x)"
      and "\e. e > 0 \ \d>0. \x. dist a x < d \ onorm (\v. f' x v - f' a v) < e"
  obtains r where "r > 0" "ball a r \ S" "inj_on f (ball a r)"
proof -
  interpret bounded_linear g'
    using assms by auto
  note f'g' = assms(4)[unfolded id_def o_def,THEN cong]
  have "g' (f' a (\Basis)) = (\Basis)" "(\Basis) \ (0::'n)"
    using f'g' by auto
  then have *: "0 < onorm g'"
    unfolding onorm_pos_lt[OF assms(3)]
    by fastforce
  define k where "k = 1 / onorm g' / 2"
  have *: "k > 0"
    unfolding k_def using * by auto
  obtain d1 where d1:
      "0 < d1"
      "\x. dist a x < d1 \ onorm (\v. f' x v - f' a v) < k"
    using assms(6) * by blast
  from \<open>open S\<close> obtain d2 where "d2 > 0" "ball a d2 \<subseteq> S"
    using \<open>a\<in>S\<close> ..
  obtain d2 where d2: "0 < d2" "ball a d2 \ S"
    using \<open>0 < d2\<close> \<open>ball a d2 \<subseteq> S\<close> by blast
  obtain d where d: "0 < d" "d < d1" "d < d2"
    using field_lbound_gt_zero[OF d1(1) d2(1)] by blast
  show ?thesis
  proof
    show "0 < d" by (fact d)
    show "ball a d \ S"
      using \<open>d < d2\<close> \<open>ball a d2 \<subseteq> S\<close> by auto
    show "inj_on f (ball a d)"
    unfolding inj_on_def
    proof (intro strip)
      fix x y
      assume as: "x \ ball a d" "y \ ball a d" "f x = f y"
      define ph where [abs_def]: "ph w = w - g' (f w - f x)" for w
      have ph':"ph = g' \<circ> (\<lambda>w. f' a w - (f w - f x))"
        unfolding ph_def o_def  by (simp add: diff f'g')
      have "norm (ph x - ph y) \ (1 / 2) * norm (x - y)"
      proof (rule differentiable_bound[OF convex_ball _ _ as(1-2)])
        fix u
        assume u: "u \ ball a d"
        then have "u \ S"
          using d d2 by auto
        have *: "(\v. v - g' (f' u v)) = g' \ (\w. f' a w - f' u w)"
          unfolding o_def and diff
          using f'g' by auto
        have blin: "bounded_linear (f' a)"
          using \<open>a \<in> S\<close> derf by blast
        show "(ph has_derivative (\v. v - g' (f' u v))) (at u within ball a d)"
          unfolding ph' * comp_def
          by (rule \<open>u \<in> S\<close> derivative_eq_intros has_derivative_at_withinI [OF derf] bounded_linear.has_derivative [OF blin]  bounded_linear.has_derivative [OF bling] |simp)+
        have **: "bounded_linear (\x. f' u x - f' a x)" "bounded_linear (\x. f' a x - f' u x)"
          using \<open>u \<in> S\<close> blin bounded_linear_sub derf by auto
        then have "onorm (\v. v - g' (f' u v)) \ onorm g' * onorm (\w. f' a w - f' u w)"
          by (simp add: "*" bounded_linear_axioms onorm_compose)
        also have "\ \ onorm g' * k"
          apply (rule mult_left_mono)
          using d1(2)[of u]
          using onorm_neg[where f="\x. f' u x - f' a x"] d u onorm_pos_le[OF bling]
           apply (auto simp: algebra_simps)
          done
        also have "\ \ 1 / 2"
          unfolding k_def by auto
        finally show "onorm (\v. v - g' (f' u v)) \ 1 / 2" .
      qed
      moreover have "norm (ph y - ph x) = norm (y - x)"
        by (simp add: as(3) ph_def)
      ultimately show "x = y"
        unfolding norm_minus_commute by auto
    qed
  qed
qed

subsection \<open>Uniformly convergent sequence of derivatives\<close>

lemma has_derivative_sequence_lipschitz_lemma:
  fixes f :: "nat \ 'a::real_normed_vector \ 'b::real_normed_vector"
  assumes "convex S"
    and derf: "\n x. x \ S \ ((f n) has_derivative (f' n x)) (at x within S)"
    and nle: "\n x h. \n\N; x \ S\ \ norm (f' n x h - g' x h) \ e * norm h"
    and "0 \ e"
  shows "\m\N. \n\N. \x\S. \y\S. norm ((f m x - f n x) - (f m y - f n y)) \ 2 * e * norm (x - y)"
proof clarify
  fix m n x y
  assume as: "N \ m" "N \ n" "x \ S" "y \ S"
  show "norm ((f m x - f n x) - (f m y - f n y)) \ 2 * e * norm (x - y)"
  proof (rule differentiable_bound[where f'="\x h. f' m x h - f' n x h", OF \convex S\ _ _ as(3-4)])
    fix x
    assume "x \ S"
    show "((\a. f m a - f n a) has_derivative (\h. f' m x h - f' n x h)) (at x within S)"
      by (rule derivative_intros derf \<open>x\<in>S\<close>)+
    show "onorm (\h. f' m x h - f' n x h) \ 2 * e"
    proof (rule onorm_bound)
      fix h
      have "norm (f' m x h - f' n x h) \ norm (f' m x h - g' x h) + norm (f' n x h - g' x h)"
        using norm_triangle_ineq[of "f' m x h - g' x h" "- f' n x h + g' x h"]
        by (auto simp add: algebra_simps norm_minus_commute)
      also have "\ \ e * norm h + e * norm h"
        using nle[OF \<open>N \<le> m\<close> \<open>x \<in> S\<close>, of h] nle[OF \<open>N \<le> n\<close> \<open>x \<in> S\<close>, of h]
        by (auto simp add: field_simps)
      finally show "norm (f' m x h - f' n x h) \ 2 * e * norm h"
        by auto
    qed (simp add: \<open>0 \<le> e\<close>)
  qed
qed

lemma has_derivative_sequence_Lipschitz:
  fixes f :: "nat \ 'a::real_normed_vector \ 'b::real_normed_vector"
  assumes "convex S"
    and "\n x. x \ S \ ((f n) has_derivative (f' n x)) (at x within S)"
    and nle: "\e. e > 0 \ \\<^sub>F n in sequentially. \x\S. \h. norm (f' n x h - g' x h) \ e * norm h"
    and "e > 0"
  shows "\N. \m\N. \n\N. \x\S. \y\S.
    norm ((f m x - f n x) - (f m y - f n y)) \<le> e * norm (x - y)"
proof -
  have *: "2 * (e/2) = e"
    using \<open>e > 0\<close> by auto
  obtain N where "\n\N. \x\S. \h. norm (f' n x h - g' x h) \ (e/2) * norm h"
    using nle \<open>e > 0\<close>
    unfolding eventually_sequentially
    by (metis less_divide_eq_numeral1(1) mult_zero_left)
  then show "\N. \m\N. \n\N. \x\S. \y\S. norm (f m x - f n x - (f m y - f n y)) \ e * norm (x - y)"
    apply (rule_tac x=N in exI)
    apply (rule has_derivative_sequence_lipschitz_lemma[where e="e/2", unfolded *])
    using assms \<open>e > 0\<close>
    apply auto
    done
qed

proposition has_derivative_sequence:
  fixes f :: "nat \ 'a::real_normed_vector \ 'b::banach"
  assumes "convex S"
    and derf: "\n x. x \ S \ ((f n) has_derivative (f' n x)) (at x within S)"
--> --------------------

--> maximum size reached

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

quality95%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

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.