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