move FrechetDeriv.thy to Library
authorhuffman
Wed Feb 18 19:51:39 2009 -0800 (2009-02-18)
changeset 299866b1ccda8bf19
parent 29985 57975b45ab70
child 29987 391dcbd7e4dd
move FrechetDeriv.thy to Library
src/HOL/Complex_Main.thy
src/HOL/FrechetDeriv.thy
src/HOL/IsaMakefile
src/HOL/Library/FrechetDeriv.thy
src/HOL/Library/Library.thy
     1.1 --- a/src/HOL/Complex_Main.thy	Wed Feb 18 19:32:26 2009 -0800
     1.2 +++ b/src/HOL/Complex_Main.thy	Wed Feb 18 19:51:39 2009 -0800
     1.3 @@ -9,7 +9,6 @@
     1.4    Ln
     1.5    Taylor
     1.6    Integration
     1.7 -  FrechetDeriv
     1.8  begin
     1.9  
    1.10  end
     2.1 --- a/src/HOL/FrechetDeriv.thy	Wed Feb 18 19:32:26 2009 -0800
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,503 +0,0 @@
     2.4 -(*  Title       : FrechetDeriv.thy
     2.5 -    ID          : $Id$
     2.6 -    Author      : Brian Huffman
     2.7 -*)
     2.8 -
     2.9 -header {* Frechet Derivative *}
    2.10 -
    2.11 -theory FrechetDeriv
    2.12 -imports Lim
    2.13 -begin
    2.14 -
    2.15 -definition
    2.16 -  fderiv ::
    2.17 -  "['a::real_normed_vector \<Rightarrow> 'b::real_normed_vector, 'a, 'a \<Rightarrow> 'b] \<Rightarrow> bool"
    2.18 -    -- {* Frechet derivative: D is derivative of function f at x *}
    2.19 -          ("(FDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where
    2.20 -  "FDERIV f x :> D = (bounded_linear D \<and>
    2.21 -    (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0)"
    2.22 -
    2.23 -lemma FDERIV_I:
    2.24 -  "\<lbrakk>bounded_linear D; (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0\<rbrakk>
    2.25 -   \<Longrightarrow> FDERIV f x :> D"
    2.26 -by (simp add: fderiv_def)
    2.27 -
    2.28 -lemma FDERIV_D:
    2.29 -  "FDERIV f x :> D \<Longrightarrow> (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0"
    2.30 -by (simp add: fderiv_def)
    2.31 -
    2.32 -lemma FDERIV_bounded_linear: "FDERIV f x :> D \<Longrightarrow> bounded_linear D"
    2.33 -by (simp add: fderiv_def)
    2.34 -
    2.35 -lemma bounded_linear_zero:
    2.36 -  "bounded_linear (\<lambda>x::'a::real_normed_vector. 0::'b::real_normed_vector)"
    2.37 -proof
    2.38 -  show "(0::'b) = 0 + 0" by simp
    2.39 -  fix r show "(0::'b) = scaleR r 0" by simp
    2.40 -  have "\<forall>x::'a. norm (0::'b) \<le> norm x * 0" by simp
    2.41 -  thus "\<exists>K. \<forall>x::'a. norm (0::'b) \<le> norm x * K" ..
    2.42 -qed
    2.43 -
    2.44 -lemma FDERIV_const: "FDERIV (\<lambda>x. k) x :> (\<lambda>h. 0)"
    2.45 -by (simp add: fderiv_def bounded_linear_zero)
    2.46 -
    2.47 -lemma bounded_linear_ident:
    2.48 -  "bounded_linear (\<lambda>x::'a::real_normed_vector. x)"
    2.49 -proof
    2.50 -  fix x y :: 'a show "x + y = x + y" by simp
    2.51 -  fix r and x :: 'a show "scaleR r x = scaleR r x" by simp
    2.52 -  have "\<forall>x::'a. norm x \<le> norm x * 1" by simp
    2.53 -  thus "\<exists>K. \<forall>x::'a. norm x \<le> norm x * K" ..
    2.54 -qed
    2.55 -
    2.56 -lemma FDERIV_ident: "FDERIV (\<lambda>x. x) x :> (\<lambda>h. h)"
    2.57 -by (simp add: fderiv_def bounded_linear_ident)
    2.58 -
    2.59 -subsection {* Addition *}
    2.60 -
    2.61 -lemma add_diff_add:
    2.62 -  fixes a b c d :: "'a::ab_group_add"
    2.63 -  shows "(a + c) - (b + d) = (a - b) + (c - d)"
    2.64 -by simp
    2.65 -
    2.66 -lemma bounded_linear_add:
    2.67 -  assumes "bounded_linear f"
    2.68 -  assumes "bounded_linear g"
    2.69 -  shows "bounded_linear (\<lambda>x. f x + g x)"
    2.70 -proof -
    2.71 -  interpret f: bounded_linear f by fact
    2.72 -  interpret g: bounded_linear g by fact
    2.73 -  show ?thesis apply (unfold_locales)
    2.74 -    apply (simp only: f.add g.add add_ac)
    2.75 -    apply (simp only: f.scaleR g.scaleR scaleR_right_distrib)
    2.76 -    apply (rule f.pos_bounded [THEN exE], rename_tac Kf)
    2.77 -    apply (rule g.pos_bounded [THEN exE], rename_tac Kg)
    2.78 -    apply (rule_tac x="Kf + Kg" in exI, safe)
    2.79 -    apply (subst right_distrib)
    2.80 -    apply (rule order_trans [OF norm_triangle_ineq])
    2.81 -    apply (rule add_mono, erule spec, erule spec)
    2.82 -    done
    2.83 -qed
    2.84 -
    2.85 -lemma norm_ratio_ineq:
    2.86 -  fixes x y :: "'a::real_normed_vector"
    2.87 -  fixes h :: "'b::real_normed_vector"
    2.88 -  shows "norm (x + y) / norm h \<le> norm x / norm h + norm y / norm h"
    2.89 -apply (rule ord_le_eq_trans)
    2.90 -apply (rule divide_right_mono)
    2.91 -apply (rule norm_triangle_ineq)
    2.92 -apply (rule norm_ge_zero)
    2.93 -apply (rule add_divide_distrib)
    2.94 -done
    2.95 -
    2.96 -lemma FDERIV_add:
    2.97 -  assumes f: "FDERIV f x :> F"
    2.98 -  assumes g: "FDERIV g x :> G"
    2.99 -  shows "FDERIV (\<lambda>x. f x + g x) x :> (\<lambda>h. F h + G h)"
   2.100 -proof (rule FDERIV_I)
   2.101 -  show "bounded_linear (\<lambda>h. F h + G h)"
   2.102 -    apply (rule bounded_linear_add)
   2.103 -    apply (rule FDERIV_bounded_linear [OF f])
   2.104 -    apply (rule FDERIV_bounded_linear [OF g])
   2.105 -    done
   2.106 -next
   2.107 -  have f': "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h) -- 0 --> 0"
   2.108 -    using f by (rule FDERIV_D)
   2.109 -  have g': "(\<lambda>h. norm (g (x + h) - g x - G h) / norm h) -- 0 --> 0"
   2.110 -    using g by (rule FDERIV_D)
   2.111 -  from f' g'
   2.112 -  have "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h
   2.113 -           + norm (g (x + h) - g x - G h) / norm h) -- 0 --> 0"
   2.114 -    by (rule LIM_add_zero)
   2.115 -  thus "(\<lambda>h. norm (f (x + h) + g (x + h) - (f x + g x) - (F h + G h))
   2.116 -           / norm h) -- 0 --> 0"
   2.117 -    apply (rule real_LIM_sandwich_zero)
   2.118 -     apply (simp add: divide_nonneg_pos)
   2.119 -    apply (simp only: add_diff_add)
   2.120 -    apply (rule norm_ratio_ineq)
   2.121 -    done
   2.122 -qed
   2.123 -
   2.124 -subsection {* Subtraction *}
   2.125 -
   2.126 -lemma bounded_linear_minus:
   2.127 -  assumes "bounded_linear f"
   2.128 -  shows "bounded_linear (\<lambda>x. - f x)"
   2.129 -proof -
   2.130 -  interpret f: bounded_linear f by fact
   2.131 -  show ?thesis apply (unfold_locales)
   2.132 -    apply (simp add: f.add)
   2.133 -    apply (simp add: f.scaleR)
   2.134 -    apply (simp add: f.bounded)
   2.135 -    done
   2.136 -qed
   2.137 -
   2.138 -lemma FDERIV_minus:
   2.139 -  "FDERIV f x :> F \<Longrightarrow> FDERIV (\<lambda>x. - f x) x :> (\<lambda>h. - F h)"
   2.140 -apply (rule FDERIV_I)
   2.141 -apply (rule bounded_linear_minus)
   2.142 -apply (erule FDERIV_bounded_linear)
   2.143 -apply (simp only: fderiv_def minus_diff_minus norm_minus_cancel)
   2.144 -done
   2.145 -
   2.146 -lemma FDERIV_diff:
   2.147 -  "\<lbrakk>FDERIV f x :> F; FDERIV g x :> G\<rbrakk>
   2.148 -   \<Longrightarrow> FDERIV (\<lambda>x. f x - g x) x :> (\<lambda>h. F h - G h)"
   2.149 -by (simp only: diff_minus FDERIV_add FDERIV_minus)
   2.150 -
   2.151 -subsection {* Continuity *}
   2.152 -
   2.153 -lemma FDERIV_isCont:
   2.154 -  assumes f: "FDERIV f x :> F"
   2.155 -  shows "isCont f x"
   2.156 -proof -
   2.157 -  from f interpret F: bounded_linear "F" by (rule FDERIV_bounded_linear)
   2.158 -  have "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h) -- 0 --> 0"
   2.159 -    by (rule FDERIV_D [OF f])
   2.160 -  hence "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h * norm h) -- 0 --> 0"
   2.161 -    by (intro LIM_mult_zero LIM_norm_zero LIM_ident)
   2.162 -  hence "(\<lambda>h. norm (f (x + h) - f x - F h)) -- 0 --> 0"
   2.163 -    by (simp cong: LIM_cong)
   2.164 -  hence "(\<lambda>h. f (x + h) - f x - F h) -- 0 --> 0"
   2.165 -    by (rule LIM_norm_zero_cancel)
   2.166 -  hence "(\<lambda>h. f (x + h) - f x - F h + F h) -- 0 --> 0"
   2.167 -    by (intro LIM_add_zero F.LIM_zero LIM_ident)
   2.168 -  hence "(\<lambda>h. f (x + h) - f x) -- 0 --> 0"
   2.169 -    by simp
   2.170 -  thus "isCont f x"
   2.171 -    unfolding isCont_iff by (rule LIM_zero_cancel)
   2.172 -qed
   2.173 -
   2.174 -subsection {* Composition *}
   2.175 -
   2.176 -lemma real_divide_cancel_lemma:
   2.177 -  fixes a b c :: real
   2.178 -  shows "(b = 0 \<Longrightarrow> a = 0) \<Longrightarrow> (a / b) * (b / c) = a / c"
   2.179 -by simp
   2.180 -
   2.181 -lemma bounded_linear_compose:
   2.182 -  assumes "bounded_linear f"
   2.183 -  assumes "bounded_linear g"
   2.184 -  shows "bounded_linear (\<lambda>x. f (g x))"
   2.185 -proof -
   2.186 -  interpret f: bounded_linear f by fact
   2.187 -  interpret g: bounded_linear g by fact
   2.188 -  show ?thesis proof (unfold_locales)
   2.189 -    fix x y show "f (g (x + y)) = f (g x) + f (g y)"
   2.190 -      by (simp only: f.add g.add)
   2.191 -  next
   2.192 -    fix r x show "f (g (scaleR r x)) = scaleR r (f (g x))"
   2.193 -      by (simp only: f.scaleR g.scaleR)
   2.194 -  next
   2.195 -    from f.pos_bounded
   2.196 -    obtain Kf where f: "\<And>x. norm (f x) \<le> norm x * Kf" and Kf: "0 < Kf" by fast
   2.197 -    from g.pos_bounded
   2.198 -    obtain Kg where g: "\<And>x. norm (g x) \<le> norm x * Kg" by fast
   2.199 -    show "\<exists>K. \<forall>x. norm (f (g x)) \<le> norm x * K"
   2.200 -    proof (intro exI allI)
   2.201 -      fix x
   2.202 -      have "norm (f (g x)) \<le> norm (g x) * Kf"
   2.203 -	using f .
   2.204 -      also have "\<dots> \<le> (norm x * Kg) * Kf"
   2.205 -	using g Kf [THEN order_less_imp_le] by (rule mult_right_mono)
   2.206 -      also have "(norm x * Kg) * Kf = norm x * (Kg * Kf)"
   2.207 -	by (rule mult_assoc)
   2.208 -      finally show "norm (f (g x)) \<le> norm x * (Kg * Kf)" .
   2.209 -    qed
   2.210 -  qed
   2.211 -qed
   2.212 -
   2.213 -lemma FDERIV_compose:
   2.214 -  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   2.215 -  fixes g :: "'b::real_normed_vector \<Rightarrow> 'c::real_normed_vector"
   2.216 -  assumes f: "FDERIV f x :> F"
   2.217 -  assumes g: "FDERIV g (f x) :> G"
   2.218 -  shows "FDERIV (\<lambda>x. g (f x)) x :> (\<lambda>h. G (F h))"
   2.219 -proof (rule FDERIV_I)
   2.220 -  from FDERIV_bounded_linear [OF g] FDERIV_bounded_linear [OF f]
   2.221 -  show "bounded_linear (\<lambda>h. G (F h))"
   2.222 -    by (rule bounded_linear_compose)
   2.223 -next
   2.224 -  let ?Rf = "\<lambda>h. f (x + h) - f x - F h"
   2.225 -  let ?Rg = "\<lambda>k. g (f x + k) - g (f x) - G k"
   2.226 -  let ?k = "\<lambda>h. f (x + h) - f x"
   2.227 -  let ?Nf = "\<lambda>h. norm (?Rf h) / norm h"
   2.228 -  let ?Ng = "\<lambda>h. norm (?Rg (?k h)) / norm (?k h)"
   2.229 -  from f interpret F!: bounded_linear "F" by (rule FDERIV_bounded_linear)
   2.230 -  from g interpret G!: bounded_linear "G" by (rule FDERIV_bounded_linear)
   2.231 -  from F.bounded obtain kF where kF: "\<And>x. norm (F x) \<le> norm x * kF" by fast
   2.232 -  from G.bounded obtain kG where kG: "\<And>x. norm (G x) \<le> norm x * kG" by fast
   2.233 -
   2.234 -  let ?fun2 = "\<lambda>h. ?Nf h * kG + ?Ng h * (?Nf h + kF)"
   2.235 -
   2.236 -  show "(\<lambda>h. norm (g (f (x + h)) - g (f x) - G (F h)) / norm h) -- 0 --> 0"
   2.237 -  proof (rule real_LIM_sandwich_zero)
   2.238 -    have Nf: "?Nf -- 0 --> 0"
   2.239 -      using FDERIV_D [OF f] .
   2.240 -
   2.241 -    have Ng1: "isCont (\<lambda>k. norm (?Rg k) / norm k) 0"
   2.242 -      by (simp add: isCont_def FDERIV_D [OF g])
   2.243 -    have Ng2: "?k -- 0 --> 0"
   2.244 -      apply (rule LIM_zero)
   2.245 -      apply (fold isCont_iff)
   2.246 -      apply (rule FDERIV_isCont [OF f])
   2.247 -      done
   2.248 -    have Ng: "?Ng -- 0 --> 0"
   2.249 -      using isCont_LIM_compose [OF Ng1 Ng2] by simp
   2.250 -
   2.251 -    have "(\<lambda>h. ?Nf h * kG + ?Ng h * (?Nf h + kF))
   2.252 -           -- 0 --> 0 * kG + 0 * (0 + kF)"
   2.253 -      by (intro LIM_add LIM_mult LIM_const Nf Ng)
   2.254 -    thus "(\<lambda>h. ?Nf h * kG + ?Ng h * (?Nf h + kF)) -- 0 --> 0"
   2.255 -      by simp
   2.256 -  next
   2.257 -    fix h::'a assume h: "h \<noteq> 0"
   2.258 -    thus "0 \<le> norm (g (f (x + h)) - g (f x) - G (F h)) / norm h"
   2.259 -      by (simp add: divide_nonneg_pos)
   2.260 -  next
   2.261 -    fix h::'a assume h: "h \<noteq> 0"
   2.262 -    have "g (f (x + h)) - g (f x) - G (F h) = G (?Rf h) + ?Rg (?k h)"
   2.263 -      by (simp add: G.diff)
   2.264 -    hence "norm (g (f (x + h)) - g (f x) - G (F h)) / norm h
   2.265 -           = norm (G (?Rf h) + ?Rg (?k h)) / norm h"
   2.266 -      by (rule arg_cong)
   2.267 -    also have "\<dots> \<le> norm (G (?Rf h)) / norm h + norm (?Rg (?k h)) / norm h"
   2.268 -      by (rule norm_ratio_ineq)
   2.269 -    also have "\<dots> \<le> ?Nf h * kG + ?Ng h * (?Nf h + kF)"
   2.270 -    proof (rule add_mono)
   2.271 -      show "norm (G (?Rf h)) / norm h \<le> ?Nf h * kG"
   2.272 -        apply (rule ord_le_eq_trans)
   2.273 -        apply (rule divide_right_mono [OF kG norm_ge_zero])
   2.274 -        apply simp
   2.275 -        done
   2.276 -    next
   2.277 -      have "norm (?Rg (?k h)) / norm h = ?Ng h * (norm (?k h) / norm h)"
   2.278 -        apply (rule real_divide_cancel_lemma [symmetric])
   2.279 -        apply (simp add: G.zero)
   2.280 -        done
   2.281 -      also have "\<dots> \<le> ?Ng h * (?Nf h + kF)"
   2.282 -      proof (rule mult_left_mono)
   2.283 -        have "norm (?k h) / norm h = norm (?Rf h + F h) / norm h"
   2.284 -          by simp
   2.285 -        also have "\<dots> \<le> ?Nf h + norm (F h) / norm h"
   2.286 -          by (rule norm_ratio_ineq)
   2.287 -        also have "\<dots> \<le> ?Nf h + kF"
   2.288 -          apply (rule add_left_mono)
   2.289 -          apply (subst pos_divide_le_eq, simp add: h)
   2.290 -          apply (subst mult_commute)
   2.291 -          apply (rule kF)
   2.292 -          done
   2.293 -        finally show "norm (?k h) / norm h \<le> ?Nf h + kF" .
   2.294 -      next
   2.295 -        show "0 \<le> ?Ng h"
   2.296 -        apply (case_tac "f (x + h) - f x = 0", simp)
   2.297 -        apply (rule divide_nonneg_pos [OF norm_ge_zero])
   2.298 -        apply simp
   2.299 -        done
   2.300 -      qed
   2.301 -      finally show "norm (?Rg (?k h)) / norm h \<le> ?Ng h * (?Nf h + kF)" .
   2.302 -    qed
   2.303 -    finally show "norm (g (f (x + h)) - g (f x) - G (F h)) / norm h
   2.304 -        \<le> ?Nf h * kG + ?Ng h * (?Nf h + kF)" .
   2.305 -  qed
   2.306 -qed
   2.307 -
   2.308 -subsection {* Product Rule *}
   2.309 -
   2.310 -lemma (in bounded_bilinear) FDERIV_lemma:
   2.311 -  "a' ** b' - a ** b - (a ** B + A ** b)
   2.312 -   = a ** (b' - b - B) + (a' - a - A) ** b' + A ** (b' - b)"
   2.313 -by (simp add: diff_left diff_right)
   2.314 -
   2.315 -lemma (in bounded_bilinear) FDERIV:
   2.316 -  fixes x :: "'d::real_normed_vector"
   2.317 -  assumes f: "FDERIV f x :> F"
   2.318 -  assumes g: "FDERIV g x :> G"
   2.319 -  shows "FDERIV (\<lambda>x. f x ** g x) x :> (\<lambda>h. f x ** G h + F h ** g x)"
   2.320 -proof (rule FDERIV_I)
   2.321 -  show "bounded_linear (\<lambda>h. f x ** G h + F h ** g x)"
   2.322 -    apply (rule bounded_linear_add)
   2.323 -    apply (rule bounded_linear_compose [OF bounded_linear_right])
   2.324 -    apply (rule FDERIV_bounded_linear [OF g])
   2.325 -    apply (rule bounded_linear_compose [OF bounded_linear_left])
   2.326 -    apply (rule FDERIV_bounded_linear [OF f])
   2.327 -    done
   2.328 -next
   2.329 -  from bounded_linear.bounded [OF FDERIV_bounded_linear [OF f]]
   2.330 -  obtain KF where norm_F: "\<And>x. norm (F x) \<le> norm x * KF" by fast
   2.331 -
   2.332 -  from pos_bounded obtain K where K: "0 < K" and norm_prod:
   2.333 -    "\<And>a b. norm (a ** b) \<le> norm a * norm b * K" by fast
   2.334 -
   2.335 -  let ?Rf = "\<lambda>h. f (x + h) - f x - F h"
   2.336 -  let ?Rg = "\<lambda>h. g (x + h) - g x - G h"
   2.337 -
   2.338 -  let ?fun1 = "\<lambda>h.
   2.339 -        norm (f x ** ?Rg h + ?Rf h ** g (x + h) + F h ** (g (x + h) - g x)) /
   2.340 -        norm h"
   2.341 -
   2.342 -  let ?fun2 = "\<lambda>h.
   2.343 -        norm (f x) * (norm (?Rg h) / norm h) * K +
   2.344 -        norm (?Rf h) / norm h * norm (g (x + h)) * K +
   2.345 -        KF * norm (g (x + h) - g x) * K"
   2.346 -
   2.347 -  have "?fun1 -- 0 --> 0"
   2.348 -  proof (rule real_LIM_sandwich_zero)
   2.349 -    from f g isCont_iff [THEN iffD1, OF FDERIV_isCont [OF g]]
   2.350 -    have "?fun2 -- 0 -->
   2.351 -          norm (f x) * 0 * K + 0 * norm (g x) * K + KF * norm (0::'b) * K"
   2.352 -      by (intro LIM_add LIM_mult LIM_const LIM_norm LIM_zero FDERIV_D)
   2.353 -    thus "?fun2 -- 0 --> 0"
   2.354 -      by simp
   2.355 -  next
   2.356 -    fix h::'d assume "h \<noteq> 0"
   2.357 -    thus "0 \<le> ?fun1 h"
   2.358 -      by (simp add: divide_nonneg_pos)
   2.359 -  next
   2.360 -    fix h::'d assume "h \<noteq> 0"
   2.361 -    have "?fun1 h \<le> (norm (f x) * norm (?Rg h) * K +
   2.362 -         norm (?Rf h) * norm (g (x + h)) * K +
   2.363 -         norm h * KF * norm (g (x + h) - g x) * K) / norm h"
   2.364 -      by (intro
   2.365 -        divide_right_mono mult_mono'
   2.366 -        order_trans [OF norm_triangle_ineq add_mono]
   2.367 -        order_trans [OF norm_prod mult_right_mono]
   2.368 -        mult_nonneg_nonneg order_refl norm_ge_zero norm_F
   2.369 -        K [THEN order_less_imp_le]
   2.370 -      )
   2.371 -    also have "\<dots> = ?fun2 h"
   2.372 -      by (simp add: add_divide_distrib)
   2.373 -    finally show "?fun1 h \<le> ?fun2 h" .
   2.374 -  qed
   2.375 -  thus "(\<lambda>h.
   2.376 -    norm (f (x + h) ** g (x + h) - f x ** g x - (f x ** G h + F h ** g x))
   2.377 -    / norm h) -- 0 --> 0"
   2.378 -    by (simp only: FDERIV_lemma)
   2.379 -qed
   2.380 -
   2.381 -lemmas FDERIV_mult = mult.FDERIV
   2.382 -
   2.383 -lemmas FDERIV_scaleR = scaleR.FDERIV
   2.384 -
   2.385 -
   2.386 -subsection {* Powers *}
   2.387 -
   2.388 -lemma FDERIV_power_Suc:
   2.389 -  fixes x :: "'a::{real_normed_algebra,recpower,comm_ring_1}"
   2.390 -  shows "FDERIV (\<lambda>x. x ^ Suc n) x :> (\<lambda>h. (1 + of_nat n) * x ^ n * h)"
   2.391 - apply (induct n)
   2.392 -  apply (simp add: power_Suc FDERIV_ident)
   2.393 - apply (drule FDERIV_mult [OF FDERIV_ident])
   2.394 - apply (simp only: of_nat_Suc left_distrib mult_1_left)
   2.395 - apply (simp only: power_Suc right_distrib add_ac mult_ac)
   2.396 -done
   2.397 -
   2.398 -lemma FDERIV_power:
   2.399 -  fixes x :: "'a::{real_normed_algebra,recpower,comm_ring_1}"
   2.400 -  shows "FDERIV (\<lambda>x. x ^ n) x :> (\<lambda>h. of_nat n * x ^ (n - 1) * h)"
   2.401 -  apply (cases n)
   2.402 -   apply (simp add: FDERIV_const)
   2.403 -  apply (simp add: FDERIV_power_Suc)
   2.404 -  done
   2.405 -
   2.406 -
   2.407 -subsection {* Inverse *}
   2.408 -
   2.409 -lemma inverse_diff_inverse:
   2.410 -  "\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk>
   2.411 -   \<Longrightarrow> inverse a - inverse b = - (inverse a * (a - b) * inverse b)"
   2.412 -by (simp add: right_diff_distrib left_diff_distrib mult_assoc)
   2.413 -
   2.414 -lemmas bounded_linear_mult_const =
   2.415 -  mult.bounded_linear_left [THEN bounded_linear_compose]
   2.416 -
   2.417 -lemmas bounded_linear_const_mult =
   2.418 -  mult.bounded_linear_right [THEN bounded_linear_compose]
   2.419 -
   2.420 -lemma FDERIV_inverse:
   2.421 -  fixes x :: "'a::real_normed_div_algebra"
   2.422 -  assumes x: "x \<noteq> 0"
   2.423 -  shows "FDERIV inverse x :> (\<lambda>h. - (inverse x * h * inverse x))"
   2.424 -        (is "FDERIV ?inv _ :> _")
   2.425 -proof (rule FDERIV_I)
   2.426 -  show "bounded_linear (\<lambda>h. - (?inv x * h * ?inv x))"
   2.427 -    apply (rule bounded_linear_minus)
   2.428 -    apply (rule bounded_linear_mult_const)
   2.429 -    apply (rule bounded_linear_const_mult)
   2.430 -    apply (rule bounded_linear_ident)
   2.431 -    done
   2.432 -next
   2.433 -  show "(\<lambda>h. norm (?inv (x + h) - ?inv x - - (?inv x * h * ?inv x)) / norm h)
   2.434 -        -- 0 --> 0"
   2.435 -  proof (rule LIM_equal2)
   2.436 -    show "0 < norm x" using x by simp
   2.437 -  next
   2.438 -    fix h::'a
   2.439 -    assume 1: "h \<noteq> 0"
   2.440 -    assume "norm (h - 0) < norm x"
   2.441 -    hence "h \<noteq> -x" by clarsimp
   2.442 -    hence 2: "x + h \<noteq> 0"
   2.443 -      apply (rule contrapos_nn)
   2.444 -      apply (rule sym)
   2.445 -      apply (erule equals_zero_I)
   2.446 -      done
   2.447 -    show "norm (?inv (x + h) - ?inv x - - (?inv x * h * ?inv x)) / norm h
   2.448 -          = norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h"
   2.449 -      apply (subst inverse_diff_inverse [OF 2 x])
   2.450 -      apply (subst minus_diff_minus)
   2.451 -      apply (subst norm_minus_cancel)
   2.452 -      apply (simp add: left_diff_distrib)
   2.453 -      done
   2.454 -  next
   2.455 -    show "(\<lambda>h. norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h)
   2.456 -          -- 0 --> 0"
   2.457 -    proof (rule real_LIM_sandwich_zero)
   2.458 -      show "(\<lambda>h. norm (?inv (x + h) - ?inv x) * norm (?inv x))
   2.459 -            -- 0 --> 0"
   2.460 -        apply (rule LIM_mult_left_zero)
   2.461 -        apply (rule LIM_norm_zero)
   2.462 -        apply (rule LIM_zero)
   2.463 -        apply (rule LIM_offset_zero)
   2.464 -        apply (rule LIM_inverse)
   2.465 -        apply (rule LIM_ident)
   2.466 -        apply (rule x)
   2.467 -        done
   2.468 -    next
   2.469 -      fix h::'a assume h: "h \<noteq> 0"
   2.470 -      show "0 \<le> norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h"
   2.471 -        apply (rule divide_nonneg_pos)
   2.472 -        apply (rule norm_ge_zero)
   2.473 -        apply (simp add: h)
   2.474 -        done
   2.475 -    next
   2.476 -      fix h::'a assume h: "h \<noteq> 0"
   2.477 -      have "norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h
   2.478 -            \<le> norm (?inv (x + h) - ?inv x) * norm h * norm (?inv x) / norm h"
   2.479 -        apply (rule divide_right_mono [OF _ norm_ge_zero])
   2.480 -        apply (rule order_trans [OF norm_mult_ineq])
   2.481 -        apply (rule mult_right_mono [OF _ norm_ge_zero])
   2.482 -        apply (rule norm_mult_ineq)
   2.483 -        done
   2.484 -      also have "\<dots> = norm (?inv (x + h) - ?inv x) * norm (?inv x)"
   2.485 -        by simp
   2.486 -      finally show "norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h
   2.487 -            \<le> norm (?inv (x + h) - ?inv x) * norm (?inv x)" .   
   2.488 -    qed
   2.489 -  qed
   2.490 -qed
   2.491 -
   2.492 -subsection {* Alternate definition *}
   2.493 -
   2.494 -lemma field_fderiv_def:
   2.495 -  fixes x :: "'a::real_normed_field" shows
   2.496 -  "FDERIV f x :> (\<lambda>h. h * D) = (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
   2.497 - apply (unfold fderiv_def)
   2.498 - apply (simp add: mult.bounded_linear_left)
   2.499 - apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric])
   2.500 - apply (subst diff_divide_distrib)
   2.501 - apply (subst times_divide_eq_left [symmetric])
   2.502 - apply (simp cong: LIM_cong)
   2.503 - apply (simp add: LIM_norm_zero_iff LIM_zero_iff)
   2.504 -done
   2.505 -
   2.506 -end
     3.1 --- a/src/HOL/IsaMakefile	Wed Feb 18 19:32:26 2009 -0800
     3.2 +++ b/src/HOL/IsaMakefile	Wed Feb 18 19:51:39 2009 -0800
     3.3 @@ -271,7 +271,6 @@
     3.4    Complex.thy \
     3.5    Deriv.thy \
     3.6    Fact.thy \
     3.7 -  FrechetDeriv.thy \
     3.8    Integration.thy \
     3.9    Lim.thy \
    3.10    Ln.thy \
    3.11 @@ -315,6 +314,7 @@
    3.12    Library/Executable_Set.thy Library/Infinite_Set.thy			\
    3.13    Library/FuncSet.thy Library/Permutations.thy Library/Determinants.thy\
    3.14    Library/Finite_Cartesian_Product.thy \
    3.15 +  Library/FrechetDeriv.thy \
    3.16    Library/Fundamental_Theorem_Algebra.thy \
    3.17    Library/Library.thy Library/List_Prefix.thy Library/State_Monad.thy	\
    3.18    Library/Nat_Int_Bij.thy Library/Multiset.thy Library/Permutation.thy	\
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Library/FrechetDeriv.thy	Wed Feb 18 19:51:39 2009 -0800
     4.3 @@ -0,0 +1,503 @@
     4.4 +(*  Title       : FrechetDeriv.thy
     4.5 +    ID          : $Id$
     4.6 +    Author      : Brian Huffman
     4.7 +*)
     4.8 +
     4.9 +header {* Frechet Derivative *}
    4.10 +
    4.11 +theory FrechetDeriv
    4.12 +imports Lim
    4.13 +begin
    4.14 +
    4.15 +definition
    4.16 +  fderiv ::
    4.17 +  "['a::real_normed_vector \<Rightarrow> 'b::real_normed_vector, 'a, 'a \<Rightarrow> 'b] \<Rightarrow> bool"
    4.18 +    -- {* Frechet derivative: D is derivative of function f at x *}
    4.19 +          ("(FDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where
    4.20 +  "FDERIV f x :> D = (bounded_linear D \<and>
    4.21 +    (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0)"
    4.22 +
    4.23 +lemma FDERIV_I:
    4.24 +  "\<lbrakk>bounded_linear D; (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0\<rbrakk>
    4.25 +   \<Longrightarrow> FDERIV f x :> D"
    4.26 +by (simp add: fderiv_def)
    4.27 +
    4.28 +lemma FDERIV_D:
    4.29 +  "FDERIV f x :> D \<Longrightarrow> (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0"
    4.30 +by (simp add: fderiv_def)
    4.31 +
    4.32 +lemma FDERIV_bounded_linear: "FDERIV f x :> D \<Longrightarrow> bounded_linear D"
    4.33 +by (simp add: fderiv_def)
    4.34 +
    4.35 +lemma bounded_linear_zero:
    4.36 +  "bounded_linear (\<lambda>x::'a::real_normed_vector. 0::'b::real_normed_vector)"
    4.37 +proof
    4.38 +  show "(0::'b) = 0 + 0" by simp
    4.39 +  fix r show "(0::'b) = scaleR r 0" by simp
    4.40 +  have "\<forall>x::'a. norm (0::'b) \<le> norm x * 0" by simp
    4.41 +  thus "\<exists>K. \<forall>x::'a. norm (0::'b) \<le> norm x * K" ..
    4.42 +qed
    4.43 +
    4.44 +lemma FDERIV_const: "FDERIV (\<lambda>x. k) x :> (\<lambda>h. 0)"
    4.45 +by (simp add: fderiv_def bounded_linear_zero)
    4.46 +
    4.47 +lemma bounded_linear_ident:
    4.48 +  "bounded_linear (\<lambda>x::'a::real_normed_vector. x)"
    4.49 +proof
    4.50 +  fix x y :: 'a show "x + y = x + y" by simp
    4.51 +  fix r and x :: 'a show "scaleR r x = scaleR r x" by simp
    4.52 +  have "\<forall>x::'a. norm x \<le> norm x * 1" by simp
    4.53 +  thus "\<exists>K. \<forall>x::'a. norm x \<le> norm x * K" ..
    4.54 +qed
    4.55 +
    4.56 +lemma FDERIV_ident: "FDERIV (\<lambda>x. x) x :> (\<lambda>h. h)"
    4.57 +by (simp add: fderiv_def bounded_linear_ident)
    4.58 +
    4.59 +subsection {* Addition *}
    4.60 +
    4.61 +lemma add_diff_add:
    4.62 +  fixes a b c d :: "'a::ab_group_add"
    4.63 +  shows "(a + c) - (b + d) = (a - b) + (c - d)"
    4.64 +by simp
    4.65 +
    4.66 +lemma bounded_linear_add:
    4.67 +  assumes "bounded_linear f"
    4.68 +  assumes "bounded_linear g"
    4.69 +  shows "bounded_linear (\<lambda>x. f x + g x)"
    4.70 +proof -
    4.71 +  interpret f: bounded_linear f by fact
    4.72 +  interpret g: bounded_linear g by fact
    4.73 +  show ?thesis apply (unfold_locales)
    4.74 +    apply (simp only: f.add g.add add_ac)
    4.75 +    apply (simp only: f.scaleR g.scaleR scaleR_right_distrib)
    4.76 +    apply (rule f.pos_bounded [THEN exE], rename_tac Kf)
    4.77 +    apply (rule g.pos_bounded [THEN exE], rename_tac Kg)
    4.78 +    apply (rule_tac x="Kf + Kg" in exI, safe)
    4.79 +    apply (subst right_distrib)
    4.80 +    apply (rule order_trans [OF norm_triangle_ineq])
    4.81 +    apply (rule add_mono, erule spec, erule spec)
    4.82 +    done
    4.83 +qed
    4.84 +
    4.85 +lemma norm_ratio_ineq:
    4.86 +  fixes x y :: "'a::real_normed_vector"
    4.87 +  fixes h :: "'b::real_normed_vector"
    4.88 +  shows "norm (x + y) / norm h \<le> norm x / norm h + norm y / norm h"
    4.89 +apply (rule ord_le_eq_trans)
    4.90 +apply (rule divide_right_mono)
    4.91 +apply (rule norm_triangle_ineq)
    4.92 +apply (rule norm_ge_zero)
    4.93 +apply (rule add_divide_distrib)
    4.94 +done
    4.95 +
    4.96 +lemma FDERIV_add:
    4.97 +  assumes f: "FDERIV f x :> F"
    4.98 +  assumes g: "FDERIV g x :> G"
    4.99 +  shows "FDERIV (\<lambda>x. f x + g x) x :> (\<lambda>h. F h + G h)"
   4.100 +proof (rule FDERIV_I)
   4.101 +  show "bounded_linear (\<lambda>h. F h + G h)"
   4.102 +    apply (rule bounded_linear_add)
   4.103 +    apply (rule FDERIV_bounded_linear [OF f])
   4.104 +    apply (rule FDERIV_bounded_linear [OF g])
   4.105 +    done
   4.106 +next
   4.107 +  have f': "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h) -- 0 --> 0"
   4.108 +    using f by (rule FDERIV_D)
   4.109 +  have g': "(\<lambda>h. norm (g (x + h) - g x - G h) / norm h) -- 0 --> 0"
   4.110 +    using g by (rule FDERIV_D)
   4.111 +  from f' g'
   4.112 +  have "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h
   4.113 +           + norm (g (x + h) - g x - G h) / norm h) -- 0 --> 0"
   4.114 +    by (rule LIM_add_zero)
   4.115 +  thus "(\<lambda>h. norm (f (x + h) + g (x + h) - (f x + g x) - (F h + G h))
   4.116 +           / norm h) -- 0 --> 0"
   4.117 +    apply (rule real_LIM_sandwich_zero)
   4.118 +     apply (simp add: divide_nonneg_pos)
   4.119 +    apply (simp only: add_diff_add)
   4.120 +    apply (rule norm_ratio_ineq)
   4.121 +    done
   4.122 +qed
   4.123 +
   4.124 +subsection {* Subtraction *}
   4.125 +
   4.126 +lemma bounded_linear_minus:
   4.127 +  assumes "bounded_linear f"
   4.128 +  shows "bounded_linear (\<lambda>x. - f x)"
   4.129 +proof -
   4.130 +  interpret f: bounded_linear f by fact
   4.131 +  show ?thesis apply (unfold_locales)
   4.132 +    apply (simp add: f.add)
   4.133 +    apply (simp add: f.scaleR)
   4.134 +    apply (simp add: f.bounded)
   4.135 +    done
   4.136 +qed
   4.137 +
   4.138 +lemma FDERIV_minus:
   4.139 +  "FDERIV f x :> F \<Longrightarrow> FDERIV (\<lambda>x. - f x) x :> (\<lambda>h. - F h)"
   4.140 +apply (rule FDERIV_I)
   4.141 +apply (rule bounded_linear_minus)
   4.142 +apply (erule FDERIV_bounded_linear)
   4.143 +apply (simp only: fderiv_def minus_diff_minus norm_minus_cancel)
   4.144 +done
   4.145 +
   4.146 +lemma FDERIV_diff:
   4.147 +  "\<lbrakk>FDERIV f x :> F; FDERIV g x :> G\<rbrakk>
   4.148 +   \<Longrightarrow> FDERIV (\<lambda>x. f x - g x) x :> (\<lambda>h. F h - G h)"
   4.149 +by (simp only: diff_minus FDERIV_add FDERIV_minus)
   4.150 +
   4.151 +subsection {* Continuity *}
   4.152 +
   4.153 +lemma FDERIV_isCont:
   4.154 +  assumes f: "FDERIV f x :> F"
   4.155 +  shows "isCont f x"
   4.156 +proof -
   4.157 +  from f interpret F: bounded_linear "F" by (rule FDERIV_bounded_linear)
   4.158 +  have "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h) -- 0 --> 0"
   4.159 +    by (rule FDERIV_D [OF f])
   4.160 +  hence "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h * norm h) -- 0 --> 0"
   4.161 +    by (intro LIM_mult_zero LIM_norm_zero LIM_ident)
   4.162 +  hence "(\<lambda>h. norm (f (x + h) - f x - F h)) -- 0 --> 0"
   4.163 +    by (simp cong: LIM_cong)
   4.164 +  hence "(\<lambda>h. f (x + h) - f x - F h) -- 0 --> 0"
   4.165 +    by (rule LIM_norm_zero_cancel)
   4.166 +  hence "(\<lambda>h. f (x + h) - f x - F h + F h) -- 0 --> 0"
   4.167 +    by (intro LIM_add_zero F.LIM_zero LIM_ident)
   4.168 +  hence "(\<lambda>h. f (x + h) - f x) -- 0 --> 0"
   4.169 +    by simp
   4.170 +  thus "isCont f x"
   4.171 +    unfolding isCont_iff by (rule LIM_zero_cancel)
   4.172 +qed
   4.173 +
   4.174 +subsection {* Composition *}
   4.175 +
   4.176 +lemma real_divide_cancel_lemma:
   4.177 +  fixes a b c :: real
   4.178 +  shows "(b = 0 \<Longrightarrow> a = 0) \<Longrightarrow> (a / b) * (b / c) = a / c"
   4.179 +by simp
   4.180 +
   4.181 +lemma bounded_linear_compose:
   4.182 +  assumes "bounded_linear f"
   4.183 +  assumes "bounded_linear g"
   4.184 +  shows "bounded_linear (\<lambda>x. f (g x))"
   4.185 +proof -
   4.186 +  interpret f: bounded_linear f by fact
   4.187 +  interpret g: bounded_linear g by fact
   4.188 +  show ?thesis proof (unfold_locales)
   4.189 +    fix x y show "f (g (x + y)) = f (g x) + f (g y)"
   4.190 +      by (simp only: f.add g.add)
   4.191 +  next
   4.192 +    fix r x show "f (g (scaleR r x)) = scaleR r (f (g x))"
   4.193 +      by (simp only: f.scaleR g.scaleR)
   4.194 +  next
   4.195 +    from f.pos_bounded
   4.196 +    obtain Kf where f: "\<And>x. norm (f x) \<le> norm x * Kf" and Kf: "0 < Kf" by fast
   4.197 +    from g.pos_bounded
   4.198 +    obtain Kg where g: "\<And>x. norm (g x) \<le> norm x * Kg" by fast
   4.199 +    show "\<exists>K. \<forall>x. norm (f (g x)) \<le> norm x * K"
   4.200 +    proof (intro exI allI)
   4.201 +      fix x
   4.202 +      have "norm (f (g x)) \<le> norm (g x) * Kf"
   4.203 +	using f .
   4.204 +      also have "\<dots> \<le> (norm x * Kg) * Kf"
   4.205 +	using g Kf [THEN order_less_imp_le] by (rule mult_right_mono)
   4.206 +      also have "(norm x * Kg) * Kf = norm x * (Kg * Kf)"
   4.207 +	by (rule mult_assoc)
   4.208 +      finally show "norm (f (g x)) \<le> norm x * (Kg * Kf)" .
   4.209 +    qed
   4.210 +  qed
   4.211 +qed
   4.212 +
   4.213 +lemma FDERIV_compose:
   4.214 +  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   4.215 +  fixes g :: "'b::real_normed_vector \<Rightarrow> 'c::real_normed_vector"
   4.216 +  assumes f: "FDERIV f x :> F"
   4.217 +  assumes g: "FDERIV g (f x) :> G"
   4.218 +  shows "FDERIV (\<lambda>x. g (f x)) x :> (\<lambda>h. G (F h))"
   4.219 +proof (rule FDERIV_I)
   4.220 +  from FDERIV_bounded_linear [OF g] FDERIV_bounded_linear [OF f]
   4.221 +  show "bounded_linear (\<lambda>h. G (F h))"
   4.222 +    by (rule bounded_linear_compose)
   4.223 +next
   4.224 +  let ?Rf = "\<lambda>h. f (x + h) - f x - F h"
   4.225 +  let ?Rg = "\<lambda>k. g (f x + k) - g (f x) - G k"
   4.226 +  let ?k = "\<lambda>h. f (x + h) - f x"
   4.227 +  let ?Nf = "\<lambda>h. norm (?Rf h) / norm h"
   4.228 +  let ?Ng = "\<lambda>h. norm (?Rg (?k h)) / norm (?k h)"
   4.229 +  from f interpret F!: bounded_linear "F" by (rule FDERIV_bounded_linear)
   4.230 +  from g interpret G!: bounded_linear "G" by (rule FDERIV_bounded_linear)
   4.231 +  from F.bounded obtain kF where kF: "\<And>x. norm (F x) \<le> norm x * kF" by fast
   4.232 +  from G.bounded obtain kG where kG: "\<And>x. norm (G x) \<le> norm x * kG" by fast
   4.233 +
   4.234 +  let ?fun2 = "\<lambda>h. ?Nf h * kG + ?Ng h * (?Nf h + kF)"
   4.235 +
   4.236 +  show "(\<lambda>h. norm (g (f (x + h)) - g (f x) - G (F h)) / norm h) -- 0 --> 0"
   4.237 +  proof (rule real_LIM_sandwich_zero)
   4.238 +    have Nf: "?Nf -- 0 --> 0"
   4.239 +      using FDERIV_D [OF f] .
   4.240 +
   4.241 +    have Ng1: "isCont (\<lambda>k. norm (?Rg k) / norm k) 0"
   4.242 +      by (simp add: isCont_def FDERIV_D [OF g])
   4.243 +    have Ng2: "?k -- 0 --> 0"
   4.244 +      apply (rule LIM_zero)
   4.245 +      apply (fold isCont_iff)
   4.246 +      apply (rule FDERIV_isCont [OF f])
   4.247 +      done
   4.248 +    have Ng: "?Ng -- 0 --> 0"
   4.249 +      using isCont_LIM_compose [OF Ng1 Ng2] by simp
   4.250 +
   4.251 +    have "(\<lambda>h. ?Nf h * kG + ?Ng h * (?Nf h + kF))
   4.252 +           -- 0 --> 0 * kG + 0 * (0 + kF)"
   4.253 +      by (intro LIM_add LIM_mult LIM_const Nf Ng)
   4.254 +    thus "(\<lambda>h. ?Nf h * kG + ?Ng h * (?Nf h + kF)) -- 0 --> 0"
   4.255 +      by simp
   4.256 +  next
   4.257 +    fix h::'a assume h: "h \<noteq> 0"
   4.258 +    thus "0 \<le> norm (g (f (x + h)) - g (f x) - G (F h)) / norm h"
   4.259 +      by (simp add: divide_nonneg_pos)
   4.260 +  next
   4.261 +    fix h::'a assume h: "h \<noteq> 0"
   4.262 +    have "g (f (x + h)) - g (f x) - G (F h) = G (?Rf h) + ?Rg (?k h)"
   4.263 +      by (simp add: G.diff)
   4.264 +    hence "norm (g (f (x + h)) - g (f x) - G (F h)) / norm h
   4.265 +           = norm (G (?Rf h) + ?Rg (?k h)) / norm h"
   4.266 +      by (rule arg_cong)
   4.267 +    also have "\<dots> \<le> norm (G (?Rf h)) / norm h + norm (?Rg (?k h)) / norm h"
   4.268 +      by (rule norm_ratio_ineq)
   4.269 +    also have "\<dots> \<le> ?Nf h * kG + ?Ng h * (?Nf h + kF)"
   4.270 +    proof (rule add_mono)
   4.271 +      show "norm (G (?Rf h)) / norm h \<le> ?Nf h * kG"
   4.272 +        apply (rule ord_le_eq_trans)
   4.273 +        apply (rule divide_right_mono [OF kG norm_ge_zero])
   4.274 +        apply simp
   4.275 +        done
   4.276 +    next
   4.277 +      have "norm (?Rg (?k h)) / norm h = ?Ng h * (norm (?k h) / norm h)"
   4.278 +        apply (rule real_divide_cancel_lemma [symmetric])
   4.279 +        apply (simp add: G.zero)
   4.280 +        done
   4.281 +      also have "\<dots> \<le> ?Ng h * (?Nf h + kF)"
   4.282 +      proof (rule mult_left_mono)
   4.283 +        have "norm (?k h) / norm h = norm (?Rf h + F h) / norm h"
   4.284 +          by simp
   4.285 +        also have "\<dots> \<le> ?Nf h + norm (F h) / norm h"
   4.286 +          by (rule norm_ratio_ineq)
   4.287 +        also have "\<dots> \<le> ?Nf h + kF"
   4.288 +          apply (rule add_left_mono)
   4.289 +          apply (subst pos_divide_le_eq, simp add: h)
   4.290 +          apply (subst mult_commute)
   4.291 +          apply (rule kF)
   4.292 +          done
   4.293 +        finally show "norm (?k h) / norm h \<le> ?Nf h + kF" .
   4.294 +      next
   4.295 +        show "0 \<le> ?Ng h"
   4.296 +        apply (case_tac "f (x + h) - f x = 0", simp)
   4.297 +        apply (rule divide_nonneg_pos [OF norm_ge_zero])
   4.298 +        apply simp
   4.299 +        done
   4.300 +      qed
   4.301 +      finally show "norm (?Rg (?k h)) / norm h \<le> ?Ng h * (?Nf h + kF)" .
   4.302 +    qed
   4.303 +    finally show "norm (g (f (x + h)) - g (f x) - G (F h)) / norm h
   4.304 +        \<le> ?Nf h * kG + ?Ng h * (?Nf h + kF)" .
   4.305 +  qed
   4.306 +qed
   4.307 +
   4.308 +subsection {* Product Rule *}
   4.309 +
   4.310 +lemma (in bounded_bilinear) FDERIV_lemma:
   4.311 +  "a' ** b' - a ** b - (a ** B + A ** b)
   4.312 +   = a ** (b' - b - B) + (a' - a - A) ** b' + A ** (b' - b)"
   4.313 +by (simp add: diff_left diff_right)
   4.314 +
   4.315 +lemma (in bounded_bilinear) FDERIV:
   4.316 +  fixes x :: "'d::real_normed_vector"
   4.317 +  assumes f: "FDERIV f x :> F"
   4.318 +  assumes g: "FDERIV g x :> G"
   4.319 +  shows "FDERIV (\<lambda>x. f x ** g x) x :> (\<lambda>h. f x ** G h + F h ** g x)"
   4.320 +proof (rule FDERIV_I)
   4.321 +  show "bounded_linear (\<lambda>h. f x ** G h + F h ** g x)"
   4.322 +    apply (rule bounded_linear_add)
   4.323 +    apply (rule bounded_linear_compose [OF bounded_linear_right])
   4.324 +    apply (rule FDERIV_bounded_linear [OF g])
   4.325 +    apply (rule bounded_linear_compose [OF bounded_linear_left])
   4.326 +    apply (rule FDERIV_bounded_linear [OF f])
   4.327 +    done
   4.328 +next
   4.329 +  from bounded_linear.bounded [OF FDERIV_bounded_linear [OF f]]
   4.330 +  obtain KF where norm_F: "\<And>x. norm (F x) \<le> norm x * KF" by fast
   4.331 +
   4.332 +  from pos_bounded obtain K where K: "0 < K" and norm_prod:
   4.333 +    "\<And>a b. norm (a ** b) \<le> norm a * norm b * K" by fast
   4.334 +
   4.335 +  let ?Rf = "\<lambda>h. f (x + h) - f x - F h"
   4.336 +  let ?Rg = "\<lambda>h. g (x + h) - g x - G h"
   4.337 +
   4.338 +  let ?fun1 = "\<lambda>h.
   4.339 +        norm (f x ** ?Rg h + ?Rf h ** g (x + h) + F h ** (g (x + h) - g x)) /
   4.340 +        norm h"
   4.341 +
   4.342 +  let ?fun2 = "\<lambda>h.
   4.343 +        norm (f x) * (norm (?Rg h) / norm h) * K +
   4.344 +        norm (?Rf h) / norm h * norm (g (x + h)) * K +
   4.345 +        KF * norm (g (x + h) - g x) * K"
   4.346 +
   4.347 +  have "?fun1 -- 0 --> 0"
   4.348 +  proof (rule real_LIM_sandwich_zero)
   4.349 +    from f g isCont_iff [THEN iffD1, OF FDERIV_isCont [OF g]]
   4.350 +    have "?fun2 -- 0 -->
   4.351 +          norm (f x) * 0 * K + 0 * norm (g x) * K + KF * norm (0::'b) * K"
   4.352 +      by (intro LIM_add LIM_mult LIM_const LIM_norm LIM_zero FDERIV_D)
   4.353 +    thus "?fun2 -- 0 --> 0"
   4.354 +      by simp
   4.355 +  next
   4.356 +    fix h::'d assume "h \<noteq> 0"
   4.357 +    thus "0 \<le> ?fun1 h"
   4.358 +      by (simp add: divide_nonneg_pos)
   4.359 +  next
   4.360 +    fix h::'d assume "h \<noteq> 0"
   4.361 +    have "?fun1 h \<le> (norm (f x) * norm (?Rg h) * K +
   4.362 +         norm (?Rf h) * norm (g (x + h)) * K +
   4.363 +         norm h * KF * norm (g (x + h) - g x) * K) / norm h"
   4.364 +      by (intro
   4.365 +        divide_right_mono mult_mono'
   4.366 +        order_trans [OF norm_triangle_ineq add_mono]
   4.367 +        order_trans [OF norm_prod mult_right_mono]
   4.368 +        mult_nonneg_nonneg order_refl norm_ge_zero norm_F
   4.369 +        K [THEN order_less_imp_le]
   4.370 +      )
   4.371 +    also have "\<dots> = ?fun2 h"
   4.372 +      by (simp add: add_divide_distrib)
   4.373 +    finally show "?fun1 h \<le> ?fun2 h" .
   4.374 +  qed
   4.375 +  thus "(\<lambda>h.
   4.376 +    norm (f (x + h) ** g (x + h) - f x ** g x - (f x ** G h + F h ** g x))
   4.377 +    / norm h) -- 0 --> 0"
   4.378 +    by (simp only: FDERIV_lemma)
   4.379 +qed
   4.380 +
   4.381 +lemmas FDERIV_mult = mult.FDERIV
   4.382 +
   4.383 +lemmas FDERIV_scaleR = scaleR.FDERIV
   4.384 +
   4.385 +
   4.386 +subsection {* Powers *}
   4.387 +
   4.388 +lemma FDERIV_power_Suc:
   4.389 +  fixes x :: "'a::{real_normed_algebra,recpower,comm_ring_1}"
   4.390 +  shows "FDERIV (\<lambda>x. x ^ Suc n) x :> (\<lambda>h. (1 + of_nat n) * x ^ n * h)"
   4.391 + apply (induct n)
   4.392 +  apply (simp add: power_Suc FDERIV_ident)
   4.393 + apply (drule FDERIV_mult [OF FDERIV_ident])
   4.394 + apply (simp only: of_nat_Suc left_distrib mult_1_left)
   4.395 + apply (simp only: power_Suc right_distrib add_ac mult_ac)
   4.396 +done
   4.397 +
   4.398 +lemma FDERIV_power:
   4.399 +  fixes x :: "'a::{real_normed_algebra,recpower,comm_ring_1}"
   4.400 +  shows "FDERIV (\<lambda>x. x ^ n) x :> (\<lambda>h. of_nat n * x ^ (n - 1) * h)"
   4.401 +  apply (cases n)
   4.402 +   apply (simp add: FDERIV_const)
   4.403 +  apply (simp add: FDERIV_power_Suc)
   4.404 +  done
   4.405 +
   4.406 +
   4.407 +subsection {* Inverse *}
   4.408 +
   4.409 +lemma inverse_diff_inverse:
   4.410 +  "\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk>
   4.411 +   \<Longrightarrow> inverse a - inverse b = - (inverse a * (a - b) * inverse b)"
   4.412 +by (simp add: right_diff_distrib left_diff_distrib mult_assoc)
   4.413 +
   4.414 +lemmas bounded_linear_mult_const =
   4.415 +  mult.bounded_linear_left [THEN bounded_linear_compose]
   4.416 +
   4.417 +lemmas bounded_linear_const_mult =
   4.418 +  mult.bounded_linear_right [THEN bounded_linear_compose]
   4.419 +
   4.420 +lemma FDERIV_inverse:
   4.421 +  fixes x :: "'a::real_normed_div_algebra"
   4.422 +  assumes x: "x \<noteq> 0"
   4.423 +  shows "FDERIV inverse x :> (\<lambda>h. - (inverse x * h * inverse x))"
   4.424 +        (is "FDERIV ?inv _ :> _")
   4.425 +proof (rule FDERIV_I)
   4.426 +  show "bounded_linear (\<lambda>h. - (?inv x * h * ?inv x))"
   4.427 +    apply (rule bounded_linear_minus)
   4.428 +    apply (rule bounded_linear_mult_const)
   4.429 +    apply (rule bounded_linear_const_mult)
   4.430 +    apply (rule bounded_linear_ident)
   4.431 +    done
   4.432 +next
   4.433 +  show "(\<lambda>h. norm (?inv (x + h) - ?inv x - - (?inv x * h * ?inv x)) / norm h)
   4.434 +        -- 0 --> 0"
   4.435 +  proof (rule LIM_equal2)
   4.436 +    show "0 < norm x" using x by simp
   4.437 +  next
   4.438 +    fix h::'a
   4.439 +    assume 1: "h \<noteq> 0"
   4.440 +    assume "norm (h - 0) < norm x"
   4.441 +    hence "h \<noteq> -x" by clarsimp
   4.442 +    hence 2: "x + h \<noteq> 0"
   4.443 +      apply (rule contrapos_nn)
   4.444 +      apply (rule sym)
   4.445 +      apply (erule equals_zero_I)
   4.446 +      done
   4.447 +    show "norm (?inv (x + h) - ?inv x - - (?inv x * h * ?inv x)) / norm h
   4.448 +          = norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h"
   4.449 +      apply (subst inverse_diff_inverse [OF 2 x])
   4.450 +      apply (subst minus_diff_minus)
   4.451 +      apply (subst norm_minus_cancel)
   4.452 +      apply (simp add: left_diff_distrib)
   4.453 +      done
   4.454 +  next
   4.455 +    show "(\<lambda>h. norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h)
   4.456 +          -- 0 --> 0"
   4.457 +    proof (rule real_LIM_sandwich_zero)
   4.458 +      show "(\<lambda>h. norm (?inv (x + h) - ?inv x) * norm (?inv x))
   4.459 +            -- 0 --> 0"
   4.460 +        apply (rule LIM_mult_left_zero)
   4.461 +        apply (rule LIM_norm_zero)
   4.462 +        apply (rule LIM_zero)
   4.463 +        apply (rule LIM_offset_zero)
   4.464 +        apply (rule LIM_inverse)
   4.465 +        apply (rule LIM_ident)
   4.466 +        apply (rule x)
   4.467 +        done
   4.468 +    next
   4.469 +      fix h::'a assume h: "h \<noteq> 0"
   4.470 +      show "0 \<le> norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h"
   4.471 +        apply (rule divide_nonneg_pos)
   4.472 +        apply (rule norm_ge_zero)
   4.473 +        apply (simp add: h)
   4.474 +        done
   4.475 +    next
   4.476 +      fix h::'a assume h: "h \<noteq> 0"
   4.477 +      have "norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h
   4.478 +            \<le> norm (?inv (x + h) - ?inv x) * norm h * norm (?inv x) / norm h"
   4.479 +        apply (rule divide_right_mono [OF _ norm_ge_zero])
   4.480 +        apply (rule order_trans [OF norm_mult_ineq])
   4.481 +        apply (rule mult_right_mono [OF _ norm_ge_zero])
   4.482 +        apply (rule norm_mult_ineq)
   4.483 +        done
   4.484 +      also have "\<dots> = norm (?inv (x + h) - ?inv x) * norm (?inv x)"
   4.485 +        by simp
   4.486 +      finally show "norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h
   4.487 +            \<le> norm (?inv (x + h) - ?inv x) * norm (?inv x)" .   
   4.488 +    qed
   4.489 +  qed
   4.490 +qed
   4.491 +
   4.492 +subsection {* Alternate definition *}
   4.493 +
   4.494 +lemma field_fderiv_def:
   4.495 +  fixes x :: "'a::real_normed_field" shows
   4.496 +  "FDERIV f x :> (\<lambda>h. h * D) = (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
   4.497 + apply (unfold fderiv_def)
   4.498 + apply (simp add: mult.bounded_linear_left)
   4.499 + apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric])
   4.500 + apply (subst diff_divide_distrib)
   4.501 + apply (subst times_divide_eq_left [symmetric])
   4.502 + apply (simp cong: LIM_cong)
   4.503 + apply (simp add: LIM_norm_zero_iff LIM_zero_iff)
   4.504 +done
   4.505 +
   4.506 +end
     5.1 --- a/src/HOL/Library/Library.thy	Wed Feb 18 19:32:26 2009 -0800
     5.2 +++ b/src/HOL/Library/Library.thy	Wed Feb 18 19:51:39 2009 -0800
     5.3 @@ -22,6 +22,7 @@
     5.4    Executable_Set
     5.5    Float
     5.6    Formal_Power_Series
     5.7 +  FrechetDeriv
     5.8    FuncSet
     5.9    Fundamental_Theorem_Algebra
    5.10    Infinite_Set