src/HOL/Library/FrechetDeriv.thy
author hoelzl
Tue Jul 19 14:37:49 2011 +0200 (2011-07-19)
changeset 43922 c6f35921056e
parent 39302 d7728f65b353
child 44127 7b57b9295d98
permissions -rw-r--r--
add nat => enat coercion
     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