src/HOL/Library/Euclidean_Space.thy
 changeset 31538 16068eb224c0 parent 31518 feaf9071f8b9 parent 31529 689f5dae1f41 child 31566 eff95000aae7
```     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Tue Jun 09 19:41:27 2009 +0200
1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Tue Jun 09 11:12:08 2009 -0700
1.3 @@ -1783,6 +1783,36 @@
1.4    then show ?thesis using Kp by blast
1.5  qed
1.6
1.7 +lemma smult_conv_scaleR: "c *s x = scaleR c x"
1.8 +  unfolding vector_scalar_mult_def vector_scaleR_def by simp
1.9 +
1.10 +lemma linear_conv_bounded_linear:
1.11 +  fixes f :: "real ^ _ \<Rightarrow> real ^ _"
1.12 +  shows "linear f \<longleftrightarrow> bounded_linear f"
1.13 +proof
1.14 +  assume "linear f"
1.15 +  show "bounded_linear f"
1.16 +  proof
1.17 +    fix x y show "f (x + y) = f x + f y"
1.18 +      using `linear f` unfolding linear_def by simp
1.19 +  next
1.20 +    fix r x show "f (scaleR r x) = scaleR r (f x)"
1.21 +      using `linear f` unfolding linear_def
1.22 +      by (simp add: smult_conv_scaleR)
1.23 +  next
1.24 +    have "\<exists>B. \<forall>x. norm (f x) \<le> B * norm x"
1.25 +      using `linear f` by (rule linear_bounded)
1.26 +    thus "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K"
1.27 +      by (simp add: mult_commute)
1.28 +  qed
1.29 +next
1.30 +  assume "bounded_linear f"
1.31 +  then interpret f: bounded_linear f .
1.32 +  show "linear f"
1.33 +    unfolding linear_def smult_conv_scaleR
1.35 +qed
1.36 +
1.37  subsection{* Bilinear functions. *}
1.38
1.39  definition "bilinear f \<longleftrightarrow> (\<forall>x. linear(\<lambda>y. f x y)) \<and> (\<forall>y. linear(\<lambda>x. f x y))"
1.40 @@ -1886,6 +1916,41 @@
1.41    with Kp show ?thesis by blast
1.42  qed
1.43
1.44 +lemma bilinear_conv_bounded_bilinear:
1.45 +  fixes h :: "real ^ _ \<Rightarrow> real ^ _ \<Rightarrow> real ^ _"
1.46 +  shows "bilinear h \<longleftrightarrow> bounded_bilinear h"
1.47 +proof
1.48 +  assume "bilinear h"
1.49 +  show "bounded_bilinear h"
1.50 +  proof
1.51 +    fix x y z show "h (x + y) z = h x z + h y z"
1.52 +      using `bilinear h` unfolding bilinear_def linear_def by simp
1.53 +  next
1.54 +    fix x y z show "h x (y + z) = h x y + h x z"
1.55 +      using `bilinear h` unfolding bilinear_def linear_def by simp
1.56 +  next
1.57 +    fix r x y show "h (scaleR r x) y = scaleR r (h x y)"
1.58 +      using `bilinear h` unfolding bilinear_def linear_def
1.59 +      by (simp add: smult_conv_scaleR)
1.60 +  next
1.61 +    fix r x y show "h x (scaleR r y) = scaleR r (h x y)"
1.62 +      using `bilinear h` unfolding bilinear_def linear_def
1.63 +      by (simp add: smult_conv_scaleR)
1.64 +  next
1.65 +    have "\<exists>B. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
1.66 +      using `bilinear h` by (rule bilinear_bounded)
1.67 +    thus "\<exists>K. \<forall>x y. norm (h x y) \<le> norm x * norm y * K"
1.68 +      by (simp add: mult_ac)
1.69 +  qed
1.70 +next
1.71 +  assume "bounded_bilinear h"
1.72 +  then interpret h: bounded_bilinear h .
1.73 +  show "bilinear h"
1.74 +    unfolding bilinear_def linear_conv_bounded_linear
1.75 +    using h.bounded_linear_left h.bounded_linear_right
1.76 +    by simp
1.77 +qed
1.78 +