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.34 +    by (simp add: f.add f.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 +
    1.79  subsection{* Adjoints. *}
    1.80  
    1.81  definition "adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"