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