author huffman Wed, 30 Jun 2010 10:26:02 -0700 changeset 37645 5cbd5d5959f2 parent 37644 48bdc2a43b46 child 37646 dbdbebec57df
generalize some euclidean_space lemmas
```--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Jun 30 18:19:53 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Jun 30 10:26:02 2010 -0700
@@ -1891,7 +1891,7 @@
subsection {* Linearity and Bilinearity continued *}

lemma linear_bounded:
-  fixes f:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
assumes lf: "linear f"
shows "\<exists>B. \<forall>x. norm (f x) \<le> B * norm x"
proof-
@@ -1919,7 +1919,7 @@
qed

lemma linear_bounded_pos:
-  fixes f:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
assumes lf: "linear f"
shows "\<exists>B > 0. \<forall>x. norm (f x) \<le> B * norm x"
proof-
@@ -1947,7 +1947,7 @@
qed

lemma linear_conv_bounded_linear:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
shows "linear f \<longleftrightarrow> bounded_linear f"
proof
assume "linear f"
@@ -1971,14 +1971,14 @@
qed

-lemma bounded_linearI': fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+lemma bounded_linearI': fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
assumes "\<And>x y. f (x + y) = f x + f y" "\<And>c x. f (c *\<^sub>R x) = c *\<^sub>R f x"
shows "bounded_linear f" unfolding linear_conv_bounded_linear[THEN sym]
by(rule linearI[OF assms])

lemma bilinear_bounded:
-  fixes h:: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'k::euclidean_space"
+  fixes h:: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'k::real_normed_vector"
assumes bh: "bilinear h"
shows "\<exists>B. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
proof-
@@ -2008,7 +2008,7 @@
qed

lemma bilinear_bounded_pos:
-  fixes h:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::euclidean_space"
+  fixes h:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::real_normed_vector"
assumes bh: "bilinear h"
shows "\<exists>B > 0. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
proof-
@@ -2029,7 +2029,7 @@
qed

lemma bilinear_conv_bounded_bilinear:
-  fixes h :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::euclidean_space"
+  fixes h :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::real_normed_vector"
shows "bilinear h \<longleftrightarrow> bounded_bilinear h"
proof
assume "bilinear h"```