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