src/HOL/Multivariate_Analysis/Derivative.thy
 author wenzelm Sun Nov 02 17:09:04 2014 +0100 (2014-11-02) changeset 58877 262572d90bc6 parent 57865 dcfb33c26f50 child 59558 5d9f0ace9af0 permissions -rw-r--r--
```     1 (*  Title:      HOL/Multivariate_Analysis/Derivative.thy
```
```     2     Author:     John Harrison
```
```     3     Author:     Robert Himmelmann, TU Muenchen (translation from HOL Light)
```
```     4 *)
```
```     5
```
```     6 section {* Multivariate calculus in Euclidean space *}
```
```     7
```
```     8 theory Derivative
```
```     9 imports Brouwer_Fixpoint Operator_Norm
```
```    10 begin
```
```    11
```
```    12 lemma netlimit_at_vector: (* TODO: move *)
```
```    13   fixes a :: "'a::real_normed_vector"
```
```    14   shows "netlimit (at a) = a"
```
```    15 proof (cases "\<exists>x. x \<noteq> a")
```
```    16   case True then obtain x where x: "x \<noteq> a" ..
```
```    17   have "\<not> trivial_limit (at a)"
```
```    18     unfolding trivial_limit_def eventually_at dist_norm
```
```    19     apply clarsimp
```
```    20     apply (rule_tac x="a + scaleR (d / 2) (sgn (x - a))" in exI)
```
```    21     apply (simp add: norm_sgn sgn_zero_iff x)
```
```    22     done
```
```    23   then show ?thesis
```
```    24     by (rule netlimit_within [of a UNIV])
```
```    25 qed simp
```
```    26
```
```    27 (* Because I do not want to type this all the time *)
```
```    28 lemmas linear_linear = linear_conv_bounded_linear[symmetric]
```
```    29
```
```    30 declare has_derivative_bounded_linear[dest]
```
```    31
```
```    32 subsection {* Derivatives *}
```
```    33
```
```    34 subsubsection {* Combining theorems. *}
```
```    35
```
```    36 lemmas has_derivative_id = has_derivative_ident
```
```    37 lemmas has_derivative_neg = has_derivative_minus
```
```    38 lemmas has_derivative_sub = has_derivative_diff
```
```    39 lemmas scaleR_right_has_derivative = has_derivative_scaleR_right
```
```    40 lemmas scaleR_left_has_derivative = has_derivative_scaleR_left
```
```    41 lemmas inner_right_has_derivative = has_derivative_inner_right
```
```    42 lemmas inner_left_has_derivative = has_derivative_inner_left
```
```    43 lemmas mult_right_has_derivative = has_derivative_mult_right
```
```    44 lemmas mult_left_has_derivative = has_derivative_mult_left
```
```    45
```
```    46 lemma has_derivative_add_const:
```
```    47   "(f has_derivative f') net \<Longrightarrow> ((\<lambda>x. f x + c) has_derivative f') net"
```
```    48   by (intro derivative_eq_intros) auto
```
```    49
```
```    50
```
```    51 subsection {* Derivative with composed bilinear function. *}
```
```    52
```
```    53 lemma has_derivative_bilinear_within:
```
```    54   assumes "(f has_derivative f') (at x within s)"
```
```    55     and "(g has_derivative g') (at x within s)"
```
```    56     and "bounded_bilinear h"
```
```    57   shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x within s)"
```
```    58   using bounded_bilinear.FDERIV[OF assms(3,1,2)] .
```
```    59
```
```    60 lemma has_derivative_bilinear_at:
```
```    61   assumes "(f has_derivative f') (at x)"
```
```    62     and "(g has_derivative g') (at x)"
```
```    63     and "bounded_bilinear h"
```
```    64   shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x)"
```
```    65   using has_derivative_bilinear_within[of f f' x UNIV g g' h] assms by simp
```
```    66
```
```    67 text {* These are the only cases we'll care about, probably. *}
```
```    68
```
```    69 lemma has_derivative_within: "(f has_derivative f') (at x within s) \<longleftrightarrow>
```
```    70     bounded_linear f' \<and> ((\<lambda>y. (1 / norm(y - x)) *\<^sub>R (f y - (f x + f' (y - x)))) ---> 0) (at x within s)"
```
```    71   unfolding has_derivative_def Lim
```
```    72   by (auto simp add: netlimit_within field_simps)
```
```    73
```
```    74 lemma has_derivative_at: "(f has_derivative f') (at x) \<longleftrightarrow>
```
```    75     bounded_linear f' \<and> ((\<lambda>y. (1 / (norm(y - x))) *\<^sub>R (f y - (f x + f' (y - x)))) ---> 0) (at x)"
```
```    76   using has_derivative_within [of f f' x UNIV]
```
```    77   by simp
```
```    78
```
```    79 text {* More explicit epsilon-delta forms. *}
```
```    80
```
```    81 lemma has_derivative_within':
```
```    82   "(f has_derivative f')(at x within s) \<longleftrightarrow>
```
```    83     bounded_linear f' \<and>
```
```    84     (\<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. 0 < norm (x' - x) \<and> norm (x' - x) < d \<longrightarrow>
```
```    85       norm (f x' - f x - f'(x' - x)) / norm (x' - x) < e)"
```
```    86   unfolding has_derivative_within Lim_within dist_norm
```
```    87   unfolding diff_0_right
```
```    88   by (simp add: diff_diff_eq)
```
```    89
```
```    90 lemma has_derivative_at':
```
```    91   "(f has_derivative f') (at x) \<longleftrightarrow> bounded_linear f' \<and>
```
```    92     (\<forall>e>0. \<exists>d>0. \<forall>x'. 0 < norm (x' - x) \<and> norm (x' - x) < d \<longrightarrow>
```
```    93       norm (f x' - f x - f'(x' - x)) / norm (x' - x) < e)"
```
```    94   using has_derivative_within' [of f f' x UNIV]
```
```    95   by simp
```
```    96
```
```    97 lemma has_derivative_at_within:
```
```    98   "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f') (at x within s)"
```
```    99   unfolding has_derivative_within' has_derivative_at'
```
```   100   by blast
```
```   101
```
```   102 lemma has_derivative_within_open:
```
```   103   "a \<in> s \<Longrightarrow> open s \<Longrightarrow>
```
```   104     (f has_derivative f') (at a within s) \<longleftrightarrow> (f has_derivative f') (at a)"
```
```   105   by (simp only: at_within_interior interior_open)
```
```   106
```
```   107 lemma has_derivative_right:
```
```   108   fixes f :: "real \<Rightarrow> real"
```
```   109     and y :: "real"
```
```   110   shows "(f has_derivative (op * y)) (at x within ({x <..} \<inter> I)) \<longleftrightarrow>
```
```   111     ((\<lambda>t. (f x - f t) / (x - t)) ---> y) (at x within ({x <..} \<inter> I))"
```
```   112 proof -
```
```   113   have "((\<lambda>t. (f t - (f x + y * (t - x))) / \<bar>t - x\<bar>) ---> 0) (at x within ({x<..} \<inter> I)) \<longleftrightarrow>
```
```   114     ((\<lambda>t. (f t - f x) / (t - x) - y) ---> 0) (at x within ({x<..} \<inter> I))"
```
```   115     by (intro Lim_cong_within) (auto simp add: diff_divide_distrib add_divide_distrib)
```
```   116   also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f t - f x) / (t - x)) ---> y) (at x within ({x<..} \<inter> I))"
```
```   117     by (simp add: Lim_null[symmetric])
```
```   118   also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f x - f t) / (x - t)) ---> y) (at x within ({x<..} \<inter> I))"
```
```   119     by (intro Lim_cong_within) (simp_all add: field_simps)
```
```   120   finally show ?thesis
```
```   121     by (simp add: bounded_linear_mult_right has_derivative_within)
```
```   122 qed
```
```   123
```
```   124 subsubsection {*Caratheodory characterization*}
```
```   125
```
```   126 lemma DERIV_within_iff:
```
```   127   "(f has_field_derivative D) (at a within s) \<longleftrightarrow> ((\<lambda>z. (f z - f a) / (z - a)) ---> D) (at a within s)"
```
```   128 proof -
```
```   129   have 1: "\<And>w y. ~(w = a) ==> y / (w - a) - D = (y - (w - a)*D)/(w - a)"
```
```   130     by (metis divide_diff_eq_iff eq_iff_diff_eq_0 mult.commute)
```
```   131   show ?thesis
```
```   132     apply (simp add: has_field_derivative_def has_derivative_within bounded_linear_mult_right)
```
```   133     apply (simp add: LIM_zero_iff [where l = D, symmetric])
```
```   134     apply (simp add: Lim_within dist_norm)
```
```   135     apply (simp add: nonzero_norm_divide [symmetric])
```
```   136     apply (simp add: 1 diff_add_eq_diff_diff ac_simps)
```
```   137     done
```
```   138 qed
```
```   139
```
```   140 lemma DERIV_caratheodory_within:
```
```   141   "(f has_field_derivative l) (at x within s) \<longleftrightarrow>
```
```   142    (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> continuous (at x within s) g \<and> g x = l)"
```
```   143       (is "?lhs = ?rhs")
```
```   144 proof
```
```   145   assume ?lhs
```
```   146   show ?rhs
```
```   147   proof (intro exI conjI)
```
```   148     let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
```
```   149     show "\<forall>z. f z - f x = ?g z * (z-x)" by simp
```
```   150     show "continuous (at x within s) ?g" using `?lhs`
```
```   151       by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within)
```
```   152     show "?g x = l" by simp
```
```   153   qed
```
```   154 next
```
```   155   assume ?rhs
```
```   156   then obtain g where
```
```   157     "(\<forall>z. f z - f x = g z * (z-x))" and "continuous (at x within s) g" and "g x = l" by blast
```
```   158   thus ?lhs
```
```   159     by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within)
```
```   160 qed
```
```   161
```
```   162 subsubsection {* Limit transformation for derivatives *}
```
```   163
```
```   164 lemma has_derivative_transform_within:
```
```   165   assumes "0 < d"
```
```   166     and "x \<in> s"
```
```   167     and "\<forall>x'\<in>s. dist x' x < d \<longrightarrow> f x' = g x'"
```
```   168     and "(f has_derivative f') (at x within s)"
```
```   169   shows "(g has_derivative f') (at x within s)"
```
```   170   using assms
```
```   171   unfolding has_derivative_within
```
```   172   apply clarify
```
```   173   apply (rule Lim_transform_within, auto)
```
```   174   done
```
```   175
```
```   176 lemma has_derivative_transform_at:
```
```   177   assumes "0 < d"
```
```   178     and "\<forall>x'. dist x' x < d \<longrightarrow> f x' = g x'"
```
```   179     and "(f has_derivative f') (at x)"
```
```   180   shows "(g has_derivative f') (at x)"
```
```   181   using has_derivative_transform_within [of d x UNIV f g f'] assms
```
```   182   by simp
```
```   183
```
```   184 lemma has_derivative_transform_within_open:
```
```   185   assumes "open s"
```
```   186     and "x \<in> s"
```
```   187     and "\<forall>y\<in>s. f y = g y"
```
```   188     and "(f has_derivative f') (at x)"
```
```   189   shows "(g has_derivative f') (at x)"
```
```   190   using assms
```
```   191   unfolding has_derivative_at
```
```   192   apply clarify
```
```   193   apply (rule Lim_transform_within_open[OF assms(1,2)], auto)
```
```   194   done
```
```   195
```
```   196 subsection {* Differentiability *}
```
```   197
```
```   198 definition
```
```   199   differentiable_on :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a set \<Rightarrow> bool"
```
```   200     (infix "differentiable'_on" 50)
```
```   201   where "f differentiable_on s \<longleftrightarrow> (\<forall>x\<in>s. f differentiable (at x within s))"
```
```   202
```
```   203 lemma differentiableI: "(f has_derivative f') net \<Longrightarrow> f differentiable net"
```
```   204   unfolding differentiable_def
```
```   205   by auto
```
```   206
```
```   207 lemma differentiable_at_withinI: "f differentiable (at x) \<Longrightarrow> f differentiable (at x within s)"
```
```   208   unfolding differentiable_def
```
```   209   using has_derivative_at_within
```
```   210   by blast
```
```   211
```
```   212 lemma differentiable_within_open: (* TODO: delete *)
```
```   213   assumes "a \<in> s"
```
```   214     and "open s"
```
```   215   shows "f differentiable (at a within s) \<longleftrightarrow> f differentiable (at a)"
```
```   216   using assms
```
```   217   by (simp only: at_within_interior interior_open)
```
```   218
```
```   219 lemma differentiable_on_eq_differentiable_at:
```
```   220   "open s \<Longrightarrow> f differentiable_on s \<longleftrightarrow> (\<forall>x\<in>s. f differentiable at x)"
```
```   221   unfolding differentiable_on_def
```
```   222   by (metis at_within_interior interior_open)
```
```   223
```
```   224 lemma differentiable_transform_within:
```
```   225   assumes "0 < d"
```
```   226     and "x \<in> s"
```
```   227     and "\<forall>x'\<in>s. dist x' x < d \<longrightarrow> f x' = g x'"
```
```   228   assumes "f differentiable (at x within s)"
```
```   229   shows "g differentiable (at x within s)"
```
```   230   using assms(4)
```
```   231   unfolding differentiable_def
```
```   232   by (auto intro!: has_derivative_transform_within[OF assms(1-3)])
```
```   233
```
```   234 lemma differentiable_transform_at:
```
```   235   assumes "0 < d"
```
```   236     and "\<forall>x'. dist x' x < d \<longrightarrow> f x' = g x'"
```
```   237     and "f differentiable at x"
```
```   238   shows "g differentiable at x"
```
```   239   using assms(3)
```
```   240   unfolding differentiable_def
```
```   241   using has_derivative_transform_at[OF assms(1-2)]
```
```   242   by auto
```
```   243
```
```   244
```
```   245 subsection {* Frechet derivative and Jacobian matrix *}
```
```   246
```
```   247 definition "frechet_derivative f net = (SOME f'. (f has_derivative f') net)"
```
```   248
```
```   249 lemma frechet_derivative_works:
```
```   250   "f differentiable net \<longleftrightarrow> (f has_derivative (frechet_derivative f net)) net"
```
```   251   unfolding frechet_derivative_def differentiable_def
```
```   252   unfolding some_eq_ex[of "\<lambda> f' . (f has_derivative f') net"] ..
```
```   253
```
```   254 lemma linear_frechet_derivative: "f differentiable net \<Longrightarrow> linear (frechet_derivative f net)"
```
```   255   unfolding frechet_derivative_works has_derivative_def
```
```   256   by (auto intro: bounded_linear.linear)
```
```   257
```
```   258
```
```   259 subsection {* Differentiability implies continuity *}
```
```   260
```
```   261 lemma differentiable_imp_continuous_within:
```
```   262   "f differentiable (at x within s) \<Longrightarrow> continuous (at x within s) f"
```
```   263   by (auto simp: differentiable_def intro: has_derivative_continuous)
```
```   264
```
```   265 lemma differentiable_imp_continuous_on:
```
```   266   "f differentiable_on s \<Longrightarrow> continuous_on s f"
```
```   267   unfolding differentiable_on_def continuous_on_eq_continuous_within
```
```   268   using differentiable_imp_continuous_within by blast
```
```   269
```
```   270 lemma differentiable_on_subset:
```
```   271   "f differentiable_on t \<Longrightarrow> s \<subseteq> t \<Longrightarrow> f differentiable_on s"
```
```   272   unfolding differentiable_on_def
```
```   273   using differentiable_within_subset
```
```   274   by blast
```
```   275
```
```   276 lemma differentiable_on_empty: "f differentiable_on {}"
```
```   277   unfolding differentiable_on_def
```
```   278   by auto
```
```   279
```
```   280 text {* Results about neighborhoods filter. *}
```
```   281
```
```   282 lemma eventually_nhds_metric_le:
```
```   283   "eventually P (nhds a) = (\<exists>d>0. \<forall>x. dist x a \<le> d \<longrightarrow> P x)"
```
```   284   unfolding eventually_nhds_metric by (safe, rule_tac x="d / 2" in exI, auto)
```
```   285
```
```   286 lemma le_nhds: "F \<le> nhds a \<longleftrightarrow> (\<forall>S. open S \<and> a \<in> S \<longrightarrow> eventually (\<lambda>x. x \<in> S) F)"
```
```   287   unfolding le_filter_def eventually_nhds by (fast elim: eventually_elim1)
```
```   288
```
```   289 lemma le_nhds_metric: "F \<le> nhds a \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist x a < e) F)"
```
```   290   unfolding le_filter_def eventually_nhds_metric by (fast elim: eventually_elim1)
```
```   291
```
```   292 lemma le_nhds_metric_le: "F \<le> nhds a \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist x a \<le> e) F)"
```
```   293   unfolding le_filter_def eventually_nhds_metric_le by (fast elim: eventually_elim1)
```
```   294
```
```   295 text {* Several results are easier using a "multiplied-out" variant.
```
```   296 (I got this idea from Dieudonne's proof of the chain rule). *}
```
```   297
```
```   298 lemma has_derivative_within_alt:
```
```   299   "(f has_derivative f') (at x within s) \<longleftrightarrow> bounded_linear f' \<and>
```
```   300     (\<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))"
```
```   301   unfolding has_derivative_within filterlim_def le_nhds_metric_le eventually_filtermap
```
```   302     eventually_at dist_norm diff_add_eq_diff_diff
```
```   303   by (force simp add: linear_0 bounded_linear.linear pos_divide_le_eq)
```
```   304
```
```   305 lemma has_derivative_within_alt2:
```
```   306   "(f has_derivative f') (at x within s) \<longleftrightarrow> bounded_linear f' \<and>
```
```   307     (\<forall>e>0. eventually (\<lambda>y. norm (f y - f x - f' (y - x)) \<le> e * norm (y - x)) (at x within s))"
```
```   308   unfolding has_derivative_within filterlim_def le_nhds_metric_le eventually_filtermap
```
```   309     eventually_at dist_norm diff_add_eq_diff_diff
```
```   310   by (force simp add: linear_0 bounded_linear.linear pos_divide_le_eq)
```
```   311
```
```   312 lemma has_derivative_at_alt:
```
```   313   "(f has_derivative f') (at x) \<longleftrightarrow>
```
```   314     bounded_linear f' \<and>
```
```   315     (\<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))"
```
```   316   using has_derivative_within_alt[where s=UNIV]
```
```   317   by simp
```
```   318
```
```   319
```
```   320 subsection {* The chain rule *}
```
```   321
```
```   322 lemma diff_chain_within[derivative_intros]:
```
```   323   assumes "(f has_derivative f') (at x within s)"
```
```   324     and "(g has_derivative g') (at (f x) within (f ` s))"
```
```   325   shows "((g \<circ> f) has_derivative (g' \<circ> f'))(at x within s)"
```
```   326   using has_derivative_in_compose[OF assms]
```
```   327   by (simp add: comp_def)
```
```   328
```
```   329 lemma diff_chain_at[derivative_intros]:
```
```   330   "(f has_derivative f') (at x) \<Longrightarrow>
```
```   331     (g has_derivative g') (at (f x)) \<Longrightarrow> ((g \<circ> f) has_derivative (g' \<circ> f')) (at x)"
```
```   332   using has_derivative_compose[of f f' x UNIV g g']
```
```   333   by (simp add: comp_def)
```
```   334
```
```   335
```
```   336 subsection {* Composition rules stated just for differentiability *}
```
```   337
```
```   338 lemma differentiable_chain_at:
```
```   339   "f differentiable (at x) \<Longrightarrow>
```
```   340     g differentiable (at (f x)) \<Longrightarrow> (g \<circ> f) differentiable (at x)"
```
```   341   unfolding differentiable_def
```
```   342   by (meson diff_chain_at)
```
```   343
```
```   344 lemma differentiable_chain_within:
```
```   345   "f differentiable (at x within s) \<Longrightarrow>
```
```   346     g differentiable (at(f x) within (f ` s)) \<Longrightarrow> (g \<circ> f) differentiable (at x within s)"
```
```   347   unfolding differentiable_def
```
```   348   by (meson diff_chain_within)
```
```   349
```
```   350
```
```   351 subsection {* Uniqueness of derivative *}
```
```   352
```
```   353
```
```   354 text {*
```
```   355  The general result is a bit messy because we need approachability of the
```
```   356  limit point from any direction. But OK for nontrivial intervals etc.
```
```   357 *}
```
```   358
```
```   359 lemma frechet_derivative_unique_within:
```
```   360   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
```
```   361   assumes "(f has_derivative f') (at x within s)"
```
```   362     and "(f has_derivative f'') (at x within s)"
```
```   363     and "\<forall>i\<in>Basis. \<forall>e>0. \<exists>d. 0 < abs d \<and> abs d < e \<and> (x + d *\<^sub>R i) \<in> s"
```
```   364   shows "f' = f''"
```
```   365 proof -
```
```   366   note as = assms(1,2)[unfolded has_derivative_def]
```
```   367   then interpret f': bounded_linear f' by auto
```
```   368   from as interpret f'': bounded_linear f'' by auto
```
```   369   have "x islimpt s" unfolding islimpt_approachable
```
```   370   proof (rule, rule)
```
```   371     fix e :: real
```
```   372     assume "e > 0"
```
```   373     obtain d where "0 < \<bar>d\<bar>" and "\<bar>d\<bar> < e" and "x + d *\<^sub>R (SOME i. i \<in> Basis) \<in> s"
```
```   374       using assms(3) SOME_Basis `e>0` by blast
```
```   375     then show "\<exists>x'\<in>s. x' \<noteq> x \<and> dist x' x < e"
```
```   376       apply (rule_tac x="x + d *\<^sub>R (SOME i. i \<in> Basis)" in bexI)
```
```   377       unfolding dist_norm
```
```   378       apply (auto simp: SOME_Basis nonzero_Basis)
```
```   379       done
```
```   380   qed
```
```   381   then have *: "netlimit (at x within s) = x"
```
```   382     apply (auto intro!: netlimit_within)
```
```   383     by (metis trivial_limit_within)
```
```   384   show ?thesis
```
```   385     apply (rule linear_eq_stdbasis)
```
```   386     unfolding linear_conv_bounded_linear
```
```   387     apply (rule as(1,2)[THEN conjunct1])+
```
```   388   proof (rule, rule ccontr)
```
```   389     fix i :: 'a
```
```   390     assume i: "i \<in> Basis"
```
```   391     def e \<equiv> "norm (f' i - f'' i)"
```
```   392     assume "f' i \<noteq> f'' i"
```
```   393     then have "e > 0"
```
```   394       unfolding e_def by auto
```
```   395     obtain d where d:
```
```   396       "0 < d"
```
```   397       "(\<And>xa. xa\<in>s \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow>
```
```   398           dist ((f xa - f x - f' (xa - x)) /\<^sub>R norm (xa - x) -
```
```   399               (f xa - f x - f'' (xa - x)) /\<^sub>R norm (xa - x)) (0 - 0) < e)"
```
```   400       using tendsto_diff [OF as(1,2)[THEN conjunct2]]
```
```   401       unfolding * Lim_within
```
```   402       using `e>0` by blast
```
```   403     obtain c where c: "0 < \<bar>c\<bar>" "\<bar>c\<bar> < d \<and> x + c *\<^sub>R i \<in> s"
```
```   404       using assms(3) i d(1) by blast
```
```   405     have *: "norm (- ((1 / \<bar>c\<bar>) *\<^sub>R f' (c *\<^sub>R i)) + (1 / \<bar>c\<bar>) *\<^sub>R f'' (c *\<^sub>R i)) =
```
```   406         norm ((1 / abs c) *\<^sub>R (- (f' (c *\<^sub>R i)) + f'' (c *\<^sub>R i)))"
```
```   407       unfolding scaleR_right_distrib by auto
```
```   408     also have "\<dots> = norm ((1 / abs c) *\<^sub>R (c *\<^sub>R (- (f' i) + f'' i)))"
```
```   409       unfolding f'.scaleR f''.scaleR
```
```   410       unfolding scaleR_right_distrib scaleR_minus_right
```
```   411       by auto
```
```   412     also have "\<dots> = e"
```
```   413       unfolding e_def
```
```   414       using c(1)
```
```   415       using norm_minus_cancel[of "f' i - f'' i"]
```
```   416       by auto
```
```   417     finally show False
```
```   418       using c
```
```   419       using d(2)[of "x + c *\<^sub>R i"]
```
```   420       unfolding dist_norm
```
```   421       unfolding f'.scaleR f''.scaleR f'.add f''.add f'.diff f''.diff
```
```   422         scaleR_scaleR scaleR_right_diff_distrib scaleR_right_distrib
```
```   423       using i
```
```   424       by (auto simp: inverse_eq_divide)
```
```   425   qed
```
```   426 qed
```
```   427
```
```   428 lemma frechet_derivative_unique_at:
```
```   429   "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f'') (at x) \<Longrightarrow> f' = f''"
```
```   430   by (rule has_derivative_unique)
```
```   431
```
```   432 lemma frechet_derivative_unique_within_closed_interval:
```
```   433   fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
```
```   434   assumes "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"
```
```   435     and "x \<in> cbox a b"
```
```   436     and "(f has_derivative f' ) (at x within cbox a b)"
```
```   437     and "(f has_derivative f'') (at x within cbox a b)"
```
```   438   shows "f' = f''"
```
```   439   apply(rule frechet_derivative_unique_within)
```
```   440   apply(rule assms(3,4))+
```
```   441 proof (rule, rule, rule)
```
```   442   fix e :: real
```
```   443   fix i :: 'a
```
```   444   assume "e > 0" and i: "i \<in> Basis"
```
```   445   then show "\<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> x + d *\<^sub>R i \<in> cbox a b"
```
```   446   proof (cases "x\<bullet>i = a\<bullet>i")
```
```   447     case True
```
```   448     then show ?thesis
```
```   449       apply (rule_tac x="(min (b\<bullet>i - a\<bullet>i)  e) / 2" in exI)
```
```   450       using assms(1)[THEN bspec[where x=i]] and `e>0` and assms(2)
```
```   451       unfolding mem_box
```
```   452       using i
```
```   453       apply (auto simp add: field_simps inner_simps inner_Basis)
```
```   454       done
```
```   455   next
```
```   456     note * = assms(2)[unfolded mem_box, THEN bspec, OF i]
```
```   457     case False
```
```   458     moreover have "a \<bullet> i < x \<bullet> i"
```
```   459       using False * by auto
```
```   460     moreover {
```
```   461       have "a \<bullet> i * 2 + min (x \<bullet> i - a \<bullet> i) e \<le> a\<bullet>i *2 + x\<bullet>i - a\<bullet>i"
```
```   462         by auto
```
```   463       also have "\<dots> = a\<bullet>i + x\<bullet>i"
```
```   464         by auto
```
```   465       also have "\<dots> \<le> 2 * (x\<bullet>i)"
```
```   466         using * by auto
```
```   467       finally have "a \<bullet> i * 2 + min (x \<bullet> i - a \<bullet> i) e \<le> x \<bullet> i * 2"
```
```   468         by auto
```
```   469     }
```
```   470     moreover have "min (x \<bullet> i - a \<bullet> i) e \<ge> 0"
```
```   471       using * and `e>0` by auto
```
```   472     then have "x \<bullet> i * 2 \<le> b \<bullet> i * 2 + min (x \<bullet> i - a \<bullet> i) e"
```
```   473       using * by auto
```
```   474     ultimately show ?thesis
```
```   475       apply (rule_tac x="- (min (x\<bullet>i - a\<bullet>i) e) / 2" in exI)
```
```   476       using assms(1)[THEN bspec, OF i] and `e>0` and assms(2)
```
```   477       unfolding mem_box
```
```   478       using i
```
```   479       apply (auto simp add: field_simps inner_simps inner_Basis)
```
```   480       done
```
```   481   qed
```
```   482 qed
```
```   483
```
```   484 lemma frechet_derivative_unique_within_open_interval:
```
```   485   fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
```
```   486   assumes "x \<in> box a b"
```
```   487     and "(f has_derivative f' ) (at x within box a b)"
```
```   488     and "(f has_derivative f'') (at x within box a b)"
```
```   489   shows "f' = f''"
```
```   490 proof -
```
```   491   from assms(1) have *: "at x within box a b = at x"
```
```   492     by (metis at_within_interior interior_open open_box)
```
```   493   from assms(2,3) [unfolded *] show "f' = f''"
```
```   494     by (rule frechet_derivative_unique_at)
```
```   495 qed
```
```   496
```
```   497 lemma frechet_derivative_at:
```
```   498   "(f has_derivative f') (at x) \<Longrightarrow> f' = frechet_derivative f (at x)"
```
```   499   apply (rule frechet_derivative_unique_at[of f])
```
```   500   apply assumption
```
```   501   unfolding frechet_derivative_works[symmetric]
```
```   502   using differentiable_def
```
```   503   apply auto
```
```   504   done
```
```   505
```
```   506 lemma frechet_derivative_within_cbox:
```
```   507   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
```
```   508   assumes "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"
```
```   509     and "x \<in> cbox a b"
```
```   510     and "(f has_derivative f') (at x within cbox a b)"
```
```   511   shows "frechet_derivative f (at x within cbox a b) = f'"
```
```   512   using assms
```
```   513   by (metis Derivative.differentiableI frechet_derivative_unique_within_closed_interval frechet_derivative_works)
```
```   514
```
```   515
```
```   516 subsection {* The traditional Rolle theorem in one dimension *}
```
```   517
```
```   518 lemma linear_componentwise:
```
```   519   fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
```
```   520   assumes lf: "linear f"
```
```   521   shows "(f x) \<bullet> j = (\<Sum>i\<in>Basis. (x\<bullet>i) * (f i\<bullet>j))" (is "?lhs = ?rhs")
```
```   522 proof -
```
```   523   have "?rhs = (\<Sum>i\<in>Basis. (x\<bullet>i) *\<^sub>R (f i))\<bullet>j"
```
```   524     by (simp add: inner_setsum_left)
```
```   525   then show ?thesis
```
```   526     unfolding linear_setsum_mul[OF lf, symmetric]
```
```   527     unfolding euclidean_representation ..
```
```   528 qed
```
```   529
```
```   530 text {* Derivatives of local minima and maxima are zero. *}
```
```   531
```
```   532 lemma has_derivative_local_min:
```
```   533   fixes f :: "'a::real_normed_vector \<Rightarrow> real"
```
```   534   assumes deriv: "(f has_derivative f') (at x)"
```
```   535   assumes min: "eventually (\<lambda>y. f x \<le> f y) (at x)"
```
```   536   shows "f' = (\<lambda>h. 0)"
```
```   537 proof
```
```   538   fix h :: 'a
```
```   539   interpret f': bounded_linear f'
```
```   540     using deriv by (rule has_derivative_bounded_linear)
```
```   541   show "f' h = 0"
```
```   542   proof (cases "h = 0")
```
```   543     assume "h \<noteq> 0"
```
```   544     from min obtain d where d1: "0 < d" and d2: "\<forall>y\<in>ball x d. f x \<le> f y"
```
```   545       unfolding eventually_at by (force simp: dist_commute)
```
```   546     have "FDERIV (\<lambda>r. x + r *\<^sub>R h) 0 :> (\<lambda>r. r *\<^sub>R h)"
```
```   547       by (intro derivative_eq_intros) auto
```
```   548     then have "FDERIV (\<lambda>r. f (x + r *\<^sub>R h)) 0 :> (\<lambda>k. f' (k *\<^sub>R h))"
```
```   549       by (rule has_derivative_compose, simp add: deriv)
```
```   550     then have "DERIV (\<lambda>r. f (x + r *\<^sub>R h)) 0 :> f' h"
```
```   551       unfolding has_field_derivative_def by (simp add: f'.scaleR mult_commute_abs)
```
```   552     moreover have "0 < d / norm h" using d1 and `h \<noteq> 0` by simp
```
```   553     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)"
```
```   554       using `h \<noteq> 0` by (auto simp add: d2 dist_norm pos_less_divide_eq)
```
```   555     ultimately show "f' h = 0"
```
```   556       by (rule DERIV_local_min)
```
```   557   qed (simp add: f'.zero)
```
```   558 qed
```
```   559
```
```   560 lemma has_derivative_local_max:
```
```   561   fixes f :: "'a::real_normed_vector \<Rightarrow> real"
```
```   562   assumes "(f has_derivative f') (at x)"
```
```   563   assumes "eventually (\<lambda>y. f y \<le> f x) (at x)"
```
```   564   shows "f' = (\<lambda>h. 0)"
```
```   565   using has_derivative_local_min [of "\<lambda>x. - f x" "\<lambda>h. - f' h" "x"]
```
```   566   using assms unfolding fun_eq_iff by simp
```
```   567
```
```   568 lemma differential_zero_maxmin:
```
```   569   fixes f::"'a::real_normed_vector \<Rightarrow> real"
```
```   570   assumes "x \<in> s"
```
```   571     and "open s"
```
```   572     and deriv: "(f has_derivative f') (at x)"
```
```   573     and mono: "(\<forall>y\<in>s. f y \<le> f x) \<or> (\<forall>y\<in>s. f x \<le> f y)"
```
```   574   shows "f' = (\<lambda>v. 0)"
```
```   575   using mono
```
```   576 proof
```
```   577   assume "\<forall>y\<in>s. f y \<le> f x"
```
```   578   with `x \<in> s` and `open s` have "eventually (\<lambda>y. f y \<le> f x) (at x)"
```
```   579     unfolding eventually_at_topological by auto
```
```   580   with deriv show ?thesis
```
```   581     by (rule has_derivative_local_max)
```
```   582 next
```
```   583   assume "\<forall>y\<in>s. f x \<le> f y"
```
```   584   with `x \<in> s` and `open s` have "eventually (\<lambda>y. f x \<le> f y) (at x)"
```
```   585     unfolding eventually_at_topological by auto
```
```   586   with deriv show ?thesis
```
```   587     by (rule has_derivative_local_min)
```
```   588 qed
```
```   589
```
```   590 lemma differential_zero_maxmin_component: (* TODO: delete? *)
```
```   591   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
```
```   592   assumes k: "k \<in> Basis"
```
```   593     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)"
```
```   594     and diff: "f differentiable (at x)"
```
```   595   shows "(\<Sum>j\<in>Basis. (frechet_derivative f (at x) j \<bullet> k) *\<^sub>R j) = (0::'a)" (is "?D k = 0")
```
```   596 proof -
```
```   597   let ?f' = "frechet_derivative f (at x)"
```
```   598   have "x \<in> ball x e" using `0 < e` by simp
```
```   599   moreover have "open (ball x e)" by simp
```
```   600   moreover have "((\<lambda>x. f x \<bullet> k) has_derivative (\<lambda>h. ?f' h \<bullet> k)) (at x)"
```
```   601     using bounded_linear_inner_left diff[unfolded frechet_derivative_works]
```
```   602     by (rule bounded_linear.has_derivative)
```
```   603   ultimately have "(\<lambda>h. frechet_derivative f (at x) h \<bullet> k) = (\<lambda>v. 0)"
```
```   604     using ball(2) by (rule differential_zero_maxmin)
```
```   605   then show ?thesis
```
```   606     unfolding fun_eq_iff by simp
```
```   607 qed
```
```   608
```
```   609 lemma rolle:
```
```   610   fixes f :: "real \<Rightarrow> real"
```
```   611   assumes "a < b"
```
```   612     and "f a = f b"
```
```   613     and "continuous_on {a .. b} f"
```
```   614     and "\<forall>x\<in>{a <..< b}. (f has_derivative f' x) (at x)"
```
```   615   shows "\<exists>x\<in>{a <..< b}. f' x = (\<lambda>v. 0)"
```
```   616 proof -
```
```   617   have "\<exists>x\<in>box a b. (\<forall>y\<in>box a b. f x \<le> f y) \<or> (\<forall>y\<in>box a b. f y \<le> f x)"
```
```   618   proof -
```
```   619     have "(a + b) / 2 \<in> {a .. b}"
```
```   620       using assms(1) by auto
```
```   621     then have *: "{a .. b} \<noteq> {}"
```
```   622       by auto
```
```   623     obtain d where d:
```
```   624         "d \<in>cbox a b"
```
```   625         "\<forall>y\<in>cbox a b. f y \<le> f d"
```
```   626       using continuous_attains_sup[OF compact_Icc * assms(3)] by auto
```
```   627     obtain c where c:
```
```   628         "c \<in> cbox a b"
```
```   629         "\<forall>y\<in>cbox a b. f c \<le> f y"
```
```   630       using continuous_attains_inf[OF compact_Icc * assms(3)] by auto
```
```   631     show ?thesis
```
```   632     proof (cases "d \<in> box a b \<or> c \<in> box a b")
```
```   633       case True
```
```   634       then show ?thesis
```
```   635         by (metis c(2) d(2) box_subset_cbox subset_iff)
```
```   636     next
```
```   637       def e \<equiv> "(a + b) /2"
```
```   638       case False
```
```   639       then have "f d = f c"
```
```   640         using d c assms(2) by auto
```
```   641       then have "\<And>x. x \<in> {a..b} \<Longrightarrow> f x = f d"
```
```   642         using c d
```
```   643         by force
```
```   644       then show ?thesis
```
```   645         apply (rule_tac x=e in bexI)
```
```   646         unfolding e_def
```
```   647         using assms(1)
```
```   648         apply auto
```
```   649         done
```
```   650     qed
```
```   651   qed
```
```   652   then obtain x where x: "x \<in> {a <..< b}" "(\<forall>y\<in>{a <..< b}. f x \<le> f y) \<or> (\<forall>y\<in>{a <..< b}. f y \<le> f x)"
```
```   653     by auto
```
```   654   then have "f' x = (\<lambda>v. 0)"
```
```   655     apply (rule_tac differential_zero_maxmin[of x "box a b" f "f' x"])
```
```   656     using assms
```
```   657     apply auto
```
```   658     done
```
```   659   then show ?thesis
```
```   660     by (metis x(1))
```
```   661 qed
```
```   662
```
```   663
```
```   664 subsection {* One-dimensional mean value theorem *}
```
```   665
```
```   666 lemma mvt:
```
```   667   fixes f :: "real \<Rightarrow> real"
```
```   668   assumes "a < b"
```
```   669     and "continuous_on {a..b} f"
```
```   670   assumes "\<forall>x\<in>{a<..<b}. (f has_derivative (f' x)) (at x)"
```
```   671   shows "\<exists>x\<in>{a<..<b}. f b - f a = (f' x) (b - a)"
```
```   672 proof -
```
```   673   have "\<exists>x\<in>{a <..< b}. (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)"
```
```   674   proof (intro rolle[OF assms(1), of "\<lambda>x. f x - (f b - f a) / (b - a) * x"] ballI)
```
```   675     fix x
```
```   676     assume x: "x \<in> {a <..< b}"
```
```   677     show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative
```
```   678         (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)"
```
```   679       by (intro derivative_intros assms(3)[rule_format,OF x])
```
```   680   qed (insert assms(1,2), auto intro!: continuous_intros simp: field_simps)
```
```   681   then obtain x where
```
```   682     "x \<in> {a <..< b}"
```
```   683     "(\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)" ..
```
```   684   then show ?thesis
```
```   685     by (metis (erased, hide_lams) assms(1) diff_less_iff(1) eq_iff_diff_eq_0
```
```   686       linordered_field_class.sign_simps(41) nonzero_mult_divide_cancel_right not_real_square_gt_zero
```
```   687       times_divide_eq_left)
```
```   688 qed
```
```   689
```
```   690 lemma mvt_simple:
```
```   691   fixes f :: "real \<Rightarrow> real"
```
```   692   assumes "a < b"
```
```   693     and "\<forall>x\<in>{a..b}. (f has_derivative f' x) (at x within {a..b})"
```
```   694   shows "\<exists>x\<in>{a<..<b}. f b - f a = f' x (b - a)"
```
```   695 proof (rule mvt)
```
```   696   have "f differentiable_on {a..b}"
```
```   697     using assms(2) unfolding differentiable_on_def differentiable_def by fast
```
```   698   then show "continuous_on {a..b} f"
```
```   699     by (rule differentiable_imp_continuous_on)
```
```   700   show "\<forall>x\<in>{a<..<b}. (f has_derivative f' x) (at x)"
```
```   701   proof
```
```   702     fix x
```
```   703     assume x: "x \<in> {a <..< b}"
```
```   704     show "(f has_derivative f' x) (at x)"
```
```   705       unfolding at_within_open[OF x open_greaterThanLessThan,symmetric]
```
```   706       apply (rule has_derivative_within_subset)
```
```   707       apply (rule assms(2)[rule_format])
```
```   708       using x
```
```   709       apply auto
```
```   710       done
```
```   711   qed
```
```   712 qed (rule assms(1))
```
```   713
```
```   714 lemma mvt_very_simple:
```
```   715   fixes f :: "real \<Rightarrow> real"
```
```   716   assumes "a \<le> b"
```
```   717     and "\<forall>x\<in>{a .. b}. (f has_derivative f' x) (at x within {a .. b})"
```
```   718   shows "\<exists>x\<in>{a .. b}. f b - f a = f' x (b - a)"
```
```   719 proof (cases "a = b")
```
```   720   interpret bounded_linear "f' b"
```
```   721     using assms(2) assms(1) by auto
```
```   722   case True
```
```   723   then show ?thesis
```
```   724     apply (rule_tac x=a in bexI)
```
```   725     using assms(2)[THEN bspec[where x=a]]
```
```   726     unfolding has_derivative_def
```
```   727     unfolding True
```
```   728     using zero
```
```   729     apply auto
```
```   730     done
```
```   731 next
```
```   732   case False
```
```   733   then show ?thesis
```
```   734     using mvt_simple[OF _ assms(2)]
```
```   735     using assms(1)
```
```   736     by auto
```
```   737 qed
```
```   738
```
```   739 text {* A nice generalization (see Havin's proof of 5.19 from Rudin's book). *}
```
```   740
```
```   741 lemma mvt_general:
```
```   742   fixes f :: "real \<Rightarrow> 'a::real_inner"
```
```   743   assumes "a < b"
```
```   744     and "continuous_on {a .. b} f"
```
```   745     and "\<forall>x\<in>{a<..<b}. (f has_derivative f'(x)) (at x)"
```
```   746   shows "\<exists>x\<in>{a<..<b}. norm (f b - f a) \<le> norm (f' x (b - a))"
```
```   747 proof -
```
```   748   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)"
```
```   749     apply (rule mvt)
```
```   750     apply (rule assms(1))
```
```   751     apply (intro continuous_intros assms(2))
```
```   752     using assms(3)
```
```   753     apply (fast intro: has_derivative_inner_right)
```
```   754     done
```
```   755   then obtain x where x:
```
```   756     "x \<in> {a<..<b}"
```
```   757     "(f b - f a) \<bullet> f b - (f b - f a) \<bullet> f a = (f b - f a) \<bullet> f' x (b - a)" ..
```
```   758   show ?thesis
```
```   759   proof (cases "f a = f b")
```
```   760     case False
```
```   761     have "norm (f b - f a) * norm (f b - f a) = (norm (f b - f a))\<^sup>2"
```
```   762       by (simp add: power2_eq_square)
```
```   763     also have "\<dots> = (f b - f a) \<bullet> (f b - f a)"
```
```   764       unfolding power2_norm_eq_inner ..
```
```   765     also have "\<dots> = (f b - f a) \<bullet> f' x (b - a)"
```
```   766       using x(2) by (simp only: inner_diff_right)
```
```   767     also have "\<dots> \<le> norm (f b - f a) * norm (f' x (b - a))"
```
```   768       by (rule norm_cauchy_schwarz)
```
```   769     finally show ?thesis
```
```   770       using False x(1)
```
```   771       by (auto simp add: mult_left_cancel)
```
```   772   next
```
```   773     case True
```
```   774     then show ?thesis
```
```   775       using assms(1)
```
```   776       apply (rule_tac x="(a + b) /2" in bexI)
```
```   777       apply auto
```
```   778       done
```
```   779   qed
```
```   780 qed
```
```   781
```
```   782 text {* Still more general bound theorem. *}
```
```   783
```
```   784 lemma differentiable_bound:
```
```   785   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_inner"
```
```   786   assumes "convex s"
```
```   787     and "\<forall>x\<in>s. (f has_derivative f' x) (at x within s)"
```
```   788     and "\<forall>x\<in>s. onorm (f' x) \<le> B"
```
```   789     and x: "x \<in> s"
```
```   790     and y: "y \<in> s"
```
```   791   shows "norm (f x - f y) \<le> B * norm (x - y)"
```
```   792 proof -
```
```   793   let ?p = "\<lambda>u. x + u *\<^sub>R (y - x)"
```
```   794   have *: "\<And>u. u\<in>{0..1} \<Longrightarrow> x + u *\<^sub>R (y - x) \<in> s"
```
```   795     using assms(1)[unfolded convex_alt,rule_format,OF x y]
```
```   796     unfolding scaleR_left_diff_distrib scaleR_right_diff_distrib
```
```   797     by (auto simp add: algebra_simps)
```
```   798   then have 1: "continuous_on {0 .. 1} (f \<circ> ?p)"
```
```   799     apply -
```
```   800     apply (rule continuous_intros)+
```
```   801     unfolding continuous_on_eq_continuous_within
```
```   802     apply rule
```
```   803     apply (rule differentiable_imp_continuous_within)
```
```   804     unfolding differentiable_def
```
```   805     apply (rule_tac x="f' xa" in exI)
```
```   806     apply (rule has_derivative_within_subset)
```
```   807     apply (rule assms(2)[rule_format])
```
```   808     apply auto
```
```   809     done
```
```   810   have 2: "\<forall>u\<in>{0 <..< 1}.
```
```   811     ((f \<circ> ?p) has_derivative f' (x + u *\<^sub>R (y - x)) \<circ> (\<lambda>u. 0 + u *\<^sub>R (y - x))) (at u)"
```
```   812   proof rule
```
```   813     case goal1
```
```   814     let ?u = "x + u *\<^sub>R (y - x)"
```
```   815     have "(f \<circ> ?p has_derivative (f' ?u) \<circ> (\<lambda>u. 0 + u *\<^sub>R (y - x))) (at u within box 0 1)"
```
```   816       apply (rule diff_chain_within)
```
```   817       apply (rule derivative_intros)+
```
```   818       apply (rule has_derivative_within_subset)
```
```   819       apply (rule assms(2)[rule_format])
```
```   820       using goal1 *
```
```   821       apply auto
```
```   822       done
```
```   823     then show ?case
```
```   824       by (simp add: has_derivative_within_open[OF goal1 open_greaterThanLessThan])
```
```   825   qed
```
```   826   obtain u where u:
```
```   827       "u \<in> {0<..<1}"
```
```   828       "norm ((f \<circ> (\<lambda>u. x + u *\<^sub>R (y - x))) 1 - (f \<circ> (\<lambda>u. x + u *\<^sub>R (y - x))) 0)
```
```   829         \<le> norm ((f' (x + u *\<^sub>R (y - x)) \<circ> (\<lambda>u. 0 + u *\<^sub>R (y - x))) (1 - 0))"
```
```   830     using mvt_general[OF zero_less_one 1 2] ..
```
```   831   have **: "\<And>x y. x \<in> s \<Longrightarrow> norm (f' x y) \<le> B * norm y"
```
```   832   proof -
```
```   833     case goal1
```
```   834     have "norm (f' x y) \<le> onorm (f' x) * norm y"
```
```   835       by (rule onorm[OF has_derivative_bounded_linear[OF assms(2)[rule_format,OF goal1]]])
```
```   836     also have "\<dots> \<le> B * norm y"
```
```   837       apply (rule mult_right_mono)
```
```   838       using assms(3)[rule_format,OF goal1]
```
```   839       apply (auto simp add: field_simps)
```
```   840       done
```
```   841     finally show ?case
```
```   842       by simp
```
```   843   qed
```
```   844   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)"
```
```   845     by (auto simp add: norm_minus_commute)
```
```   846   also have "\<dots> \<le> norm (f' (x + u *\<^sub>R (y - x)) (y - x))"
```
```   847     using u by auto
```
```   848   also have "\<dots> \<le> B * norm(y - x)"
```
```   849     apply (rule **)
```
```   850     using * and u
```
```   851     apply auto
```
```   852     done
```
```   853   finally show ?thesis
```
```   854     by (auto simp add: norm_minus_commute)
```
```   855 qed
```
```   856
```
```   857 text {* In particular. *}
```
```   858
```
```   859 lemma has_derivative_zero_constant:
```
```   860   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_inner"
```
```   861   assumes "convex s"
```
```   862     and "\<And>x. x \<in> s \<Longrightarrow> (f has_derivative (\<lambda>h. 0)) (at x within s)"
```
```   863   shows "\<exists>c. \<forall>x\<in>s. f x = c"
```
```   864 proof -
```
```   865   { fix x y assume "x \<in> s" "y \<in> s"
```
```   866     then have "norm (f x - f y) \<le> 0 * norm (x - y)"
```
```   867       using assms by (intro differentiable_bound[of s]) (auto simp: onorm_zero)
```
```   868     then have "f x = f y"
```
```   869       by simp }
```
```   870   then show ?thesis
```
```   871     by metis
```
```   872 qed
```
```   873
```
```   874 lemma has_derivative_zero_unique:
```
```   875   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_inner"
```
```   876   assumes "convex s"
```
```   877     and "\<And>x. x \<in> s \<Longrightarrow> (f has_derivative (\<lambda>h. 0)) (at x within s)"
```
```   878     and "x \<in> s" "y \<in> s"
```
```   879   shows "f x = f y"
```
```   880   using has_derivative_zero_constant[OF assms(1,2)] assms(3-) by force
```
```   881
```
```   882 lemma has_derivative_zero_unique_connected:
```
```   883   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_inner"
```
```   884   assumes "open s" "connected s"
```
```   885   assumes f: "\<And>x. x \<in> s \<Longrightarrow> (f has_derivative (\<lambda>x. 0)) (at x)"
```
```   886   assumes "x \<in> s" "y \<in> s"
```
```   887   shows "f x = f y"
```
```   888 proof (rule connected_local_const[where f=f, OF `connected s` `x\<in>s` `y\<in>s`])
```
```   889   show "\<forall>a\<in>s. eventually (\<lambda>b. f a = f b) (at a within s)"
```
```   890   proof
```
```   891     fix a assume "a \<in> s"
```
```   892     with `open s` obtain e where "0 < e" "ball a e \<subseteq> s"
```
```   893       by (rule openE)
```
```   894     then have "\<exists>c. \<forall>x\<in>ball a e. f x = c"
```
```   895       by (intro has_derivative_zero_constant)
```
```   896          (auto simp: at_within_open[OF _ open_ball] f convex_ball)
```
```   897     with `0<e` have "\<forall>x\<in>ball a e. f a = f x"
```
```   898       by auto
```
```   899     then show "eventually (\<lambda>b. f a = f b) (at a within s)"
```
```   900       using `0<e` unfolding eventually_at_topological
```
```   901       by (intro exI[of _ "ball a e"]) auto
```
```   902   qed
```
```   903 qed
```
```   904
```
```   905 subsection {* Differentiability of inverse function (most basic form) *}
```
```   906
```
```   907 lemma has_derivative_inverse_basic:
```
```   908   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
```
```   909   assumes "(f has_derivative f') (at (g y))"
```
```   910     and "bounded_linear g'"
```
```   911     and "g' \<circ> f' = id"
```
```   912     and "continuous (at y) g"
```
```   913     and "open t"
```
```   914     and "y \<in> t"
```
```   915     and "\<forall>z\<in>t. f (g z) = z"
```
```   916   shows "(g has_derivative g') (at y)"
```
```   917 proof -
```
```   918   interpret f': bounded_linear f'
```
```   919     using assms unfolding has_derivative_def by auto
```
```   920   interpret g': bounded_linear g'
```
```   921     using assms by auto
```
```   922   obtain C where C: "0 < C" "\<And>x. norm (g' x) \<le> norm x * C"
```
```   923     using bounded_linear.pos_bounded[OF assms(2)] by blast
```
```   924   have lem1: "\<forall>e>0. \<exists>d>0. \<forall>z.
```
```   925     norm (z - y) < d \<longrightarrow> norm (g z - g y - g'(z - y)) \<le> e * norm (g z - g y)"
```
```   926   proof (rule, rule)
```
```   927     case goal1
```
```   928     have *: "e / C > 0" using `e > 0` C(1) by auto
```
```   929     obtain d0 where d0:
```
```   930         "0 < d0"
```
```   931         "\<forall>ya. norm (ya - g y) < d0 \<longrightarrow> norm (f ya - f (g y) - f' (ya - g y)) \<le> e / C * norm (ya - g y)"
```
```   932       using assms(1)
```
```   933       unfolding has_derivative_at_alt
```
```   934       using * by blast
```
```   935     obtain d1 where d1:
```
```   936         "0 < d1"
```
```   937         "\<forall>x. 0 < dist x y \<and> dist x y < d1 \<longrightarrow> dist (g x) (g y) < d0"
```
```   938       using assms(4)
```
```   939       unfolding continuous_at Lim_at
```
```   940       using d0(1) by blast
```
```   941     obtain d2 where d2:
```
```   942         "0 < d2"
```
```   943         "\<forall>ya. dist ya y < d2 \<longrightarrow> ya \<in> t"
```
```   944       using assms(5)
```
```   945       unfolding open_dist
```
```   946       using assms(6) by blast
```
```   947     obtain d where d: "0 < d" "d < d1" "d < d2"
```
```   948       using real_lbound_gt_zero[OF d1(1) d2(1)] by blast
```
```   949     then show ?case
```
```   950       apply (rule_tac x=d in exI)
```
```   951       apply rule
```
```   952       defer
```
```   953       apply rule
```
```   954       apply rule
```
```   955     proof -
```
```   956       fix z
```
```   957       assume as: "norm (z - y) < d"
```
```   958       then have "z \<in> t"
```
```   959         using d2 d unfolding dist_norm by auto
```
```   960       have "norm (g z - g y - g' (z - y)) \<le> norm (g' (f (g z) - y - f' (g z - g y)))"
```
```   961         unfolding g'.diff f'.diff
```
```   962         unfolding assms(3)[unfolded o_def id_def, THEN fun_cong]
```
```   963         unfolding assms(7)[rule_format,OF `z\<in>t`]
```
```   964         apply (subst norm_minus_cancel[symmetric])
```
```   965         apply auto
```
```   966         done
```
```   967       also have "\<dots> \<le> norm (f (g z) - y - f' (g z - g y)) * C"
```
```   968         by (rule C(2))
```
```   969       also have "\<dots> \<le> (e / C) * norm (g z - g y) * C"
```
```   970         apply (rule mult_right_mono)
```
```   971         apply (rule d0(2)[rule_format,unfolded assms(7)[rule_format,OF `y\<in>t`]])
```
```   972         apply (cases "z = y")
```
```   973         defer
```
```   974         apply (rule d1(2)[unfolded dist_norm,rule_format])
```
```   975         using as d C d0
```
```   976         apply auto
```
```   977         done
```
```   978       also have "\<dots> \<le> e * norm (g z - g y)"
```
```   979         using C by (auto simp add: field_simps)
```
```   980       finally show "norm (g z - g y - g' (z - y)) \<le> e * norm (g z - g y)"
```
```   981         by simp
```
```   982     qed auto
```
```   983   qed
```
```   984   have *: "(0::real) < 1 / 2"
```
```   985     by auto
```
```   986   obtain d where d:
```
```   987       "0 < d"
```
```   988       "\<forall>z. norm (z - y) < d \<longrightarrow> norm (g z - g y - g' (z - y)) \<le> 1 / 2 * norm (g z - g y)"
```
```   989     using lem1 * by blast
```
```   990   def B \<equiv> "C * 2"
```
```   991   have "B > 0"
```
```   992     unfolding B_def using C by auto
```
```   993   have lem2: "\<forall>z. norm(z - y) < d \<longrightarrow> norm (g z - g y) \<le> B * norm (z - y)"
```
```   994   proof (rule, rule)
```
```   995     case goal1
```
```   996     have "norm (g z - g y) \<le> norm(g' (z - y)) + norm ((g z - g y) - g'(z - y))"
```
```   997       by (rule norm_triangle_sub)
```
```   998     also have "\<dots> \<le> norm (g' (z - y)) + 1 / 2 * norm (g z - g y)"
```
```   999       apply (rule add_left_mono)
```
```  1000       using d and goal1
```
```  1001       apply auto
```
```  1002       done
```
```  1003     also have "\<dots> \<le> norm (z - y) * C + 1 / 2 * norm (g z - g y)"
```
```  1004       apply (rule add_right_mono)
```
```  1005       using C
```
```  1006       apply auto
```
```  1007       done
```
```  1008     finally show ?case
```
```  1009       unfolding B_def
```
```  1010       by (auto simp add: field_simps)
```
```  1011   qed
```
```  1012   show ?thesis
```
```  1013     unfolding has_derivative_at_alt
```
```  1014     apply rule
```
```  1015     apply (rule assms)
```
```  1016     apply rule
```
```  1017     apply rule
```
```  1018   proof -
```
```  1019     case goal1
```
```  1020     hence *: "e / B >0" by (metis `0 < B` divide_pos_pos)
```
```  1021     obtain d' where d':
```
```  1022         "0 < d'"
```
```  1023         "\<forall>z. norm (z - y) < d' \<longrightarrow> norm (g z - g y - g' (z - y)) \<le> e / B * norm (g z - g y)"
```
```  1024       using lem1 * by blast
```
```  1025     obtain k where k: "0 < k" "k < d" "k < d'"
```
```  1026       using real_lbound_gt_zero[OF d(1) d'(1)] by blast
```
```  1027     show ?case
```
```  1028       apply (rule_tac x=k in exI)
```
```  1029       apply auto
```
```  1030     proof -
```
```  1031       fix z
```
```  1032       assume as: "norm (z - y) < k"
```
```  1033       then have "norm (g z - g y - g' (z - y)) \<le> e / B * norm(g z - g y)"
```
```  1034         using d' k by auto
```
```  1035       also have "\<dots> \<le> e * norm (z - y)"
```
```  1036         unfolding times_divide_eq_left pos_divide_le_eq[OF `B>0`]
```
```  1037         using lem2[THEN spec[where x=z]]
```
```  1038         using k as using `e > 0`
```
```  1039         by (auto simp add: field_simps)
```
```  1040       finally show "norm (g z - g y - g' (z - y)) \<le> e * norm (z - y)"
```
```  1041         by simp
```
```  1042     qed(insert k, auto)
```
```  1043   qed
```
```  1044 qed
```
```  1045
```
```  1046 text {* Simply rewrite that based on the domain point x. *}
```
```  1047
```
```  1048 lemma has_derivative_inverse_basic_x:
```
```  1049   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
```
```  1050   assumes "(f has_derivative f') (at x)"
```
```  1051     and "bounded_linear g'"
```
```  1052     and "g' \<circ> f' = id"
```
```  1053     and "continuous (at (f x)) g"
```
```  1054     and "g (f x) = x"
```
```  1055     and "open t"
```
```  1056     and "f x \<in> t"
```
```  1057     and "\<forall>y\<in>t. f (g y) = y"
```
```  1058   shows "(g has_derivative g') (at (f x))"
```
```  1059   apply (rule has_derivative_inverse_basic)
```
```  1060   using assms
```
```  1061   apply auto
```
```  1062   done
```
```  1063
```
```  1064 text {* This is the version in Dieudonne', assuming continuity of f and g. *}
```
```  1065
```
```  1066 lemma has_derivative_inverse_dieudonne:
```
```  1067   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
```
```  1068   assumes "open s"
```
```  1069     and "open (f ` s)"
```
```  1070     and "continuous_on s f"
```
```  1071     and "continuous_on (f ` s) g"
```
```  1072     and "\<forall>x\<in>s. g (f x) = x"
```
```  1073     and "x \<in> s"
```
```  1074     and "(f has_derivative f') (at x)"
```
```  1075     and "bounded_linear g'"
```
```  1076     and "g' \<circ> f' = id"
```
```  1077   shows "(g has_derivative g') (at (f x))"
```
```  1078   apply (rule has_derivative_inverse_basic_x[OF assms(7-9) _ _ assms(2)])
```
```  1079   using assms(3-6)
```
```  1080   unfolding continuous_on_eq_continuous_at[OF assms(1)] continuous_on_eq_continuous_at[OF assms(2)]
```
```  1081   apply auto
```
```  1082   done
```
```  1083
```
```  1084 text {* Here's the simplest way of not assuming much about g. *}
```
```  1085
```
```  1086 lemma has_derivative_inverse:
```
```  1087   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
```
```  1088   assumes "compact s"
```
```  1089     and "x \<in> s"
```
```  1090     and "f x \<in> interior (f ` s)"
```
```  1091     and "continuous_on s f"
```
```  1092     and "\<forall>y\<in>s. g (f y) = y"
```
```  1093     and "(f has_derivative f') (at x)"
```
```  1094     and "bounded_linear g'"
```
```  1095     and "g' \<circ> f' = id"
```
```  1096   shows "(g has_derivative g') (at (f x))"
```
```  1097 proof -
```
```  1098   {
```
```  1099     fix y
```
```  1100     assume "y \<in> interior (f ` s)"
```
```  1101     then obtain x where "x \<in> s" and *: "y = f x"
```
```  1102       unfolding image_iff
```
```  1103       using interior_subset
```
```  1104       by auto
```
```  1105     have "f (g y) = y"
```
```  1106       unfolding * and assms(5)[rule_format,OF `x\<in>s`] ..
```
```  1107   } note * = this
```
```  1108   show ?thesis
```
```  1109     apply (rule has_derivative_inverse_basic_x[OF assms(6-8)])
```
```  1110     apply (rule continuous_on_interior[OF _ assms(3)])
```
```  1111     apply (rule continuous_on_inv[OF assms(4,1)])
```
```  1112     apply (rule assms(2,5) assms(5)[rule_format] open_interior assms(3))+
```
```  1113     apply (metis *)
```
```  1114     done
```
```  1115 qed
```
```  1116
```
```  1117
```
```  1118 subsection {* Proving surjectivity via Brouwer fixpoint theorem *}
```
```  1119
```
```  1120 lemma brouwer_surjective:
```
```  1121   fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
```
```  1122   assumes "compact t"
```
```  1123     and "convex t"
```
```  1124     and "t \<noteq> {}"
```
```  1125     and "continuous_on t f"
```
```  1126     and "\<forall>x\<in>s. \<forall>y\<in>t. x + (y - f y) \<in> t"
```
```  1127     and "x \<in> s"
```
```  1128   shows "\<exists>y\<in>t. f y = x"
```
```  1129 proof -
```
```  1130   have *: "\<And>x y. f y = x \<longleftrightarrow> x + (y - f y) = y"
```
```  1131     by (auto simp add: algebra_simps)
```
```  1132   show ?thesis
```
```  1133     unfolding *
```
```  1134     apply (rule brouwer[OF assms(1-3), of "\<lambda>y. x + (y - f y)"])
```
```  1135     apply (rule continuous_intros assms)+
```
```  1136     using assms(4-6)
```
```  1137     apply auto
```
```  1138     done
```
```  1139 qed
```
```  1140
```
```  1141 lemma brouwer_surjective_cball:
```
```  1142   fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
```
```  1143   assumes "e > 0"
```
```  1144     and "continuous_on (cball a e) f"
```
```  1145     and "\<forall>x\<in>s. \<forall>y\<in>cball a e. x + (y - f y) \<in> cball a e"
```
```  1146     and "x \<in> s"
```
```  1147   shows "\<exists>y\<in>cball a e. f y = x"
```
```  1148   apply (rule brouwer_surjective)
```
```  1149   apply (rule compact_cball convex_cball)+
```
```  1150   unfolding cball_eq_empty
```
```  1151   using assms
```
```  1152   apply auto
```
```  1153   done
```
```  1154
```
```  1155 text {* See Sussmann: "Multidifferential calculus", Theorem 2.1.1 *}
```
```  1156
```
```  1157 lemma sussmann_open_mapping:
```
```  1158   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
```
```  1159   assumes "open s"
```
```  1160     and "continuous_on s f"
```
```  1161     and "x \<in> s"
```
```  1162     and "(f has_derivative f') (at x)"
```
```  1163     and "bounded_linear g'" "f' \<circ> g' = id"
```
```  1164     and "t \<subseteq> s"
```
```  1165     and "x \<in> interior t"
```
```  1166   shows "f x \<in> interior (f ` t)"
```
```  1167 proof -
```
```  1168   interpret f': bounded_linear f'
```
```  1169     using assms
```
```  1170     unfolding has_derivative_def
```
```  1171     by auto
```
```  1172   interpret g': bounded_linear g'
```
```  1173     using assms
```
```  1174     by auto
```
```  1175   obtain B where B: "0 < B" "\<forall>x. norm (g' x) \<le> norm x * B"
```
```  1176     using bounded_linear.pos_bounded[OF assms(5)] by blast
```
```  1177   hence *: "1 / (2 * B) > 0" by auto
```
```  1178   obtain e0 where e0:
```
```  1179       "0 < e0"
```
```  1180       "\<forall>y. norm (y - x) < e0 \<longrightarrow> norm (f y - f x - f' (y - x)) \<le> 1 / (2 * B) * norm (y - x)"
```
```  1181     using assms(4)
```
```  1182     unfolding has_derivative_at_alt
```
```  1183     using * by blast
```
```  1184   obtain e1 where e1: "0 < e1" "cball x e1 \<subseteq> t"
```
```  1185     using assms(8)
```
```  1186     unfolding mem_interior_cball
```
```  1187     by blast
```
```  1188   have *: "0 < e0 / B" "0 < e1 / B" using e0 e1 B by auto
```
```  1189   obtain e where e: "0 < e" "e < e0 / B" "e < e1 / B"
```
```  1190     using real_lbound_gt_zero[OF *] by blast
```
```  1191   have "\<forall>z\<in>cball (f x) (e / 2). \<exists>y\<in>cball (f x) e. f (x + g' (y - f x)) = z"
```
```  1192     apply rule
```
```  1193     apply (rule brouwer_surjective_cball[where s="cball (f x) (e/2)"])
```
```  1194     prefer 3
```
```  1195     apply rule
```
```  1196     apply rule
```
```  1197   proof-
```
```  1198     show "continuous_on (cball (f x) e) (\<lambda>y. f (x + g' (y - f x)))"
```
```  1199       unfolding g'.diff
```
```  1200       apply (rule continuous_on_compose[of _ _ f, unfolded o_def])
```
```  1201       apply (rule continuous_intros linear_continuous_on[OF assms(5)])+
```
```  1202       apply (rule continuous_on_subset[OF assms(2)])
```
```  1203       apply rule
```
```  1204       apply (unfold image_iff)
```
```  1205       apply (erule bexE)
```
```  1206     proof-
```
```  1207       fix y z
```
```  1208       assume as: "y \<in>cball (f x) e" "z = x + (g' y - g' (f x))"
```
```  1209       have "dist x z = norm (g' (f x) - g' y)"
```
```  1210         unfolding as(2) and dist_norm by auto
```
```  1211       also have "\<dots> \<le> norm (f x - y) * B"
```
```  1212         unfolding g'.diff[symmetric]
```
```  1213         using B
```
```  1214         by auto
```
```  1215       also have "\<dots> \<le> e * B"
```
```  1216         using as(1)[unfolded mem_cball dist_norm]
```
```  1217         using B
```
```  1218         by auto
```
```  1219       also have "\<dots> \<le> e1"
```
```  1220         using e
```
```  1221         unfolding less_divide_eq
```
```  1222         using B
```
```  1223         by auto
```
```  1224       finally have "z \<in> cball x e1"
```
```  1225         unfolding mem_cball
```
```  1226         by force
```
```  1227       then show "z \<in> s"
```
```  1228         using e1 assms(7) by auto
```
```  1229     qed
```
```  1230   next
```
```  1231     fix y z
```
```  1232     assume as: "y \<in> cball (f x) (e / 2)" "z \<in> cball (f x) e"
```
```  1233     have "norm (g' (z - f x)) \<le> norm (z - f x) * B"
```
```  1234       using B by auto
```
```  1235     also have "\<dots> \<le> e * B"
```
```  1236       apply (rule mult_right_mono)
```
```  1237       using as(2)[unfolded mem_cball dist_norm] and B
```
```  1238       unfolding norm_minus_commute
```
```  1239       apply auto
```
```  1240       done
```
```  1241     also have "\<dots> < e0"
```
```  1242       using e and B
```
```  1243       unfolding less_divide_eq
```
```  1244       by auto
```
```  1245     finally have *: "norm (x + g' (z - f x) - x) < e0"
```
```  1246       by auto
```
```  1247     have **: "f x + f' (x + g' (z - f x) - x) = z"
```
```  1248       using assms(6)[unfolded o_def id_def,THEN cong]
```
```  1249       by auto
```
```  1250     have "norm (f x - (y + (z - f (x + g' (z - f x))))) \<le>
```
```  1251         norm (f (x + g' (z - f x)) - z) + norm (f x - y)"
```
```  1252       using norm_triangle_ineq[of "f (x + g'(z - f x)) - z" "f x - y"]
```
```  1253       by (auto simp add: algebra_simps)
```
```  1254     also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + norm (f x - y)"
```
```  1255       using e0(2)[rule_format, OF *]
```
```  1256       unfolding algebra_simps **
```
```  1257       by auto
```
```  1258     also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + e/2"
```
```  1259       using as(1)[unfolded mem_cball dist_norm]
```
```  1260       by auto
```
```  1261     also have "\<dots> \<le> 1 / (B * 2) * B * norm (z - f x) + e/2"
```
```  1262       using * and B
```
```  1263       by (auto simp add: field_simps)
```
```  1264     also have "\<dots> \<le> 1 / 2 * norm (z - f x) + e/2"
```
```  1265       by auto
```
```  1266     also have "\<dots> \<le> e/2 + e/2"
```
```  1267       apply (rule add_right_mono)
```
```  1268       using as(2)[unfolded mem_cball dist_norm]
```
```  1269       unfolding norm_minus_commute
```
```  1270       apply auto
```
```  1271       done
```
```  1272     finally show "y + (z - f (x + g' (z - f x))) \<in> cball (f x) e"
```
```  1273       unfolding mem_cball dist_norm
```
```  1274       by auto
```
```  1275   qed (insert e, auto) note lem = this
```
```  1276   show ?thesis
```
```  1277     unfolding mem_interior
```
```  1278     apply (rule_tac x="e/2" in exI)
```
```  1279     apply rule
```
```  1280     apply (rule divide_pos_pos)
```
```  1281     prefer 3
```
```  1282   proof
```
```  1283     fix y
```
```  1284     assume "y \<in> ball (f x) (e / 2)"
```
```  1285     then have *: "y \<in> cball (f x) (e / 2)"
```
```  1286       by auto
```
```  1287     obtain z where z: "z \<in> cball (f x) e" "f (x + g' (z - f x)) = y"
```
```  1288       using lem * by blast
```
```  1289     then have "norm (g' (z - f x)) \<le> norm (z - f x) * B"
```
```  1290       using B
```
```  1291       by (auto simp add: field_simps)
```
```  1292     also have "\<dots> \<le> e * B"
```
```  1293       apply (rule mult_right_mono)
```
```  1294       using z(1)
```
```  1295       unfolding mem_cball dist_norm norm_minus_commute
```
```  1296       using B
```
```  1297       apply auto
```
```  1298       done
```
```  1299     also have "\<dots> \<le> e1"
```
```  1300       using e B unfolding less_divide_eq by auto
```
```  1301     finally have "x + g'(z - f x) \<in> t"
```
```  1302       apply -
```
```  1303       apply (rule e1(2)[unfolded subset_eq,rule_format])
```
```  1304       unfolding mem_cball dist_norm
```
```  1305       apply auto
```
```  1306       done
```
```  1307     then show "y \<in> f ` t"
```
```  1308       using z by auto
```
```  1309   qed (insert e, auto)
```
```  1310 qed
```
```  1311
```
```  1312 text {* Hence the following eccentric variant of the inverse function theorem.
```
```  1313   This has no continuity assumptions, but we do need the inverse function.
```
```  1314   We could put @{text "f' \<circ> g = I"} but this happens to fit with the minimal linear
```
```  1315   algebra theory I've set up so far. *}
```
```  1316
```
```  1317 (* move  before left_inverse_linear in Euclidean_Space*)
```
```  1318
```
```  1319 lemma right_inverse_linear:
```
```  1320   fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
```
```  1321   assumes lf: "linear f"
```
```  1322     and gf: "f \<circ> g = id"
```
```  1323   shows "linear g"
```
```  1324 proof -
```
```  1325   from gf have fi: "surj f"
```
```  1326     by (auto simp add: surj_def o_def id_def) metis
```
```  1327   from linear_surjective_isomorphism[OF lf fi]
```
```  1328   obtain h:: "'a \<Rightarrow> 'a" where h: "linear h" "\<forall>x. h (f x) = x" "\<forall>x. f (h x) = x"
```
```  1329     by blast
```
```  1330   have "h = g"
```
```  1331     apply (rule ext)
```
```  1332     using gf h(2,3)
```
```  1333     apply (simp add: o_def id_def fun_eq_iff)
```
```  1334     apply metis
```
```  1335     done
```
```  1336   with h(1) show ?thesis by blast
```
```  1337 qed
```
```  1338
```
```  1339 lemma has_derivative_inverse_strong:
```
```  1340   fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
```
```  1341   assumes "open s"
```
```  1342     and "x \<in> s"
```
```  1343     and "continuous_on s f"
```
```  1344     and "\<forall>x\<in>s. g (f x) = x"
```
```  1345     and "(f has_derivative f') (at x)"
```
```  1346     and "f' \<circ> g' = id"
```
```  1347   shows "(g has_derivative g') (at (f x))"
```
```  1348 proof -
```
```  1349   have linf: "bounded_linear f'"
```
```  1350     using assms(5) unfolding has_derivative_def by auto
```
```  1351   then have ling: "bounded_linear g'"
```
```  1352     unfolding linear_conv_bounded_linear[symmetric]
```
```  1353     apply -
```
```  1354     apply (rule right_inverse_linear)
```
```  1355     using assms(6)
```
```  1356     apply auto
```
```  1357     done
```
```  1358   moreover have "g' \<circ> f' = id"
```
```  1359     using assms(6) linf ling
```
```  1360     unfolding linear_conv_bounded_linear[symmetric]
```
```  1361     using linear_inverse_left
```
```  1362     by auto
```
```  1363   moreover have *:"\<forall>t\<subseteq>s. x \<in> interior t \<longrightarrow> f x \<in> interior (f ` t)"
```
```  1364     apply clarify
```
```  1365     apply (rule sussmann_open_mapping)
```
```  1366     apply (rule assms ling)+
```
```  1367     apply auto
```
```  1368     done
```
```  1369   have "continuous (at (f x)) g"
```
```  1370     unfolding continuous_at Lim_at
```
```  1371   proof (rule, rule)
```
```  1372     fix e :: real
```
```  1373     assume "e > 0"
```
```  1374     then have "f x \<in> interior (f ` (ball x e \<inter> s))"
```
```  1375       using *[rule_format,of "ball x e \<inter> s"] `x \<in> s`
```
```  1376       by (auto simp add: interior_open[OF open_ball] interior_open[OF assms(1)])
```
```  1377     then obtain d where d: "0 < d" "ball (f x) d \<subseteq> f ` (ball x e \<inter> s)"
```
```  1378       unfolding mem_interior by blast
```
```  1379     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"
```
```  1380       apply (rule_tac x=d in exI)
```
```  1381       apply rule
```
```  1382       apply (rule d(1))
```
```  1383       apply rule
```
```  1384       apply rule
```
```  1385     proof -
```
```  1386       case goal1
```
```  1387       then have "g y \<in> g ` f ` (ball x e \<inter> s)"
```
```  1388         using d(2)[unfolded subset_eq,THEN bspec[where x=y]]
```
```  1389         by (auto simp add: dist_commute)
```
```  1390       then have "g y \<in> ball x e \<inter> s"
```
```  1391         using assms(4) by auto
```
```  1392       then show "dist (g y) (g (f x)) < e"
```
```  1393         using assms(4)[rule_format,OF `x \<in> s`]
```
```  1394         by (auto simp add: dist_commute)
```
```  1395     qed
```
```  1396   qed
```
```  1397   moreover have "f x \<in> interior (f ` s)"
```
```  1398     apply (rule sussmann_open_mapping)
```
```  1399     apply (rule assms ling)+
```
```  1400     using interior_open[OF assms(1)] and `x \<in> s`
```
```  1401     apply auto
```
```  1402     done
```
```  1403   moreover have "\<And>y. y \<in> interior (f ` s) \<Longrightarrow> f (g y) = y"
```
```  1404   proof -
```
```  1405     case goal1
```
```  1406     then have "y \<in> f ` s"
```
```  1407       using interior_subset by auto
```
```  1408     then obtain z where "z \<in> s" "y = f z" unfolding image_iff ..
```
```  1409     then show ?case
```
```  1410       using assms(4) by auto
```
```  1411   qed
```
```  1412   ultimately show ?thesis using assms
```
```  1413     by (metis has_derivative_inverse_basic_x open_interior)
```
```  1414 qed
```
```  1415
```
```  1416 text {* A rewrite based on the other domain. *}
```
```  1417
```
```  1418 lemma has_derivative_inverse_strong_x:
```
```  1419   fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
```
```  1420   assumes "open s"
```
```  1421     and "g y \<in> s"
```
```  1422     and "continuous_on s f"
```
```  1423     and "\<forall>x\<in>s. g (f x) = x"
```
```  1424     and "(f has_derivative f') (at (g y))"
```
```  1425     and "f' \<circ> g' = id"
```
```  1426     and "f (g y) = y"
```
```  1427   shows "(g has_derivative g') (at y)"
```
```  1428   using has_derivative_inverse_strong[OF assms(1-6)]
```
```  1429   unfolding assms(7)
```
```  1430   by simp
```
```  1431
```
```  1432 text {* On a region. *}
```
```  1433
```
```  1434 lemma has_derivative_inverse_on:
```
```  1435   fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
```
```  1436   assumes "open s"
```
```  1437     and "\<forall>x\<in>s. (f has_derivative f'(x)) (at x)"
```
```  1438     and "\<forall>x\<in>s. g (f x) = x"
```
```  1439     and "f' x \<circ> g' x = id"
```
```  1440     and "x \<in> s"
```
```  1441   shows "(g has_derivative g'(x)) (at (f x))"
```
```  1442   apply (rule has_derivative_inverse_strong[where g'="g' x" and f=f])
```
```  1443   apply (rule assms)+
```
```  1444   unfolding continuous_on_eq_continuous_at[OF assms(1)]
```
```  1445   apply rule
```
```  1446   apply (rule differentiable_imp_continuous_within)
```
```  1447   unfolding differentiable_def
```
```  1448   using assms
```
```  1449   apply auto
```
```  1450   done
```
```  1451
```
```  1452 text {* Invertible derivative continous at a point implies local
```
```  1453 injectivity. It's only for this we need continuity of the derivative,
```
```  1454 except of course if we want the fact that the inverse derivative is
```
```  1455 also continuous. So if we know for some other reason that the inverse
```
```  1456 function exists, it's OK. *}
```
```  1457
```
```  1458 lemma bounded_linear_sub: "bounded_linear f \<Longrightarrow> bounded_linear g \<Longrightarrow> bounded_linear (\<lambda>x. f x - g x)"
```
```  1459   using bounded_linear_add[of f "\<lambda>x. - g x"] bounded_linear_minus[of g]
```
```  1460   by (auto simp add: algebra_simps)
```
```  1461
```
```  1462 lemma has_derivative_locally_injective:
```
```  1463   fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
```
```  1464   assumes "a \<in> s"
```
```  1465     and "open s"
```
```  1466     and "bounded_linear g'"
```
```  1467     and "g' \<circ> f' a = id"
```
```  1468     and "\<forall>x\<in>s. (f has_derivative f' x) (at x)"
```
```  1469     and "\<forall>e>0. \<exists>d>0. \<forall>x. dist a x < d \<longrightarrow> onorm (\<lambda>v. f' x v - f' a v) < e"
```
```  1470   obtains t where "a \<in> t" "open t" "\<forall>x\<in>t. \<forall>x'\<in>t. f x' = f x \<longrightarrow> x' = x"
```
```  1471 proof -
```
```  1472   interpret bounded_linear g'
```
```  1473     using assms by auto
```
```  1474   note f'g' = assms(4)[unfolded id_def o_def,THEN cong]
```
```  1475   have "g' (f' a (\<Sum>Basis)) = (\<Sum>Basis)" "(\<Sum>Basis) \<noteq> (0::'n)"
```
```  1476     defer
```
```  1477     apply (subst euclidean_eq_iff)
```
```  1478     using f'g'
```
```  1479     apply auto
```
```  1480     done
```
```  1481   then have *: "0 < onorm g'"
```
```  1482     unfolding onorm_pos_lt[OF assms(3)]
```
```  1483     by fastforce
```
```  1484   def k \<equiv> "1 / onorm g' / 2"
```
```  1485   have *: "k > 0"
```
```  1486     unfolding k_def using * by auto
```
```  1487   obtain d1 where d1:
```
```  1488       "0 < d1"
```
```  1489       "\<And>x. dist a x < d1 \<Longrightarrow> onorm (\<lambda>v. f' x v - f' a v) < k"
```
```  1490     using assms(6) * by blast
```
```  1491   from `open s` obtain d2 where "d2 > 0" "ball a d2 \<subseteq> s"
```
```  1492     using `a\<in>s` ..
```
```  1493   obtain d2 where "d2 > 0" "ball a d2 \<subseteq> s"
```
```  1494     using assms(2,1) ..
```
```  1495   obtain d2 where d2: "0 < d2" "ball a d2 \<subseteq> s"
```
```  1496     using assms(2)
```
```  1497     unfolding open_contains_ball
```
```  1498     using `a\<in>s` by blast
```
```  1499   obtain d where d: "0 < d" "d < d1" "d < d2"
```
```  1500     using real_lbound_gt_zero[OF d1(1) d2(1)] by blast
```
```  1501   show ?thesis
```
```  1502   proof
```
```  1503     show "a \<in> ball a d"
```
```  1504       using d by auto
```
```  1505     show "\<forall>x\<in>ball a d. \<forall>x'\<in>ball a d. f x' = f x \<longrightarrow> x' = x"
```
```  1506     proof (intro strip)
```
```  1507       fix x y
```
```  1508       assume as: "x \<in> ball a d" "y \<in> ball a d" "f x = f y"
```
```  1509       def ph \<equiv> "\<lambda>w. w - g' (f w - f x)"
```
```  1510       have ph':"ph = g' \<circ> (\<lambda>w. f' a w - (f w - f x))"
```
```  1511         unfolding ph_def o_def
```
```  1512         unfolding diff
```
```  1513         using f'g'
```
```  1514         by (auto simp add: algebra_simps)
```
```  1515       have "norm (ph x - ph y) \<le> (1 / 2) * norm (x - y)"
```
```  1516         apply (rule differentiable_bound[OF convex_ball _ _ as(1-2), where f'="\<lambda>x v. v - g'(f' x v)"])
```
```  1517         apply (rule_tac[!] ballI)
```
```  1518       proof -
```
```  1519         fix u
```
```  1520         assume u: "u \<in> ball a d"
```
```  1521         then have "u \<in> s"
```
```  1522           using d d2 by auto
```
```  1523         have *: "(\<lambda>v. v - g' (f' u v)) = g' \<circ> (\<lambda>w. f' a w - f' u w)"
```
```  1524           unfolding o_def and diff
```
```  1525           using f'g' by auto
```
```  1526         show "(ph has_derivative (\<lambda>v. v - g' (f' u v))) (at u within ball a d)"
```
```  1527           unfolding ph' *
```
```  1528           apply (simp add: comp_def)
```
```  1529           apply (rule bounded_linear.has_derivative[OF assms(3)])
```
```  1530           apply (rule derivative_intros)
```
```  1531           defer
```
```  1532           apply (rule has_derivative_sub[where g'="\<lambda>x.0",unfolded diff_0_right])
```
```  1533           apply (rule has_derivative_at_within)
```
```  1534           using assms(5) and `u \<in> s` `a \<in> s`
```
```  1535           apply (auto intro!: derivative_intros bounded_linear.has_derivative[of _ "\<lambda>x. x"] has_derivative_bounded_linear)
```
```  1536           done
```
```  1537         have **: "bounded_linear (\<lambda>x. f' u x - f' a x)" "bounded_linear (\<lambda>x. f' a x - f' u x)"
```
```  1538           apply (rule_tac[!] bounded_linear_sub)
```
```  1539           apply (rule_tac[!] has_derivative_bounded_linear)
```
```  1540           using assms(5) `u \<in> s` `a \<in> s`
```
```  1541           apply auto
```
```  1542           done
```
```  1543         have "onorm (\<lambda>v. v - g' (f' u v)) \<le> onorm g' * onorm (\<lambda>w. f' a w - f' u w)"
```
```  1544           unfolding *
```
```  1545           apply (rule onorm_compose)
```
```  1546           apply (rule assms(3) **)+
```
```  1547           done
```
```  1548         also have "\<dots> \<le> onorm g' * k"
```
```  1549           apply (rule mult_left_mono)
```
```  1550           using d1(2)[of u]
```
```  1551           using onorm_neg[where f="\<lambda>x. f' u x - f' a x"]
```
```  1552           using d and u and onorm_pos_le[OF assms(3)]
```
```  1553           apply (auto simp add: algebra_simps)
```
```  1554           done
```
```  1555         also have "\<dots> \<le> 1 / 2"
```
```  1556           unfolding k_def by auto
```
```  1557         finally show "onorm (\<lambda>v. v - g' (f' u v)) \<le> 1 / 2" .
```
```  1558       qed
```
```  1559       moreover have "norm (ph y - ph x) = norm (y - x)"
```
```  1560         apply (rule arg_cong[where f=norm])
```
```  1561         unfolding ph_def
```
```  1562         using diff
```
```  1563         unfolding as
```
```  1564         apply auto
```
```  1565         done
```
```  1566       ultimately show "x = y"
```
```  1567         unfolding norm_minus_commute by auto
```
```  1568     qed
```
```  1569   qed auto
```
```  1570 qed
```
```  1571
```
```  1572
```
```  1573 subsection {* Uniformly convergent sequence of derivatives *}
```
```  1574
```
```  1575 lemma has_derivative_sequence_lipschitz_lemma:
```
```  1576   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::real_inner"
```
```  1577   assumes "convex s"
```
```  1578     and "\<forall>n. \<forall>x\<in>s. ((f n) has_derivative (f' n x)) (at x within s)"
```
```  1579     and "\<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
```
```  1580     and "0 \<le> e"
```
```  1581   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)"
```
```  1582 proof rule+
```
```  1583   fix m n x y
```
```  1584   assume as: "N \<le> m" "N \<le> n" "x \<in> s" "y \<in> s"
```
```  1585   show "norm ((f m x - f n x) - (f m y - f n y)) \<le> 2 * e * norm (x - y)"
```
```  1586     apply (rule differentiable_bound[where f'="\<lambda>x h. f' m x h - f' n x h", OF assms(1) _ _ as(3-4)])
```
```  1587     apply (rule_tac[!] ballI)
```
```  1588   proof -
```
```  1589     fix x
```
```  1590     assume "x \<in> s"
```
```  1591     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)"
```
```  1592       by (rule derivative_intros assms(2)[rule_format] `x\<in>s`)+
```
```  1593     show "onorm (\<lambda>h. f' m x h - f' n x h) \<le> 2 * e"
```
```  1594     proof (rule onorm_bound)
```
```  1595       fix h
```
```  1596       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)"
```
```  1597         using norm_triangle_ineq[of "f' m x h - g' x h" "- f' n x h + g' x h"]
```
```  1598         unfolding norm_minus_commute
```
```  1599         by (auto simp add: algebra_simps)
```
```  1600       also have "\<dots> \<le> e * norm h + e * norm h"
```
```  1601         using assms(3)[rule_format,OF `N \<le> m` `x \<in> s`, of h]
```
```  1602         using assms(3)[rule_format,OF `N \<le> n` `x \<in> s`, of h]
```
```  1603         by (auto simp add: field_simps)
```
```  1604       finally show "norm (f' m x h - f' n x h) \<le> 2 * e * norm h"
```
```  1605         by auto
```
```  1606     qed (simp add: `0 \<le> e`)
```
```  1607   qed
```
```  1608 qed
```
```  1609
```
```  1610 lemma has_derivative_sequence_lipschitz:
```
```  1611   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::real_inner"
```
```  1612   assumes "convex s"
```
```  1613     and "\<forall>n. \<forall>x\<in>s. ((f n) has_derivative (f' n x)) (at x within s)"
```
```  1614     and "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
```
```  1615   shows "\<forall>e>0. \<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s.
```
```  1616     norm ((f m x - f n x) - (f m y - f n y)) \<le> e * norm (x - y)"
```
```  1617 proof (rule, rule)
```
```  1618   case goal1 have *: "2 * (1/2* e) = e" "1/2 * e >0"
```
```  1619     using `e > 0` by auto
```
```  1620   obtain N where "\<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> 1 / 2 * e * norm h"
```
```  1621     using assms(3) *(2) by blast
```
```  1622   then show ?case
```
```  1623     apply (rule_tac x=N in exI)
```
```  1624     apply (rule has_derivative_sequence_lipschitz_lemma[where e="1/2 *e", unfolded *])
```
```  1625     using assms `e > 0`
```
```  1626     apply auto
```
```  1627     done
```
```  1628 qed
```
```  1629
```
```  1630 lemma has_derivative_sequence:
```
```  1631   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::{real_inner, complete_space}"
```
```  1632   assumes "convex s"
```
```  1633     and "\<forall>n. \<forall>x\<in>s. ((f n) has_derivative (f' n x)) (at x within s)"
```
```  1634     and "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
```
```  1635     and "x0 \<in> s"
```
```  1636     and "((\<lambda>n. f n x0) ---> l) sequentially"
```
```  1637   shows "\<exists>g. \<forall>x\<in>s. ((\<lambda>n. f n x) ---> g x) sequentially \<and> (g has_derivative g'(x)) (at x within s)"
```
```  1638 proof -
```
```  1639   have lem1: "\<forall>e>0. \<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s.
```
```  1640       norm ((f m x - f n x) - (f m y - f n y)) \<le> e * norm (x - y)"
```
```  1641     using assms(1,2,3) by (rule has_derivative_sequence_lipschitz)
```
```  1642   have "\<exists>g. \<forall>x\<in>s. ((\<lambda>n. f n x) ---> g x) sequentially"
```
```  1643     apply (rule bchoice)
```
```  1644     unfolding convergent_eq_cauchy
```
```  1645   proof
```
```  1646     fix x
```
```  1647     assume "x \<in> s"
```
```  1648     show "Cauchy (\<lambda>n. f n x)"
```
```  1649     proof (cases "x = x0")
```
```  1650       case True
```
```  1651       then show ?thesis
```
```  1652         using LIMSEQ_imp_Cauchy[OF assms(5)] by auto
```
```  1653     next
```
```  1654       case False
```
```  1655       show ?thesis
```
```  1656         unfolding Cauchy_def
```
```  1657       proof (rule, rule)
```
```  1658         fix e :: real
```
```  1659         assume "e > 0"
```
```  1660         hence *: "e / 2 > 0" "e / 2 / norm (x - x0) > 0" using False by auto
```
```  1661         obtain M where M: "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x0) (f n x0) < e / 2"
```
```  1662           using LIMSEQ_imp_Cauchy[OF assms(5)]
```
```  1663           unfolding Cauchy_def
```
```  1664           using *(1) by blast
```
```  1665         obtain N where N:
```
```  1666           "\<forall>m\<ge>N. \<forall>n\<ge>N.
```
```  1667             \<forall>xa\<in>s. \<forall>y\<in>s. norm (f m xa - f n xa - (f m y - f n y)) \<le>
```
```  1668               e / 2 / norm (x - x0) * norm (xa - y)"
```
```  1669         using lem1 *(2) by blast
```
```  1670         show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < e"
```
```  1671           apply (rule_tac x="max M N" in exI)
```
```  1672         proof rule+
```
```  1673           fix m n
```
```  1674           assume as: "max M N \<le>m" "max M N\<le>n"
```
```  1675           have "dist (f m x) (f n x) \<le>
```
```  1676               norm (f m x0 - f n x0) + norm (f m x - f n x - (f m x0 - f n x0))"
```
```  1677             unfolding dist_norm
```
```  1678             by (rule norm_triangle_sub)
```
```  1679           also have "\<dots> \<le> norm (f m x0 - f n x0) + e / 2"
```
```  1680             using N[rule_format,OF _ _ `x\<in>s` `x0\<in>s`, of m n] and as and False
```
```  1681             by auto
```
```  1682           also have "\<dots> < e / 2 + e / 2"
```
```  1683             apply (rule add_strict_right_mono)
```
```  1684             using as and M[rule_format]
```
```  1685             unfolding dist_norm
```
```  1686             apply auto
```
```  1687             done
```
```  1688           finally show "dist (f m x) (f n x) < e"
```
```  1689             by auto
```
```  1690         qed
```
```  1691       qed
```
```  1692     qed
```
```  1693   qed
```
```  1694   then obtain g where g: "\<forall>x\<in>s. (\<lambda>n. f n x) ----> g x" ..
```
```  1695   have lem2: "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s. norm ((f n x - f n y) - (g x - g y)) \<le> e * norm (x - y)"
```
```  1696   proof (rule, rule)
```
```  1697     fix e :: real
```
```  1698     assume *: "e > 0"
```
```  1699     obtain N where
```
```  1700       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)"
```
```  1701       using lem1 * by blast
```
```  1702     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)"
```
```  1703       apply (rule_tac x=N in exI)
```
```  1704     proof rule+
```
```  1705       fix n x y
```
```  1706       assume as: "N \<le> n" "x \<in> s" "y \<in> s"
```
```  1707       have "((\<lambda>m. norm (f n x - f n y - (f m x - f m y))) ---> norm (f n x - f n y - (g x - g y))) sequentially"
```
```  1708         by (intro tendsto_intros g[rule_format] as)
```
```  1709       moreover have "eventually (\<lambda>m. norm (f n x - f n y - (f m x - f m y)) \<le> e * norm (x - y)) sequentially"
```
```  1710         unfolding eventually_sequentially
```
```  1711         apply (rule_tac x=N in exI)
```
```  1712         apply rule
```
```  1713         apply rule
```
```  1714       proof -
```
```  1715         fix m
```
```  1716         assume "N \<le> m"
```
```  1717         then show "norm (f n x - f n y - (f m x - f m y)) \<le> e * norm (x - y)"
```
```  1718           using N[rule_format, of n m x y] and as
```
```  1719           by (auto simp add: algebra_simps)
```
```  1720       qed
```
```  1721       ultimately show "norm (f n x - f n y - (g x - g y)) \<le> e * norm (x - y)"
```
```  1722         by (rule tendsto_ge_const[OF trivial_limit_sequentially])
```
```  1723     qed
```
```  1724   qed
```
```  1725   have "\<forall>x\<in>s. ((\<lambda>n. f n x) ---> g x) sequentially \<and> (g has_derivative g' x) (at x within s)"
```
```  1726     unfolding has_derivative_within_alt2
```
```  1727   proof (intro ballI conjI)
```
```  1728     fix x
```
```  1729     assume "x \<in> s"
```
```  1730     then show "((\<lambda>n. f n x) ---> g x) sequentially"
```
```  1731       by (simp add: g)
```
```  1732     have lem3: "\<forall>u. ((\<lambda>n. f' n x u) ---> g' x u) sequentially"
```
```  1733       unfolding filterlim_def le_nhds_metric_le eventually_filtermap dist_norm
```
```  1734     proof (intro allI impI)
```
```  1735       fix u
```
```  1736       fix e :: real
```
```  1737       assume "e > 0"
```
```  1738       show "eventually (\<lambda>n. norm (f' n x u - g' x u) \<le> e) sequentially"
```
```  1739       proof (cases "u = 0")
```
```  1740         case True
```
```  1741         have "eventually (\<lambda>n. norm (f' n x u - g' x u) \<le> e * norm u) sequentially"
```
```  1742           using assms(3)[folded eventually_sequentially] and `0 < e` and `x \<in> s`
```
```  1743           by (fast elim: eventually_elim1)
```
```  1744         then show ?thesis
```
```  1745           using `u = 0` and `0 < e` by (auto elim: eventually_elim1)
```
```  1746       next
```
```  1747         case False
```
```  1748         with `0 < e` have "0 < e / norm u" by simp
```
```  1749         then have "eventually (\<lambda>n. norm (f' n x u - g' x u) \<le> e / norm u * norm u) sequentially"
```
```  1750           using assms(3)[folded eventually_sequentially] and `x \<in> s`
```
```  1751           by (fast elim: eventually_elim1)
```
```  1752         then show ?thesis
```
```  1753           using `u \<noteq> 0` by simp
```
```  1754       qed
```
```  1755     qed
```
```  1756     show "bounded_linear (g' x)"
```
```  1757     proof
```
```  1758       fix x' y z :: 'a
```
```  1759       fix c :: real
```
```  1760       note lin = assms(2)[rule_format,OF `x\<in>s`,THEN has_derivative_bounded_linear]
```
```  1761       show "g' x (c *\<^sub>R x') = c *\<^sub>R g' x x'"
```
```  1762         apply (rule tendsto_unique[OF trivial_limit_sequentially])
```
```  1763         apply (rule lem3[rule_format])
```
```  1764         unfolding lin[THEN bounded_linear.linear, THEN linear_cmul]
```
```  1765         apply (intro tendsto_intros)
```
```  1766         apply (rule lem3[rule_format])
```
```  1767         done
```
```  1768       show "g' x (y + z) = g' x y + g' x z"
```
```  1769         apply (rule tendsto_unique[OF trivial_limit_sequentially])
```
```  1770         apply (rule lem3[rule_format])
```
```  1771         unfolding lin[THEN bounded_linear.linear, THEN linear_add]
```
```  1772         apply (rule tendsto_add)
```
```  1773         apply (rule lem3[rule_format])+
```
```  1774         done
```
```  1775       obtain N where N: "\<forall>h. norm (f' N x h - g' x h) \<le> 1 * norm h"
```
```  1776         using assms(3) `x \<in> s` by (fast intro: zero_less_one)
```
```  1777       have "bounded_linear (f' N x)"
```
```  1778         using assms(2) `x \<in> s` by fast
```
```  1779       from bounded_linear.bounded [OF this]
```
```  1780       obtain K where K: "\<forall>h. norm (f' N x h) \<le> norm h * K" ..
```
```  1781       {
```
```  1782         fix h
```
```  1783         have "norm (g' x h) = norm (f' N x h - (f' N x h - g' x h))"
```
```  1784           by simp
```
```  1785         also have "\<dots> \<le> norm (f' N x h) + norm (f' N x h - g' x h)"
```
```  1786           by (rule norm_triangle_ineq4)
```
```  1787         also have "\<dots> \<le> norm h * K + 1 * norm h"
```
```  1788           using N K by (fast intro: add_mono)
```
```  1789         finally have "norm (g' x h) \<le> norm h * (K + 1)"
```
```  1790           by (simp add: ring_distribs)
```
```  1791       }
```
```  1792       then show "\<exists>K. \<forall>h. norm (g' x h) \<le> norm h * K" by fast
```
```  1793     qed
```
```  1794     show "\<forall>e>0. eventually (\<lambda>y. norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)) (at x within s)"
```
```  1795     proof (rule, rule)
```
```  1796       case goal1
```
```  1797       have *: "e / 3 > 0"
```
```  1798         using goal1 by auto
```
```  1799       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"
```
```  1800         using assms(3) * by blast
```
```  1801       obtain N2 where
```
```  1802           N2: "\<forall>n\<ge>N2. \<forall>x\<in>s. \<forall>y\<in>s. norm (f n x - f n y - (g x - g y)) \<le> e / 3 * norm (x - y)"
```
```  1803         using lem2 * by blast
```
```  1804       let ?N = "max N1 N2"
```
```  1805       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)"
```
```  1806         using assms(2)[unfolded has_derivative_within_alt2] and `x \<in> s` and * by fast
```
```  1807       moreover have "eventually (\<lambda>y. y \<in> s) (at x within s)"
```
```  1808         unfolding eventually_at by (fast intro: zero_less_one)
```
```  1809       ultimately show ?case
```
```  1810       proof (rule eventually_elim2)
```
```  1811         fix y
```
```  1812         assume "y \<in> s"
```
```  1813         assume "norm (f ?N y - f ?N x - f' ?N x (y - x)) \<le> e / 3 * norm (y - x)"
```
```  1814         moreover have "norm (g y - g x - (f ?N y - f ?N x)) \<le> e / 3 * norm (y - x)"
```
```  1815           using N2[rule_format, OF _ `y \<in> s` `x \<in> s`]
```
```  1816           by (simp add: norm_minus_commute)
```
```  1817         ultimately have "norm (g y - g x - f' ?N x (y - x)) \<le> 2 * e / 3 * norm (y - x)"
```
```  1818           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)"]
```
```  1819           by (auto simp add: algebra_simps)
```
```  1820         moreover
```
```  1821         have " norm (f' ?N x (y - x) - g' x (y - x)) \<le> e / 3 * norm (y - x)"
```
```  1822           using N1 `x \<in> s` by auto
```
```  1823         ultimately show "norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)"
```
```  1824           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)"]
```
```  1825           by (auto simp add: algebra_simps)
```
```  1826       qed
```
```  1827     qed
```
```  1828   qed
```
```  1829   then show ?thesis by fast
```
```  1830 qed
```
```  1831
```
```  1832 text {* Can choose to line up antiderivatives if we want. *}
```
```  1833
```
```  1834 lemma has_antiderivative_sequence:
```
```  1835   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::{real_inner, complete_space}"
```
```  1836   assumes "convex s"
```
```  1837     and "\<forall>n. \<forall>x\<in>s. ((f n) has_derivative (f' n x)) (at x within s)"
```
```  1838     and "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
```
```  1839   shows "\<exists>g. \<forall>x\<in>s. (g has_derivative g' x) (at x within s)"
```
```  1840 proof (cases "s = {}")
```
```  1841   case False
```
```  1842   then obtain a where "a \<in> s"
```
```  1843     by auto
```
```  1844   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"
```
```  1845     by auto
```
```  1846   show ?thesis
```
```  1847     apply (rule *)
```
```  1848     apply (rule has_derivative_sequence[OF assms(1) _ assms(3), of "\<lambda>n x. f n x + (f 0 a - f n a)"])
```
```  1849     apply (metis assms(2) has_derivative_add_const)
```
```  1850     apply (rule `a \<in> s`)
```
```  1851     apply auto
```
```  1852     done
```
```  1853 qed auto
```
```  1854
```
```  1855 lemma has_antiderivative_limit:
```
```  1856   fixes g' :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'b::{real_inner, complete_space}"
```
```  1857   assumes "convex s"
```
```  1858     and "\<forall>e>0. \<exists>f f'. \<forall>x\<in>s.
```
```  1859       (f has_derivative (f' x)) (at x within s) \<and> (\<forall>h. norm (f' x h - g' x h) \<le> e * norm h)"
```
```  1860   shows "\<exists>g. \<forall>x\<in>s. (g has_derivative g' x) (at x within s)"
```
```  1861 proof -
```
```  1862   have *: "\<forall>n. \<exists>f f'. \<forall>x\<in>s.
```
```  1863     (f has_derivative (f' x)) (at x within s) \<and>
```
```  1864     (\<forall>h. norm(f' x h - g' x h) \<le> inverse (real (Suc n)) * norm h)"
```
```  1865     by (metis assms(2) inverse_positive_iff_positive real_of_nat_Suc_gt_zero)
```
```  1866   obtain f where
```
```  1867     *: "\<forall>x. \<exists>f'. \<forall>xa\<in>s. (f x has_derivative f' xa) (at xa within s) \<and>
```
```  1868       (\<forall>h. norm (f' xa h - g' xa h) \<le> inverse (real (Suc x)) * norm h)"
```
```  1869     using *[THEN choice] ..
```
```  1870   obtain f' where
```
```  1871     f: "\<forall>x. \<forall>xa\<in>s. (f x has_derivative f' x xa) (at xa within s) \<and>
```
```  1872       (\<forall>h. norm (f' x xa h - g' xa h) \<le> inverse (real (Suc x)) * norm h)"
```
```  1873     using *[THEN choice] ..
```
```  1874   show ?thesis
```
```  1875     apply (rule has_antiderivative_sequence[OF assms(1), of f f'])
```
```  1876     defer
```
```  1877     apply rule
```
```  1878     apply rule
```
```  1879   proof -
```
```  1880     fix e :: real
```
```  1881     assume "e > 0"
```
```  1882     obtain N where N: "inverse (real (Suc N)) < e"
```
```  1883       using reals_Archimedean[OF `e>0`] ..
```
```  1884     show "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
```
```  1885       apply (rule_tac x=N in exI)
```
```  1886     proof rule+
```
```  1887       case goal1
```
```  1888       have *: "inverse (real (Suc n)) \<le> e"
```
```  1889         apply (rule order_trans[OF _ N[THEN less_imp_le]])
```
```  1890         using goal1(1)
```
```  1891         apply (auto simp add: field_simps)
```
```  1892         done
```
```  1893       show ?case
```
```  1894         using f[rule_format,THEN conjunct2,OF goal1(2), of n, THEN spec[where x=h]]
```
```  1895         apply (rule order_trans)
```
```  1896         using N *
```
```  1897         apply (cases "h = 0")
```
```  1898         apply auto
```
```  1899         done
```
```  1900     qed
```
```  1901   qed (insert f, auto)
```
```  1902 qed
```
```  1903
```
```  1904
```
```  1905 subsection {* Differentiation of a series *}
```
```  1906
```
```  1907 lemma has_derivative_series:
```
```  1908   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::{real_inner, complete_space}"
```
```  1909   assumes "convex s"
```
```  1910     and "\<And>n x. x \<in> s \<Longrightarrow> ((f n) has_derivative (f' n x)) (at x within s)"
```
```  1911     and "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (setsum (\<lambda>i. f' i x h) {..<n} - g' x h) \<le> e * norm h"
```
```  1912     and "x \<in> s"
```
```  1913     and "(\<lambda>n. f n x) sums l"
```
```  1914   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)"
```
```  1915   unfolding sums_def
```
```  1916   apply (rule has_derivative_sequence[OF assms(1) _ assms(3)])
```
```  1917   apply (metis assms(2) has_derivative_setsum)
```
```  1918   using assms(4-5)
```
```  1919   unfolding sums_def
```
```  1920   apply auto
```
```  1921   done
```
```  1922
```
```  1923 text {* Considering derivative @{typ "real \<Rightarrow> 'b\<Colon>real_normed_vector"} as a vector. *}
```
```  1924
```
```  1925 lemma has_field_derivative_iff_has_vector_derivative:
```
```  1926   "(f has_field_derivative y) F \<longleftrightarrow> (f has_vector_derivative y) F"
```
```  1927   unfolding has_vector_derivative_def has_field_derivative_def real_scaleR_def mult_commute_abs ..
```
```  1928
```
```  1929 lemma has_field_derivative_subset:
```
```  1930   "(f has_field_derivative y) (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_field_derivative y) (at x within t)"
```
```  1931   unfolding has_field_derivative_def by (rule has_derivative_subset)
```
```  1932
```
```  1933 lemma has_vector_derivative_const[simp, derivative_intros]: "((\<lambda>x. c) has_vector_derivative 0) net"
```
```  1934   by (auto simp: has_vector_derivative_def)
```
```  1935
```
```  1936 lemma has_vector_derivative_id[simp, derivative_intros]: "((\<lambda>x. x) has_vector_derivative 1) net"
```
```  1937   by (auto simp: has_vector_derivative_def)
```
```  1938
```
```  1939 lemma has_vector_derivative_minus[derivative_intros]:
```
```  1940   "(f has_vector_derivative f') net \<Longrightarrow> ((\<lambda>x. - f x) has_vector_derivative (- f')) net"
```
```  1941   by (auto simp: has_vector_derivative_def)
```
```  1942
```
```  1943 lemma has_vector_derivative_add[derivative_intros]:
```
```  1944   "(f has_vector_derivative f') net \<Longrightarrow> (g has_vector_derivative g') net \<Longrightarrow>
```
```  1945     ((\<lambda>x. f x + g x) has_vector_derivative (f' + g')) net"
```
```  1946   by (auto simp: has_vector_derivative_def scaleR_right_distrib)
```
```  1947
```
```  1948 lemma has_vector_derivative_setsum[derivative_intros]:
```
```  1949   "(\<And>i. i \<in> I \<Longrightarrow> (f i has_vector_derivative f' i) net) \<Longrightarrow>
```
```  1950     ((\<lambda>x. \<Sum>i\<in>I. f i x) has_vector_derivative (\<Sum>i\<in>I. f' i)) net"
```
```  1951   by (auto simp: has_vector_derivative_def fun_eq_iff scaleR_setsum_right intro!: derivative_eq_intros)
```
```  1952
```
```  1953 lemma has_vector_derivative_diff[derivative_intros]:
```
```  1954   "(f has_vector_derivative f') net \<Longrightarrow> (g has_vector_derivative g') net \<Longrightarrow>
```
```  1955     ((\<lambda>x. f x - g x) has_vector_derivative (f' - g')) net"
```
```  1956   by (auto simp: has_vector_derivative_def scaleR_diff_right)
```
```  1957
```
```  1958 lemma (in bounded_linear) has_vector_derivative:
```
```  1959   assumes "(g has_vector_derivative g') F"
```
```  1960   shows "((\<lambda>x. f (g x)) has_vector_derivative f g') F"
```
```  1961   using has_derivative[OF assms[unfolded has_vector_derivative_def]]
```
```  1962   by (simp add: has_vector_derivative_def scaleR)
```
```  1963
```
```  1964 lemma (in bounded_bilinear) has_vector_derivative:
```
```  1965   assumes "(f has_vector_derivative f') (at x within s)"
```
```  1966     and "(g has_vector_derivative g') (at x within s)"
```
```  1967   shows "((\<lambda>x. f x ** g x) has_vector_derivative (f x ** g' + f' ** g x)) (at x within s)"
```
```  1968   using FDERIV[OF assms(1-2)[unfolded has_vector_derivative_def]]
```
```  1969   by (simp add: has_vector_derivative_def scaleR_right scaleR_left scaleR_right_distrib)
```
```  1970
```
```  1971 lemma has_vector_derivative_scaleR[derivative_intros]:
```
```  1972   "(f has_field_derivative f') (at x within s) \<Longrightarrow> (g has_vector_derivative g') (at x within s) \<Longrightarrow>
```
```  1973     ((\<lambda>x. f x *\<^sub>R g x) has_vector_derivative (f x *\<^sub>R g' + f' *\<^sub>R g x)) (at x within s)"
```
```  1974   unfolding has_field_derivative_iff_has_vector_derivative
```
```  1975   by (rule bounded_bilinear.has_vector_derivative[OF bounded_bilinear_scaleR])
```
```  1976
```
```  1977 lemma has_vector_derivative_mult[derivative_intros]:
```
```  1978   "(f has_vector_derivative f') (at x within s) \<Longrightarrow> (g has_vector_derivative g') (at x within s) \<Longrightarrow>
```
```  1979     ((\<lambda>x. f x * g x) has_vector_derivative (f x * g' + f' * g x :: 'a :: real_normed_algebra)) (at x within s)"
```
```  1980   by (rule bounded_bilinear.has_vector_derivative[OF bounded_bilinear_mult])
```
```  1981
```
```  1982 lemma has_vector_derivative_of_real[derivative_intros]:
```
```  1983   "(f has_field_derivative D) F \<Longrightarrow> ((\<lambda>x. of_real (f x)) has_vector_derivative (of_real D)) F"
```
```  1984   by (rule bounded_linear.has_vector_derivative[OF bounded_linear_of_real])
```
```  1985      (simp add: has_field_derivative_iff_has_vector_derivative)
```
```  1986
```
```  1987 lemma has_vector_derivative_continuous: "(f has_vector_derivative D) (at x within s) \<Longrightarrow> continuous (at x within s) f"
```
```  1988   by (auto intro: has_derivative_continuous simp: has_vector_derivative_def)
```
```  1989
```
```  1990 lemma has_vector_derivative_mult_right[derivative_intros]:
```
```  1991   fixes a :: "'a :: real_normed_algebra"
```
```  1992   shows "(f has_vector_derivative x) F \<Longrightarrow> ((\<lambda>x. a * f x) has_vector_derivative (a * x)) F"
```
```  1993   by (rule bounded_linear.has_vector_derivative[OF bounded_linear_mult_right])
```
```  1994
```
```  1995 lemma has_vector_derivative_mult_left[derivative_intros]:
```
```  1996   fixes a :: "'a :: real_normed_algebra"
```
```  1997   shows "(f has_vector_derivative x) F \<Longrightarrow> ((\<lambda>x. f x * a) has_vector_derivative (x * a)) F"
```
```  1998   by (rule bounded_linear.has_vector_derivative[OF bounded_linear_mult_left])
```
```  1999
```
```  2000 definition "vector_derivative f net = (SOME f'. (f has_vector_derivative f') net)"
```
```  2001
```
```  2002 lemma vector_derivative_unique_at:
```
```  2003   assumes "(f has_vector_derivative f') (at x)"
```
```  2004     and "(f has_vector_derivative f'') (at x)"
```
```  2005   shows "f' = f''"
```
```  2006 proof -
```
```  2007   have "(\<lambda>x. x *\<^sub>R f') = (\<lambda>x. x *\<^sub>R f'')"
```
```  2008     using assms [unfolded has_vector_derivative_def]
```
```  2009     by (rule frechet_derivative_unique_at)
```
```  2010   then show ?thesis
```
```  2011     unfolding fun_eq_iff by auto
```
```  2012 qed
```
```  2013
```
```  2014 lemma vector_derivative_works:
```
```  2015   "f differentiable net \<longleftrightarrow> (f has_vector_derivative (vector_derivative f net)) net"
```
```  2016     (is "?l = ?r")
```
```  2017 proof
```
```  2018   assume ?l
```
```  2019   obtain f' where f': "(f has_derivative f') net"
```
```  2020     using `?l` unfolding differentiable_def ..
```
```  2021   then interpret bounded_linear f'
```
```  2022     by auto
```
```  2023   show ?r
```
```  2024     unfolding vector_derivative_def has_vector_derivative_def
```
```  2025     by (rule someI[of _ "f' 1"]) (simp add: scaleR[symmetric] f')
```
```  2026 qed (auto simp: vector_derivative_def has_vector_derivative_def differentiable_def)
```
```  2027
```
```  2028 lemma vector_derivative_unique_within_closed_interval:
```
```  2029   assumes "a < b"
```
```  2030     and "x \<in> cbox a b"
```
```  2031   assumes "(f has_vector_derivative f') (at x within cbox a b)"
```
```  2032   assumes "(f has_vector_derivative f'') (at x within cbox a b)"
```
```  2033   shows "f' = f''"
```
```  2034 proof -
```
```  2035   have *: "(\<lambda>x. x *\<^sub>R f') = (\<lambda>x. x *\<^sub>R f'')"
```
```  2036     apply (rule frechet_derivative_unique_within_closed_interval[of "a" "b"])
```
```  2037     using assms(3-)[unfolded has_vector_derivative_def]
```
```  2038     using assms(1-2)
```
```  2039     apply auto
```
```  2040     done
```
```  2041   show ?thesis
```
```  2042   proof (rule ccontr)
```
```  2043     assume **: "f' \<noteq> f''"
```
```  2044     with * have "(\<lambda>x. x *\<^sub>R f') 1 = (\<lambda>x. x *\<^sub>R f'') 1"
```
```  2045       by (auto simp: fun_eq_iff)
```
```  2046     with ** show False
```
```  2047       unfolding o_def by auto
```
```  2048   qed
```
```  2049 qed
```
```  2050
```
```  2051 lemma vector_derivative_at:
```
```  2052   "(f has_vector_derivative f') (at x) \<Longrightarrow> vector_derivative f (at x) = f'"
```
```  2053   apply (rule vector_derivative_unique_at)
```
```  2054   defer
```
```  2055   apply assumption
```
```  2056   unfolding vector_derivative_works[symmetric] differentiable_def
```
```  2057   unfolding has_vector_derivative_def
```
```  2058   apply auto
```
```  2059   done
```
```  2060
```
```  2061 lemma vector_derivative_within_closed_interval:
```
```  2062   assumes "a < b"
```
```  2063     and "x \<in> cbox a b"
```
```  2064   assumes "(f has_vector_derivative f') (at x within cbox a b)"
```
```  2065   shows "vector_derivative f (at x within cbox a b) = f'"
```
```  2066   apply (rule vector_derivative_unique_within_closed_interval)
```
```  2067   using vector_derivative_works[unfolded differentiable_def]
```
```  2068   using assms
```
```  2069   apply (auto simp add:has_vector_derivative_def)
```
```  2070   done
```
```  2071
```
```  2072 lemma has_vector_derivative_within_subset:
```
```  2073   "(f has_vector_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_vector_derivative f') (at x within t)"
```
```  2074   by (auto simp: has_vector_derivative_def intro: has_derivative_within_subset)
```
```  2075
```
```  2076 lemma has_vector_derivative_at_within:
```
```  2077   "(f has_vector_derivative f') (at x) \<Longrightarrow> (f has_vector_derivative f') (at x within s)"
```
```  2078   unfolding has_vector_derivative_def
```
```  2079   by (rule has_derivative_at_within)
```
```  2080
```
```  2081 lemma has_vector_derivative_transform_within:
```
```  2082   assumes "0 < d"
```
```  2083     and "x \<in> s"
```
```  2084     and "\<forall>x'\<in>s. dist x' x < d \<longrightarrow> f x' = g x'"
```
```  2085   assumes "(f has_vector_derivative f') (at x within s)"
```
```  2086   shows "(g has_vector_derivative f') (at x within s)"
```
```  2087   using assms
```
```  2088   unfolding has_vector_derivative_def
```
```  2089   by (rule has_derivative_transform_within)
```
```  2090
```
```  2091 lemma has_vector_derivative_transform_at:
```
```  2092   assumes "0 < d"
```
```  2093     and "\<forall>x'. dist x' x < d \<longrightarrow> f x' = g x'"
```
```  2094     and "(f has_vector_derivative f') (at x)"
```
```  2095   shows "(g has_vector_derivative f') (at x)"
```
```  2096   using assms
```
```  2097   unfolding has_vector_derivative_def
```
```  2098   by (rule has_derivative_transform_at)
```
```  2099
```
```  2100 lemma has_vector_derivative_transform_within_open:
```
```  2101   assumes "open s"
```
```  2102     and "x \<in> s"
```
```  2103     and "\<forall>y\<in>s. f y = g y"
```
```  2104     and "(f has_vector_derivative f') (at x)"
```
```  2105   shows "(g has_vector_derivative f') (at x)"
```
```  2106   using assms
```
```  2107   unfolding has_vector_derivative_def
```
```  2108   by (rule has_derivative_transform_within_open)
```
```  2109
```
```  2110 lemma vector_diff_chain_at:
```
```  2111   assumes "(f has_vector_derivative f') (at x)"
```
```  2112     and "(g has_vector_derivative g') (at (f x))"
```
```  2113   shows "((g \<circ> f) has_vector_derivative (f' *\<^sub>R g')) (at x)"
```
```  2114   using assms(2)
```
```  2115   unfolding has_vector_derivative_def
```
```  2116   apply -
```
```  2117   apply (drule diff_chain_at[OF assms(1)[unfolded has_vector_derivative_def]])
```
```  2118   apply (simp only: o_def real_scaleR_def scaleR_scaleR)
```
```  2119   done
```
```  2120
```
```  2121 lemma vector_diff_chain_within:
```
```  2122   assumes "(f has_vector_derivative f') (at x within s)"
```
```  2123     and "(g has_vector_derivative g') (at (f x) within f ` s)"
```
```  2124   shows "((g \<circ> f) has_vector_derivative (f' *\<^sub>R g')) (at x within s)"
```
```  2125   using assms(2)
```
```  2126   unfolding has_vector_derivative_def
```
```  2127   apply -
```
```  2128   apply (drule diff_chain_within[OF assms(1)[unfolded has_vector_derivative_def]])
```
```  2129   apply (simp only: o_def real_scaleR_def scaleR_scaleR)
```
```  2130   done
```
```  2131
```
```  2132 end
```