author huffman Sun, 04 Jul 2010 09:25:17 -0700 changeset 37729 daea77769276 parent 37704 c6161bee8486 child 37730 1a24950dae33
uniqueness of Frechet derivative
--- 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"
+      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