src/HOL/Hyperreal/FrechetDeriv.thy
author wenzelm
Thu Nov 20 19:43:34 2008 +0100 (2008-11-20)
changeset 28866 30cd9d89a0fb
parent 28823 dcbef866c9e2
permissions -rw-r--r--
reactivated some dead theories (based on hints by Mark Hillebrand);
huffman@21776
     1
(*  Title       : FrechetDeriv.thy
huffman@21776
     2
    ID          : $Id$
huffman@21776
     3
    Author      : Brian Huffman
huffman@21776
     4
*)
huffman@21776
     5
huffman@21776
     6
header {* Frechet Derivative *}
huffman@21776
     7
huffman@21776
     8
theory FrechetDeriv
huffman@21776
     9
imports Lim
huffman@21776
    10
begin
huffman@21776
    11
huffman@21776
    12
definition
huffman@21776
    13
  fderiv ::
huffman@21776
    14
  "['a::real_normed_vector \<Rightarrow> 'b::real_normed_vector, 'a, 'a \<Rightarrow> 'b] \<Rightarrow> bool"
huffman@21776
    15
    -- {* Frechet derivative: D is derivative of function f at x *}
huffman@21776
    16
          ("(FDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where
huffman@21776
    17
  "FDERIV f x :> D = (bounded_linear D \<and>
huffman@21776
    18
    (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0)"
huffman@21776
    19
huffman@21776
    20
lemma FDERIV_I:
huffman@21776
    21
  "\<lbrakk>bounded_linear D; (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0\<rbrakk>
huffman@21776
    22
   \<Longrightarrow> FDERIV f x :> D"
huffman@21776
    23
by (simp add: fderiv_def)
huffman@21776
    24
huffman@21776
    25
lemma FDERIV_D:
huffman@21776
    26
  "FDERIV f x :> D \<Longrightarrow> (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0"
huffman@21776
    27
by (simp add: fderiv_def)
huffman@21776
    28
huffman@21776
    29
lemma FDERIV_bounded_linear: "FDERIV f x :> D \<Longrightarrow> bounded_linear D"
huffman@21776
    30
by (simp add: fderiv_def)
huffman@21776
    31
huffman@21776
    32
lemma bounded_linear_zero:
huffman@21776
    33
  "bounded_linear (\<lambda>x::'a::real_normed_vector. 0::'b::real_normed_vector)"
haftmann@28823
    34
proof
huffman@21776
    35
  show "(0::'b) = 0 + 0" by simp
huffman@21776
    36
  fix r show "(0::'b) = scaleR r 0" by simp
huffman@21776
    37
  have "\<forall>x::'a. norm (0::'b) \<le> norm x * 0" by simp
huffman@21776
    38
  thus "\<exists>K. \<forall>x::'a. norm (0::'b) \<le> norm x * K" ..
huffman@21776
    39
qed
huffman@21776
    40
huffman@21776
    41
lemma FDERIV_const: "FDERIV (\<lambda>x. k) x :> (\<lambda>h. 0)"
huffman@21776
    42
by (simp add: fderiv_def bounded_linear_zero)
huffman@21776
    43
huffman@21776
    44
lemma bounded_linear_ident:
huffman@21776
    45
  "bounded_linear (\<lambda>x::'a::real_normed_vector. x)"
haftmann@28823
    46
proof
huffman@21776
    47
  fix x y :: 'a show "x + y = x + y" by simp
huffman@21776
    48
  fix r and x :: 'a show "scaleR r x = scaleR r x" by simp
huffman@21776
    49
  have "\<forall>x::'a. norm x \<le> norm x * 1" by simp
huffman@21776
    50
  thus "\<exists>K. \<forall>x::'a. norm x \<le> norm x * K" ..
huffman@21776
    51
qed
huffman@21776
    52
huffman@21776
    53
lemma FDERIV_ident: "FDERIV (\<lambda>x. x) x :> (\<lambda>h. h)"
huffman@21776
    54
by (simp add: fderiv_def bounded_linear_ident)
huffman@21776
    55
huffman@21776
    56
subsection {* Addition *}
huffman@21776
    57
huffman@21776
    58
lemma add_diff_add:
huffman@21776
    59
  fixes a b c d :: "'a::ab_group_add"
huffman@21776
    60
  shows "(a + c) - (b + d) = (a - b) + (c - d)"
huffman@21776
    61
by simp
huffman@21776
    62
huffman@21776
    63
lemma bounded_linear_add:
ballarin@27611
    64
  assumes "bounded_linear f"
ballarin@27611
    65
  assumes "bounded_linear g"
huffman@21776
    66
  shows "bounded_linear (\<lambda>x. f x + g x)"
ballarin@27611
    67
proof -
ballarin@27611
    68
  interpret f: bounded_linear [f] by fact
ballarin@27611
    69
  interpret g: bounded_linear [g] by fact
ballarin@27611
    70
  show ?thesis apply (unfold_locales)
ballarin@27611
    71
    apply (simp only: f.add g.add add_ac)
ballarin@27611
    72
    apply (simp only: f.scaleR g.scaleR scaleR_right_distrib)
ballarin@27611
    73
    apply (rule f.pos_bounded [THEN exE], rename_tac Kf)
ballarin@27611
    74
    apply (rule g.pos_bounded [THEN exE], rename_tac Kg)
ballarin@27611
    75
    apply (rule_tac x="Kf + Kg" in exI, safe)
ballarin@27611
    76
    apply (subst right_distrib)
ballarin@27611
    77
    apply (rule order_trans [OF norm_triangle_ineq])
ballarin@27611
    78
    apply (rule add_mono, erule spec, erule spec)
ballarin@27611
    79
    done
ballarin@27611
    80
qed
huffman@21776
    81
huffman@21776
    82
lemma norm_ratio_ineq:
huffman@21776
    83
  fixes x y :: "'a::real_normed_vector"
huffman@21776
    84
  fixes h :: "'b::real_normed_vector"
huffman@21776
    85
  shows "norm (x + y) / norm h \<le> norm x / norm h + norm y / norm h"
huffman@21776
    86
apply (rule ord_le_eq_trans)
huffman@21776
    87
apply (rule divide_right_mono)
huffman@21776
    88
apply (rule norm_triangle_ineq)
huffman@21776
    89
apply (rule norm_ge_zero)
huffman@21776
    90
apply (rule add_divide_distrib)
huffman@21776
    91
done
huffman@21776
    92
huffman@21776
    93
lemma FDERIV_add:
huffman@21776
    94
  assumes f: "FDERIV f x :> F"
huffman@21776
    95
  assumes g: "FDERIV g x :> G"
huffman@21776
    96
  shows "FDERIV (\<lambda>x. f x + g x) x :> (\<lambda>h. F h + G h)"
huffman@21776
    97
proof (rule FDERIV_I)
huffman@21776
    98
  show "bounded_linear (\<lambda>h. F h + G h)"
huffman@21776
    99
    apply (rule bounded_linear_add)
huffman@21776
   100
    apply (rule FDERIV_bounded_linear [OF f])
huffman@21776
   101
    apply (rule FDERIV_bounded_linear [OF g])
huffman@21776
   102
    done
huffman@21776
   103
next
huffman@21776
   104
  have f': "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h) -- 0 --> 0"
huffman@21776
   105
    using f by (rule FDERIV_D)
huffman@21776
   106
  have g': "(\<lambda>h. norm (g (x + h) - g x - G h) / norm h) -- 0 --> 0"
huffman@21776
   107
    using g by (rule FDERIV_D)
huffman@21776
   108
  from f' g'
huffman@21776
   109
  have "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h
huffman@21776
   110
           + norm (g (x + h) - g x - G h) / norm h) -- 0 --> 0"
huffman@21776
   111
    by (rule LIM_add_zero)
huffman@21776
   112
  thus "(\<lambda>h. norm (f (x + h) + g (x + h) - (f x + g x) - (F h + G h))
huffman@21776
   113
           / norm h) -- 0 --> 0"
huffman@21776
   114
    apply (rule real_LIM_sandwich_zero)
huffman@21776
   115
     apply (simp add: divide_nonneg_pos)
huffman@21776
   116
    apply (simp only: add_diff_add)
huffman@21776
   117
    apply (rule norm_ratio_ineq)
huffman@21776
   118
    done
huffman@21776
   119
qed
huffman@21776
   120
huffman@21776
   121
subsection {* Subtraction *}
huffman@21776
   122
huffman@21776
   123
lemma bounded_linear_minus:
ballarin@27611
   124
  assumes "bounded_linear f"
huffman@21776
   125
  shows "bounded_linear (\<lambda>x. - f x)"
ballarin@27611
   126
proof -
ballarin@27611
   127
  interpret f: bounded_linear [f] by fact
ballarin@27611
   128
  show ?thesis apply (unfold_locales)
ballarin@27611
   129
    apply (simp add: f.add)
ballarin@27611
   130
    apply (simp add: f.scaleR)
ballarin@27611
   131
    apply (simp add: f.bounded)
ballarin@27611
   132
    done
ballarin@27611
   133
qed
huffman@21776
   134
huffman@21776
   135
lemma FDERIV_minus:
huffman@21776
   136
  "FDERIV f x :> F \<Longrightarrow> FDERIV (\<lambda>x. - f x) x :> (\<lambda>h. - F h)"
huffman@21776
   137
apply (rule FDERIV_I)
huffman@21776
   138
apply (rule bounded_linear_minus)
huffman@21776
   139
apply (erule FDERIV_bounded_linear)
huffman@21776
   140
apply (simp only: fderiv_def minus_diff_minus norm_minus_cancel)
huffman@21776
   141
done
huffman@21776
   142
huffman@21776
   143
lemma FDERIV_diff:
huffman@21776
   144
  "\<lbrakk>FDERIV f x :> F; FDERIV g x :> G\<rbrakk>
huffman@21776
   145
   \<Longrightarrow> FDERIV (\<lambda>x. f x - g x) x :> (\<lambda>h. F h - G h)"
huffman@21776
   146
by (simp only: diff_minus FDERIV_add FDERIV_minus)
huffman@21776
   147
huffman@21776
   148
subsection {* Continuity *}
huffman@21776
   149
huffman@21776
   150
lemma FDERIV_isCont:
huffman@21776
   151
  assumes f: "FDERIV f x :> F"
huffman@21776
   152
  shows "isCont f x"
huffman@21776
   153
proof -
huffman@21776
   154
  from f interpret F: bounded_linear ["F"] by (rule FDERIV_bounded_linear)
huffman@21776
   155
  have "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h) -- 0 --> 0"
huffman@21776
   156
    by (rule FDERIV_D [OF f])
huffman@21776
   157
  hence "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h * norm h) -- 0 --> 0"
wenzelm@28866
   158
    by (intro LIM_mult_zero LIM_norm_zero LIM_ident)
huffman@21776
   159
  hence "(\<lambda>h. norm (f (x + h) - f x - F h)) -- 0 --> 0"
huffman@21776
   160
    by (simp cong: LIM_cong)
huffman@21776
   161
  hence "(\<lambda>h. f (x + h) - f x - F h) -- 0 --> 0"
huffman@21776
   162
    by (rule LIM_norm_zero_cancel)
huffman@21776
   163
  hence "(\<lambda>h. f (x + h) - f x - F h + F h) -- 0 --> 0"
wenzelm@28866
   164
    by (intro LIM_add_zero F.LIM_zero LIM_ident)
huffman@21776
   165
  hence "(\<lambda>h. f (x + h) - f x) -- 0 --> 0"
huffman@21776
   166
    by simp
huffman@21776
   167
  thus "isCont f x"
huffman@21776
   168
    unfolding isCont_iff by (rule LIM_zero_cancel)
huffman@21776
   169
qed
huffman@21776
   170
huffman@21776
   171
subsection {* Composition *}
huffman@21776
   172
huffman@21776
   173
lemma real_divide_cancel_lemma:
huffman@21776
   174
  fixes a b c :: real
huffman@21776
   175
  shows "(b = 0 \<Longrightarrow> a = 0) \<Longrightarrow> (a / b) * (b / c) = a / c"
huffman@21776
   176
by simp
huffman@21776
   177
huffman@21776
   178
lemma bounded_linear_compose:
ballarin@27611
   179
  assumes "bounded_linear f"
ballarin@27611
   180
  assumes "bounded_linear g"
huffman@21776
   181
  shows "bounded_linear (\<lambda>x. f (g x))"
ballarin@27611
   182
proof -
ballarin@27611
   183
  interpret f: bounded_linear [f] by fact
ballarin@27611
   184
  interpret g: bounded_linear [g] by fact
ballarin@27611
   185
  show ?thesis proof (unfold_locales)
ballarin@27611
   186
    fix x y show "f (g (x + y)) = f (g x) + f (g y)"
ballarin@27611
   187
      by (simp only: f.add g.add)
ballarin@27611
   188
  next
ballarin@27611
   189
    fix r x show "f (g (scaleR r x)) = scaleR r (f (g x))"
ballarin@27611
   190
      by (simp only: f.scaleR g.scaleR)
ballarin@27611
   191
  next
ballarin@27611
   192
    from f.pos_bounded
ballarin@27611
   193
    obtain Kf where f: "\<And>x. norm (f x) \<le> norm x * Kf" and Kf: "0 < Kf" by fast
ballarin@27611
   194
    from g.pos_bounded
ballarin@27611
   195
    obtain Kg where g: "\<And>x. norm (g x) \<le> norm x * Kg" by fast
ballarin@27611
   196
    show "\<exists>K. \<forall>x. norm (f (g x)) \<le> norm x * K"
ballarin@27611
   197
    proof (intro exI allI)
ballarin@27611
   198
      fix x
ballarin@27611
   199
      have "norm (f (g x)) \<le> norm (g x) * Kf"
ballarin@27611
   200
	using f .
ballarin@27611
   201
      also have "\<dots> \<le> (norm x * Kg) * Kf"
ballarin@27611
   202
	using g Kf [THEN order_less_imp_le] by (rule mult_right_mono)
ballarin@27611
   203
      also have "(norm x * Kg) * Kf = norm x * (Kg * Kf)"
ballarin@27611
   204
	by (rule mult_assoc)
ballarin@27611
   205
      finally show "norm (f (g x)) \<le> norm x * (Kg * Kf)" .
ballarin@27611
   206
    qed
huffman@21776
   207
  qed
huffman@21776
   208
qed
huffman@21776
   209
huffman@21776
   210
lemma FDERIV_compose:
huffman@21776
   211
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
huffman@21776
   212
  fixes g :: "'b::real_normed_vector \<Rightarrow> 'c::real_normed_vector"
huffman@21776
   213
  assumes f: "FDERIV f x :> F"
huffman@21776
   214
  assumes g: "FDERIV g (f x) :> G"
huffman@21776
   215
  shows "FDERIV (\<lambda>x. g (f x)) x :> (\<lambda>h. G (F h))"
huffman@21776
   216
proof (rule FDERIV_I)
huffman@21776
   217
  from FDERIV_bounded_linear [OF g] FDERIV_bounded_linear [OF f]
huffman@21776
   218
  show "bounded_linear (\<lambda>h. G (F h))"
huffman@21776
   219
    by (rule bounded_linear_compose)
huffman@21776
   220
next
huffman@21776
   221
  let ?Rf = "\<lambda>h. f (x + h) - f x - F h"
huffman@21776
   222
  let ?Rg = "\<lambda>k. g (f x + k) - g (f x) - G k"
huffman@21776
   223
  let ?k = "\<lambda>h. f (x + h) - f x"
huffman@21776
   224
  let ?Nf = "\<lambda>h. norm (?Rf h) / norm h"
huffman@21776
   225
  let ?Ng = "\<lambda>h. norm (?Rg (?k h)) / norm (?k h)"
huffman@21776
   226
  from f interpret F: bounded_linear ["F"] by (rule FDERIV_bounded_linear)
huffman@21776
   227
  from g interpret G: bounded_linear ["G"] by (rule FDERIV_bounded_linear)
huffman@21776
   228
  from F.bounded obtain kF where kF: "\<And>x. norm (F x) \<le> norm x * kF" by fast
huffman@21776
   229
  from G.bounded obtain kG where kG: "\<And>x. norm (G x) \<le> norm x * kG" by fast
huffman@21776
   230
huffman@21776
   231
  let ?fun2 = "\<lambda>h. ?Nf h * kG + ?Ng h * (?Nf h + kF)"
huffman@21776
   232
huffman@21776
   233
  show "(\<lambda>h. norm (g (f (x + h)) - g (f x) - G (F h)) / norm h) -- 0 --> 0"
huffman@21776
   234
  proof (rule real_LIM_sandwich_zero)
huffman@21776
   235
    have Nf: "?Nf -- 0 --> 0"
huffman@21776
   236
      using FDERIV_D [OF f] .
huffman@21776
   237
huffman@21776
   238
    have Ng1: "isCont (\<lambda>k. norm (?Rg k) / norm k) 0"
huffman@21776
   239
      by (simp add: isCont_def FDERIV_D [OF g])
huffman@21776
   240
    have Ng2: "?k -- 0 --> 0"
huffman@21776
   241
      apply (rule LIM_zero)
huffman@21776
   242
      apply (fold isCont_iff)
huffman@21776
   243
      apply (rule FDERIV_isCont [OF f])
huffman@21776
   244
      done
huffman@21776
   245
    have Ng: "?Ng -- 0 --> 0"
huffman@21776
   246
      using isCont_LIM_compose [OF Ng1 Ng2] by simp
huffman@21776
   247
huffman@21776
   248
    have "(\<lambda>h. ?Nf h * kG + ?Ng h * (?Nf h + kF))
huffman@21776
   249
           -- 0 --> 0 * kG + 0 * (0 + kF)"
huffman@21776
   250
      by (intro LIM_add LIM_mult LIM_const Nf Ng)
huffman@21776
   251
    thus "(\<lambda>h. ?Nf h * kG + ?Ng h * (?Nf h + kF)) -- 0 --> 0"
huffman@21776
   252
      by simp
huffman@21776
   253
  next
huffman@21776
   254
    fix h::'a assume h: "h \<noteq> 0"
huffman@21776
   255
    thus "0 \<le> norm (g (f (x + h)) - g (f x) - G (F h)) / norm h"
huffman@21776
   256
      by (simp add: divide_nonneg_pos)
huffman@21776
   257
  next
huffman@21776
   258
    fix h::'a assume h: "h \<noteq> 0"
huffman@21776
   259
    have "g (f (x + h)) - g (f x) - G (F h) = G (?Rf h) + ?Rg (?k h)"
huffman@21776
   260
      by (simp add: G.diff)
huffman@21776
   261
    hence "norm (g (f (x + h)) - g (f x) - G (F h)) / norm h
huffman@21776
   262
           = norm (G (?Rf h) + ?Rg (?k h)) / norm h"
huffman@21776
   263
      by (rule arg_cong)
huffman@21776
   264
    also have "\<dots> \<le> norm (G (?Rf h)) / norm h + norm (?Rg (?k h)) / norm h"
huffman@21776
   265
      by (rule norm_ratio_ineq)
huffman@21776
   266
    also have "\<dots> \<le> ?Nf h * kG + ?Ng h * (?Nf h + kF)"
huffman@21776
   267
    proof (rule add_mono)
huffman@21776
   268
      show "norm (G (?Rf h)) / norm h \<le> ?Nf h * kG"
huffman@21776
   269
        apply (rule ord_le_eq_trans)
huffman@21776
   270
        apply (rule divide_right_mono [OF kG norm_ge_zero])
huffman@21776
   271
        apply simp
huffman@21776
   272
        done
huffman@21776
   273
    next
huffman@21776
   274
      have "norm (?Rg (?k h)) / norm h = ?Ng h * (norm (?k h) / norm h)"
huffman@21776
   275
        apply (rule real_divide_cancel_lemma [symmetric])
huffman@21776
   276
        apply (simp add: G.zero)
huffman@21776
   277
        done
huffman@21776
   278
      also have "\<dots> \<le> ?Ng h * (?Nf h + kF)"
huffman@21776
   279
      proof (rule mult_left_mono)
huffman@21776
   280
        have "norm (?k h) / norm h = norm (?Rf h + F h) / norm h"
huffman@21776
   281
          by simp
huffman@21776
   282
        also have "\<dots> \<le> ?Nf h + norm (F h) / norm h"
huffman@21776
   283
          by (rule norm_ratio_ineq)
huffman@21776
   284
        also have "\<dots> \<le> ?Nf h + kF"
huffman@21776
   285
          apply (rule add_left_mono)
huffman@21776
   286
          apply (subst pos_divide_le_eq, simp add: h)
huffman@21776
   287
          apply (subst mult_commute)
huffman@21776
   288
          apply (rule kF)
huffman@21776
   289
          done
huffman@21776
   290
        finally show "norm (?k h) / norm h \<le> ?Nf h + kF" .
huffman@21776
   291
      next
huffman@21776
   292
        show "0 \<le> ?Ng h"
huffman@21776
   293
        apply (case_tac "f (x + h) - f x = 0", simp)
huffman@21776
   294
        apply (rule divide_nonneg_pos [OF norm_ge_zero])
huffman@21776
   295
        apply simp
huffman@21776
   296
        done
huffman@21776
   297
      qed
huffman@21776
   298
      finally show "norm (?Rg (?k h)) / norm h \<le> ?Ng h * (?Nf h + kF)" .
huffman@21776
   299
    qed
huffman@21776
   300
    finally show "norm (g (f (x + h)) - g (f x) - G (F h)) / norm h
huffman@21776
   301
        \<le> ?Nf h * kG + ?Ng h * (?Nf h + kF)" .
huffman@21776
   302
  qed
huffman@21776
   303
qed
huffman@21776
   304
huffman@21776
   305
subsection {* Product Rule *}
huffman@21776
   306
huffman@21776
   307
lemma (in bounded_bilinear) FDERIV_lemma:
huffman@21776
   308
  "a' ** b' - a ** b - (a ** B + A ** b)
huffman@21776
   309
   = a ** (b' - b - B) + (a' - a - A) ** b' + A ** (b' - b)"
huffman@21776
   310
by (simp add: diff_left diff_right)
huffman@21776
   311
huffman@21776
   312
lemma (in bounded_bilinear) FDERIV:
huffman@21776
   313
  fixes x :: "'d::real_normed_vector"
huffman@21776
   314
  assumes f: "FDERIV f x :> F"
huffman@21776
   315
  assumes g: "FDERIV g x :> G"
huffman@21776
   316
  shows "FDERIV (\<lambda>x. f x ** g x) x :> (\<lambda>h. f x ** G h + F h ** g x)"
huffman@21776
   317
proof (rule FDERIV_I)
huffman@21776
   318
  show "bounded_linear (\<lambda>h. f x ** G h + F h ** g x)"
huffman@21776
   319
    apply (rule bounded_linear_add)
huffman@21776
   320
    apply (rule bounded_linear_compose [OF bounded_linear_right])
huffman@21776
   321
    apply (rule FDERIV_bounded_linear [OF g])
huffman@21776
   322
    apply (rule bounded_linear_compose [OF bounded_linear_left])
huffman@21776
   323
    apply (rule FDERIV_bounded_linear [OF f])
huffman@21776
   324
    done
huffman@21776
   325
next
huffman@21776
   326
  from bounded_linear.bounded [OF FDERIV_bounded_linear [OF f]]
huffman@21776
   327
  obtain KF where norm_F: "\<And>x. norm (F x) \<le> norm x * KF" by fast
huffman@21776
   328
huffman@21776
   329
  from pos_bounded obtain K where K: "0 < K" and norm_prod:
huffman@21776
   330
    "\<And>a b. norm (a ** b) \<le> norm a * norm b * K" by fast
huffman@21776
   331
huffman@21776
   332
  let ?Rf = "\<lambda>h. f (x + h) - f x - F h"
huffman@21776
   333
  let ?Rg = "\<lambda>h. g (x + h) - g x - G h"
huffman@21776
   334
huffman@21776
   335
  let ?fun1 = "\<lambda>h.
huffman@21776
   336
        norm (f x ** ?Rg h + ?Rf h ** g (x + h) + F h ** (g (x + h) - g x)) /
huffman@21776
   337
        norm h"
huffman@21776
   338
huffman@21776
   339
  let ?fun2 = "\<lambda>h.
huffman@21776
   340
        norm (f x) * (norm (?Rg h) / norm h) * K +
huffman@21776
   341
        norm (?Rf h) / norm h * norm (g (x + h)) * K +
huffman@21776
   342
        KF * norm (g (x + h) - g x) * K"
huffman@21776
   343
huffman@21776
   344
  have "?fun1 -- 0 --> 0"
huffman@21776
   345
  proof (rule real_LIM_sandwich_zero)
huffman@21776
   346
    from f g isCont_iff [THEN iffD1, OF FDERIV_isCont [OF g]]
huffman@21776
   347
    have "?fun2 -- 0 -->
huffman@21776
   348
          norm (f x) * 0 * K + 0 * norm (g x) * K + KF * norm (0::'b) * K"
huffman@21776
   349
      by (intro LIM_add LIM_mult LIM_const LIM_norm LIM_zero FDERIV_D)
huffman@21776
   350
    thus "?fun2 -- 0 --> 0"
huffman@21776
   351
      by simp
huffman@21776
   352
  next
huffman@21776
   353
    fix h::'d assume "h \<noteq> 0"
huffman@21776
   354
    thus "0 \<le> ?fun1 h"
huffman@21776
   355
      by (simp add: divide_nonneg_pos)
huffman@21776
   356
  next
huffman@21776
   357
    fix h::'d assume "h \<noteq> 0"
huffman@21776
   358
    have "?fun1 h \<le> (norm (f x) * norm (?Rg h) * K +
huffman@21776
   359
         norm (?Rf h) * norm (g (x + h)) * K +
huffman@21776
   360
         norm h * KF * norm (g (x + h) - g x) * K) / norm h"
huffman@21776
   361
      by (intro
huffman@21776
   362
        divide_right_mono mult_mono'
huffman@21776
   363
        order_trans [OF norm_triangle_ineq add_mono]
huffman@21776
   364
        order_trans [OF norm_prod mult_right_mono]
huffman@21776
   365
        mult_nonneg_nonneg order_refl norm_ge_zero norm_F
huffman@21776
   366
        K [THEN order_less_imp_le]
huffman@21776
   367
      )
huffman@21776
   368
    also have "\<dots> = ?fun2 h"
huffman@21776
   369
      by (simp add: add_divide_distrib)
huffman@21776
   370
    finally show "?fun1 h \<le> ?fun2 h" .
huffman@21776
   371
  qed
huffman@21776
   372
  thus "(\<lambda>h.
huffman@21776
   373
    norm (f (x + h) ** g (x + h) - f x ** g x - (f x ** G h + F h ** g x))
huffman@21776
   374
    / norm h) -- 0 --> 0"
huffman@21776
   375
    by (simp only: FDERIV_lemma)
huffman@21776
   376
qed
huffman@21776
   377
wenzelm@28866
   378
lemmas FDERIV_mult = bounded_bilinear_locale.mult.prod.FDERIV
huffman@21776
   379
wenzelm@28866
   380
lemmas FDERIV_scaleR = bounded_bilinear_locale.scaleR.prod.FDERIV
wenzelm@28866
   381
huffman@21776
   382
huffman@21776
   383
subsection {* Powers *}
huffman@21776
   384
huffman@21776
   385
lemma FDERIV_power_Suc:
huffman@21776
   386
  fixes x :: "'a::{real_normed_algebra,recpower,comm_ring_1}"
wenzelm@28866
   387
  shows "FDERIV (\<lambda>x. x ^ Suc n) x :> (\<lambda>h. (1 + of_nat n) * x ^ n * h)"
huffman@21776
   388
 apply (induct n)
huffman@21776
   389
  apply (simp add: power_Suc FDERIV_ident)
huffman@21776
   390
 apply (drule FDERIV_mult [OF FDERIV_ident])
wenzelm@28866
   391
 apply (simp only: of_nat_Suc left_distrib mult_1_left)
wenzelm@28866
   392
 apply (simp only: power_Suc right_distrib add_ac mult_ac)
huffman@21776
   393
done
huffman@21776
   394
huffman@21776
   395
lemma FDERIV_power:
huffman@21776
   396
  fixes x :: "'a::{real_normed_algebra,recpower,comm_ring_1}"
huffman@21776
   397
  shows "FDERIV (\<lambda>x. x ^ n) x :> (\<lambda>h. of_nat n * x ^ (n - 1) * h)"
wenzelm@28866
   398
  apply (cases n)
wenzelm@28866
   399
   apply (simp add: FDERIV_const)
wenzelm@28866
   400
  apply (simp add: FDERIV_power_Suc)
wenzelm@28866
   401
  done
wenzelm@28866
   402
huffman@21776
   403
huffman@21776
   404
subsection {* Inverse *}
huffman@21776
   405
huffman@21776
   406
lemma inverse_diff_inverse:
huffman@21776
   407
  "\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk>
huffman@21776
   408
   \<Longrightarrow> inverse a - inverse b = - (inverse a * (a - b) * inverse b)"
huffman@21776
   409
by (simp add: right_diff_distrib left_diff_distrib mult_assoc)
huffman@21776
   410
huffman@21776
   411
lemmas bounded_linear_mult_const =
wenzelm@28866
   412
  bounded_bilinear_locale.mult.prod.bounded_linear_left [THEN bounded_linear_compose]
huffman@21776
   413
huffman@21776
   414
lemmas bounded_linear_const_mult =
wenzelm@28866
   415
  bounded_bilinear_locale.mult.prod.bounded_linear_right [THEN bounded_linear_compose]
huffman@21776
   416
huffman@21776
   417
lemma FDERIV_inverse:
huffman@21776
   418
  fixes x :: "'a::real_normed_div_algebra"
huffman@21776
   419
  assumes x: "x \<noteq> 0"
huffman@21776
   420
  shows "FDERIV inverse x :> (\<lambda>h. - (inverse x * h * inverse x))"
huffman@21776
   421
        (is "FDERIV ?inv _ :> _")
huffman@21776
   422
proof (rule FDERIV_I)
huffman@21776
   423
  show "bounded_linear (\<lambda>h. - (?inv x * h * ?inv x))"
huffman@21776
   424
    apply (rule bounded_linear_minus)
huffman@21776
   425
    apply (rule bounded_linear_mult_const)
huffman@21776
   426
    apply (rule bounded_linear_const_mult)
huffman@21776
   427
    apply (rule bounded_linear_ident)
huffman@21776
   428
    done
huffman@21776
   429
next
huffman@21776
   430
  show "(\<lambda>h. norm (?inv (x + h) - ?inv x - - (?inv x * h * ?inv x)) / norm h)
huffman@21776
   431
        -- 0 --> 0"
huffman@21776
   432
  proof (rule LIM_equal2)
huffman@21776
   433
    show "0 < norm x" using x by simp
huffman@21776
   434
  next
huffman@21776
   435
    fix h::'a
huffman@21776
   436
    assume 1: "h \<noteq> 0"
huffman@21776
   437
    assume "norm (h - 0) < norm x"
huffman@21776
   438
    hence "h \<noteq> -x" by clarsimp
huffman@21776
   439
    hence 2: "x + h \<noteq> 0"
huffman@21776
   440
      apply (rule contrapos_nn)
huffman@21776
   441
      apply (rule sym)
huffman@21776
   442
      apply (erule equals_zero_I)
huffman@21776
   443
      done
huffman@21776
   444
    show "norm (?inv (x + h) - ?inv x - - (?inv x * h * ?inv x)) / norm h
huffman@21776
   445
          = norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h"
huffman@21776
   446
      apply (subst inverse_diff_inverse [OF 2 x])
huffman@21776
   447
      apply (subst minus_diff_minus)
huffman@21776
   448
      apply (subst norm_minus_cancel)
huffman@21776
   449
      apply (simp add: left_diff_distrib)
huffman@21776
   450
      done
huffman@21776
   451
  next
huffman@21776
   452
    show "(\<lambda>h. norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h)
huffman@21776
   453
          -- 0 --> 0"
huffman@21776
   454
    proof (rule real_LIM_sandwich_zero)
huffman@21776
   455
      show "(\<lambda>h. norm (?inv (x + h) - ?inv x) * norm (?inv x))
huffman@21776
   456
            -- 0 --> 0"
huffman@21776
   457
        apply (rule LIM_mult_left_zero)
huffman@21776
   458
        apply (rule LIM_norm_zero)
huffman@21776
   459
        apply (rule LIM_zero)
huffman@21776
   460
        apply (rule LIM_offset_zero)
huffman@21776
   461
        apply (rule LIM_inverse)
wenzelm@28866
   462
        apply (rule LIM_ident)
huffman@21776
   463
        apply (rule x)
huffman@21776
   464
        done
huffman@21776
   465
    next
huffman@21776
   466
      fix h::'a assume h: "h \<noteq> 0"
huffman@21776
   467
      show "0 \<le> norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h"
huffman@21776
   468
        apply (rule divide_nonneg_pos)
huffman@21776
   469
        apply (rule norm_ge_zero)
huffman@21776
   470
        apply (simp add: h)
huffman@21776
   471
        done
huffman@21776
   472
    next
huffman@21776
   473
      fix h::'a assume h: "h \<noteq> 0"
huffman@21776
   474
      have "norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h
huffman@21776
   475
            \<le> norm (?inv (x + h) - ?inv x) * norm h * norm (?inv x) / norm h"
huffman@21776
   476
        apply (rule divide_right_mono [OF _ norm_ge_zero])
huffman@21776
   477
        apply (rule order_trans [OF norm_mult_ineq])
huffman@21776
   478
        apply (rule mult_right_mono [OF _ norm_ge_zero])
huffman@21776
   479
        apply (rule norm_mult_ineq)
huffman@21776
   480
        done
huffman@21776
   481
      also have "\<dots> = norm (?inv (x + h) - ?inv x) * norm (?inv x)"
huffman@21776
   482
        by simp
huffman@21776
   483
      finally show "norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h
huffman@21776
   484
            \<le> norm (?inv (x + h) - ?inv x) * norm (?inv x)" .   
huffman@21776
   485
    qed
huffman@21776
   486
  qed
huffman@21776
   487
qed
huffman@21776
   488
huffman@21776
   489
subsection {* Alternate definition *}
huffman@21776
   490
huffman@21776
   491
lemma field_fderiv_def:
huffman@21776
   492
  fixes x :: "'a::real_normed_field" shows
huffman@21776
   493
  "FDERIV f x :> (\<lambda>h. h * D) = (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
huffman@21776
   494
 apply (unfold fderiv_def)
wenzelm@28866
   495
 apply (simp add: bounded_bilinear_locale.mult.prod.bounded_linear_left)
huffman@21776
   496
 apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric])
huffman@21776
   497
 apply (subst diff_divide_distrib)
huffman@21776
   498
 apply (subst times_divide_eq_left [symmetric])
nipkow@23398
   499
 apply (simp cong: LIM_cong)
huffman@21776
   500
 apply (simp add: LIM_norm_zero_iff LIM_zero_iff)
huffman@21776
   501
done
huffman@21776
   502
huffman@21776
   503
end