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--
modernized header;
     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