1.1 --- a/src/HOL/Library/FrechetDeriv.thy	Sat Jul 03 00:50:35 2010 +0200
     1.2 +++ b/src/HOL/Library/FrechetDeriv.thy	Sun Jul 04 09:25:17 2010 -0700
     1.3 @@ -139,6 +139,47 @@
     1.4     \<Longrightarrow> FDERIV (\<lambda>x. f x - g x) x :> (\<lambda>h. F h - G h)"
     1.5  by (simp only: diff_minus FDERIV_add FDERIV_minus)
     1.6  
     1.7 +subsection {* Uniqueness *}
     1.8 +
     1.9 +lemma FDERIV_zero_unique:
    1.10 +  assumes "FDERIV (\<lambda>x. 0) x :> F" shows "F = (\<lambda>h. 0)"
    1.11 +proof -
    1.12 +  interpret F: bounded_linear F
    1.13 +    using assms by (rule FDERIV_bounded_linear)
    1.14 +  let ?r = "\<lambda>h. norm (F h) / norm h"
    1.15 +  have *: "?r -- 0 --> 0"
    1.16 +    using assms unfolding fderiv_def by simp
    1.17 +  show "F = (\<lambda>h. 0)"
    1.18 +  proof
    1.19 +    fix h show "F h = 0"
    1.20 +    proof (rule ccontr)
    1.21 +      assume "F h \<noteq> 0"
    1.22 +      moreover from this have h: "h \<noteq> 0"
    1.23 +        by (clarsimp simp add: F.zero)
    1.24 +      ultimately have "0 < ?r h"
    1.25 +        by (simp add: divide_pos_pos)
    1.26 +      from LIM_D [OF * this] obtain s where s: "0 < s"
    1.27 +        and r: "\<And>x. x \<noteq> 0 \<Longrightarrow> norm x < s \<Longrightarrow> ?r x < ?r h" by auto
    1.28 +      from dense [OF s] obtain t where t: "0 < t \<and> t < s" ..
    1.29 +      let ?x = "scaleR (t / norm h) h"
    1.30 +      have "?x \<noteq> 0" and "norm ?x < s" using t h by simp_all
    1.31 +      hence "?r ?x < ?r h" by (rule r)
    1.32 +      thus "False" using t h by (simp add: F.scaleR)
    1.33 +    qed
    1.34 +  qed
    1.35 +qed
    1.36 +
    1.37 +lemma FDERIV_unique:
    1.38 +  assumes "FDERIV f x :> F" and "FDERIV f x :> F'" shows "F = F'"
    1.39 +proof -
    1.40 +  have "FDERIV (\<lambda>x. 0) x :> (\<lambda>h. F h - F' h)"
    1.41 +    using FDERIV_diff [OF assms] by simp
    1.42 +  hence "(\<lambda>h. F h - F' h) = (\<lambda>h. 0)"
    1.43 +    by (rule FDERIV_zero_unique)
    1.44 +  thus "F = F'"
    1.45 +    unfolding expand_fun_eq right_minus_eq .
    1.46 +qed
    1.47 +
    1.48  subsection {* Continuity *}
    1.49  
    1.50  lemma FDERIV_isCont:
    1.51 @@ -470,7 +511,7 @@
    1.52        also have "\<dots> = norm (?inv (x + h) - ?inv x) * norm (?inv x)"
    1.53          by simp
    1.54        finally show "norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h
    1.55 -            \<le> norm (?inv (x + h) - ?inv x) * norm (?inv x)" .   
    1.56 +            \<le> norm (?inv (x + h) - ?inv x) * norm (?inv x)" .
    1.57      qed
    1.58    qed
    1.59  qed