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