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