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