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
```