# HG changeset patch
# User huffman
# Date 1277949615 25200
# Node ID 41b7dfdc4941dd1bc0c613cf2002207a47850331
# Parent  a5400b94d2dd4e7eca2c1f6f84b3b32240ef8838
generalize more euclidean_space lemmas

diff -r a5400b94d2dd -r 41b7dfdc4941 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Jun 30 11:51:35 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Jun 30 19:00:15 2010 -0700
@@ -88,9 +88,17 @@
   "a \<in> s \<Longrightarrow> open s \<Longrightarrow> ((f has_derivative f') (at a within s) \<longleftrightarrow> (f has_derivative f') (at a))"
   unfolding has_derivative_within has_derivative_at using Lim_within_open by auto
 
-lemma derivative_is_linear: fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space" shows
+lemma bounded_linear_imp_linear: "bounded_linear f \<Longrightarrow> linear f" (* TODO: move elsewhere *)
+proof -
+  assume "bounded_linear f"
+  then interpret f: bounded_linear f .
+  show "linear f"
+    by (simp add: f.add f.scaleR linear_def)
+qed
+
+lemma derivative_is_linear:
   "(f has_derivative f') net \<Longrightarrow> linear f'"
-  unfolding has_derivative_def and linear_conv_bounded_linear by auto
+  by (rule derivative_linear [THEN bounded_linear_imp_linear])
 
 subsection {* Combining theorems. *}
 
@@ -166,14 +174,21 @@
   using lf
   by (auto simp add: linear_def algebra_simps)
 
-lemma has_derivative_vmul_component: fixes c::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space" and v::"'c::euclidean_space"
+lemma bounded_linear_euclidean_component: "bounded_linear (\<lambda>x. x $$ k)"
+  unfolding euclidean_component_def
+  by (rule inner.bounded_linear_right)
+
+lemma has_derivative_vmul_component: fixes c::"'a::real_normed_vector \<Rightarrow> 'b::euclidean_space" and v::"'c::real_normed_vector"
   assumes "(c has_derivative c') net"
   shows "((\<lambda>x. c(x)$$k *\<^sub>R v) has_derivative (\<lambda>x. (c' x)$$k *\<^sub>R v)) net" proof-
   have *:"\<And>y. (c y $$ k *\<^sub>R v - (c (netlimit net) $$ k *\<^sub>R v + c' (y - netlimit net) $$ k *\<^sub>R v)) = 
         (c y $$ k - (c (netlimit net) $$ k + c' (y - netlimit net) $$ k)) *\<^sub>R v" 
     unfolding scaleR_left_diff_distrib scaleR_left_distrib by auto
-  show ?thesis unfolding has_derivative_def and * and linear_conv_bounded_linear[symmetric]
-    apply(rule,rule linear_vmul_component[of c' k v]) defer 
+  show ?thesis unfolding has_derivative_def and *
+    apply (rule conjI)
+    apply (rule bounded_linear_compose [OF scaleR.bounded_linear_left])
+    apply (rule bounded_linear_compose [OF bounded_linear_euclidean_component])
+    apply (rule derivative_linear [OF assms])
     apply(subst scaleR_zero_left[THEN sym, of v]) unfolding scaleR_scaleR apply(rule Lim_vmul)
     using assms[unfolded has_derivative_def] unfolding Lim o_def apply- apply(cases "trivial_limit net")
     apply(rule,assumption,rule disjI2,rule,rule) proof-
@@ -192,14 +207,15 @@
         using component_le_norm[of "(1 / norm (x - netlimit net)) *\<^sub>R
           (c x - (c (netlimit net) + c' (x - netlimit net))) - 0" k] by auto
     qed
-  qed(insert assms[unfolded has_derivative_def], auto simp add:linear_conv_bounded_linear) qed 
+  qed
+qed
 
-lemma has_derivative_vmul_within: fixes c::"real \<Rightarrow> real" and v::"'a::euclidean_space"
+lemma has_derivative_vmul_within: fixes c::"real \<Rightarrow> real"
   assumes "(c has_derivative c') (at x within s)"
   shows "((\<lambda>x. (c x) *\<^sub>R v) has_derivative (\<lambda>x. (c' x) *\<^sub>R v)) (at x within s)"
   using has_derivative_vmul_component[OF assms, of 0 v] by auto
 
-lemma has_derivative_vmul_at: fixes c::"real \<Rightarrow> real" and v::"'a::euclidean_space"
+lemma has_derivative_vmul_at: fixes c::"real \<Rightarrow> real"
   assumes "(c has_derivative c') (at x)"
   shows "((\<lambda>x. (c x) *\<^sub>R v) has_derivative (\<lambda>x. (c' x) *\<^sub>R v)) (at x)"
   using has_derivative_vmul_within[where s=UNIV] and assms by(auto simp add: within_UNIV)
@@ -279,9 +295,9 @@
  "f differentiable net \<longleftrightarrow> (f has_derivative (frechet_derivative f net)) net"
   unfolding frechet_derivative_def differentiable_def and some_eq_ex[of "\<lambda> f' . (f has_derivative f') net"] ..
 
-lemma linear_frechet_derivative: fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+lemma linear_frechet_derivative:
   shows "f differentiable net \<Longrightarrow> linear(frechet_derivative f net)"
-  unfolding frechet_derivative_works has_derivative_def unfolding linear_conv_bounded_linear by auto
+  unfolding frechet_derivative_works has_derivative_def by (auto intro: bounded_linear_imp_linear)
 
 subsection {* Differentiability implies continuity. *}
 
@@ -442,13 +458,13 @@
   unfolding differentiable_def apply(erule exE)+ apply(rule_tac x="\<lambda>z. f' z - f'a z" in exI)
     apply(rule has_derivative_sub) by auto 
 
-lemma differentiable_setsum: fixes f::"'a \<Rightarrow> ('n::euclidean_space \<Rightarrow> 'n::euclidean_space)"
+lemma differentiable_setsum:
   assumes "finite s" "\<forall>a\<in>s. (f a) differentiable net"
   shows "(\<lambda>x. setsum (\<lambda>a. f a x) s) differentiable net" proof-
   guess f' using bchoice[OF assms(2)[unfolded differentiable_def]] ..
   thus ?thesis unfolding differentiable_def apply- apply(rule,rule has_derivative_setsum[where f'=f'],rule assms(1)) by auto qed
 
-lemma differentiable_setsum_numseg: fixes f::"_ \<Rightarrow> ('n::euclidean_space \<Rightarrow> 'n::euclidean_space)"
+lemma differentiable_setsum_numseg:
   shows "\<forall>i. m \<le> i \<and> i \<le> n \<longrightarrow> (f i) differentiable net \<Longrightarrow> (\<lambda>x. setsum (\<lambda>a. f a x) {m::nat..n}) differentiable net"
   apply(rule differentiable_setsum) using finite_atLeastAtMost[of n m] by auto
 
@@ -466,7 +482,7 @@
 (* The general result is a bit messy because we need approachability of the  *)
 (* limit point from any direction. But OK for nontrivial intervals etc. *}
     
-lemma frechet_derivative_unique_within: fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+lemma frechet_derivative_unique_within: fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   assumes "(f has_derivative f') (at x within s)" "(f has_derivative f'') (at x within s)"
   "(\<forall>i<DIM('a). \<forall>e>0. \<exists>d. 0 < abs(d) \<and> abs(d) < e \<and> (x + d *\<^sub>R basis i) \<in> s)" shows "f' = f''" proof-
   note as = assms(1,2)[unfolded has_derivative_def]
@@ -491,7 +507,7 @@
       unfolding dist_norm unfolding f'.scaleR f''.scaleR f'.add f''.add f'.diff f''.diff
         scaleR_scaleR scaleR_right_diff_distrib scaleR_right_distrib using i by auto qed qed
 
-lemma frechet_derivative_unique_at: fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+lemma frechet_derivative_unique_at: fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   shows "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f'') (at x) \<Longrightarrow> f' = f''"
   apply(rule frechet_derivative_unique_within[of f f' x UNIV f'']) unfolding within_UNIV apply(assumption)+
   apply(rule,rule,rule,rule) apply(rule_tac x="e/2" in exI) by auto
@@ -499,7 +515,7 @@
 lemma "isCont f x = continuous (at x) f" unfolding isCont_def LIM_def
   unfolding continuous_at Lim_at unfolding dist_nz by auto
 
-lemma frechet_derivative_unique_within_closed_interval: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::ordered_euclidean_space"
+lemma frechet_derivative_unique_within_closed_interval: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"
   assumes "\<forall>i<DIM('a). a$$i < b$$i" "x \<in> {a..b}" (is "x\<in>?I") and
   "(f has_derivative f' ) (at x within {a..b})" and
   "(f has_derivative f'') (at x within {a..b})"
@@ -520,7 +536,7 @@
       using assms(1)[THEN spec[where x=i]] and `e>0` and assms(2)
       unfolding mem_interval euclidean_simps basis_component using i by(auto simp add:field_simps) qed qed
 
-lemma frechet_derivative_unique_within_open_interval: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::ordered_euclidean_space"
+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)
@@ -537,12 +553,12 @@
     using `e>0` and assms(1) unfolding mem_interval euclidean_simps apply safe unfolding basis_component
     by(auto simp add:field_simps) qed
 
-lemma frechet_derivative_at: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::ordered_euclidean_space"
+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))"
   apply(rule frechet_derivative_unique_at[of f],assumption)
   unfolding frechet_derivative_works[THEN sym] using differentiable_def by auto
 
-lemma frechet_derivative_within_closed_interval: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::ordered_euclidean_space"
+lemma frechet_derivative_within_closed_interval: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"
   assumes "\<forall>i<DIM('a). a$$i < b$$i" "x \<in> {a..b}" "(f has_derivative f') (at x within {a.. b})"
   shows "frechet_derivative f (at x within {a.. b}) = f'"
   apply(rule frechet_derivative_unique_within_closed_interval[where f=f])