src/HOL/Real_Vector_Spaces.thy
changeset 61916 7950ae6d3266
parent 61915 e9812a95d108
child 61942 f02b26f7d39d
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Tue Dec 22 21:58:27 2015 +0100
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Wed Dec 23 14:36:45 2015 +0100
     1.3 @@ -1435,6 +1435,43 @@
     1.4    "(x ** y - a ** b) = (x - a) ** (y - b) + (x - a) ** b + a ** (y - b)"
     1.5  by (simp add: diff_left diff_right)
     1.6  
     1.7 +lemma flip: "bounded_bilinear (\<lambda>x y. y ** x)"
     1.8 +  apply standard
     1.9 +  apply (rule add_right)
    1.10 +  apply (rule add_left)
    1.11 +  apply (rule scaleR_right)
    1.12 +  apply (rule scaleR_left)
    1.13 +  apply (subst mult.commute)
    1.14 +  using bounded
    1.15 +  apply blast
    1.16 +  done
    1.17 +
    1.18 +lemma comp1:
    1.19 +  assumes "bounded_linear g"
    1.20 +  shows "bounded_bilinear (\<lambda>x. op ** (g x))"
    1.21 +proof unfold_locales
    1.22 +  interpret g: bounded_linear g by fact
    1.23 +  show "\<And>a a' b. g (a + a') ** b = g a ** b + g a' ** b"
    1.24 +    "\<And>a b b'. g a ** (b + b') = g a ** b + g a ** b'"
    1.25 +    "\<And>r a b. g (r *\<^sub>R a) ** b = r *\<^sub>R (g a ** b)"
    1.26 +    "\<And>a r b. g a ** (r *\<^sub>R b) = r *\<^sub>R (g a ** b)"
    1.27 +    by (auto simp: g.add add_left add_right g.scaleR scaleR_left scaleR_right)
    1.28 +  from g.nonneg_bounded nonneg_bounded
    1.29 +  obtain K L
    1.30 +  where nn: "0 \<le> K" "0 \<le> L"
    1.31 +    and K: "\<And>x. norm (g x) \<le> norm x * K"
    1.32 +    and L: "\<And>a b. norm (a ** b) \<le> norm a * norm b * L"
    1.33 +    by auto
    1.34 +  have "norm (g a ** b) \<le> norm a * K * norm b * L" for a b
    1.35 +    by (auto intro!:  order_trans[OF K] order_trans[OF L] mult_mono simp: nn)
    1.36 +  then show "\<exists>K. \<forall>a b. norm (g a ** b) \<le> norm a * norm b * K"
    1.37 +    by (auto intro!: exI[where x="K * L"] simp: ac_simps)
    1.38 +qed
    1.39 +
    1.40 +lemma comp:
    1.41 +  "bounded_linear f \<Longrightarrow> bounded_linear g \<Longrightarrow> bounded_bilinear (\<lambda>x y. f x ** g y)"
    1.42 +  by (rule bounded_bilinear.flip[OF bounded_bilinear.comp1[OF bounded_bilinear.flip[OF comp1]]])
    1.43 +
    1.44  end
    1.45  
    1.46  lemma bounded_linear_ident[simp]: "bounded_linear (\<lambda>x. x)"