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