# HG changeset patch
# User huffman
# Date 1277958598 25200
# Node ID 181a70d7b52578e0e20883e8d933a786021a60cf
# Parent  f37f6babf51ca18dc8866275353849e299974885
generalize some lemmas about derivatives

diff -r f37f6babf51c -r 181a70d7b525 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Jun 30 21:13:46 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Jun 30 21:29:58 2010 -0700
@@ -539,19 +539,13 @@
 lemma frechet_derivative_unique_within_open_interval: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"
   assumes "x \<in> {a<..<b}" "(f has_derivative f' ) (at x within {a<..<b})"
                          "(f has_derivative f'') (at x within {a<..<b})"
-  shows "f' = f''" apply(rule frechet_derivative_unique_within) apply(rule assms(2-3))+ proof(rule,rule,rule,rule)
-  fix e::real and i assume "e>0" and i:"i<DIM('a)"
-  note * = assms(1)[unfolded mem_interval,rule_format,OF i]
-  have "a $$ i < x $$ i" using  * by auto
-  moreover { have "a $$ i * 2 + min (x $$ i - a $$ i) e \<le> a$$i *2 + x$$i - a$$i" by auto
-  also have "\<dots> = a$$i + x$$i" by auto also have "\<dots> < 2 * x$$i" using * by auto 
-  finally have "a $$ i * 2 + min (x $$ i - a $$ i) e < x $$ i * 2" by auto }
-  moreover have "min (x $$ i - a $$ i) e \<ge> 0" using * and `e>0` by auto
-  hence "x $$ i * 2 < b $$ i * 2 + min (x $$ i - a $$ i) e" using * by auto
-  ultimately show "\<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> x + d *\<^sub>R basis i \<in> {a<..<b}"
-    apply(rule_tac x="- (min (x$$i - a$$i) e) / 2" in exI)
-    using `e>0` and assms(1) unfolding mem_interval euclidean_simps apply safe unfolding basis_component
-    by(auto simp add:field_simps) qed
+  shows "f' = f''"
+proof -
+  from assms(1) have *: "at x within {a<..<b} = at x"
+    by (simp add: at_within_interior interior_open open_interval)
+  from assms(2,3) [unfolded *] show "f' = f''"
+    by (rule frechet_derivative_unique_at)
+qed
 
 lemma frechet_derivative_at: fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   shows "(f has_derivative f') (at x) \<Longrightarrow> (f' = frechet_derivative f (at x))"
@@ -638,7 +632,7 @@
 subsection {* In particular if we have a mapping into @{typ "real"}. *}
 
 lemma differential_zero_maxmin:
-  fixes f::"'a\<Colon>ordered_euclidean_space \<Rightarrow> real"
+  fixes f::"'a\<Colon>euclidean_space \<Rightarrow> real"
   assumes "x \<in> s" "open s"
   and deriv: "(f has_derivative f') (at x)"
   and mono: "(\<forall>y\<in>s. f y \<le> f x) \<or> (\<forall>y\<in>s. f x \<le> f y)"
@@ -1183,8 +1177,7 @@
 
 subsection {* Derivative with composed bilinear function. *}
 
-lemma has_derivative_bilinear_within: fixes h::"'m::euclidean_space \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'p::euclidean_space"
-  and f::"'q::euclidean_space \<Rightarrow> 'm::euclidean_space"
+lemma has_derivative_bilinear_within:
   assumes "(f has_derivative f') (at x within s)" "(g has_derivative g') (at x within s)" "bounded_bilinear h"
   shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x within s)" proof-
   have "(g ---> g x) (at x within s)" apply(rule differentiable_imp_continuous_within[unfolded continuous_within])
@@ -1216,15 +1209,17 @@
 	using as(3)[unfolded dist_norm] and as(2) unfolding pos_less_divide_eq[OF bcd] by (auto simp add:field_simps)
       finally show "dist ((1 / norm (y - x)) *\<^sub>R h (f' (y - x)) (g' (y - x))) 0 < e"
 	unfolding dist_norm apply-apply(cases "y = x") by(auto simp add:field_simps) qed qed
-  have "bounded_linear (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))" unfolding linear_linear linear_def
-    unfolding g'.add f'.scaleR f'.add g'.scaleR 
-    unfolding h.add_right h.add_left scaleR_right_distrib h.scaleR_left h.scaleR_right by auto
+  have "bounded_linear (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))"
+    apply (rule bounded_linear_add)
+    apply (rule bounded_linear_compose [OF h.bounded_linear_right `bounded_linear g'`])
+    apply (rule bounded_linear_compose [OF h.bounded_linear_left `bounded_linear f'`])
+    done
   thus ?thesis using Lim_add[OF * **] unfolding has_derivative_within 
     unfolding g'.add f'.scaleR f'.add g'.scaleR f'.diff g'.diff
      h.add_right h.add_left scaleR_right_distrib h.scaleR_left h.scaleR_right h.diff_right h.diff_left
     scaleR_right_diff_distrib h.zero_right h.zero_left by(auto simp add:field_simps) qed
 
-lemma has_derivative_bilinear_at: fixes h::"'m::euclidean_space \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'p::euclidean_space" and f::"'p::euclidean_space \<Rightarrow> 'm::euclidean_space"
+lemma has_derivative_bilinear_at:
   assumes "(f has_derivative f') (at x)" "(g has_derivative g') (at x)" "bounded_bilinear h"
   shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x)"
   using has_derivative_bilinear_within[of f f' x UNIV g g' h] unfolding within_UNIV using assms by auto
@@ -1313,7 +1308,7 @@
   using has_derivative_sub[OF assms[unfolded has_vector_derivative_def]]
   unfolding has_vector_derivative_def scaleR_right_diff_distrib by auto
 
-lemma has_vector_derivative_bilinear_within: fixes h::"'m::euclidean_space \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'p::euclidean_space"
+lemma has_vector_derivative_bilinear_within:
   assumes "(f has_vector_derivative f') (at x within s)" "(g has_vector_derivative g') (at x within s)" "bounded_bilinear h"
   shows "((\<lambda>x. h (f x) (g x)) has_vector_derivative (h (f x) g' + h f' (g x))) (at x within s)" proof-
   interpret bounded_bilinear h using assms by auto 
@@ -1321,7 +1316,7 @@
     unfolding o_def has_vector_derivative_def
     using assms(3) unfolding scaleR_right scaleR_left scaleR_right_distrib by auto qed
 
-lemma has_vector_derivative_bilinear_at: fixes h::"'m::euclidean_space \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'p::euclidean_space"
+lemma has_vector_derivative_bilinear_at:
   assumes "(f has_vector_derivative f') (at x)" "(g has_vector_derivative g') (at x)" "bounded_bilinear h"
   shows "((\<lambda>x. h (f x) (g x)) has_vector_derivative (h (f x) g' + h f' (g x))) (at x)"
   apply(rule has_vector_derivative_bilinear_within[where s=UNIV, unfolded within_UNIV]) using assms by auto