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