# HG changeset patch
# User huffman
# Date 1278260717 25200
# Node ID daea777692764e1f971b7c28b91203d7db8de65a
# Parent  c6161bee84860f4fabb5ddc0df82eaa25380b574
uniqueness of Frechet derivative

diff -r c6161bee8486 -r daea77769276 src/HOL/Library/FrechetDeriv.thy
--- a/src/HOL/Library/FrechetDeriv.thy	Sat Jul 03 00:50:35 2010 +0200
+++ b/src/HOL/Library/FrechetDeriv.thy	Sun Jul 04 09:25:17 2010 -0700
@@ -139,6 +139,47 @@
    \<Longrightarrow> FDERIV (\<lambda>x. f x - g x) x :> (\<lambda>h. F h - G h)"
 by (simp only: diff_minus FDERIV_add FDERIV_minus)
 
+subsection {* Uniqueness *}
+
+lemma FDERIV_zero_unique:
+  assumes "FDERIV (\<lambda>x. 0) x :> F" shows "F = (\<lambda>h. 0)"
+proof -
+  interpret F: bounded_linear F
+    using assms by (rule FDERIV_bounded_linear)
+  let ?r = "\<lambda>h. norm (F h) / norm h"
+  have *: "?r -- 0 --> 0"
+    using assms unfolding fderiv_def by simp
+  show "F = (\<lambda>h. 0)"
+  proof
+    fix h show "F h = 0"
+    proof (rule ccontr)
+      assume "F h \<noteq> 0"
+      moreover from this have h: "h \<noteq> 0"
+        by (clarsimp simp add: F.zero)
+      ultimately have "0 < ?r h"
+        by (simp add: divide_pos_pos)
+      from LIM_D [OF * this] obtain s where s: "0 < s"
+        and r: "\<And>x. x \<noteq> 0 \<Longrightarrow> norm x < s \<Longrightarrow> ?r x < ?r h" by auto
+      from dense [OF s] obtain t where t: "0 < t \<and> t < s" ..
+      let ?x = "scaleR (t / norm h) h"
+      have "?x \<noteq> 0" and "norm ?x < s" using t h by simp_all
+      hence "?r ?x < ?r h" by (rule r)
+      thus "False" using t h by (simp add: F.scaleR)
+    qed
+  qed
+qed
+
+lemma FDERIV_unique:
+  assumes "FDERIV f x :> F" and "FDERIV f x :> F'" shows "F = F'"
+proof -
+  have "FDERIV (\<lambda>x. 0) x :> (\<lambda>h. F h - F' h)"
+    using FDERIV_diff [OF assms] by simp
+  hence "(\<lambda>h. F h - F' h) = (\<lambda>h. 0)"
+    by (rule FDERIV_zero_unique)
+  thus "F = F'"
+    unfolding expand_fun_eq right_minus_eq .
+qed
+
 subsection {* Continuity *}
 
 lemma FDERIV_isCont:
@@ -470,7 +511,7 @@
       also have "\<dots> = norm (?inv (x + h) - ?inv x) * norm (?inv x)"
         by simp
       finally show "norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h
-            \<le> norm (?inv (x + h) - ?inv x) * norm (?inv x)" .   
+            \<le> norm (?inv (x + h) - ?inv x) * norm (?inv x)" .
     qed
   qed
 qed