src/HOL/Analysis/Derivative.thy
author wenzelm
Sun Sep 18 20:33:48 2016 +0200 (2016-09-18)
changeset 63915 bab633745c7f
parent 63886 685fb01256af
child 63918 6bf55e6e0b75
permissions -rw-r--r--
tuned proofs;
     1 (*  Title:      HOL/Analysis/Derivative.thy
     2     Author:     John Harrison
     3     Author:     Robert Himmelmann, TU Muenchen (translation from HOL Light)
     4 *)
     5 
     6 section \<open>Multivariate calculus in Euclidean space\<close>
     7 
     8 theory Derivative
     9 imports Brouwer_Fixpoint Operator_Norm Uniform_Limit Bounded_Linear_Function
    10 begin
    11 
    12 lemma bounded_linear_component [intro]: "bounded_linear (\<lambda>x::'a::euclidean_space. x \<bullet> k)"
    13   by (rule bounded_linear_inner_left)
    14 
    15 lemma onorm_inner_left:
    16   assumes "bounded_linear r"
    17   shows "onorm (\<lambda>x. r x \<bullet> f) \<le> onorm r * norm f"
    18 proof (rule onorm_bound)
    19   fix x
    20   have "norm (r x \<bullet> f) \<le> norm (r x) * norm f"
    21     by (simp add: Cauchy_Schwarz_ineq2)
    22   also have "\<dots> \<le> onorm r * norm x * norm f"
    23     by (intro mult_right_mono onorm assms norm_ge_zero)
    24   finally show "norm (r x \<bullet> f) \<le> onorm r * norm f * norm x"
    25     by (simp add: ac_simps)
    26 qed (intro mult_nonneg_nonneg norm_ge_zero onorm_pos_le assms)
    27 
    28 lemma onorm_inner_right:
    29   assumes "bounded_linear r"
    30   shows "onorm (\<lambda>x. f \<bullet> r x) \<le> norm f * onorm r"
    31   apply (subst inner_commute)
    32   apply (rule onorm_inner_left[OF assms, THEN order_trans])
    33   apply simp
    34   done
    35 
    36 declare has_derivative_bounded_linear[dest]
    37 
    38 subsection \<open>Derivatives\<close>
    39 
    40 subsubsection \<open>Combining theorems.\<close>
    41 
    42 lemmas has_derivative_id = has_derivative_ident
    43 lemmas has_derivative_neg = has_derivative_minus
    44 lemmas has_derivative_sub = has_derivative_diff
    45 lemmas scaleR_right_has_derivative = has_derivative_scaleR_right
    46 lemmas scaleR_left_has_derivative = has_derivative_scaleR_left
    47 lemmas inner_right_has_derivative = has_derivative_inner_right
    48 lemmas inner_left_has_derivative = has_derivative_inner_left
    49 lemmas mult_right_has_derivative = has_derivative_mult_right
    50 lemmas mult_left_has_derivative = has_derivative_mult_left
    51 
    52 lemma has_derivative_add_const:
    53   "(f has_derivative f') net \<Longrightarrow> ((\<lambda>x. f x + c) has_derivative f') net"
    54   by (intro derivative_eq_intros) auto
    55 
    56 
    57 subsection \<open>Derivative with composed bilinear function.\<close>
    58 
    59 lemma has_derivative_bilinear_within:
    60   assumes "(f has_derivative f') (at x within s)"
    61     and "(g has_derivative g') (at x within s)"
    62     and "bounded_bilinear h"
    63   shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x within s)"
    64   using bounded_bilinear.FDERIV[OF assms(3,1,2)] .
    65 
    66 lemma has_derivative_bilinear_at:
    67   assumes "(f has_derivative f') (at x)"
    68     and "(g has_derivative g') (at x)"
    69     and "bounded_bilinear h"
    70   shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x)"
    71   using has_derivative_bilinear_within[of f f' x UNIV g g' h] assms by simp
    72 
    73 text \<open>These are the only cases we'll care about, probably.\<close>
    74 
    75 lemma has_derivative_within: "(f has_derivative f') (at x within s) \<longleftrightarrow>
    76     bounded_linear f' \<and> ((\<lambda>y. (1 / norm(y - x)) *\<^sub>R (f y - (f x + f' (y - x)))) \<longlongrightarrow> 0) (at x within s)"
    77   unfolding has_derivative_def Lim
    78   by (auto simp add: netlimit_within field_simps)
    79 
    80 lemma has_derivative_at: "(f has_derivative f') (at x) \<longleftrightarrow>
    81     bounded_linear f' \<and> ((\<lambda>y. (1 / (norm(y - x))) *\<^sub>R (f y - (f x + f' (y - x)))) \<longlongrightarrow> 0) (at x)"
    82   using has_derivative_within [of f f' x UNIV]
    83   by simp
    84 
    85 text \<open>More explicit epsilon-delta forms.\<close>
    86 
    87 lemma has_derivative_within':
    88   "(f has_derivative f')(at x within s) \<longleftrightarrow>
    89     bounded_linear f' \<and>
    90     (\<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. 0 < norm (x' - x) \<and> norm (x' - x) < d \<longrightarrow>
    91       norm (f x' - f x - f'(x' - x)) / norm (x' - x) < e)"
    92   unfolding has_derivative_within Lim_within dist_norm
    93   unfolding diff_0_right
    94   by (simp add: diff_diff_eq)
    95 
    96 lemma has_derivative_at':
    97   "(f has_derivative f') (at x) \<longleftrightarrow> bounded_linear f' \<and>
    98     (\<forall>e>0. \<exists>d>0. \<forall>x'. 0 < norm (x' - x) \<and> norm (x' - x) < d \<longrightarrow>
    99       norm (f x' - f x - f'(x' - x)) / norm (x' - x) < e)"
   100   using has_derivative_within' [of f f' x UNIV]
   101   by simp
   102 
   103 lemma has_derivative_at_within:
   104   "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f') (at x within s)"
   105   unfolding has_derivative_within' has_derivative_at'
   106   by blast
   107 
   108 lemma has_derivative_within_open:
   109   "a \<in> s \<Longrightarrow> open s \<Longrightarrow>
   110     (f has_derivative f') (at a within s) \<longleftrightarrow> (f has_derivative f') (at a)"
   111   by (simp only: at_within_interior interior_open)
   112 
   113 lemma has_derivative_right:
   114   fixes f :: "real \<Rightarrow> real"
   115     and y :: "real"
   116   shows "(f has_derivative (op * y)) (at x within ({x <..} \<inter> I)) \<longleftrightarrow>
   117     ((\<lambda>t. (f x - f t) / (x - t)) \<longlongrightarrow> y) (at x within ({x <..} \<inter> I))"
   118 proof -
   119   have "((\<lambda>t. (f t - (f x + y * (t - x))) / \<bar>t - x\<bar>) \<longlongrightarrow> 0) (at x within ({x<..} \<inter> I)) \<longleftrightarrow>
   120     ((\<lambda>t. (f t - f x) / (t - x) - y) \<longlongrightarrow> 0) (at x within ({x<..} \<inter> I))"
   121     by (intro Lim_cong_within) (auto simp add: diff_divide_distrib add_divide_distrib)
   122   also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f t - f x) / (t - x)) \<longlongrightarrow> y) (at x within ({x<..} \<inter> I))"
   123     by (simp add: Lim_null[symmetric])
   124   also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f x - f t) / (x - t)) \<longlongrightarrow> y) (at x within ({x<..} \<inter> I))"
   125     by (intro Lim_cong_within) (simp_all add: field_simps)
   126   finally show ?thesis
   127     by (simp add: bounded_linear_mult_right has_derivative_within)
   128 qed
   129 
   130 subsubsection \<open>Caratheodory characterization\<close>
   131 
   132 lemmas DERIV_within_iff = has_field_derivative_iff
   133 
   134 lemma DERIV_caratheodory_within:
   135   "(f has_field_derivative l) (at x within s) \<longleftrightarrow>
   136    (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> continuous (at x within s) g \<and> g x = l)"
   137       (is "?lhs = ?rhs")
   138 proof
   139   assume ?lhs
   140   show ?rhs
   141   proof (intro exI conjI)
   142     let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
   143     show "\<forall>z. f z - f x = ?g z * (z-x)" by simp
   144     show "continuous (at x within s) ?g" using \<open>?lhs\<close>
   145       by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within)
   146     show "?g x = l" by simp
   147   qed
   148 next
   149   assume ?rhs
   150   then obtain g where
   151     "(\<forall>z. f z - f x = g z * (z-x))" and "continuous (at x within s) g" and "g x = l" by blast
   152   thus ?lhs
   153     by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within)
   154 qed
   155 
   156 subsubsection \<open>Limit transformation for derivatives\<close>
   157 
   158 lemma has_derivative_transform_within:
   159   assumes "(f has_derivative f') (at x within s)"
   160     and "0 < d"
   161     and "x \<in> s"
   162     and "\<And>x'. \<lbrakk>x' \<in> s; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
   163   shows "(g has_derivative f') (at x within s)"
   164   using assms
   165   unfolding has_derivative_within
   166   by (force simp add: intro: Lim_transform_within)
   167 
   168 lemma has_derivative_transform_within_open:
   169   assumes "(f has_derivative f') (at x)"
   170     and "open s"
   171     and "x \<in> s"
   172     and "\<And>x. x\<in>s \<Longrightarrow> f x = g x"
   173   shows "(g has_derivative f') (at x)"
   174   using assms  unfolding has_derivative_at
   175   by (force simp add: intro: Lim_transform_within_open)
   176 
   177 subsection \<open>Differentiability\<close>
   178 
   179 definition
   180   differentiable_on :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a set \<Rightarrow> bool"
   181     (infix "differentiable'_on" 50)
   182   where "f differentiable_on s \<longleftrightarrow> (\<forall>x\<in>s. f differentiable (at x within s))"
   183 
   184 lemma differentiableI: "(f has_derivative f') net \<Longrightarrow> f differentiable net"
   185   unfolding differentiable_def
   186   by auto
   187 
   188 lemma differentiable_onD: "\<lbrakk>f differentiable_on S; x \<in> S\<rbrakk> \<Longrightarrow> f differentiable (at x within S)"
   189   using differentiable_on_def by blast
   190 
   191 lemma differentiable_at_withinI: "f differentiable (at x) \<Longrightarrow> f differentiable (at x within s)"
   192   unfolding differentiable_def
   193   using has_derivative_at_within
   194   by blast
   195 
   196 lemma differentiable_at_imp_differentiable_on:
   197   "(\<And>x. x \<in> s \<Longrightarrow> f differentiable at x) \<Longrightarrow> f differentiable_on s"
   198   by (metis differentiable_at_withinI differentiable_on_def)
   199 
   200 corollary differentiable_iff_scaleR:
   201   fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
   202   shows "f differentiable F \<longleftrightarrow> (\<exists>d. (f has_derivative (\<lambda>x. x *\<^sub>R d)) F)"
   203   by (auto simp: differentiable_def dest: has_derivative_linear linear_imp_scaleR)
   204 
   205 lemma differentiable_within_open: (* TODO: delete *)
   206   assumes "a \<in> s"
   207     and "open s"
   208   shows "f differentiable (at a within s) \<longleftrightarrow> f differentiable (at a)"
   209   using assms
   210   by (simp only: at_within_interior interior_open)
   211 
   212 lemma differentiable_on_eq_differentiable_at:
   213   "open s \<Longrightarrow> f differentiable_on s \<longleftrightarrow> (\<forall>x\<in>s. f differentiable at x)"
   214   unfolding differentiable_on_def
   215   by (metis at_within_interior interior_open)
   216 
   217 lemma differentiable_transform_within:
   218   assumes "f differentiable (at x within s)"
   219     and "0 < d"
   220     and "x \<in> s"
   221     and "\<And>x'. \<lbrakk>x'\<in>s; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
   222   shows "g differentiable (at x within s)"
   223    using assms has_derivative_transform_within unfolding differentiable_def
   224    by blast
   225 
   226 lemma differentiable_on_ident [simp, derivative_intros]: "(\<lambda>x. x) differentiable_on S"
   227   by (simp add: differentiable_at_imp_differentiable_on)
   228 
   229 lemma differentiable_on_id [simp, derivative_intros]: "id differentiable_on S"
   230   by (simp add: id_def)
   231 
   232 lemma differentiable_on_compose:
   233    "\<lbrakk>g differentiable_on S; f differentiable_on (g ` S)\<rbrakk> \<Longrightarrow> (\<lambda>x. f (g x)) differentiable_on S"
   234 by (simp add: differentiable_in_compose differentiable_on_def)
   235 
   236 lemma bounded_linear_imp_differentiable_on: "bounded_linear f \<Longrightarrow> f differentiable_on S"
   237   by (simp add: differentiable_on_def bounded_linear_imp_differentiable)
   238 
   239 lemma linear_imp_differentiable_on:
   240   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   241   shows "linear f \<Longrightarrow> f differentiable_on S"
   242 by (simp add: differentiable_on_def linear_imp_differentiable)
   243 
   244 lemma differentiable_on_minus [simp, derivative_intros]:
   245    "f differentiable_on S \<Longrightarrow> (\<lambda>z. -(f z)) differentiable_on S"
   246 by (simp add: differentiable_on_def)
   247 
   248 lemma differentiable_on_add [simp, derivative_intros]:
   249    "\<lbrakk>f differentiable_on S; g differentiable_on S\<rbrakk> \<Longrightarrow> (\<lambda>z. f z + g z) differentiable_on S"
   250 by (simp add: differentiable_on_def)
   251 
   252 lemma differentiable_on_diff [simp, derivative_intros]:
   253    "\<lbrakk>f differentiable_on S; g differentiable_on S\<rbrakk> \<Longrightarrow> (\<lambda>z. f z - g z) differentiable_on S"
   254 by (simp add: differentiable_on_def)
   255 
   256 lemma differentiable_on_inverse [simp, derivative_intros]:
   257   fixes f :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
   258   shows "f differentiable_on S \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> f x \<noteq> 0) \<Longrightarrow> (\<lambda>x. inverse (f x)) differentiable_on S"
   259 by (simp add: differentiable_on_def)
   260 
   261 lemma differentiable_on_scaleR [derivative_intros, simp]:
   262    "\<lbrakk>f differentiable_on S; g differentiable_on S\<rbrakk> \<Longrightarrow> (\<lambda>x. f x *\<^sub>R g x) differentiable_on S"
   263   unfolding differentiable_on_def
   264   by (blast intro: differentiable_scaleR)
   265 
   266 lemma has_derivative_sqnorm_at [derivative_intros, simp]:
   267    "((\<lambda>x. (norm x)\<^sup>2) has_derivative (\<lambda>x. 2 *\<^sub>R (a \<bullet> x))) (at a)"
   268 using has_derivative_bilinear_at [of id id a id id "op  \<bullet>"]
   269 by (auto simp: inner_commute dot_square_norm bounded_bilinear_inner)
   270 
   271 lemma differentiable_sqnorm_at [derivative_intros, simp]:
   272   fixes a :: "'a :: {real_normed_vector,real_inner}"
   273   shows "(\<lambda>x. (norm x)\<^sup>2) differentiable (at a)"
   274 by (force simp add: differentiable_def intro: has_derivative_sqnorm_at)
   275 
   276 lemma differentiable_on_sqnorm [derivative_intros, simp]:
   277   fixes S :: "'a :: {real_normed_vector,real_inner} set"
   278   shows "(\<lambda>x. (norm x)\<^sup>2) differentiable_on S"
   279 by (simp add: differentiable_at_imp_differentiable_on)
   280 
   281 lemma differentiable_norm_at [derivative_intros, simp]:
   282   fixes a :: "'a :: {real_normed_vector,real_inner}"
   283   shows "a \<noteq> 0 \<Longrightarrow> norm differentiable (at a)"
   284 using differentiableI has_derivative_norm by blast
   285 
   286 lemma differentiable_on_norm [derivative_intros, simp]:
   287   fixes S :: "'a :: {real_normed_vector,real_inner} set"
   288   shows "0 \<notin> S \<Longrightarrow> norm differentiable_on S"
   289 by (metis differentiable_at_imp_differentiable_on differentiable_norm_at)
   290 
   291 
   292 subsection \<open>Frechet derivative and Jacobian matrix\<close>
   293 
   294 definition "frechet_derivative f net = (SOME f'. (f has_derivative f') net)"
   295 
   296 lemma frechet_derivative_works:
   297   "f differentiable net \<longleftrightarrow> (f has_derivative (frechet_derivative f net)) net"
   298   unfolding frechet_derivative_def differentiable_def
   299   unfolding some_eq_ex[of "\<lambda> f' . (f has_derivative f') net"] ..
   300 
   301 lemma linear_frechet_derivative: "f differentiable net \<Longrightarrow> linear (frechet_derivative f net)"
   302   unfolding frechet_derivative_works has_derivative_def
   303   by (auto intro: bounded_linear.linear)
   304 
   305 
   306 subsection \<open>Differentiability implies continuity\<close>
   307 
   308 lemma differentiable_imp_continuous_within:
   309   "f differentiable (at x within s) \<Longrightarrow> continuous (at x within s) f"
   310   by (auto simp: differentiable_def intro: has_derivative_continuous)
   311 
   312 lemma differentiable_imp_continuous_on:
   313   "f differentiable_on s \<Longrightarrow> continuous_on s f"
   314   unfolding differentiable_on_def continuous_on_eq_continuous_within
   315   using differentiable_imp_continuous_within by blast
   316 
   317 lemma differentiable_on_subset:
   318   "f differentiable_on t \<Longrightarrow> s \<subseteq> t \<Longrightarrow> f differentiable_on s"
   319   unfolding differentiable_on_def
   320   using differentiable_within_subset
   321   by blast
   322 
   323 lemma differentiable_on_empty: "f differentiable_on {}"
   324   unfolding differentiable_on_def
   325   by auto
   326 
   327 text \<open>Results about neighborhoods filter.\<close>
   328 
   329 lemma eventually_nhds_metric_le:
   330   "eventually P (nhds a) = (\<exists>d>0. \<forall>x. dist x a \<le> d \<longrightarrow> P x)"
   331   unfolding eventually_nhds_metric by (safe, rule_tac x="d / 2" in exI, auto)
   332 
   333 lemma le_nhds: "F \<le> nhds a \<longleftrightarrow> (\<forall>S. open S \<and> a \<in> S \<longrightarrow> eventually (\<lambda>x. x \<in> S) F)"
   334   unfolding le_filter_def eventually_nhds by (fast elim: eventually_mono)
   335 
   336 lemma le_nhds_metric: "F \<le> nhds a \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist x a < e) F)"
   337   unfolding le_filter_def eventually_nhds_metric by (fast elim: eventually_mono)
   338 
   339 lemma le_nhds_metric_le: "F \<le> nhds a \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist x a \<le> e) F)"
   340   unfolding le_filter_def eventually_nhds_metric_le by (fast elim: eventually_mono)
   341 
   342 text \<open>Several results are easier using a "multiplied-out" variant.
   343 (I got this idea from Dieudonne's proof of the chain rule).\<close>
   344 
   345 lemma has_derivative_within_alt:
   346   "(f has_derivative f') (at x within s) \<longleftrightarrow> bounded_linear f' \<and>
   347     (\<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))"
   348   unfolding has_derivative_within filterlim_def le_nhds_metric_le eventually_filtermap
   349     eventually_at dist_norm diff_diff_eq
   350   by (force simp add: linear_0 bounded_linear.linear pos_divide_le_eq)
   351 
   352 lemma has_derivative_within_alt2:
   353   "(f has_derivative f') (at x within s) \<longleftrightarrow> bounded_linear f' \<and>
   354     (\<forall>e>0. eventually (\<lambda>y. norm (f y - f x - f' (y - x)) \<le> e * norm (y - x)) (at x within s))"
   355   unfolding has_derivative_within filterlim_def le_nhds_metric_le eventually_filtermap
   356     eventually_at dist_norm diff_diff_eq
   357   by (force simp add: linear_0 bounded_linear.linear pos_divide_le_eq)
   358 
   359 lemma has_derivative_at_alt:
   360   "(f has_derivative f') (at x) \<longleftrightarrow>
   361     bounded_linear f' \<and>
   362     (\<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))"
   363   using has_derivative_within_alt[where s=UNIV]
   364   by simp
   365 
   366 
   367 subsection \<open>The chain rule\<close>
   368 
   369 lemma diff_chain_within[derivative_intros]:
   370   assumes "(f has_derivative f') (at x within s)"
   371     and "(g has_derivative g') (at (f x) within (f ` s))"
   372   shows "((g \<circ> f) has_derivative (g' \<circ> f'))(at x within s)"
   373   using has_derivative_in_compose[OF assms]
   374   by (simp add: comp_def)
   375 
   376 lemma diff_chain_at[derivative_intros]:
   377   "(f has_derivative f') (at x) \<Longrightarrow>
   378     (g has_derivative g') (at (f x)) \<Longrightarrow> ((g \<circ> f) has_derivative (g' \<circ> f')) (at x)"
   379   using has_derivative_compose[of f f' x UNIV g g']
   380   by (simp add: comp_def)
   381 
   382 
   383 subsection \<open>Composition rules stated just for differentiability\<close>
   384 
   385 lemma differentiable_chain_at:
   386   "f differentiable (at x) \<Longrightarrow>
   387     g differentiable (at (f x)) \<Longrightarrow> (g \<circ> f) differentiable (at x)"
   388   unfolding differentiable_def
   389   by (meson diff_chain_at)
   390 
   391 lemma differentiable_chain_within:
   392   "f differentiable (at x within s) \<Longrightarrow>
   393     g differentiable (at(f x) within (f ` s)) \<Longrightarrow> (g \<circ> f) differentiable (at x within s)"
   394   unfolding differentiable_def
   395   by (meson diff_chain_within)
   396 
   397 
   398 subsection \<open>Uniqueness of derivative\<close>
   399 
   400 
   401 text \<open>
   402  The general result is a bit messy because we need approachability of the
   403  limit point from any direction. But OK for nontrivial intervals etc.
   404 \<close>
   405 
   406 lemma frechet_derivative_unique_within:
   407   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   408   assumes "(f has_derivative f') (at x within s)"
   409     and "(f has_derivative f'') (at x within s)"
   410     and "\<forall>i\<in>Basis. \<forall>e>0. \<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> (x + d *\<^sub>R i) \<in> s"
   411   shows "f' = f''"
   412 proof -
   413   note as = assms(1,2)[unfolded has_derivative_def]
   414   then interpret f': bounded_linear f' by auto
   415   from as interpret f'': bounded_linear f'' by auto
   416   have "x islimpt s" unfolding islimpt_approachable
   417   proof (rule, rule)
   418     fix e :: real
   419     assume "e > 0"
   420     obtain d where "0 < \<bar>d\<bar>" and "\<bar>d\<bar> < e" and "x + d *\<^sub>R (SOME i. i \<in> Basis) \<in> s"
   421       using assms(3) SOME_Basis \<open>e>0\<close> by blast
   422     then show "\<exists>x'\<in>s. x' \<noteq> x \<and> dist x' x < e"
   423       apply (rule_tac x="x + d *\<^sub>R (SOME i. i \<in> Basis)" in bexI)
   424       unfolding dist_norm
   425       apply (auto simp: SOME_Basis nonzero_Basis)
   426       done
   427   qed
   428   then have *: "netlimit (at x within s) = x"
   429     apply (auto intro!: netlimit_within)
   430     by (metis trivial_limit_within)
   431   show ?thesis
   432     apply (rule linear_eq_stdbasis)
   433     unfolding linear_conv_bounded_linear
   434     apply (rule as(1,2)[THEN conjunct1])+
   435   proof (rule, rule ccontr)
   436     fix i :: 'a
   437     assume i: "i \<in> Basis"
   438     define e where "e = norm (f' i - f'' i)"
   439     assume "f' i \<noteq> f'' i"
   440     then have "e > 0"
   441       unfolding e_def by auto
   442     obtain d where d:
   443       "0 < d"
   444       "(\<And>xa. xa\<in>s \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow>
   445           dist ((f xa - f x - f' (xa - x)) /\<^sub>R norm (xa - x) -
   446               (f xa - f x - f'' (xa - x)) /\<^sub>R norm (xa - x)) (0 - 0) < e)"
   447       using tendsto_diff [OF as(1,2)[THEN conjunct2]]
   448       unfolding * Lim_within
   449       using \<open>e>0\<close> by blast
   450     obtain c where c: "0 < \<bar>c\<bar>" "\<bar>c\<bar> < d \<and> x + c *\<^sub>R i \<in> s"
   451       using assms(3) i d(1) by blast
   452     have *: "norm (- ((1 / \<bar>c\<bar>) *\<^sub>R f' (c *\<^sub>R i)) + (1 / \<bar>c\<bar>) *\<^sub>R f'' (c *\<^sub>R i)) =
   453         norm ((1 / \<bar>c\<bar>) *\<^sub>R (- (f' (c *\<^sub>R i)) + f'' (c *\<^sub>R i)))"
   454       unfolding scaleR_right_distrib by auto
   455     also have "\<dots> = norm ((1 / \<bar>c\<bar>) *\<^sub>R (c *\<^sub>R (- (f' i) + f'' i)))"
   456       unfolding f'.scaleR f''.scaleR
   457       unfolding scaleR_right_distrib scaleR_minus_right
   458       by auto
   459     also have "\<dots> = e"
   460       unfolding e_def
   461       using c(1)
   462       using norm_minus_cancel[of "f' i - f'' i"]
   463       by auto
   464     finally show False
   465       using c
   466       using d(2)[of "x + c *\<^sub>R i"]
   467       unfolding dist_norm
   468       unfolding f'.scaleR f''.scaleR f'.add f''.add f'.diff f''.diff
   469         scaleR_scaleR scaleR_right_diff_distrib scaleR_right_distrib
   470       using i
   471       by (auto simp: inverse_eq_divide)
   472   qed
   473 qed
   474 
   475 lemma frechet_derivative_unique_at:
   476   "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f'') (at x) \<Longrightarrow> f' = f''"
   477   by (rule has_derivative_unique)
   478 
   479 lemma frechet_derivative_unique_within_closed_interval:
   480   fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   481   assumes "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"
   482     and "x \<in> cbox a b"
   483     and "(f has_derivative f' ) (at x within cbox a b)"
   484     and "(f has_derivative f'') (at x within cbox a b)"
   485   shows "f' = f''"
   486   apply(rule frechet_derivative_unique_within)
   487   apply(rule assms(3,4))+
   488 proof (rule, rule, rule)
   489   fix e :: real
   490   fix i :: 'a
   491   assume "e > 0" and i: "i \<in> Basis"
   492   then show "\<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> x + d *\<^sub>R i \<in> cbox a b"
   493   proof (cases "x\<bullet>i = a\<bullet>i")
   494     case True
   495     then show ?thesis
   496       apply (rule_tac x="(min (b\<bullet>i - a\<bullet>i)  e) / 2" in exI)
   497       using assms(1)[THEN bspec[where x=i]] and \<open>e>0\<close> and assms(2)
   498       unfolding mem_box
   499       using i
   500       apply (auto simp add: field_simps inner_simps inner_Basis)
   501       done
   502   next
   503     note * = assms(2)[unfolded mem_box, THEN bspec, OF i]
   504     case False
   505     moreover have "a \<bullet> i < x \<bullet> i"
   506       using False * by auto
   507     moreover {
   508       have "a \<bullet> i * 2 + min (x \<bullet> i - a \<bullet> i) e \<le> a\<bullet>i *2 + x\<bullet>i - a\<bullet>i"
   509         by auto
   510       also have "\<dots> = a\<bullet>i + x\<bullet>i"
   511         by auto
   512       also have "\<dots> \<le> 2 * (x\<bullet>i)"
   513         using * by auto
   514       finally have "a \<bullet> i * 2 + min (x \<bullet> i - a \<bullet> i) e \<le> x \<bullet> i * 2"
   515         by auto
   516     }
   517     moreover have "min (x \<bullet> i - a \<bullet> i) e \<ge> 0"
   518       using * and \<open>e>0\<close> by auto
   519     then have "x \<bullet> i * 2 \<le> b \<bullet> i * 2 + min (x \<bullet> i - a \<bullet> i) e"
   520       using * by auto
   521     ultimately show ?thesis
   522       apply (rule_tac x="- (min (x\<bullet>i - a\<bullet>i) e) / 2" in exI)
   523       using assms(1)[THEN bspec, OF i] and \<open>e>0\<close> and assms(2)
   524       unfolding mem_box
   525       using i
   526       apply (auto simp add: field_simps inner_simps inner_Basis)
   527       done
   528   qed
   529 qed
   530 
   531 lemma frechet_derivative_unique_within_open_interval:
   532   fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   533   assumes "x \<in> box a b"
   534     and "(f has_derivative f' ) (at x within box a b)"
   535     and "(f has_derivative f'') (at x within box a b)"
   536   shows "f' = f''"
   537 proof -
   538   from assms(1) have *: "at x within box a b = at x"
   539     by (metis at_within_interior interior_open open_box)
   540   from assms(2,3) [unfolded *] show "f' = f''"
   541     by (rule frechet_derivative_unique_at)
   542 qed
   543 
   544 lemma frechet_derivative_at:
   545   "(f has_derivative f') (at x) \<Longrightarrow> f' = frechet_derivative f (at x)"
   546   apply (rule frechet_derivative_unique_at[of f])
   547   apply assumption
   548   unfolding frechet_derivative_works[symmetric]
   549   using differentiable_def
   550   apply auto
   551   done
   552 
   553 lemma frechet_derivative_within_cbox:
   554   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   555   assumes "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"
   556     and "x \<in> cbox a b"
   557     and "(f has_derivative f') (at x within cbox a b)"
   558   shows "frechet_derivative f (at x within cbox a b) = f'"
   559   using assms
   560   by (metis Derivative.differentiableI frechet_derivative_unique_within_closed_interval frechet_derivative_works)
   561 
   562 
   563 subsection \<open>The traditional Rolle theorem in one dimension\<close>
   564 
   565 text \<open>Derivatives of local minima and maxima are zero.\<close>
   566 
   567 lemma has_derivative_local_min:
   568   fixes f :: "'a::real_normed_vector \<Rightarrow> real"
   569   assumes deriv: "(f has_derivative f') (at x)"
   570   assumes min: "eventually (\<lambda>y. f x \<le> f y) (at x)"
   571   shows "f' = (\<lambda>h. 0)"
   572 proof
   573   fix h :: 'a
   574   interpret f': bounded_linear f'
   575     using deriv by (rule has_derivative_bounded_linear)
   576   show "f' h = 0"
   577   proof (cases "h = 0")
   578     assume "h \<noteq> 0"
   579     from min obtain d where d1: "0 < d" and d2: "\<forall>y\<in>ball x d. f x \<le> f y"
   580       unfolding eventually_at by (force simp: dist_commute)
   581     have "FDERIV (\<lambda>r. x + r *\<^sub>R h) 0 :> (\<lambda>r. r *\<^sub>R h)"
   582       by (intro derivative_eq_intros) auto
   583     then have "FDERIV (\<lambda>r. f (x + r *\<^sub>R h)) 0 :> (\<lambda>k. f' (k *\<^sub>R h))"
   584       by (rule has_derivative_compose, simp add: deriv)
   585     then have "DERIV (\<lambda>r. f (x + r *\<^sub>R h)) 0 :> f' h"
   586       unfolding has_field_derivative_def by (simp add: f'.scaleR mult_commute_abs)
   587     moreover have "0 < d / norm h" using d1 and \<open>h \<noteq> 0\<close> by simp
   588     moreover have "\<forall>y. \<bar>0 - y\<bar> < d / norm h \<longrightarrow> f (x + 0 *\<^sub>R h) \<le> f (x + y *\<^sub>R h)"
   589       using \<open>h \<noteq> 0\<close> by (auto simp add: d2 dist_norm pos_less_divide_eq)
   590     ultimately show "f' h = 0"
   591       by (rule DERIV_local_min)
   592   qed (simp add: f'.zero)
   593 qed
   594 
   595 lemma has_derivative_local_max:
   596   fixes f :: "'a::real_normed_vector \<Rightarrow> real"
   597   assumes "(f has_derivative f') (at x)"
   598   assumes "eventually (\<lambda>y. f y \<le> f x) (at x)"
   599   shows "f' = (\<lambda>h. 0)"
   600   using has_derivative_local_min [of "\<lambda>x. - f x" "\<lambda>h. - f' h" "x"]
   601   using assms unfolding fun_eq_iff by simp
   602 
   603 lemma differential_zero_maxmin:
   604   fixes f::"'a::real_normed_vector \<Rightarrow> real"
   605   assumes "x \<in> s"
   606     and "open s"
   607     and deriv: "(f has_derivative f') (at x)"
   608     and mono: "(\<forall>y\<in>s. f y \<le> f x) \<or> (\<forall>y\<in>s. f x \<le> f y)"
   609   shows "f' = (\<lambda>v. 0)"
   610   using mono
   611 proof
   612   assume "\<forall>y\<in>s. f y \<le> f x"
   613   with \<open>x \<in> s\<close> and \<open>open s\<close> have "eventually (\<lambda>y. f y \<le> f x) (at x)"
   614     unfolding eventually_at_topological by auto
   615   with deriv show ?thesis
   616     by (rule has_derivative_local_max)
   617 next
   618   assume "\<forall>y\<in>s. f x \<le> f y"
   619   with \<open>x \<in> s\<close> and \<open>open s\<close> have "eventually (\<lambda>y. f x \<le> f y) (at x)"
   620     unfolding eventually_at_topological by auto
   621   with deriv show ?thesis
   622     by (rule has_derivative_local_min)
   623 qed
   624 
   625 lemma differential_zero_maxmin_component: (* TODO: delete? *)
   626   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   627   assumes k: "k \<in> Basis"
   628     and ball: "0 < e" "(\<forall>y \<in> ball x e. (f y)\<bullet>k \<le> (f x)\<bullet>k) \<or> (\<forall>y\<in>ball x e. (f x)\<bullet>k \<le> (f y)\<bullet>k)"
   629     and diff: "f differentiable (at x)"
   630   shows "(\<Sum>j\<in>Basis. (frechet_derivative f (at x) j \<bullet> k) *\<^sub>R j) = (0::'a)" (is "?D k = 0")
   631 proof -
   632   let ?f' = "frechet_derivative f (at x)"
   633   have "x \<in> ball x e" using \<open>0 < e\<close> by simp
   634   moreover have "open (ball x e)" by simp
   635   moreover have "((\<lambda>x. f x \<bullet> k) has_derivative (\<lambda>h. ?f' h \<bullet> k)) (at x)"
   636     using bounded_linear_inner_left diff[unfolded frechet_derivative_works]
   637     by (rule bounded_linear.has_derivative)
   638   ultimately have "(\<lambda>h. frechet_derivative f (at x) h \<bullet> k) = (\<lambda>v. 0)"
   639     using ball(2) by (rule differential_zero_maxmin)
   640   then show ?thesis
   641     unfolding fun_eq_iff by simp
   642 qed
   643 
   644 lemma rolle:
   645   fixes f :: "real \<Rightarrow> real"
   646   assumes "a < b"
   647     and "f a = f b"
   648     and "continuous_on {a .. b} f"
   649     and "\<forall>x\<in>{a <..< b}. (f has_derivative f' x) (at x)"
   650   shows "\<exists>x\<in>{a <..< b}. f' x = (\<lambda>v. 0)"
   651 proof -
   652   have "\<exists>x\<in>box a b. (\<forall>y\<in>box a b. f x \<le> f y) \<or> (\<forall>y\<in>box a b. f y \<le> f x)"
   653   proof -
   654     have "(a + b) / 2 \<in> {a .. b}"
   655       using assms(1) by auto
   656     then have *: "{a .. b} \<noteq> {}"
   657       by auto
   658     obtain d where d:
   659         "d \<in>cbox a b"
   660         "\<forall>y\<in>cbox a b. f y \<le> f d"
   661       using continuous_attains_sup[OF compact_Icc * assms(3)] by auto
   662     obtain c where c:
   663         "c \<in> cbox a b"
   664         "\<forall>y\<in>cbox a b. f c \<le> f y"
   665       using continuous_attains_inf[OF compact_Icc * assms(3)] by auto
   666     show ?thesis
   667     proof (cases "d \<in> box a b \<or> c \<in> box a b")
   668       case True
   669       then show ?thesis
   670         by (metis c(2) d(2) box_subset_cbox subset_iff)
   671     next
   672       define e where "e = (a + b) /2"
   673       case False
   674       then have "f d = f c"
   675         using d c assms(2) by auto
   676       then have "\<And>x. x \<in> {a..b} \<Longrightarrow> f x = f d"
   677         using c d
   678         by force
   679       then show ?thesis
   680         apply (rule_tac x=e in bexI)
   681         unfolding e_def
   682         using assms(1)
   683         apply auto
   684         done
   685     qed
   686   qed
   687   then obtain x where x: "x \<in> {a <..< b}" "(\<forall>y\<in>{a <..< b}. f x \<le> f y) \<or> (\<forall>y\<in>{a <..< b}. f y \<le> f x)"
   688     by auto
   689   then have "f' x = (\<lambda>v. 0)"
   690     apply (rule_tac differential_zero_maxmin[of x "box a b" f "f' x"])
   691     using assms
   692     apply auto
   693     done
   694   then show ?thesis
   695     by (metis x(1))
   696 qed
   697 
   698 
   699 subsection \<open>One-dimensional mean value theorem\<close>
   700 
   701 lemma mvt:
   702   fixes f :: "real \<Rightarrow> real"
   703   assumes "a < b"
   704     and "continuous_on {a..b} f"
   705   assumes "\<forall>x\<in>{a<..<b}. (f has_derivative (f' x)) (at x)"
   706   shows "\<exists>x\<in>{a<..<b}. f b - f a = (f' x) (b - a)"
   707 proof -
   708   have "\<exists>x\<in>{a <..< b}. (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)"
   709   proof (intro rolle[OF assms(1), of "\<lambda>x. f x - (f b - f a) / (b - a) * x"] ballI)
   710     fix x
   711     assume x: "x \<in> {a <..< b}"
   712     show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative
   713         (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)"
   714       by (intro derivative_intros assms(3)[rule_format,OF x])
   715   qed (insert assms(1,2), auto intro!: continuous_intros simp: field_simps)
   716   then obtain x where
   717     "x \<in> {a <..< b}"
   718     "(\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)" ..
   719   then show ?thesis
   720     by (metis (hide_lams) assms(1) diff_gt_0_iff_gt eq_iff_diff_eq_0
   721       zero_less_mult_iff nonzero_mult_divide_cancel_right not_real_square_gt_zero
   722       times_divide_eq_left)
   723 qed
   724 
   725 lemma mvt_simple:
   726   fixes f :: "real \<Rightarrow> real"
   727   assumes "a < b"
   728     and "\<forall>x\<in>{a..b}. (f has_derivative f' x) (at x within {a..b})"
   729   shows "\<exists>x\<in>{a<..<b}. f b - f a = f' x (b - a)"
   730 proof (rule mvt)
   731   have "f differentiable_on {a..b}"
   732     using assms(2) unfolding differentiable_on_def differentiable_def by fast
   733   then show "continuous_on {a..b} f"
   734     by (rule differentiable_imp_continuous_on)
   735   show "\<forall>x\<in>{a<..<b}. (f has_derivative f' x) (at x)"
   736   proof
   737     fix x
   738     assume x: "x \<in> {a <..< b}"
   739     show "(f has_derivative f' x) (at x)"
   740       unfolding at_within_open[OF x open_greaterThanLessThan,symmetric]
   741       apply (rule has_derivative_within_subset)
   742       apply (rule assms(2)[rule_format])
   743       using x
   744       apply auto
   745       done
   746   qed
   747 qed (rule assms(1))
   748 
   749 lemma mvt_very_simple:
   750   fixes f :: "real \<Rightarrow> real"
   751   assumes "a \<le> b"
   752     and "\<forall>x\<in>{a .. b}. (f has_derivative f' x) (at x within {a .. b})"
   753   shows "\<exists>x\<in>{a .. b}. f b - f a = f' x (b - a)"
   754 proof (cases "a = b")
   755   interpret bounded_linear "f' b"
   756     using assms(2) assms(1) by auto
   757   case True
   758   then show ?thesis
   759     apply (rule_tac x=a in bexI)
   760     using assms(2)[THEN bspec[where x=a]]
   761     unfolding has_derivative_def
   762     unfolding True
   763     using zero
   764     apply auto
   765     done
   766 next
   767   case False
   768   then show ?thesis
   769     using mvt_simple[OF _ assms(2)]
   770     using assms(1)
   771     by auto
   772 qed
   773 
   774 text \<open>A nice generalization (see Havin's proof of 5.19 from Rudin's book).\<close>
   775 
   776 lemma mvt_general:
   777   fixes f :: "real \<Rightarrow> 'a::real_inner"
   778   assumes "a < b"
   779     and "continuous_on {a .. b} f"
   780     and "\<forall>x\<in>{a<..<b}. (f has_derivative f'(x)) (at x)"
   781   shows "\<exists>x\<in>{a<..<b}. norm (f b - f a) \<le> norm (f' x (b - a))"
   782 proof -
   783   have "\<exists>x\<in>{a<..<b}. (f b - f a) \<bullet> f b - (f b - f a) \<bullet> f a = (f b - f a) \<bullet> f' x (b - a)"
   784     apply (rule mvt)
   785     apply (rule assms(1))
   786     apply (intro continuous_intros assms(2))
   787     using assms(3)
   788     apply (fast intro: has_derivative_inner_right)
   789     done
   790   then obtain x where x:
   791     "x \<in> {a<..<b}"
   792     "(f b - f a) \<bullet> f b - (f b - f a) \<bullet> f a = (f b - f a) \<bullet> f' x (b - a)" ..
   793   show ?thesis
   794   proof (cases "f a = f b")
   795     case False
   796     have "norm (f b - f a) * norm (f b - f a) = (norm (f b - f a))\<^sup>2"
   797       by (simp add: power2_eq_square)
   798     also have "\<dots> = (f b - f a) \<bullet> (f b - f a)"
   799       unfolding power2_norm_eq_inner ..
   800     also have "\<dots> = (f b - f a) \<bullet> f' x (b - a)"
   801       using x(2) by (simp only: inner_diff_right)
   802     also have "\<dots> \<le> norm (f b - f a) * norm (f' x (b - a))"
   803       by (rule norm_cauchy_schwarz)
   804     finally show ?thesis
   805       using False x(1)
   806       by (auto simp add: mult_left_cancel)
   807   next
   808     case True
   809     then show ?thesis
   810       using assms(1)
   811       apply (rule_tac x="(a + b) /2" in bexI)
   812       apply auto
   813       done
   814   qed
   815 qed
   816 
   817 
   818 subsection \<open>More general bound theorems\<close>
   819 
   820 lemma differentiable_bound_general:
   821   fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
   822   assumes "a < b"
   823     and f_cont: "continuous_on {a .. b} f"
   824     and phi_cont: "continuous_on {a .. b} \<phi>"
   825     and f': "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
   826     and phi': "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> (\<phi> has_vector_derivative \<phi>' x) (at x)"
   827     and bnd: "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> norm (f' x) \<le> \<phi>' x"
   828   shows "norm (f b - f a) \<le> \<phi> b - \<phi> a"
   829 proof -
   830   {
   831     fix x assume x: "a < x" "x < b"
   832     have "0 \<le> norm (f' x)" by simp
   833     also have "\<dots> \<le> \<phi>' x" using x by (auto intro!: bnd)
   834     finally have "0 \<le> \<phi>' x" .
   835   } note phi'_nonneg = this
   836   note f_tendsto = assms(2)[simplified continuous_on_def, rule_format]
   837   note phi_tendsto = assms(3)[simplified continuous_on_def, rule_format]
   838   {
   839     fix e::real assume "e > 0"
   840     define e2 where "e2 = e / 2"
   841     with \<open>e > 0\<close> have "e2 > 0" by simp
   842     let ?le = "\<lambda>x1. norm (f x1 - f a) \<le> \<phi> x1 - \<phi> a + e * (x1 - a) + e"
   843     define A where "A = {x2. a \<le> x2 \<and> x2 \<le> b \<and> (\<forall>x1\<in>{a ..< x2}. ?le x1)}"
   844     have A_subset: "A \<subseteq> {a .. b}" by (auto simp: A_def)
   845     {
   846       fix x2
   847       assume a: "a \<le> x2" "x2 \<le> b" and le: "\<forall>x1\<in>{a..<x2}. ?le x1"
   848       have "?le x2" using \<open>e > 0\<close>
   849       proof cases
   850         assume "x2 \<noteq> a" with a have "a < x2" by simp
   851         have "at x2 within {a <..<x2}\<noteq> bot"
   852           using \<open>a < x2\<close>
   853           by (auto simp: trivial_limit_within islimpt_in_closure)
   854         moreover
   855         have "((\<lambda>x1. (\<phi> x1 - \<phi> a) + e * (x1 - a) + e) \<longlongrightarrow> (\<phi> x2 - \<phi> a) + e * (x2 - a) + e) (at x2 within {a <..<x2})"
   856           "((\<lambda>x1. norm (f x1 - f a)) \<longlongrightarrow> norm (f x2 - f a)) (at x2 within {a <..<x2})"
   857           using a
   858           by (auto intro!: tendsto_eq_intros f_tendsto phi_tendsto
   859             intro: tendsto_within_subset[where S="{a .. b}"])
   860         moreover
   861         have "eventually (\<lambda>x. x > a) (at x2 within {a <..<x2})"
   862           by (auto simp: eventually_at_filter)
   863         hence "eventually ?le (at x2 within {a <..<x2})"
   864           unfolding eventually_at_filter
   865           by eventually_elim (insert le, auto)
   866         ultimately
   867         show ?thesis
   868           by (rule tendsto_le)
   869       qed simp
   870     } note le_cont = this
   871     have "a \<in> A"
   872       using assms by (auto simp: A_def)
   873     hence [simp]: "A \<noteq> {}" by auto
   874     have A_ivl: "\<And>x1 x2. x2 \<in> A \<Longrightarrow> x1 \<in> {a ..x2} \<Longrightarrow> x1 \<in> A"
   875       by (simp add: A_def)
   876     have [simp]: "bdd_above A" by (auto simp: A_def)
   877     define y where "y = Sup A"
   878     have "y \<le> b"
   879       unfolding y_def
   880       by (simp add: cSup_le_iff) (simp add: A_def)
   881      have leI: "\<And>x x1. a \<le> x1 \<Longrightarrow> x \<in> A \<Longrightarrow> x1 < x \<Longrightarrow> ?le x1"
   882        by (auto simp: A_def intro!: le_cont)
   883     have y_all_le: "\<forall>x1\<in>{a..<y}. ?le x1"
   884       by (auto simp: y_def less_cSup_iff leI)
   885     have "a \<le> y"
   886       by (metis \<open>a \<in> A\<close> \<open>bdd_above A\<close> cSup_upper y_def)
   887     have "y \<in> A"
   888       using y_all_le \<open>a \<le> y\<close> \<open>y \<le> b\<close>
   889       by (auto simp: A_def)
   890     hence "A = {a .. y}"
   891       using A_subset
   892       by (auto simp: subset_iff y_def cSup_upper intro: A_ivl)
   893     from le_cont[OF \<open>a \<le> y\<close> \<open>y \<le> b\<close> y_all_le] have le_y: "?le y" .
   894     {
   895       assume "a \<noteq> y" with \<open>a \<le> y\<close> have "a < y" by simp
   896       have "y = b"
   897       proof (rule ccontr)
   898         assume "y \<noteq> b"
   899         hence "y < b" using \<open>y \<le> b\<close> by simp
   900         let ?F = "at y within {y..<b}"
   901         from f' phi'
   902         have "(f has_vector_derivative f' y) ?F"
   903           and "(\<phi> has_vector_derivative \<phi>' y) ?F"
   904           using \<open>a < y\<close> \<open>y < b\<close>
   905           by (auto simp add: at_within_open[of _ "{a<..<b}"] has_vector_derivative_def
   906             intro!: has_derivative_subset[where s="{a<..<b}" and t="{y..<b}"])
   907         hence "\<forall>\<^sub>F x1 in ?F. norm (f x1 - f y - (x1 - y) *\<^sub>R f' y) \<le> e2 * \<bar>x1 - y\<bar>"
   908             "\<forall>\<^sub>F x1 in ?F. norm (\<phi> x1 - \<phi> y - (x1 - y) *\<^sub>R \<phi>' y) \<le> e2 * \<bar>x1 - y\<bar>"
   909           using \<open>e2 > 0\<close>
   910           by (auto simp: has_derivative_within_alt2 has_vector_derivative_def)
   911         moreover
   912         have "\<forall>\<^sub>F x1 in ?F. y \<le> x1" "\<forall>\<^sub>F x1 in ?F. x1 < b"
   913           by (auto simp: eventually_at_filter)
   914         ultimately
   915         have "\<forall>\<^sub>F x1 in ?F. norm (f x1 - f y) \<le> (\<phi> x1 - \<phi> y) + e * \<bar>x1 - y\<bar>"
   916           (is "\<forall>\<^sub>F x1 in ?F. ?le' x1")
   917         proof eventually_elim
   918           case (elim x1)
   919           from norm_triangle_ineq2[THEN order_trans, OF elim(1)]
   920           have "norm (f x1 - f y) \<le> norm (f' y) * \<bar>x1 - y\<bar> + e2 * \<bar>x1 - y\<bar>"
   921             by (simp add: ac_simps)
   922           also have "norm (f' y) \<le> \<phi>' y" using bnd \<open>a < y\<close> \<open>y < b\<close> by simp
   923           also
   924           from elim have "\<phi>' y * \<bar>x1 - y\<bar> \<le> \<phi> x1 - \<phi> y + e2 * \<bar>x1 - y\<bar>"
   925             by (simp add: ac_simps)
   926           finally
   927           have "norm (f x1 - f y) \<le> \<phi> x1 - \<phi> y + e2 * \<bar>x1 - y\<bar> + e2 * \<bar>x1 - y\<bar>"
   928             by (auto simp: mult_right_mono)
   929           thus ?case by (simp add: e2_def)
   930         qed
   931         moreover have "?le' y" by simp
   932         ultimately obtain S
   933         where S: "open S" "y \<in> S" "\<And>x. x\<in>S \<Longrightarrow> x \<in> {y..<b} \<Longrightarrow> ?le' x"
   934           unfolding eventually_at_topological
   935           by metis
   936         from \<open>open S\<close> obtain d where d: "\<And>x. dist x y < d \<Longrightarrow> x \<in> S" "d > 0"
   937           by (force simp: dist_commute open_dist ball_def dest!: bspec[OF _ \<open>y \<in> S\<close>])
   938         define d' where "d' = min ((y + b)/2) (y + (d/2))"
   939         have "d' \<in> A"
   940           unfolding A_def
   941         proof safe
   942           show "a \<le> d'" using \<open>a < y\<close> \<open>0 < d\<close> \<open>y < b\<close> by (simp add: d'_def)
   943           show "d' \<le> b" using \<open>y < b\<close> by (simp add: d'_def min_def)
   944           fix x1
   945           assume x1: "x1 \<in> {a..<d'}"
   946           {
   947             assume "x1 < y"
   948             hence "?le x1"
   949               using \<open>x1 \<in> {a..<d'}\<close> y_all_le by auto
   950           } moreover {
   951             assume "x1 \<ge> y"
   952             hence x1': "x1 \<in> S" "x1 \<in> {y..<b}" using x1
   953               by (auto simp: d'_def dist_real_def intro!: d)
   954             have "norm (f x1 - f a) \<le> norm (f x1 - f y) + norm (f y - f a)"
   955               by (rule order_trans[OF _ norm_triangle_ineq]) simp
   956             also note S(3)[OF x1']
   957             also note le_y
   958             finally have "?le x1"
   959               using \<open>x1 \<ge> y\<close> by (auto simp: algebra_simps)
   960           } ultimately show "?le x1" by arith
   961         qed
   962         hence "d' \<le> y"
   963           unfolding y_def
   964           by (rule cSup_upper) simp
   965         thus False using \<open>d > 0\<close> \<open>y < b\<close>
   966           by (simp add: d'_def min_def split: if_split_asm)
   967       qed
   968     } moreover {
   969       assume "a = y"
   970       with \<open>a < b\<close> have "y < b" by simp
   971       with \<open>a = y\<close> f_cont phi_cont \<open>e2 > 0\<close>
   972       have 1: "\<forall>\<^sub>F x in at y within {y..b}. dist (f x) (f y) < e2"
   973        and 2: "\<forall>\<^sub>F x in at y within {y..b}. dist (\<phi> x) (\<phi> y) < e2"
   974         by (auto simp: continuous_on_def tendsto_iff)
   975       have 3: "eventually (\<lambda>x. y < x) (at y within {y..b})"
   976         by (auto simp: eventually_at_filter)
   977       have 4: "eventually (\<lambda>x::real. x < b) (at y within {y..b})"
   978         using _ \<open>y < b\<close>
   979         by (rule order_tendstoD) (auto intro!: tendsto_eq_intros)
   980       from 1 2 3 4
   981       have eventually_le: "eventually (\<lambda>x. ?le x) (at y within {y .. b})"
   982       proof eventually_elim
   983         case (elim x1)
   984         have "norm (f x1 - f a) = norm (f x1 - f y)"
   985           by (simp add: \<open>a = y\<close>)
   986         also have "norm (f x1 - f y) \<le> e2"
   987           using elim \<open>a = y\<close> by (auto simp : dist_norm intro!:  less_imp_le)
   988         also have "\<dots> \<le> e2 + (\<phi> x1 - \<phi> a + e2 + e * (x1 - a))"
   989           using \<open>0 < e\<close> elim
   990           by (intro add_increasing2[OF add_nonneg_nonneg order.refl])
   991             (auto simp: \<open>a = y\<close> dist_norm intro!: mult_nonneg_nonneg)
   992         also have "\<dots> = \<phi> x1 - \<phi> a + e * (x1 - a) + e"
   993           by (simp add: e2_def)
   994         finally show "?le x1" .
   995       qed
   996       from this[unfolded eventually_at_topological] \<open>?le y\<close>
   997       obtain S
   998       where S: "open S" "y \<in> S" "\<And>x. x\<in>S \<Longrightarrow> x \<in> {y..b} \<Longrightarrow> ?le x"
   999         by metis
  1000       from \<open>open S\<close> obtain d where d: "\<And>x. dist x y < d \<Longrightarrow> x \<in> S" "d > 0"
  1001         by (force simp: dist_commute open_dist ball_def dest!: bspec[OF _ \<open>y \<in> S\<close>])
  1002       define d' where "d' = min b (y + (d/2))"
  1003       have "d' \<in> A"
  1004         unfolding A_def
  1005       proof safe
  1006         show "a \<le> d'" using \<open>a = y\<close> \<open>0 < d\<close> \<open>y < b\<close> by (simp add: d'_def)
  1007         show "d' \<le> b" by (simp add: d'_def)
  1008         fix x1
  1009         assume "x1 \<in> {a..<d'}"
  1010         hence "x1 \<in> S" "x1 \<in> {y..b}"
  1011           by (auto simp: \<open>a = y\<close> d'_def dist_real_def intro!: d )
  1012         thus "?le x1"
  1013           by (rule S)
  1014       qed
  1015       hence "d' \<le> y"
  1016         unfolding y_def
  1017         by (rule cSup_upper) simp
  1018       hence "y = b" using \<open>d > 0\<close> \<open>y < b\<close>
  1019         by (simp add: d'_def)
  1020     } ultimately have "y = b"
  1021       by auto
  1022     with le_y have "norm (f b - f a) \<le> \<phi> b - \<phi> a + e * (b - a + 1)"
  1023       by (simp add: algebra_simps)
  1024   } note * = this
  1025   {
  1026     fix e::real assume "e > 0"
  1027     hence "norm (f b - f a) \<le> \<phi> b - \<phi> a + e"
  1028       using *[of "e / (b - a + 1)"] \<open>a < b\<close> by simp
  1029   } thus ?thesis
  1030     by (rule field_le_epsilon)
  1031 qed
  1032 
  1033 lemma differentiable_bound:
  1034   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
  1035   assumes "convex s"
  1036     and "\<forall>x\<in>s. (f has_derivative f' x) (at x within s)"
  1037     and "\<forall>x\<in>s. onorm (f' x) \<le> B"
  1038     and x: "x \<in> s"
  1039     and y: "y \<in> s"
  1040   shows "norm (f x - f y) \<le> B * norm (x - y)"
  1041 proof -
  1042   let ?p = "\<lambda>u. x + u *\<^sub>R (y - x)"
  1043   let ?\<phi> = "\<lambda>h. h * B * norm (x - y)"
  1044   have *: "\<And>u. u\<in>{0..1} \<Longrightarrow> x + u *\<^sub>R (y - x) \<in> s"
  1045     using assms(1)[unfolded convex_alt,rule_format,OF x y]
  1046     unfolding scaleR_left_diff_distrib scaleR_right_diff_distrib
  1047     by (auto simp add: algebra_simps)
  1048   have 0: "continuous_on (?p ` {0..1}) f"
  1049     using *
  1050     unfolding continuous_on_eq_continuous_within
  1051     apply -
  1052     apply rule
  1053     apply (rule differentiable_imp_continuous_within)
  1054     unfolding differentiable_def
  1055     apply (rule_tac x="f' xa" in exI)
  1056     apply (rule has_derivative_within_subset)
  1057     apply (rule assms(2)[rule_format])
  1058     apply auto
  1059     done
  1060   from * have 1: "continuous_on {0 .. 1} (f \<circ> ?p)"
  1061     by (intro continuous_intros 0)+
  1062   {
  1063     fix u::real assume u: "u \<in>{0 <..< 1}"
  1064     let ?u = "?p u"
  1065     interpret linear "(f' ?u)"
  1066       using u by (auto intro!: has_derivative_linear assms(2)[rule_format] *)
  1067     have "(f \<circ> ?p has_derivative (f' ?u) \<circ> (\<lambda>u. 0 + u *\<^sub>R (y - x))) (at u within box 0 1)"
  1068       apply (rule diff_chain_within)
  1069       apply (rule derivative_intros)+
  1070       apply (rule has_derivative_within_subset)
  1071       apply (rule assms(2)[rule_format])
  1072       using u *
  1073       apply auto
  1074       done
  1075     hence "((f \<circ> ?p) has_vector_derivative f' ?u (y - x)) (at u)"
  1076       by (simp add: has_derivative_within_open[OF u open_greaterThanLessThan]
  1077         scaleR has_vector_derivative_def o_def)
  1078   } note 2 = this
  1079   {
  1080     have "continuous_on {0..1} ?\<phi>"
  1081       by (rule continuous_intros)+
  1082   } note 3 = this
  1083   {
  1084     fix u::real assume u: "u \<in>{0 <..< 1}"
  1085     have "(?\<phi> has_vector_derivative B * norm (x - y)) (at u)"
  1086       by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros)
  1087   } note 4 = this
  1088   {
  1089     fix u::real assume u: "u \<in>{0 <..< 1}"
  1090     let ?u = "?p u"
  1091     interpret bounded_linear "(f' ?u)"
  1092       using u by (auto intro!: has_derivative_bounded_linear assms(2)[rule_format] *)
  1093     have "norm (f' ?u (y - x)) \<le> onorm (f' ?u) * norm (y - x)"
  1094       by (rule onorm) fact
  1095     also have "onorm (f' ?u) \<le> B"
  1096       using u by (auto intro!: assms(3)[rule_format] *)
  1097     finally have "norm ((f' ?u) (y - x)) \<le> B * norm (x - y)"
  1098       by (simp add: mult_right_mono norm_minus_commute)
  1099   } note 5 = this
  1100   have "norm (f x - f y) = norm ((f \<circ> (\<lambda>u. x + u *\<^sub>R (y - x))) 1 - (f \<circ> (\<lambda>u. x + u *\<^sub>R (y - x))) 0)"
  1101     by (auto simp add: norm_minus_commute)
  1102   also
  1103   from differentiable_bound_general[OF zero_less_one 1, OF 3 2 4 5]
  1104   have "norm ((f \<circ> ?p) 1 - (f \<circ> ?p) 0) \<le> B * norm (x - y)"
  1105     by simp
  1106   finally show ?thesis .
  1107 qed
  1108 
  1109 lemma
  1110   differentiable_bound_segment:
  1111   fixes f::"'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
  1112   assumes "\<And>t. t \<in> {0..1} \<Longrightarrow> x0 + t *\<^sub>R a \<in> G"
  1113   assumes f': "\<And>x. x \<in> G \<Longrightarrow> (f has_derivative f' x) (at x within G)"
  1114   assumes B: "\<forall>x\<in>{0..1}. onorm (f' (x0 + x *\<^sub>R a)) \<le> B"
  1115   shows "norm (f (x0 + a) - f x0) \<le> norm a * B"
  1116 proof -
  1117   let ?G = "(\<lambda>x. x0 + x *\<^sub>R a) ` {0..1}"
  1118   have "?G = op + x0 ` (\<lambda>x. x *\<^sub>R a) ` {0..1}" by auto
  1119   also have "convex \<dots>"
  1120     by (intro convex_translation convex_scaled convex_real_interval)
  1121   finally have "convex ?G" .
  1122   moreover have "?G \<subseteq> G" "x0 \<in> ?G" "x0 + a \<in> ?G" using assms by (auto intro: image_eqI[where x=1])
  1123   ultimately show ?thesis
  1124     using has_derivative_subset[OF f' \<open>?G \<subseteq> G\<close>] B
  1125       differentiable_bound[of "(\<lambda>x. x0 + x *\<^sub>R a) ` {0..1}" f f' B "x0 + a" x0]
  1126     by (auto simp: ac_simps)
  1127 qed
  1128 
  1129 lemma differentiable_bound_linearization:
  1130   fixes f::"'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
  1131   assumes "\<And>t. t \<in> {0..1} \<Longrightarrow> a + t *\<^sub>R (b - a) \<in> S"
  1132   assumes f'[derivative_intros]: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)"
  1133   assumes B: "\<forall>x\<in>S. onorm (f' x - f' x0) \<le> B"
  1134   assumes "x0 \<in> S"
  1135   shows "norm (f b - f a - f' x0 (b - a)) \<le> norm (b - a) * B"
  1136 proof -
  1137   define g where [abs_def]: "g x = f x - f' x0 x" for x
  1138   have g: "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative (\<lambda>i. f' x i - f' x0 i)) (at x within S)"
  1139     unfolding g_def using assms
  1140     by (auto intro!: derivative_eq_intros
  1141       bounded_linear.has_derivative[OF has_derivative_bounded_linear, OF f'])
  1142   from B have B: "\<forall>x\<in>{0..1}. onorm (\<lambda>i. f' (a + x *\<^sub>R (b - a)) i - f' x0 i) \<le> B"
  1143      using assms by (auto simp: fun_diff_def)
  1144   from differentiable_bound_segment[OF assms(1) g B] \<open>x0 \<in> S\<close>
  1145   show ?thesis
  1146     by (simp add: g_def field_simps linear_diff[OF has_derivative_linear[OF f']])
  1147 qed
  1148 
  1149 text \<open>In particular.\<close>
  1150 
  1151 lemma has_derivative_zero_constant:
  1152   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
  1153   assumes "convex s"
  1154     and "\<And>x. x \<in> s \<Longrightarrow> (f has_derivative (\<lambda>h. 0)) (at x within s)"
  1155   shows "\<exists>c. \<forall>x\<in>s. f x = c"
  1156 proof -
  1157   { fix x y assume "x \<in> s" "y \<in> s"
  1158     then have "norm (f x - f y) \<le> 0 * norm (x - y)"
  1159       using assms by (intro differentiable_bound[of s]) (auto simp: onorm_zero)
  1160     then have "f x = f y"
  1161       by simp }
  1162   then show ?thesis
  1163     by metis
  1164 qed
  1165 
  1166 lemma has_field_derivative_zero_constant:
  1167   assumes "convex s" "\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative 0) (at x within s)"
  1168   shows   "\<exists>c. \<forall>x\<in>s. f (x) = (c :: 'a :: real_normed_field)"
  1169 proof (rule has_derivative_zero_constant)
  1170   have A: "op * 0 = (\<lambda>_. 0 :: 'a)" by (intro ext) simp
  1171   fix x assume "x \<in> s" thus "(f has_derivative (\<lambda>h. 0)) (at x within s)"
  1172     using assms(2)[of x] by (simp add: has_field_derivative_def A)
  1173 qed fact
  1174 
  1175 lemma has_derivative_zero_unique:
  1176   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
  1177   assumes "convex s"
  1178     and "\<And>x. x \<in> s \<Longrightarrow> (f has_derivative (\<lambda>h. 0)) (at x within s)"
  1179     and "x \<in> s" "y \<in> s"
  1180   shows "f x = f y"
  1181   using has_derivative_zero_constant[OF assms(1,2)] assms(3-) by force
  1182 
  1183 lemma has_derivative_zero_unique_connected:
  1184   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
  1185   assumes "open s" "connected s"
  1186   assumes f: "\<And>x. x \<in> s \<Longrightarrow> (f has_derivative (\<lambda>x. 0)) (at x)"
  1187   assumes "x \<in> s" "y \<in> s"
  1188   shows "f x = f y"
  1189 proof (rule connected_local_const[where f=f, OF \<open>connected s\<close> \<open>x\<in>s\<close> \<open>y\<in>s\<close>])
  1190   show "\<forall>a\<in>s. eventually (\<lambda>b. f a = f b) (at a within s)"
  1191   proof
  1192     fix a assume "a \<in> s"
  1193     with \<open>open s\<close> obtain e where "0 < e" "ball a e \<subseteq> s"
  1194       by (rule openE)
  1195     then have "\<exists>c. \<forall>x\<in>ball a e. f x = c"
  1196       by (intro has_derivative_zero_constant)
  1197          (auto simp: at_within_open[OF _ open_ball] f convex_ball)
  1198     with \<open>0<e\<close> have "\<forall>x\<in>ball a e. f a = f x"
  1199       by auto
  1200     then show "eventually (\<lambda>b. f a = f b) (at a within s)"
  1201       using \<open>0<e\<close> unfolding eventually_at_topological
  1202       by (intro exI[of _ "ball a e"]) auto
  1203   qed
  1204 qed
  1205 
  1206 subsection \<open>Differentiability of inverse function (most basic form)\<close>
  1207 
  1208 lemma has_derivative_inverse_basic:
  1209   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
  1210   assumes "(f has_derivative f') (at (g y))"
  1211     and "bounded_linear g'"
  1212     and "g' \<circ> f' = id"
  1213     and "continuous (at y) g"
  1214     and "open t"
  1215     and "y \<in> t"
  1216     and "\<forall>z\<in>t. f (g z) = z"
  1217   shows "(g has_derivative g') (at y)"
  1218 proof -
  1219   interpret f': bounded_linear f'
  1220     using assms unfolding has_derivative_def by auto
  1221   interpret g': bounded_linear g'
  1222     using assms by auto
  1223   obtain C where C: "0 < C" "\<And>x. norm (g' x) \<le> norm x * C"
  1224     using bounded_linear.pos_bounded[OF assms(2)] by blast
  1225   have lem1: "\<forall>e>0. \<exists>d>0. \<forall>z.
  1226     norm (z - y) < d \<longrightarrow> norm (g z - g y - g'(z - y)) \<le> e * norm (g z - g y)"
  1227   proof (rule, rule)
  1228     fix e :: real
  1229     assume "e > 0"
  1230     with C(1) have *: "e / C > 0" by auto
  1231     obtain d0 where d0:
  1232         "0 < d0"
  1233         "\<forall>ya. norm (ya - g y) < d0 \<longrightarrow> norm (f ya - f (g y) - f' (ya - g y)) \<le> e / C * norm (ya - g y)"
  1234       using assms(1)
  1235       unfolding has_derivative_at_alt
  1236       using * by blast
  1237     obtain d1 where d1:
  1238         "0 < d1"
  1239         "\<forall>x. 0 < dist x y \<and> dist x y < d1 \<longrightarrow> dist (g x) (g y) < d0"
  1240       using assms(4)
  1241       unfolding continuous_at Lim_at
  1242       using d0(1) by blast
  1243     obtain d2 where d2:
  1244         "0 < d2"
  1245         "\<forall>ya. dist ya y < d2 \<longrightarrow> ya \<in> t"
  1246       using assms(5)
  1247       unfolding open_dist
  1248       using assms(6) by blast
  1249     obtain d where d: "0 < d" "d < d1" "d < d2"
  1250       using real_lbound_gt_zero[OF d1(1) d2(1)] by blast
  1251     then show "\<exists>d>0. \<forall>z. norm (z - y) < d \<longrightarrow> norm (g z - g y - g' (z - y)) \<le> e * norm (g z - g y)"
  1252       apply (rule_tac x=d in exI)
  1253       apply rule
  1254       defer
  1255       apply rule
  1256       apply rule
  1257     proof -
  1258       fix z
  1259       assume as: "norm (z - y) < d"
  1260       then have "z \<in> t"
  1261         using d2 d unfolding dist_norm by auto
  1262       have "norm (g z - g y - g' (z - y)) \<le> norm (g' (f (g z) - y - f' (g z - g y)))"
  1263         unfolding g'.diff f'.diff
  1264         unfolding assms(3)[unfolded o_def id_def, THEN fun_cong]
  1265         unfolding assms(7)[rule_format,OF \<open>z\<in>t\<close>]
  1266         apply (subst norm_minus_cancel[symmetric])
  1267         apply auto
  1268         done
  1269       also have "\<dots> \<le> norm (f (g z) - y - f' (g z - g y)) * C"
  1270         by (rule C(2))
  1271       also have "\<dots> \<le> (e / C) * norm (g z - g y) * C"
  1272         apply (rule mult_right_mono)
  1273         apply (rule d0(2)[rule_format,unfolded assms(7)[rule_format,OF \<open>y\<in>t\<close>]])
  1274         apply (cases "z = y")
  1275         defer
  1276         apply (rule d1(2)[unfolded dist_norm,rule_format])
  1277         using as d C d0
  1278         apply auto
  1279         done
  1280       also have "\<dots> \<le> e * norm (g z - g y)"
  1281         using C by (auto simp add: field_simps)
  1282       finally show "norm (g z - g y - g' (z - y)) \<le> e * norm (g z - g y)"
  1283         by simp
  1284     qed auto
  1285   qed
  1286   have *: "(0::real) < 1 / 2"
  1287     by auto
  1288   obtain d where d:
  1289       "0 < d"
  1290       "\<forall>z. norm (z - y) < d \<longrightarrow> norm (g z - g y - g' (z - y)) \<le> 1 / 2 * norm (g z - g y)"
  1291     using lem1 * by blast
  1292   define B where "B = C * 2"
  1293   have "B > 0"
  1294     unfolding B_def using C by auto
  1295   have lem2: "norm (g z - g y) \<le> B * norm (z - y)" if z: "norm(z - y) < d" for z
  1296   proof -
  1297     have "norm (g z - g y) \<le> norm(g' (z - y)) + norm ((g z - g y) - g'(z - y))"
  1298       by (rule norm_triangle_sub)
  1299     also have "\<dots> \<le> norm (g' (z - y)) + 1 / 2 * norm (g z - g y)"
  1300       apply (rule add_left_mono)
  1301       using d and z
  1302       apply auto
  1303       done
  1304     also have "\<dots> \<le> norm (z - y) * C + 1 / 2 * norm (g z - g y)"
  1305       apply (rule add_right_mono)
  1306       using C
  1307       apply auto
  1308       done
  1309     finally show "norm (g z - g y) \<le> B * norm (z - y)"
  1310       unfolding B_def
  1311       by (auto simp add: field_simps)
  1312   qed
  1313   show ?thesis
  1314     unfolding has_derivative_at_alt
  1315     apply rule
  1316     apply (rule assms)
  1317     apply rule
  1318     apply rule
  1319   proof -
  1320     fix e :: real
  1321     assume "e > 0"
  1322     then have *: "e / B > 0" by (metis \<open>B > 0\<close> divide_pos_pos)
  1323     obtain d' where d':
  1324         "0 < d'"
  1325         "\<forall>z. norm (z - y) < d' \<longrightarrow> norm (g z - g y - g' (z - y)) \<le> e / B * norm (g z - g y)"
  1326       using lem1 * by blast
  1327     obtain k where k: "0 < k" "k < d" "k < d'"
  1328       using real_lbound_gt_zero[OF d(1) d'(1)] by blast
  1329     show "\<exists>d>0. \<forall>ya. norm (ya - y) < d \<longrightarrow> norm (g ya - g y - g' (ya - y)) \<le> e * norm (ya - y)"
  1330       apply (rule_tac x=k in exI)
  1331       apply auto
  1332     proof -
  1333       fix z
  1334       assume as: "norm (z - y) < k"
  1335       then have "norm (g z - g y - g' (z - y)) \<le> e / B * norm(g z - g y)"
  1336         using d' k by auto
  1337       also have "\<dots> \<le> e * norm (z - y)"
  1338         unfolding times_divide_eq_left pos_divide_le_eq[OF \<open>B>0\<close>]
  1339         using lem2[of z]
  1340         using k as using \<open>e > 0\<close>
  1341         by (auto simp add: field_simps)
  1342       finally show "norm (g z - g y - g' (z - y)) \<le> e * norm (z - y)"
  1343         by simp
  1344     qed(insert k, auto)
  1345   qed
  1346 qed
  1347 
  1348 text \<open>Simply rewrite that based on the domain point x.\<close>
  1349 
  1350 lemma has_derivative_inverse_basic_x:
  1351   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
  1352   assumes "(f has_derivative f') (at x)"
  1353     and "bounded_linear g'"
  1354     and "g' \<circ> f' = id"
  1355     and "continuous (at (f x)) g"
  1356     and "g (f x) = x"
  1357     and "open t"
  1358     and "f x \<in> t"
  1359     and "\<forall>y\<in>t. f (g y) = y"
  1360   shows "(g has_derivative g') (at (f x))"
  1361   apply (rule has_derivative_inverse_basic)
  1362   using assms
  1363   apply auto
  1364   done
  1365 
  1366 text \<open>This is the version in Dieudonne', assuming continuity of f and g.\<close>
  1367 
  1368 lemma has_derivative_inverse_dieudonne:
  1369   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
  1370   assumes "open s"
  1371     and "open (f ` s)"
  1372     and "continuous_on s f"
  1373     and "continuous_on (f ` s) g"
  1374     and "\<forall>x\<in>s. g (f x) = x"
  1375     and "x \<in> s"
  1376     and "(f has_derivative f') (at x)"
  1377     and "bounded_linear g'"
  1378     and "g' \<circ> f' = id"
  1379   shows "(g has_derivative g') (at (f x))"
  1380   apply (rule has_derivative_inverse_basic_x[OF assms(7-9) _ _ assms(2)])
  1381   using assms(3-6)
  1382   unfolding continuous_on_eq_continuous_at[OF assms(1)] continuous_on_eq_continuous_at[OF assms(2)]
  1383   apply auto
  1384   done
  1385 
  1386 text \<open>Here's the simplest way of not assuming much about g.\<close>
  1387 
  1388 lemma has_derivative_inverse:
  1389   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
  1390   assumes "compact s"
  1391     and "x \<in> s"
  1392     and "f x \<in> interior (f ` s)"
  1393     and "continuous_on s f"
  1394     and "\<forall>y\<in>s. g (f y) = y"
  1395     and "(f has_derivative f') (at x)"
  1396     and "bounded_linear g'"
  1397     and "g' \<circ> f' = id"
  1398   shows "(g has_derivative g') (at (f x))"
  1399 proof -
  1400   {
  1401     fix y
  1402     assume "y \<in> interior (f ` s)"
  1403     then obtain x where "x \<in> s" and *: "y = f x"
  1404       unfolding image_iff
  1405       using interior_subset
  1406       by auto
  1407     have "f (g y) = y"
  1408       unfolding * and assms(5)[rule_format,OF \<open>x\<in>s\<close>] ..
  1409   } note * = this
  1410   show ?thesis
  1411     apply (rule has_derivative_inverse_basic_x[OF assms(6-8)])
  1412     apply (rule continuous_on_interior[OF _ assms(3)])
  1413     apply (rule continuous_on_inv[OF assms(4,1)])
  1414     apply (rule assms(2,5) assms(5)[rule_format] open_interior assms(3))+
  1415     apply (metis *)
  1416     done
  1417 qed
  1418 
  1419 
  1420 subsection \<open>Proving surjectivity via Brouwer fixpoint theorem\<close>
  1421 
  1422 lemma brouwer_surjective:
  1423   fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
  1424   assumes "compact t"
  1425     and "convex t"
  1426     and "t \<noteq> {}"
  1427     and "continuous_on t f"
  1428     and "\<forall>x\<in>s. \<forall>y\<in>t. x + (y - f y) \<in> t"
  1429     and "x \<in> s"
  1430   shows "\<exists>y\<in>t. f y = x"
  1431 proof -
  1432   have *: "\<And>x y. f y = x \<longleftrightarrow> x + (y - f y) = y"
  1433     by (auto simp add: algebra_simps)
  1434   show ?thesis
  1435     unfolding *
  1436     apply (rule brouwer[OF assms(1-3), of "\<lambda>y. x + (y - f y)"])
  1437     apply (rule continuous_intros assms)+
  1438     using assms(4-6)
  1439     apply auto
  1440     done
  1441 qed
  1442 
  1443 lemma brouwer_surjective_cball:
  1444   fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
  1445   assumes "e > 0"
  1446     and "continuous_on (cball a e) f"
  1447     and "\<forall>x\<in>s. \<forall>y\<in>cball a e. x + (y - f y) \<in> cball a e"
  1448     and "x \<in> s"
  1449   shows "\<exists>y\<in>cball a e. f y = x"
  1450   apply (rule brouwer_surjective)
  1451   apply (rule compact_cball convex_cball)+
  1452   unfolding cball_eq_empty
  1453   using assms
  1454   apply auto
  1455   done
  1456 
  1457 text \<open>See Sussmann: "Multidifferential calculus", Theorem 2.1.1\<close>
  1458 
  1459 lemma sussmann_open_mapping:
  1460   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
  1461   assumes "open s"
  1462     and "continuous_on s f"
  1463     and "x \<in> s"
  1464     and "(f has_derivative f') (at x)"
  1465     and "bounded_linear g'" "f' \<circ> g' = id"
  1466     and "t \<subseteq> s"
  1467     and "x \<in> interior t"
  1468   shows "f x \<in> interior (f ` t)"
  1469 proof -
  1470   interpret f': bounded_linear f'
  1471     using assms
  1472     unfolding has_derivative_def
  1473     by auto
  1474   interpret g': bounded_linear g'
  1475     using assms
  1476     by auto
  1477   obtain B where B: "0 < B" "\<forall>x. norm (g' x) \<le> norm x * B"
  1478     using bounded_linear.pos_bounded[OF assms(5)] by blast
  1479   hence *: "1 / (2 * B) > 0" by auto
  1480   obtain e0 where e0:
  1481       "0 < e0"
  1482       "\<forall>y. norm (y - x) < e0 \<longrightarrow> norm (f y - f x - f' (y - x)) \<le> 1 / (2 * B) * norm (y - x)"
  1483     using assms(4)
  1484     unfolding has_derivative_at_alt
  1485     using * by blast
  1486   obtain e1 where e1: "0 < e1" "cball x e1 \<subseteq> t"
  1487     using assms(8)
  1488     unfolding mem_interior_cball
  1489     by blast
  1490   have *: "0 < e0 / B" "0 < e1 / B" using e0 e1 B by auto
  1491   obtain e where e: "0 < e" "e < e0 / B" "e < e1 / B"
  1492     using real_lbound_gt_zero[OF *] by blast
  1493   have "\<forall>z\<in>cball (f x) (e / 2). \<exists>y\<in>cball (f x) e. f (x + g' (y - f x)) = z"
  1494     apply rule
  1495     apply (rule brouwer_surjective_cball[where s="cball (f x) (e/2)"])
  1496     prefer 3
  1497     apply rule
  1498     apply rule
  1499   proof-
  1500     show "continuous_on (cball (f x) e) (\<lambda>y. f (x + g' (y - f x)))"
  1501       unfolding g'.diff
  1502       apply (rule continuous_on_compose[of _ _ f, unfolded o_def])
  1503       apply (rule continuous_intros linear_continuous_on[OF assms(5)])+
  1504       apply (rule continuous_on_subset[OF assms(2)])
  1505       apply rule
  1506       apply (unfold image_iff)
  1507       apply (erule bexE)
  1508     proof-
  1509       fix y z
  1510       assume as: "y \<in>cball (f x) e" "z = x + (g' y - g' (f x))"
  1511       have "dist x z = norm (g' (f x) - g' y)"
  1512         unfolding as(2) and dist_norm by auto
  1513       also have "\<dots> \<le> norm (f x - y) * B"
  1514         unfolding g'.diff[symmetric]
  1515         using B
  1516         by auto
  1517       also have "\<dots> \<le> e * B"
  1518         using as(1)[unfolded mem_cball dist_norm]
  1519         using B
  1520         by auto
  1521       also have "\<dots> \<le> e1"
  1522         using e
  1523         unfolding less_divide_eq
  1524         using B
  1525         by auto
  1526       finally have "z \<in> cball x e1"
  1527         unfolding mem_cball
  1528         by force
  1529       then show "z \<in> s"
  1530         using e1 assms(7) by auto
  1531     qed
  1532   next
  1533     fix y z
  1534     assume as: "y \<in> cball (f x) (e / 2)" "z \<in> cball (f x) e"
  1535     have "norm (g' (z - f x)) \<le> norm (z - f x) * B"
  1536       using B by auto
  1537     also have "\<dots> \<le> e * B"
  1538       apply (rule mult_right_mono)
  1539       using as(2)[unfolded mem_cball dist_norm] and B
  1540       unfolding norm_minus_commute
  1541       apply auto
  1542       done
  1543     also have "\<dots> < e0"
  1544       using e and B
  1545       unfolding less_divide_eq
  1546       by auto
  1547     finally have *: "norm (x + g' (z - f x) - x) < e0"
  1548       by auto
  1549     have **: "f x + f' (x + g' (z - f x) - x) = z"
  1550       using assms(6)[unfolded o_def id_def,THEN cong]
  1551       by auto
  1552     have "norm (f x - (y + (z - f (x + g' (z - f x))))) \<le>
  1553         norm (f (x + g' (z - f x)) - z) + norm (f x - y)"
  1554       using norm_triangle_ineq[of "f (x + g'(z - f x)) - z" "f x - y"]
  1555       by (auto simp add: algebra_simps)
  1556     also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + norm (f x - y)"
  1557       using e0(2)[rule_format, OF *]
  1558       by (simp only: algebra_simps **) auto
  1559     also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + e/2"
  1560       using as(1)[unfolded mem_cball dist_norm]
  1561       by auto
  1562     also have "\<dots> \<le> 1 / (B * 2) * B * norm (z - f x) + e/2"
  1563       using * and B
  1564       by (auto simp add: field_simps)
  1565     also have "\<dots> \<le> 1 / 2 * norm (z - f x) + e/2"
  1566       by auto
  1567     also have "\<dots> \<le> e/2 + e/2"
  1568       apply (rule add_right_mono)
  1569       using as(2)[unfolded mem_cball dist_norm]
  1570       unfolding norm_minus_commute
  1571       apply auto
  1572       done
  1573     finally show "y + (z - f (x + g' (z - f x))) \<in> cball (f x) e"
  1574       unfolding mem_cball dist_norm
  1575       by auto
  1576   qed (insert e, auto) note lem = this
  1577   show ?thesis
  1578     unfolding mem_interior
  1579     apply (rule_tac x="e/2" in exI)
  1580     apply rule
  1581     apply (rule divide_pos_pos)
  1582     prefer 3
  1583   proof
  1584     fix y
  1585     assume "y \<in> ball (f x) (e / 2)"
  1586     then have *: "y \<in> cball (f x) (e / 2)"
  1587       by auto
  1588     obtain z where z: "z \<in> cball (f x) e" "f (x + g' (z - f x)) = y"
  1589       using lem * by blast
  1590     then have "norm (g' (z - f x)) \<le> norm (z - f x) * B"
  1591       using B
  1592       by (auto simp add: field_simps)
  1593     also have "\<dots> \<le> e * B"
  1594       apply (rule mult_right_mono)
  1595       using z(1)
  1596       unfolding mem_cball dist_norm norm_minus_commute
  1597       using B
  1598       apply auto
  1599       done
  1600     also have "\<dots> \<le> e1"
  1601       using e B unfolding less_divide_eq by auto
  1602     finally have "x + g'(z - f x) \<in> t"
  1603       apply -
  1604       apply (rule e1(2)[unfolded subset_eq,rule_format])
  1605       unfolding mem_cball dist_norm
  1606       apply auto
  1607       done
  1608     then show "y \<in> f ` t"
  1609       using z by auto
  1610   qed (insert e, auto)
  1611 qed
  1612 
  1613 text \<open>Hence the following eccentric variant of the inverse function theorem.
  1614   This has no continuity assumptions, but we do need the inverse function.
  1615   We could put \<open>f' \<circ> g = I\<close> but this happens to fit with the minimal linear
  1616   algebra theory I've set up so far.\<close>
  1617 
  1618 (* move  before left_inverse_linear in Euclidean_Space*)
  1619 
  1620 lemma right_inverse_linear:
  1621   fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
  1622   assumes lf: "linear f"
  1623     and gf: "f \<circ> g = id"
  1624   shows "linear g"
  1625 proof -
  1626   from gf have fi: "surj f"
  1627     by (auto simp add: surj_def o_def id_def) metis
  1628   from linear_surjective_isomorphism[OF lf fi]
  1629   obtain h:: "'a \<Rightarrow> 'a" where h: "linear h" "\<forall>x. h (f x) = x" "\<forall>x. f (h x) = x"
  1630     by blast
  1631   have "h = g"
  1632     apply (rule ext)
  1633     using gf h(2,3)
  1634     apply (simp add: o_def id_def fun_eq_iff)
  1635     apply metis
  1636     done
  1637   with h(1) show ?thesis by blast
  1638 qed
  1639 
  1640 lemma has_derivative_inverse_strong:
  1641   fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
  1642   assumes "open s"
  1643     and "x \<in> s"
  1644     and "continuous_on s f"
  1645     and "\<forall>x\<in>s. g (f x) = x"
  1646     and "(f has_derivative f') (at x)"
  1647     and "f' \<circ> g' = id"
  1648   shows "(g has_derivative g') (at (f x))"
  1649 proof -
  1650   have linf: "bounded_linear f'"
  1651     using assms(5) unfolding has_derivative_def by auto
  1652   then have ling: "bounded_linear g'"
  1653     unfolding linear_conv_bounded_linear[symmetric]
  1654     apply -
  1655     apply (rule right_inverse_linear)
  1656     using assms(6)
  1657     apply auto
  1658     done
  1659   moreover have "g' \<circ> f' = id"
  1660     using assms(6) linf ling
  1661     unfolding linear_conv_bounded_linear[symmetric]
  1662     using linear_inverse_left
  1663     by auto
  1664   moreover have *:"\<forall>t\<subseteq>s. x \<in> interior t \<longrightarrow> f x \<in> interior (f ` t)"
  1665     apply clarify
  1666     apply (rule sussmann_open_mapping)
  1667     apply (rule assms ling)+
  1668     apply auto
  1669     done
  1670   have "continuous (at (f x)) g"
  1671     unfolding continuous_at Lim_at
  1672   proof (rule, rule)
  1673     fix e :: real
  1674     assume "e > 0"
  1675     then have "f x \<in> interior (f ` (ball x e \<inter> s))"
  1676       using *[rule_format,of "ball x e \<inter> s"] \<open>x \<in> s\<close>
  1677       by (auto simp add: interior_open[OF open_ball] interior_open[OF assms(1)])
  1678     then obtain d where d: "0 < d" "ball (f x) d \<subseteq> f ` (ball x e \<inter> s)"
  1679       unfolding mem_interior by blast
  1680     show "\<exists>d>0. \<forall>y. 0 < dist y (f x) \<and> dist y (f x) < d \<longrightarrow> dist (g y) (g (f x)) < e"
  1681       apply (rule_tac x=d in exI)
  1682       apply rule
  1683       apply (rule d(1))
  1684       apply rule
  1685       apply rule
  1686     proof -
  1687       fix y
  1688       assume "0 < dist y (f x) \<and> dist y (f x) < d"
  1689       then have "g y \<in> g ` f ` (ball x e \<inter> s)"
  1690         using d(2)[unfolded subset_eq,THEN bspec[where x=y]]
  1691         by (auto simp add: dist_commute)
  1692       then have "g y \<in> ball x e \<inter> s"
  1693         using assms(4) by auto
  1694       then show "dist (g y) (g (f x)) < e"
  1695         using assms(4)[rule_format,OF \<open>x \<in> s\<close>]
  1696         by (auto simp add: dist_commute)
  1697     qed
  1698   qed
  1699   moreover have "f x \<in> interior (f ` s)"
  1700     apply (rule sussmann_open_mapping)
  1701     apply (rule assms ling)+
  1702     using interior_open[OF assms(1)] and \<open>x \<in> s\<close>
  1703     apply auto
  1704     done
  1705   moreover have "f (g y) = y" if "y \<in> interior (f ` s)" for y
  1706   proof -
  1707     from that have "y \<in> f ` s"
  1708       using interior_subset by auto
  1709     then obtain z where "z \<in> s" "y = f z" unfolding image_iff ..
  1710     then show ?thesis
  1711       using assms(4) by auto
  1712   qed
  1713   ultimately show ?thesis using assms
  1714     by (metis has_derivative_inverse_basic_x open_interior)
  1715 qed
  1716 
  1717 text \<open>A rewrite based on the other domain.\<close>
  1718 
  1719 lemma has_derivative_inverse_strong_x:
  1720   fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
  1721   assumes "open s"
  1722     and "g y \<in> s"
  1723     and "continuous_on s f"
  1724     and "\<forall>x\<in>s. g (f x) = x"
  1725     and "(f has_derivative f') (at (g y))"
  1726     and "f' \<circ> g' = id"
  1727     and "f (g y) = y"
  1728   shows "(g has_derivative g') (at y)"
  1729   using has_derivative_inverse_strong[OF assms(1-6)]
  1730   unfolding assms(7)
  1731   by simp
  1732 
  1733 text \<open>On a region.\<close>
  1734 
  1735 lemma has_derivative_inverse_on:
  1736   fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
  1737   assumes "open s"
  1738     and "\<forall>x\<in>s. (f has_derivative f'(x)) (at x)"
  1739     and "\<forall>x\<in>s. g (f x) = x"
  1740     and "f' x \<circ> g' x = id"
  1741     and "x \<in> s"
  1742   shows "(g has_derivative g'(x)) (at (f x))"
  1743   apply (rule has_derivative_inverse_strong[where g'="g' x" and f=f])
  1744   apply (rule assms)+
  1745   unfolding continuous_on_eq_continuous_at[OF assms(1)]
  1746   apply rule
  1747   apply (rule differentiable_imp_continuous_within)
  1748   unfolding differentiable_def
  1749   using assms
  1750   apply auto
  1751   done
  1752 
  1753 text \<open>Invertible derivative continous at a point implies local
  1754 injectivity. It's only for this we need continuity of the derivative,
  1755 except of course if we want the fact that the inverse derivative is
  1756 also continuous. So if we know for some other reason that the inverse
  1757 function exists, it's OK.\<close>
  1758 
  1759 proposition has_derivative_locally_injective:
  1760   fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
  1761   assumes "a \<in> s"
  1762       and "open s"
  1763       and "bounded_linear g'"
  1764       and "g' \<circ> f' a = id"
  1765       and "\<And>x. x \<in> s \<Longrightarrow> (f has_derivative f' x) (at x)"
  1766       and "\<And>e. e > 0 \<Longrightarrow> \<exists>d>0. \<forall>x. dist a x < d \<longrightarrow> onorm (\<lambda>v. f' x v - f' a v) < e"
  1767   obtains r where "r > 0" "ball a r \<subseteq> s" "inj_on f (ball a r)"
  1768 proof -
  1769   interpret bounded_linear g'
  1770     using assms by auto
  1771   note f'g' = assms(4)[unfolded id_def o_def,THEN cong]
  1772   have "g' (f' a (\<Sum>Basis)) = (\<Sum>Basis)" "(\<Sum>Basis) \<noteq> (0::'n)"
  1773     defer
  1774     apply (subst euclidean_eq_iff)
  1775     using f'g'
  1776     apply auto
  1777     done
  1778   then have *: "0 < onorm g'"
  1779     unfolding onorm_pos_lt[OF assms(3)]
  1780     by fastforce
  1781   define k where "k = 1 / onorm g' / 2"
  1782   have *: "k > 0"
  1783     unfolding k_def using * by auto
  1784   obtain d1 where d1:
  1785       "0 < d1"
  1786       "\<And>x. dist a x < d1 \<Longrightarrow> onorm (\<lambda>v. f' x v - f' a v) < k"
  1787     using assms(6) * by blast
  1788   from \<open>open s\<close> obtain d2 where "d2 > 0" "ball a d2 \<subseteq> s"
  1789     using \<open>a\<in>s\<close> ..
  1790   obtain d2 where "d2 > 0" "ball a d2 \<subseteq> s"
  1791     using assms(2,1) ..
  1792   obtain d2 where d2: "0 < d2" "ball a d2 \<subseteq> s"
  1793     using assms(2)
  1794     unfolding open_contains_ball
  1795     using \<open>a\<in>s\<close> by blast
  1796   obtain d where d: "0 < d" "d < d1" "d < d2"
  1797     using real_lbound_gt_zero[OF d1(1) d2(1)] by blast
  1798   show ?thesis
  1799   proof
  1800     show "0 < d" by (fact d)
  1801     show "ball a d \<subseteq> s"
  1802       using \<open>d < d2\<close> \<open>ball a d2 \<subseteq> s\<close> by auto
  1803     show "inj_on f (ball a d)"
  1804     unfolding inj_on_def
  1805     proof (intro strip)
  1806       fix x y
  1807       assume as: "x \<in> ball a d" "y \<in> ball a d" "f x = f y"
  1808       define ph where [abs_def]: "ph w = w - g' (f w - f x)" for w
  1809       have ph':"ph = g' \<circ> (\<lambda>w. f' a w - (f w - f x))"
  1810         unfolding ph_def o_def
  1811         unfolding diff
  1812         using f'g'
  1813         by (auto simp: algebra_simps)
  1814       have "norm (ph x - ph y) \<le> (1 / 2) * norm (x - y)"
  1815         apply (rule differentiable_bound[OF convex_ball _ _ as(1-2), where f'="\<lambda>x v. v - g'(f' x v)"])
  1816         apply (rule_tac[!] ballI)
  1817       proof -
  1818         fix u
  1819         assume u: "u \<in> ball a d"
  1820         then have "u \<in> s"
  1821           using d d2 by auto
  1822         have *: "(\<lambda>v. v - g' (f' u v)) = g' \<circ> (\<lambda>w. f' a w - f' u w)"
  1823           unfolding o_def and diff
  1824           using f'g' by auto
  1825         show "(ph has_derivative (\<lambda>v. v - g' (f' u v))) (at u within ball a d)"
  1826           unfolding ph' *
  1827           apply (simp add: comp_def)
  1828           apply (rule bounded_linear.has_derivative[OF assms(3)])
  1829           apply (rule derivative_intros)
  1830           defer
  1831           apply (rule has_derivative_sub[where g'="\<lambda>x.0",unfolded diff_0_right])
  1832           apply (rule has_derivative_at_within)
  1833           using assms(5) and \<open>u \<in> s\<close> \<open>a \<in> s\<close>
  1834           apply (auto intro!: derivative_intros bounded_linear.has_derivative[of _ "\<lambda>x. x"] has_derivative_bounded_linear)
  1835           done
  1836         have **: "bounded_linear (\<lambda>x. f' u x - f' a x)" "bounded_linear (\<lambda>x. f' a x - f' u x)"
  1837           apply (rule_tac[!] bounded_linear_sub)
  1838           apply (rule_tac[!] has_derivative_bounded_linear)
  1839           using assms(5) \<open>u \<in> s\<close> \<open>a \<in> s\<close>
  1840           apply auto
  1841           done
  1842         have "onorm (\<lambda>v. v - g' (f' u v)) \<le> onorm g' * onorm (\<lambda>w. f' a w - f' u w)"
  1843           unfolding *
  1844           apply (rule onorm_compose)
  1845           apply (rule assms(3) **)+
  1846           done
  1847         also have "\<dots> \<le> onorm g' * k"
  1848           apply (rule mult_left_mono)
  1849           using d1(2)[of u]
  1850           using onorm_neg[where f="\<lambda>x. f' u x - f' a x"]
  1851           using d and u and onorm_pos_le[OF assms(3)]
  1852           apply (auto simp: algebra_simps)
  1853           done
  1854         also have "\<dots> \<le> 1 / 2"
  1855           unfolding k_def by auto
  1856         finally show "onorm (\<lambda>v. v - g' (f' u v)) \<le> 1 / 2" .
  1857       qed
  1858       moreover have "norm (ph y - ph x) = norm (y - x)"
  1859         apply (rule arg_cong[where f=norm])
  1860         unfolding ph_def
  1861         using diff
  1862         unfolding as
  1863         apply auto
  1864         done
  1865       ultimately show "x = y"
  1866         unfolding norm_minus_commute by auto
  1867     qed
  1868   qed
  1869 qed
  1870 
  1871 
  1872 subsection \<open>Uniformly convergent sequence of derivatives\<close>
  1873 
  1874 lemma has_derivative_sequence_lipschitz_lemma:
  1875   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
  1876   assumes "convex s"
  1877     and "\<forall>n. \<forall>x\<in>s. ((f n) has_derivative (f' n x)) (at x within s)"
  1878     and "\<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
  1879     and "0 \<le> e"
  1880   shows "\<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s. norm ((f m x - f n x) - (f m y - f n y)) \<le> 2 * e * norm (x - y)"
  1881 proof rule+
  1882   fix m n x y
  1883   assume as: "N \<le> m" "N \<le> n" "x \<in> s" "y \<in> s"
  1884   show "norm ((f m x - f n x) - (f m y - f n y)) \<le> 2 * e * norm (x - y)"
  1885     apply (rule differentiable_bound[where f'="\<lambda>x h. f' m x h - f' n x h", OF assms(1) _ _ as(3-4)])
  1886     apply (rule_tac[!] ballI)
  1887   proof -
  1888     fix x
  1889     assume "x \<in> s"
  1890     show "((\<lambda>a. f m a - f n a) has_derivative (\<lambda>h. f' m x h - f' n x h)) (at x within s)"
  1891       by (rule derivative_intros assms(2)[rule_format] \<open>x\<in>s\<close>)+
  1892     show "onorm (\<lambda>h. f' m x h - f' n x h) \<le> 2 * e"
  1893     proof (rule onorm_bound)
  1894       fix h
  1895       have "norm (f' m x h - f' n x h) \<le> norm (f' m x h - g' x h) + norm (f' n x h - g' x h)"
  1896         using norm_triangle_ineq[of "f' m x h - g' x h" "- f' n x h + g' x h"]
  1897         unfolding norm_minus_commute
  1898         by (auto simp add: algebra_simps)
  1899       also have "\<dots> \<le> e * norm h + e * norm h"
  1900         using assms(3)[rule_format,OF \<open>N \<le> m\<close> \<open>x \<in> s\<close>, of h]
  1901         using assms(3)[rule_format,OF \<open>N \<le> n\<close> \<open>x \<in> s\<close>, of h]
  1902         by (auto simp add: field_simps)
  1903       finally show "norm (f' m x h - f' n x h) \<le> 2 * e * norm h"
  1904         by auto
  1905     qed (simp add: \<open>0 \<le> e\<close>)
  1906   qed
  1907 qed
  1908 
  1909 lemma has_derivative_sequence_lipschitz:
  1910   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
  1911   assumes "convex s"
  1912     and "\<forall>n. \<forall>x\<in>s. ((f n) has_derivative (f' n x)) (at x within s)"
  1913     and "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
  1914   shows "\<forall>e>0. \<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s.
  1915     norm ((f m x - f n x) - (f m y - f n y)) \<le> e * norm (x - y)"
  1916 proof (rule, rule)
  1917   fix e :: real
  1918   assume "e > 0"
  1919   then have *: "2 * (1/2* e) = e" "1/2 * e >0"
  1920     by auto
  1921   obtain N where "\<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> 1 / 2 * e * norm h"
  1922     using assms(3) *(2) by blast
  1923   then show "\<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s. norm (f m x - f n x - (f m y - f n y)) \<le> e * norm (x - y)"
  1924     apply (rule_tac x=N in exI)
  1925     apply (rule has_derivative_sequence_lipschitz_lemma[where e="1/2 *e", unfolded *])
  1926     using assms \<open>e > 0\<close>
  1927     apply auto
  1928     done
  1929 qed
  1930 
  1931 lemma has_derivative_sequence:
  1932   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::banach"
  1933   assumes "convex s"
  1934     and "\<forall>n. \<forall>x\<in>s. ((f n) has_derivative (f' n x)) (at x within s)"
  1935     and "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
  1936     and "x0 \<in> s"
  1937     and "((\<lambda>n. f n x0) \<longlongrightarrow> l) sequentially"
  1938   shows "\<exists>g. \<forall>x\<in>s. ((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially \<and> (g has_derivative g'(x)) (at x within s)"
  1939 proof -
  1940   have lem1: "\<forall>e>0. \<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s.
  1941       norm ((f m x - f n x) - (f m y - f n y)) \<le> e * norm (x - y)"
  1942     using assms(1,2,3) by (rule has_derivative_sequence_lipschitz)
  1943   have "\<exists>g. \<forall>x\<in>s. ((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially"
  1944     apply (rule bchoice)
  1945     unfolding convergent_eq_cauchy
  1946   proof
  1947     fix x
  1948     assume "x \<in> s"
  1949     show "Cauchy (\<lambda>n. f n x)"
  1950     proof (cases "x = x0")
  1951       case True
  1952       then show ?thesis
  1953         using LIMSEQ_imp_Cauchy[OF assms(5)] by auto
  1954     next
  1955       case False
  1956       show ?thesis
  1957         unfolding Cauchy_def
  1958       proof (rule, rule)
  1959         fix e :: real
  1960         assume "e > 0"
  1961         hence *: "e / 2 > 0" "e / 2 / norm (x - x0) > 0" using False by auto
  1962         obtain M where M: "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x0) (f n x0) < e / 2"
  1963           using LIMSEQ_imp_Cauchy[OF assms(5)]
  1964           unfolding Cauchy_def
  1965           using *(1) by blast
  1966         obtain N where N:
  1967           "\<forall>m\<ge>N. \<forall>n\<ge>N.
  1968             \<forall>xa\<in>s. \<forall>y\<in>s. norm (f m xa - f n xa - (f m y - f n y)) \<le>
  1969               e / 2 / norm (x - x0) * norm (xa - y)"
  1970         using lem1 *(2) by blast
  1971         show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < e"
  1972           apply (rule_tac x="max M N" in exI)
  1973         proof rule+
  1974           fix m n
  1975           assume as: "max M N \<le>m" "max M N\<le>n"
  1976           have "dist (f m x) (f n x) \<le>
  1977               norm (f m x0 - f n x0) + norm (f m x - f n x - (f m x0 - f n x0))"
  1978             unfolding dist_norm
  1979             by (rule norm_triangle_sub)
  1980           also have "\<dots> \<le> norm (f m x0 - f n x0) + e / 2"
  1981             using N[rule_format,OF _ _ \<open>x\<in>s\<close> \<open>x0\<in>s\<close>, of m n] and as and False
  1982             by auto
  1983           also have "\<dots> < e / 2 + e / 2"
  1984             apply (rule add_strict_right_mono)
  1985             using as and M[rule_format]
  1986             unfolding dist_norm
  1987             apply auto
  1988             done
  1989           finally show "dist (f m x) (f n x) < e"
  1990             by auto
  1991         qed
  1992       qed
  1993     qed
  1994   qed
  1995   then obtain g where g: "\<forall>x\<in>s. (\<lambda>n. f n x) \<longlonglongrightarrow> g x" ..
  1996   have lem2: "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s. norm ((f n x - f n y) - (g x - g y)) \<le> e * norm (x - y)"
  1997   proof (rule, rule)
  1998     fix e :: real
  1999     assume *: "e > 0"
  2000     obtain N where
  2001       N: "\<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s. norm (f m x - f n x - (f m y - f n y)) \<le> e * norm (x - y)"
  2002       using lem1 * by blast
  2003     show "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s. norm (f n x - f n y - (g x - g y)) \<le> e * norm (x - y)"
  2004       apply (rule_tac x=N in exI)
  2005     proof rule+
  2006       fix n x y
  2007       assume as: "N \<le> n" "x \<in> s" "y \<in> s"
  2008       have "((\<lambda>m. norm (f n x - f n y - (f m x - f m y))) \<longlongrightarrow> norm (f n x - f n y - (g x - g y))) sequentially"
  2009         by (intro tendsto_intros g[rule_format] as)
  2010       moreover have "eventually (\<lambda>m. norm (f n x - f n y - (f m x - f m y)) \<le> e * norm (x - y)) sequentially"
  2011         unfolding eventually_sequentially
  2012         apply (rule_tac x=N in exI)
  2013         apply rule
  2014         apply rule
  2015       proof -
  2016         fix m
  2017         assume "N \<le> m"
  2018         then show "norm (f n x - f n y - (f m x - f m y)) \<le> e * norm (x - y)"
  2019           using N[rule_format, of n m x y] and as
  2020           by (auto simp add: algebra_simps)
  2021       qed
  2022       ultimately show "norm (f n x - f n y - (g x - g y)) \<le> e * norm (x - y)"
  2023         by (rule tendsto_ge_const[OF trivial_limit_sequentially])
  2024     qed
  2025   qed
  2026   have "\<forall>x\<in>s. ((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially \<and> (g has_derivative g' x) (at x within s)"
  2027     unfolding has_derivative_within_alt2
  2028   proof (intro ballI conjI)
  2029     fix x
  2030     assume "x \<in> s"
  2031     then show "((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially"
  2032       by (simp add: g)
  2033     have lem3: "\<forall>u. ((\<lambda>n. f' n x u) \<longlongrightarrow> g' x u) sequentially"
  2034       unfolding filterlim_def le_nhds_metric_le eventually_filtermap dist_norm
  2035     proof (intro allI impI)
  2036       fix u
  2037       fix e :: real
  2038       assume "e > 0"
  2039       show "eventually (\<lambda>n. norm (f' n x u - g' x u) \<le> e) sequentially"
  2040       proof (cases "u = 0")
  2041         case True
  2042         have "eventually (\<lambda>n. norm (f' n x u - g' x u) \<le> e * norm u) sequentially"
  2043           using assms(3)[folded eventually_sequentially] and \<open>0 < e\<close> and \<open>x \<in> s\<close>
  2044           by (fast elim: eventually_mono)
  2045         then show ?thesis
  2046           using \<open>u = 0\<close> and \<open>0 < e\<close> by (auto elim: eventually_mono)
  2047       next
  2048         case False
  2049         with \<open>0 < e\<close> have "0 < e / norm u" by simp
  2050         then have "eventually (\<lambda>n. norm (f' n x u - g' x u) \<le> e / norm u * norm u) sequentially"
  2051           using assms(3)[folded eventually_sequentially] and \<open>x \<in> s\<close>
  2052           by (fast elim: eventually_mono)
  2053         then show ?thesis
  2054           using \<open>u \<noteq> 0\<close> by simp
  2055       qed
  2056     qed
  2057     show "bounded_linear (g' x)"
  2058     proof
  2059       fix x' y z :: 'a
  2060       fix c :: real
  2061       note lin = assms(2)[rule_format,OF \<open>x\<in>s\<close>,THEN has_derivative_bounded_linear]
  2062       show "g' x (c *\<^sub>R x') = c *\<^sub>R g' x x'"
  2063         apply (rule tendsto_unique[OF trivial_limit_sequentially])
  2064         apply (rule lem3[rule_format])
  2065         unfolding lin[THEN bounded_linear.linear, THEN linear_cmul]
  2066         apply (intro tendsto_intros)
  2067         apply (rule lem3[rule_format])
  2068         done
  2069       show "g' x (y + z) = g' x y + g' x z"
  2070         apply (rule tendsto_unique[OF trivial_limit_sequentially])
  2071         apply (rule lem3[rule_format])
  2072         unfolding lin[THEN bounded_linear.linear, THEN linear_add]
  2073         apply (rule tendsto_add)
  2074         apply (rule lem3[rule_format])+
  2075         done
  2076       obtain N where N: "\<forall>h. norm (f' N x h - g' x h) \<le> 1 * norm h"
  2077         using assms(3) \<open>x \<in> s\<close> by (fast intro: zero_less_one)
  2078       have "bounded_linear (f' N x)"
  2079         using assms(2) \<open>x \<in> s\<close> by fast
  2080       from bounded_linear.bounded [OF this]
  2081       obtain K where K: "\<forall>h. norm (f' N x h) \<le> norm h * K" ..
  2082       {
  2083         fix h
  2084         have "norm (g' x h) = norm (f' N x h - (f' N x h - g' x h))"
  2085           by simp
  2086         also have "\<dots> \<le> norm (f' N x h) + norm (f' N x h - g' x h)"
  2087           by (rule norm_triangle_ineq4)
  2088         also have "\<dots> \<le> norm h * K + 1 * norm h"
  2089           using N K by (fast intro: add_mono)
  2090         finally have "norm (g' x h) \<le> norm h * (K + 1)"
  2091           by (simp add: ring_distribs)
  2092       }
  2093       then show "\<exists>K. \<forall>h. norm (g' x h) \<le> norm h * K" by fast
  2094     qed
  2095     show "\<forall>e>0. eventually (\<lambda>y. norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)) (at x within s)"
  2096     proof (rule, rule)
  2097       fix e :: real
  2098       assume "e > 0"
  2099       then have *: "e / 3 > 0"
  2100         by auto
  2101       obtain N1 where N1: "\<forall>n\<ge>N1. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e / 3 * norm h"
  2102         using assms(3) * by blast
  2103       obtain N2 where
  2104           N2: "\<forall>n\<ge>N2. \<forall>x\<in>s. \<forall>y\<in>s. norm (f n x - f n y - (g x - g y)) \<le> e / 3 * norm (x - y)"
  2105         using lem2 * by blast
  2106       let ?N = "max N1 N2"
  2107       have "eventually (\<lambda>y. norm (f ?N y - f ?N x - f' ?N x (y - x)) \<le> e / 3 * norm (y - x)) (at x within s)"
  2108         using assms(2)[unfolded has_derivative_within_alt2] and \<open>x \<in> s\<close> and * by fast
  2109       moreover have "eventually (\<lambda>y. y \<in> s) (at x within s)"
  2110         unfolding eventually_at by (fast intro: zero_less_one)
  2111       ultimately show "\<forall>\<^sub>F y in at x within s. norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)"
  2112       proof (rule eventually_elim2)
  2113         fix y
  2114         assume "y \<in> s"
  2115         assume "norm (f ?N y - f ?N x - f' ?N x (y - x)) \<le> e / 3 * norm (y - x)"
  2116         moreover have "norm (g y - g x - (f ?N y - f ?N x)) \<le> e / 3 * norm (y - x)"
  2117           using N2[rule_format, OF _ \<open>y \<in> s\<close> \<open>x \<in> s\<close>]
  2118           by (simp add: norm_minus_commute)
  2119         ultimately have "norm (g y - g x - f' ?N x (y - x)) \<le> 2 * e / 3 * norm (y - x)"
  2120           using norm_triangle_le[of "g y - g x - (f ?N y - f ?N x)" "f ?N y - f ?N x - f' ?N x (y - x)" "2 * e / 3 * norm (y - x)"]
  2121           by (auto simp add: algebra_simps)
  2122         moreover
  2123         have " norm (f' ?N x (y - x) - g' x (y - x)) \<le> e / 3 * norm (y - x)"
  2124           using N1 \<open>x \<in> s\<close> by auto
  2125         ultimately show "norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)"
  2126           using norm_triangle_le[of "g y - g x - f' (max N1 N2) x (y - x)" "f' (max N1 N2) x (y - x) - g' x (y - x)"]
  2127           by (auto simp add: algebra_simps)
  2128       qed
  2129     qed
  2130   qed
  2131   then show ?thesis by fast
  2132 qed
  2133 
  2134 text \<open>Can choose to line up antiderivatives if we want.\<close>
  2135 
  2136 lemma has_antiderivative_sequence:
  2137   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::banach"
  2138   assumes "convex s"
  2139     and "\<forall>n. \<forall>x\<in>s. ((f n) has_derivative (f' n x)) (at x within s)"
  2140     and "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
  2141   shows "\<exists>g. \<forall>x\<in>s. (g has_derivative g' x) (at x within s)"
  2142 proof (cases "s = {}")
  2143   case False
  2144   then obtain a where "a \<in> s"
  2145     by auto
  2146   have *: "\<And>P Q. \<exists>g. \<forall>x\<in>s. P g x \<and> Q g x \<Longrightarrow> \<exists>g. \<forall>x\<in>s. Q g x"
  2147     by auto
  2148   show ?thesis
  2149     apply (rule *)
  2150     apply (rule has_derivative_sequence[OF assms(1) _ assms(3), of "\<lambda>n x. f n x + (f 0 a - f n a)"])
  2151     apply (metis assms(2) has_derivative_add_const)
  2152     apply (rule \<open>a \<in> s\<close>)
  2153     apply auto
  2154     done
  2155 qed auto
  2156 
  2157 lemma has_antiderivative_limit:
  2158   fixes g' :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'b::banach"
  2159   assumes "convex s"
  2160     and "\<forall>e>0. \<exists>f f'. \<forall>x\<in>s.
  2161       (f has_derivative (f' x)) (at x within s) \<and> (\<forall>h. norm (f' x h - g' x h) \<le> e * norm h)"
  2162   shows "\<exists>g. \<forall>x\<in>s. (g has_derivative g' x) (at x within s)"
  2163 proof -
  2164   have *: "\<forall>n. \<exists>f f'. \<forall>x\<in>s.
  2165     (f has_derivative (f' x)) (at x within s) \<and>
  2166     (\<forall>h. norm(f' x h - g' x h) \<le> inverse (real (Suc n)) * norm h)"
  2167     by (simp add: assms(2))
  2168   obtain f where
  2169     *: "\<forall>x. \<exists>f'. \<forall>xa\<in>s. (f x has_derivative f' xa) (at xa within s) \<and>
  2170       (\<forall>h. norm (f' xa h - g' xa h) \<le> inverse (real (Suc x)) * norm h)"
  2171     using *[THEN choice] ..
  2172   obtain f' where
  2173     f: "\<forall>x. \<forall>xa\<in>s. (f x has_derivative f' x xa) (at xa within s) \<and>
  2174       (\<forall>h. norm (f' x xa h - g' xa h) \<le> inverse (real (Suc x)) * norm h)"
  2175     using *[THEN choice] ..
  2176   show ?thesis
  2177     apply (rule has_antiderivative_sequence[OF assms(1), of f f'])
  2178     defer
  2179     apply rule
  2180     apply rule
  2181   proof -
  2182     fix e :: real
  2183     assume "e > 0"
  2184     obtain N where N: "inverse (real (Suc N)) < e"
  2185       using reals_Archimedean[OF \<open>e>0\<close>] ..
  2186     show "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
  2187       apply (rule_tac x=N in exI)
  2188       apply rule
  2189       apply rule
  2190       apply rule
  2191       apply rule
  2192     proof -
  2193       fix n x h
  2194       assume n: "N \<le> n" and x: "x \<in> s"
  2195       have *: "inverse (real (Suc n)) \<le> e"
  2196         apply (rule order_trans[OF _ N[THEN less_imp_le]])
  2197         using n
  2198         apply (auto simp add: field_simps)
  2199         done
  2200       show "norm (f' n x h - g' x h) \<le> e * norm h"
  2201         using f[rule_format,THEN conjunct2, OF x, of n, THEN spec[where x=h]]
  2202         apply (rule order_trans)
  2203         using N *
  2204         apply (cases "h = 0")
  2205         apply auto
  2206         done
  2207     qed
  2208   qed (insert f, auto)
  2209 qed
  2210 
  2211 
  2212 subsection \<open>Differentiation of a series\<close>
  2213 
  2214 lemma has_derivative_series:
  2215   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::banach"
  2216   assumes "convex s"
  2217     and "\<And>n x. x \<in> s \<Longrightarrow> ((f n) has_derivative (f' n x)) (at x within s)"
  2218     and "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (setsum (\<lambda>i. f' i x h) {..<n} - g' x h) \<le> e * norm h"
  2219     and "x \<in> s"
  2220     and "(\<lambda>n. f n x) sums l"
  2221   shows "\<exists>g. \<forall>x\<in>s. (\<lambda>n. f n x) sums (g x) \<and> (g has_derivative g' x) (at x within s)"
  2222   unfolding sums_def
  2223   apply (rule has_derivative_sequence[OF assms(1) _ assms(3)])
  2224   apply (metis assms(2) has_derivative_setsum)
  2225   using assms(4-5)
  2226   unfolding sums_def
  2227   apply auto
  2228   done
  2229 
  2230 lemma has_field_derivative_series:
  2231   fixes f :: "nat \<Rightarrow> ('a :: {real_normed_field,banach}) \<Rightarrow> 'a"
  2232   assumes "convex s"
  2233   assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x within s)"
  2234   assumes "uniform_limit s (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
  2235   assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)"
  2236   shows   "\<exists>g. \<forall>x\<in>s. (\<lambda>n. f n x) sums g x \<and> (g has_field_derivative g' x) (at x within s)"
  2237 unfolding has_field_derivative_def
  2238 proof (rule has_derivative_series)
  2239   show "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm ((\<Sum>i<n. f' i x * h) - g' x * h) \<le> e * norm h"
  2240   proof (intro allI impI)
  2241     fix e :: real assume "e > 0"
  2242     with assms(3) obtain N where N: "\<And>n x. n \<ge> N \<Longrightarrow> x \<in> s \<Longrightarrow> norm ((\<Sum>i<n. f' i x) - g' x) < e"
  2243       unfolding uniform_limit_iff eventually_at_top_linorder dist_norm by blast
  2244     {
  2245       fix n :: nat and x h :: 'a assume nx: "n \<ge> N" "x \<in> s"
  2246       have "norm ((\<Sum>i<n. f' i x * h) - g' x * h) = norm ((\<Sum>i<n. f' i x) - g' x) * norm h"
  2247         by (simp add: norm_mult [symmetric] ring_distribs setsum_left_distrib)
  2248       also from N[OF nx] have "norm ((\<Sum>i<n. f' i x) - g' x) \<le> e" by simp
  2249       hence "norm ((\<Sum>i<n. f' i x) - g' x) * norm h \<le> e * norm h"
  2250         by (intro mult_right_mono) simp_all
  2251       finally have "norm ((\<Sum>i<n. f' i x * h) - g' x * h) \<le> e * norm h" .
  2252     }
  2253     thus "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm ((\<Sum>i<n. f' i x * h) - g' x * h) \<le> e * norm h" by blast
  2254   qed
  2255 qed (insert assms, auto simp: has_field_derivative_def)
  2256 
  2257 lemma has_field_derivative_series':
  2258   fixes f :: "nat \<Rightarrow> ('a :: {real_normed_field,banach}) \<Rightarrow> 'a"
  2259   assumes "convex s"
  2260   assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x within s)"
  2261   assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
  2262   assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)" "x \<in> interior s"
  2263   shows   "summable (\<lambda>n. f n x)" "((\<lambda>x. \<Sum>n. f n x) has_field_derivative (\<Sum>n. f' n x)) (at x)"
  2264 proof -
  2265   from \<open>x \<in> interior s\<close> have "x \<in> s" using interior_subset by blast
  2266   define g' where [abs_def]: "g' x = (\<Sum>i. f' i x)" for x
  2267   from assms(3) have "uniform_limit s (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
  2268     by (simp add: uniformly_convergent_uniform_limit_iff suminf_eq_lim g'_def)
  2269   from has_field_derivative_series[OF assms(1,2) this assms(4,5)] obtain g where g:
  2270     "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>n. f n x) sums g x"
  2271     "\<And>x. x \<in> s \<Longrightarrow> (g has_field_derivative g' x) (at x within s)" by blast
  2272   from g(1)[OF \<open>x \<in> s\<close>] show "summable (\<lambda>n. f n x)" by (simp add: sums_iff)
  2273   from g(2)[OF \<open>x \<in> s\<close>] \<open>x \<in> interior s\<close> have "(g has_field_derivative g' x) (at x)"
  2274     by (simp add: at_within_interior[of x s])
  2275   also have "(g has_field_derivative g' x) (at x) \<longleftrightarrow>
  2276                 ((\<lambda>x. \<Sum>n. f n x) has_field_derivative g' x) (at x)"
  2277     using eventually_nhds_in_nhd[OF \<open>x \<in> interior s\<close>] interior_subset[of s] g(1)
  2278     by (intro DERIV_cong_ev) (auto elim!: eventually_mono simp: sums_iff)
  2279   finally show "((\<lambda>x. \<Sum>n. f n x) has_field_derivative g' x) (at x)" .
  2280 qed
  2281 
  2282 lemma differentiable_series:
  2283   fixes f :: "nat \<Rightarrow> ('a :: {real_normed_field,banach}) \<Rightarrow> 'a"
  2284   assumes "convex s" "open s"
  2285   assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
  2286   assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
  2287   assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)" and x: "x \<in> s"
  2288   shows   "summable (\<lambda>n. f n x)" and "(\<lambda>x. \<Sum>n. f n x) differentiable (at x)"
  2289 proof -
  2290   from assms(4) obtain g' where A: "uniform_limit s (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
  2291     unfolding uniformly_convergent_on_def by blast
  2292   from x and \<open>open s\<close> have s: "at x within s = at x" by (rule at_within_open)
  2293   have "\<exists>g. \<forall>x\<in>s. (\<lambda>n. f n x) sums g x \<and> (g has_field_derivative g' x) (at x within s)"
  2294     by (intro has_field_derivative_series[of s f f' g' x0] assms A has_field_derivative_at_within)
  2295   then obtain g where g: "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>n. f n x) sums g x"
  2296     "\<And>x. x \<in> s \<Longrightarrow> (g has_field_derivative g' x) (at x within s)" by blast
  2297   from g[OF x] show "summable (\<lambda>n. f n x)" by (auto simp: summable_def)
  2298   from g(2)[OF x] have g': "(g has_derivative op * (g' x)) (at x)"
  2299     by (simp add: has_field_derivative_def s)
  2300   have "((\<lambda>x. \<Sum>n. f n x) has_derivative op * (g' x)) (at x)"
  2301     by (rule has_derivative_transform_within_open[OF g' \<open>open s\<close> x])
  2302        (insert g, auto simp: sums_iff)
  2303   thus "(\<lambda>x. \<Sum>n. f n x) differentiable (at x)" unfolding differentiable_def
  2304     by (auto simp: summable_def differentiable_def has_field_derivative_def)
  2305 qed
  2306 
  2307 lemma differentiable_series':
  2308   fixes f :: "nat \<Rightarrow> ('a :: {real_normed_field,banach}) \<Rightarrow> 'a"
  2309   assumes "convex s" "open s"
  2310   assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
  2311   assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
  2312   assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)"
  2313   shows   "(\<lambda>x. \<Sum>n. f n x) differentiable (at x0)"
  2314   using differentiable_series[OF assms, of x0] \<open>x0 \<in> s\<close> by blast+
  2315 
  2316 text \<open>Considering derivative @{typ "real \<Rightarrow> 'b::real_normed_vector"} as a vector.\<close>
  2317 
  2318 definition "vector_derivative f net = (SOME f'. (f has_vector_derivative f') net)"
  2319 
  2320 lemma vector_derivative_unique_within:
  2321   assumes not_bot: "at x within s \<noteq> bot"
  2322     and f': "(f has_vector_derivative f') (at x within s)"
  2323     and f'': "(f has_vector_derivative f'') (at x within s)"
  2324   shows "f' = f''"
  2325 proof -
  2326   have "(\<lambda>x. x *\<^sub>R f') = (\<lambda>x. x *\<^sub>R f'')"
  2327   proof (rule frechet_derivative_unique_within)
  2328     show "\<forall>i\<in>Basis. \<forall>e>0. \<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> x + d *\<^sub>R i \<in> s"
  2329     proof clarsimp
  2330       fix e :: real assume "0 < e"
  2331       with islimpt_approachable_real[of x s] not_bot
  2332       obtain x' where "x' \<in> s" "x' \<noteq> x" "\<bar>x' - x\<bar> < e"
  2333         by (auto simp add: trivial_limit_within)
  2334       then show "\<exists>d. d \<noteq> 0 \<and> \<bar>d\<bar> < e \<and> x + d \<in> s"
  2335         by (intro exI[of _ "x' - x"]) auto
  2336     qed
  2337   qed (insert f' f'', auto simp: has_vector_derivative_def)
  2338   then show ?thesis
  2339     unfolding fun_eq_iff by (metis scaleR_one)
  2340 qed
  2341 
  2342 lemma vector_derivative_unique_at:
  2343   "(f has_vector_derivative f') (at x) \<Longrightarrow> (f has_vector_derivative f'') (at x) \<Longrightarrow> f' = f''"
  2344   by (rule vector_derivative_unique_within) auto
  2345 
  2346 lemma differentiableI_vector: "(f has_vector_derivative y) F \<Longrightarrow> f differentiable F"
  2347   by (auto simp: differentiable_def has_vector_derivative_def)
  2348 
  2349 lemma vector_derivative_works:
  2350   "f differentiable net \<longleftrightarrow> (f has_vector_derivative (vector_derivative f net)) net"
  2351     (is "?l = ?r")
  2352 proof
  2353   assume ?l
  2354   obtain f' where f': "(f has_derivative f') net"
  2355     using \<open>?l\<close> unfolding differentiable_def ..
  2356   then interpret bounded_linear f'
  2357     by auto
  2358   show ?r
  2359     unfolding vector_derivative_def has_vector_derivative_def
  2360     by (rule someI[of _ "f' 1"]) (simp add: scaleR[symmetric] f')
  2361 qed (auto simp: vector_derivative_def has_vector_derivative_def differentiable_def)
  2362 
  2363 lemma vector_derivative_within:
  2364   assumes not_bot: "at x within s \<noteq> bot" and y: "(f has_vector_derivative y) (at x within s)"
  2365   shows "vector_derivative f (at x within s) = y"
  2366   using y
  2367   by (intro vector_derivative_unique_within[OF not_bot vector_derivative_works[THEN iffD1] y])
  2368      (auto simp: differentiable_def has_vector_derivative_def)
  2369 
  2370 lemma frechet_derivative_eq_vector_derivative:
  2371   assumes "f differentiable (at x)"
  2372     shows  "(frechet_derivative f (at x)) = (\<lambda>r. r *\<^sub>R vector_derivative f (at x))"
  2373 using assms
  2374 by (auto simp: differentiable_iff_scaleR vector_derivative_def has_vector_derivative_def
  2375          intro: someI frechet_derivative_at [symmetric])
  2376 
  2377 lemma has_real_derivative:
  2378   fixes f :: "real \<Rightarrow> real"
  2379   assumes "(f has_derivative f') F"
  2380   obtains c where "(f has_real_derivative c) F"
  2381 proof -
  2382   obtain c where "f' = (\<lambda>x. x * c)"
  2383     by (metis assms has_derivative_bounded_linear real_bounded_linear)
  2384   then show ?thesis
  2385     by (metis assms that has_field_derivative_def mult_commute_abs)
  2386 qed
  2387 
  2388 lemma has_real_derivative_iff:
  2389   fixes f :: "real \<Rightarrow> real"
  2390   shows "(\<exists>c. (f has_real_derivative c) F) = (\<exists>D. (f has_derivative D) F)"
  2391   by (metis has_field_derivative_def has_real_derivative)
  2392 
  2393 definition deriv :: "('a \<Rightarrow> 'a::real_normed_field) \<Rightarrow> 'a \<Rightarrow> 'a" where
  2394   "deriv f x \<equiv> SOME D. DERIV f x :> D"
  2395 
  2396 lemma DERIV_imp_deriv: "DERIV f x :> f' \<Longrightarrow> deriv f x = f'"
  2397   unfolding deriv_def by (metis some_equality DERIV_unique)
  2398 
  2399 lemma DERIV_deriv_iff_has_field_derivative:
  2400   "DERIV f x :> deriv f x \<longleftrightarrow> (\<exists>f'. (f has_field_derivative f') (at x))"
  2401   by (auto simp: has_field_derivative_def DERIV_imp_deriv)
  2402 
  2403 lemma DERIV_deriv_iff_real_differentiable:
  2404   fixes x :: real
  2405   shows "DERIV f x :> deriv f x \<longleftrightarrow> f differentiable at x"
  2406   unfolding differentiable_def by (metis DERIV_imp_deriv has_real_derivative_iff)
  2407 
  2408 lemma real_derivative_chain:
  2409   fixes x :: real
  2410   shows "f differentiable at x \<Longrightarrow> g differentiable at (f x)
  2411     \<Longrightarrow> deriv (g o f) x = deriv g (f x) * deriv f x"
  2412   by (metis DERIV_deriv_iff_real_differentiable DERIV_chain DERIV_imp_deriv)
  2413 lemma field_derivative_eq_vector_derivative:
  2414    "(deriv f x) = vector_derivative f (at x)"
  2415 by (simp add: mult.commute deriv_def vector_derivative_def has_vector_derivative_def has_field_derivative_def)
  2416 
  2417 lemma islimpt_closure_open:
  2418   fixes s :: "'a::perfect_space set"
  2419   assumes "open s" and t: "t = closure s" "x \<in> t"
  2420   shows "x islimpt t"
  2421 proof cases
  2422   assume "x \<in> s"
  2423   { fix T assume "x \<in> T" "open T"
  2424     then have "open (s \<inter> T)"
  2425       using \<open>open s\<close> by auto
  2426     then have "s \<inter> T \<noteq> {x}"
  2427       using not_open_singleton[of x] by auto
  2428     with \<open>x \<in> T\<close> \<open>x \<in> s\<close> have "\<exists>y\<in>t. y \<in> T \<and> y \<noteq> x"
  2429       using closure_subset[of s] by (auto simp: t) }
  2430   then show ?thesis
  2431     by (auto intro!: islimptI)
  2432 next
  2433   assume "x \<notin> s" with t show ?thesis
  2434     unfolding t closure_def by (auto intro: islimpt_subset)
  2435 qed
  2436 
  2437 lemma vector_derivative_unique_within_closed_interval:
  2438   assumes ab: "a < b" "x \<in> cbox a b"
  2439   assumes D: "(f has_vector_derivative f') (at x within cbox a b)" "(f has_vector_derivative f'') (at x within cbox a b)"
  2440   shows "f' = f''"
  2441   using ab
  2442   by (intro vector_derivative_unique_within[OF _ D])
  2443      (auto simp: trivial_limit_within intro!: islimpt_closure_open[where s="{a <..< b}"])
  2444 
  2445 lemma vector_derivative_at:
  2446   "(f has_vector_derivative f') (at x) \<Longrightarrow> vector_derivative f (at x) = f'"
  2447   by (intro vector_derivative_within at_neq_bot)
  2448 
  2449 lemma has_vector_derivative_id_at [simp]: "vector_derivative (\<lambda>x. x) (at a) = 1"
  2450   by (simp add: vector_derivative_at)
  2451 
  2452 lemma vector_derivative_minus_at [simp]:
  2453   "f differentiable at a
  2454    \<Longrightarrow> vector_derivative (\<lambda>x. - f x) (at a) = - vector_derivative f (at a)"
  2455   by (simp add: vector_derivative_at has_vector_derivative_minus vector_derivative_works [symmetric])
  2456 
  2457 lemma vector_derivative_add_at [simp]:
  2458   "\<lbrakk>f differentiable at a; g differentiable at a\<rbrakk>
  2459    \<Longrightarrow> vector_derivative (\<lambda>x. f x + g x) (at a) = vector_derivative f (at a) + vector_derivative g (at a)"
  2460   by (simp add: vector_derivative_at has_vector_derivative_add vector_derivative_works [symmetric])
  2461 
  2462 lemma vector_derivative_diff_at [simp]:
  2463   "\<lbrakk>f differentiable at a; g differentiable at a\<rbrakk>
  2464    \<Longrightarrow> vector_derivative (\<lambda>x. f x - g x) (at a) = vector_derivative f (at a) - vector_derivative g (at a)"
  2465   by (simp add: vector_derivative_at has_vector_derivative_diff vector_derivative_works [symmetric])
  2466 
  2467 lemma vector_derivative_mult_at [simp]:
  2468   fixes f g :: "real \<Rightarrow> 'a :: real_normed_algebra"
  2469   shows  "\<lbrakk>f differentiable at a; g differentiable at a\<rbrakk>
  2470    \<Longrightarrow> vector_derivative (\<lambda>x. f x * g x) (at a) = f a * vector_derivative g (at a) + vector_derivative f (at a) * g a"
  2471   by (simp add: vector_derivative_at has_vector_derivative_mult vector_derivative_works [symmetric])
  2472 
  2473 lemma vector_derivative_scaleR_at [simp]:
  2474     "\<lbrakk>f differentiable at a; g differentiable at a\<rbrakk>
  2475    \<Longrightarrow> vector_derivative (\<lambda>x. f x *\<^sub>R g x) (at a) = f a *\<^sub>R vector_derivative g (at a) + vector_derivative f (at a) *\<^sub>R g a"
  2476 apply (rule vector_derivative_at)
  2477 apply (rule has_vector_derivative_scaleR)
  2478 apply (auto simp: vector_derivative_works has_vector_derivative_def has_field_derivative_def mult_commute_abs)
  2479 done
  2480 
  2481 lemma vector_derivative_within_closed_interval:
  2482   assumes ab: "a < b" "x \<in> cbox a b"
  2483   assumes f: "(f has_vector_derivative f') (at x within cbox a b)"
  2484   shows "vector_derivative f (at x within cbox a b) = f'"
  2485   by (intro vector_derivative_unique_within_closed_interval[OF ab _ f]
  2486             vector_derivative_works[THEN iffD1] differentiableI_vector)
  2487      fact
  2488 
  2489 lemma has_vector_derivative_within_subset:
  2490   "(f has_vector_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_vector_derivative f') (at x within t)"
  2491   by (auto simp: has_vector_derivative_def intro: has_derivative_within_subset)
  2492 
  2493 lemma has_vector_derivative_at_within:
  2494   "(f has_vector_derivative f') (at x) \<Longrightarrow> (f has_vector_derivative f') (at x within s)"
  2495   unfolding has_vector_derivative_def
  2496   by (rule has_derivative_at_within)
  2497 
  2498 lemma has_vector_derivative_weaken:
  2499   fixes x D and f g s t
  2500   assumes f: "(f has_vector_derivative D) (at x within t)"
  2501     and "x \<in> s" "s \<subseteq> t"
  2502     and "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
  2503   shows "(g has_vector_derivative D) (at x within s)"
  2504 proof -
  2505   have "(f has_vector_derivative D) (at x within s) \<longleftrightarrow> (g has_vector_derivative D) (at x within s)"
  2506     unfolding has_vector_derivative_def has_derivative_iff_norm
  2507     using assms by (intro conj_cong Lim_cong_within refl) auto
  2508   then show ?thesis
  2509     using has_vector_derivative_within_subset[OF f \<open>s \<subseteq> t\<close>] by simp
  2510 qed
  2511 
  2512 lemma has_vector_derivative_transform_within:
  2513   assumes "(f has_vector_derivative f') (at x within s)"
  2514     and "0 < d"
  2515     and "x \<in> s"
  2516     and "\<And>x'. \<lbrakk>x'\<in>s; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
  2517     shows "(g has_vector_derivative f') (at x within s)"
  2518   using assms
  2519   unfolding has_vector_derivative_def
  2520   by (rule has_derivative_transform_within)
  2521 
  2522 lemma has_vector_derivative_transform_within_open:
  2523   assumes "(f has_vector_derivative f') (at x)"
  2524     and "open s"
  2525     and "x \<in> s"
  2526     and "\<And>y. y\<in>s \<Longrightarrow> f y = g y"
  2527   shows "(g has_vector_derivative f') (at x)"
  2528   using assms
  2529   unfolding has_vector_derivative_def
  2530   by (rule has_derivative_transform_within_open)
  2531 
  2532 lemma vector_diff_chain_at:
  2533   assumes "(f has_vector_derivative f') (at x)"
  2534     and "(g has_vector_derivative g') (at (f x))"
  2535   shows "((g \<circ> f) has_vector_derivative (f' *\<^sub>R g')) (at x)"
  2536   using assms(2)
  2537   unfolding has_vector_derivative_def
  2538   apply -
  2539   apply (drule diff_chain_at[OF assms(1)[unfolded has_vector_derivative_def]])
  2540   apply (simp only: o_def real_scaleR_def scaleR_scaleR)
  2541   done
  2542 
  2543 lemma vector_diff_chain_within:
  2544   assumes "(f has_vector_derivative f') (at x within s)"
  2545     and "(g has_vector_derivative g') (at (f x) within f ` s)"
  2546   shows "((g \<circ> f) has_vector_derivative (f' *\<^sub>R g')) (at x within s)"
  2547   using assms(2)
  2548   unfolding has_vector_derivative_def
  2549   apply -
  2550   apply (drule diff_chain_within[OF assms(1)[unfolded has_vector_derivative_def]])
  2551   apply (simp only: o_def real_scaleR_def scaleR_scaleR)
  2552   done
  2553 
  2554 lemma vector_derivative_const_at [simp]: "vector_derivative (\<lambda>x. c) (at a) = 0"
  2555   by (simp add: vector_derivative_at)
  2556 
  2557 lemma vector_derivative_at_within_ivl:
  2558   "(f has_vector_derivative f') (at x) \<Longrightarrow>
  2559     a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> a<b \<Longrightarrow> vector_derivative f (at x within {a..b}) = f'"
  2560 using has_vector_derivative_at_within vector_derivative_within_closed_interval by fastforce
  2561 
  2562 lemma vector_derivative_chain_at:
  2563   assumes "f differentiable at x" "(g differentiable at (f x))"
  2564   shows "vector_derivative (g \<circ> f) (at x) =
  2565          vector_derivative f (at x) *\<^sub>R vector_derivative g (at (f x))"
  2566 by (metis vector_diff_chain_at vector_derivative_at vector_derivative_works assms)
  2567 
  2568 lemma field_vector_diff_chain_at:  (*thanks to Wenda Li*)
  2569  assumes Df: "(f has_vector_derivative f') (at x)"
  2570      and Dg: "(g has_field_derivative g') (at (f x))"
  2571  shows "((g \<circ> f) has_vector_derivative (f' * g')) (at x)"
  2572 using diff_chain_at[OF Df[unfolded has_vector_derivative_def]
  2573                        Dg [unfolded has_field_derivative_def]]
  2574  by (auto simp: o_def mult.commute has_vector_derivative_def)
  2575 
  2576 lemma vector_derivative_chain_at_general:  (*thanks to Wenda Li*)
  2577  assumes "f differentiable at x" "(\<exists>g'. (g has_field_derivative g') (at (f x)))"
  2578  shows "vector_derivative (g \<circ> f) (at x) =
  2579         vector_derivative f (at x) * deriv g (f x)"
  2580 apply (rule vector_derivative_at [OF field_vector_diff_chain_at])
  2581 using assms
  2582 by (auto simp: vector_derivative_works DERIV_deriv_iff_has_field_derivative)
  2583 
  2584 lemma exp_scaleR_has_vector_derivative_right:
  2585   "((\<lambda>t. exp (t *\<^sub>R A)) has_vector_derivative exp (t *\<^sub>R A) * A) (at t within T)"
  2586   unfolding has_vector_derivative_def
  2587 proof (rule has_derivativeI)
  2588   let ?F = "at t within (T \<inter> {t - 1 <..< t + 1})"
  2589   have *: "at t within T = ?F"
  2590     by (rule at_within_nhd[where S="{t - 1 <..< t + 1}"]) auto
  2591   let ?e = "\<lambda>i x. (inverse (1 + real i) * inverse (fact i) * (x - t) ^ i) *\<^sub>R (A * A ^ i)"
  2592   have "\<forall>\<^sub>F n in sequentially.
  2593       \<forall>x\<in>T \<inter> {t - 1<..<t + 1}. norm (?e n x) \<le> norm (A ^ (n + 1) /\<^sub>R fact (n + 1))"
  2594     by (auto simp: divide_simps power_abs intro!: mult_left_le_one_le power_le_one eventuallyI)
  2595   then have "uniform_limit (T \<inter> {t - 1<..<t + 1}) (\<lambda>n x. \<Sum>i<n. ?e i x) (\<lambda>x. \<Sum>i. ?e i x) sequentially"
  2596     by (rule weierstrass_m_test_ev) (intro summable_ignore_initial_segment summable_norm_exp)
  2597   moreover
  2598   have "\<forall>\<^sub>F x in sequentially. x > 0"
  2599     by (metis eventually_gt_at_top)
  2600   then have
  2601     "\<forall>\<^sub>F n in sequentially. ((\<lambda>x. \<Sum>i<n. ?e i x) \<longlongrightarrow> A) ?F"
  2602     by eventually_elim
  2603       (auto intro!: tendsto_eq_intros
  2604         simp: power_0_left if_distrib cond_application_beta setsum.delta
  2605         cong: if_cong)
  2606   ultimately
  2607   have [tendsto_intros]: "((\<lambda>x. \<Sum>i. ?e i x) \<longlongrightarrow> A) ?F"
  2608     by (auto intro!: swap_uniform_limit[where f="\<lambda>n x. \<Sum>i < n. ?e i x" and F = sequentially])
  2609   have [tendsto_intros]: "((\<lambda>x. if x = t then 0 else 1) \<longlongrightarrow> 1) ?F"
  2610     by (rule Lim_eventually) (simp add: eventually_at_filter)
  2611   have "((\<lambda>y. ((y - t) / abs (y - t)) *\<^sub>R ((\<Sum>n. ?e n y) - A)) \<longlongrightarrow> 0) (at t within T)"
  2612     unfolding *
  2613     by (rule tendsto_norm_zero_cancel) (auto intro!: tendsto_eq_intros)
  2614 
  2615   moreover
  2616 
  2617   have "\<forall>\<^sub>F x in at t within T. x \<noteq> t"
  2618     by (simp add: eventually_at_filter)
  2619   then have "\<forall>\<^sub>F x in at t within T. ((x - t) / \<bar>x - t\<bar>) *\<^sub>R ((\<Sum>n. ?e n x) - A) =
  2620     (exp ((x - t) *\<^sub>R A) - 1 - (x - t) *\<^sub>R A) /\<^sub>R norm (x - t)"
  2621   proof eventually_elim
  2622     case (elim x)
  2623     have "(exp ((x - t) *\<^sub>R A) - 1 - (x - t) *\<^sub>R A) /\<^sub>R norm (x - t) =
  2624       ((\<Sum>n. (x - t) *\<^sub>R ?e n x) - (x - t) *\<^sub>R A) /\<^sub>R norm (x - t)"
  2625       unfolding exp_first_term
  2626       by (simp add: ac_simps)
  2627     also
  2628     have "summable (\<lambda>n. ?e n x)"
  2629     proof -
  2630       from elim have "?e n x = (((x - t) *\<^sub>R A) ^ (n + 1)) /\<^sub>R fact (n + 1) /\<^sub>R (x - t)" for n
  2631         by simp
  2632       then show ?thesis
  2633         by (auto simp only:
  2634           intro!: summable_scaleR_right summable_ignore_initial_segment summable_exp_generic)
  2635     qed
  2636     then have "(\<Sum>n. (x - t) *\<^sub>R ?e n x) = (x - t) *\<^sub>R (\<Sum>n. ?e n x)"
  2637       by (rule suminf_scaleR_right[symmetric])
  2638     also have "(\<dots> - (x - t) *\<^sub>R A) /\<^sub>R norm (x - t) = (x - t) *\<^sub>R ((\<Sum>n. ?e n x) - A) /\<^sub>R norm (x - t)"
  2639       by (simp add: algebra_simps)
  2640     finally show ?case
  2641       by (simp add: divide_simps)
  2642   qed
  2643 
  2644   ultimately
  2645 
  2646   have "((\<lambda>y. (exp ((y - t) *\<^sub>R A) - 1 - (y - t) *\<^sub>R A) /\<^sub>R norm (y - t)) \<longlongrightarrow> 0) (at t within T)"
  2647     by (rule Lim_transform_eventually[rotated])
  2648   from tendsto_mult_right_zero[OF this, where c="exp (t *\<^sub>R A)"]
  2649   show "((\<lambda>y. (exp (y *\<^sub>R A) - exp (t *\<^sub>R A) - (y - t) *\<^sub>R (exp (t *\<^sub>R A) * A)) /\<^sub>R norm (y - t)) \<longlongrightarrow> 0)
  2650       (at t within T)"
  2651     by (rule Lim_transform_eventually[rotated])
  2652       (auto simp: algebra_simps divide_simps exp_add_commuting[symmetric])
  2653 qed (rule bounded_linear_scaleR_left)
  2654 
  2655 lemma exp_times_scaleR_commute: "exp (t *\<^sub>R A) * A = A * exp (t *\<^sub>R A)"
  2656   using exp_times_arg_commute[symmetric, of "t *\<^sub>R A"]
  2657   by (auto simp: algebra_simps)
  2658 
  2659 lemma exp_scaleR_has_vector_derivative_left: "((\<lambda>t. exp (t *\<^sub>R A)) has_vector_derivative A * exp (t *\<^sub>R A)) (at t)"
  2660   using exp_scaleR_has_vector_derivative_right[of A t]
  2661   by (simp add: exp_times_scaleR_commute)
  2662 
  2663 
  2664 subsection \<open>Relation between convexity and derivative\<close>
  2665 
  2666 (* TODO: Generalise to real vector spaces? *)
  2667 lemma convex_on_imp_above_tangent:
  2668   assumes convex: "convex_on A f" and connected: "connected A"
  2669   assumes c: "c \<in> interior A" and x : "x \<in> A"
  2670   assumes deriv: "(f has_field_derivative f') (at c within A)"
  2671   shows   "f x - f c \<ge> f' * (x - c)"
  2672 proof (cases x c rule: linorder_cases)
  2673   assume xc: "x > c"
  2674   let ?A' = "interior A \<inter> {c<..}"
  2675   from c have "c \<in> interior A \<inter> closure {c<..}" by auto
  2676   also have "\<dots> \<subseteq> closure (interior A \<inter> {c<..})" by (intro open_Int_closure_subset) auto
  2677   finally have "at c within ?A' \<noteq> bot" by (subst at_within_eq_bot_iff) auto
  2678   moreover from deriv have "((\<lambda>y. (f y - f c) / (y - c)) \<longlongrightarrow> f') (at c within ?A')"
  2679     unfolding DERIV_within_iff using interior_subset[of A] by (blast intro: tendsto_mono at_le)
  2680   moreover from eventually_at_right_real[OF xc]
  2681     have "eventually (\<lambda>y. (f y - f c) / (y - c) \<le> (f x - f c) / (x - c)) (at_right c)"
  2682   proof eventually_elim
  2683     fix y assume y: "y \<in> {c<..<x}"
  2684     with convex connected x c have "f y \<le> (f x - f c) / (x - c) * (y - c) + f c"
  2685       using interior_subset[of A]
  2686       by (intro convex_onD_Icc' convex_on_subset[OF convex] connected_contains_Icc) auto
  2687     hence "f y - f c \<le> (f x - f c) / (x - c) * (y - c)" by simp
  2688     thus "(f y - f c) / (y - c) \<le> (f x - f c) / (x - c)" using y xc by (simp add: divide_simps)
  2689   qed
  2690   hence "eventually (\<lambda>y. (f y - f c) / (y - c) \<le> (f x - f c) / (x - c)) (at c within ?A')"
  2691     by (blast intro: filter_leD at_le)
  2692   ultimately have "f' \<le> (f x - f c) / (x - c)" by (rule tendsto_ge_const)
  2693   thus ?thesis using xc by (simp add: field_simps)
  2694 next
  2695   assume xc: "x < c"
  2696   let ?A' = "interior A \<inter> {..<c}"
  2697   from c have "c \<in> interior A \<inter> closure {..<c}" by auto
  2698   also have "\<dots> \<subseteq> closure (interior A \<inter> {..<c})" by (intro open_Int_closure_subset) auto
  2699   finally have "at c within ?A' \<noteq> bot" by (subst at_within_eq_bot_iff) auto
  2700   moreover from deriv have "((\<lambda>y. (f y - f c) / (y - c)) \<longlongrightarrow> f') (at c within ?A')"
  2701     unfolding DERIV_within_iff using interior_subset[of A] by (blast intro: tendsto_mono at_le)
  2702   moreover from eventually_at_left_real[OF xc]
  2703     have "eventually (\<lambda>y. (f y - f c) / (y - c) \<ge> (f x - f c) / (x - c)) (at_left c)"
  2704   proof eventually_elim
  2705     fix y assume y: "y \<in> {x<..<c}"
  2706     with convex connected x c have "f y \<le> (f x - f c) / (c - x) * (c - y) + f c"
  2707       using interior_subset[of A]
  2708       by (intro convex_onD_Icc'' convex_on_subset[OF convex] connected_contains_Icc) auto
  2709     hence "f y - f c \<le> (f x - f c) * ((c - y) / (c - x))" by simp
  2710     also have "(c - y) / (c - x) = (y - c) / (x - c)" using y xc by (simp add: field_simps)
  2711     finally show "(f y - f c) / (y - c) \<ge> (f x - f c) / (x - c)" using y xc
  2712       by (simp add: divide_simps)
  2713   qed
  2714   hence "eventually (\<lambda>y. (f y - f c) / (y - c) \<ge> (f x - f c) / (x - c)) (at c within ?A')"
  2715     by (blast intro: filter_leD at_le)
  2716   ultimately have "f' \<ge> (f x - f c) / (x - c)" by (rule tendsto_le_const)
  2717   thus ?thesis using xc by (simp add: field_simps)
  2718 qed simp_all
  2719 
  2720 
  2721 subsection \<open>Partial derivatives\<close>
  2722 
  2723 lemma eventually_at_Pair_within_TimesI1:
  2724   fixes x::"'a::metric_space"
  2725   assumes "\<forall>\<^sub>F x' in at x within X. P x'"
  2726   assumes "P x"
  2727   shows "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. P x'"
  2728 proof -
  2729   from assms[unfolded eventually_at_topological]
  2730   obtain S where S: "open S" "x \<in> S" "\<And>x'. x' \<in> X \<Longrightarrow> x' \<in> S \<Longrightarrow> P x'"
  2731     by metis
  2732   show "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. P x'"
  2733     unfolding eventually_at_topological
  2734     by (auto intro!: exI[where x="S \<times> UNIV"] S open_Times)
  2735 qed
  2736 
  2737 lemma eventually_at_Pair_within_TimesI2:
  2738   fixes x::"'a::metric_space"
  2739   assumes "\<forall>\<^sub>F y' in at y within Y. P y'"
  2740   assumes "P y"
  2741   shows "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. P y'"
  2742 proof -
  2743   from assms[unfolded eventually_at_topological]
  2744   obtain S where S: "open S" "y \<in> S" "\<And>y'. y' \<in> Y \<Longrightarrow> y' \<in> S \<Longrightarrow> P y'"
  2745     by metis
  2746   show "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. P y'"
  2747     unfolding eventually_at_topological
  2748     by (auto intro!: exI[where x="UNIV \<times> S"] S open_Times)
  2749 qed
  2750 
  2751 lemma has_derivative_partialsI:
  2752   assumes fx: "\<And>x y. x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> ((\<lambda>x. f x y) has_derivative blinfun_apply (fx x y)) (at x within X)"
  2753   assumes fy: "\<And>x y. x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> ((\<lambda>y. f x y) has_derivative blinfun_apply (fy x y)) (at y within Y)"
  2754   assumes fx_cont: "continuous_on (X \<times> Y) (\<lambda>(x, y). fx x y)"
  2755   assumes fy_cont: "continuous_on (X \<times> Y) (\<lambda>(x, y). fy x y)"
  2756   assumes "x \<in> X" "y \<in> Y"
  2757   assumes "convex X" "convex Y"
  2758   shows "((\<lambda>(x, y). f x y) has_derivative (\<lambda>(tx, ty). fx x y tx + fy x y ty)) (at (x, y) within X \<times> Y)"
  2759 proof (safe intro!: has_derivativeI tendstoI, goal_cases)
  2760   case (2 e')
  2761   define e where "e = e' / 9"
  2762   have "e > 0" using \<open>e' > 0\<close> by (simp add: e_def)
  2763 
  2764   have "(x, y) \<in> X \<times> Y" using assms by auto
  2765   from fy_cont[unfolded continuous_on_eq_continuous_within, rule_format, OF this,
  2766     unfolded continuous_within, THEN tendstoD, OF \<open>e > 0\<close>]
  2767   have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. dist (fy x' y') (fy x y) < e"
  2768     by (auto simp: split_beta')
  2769   from this[unfolded eventually_at] obtain d' where
  2770     "d' > 0"
  2771     "\<And>x' y'. x' \<in> X \<Longrightarrow> y' \<in> Y \<Longrightarrow> (x', y') \<noteq> (x, y) \<Longrightarrow> dist (x', y') (x, y) < d' \<Longrightarrow>
  2772       dist (fy x' y') (fy x y) < e"
  2773     by auto
  2774   then
  2775   have d': "x' \<in> X \<Longrightarrow> y' \<in> Y \<Longrightarrow> dist (x', y') (x, y) < d' \<Longrightarrow> dist (fy x' y') (fy x y) < e"
  2776     for x' y'
  2777     using \<open>0 < e\<close>
  2778     by (cases "(x', y') = (x, y)") auto
  2779   define d where "d = d' / sqrt 2"
  2780   have "d > 0" using \<open>0 < d'\<close> by (simp add: d_def)
  2781   have d: "x' \<in> X \<Longrightarrow> y' \<in> Y \<Longrightarrow> dist x' x < d \<Longrightarrow> dist y' y < d \<Longrightarrow> dist (fy x' y') (fy x y) < e"
  2782     for x' y'
  2783     by (auto simp: dist_prod_def d_def intro!: d' real_sqrt_sum_squares_less)
  2784 
  2785   let ?S = "ball y d \<inter> Y"
  2786   have "convex ?S"
  2787     by (auto intro!: convex_Int \<open>convex Y\<close>)
  2788   {
  2789     fix x'::'a and y'::'b
  2790     assume x': "x' \<in> X" and y': "y' \<in> Y"
  2791     assume dx': "dist x' x < d" and dy': "dist y' y < d"
  2792     have "norm (fy x' y' - fy x' y) \<le> dist (fy x' y') (fy x y) + dist (fy x' y) (fy x y)"
  2793       by norm
  2794     also have "dist (fy x' y') (fy x y) < e"
  2795       by (rule d; fact)
  2796     also have "dist (fy x' y) (fy x y) < e"
  2797       by (auto intro!: d simp: dist_prod_def x' \<open>d > 0\<close> \<open>y \<in> Y\<close> dx')
  2798     finally
  2799     have "norm (fy x' y' - fy x' y) < e + e"
  2800       by arith
  2801     then have "onorm (blinfun_apply (fy x' y') - blinfun_apply (fy x' y)) < e + e"
  2802       by (auto simp: norm_blinfun.rep_eq blinfun.diff_left[abs_def] fun_diff_def)
  2803   } note onorm = this
  2804 
  2805   have ev_mem: "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. (x', y') \<in> X \<times> Y"
  2806     using \<open>x \<in> X\<close> \<open>y \<in> Y\<close>
  2807     by (auto simp: eventually_at intro!: zero_less_one)
  2808   moreover
  2809   have ev_dist: "\<forall>\<^sub>F xy in at (x, y) within X \<times> Y. dist xy (x, y) < d" if "d > 0" for d
  2810     using eventually_at_ball[OF that]
  2811     by (rule eventually_elim2) (auto simp: dist_commute intro!: eventually_True)
  2812   note ev_dist[OF \<open>0 < d\<close>]
  2813   ultimately
  2814   have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y.
  2815     norm (f x' y' - f x' y - (fy x' y) (y' - y)) \<le> norm (y' - y) * (e + e)"
  2816   proof (eventually_elim, safe)
  2817     fix x' y'
  2818     assume "x' \<in> X" and y': "y' \<in> Y"
  2819     assume dist: "dist (x', y') (x, y) < d"
  2820     then have dx: "dist x' x < d" and dy: "dist y' y < d"
  2821       unfolding dist_prod_def fst_conv snd_conv atomize_conj
  2822       by (metis le_less_trans real_sqrt_sum_squares_ge1 real_sqrt_sum_squares_ge2)
  2823     {
  2824       fix t::real
  2825       assume "t \<in> {0 .. 1}"
  2826       then have "y + t *\<^sub>R (y' - y) \<in> closed_segment y y'"
  2827         by (auto simp: closed_segment_def algebra_simps intro!: exI[where x=t])
  2828       also
  2829       have "\<dots> \<subseteq> ball y d \<inter> Y"
  2830         using \<open>y \<in> Y\<close> \<open>0 < d\<close> dy y'
  2831         by (intro \<open>convex ?S\<close>[unfolded convex_contains_segment, rule_format, of y y'])
  2832           (auto simp: dist_commute)
  2833       finally have "y + t *\<^sub>R (y' - y) \<in> ?S" .
  2834     } note seg = this
  2835 
  2836     have "\<forall>x\<in>ball y d \<inter> Y. onorm (blinfun_apply (fy x' x) - blinfun_apply (fy x' y)) \<le> e + e"
  2837       by (safe intro!: onorm less_imp_le \<open>x' \<in> X\<close> dx) (auto simp: dist_commute \<open>0 < d\<close> \<open>y \<in> Y\<close>)
  2838     with seg has_derivative_within_subset[OF assms(2)[OF \<open>x' \<in> X\<close>]]
  2839     show "norm (f x' y' - f x' y - (fy x' y) (y' - y)) \<le> norm (y' - y) * (e + e)"
  2840       by (rule differentiable_bound_linearization[where S="?S"])
  2841         (auto intro!: \<open>0 < d\<close> \<open>y \<in> Y\<close>)
  2842   qed
  2843   moreover
  2844   let ?le = "\<lambda>x'. norm (f x' y - f x y - (fx x y) (x' - x)) \<le> norm (x' - x) * e"
  2845   from fx[OF \<open>x \<in> X\<close> \<open>y \<in> Y\<close>, unfolded has_derivative_within, THEN conjunct2, THEN tendstoD, OF \<open>0 < e\<close>]
  2846   have "\<forall>\<^sub>F x' in at x within X. ?le x'"
  2847     by eventually_elim
  2848        (auto simp: dist_norm divide_simps blinfun.bilinear_simps field_simps split: if_split_asm)
  2849   then have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. ?le x'"
  2850     by (rule eventually_at_Pair_within_TimesI1)
  2851        (simp add: blinfun.bilinear_simps)
  2852   moreover have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. norm ((x', y') - (x, y)) \<noteq> 0"
  2853     unfolding norm_eq_zero right_minus_eq
  2854     by (auto simp: eventually_at intro!: zero_less_one)
  2855   moreover
  2856   from fy_cont[unfolded continuous_on_eq_continuous_within, rule_format, OF SigmaI[OF \<open>x \<in> X\<close> \<open>y \<in> Y\<close>],
  2857       unfolded continuous_within, THEN tendstoD, OF \<open>0 < e\<close>]
  2858   have "\<forall>\<^sub>F x' in at x within X. norm (fy x' y - fy x y) < e"
  2859     unfolding eventually_at
  2860     using \<open>y \<in> Y\<close>
  2861     by (auto simp: dist_prod_def dist_norm)
  2862   then have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. norm (fy x' y - fy x y) < e"
  2863     by (rule eventually_at_Pair_within_TimesI1)
  2864        (simp add: blinfun.bilinear_simps \<open>0 < e\<close>)
  2865   ultimately
  2866   have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y.
  2867             norm ((f x' y' - f x y - (fx x y (x' - x) + fy x y (y' - y))) /\<^sub>R
  2868               norm ((x', y') - (x, y)))
  2869             < e'"
  2870     apply eventually_elim
  2871   proof safe
  2872     fix x' y'
  2873     have "norm (f x' y' - f x y - (fx x y (x' - x) + fy x y (y' - y))) \<le>
  2874         norm (f x' y' - f x' y - fy x' y (y' - y)) +
  2875         norm (fy x y (y' - y) - fy x' y (y' - y)) +
  2876         norm (f x' y - f x y - fx x y (x' - x))"
  2877       by norm
  2878     also
  2879     assume nz: "norm ((x', y') - (x, y)) \<noteq> 0"
  2880       and nfy: "norm (fy x' y - fy x y) < e"
  2881     assume "norm (f x' y' - f x' y - blinfun_apply (fy x' y) (y' - y)) \<le> norm (y' - y) * (e + e)"
  2882     also assume "norm (f x' y - f x y - blinfun_apply (fx x y) (x' - x)) \<le> norm (x' - x) * e"
  2883     also
  2884     have "norm ((fy x y) (y' - y) - (fy x' y) (y' - y)) \<le> norm ((fy x y) - (fy x' y)) * norm (y' - y)"
  2885       by (auto simp: blinfun.bilinear_simps[symmetric] intro!: norm_blinfun)
  2886     also have "\<dots> \<le> (e + e) * norm (y' - y)"
  2887       using \<open>e > 0\<close> nfy
  2888       by (auto simp: norm_minus_commute intro!: mult_right_mono)
  2889     also have "norm (x' - x) * e \<le> norm (x' - x) * (e + e)"
  2890       using \<open>0 < e\<close> by simp
  2891     also have "norm (y' - y) * (e + e) + (e + e) * norm (y' - y) + norm (x' - x) * (e + e) \<le>
  2892         (norm (y' - y) + norm (x' - x)) * (4 * e)"
  2893       using \<open>e > 0\<close>
  2894       by (simp add: algebra_simps)
  2895     also have "\<dots> \<le> 2 * norm ((x', y') - (x, y)) * (4 * e)"
  2896       using \<open>0 < e\<close> real_sqrt_sum_squares_ge1[of "norm (x' - x)" "norm (y' - y)"]
  2897         real_sqrt_sum_squares_ge2[of "norm (y' - y)" "norm (x' - x)"]
  2898       by (auto intro!: mult_right_mono simp: norm_prod_def
  2899         simp del: real_sqrt_sum_squares_ge1 real_sqrt_sum_squares_ge2)
  2900     also have "\<dots> \<le> norm ((x', y') - (x, y)) * (8 * e)"
  2901       by simp
  2902     also have "\<dots> < norm ((x', y') - (x, y)) * e'"
  2903       using \<open>0 < e'\<close> nz
  2904       by (auto simp: e_def)
  2905     finally show "norm ((f x' y' - f x y - (fx x y (x' - x) + fy x y (y' - y))) /\<^sub>R norm ((x', y') - (x, y))) < e'"
  2906       by (auto simp: divide_simps dist_norm mult.commute)
  2907   qed
  2908   then show ?case
  2909     by eventually_elim (auto simp: dist_norm field_simps)
  2910 qed (auto intro!: bounded_linear_intros simp: split_beta')
  2911 
  2912 end