transfer rule for bounded_linear of blinfun
authorimmler
Wed Dec 23 14:36:45 2015 +0100 (2015-12-23)
changeset 619167950ae6d3266
parent 61915 e9812a95d108
child 61920 0df21d79fe32
transfer rule for bounded_linear of blinfun
src/HOL/Limits.thy
src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy
src/HOL/Real_Vector_Spaces.thy
     1.1 --- a/src/HOL/Limits.thy	Tue Dec 22 21:58:27 2015 +0100
     1.2 +++ b/src/HOL/Limits.thy	Wed Dec 23 14:36:45 2015 +0100
     1.3 @@ -827,18 +827,6 @@
     1.4      by (rule Zfun_imp_Zfun)
     1.5  qed
     1.6  
     1.7 -lemma (in bounded_bilinear) flip:
     1.8 -  "bounded_bilinear (\<lambda>x y. y ** x)"
     1.9 -  apply standard
    1.10 -  apply (rule add_right)
    1.11 -  apply (rule add_left)
    1.12 -  apply (rule scaleR_right)
    1.13 -  apply (rule scaleR_left)
    1.14 -  apply (subst mult.commute)
    1.15 -  using bounded
    1.16 -  apply blast
    1.17 -  done
    1.18 -
    1.19  lemma (in bounded_bilinear) Bfun_prod_Zfun:
    1.20    assumes f: "Bfun f F"
    1.21    assumes g: "Zfun g F"
     2.1 --- a/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Tue Dec 22 21:58:27 2015 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Wed Dec 23 14:36:45 2015 +0100
     2.3 @@ -594,17 +594,26 @@
     2.4  
     2.5  subsection \<open>concrete bounded linear functions\<close>
     2.6  
     2.7 -lemma bounded_linear_bounded_bilinear_blinfun_applyI: --"TODO: transfer rule!"
     2.8 -  assumes n: "bounded_bilinear (\<lambda>i x. (blinfun_apply (f x) i))"
     2.9 -  shows "bounded_linear f"
    2.10 -proof (unfold_locales, safe intro!: blinfun_eqI)
    2.11 -  fix i
    2.12 -  interpret bounded_bilinear "\<lambda>i x. f x i" by fact
    2.13 -  show "f (x + y) i = (f x + f y) i" "f (r *\<^sub>R x) i = (r *\<^sub>R f x) i" for r x y
    2.14 -    by (auto intro!: blinfun_eqI simp: blinfun.bilinear_simps)
    2.15 -  from _ nonneg_bounded show "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K"
    2.16 -    by (rule ex_reg) (auto intro!: onorm_bound simp: norm_blinfun.rep_eq assms ac_simps)
    2.17 -qed
    2.18 +lemma transfer_bounded_bilinear_bounded_linearI:
    2.19 +  assumes "g = (\<lambda>i x. (blinfun_apply (f i) x))"
    2.20 +  shows "bounded_bilinear g = bounded_linear f"
    2.21 +proof
    2.22 +  assume "bounded_bilinear g"
    2.23 +  then interpret bounded_bilinear f by (simp add: assms)
    2.24 +  show "bounded_linear f"
    2.25 +  proof (unfold_locales, safe intro!: blinfun_eqI)
    2.26 +    fix i
    2.27 +    show "f (x + y) i = (f x + f y) i" "f (r *\<^sub>R x) i = (r *\<^sub>R f x) i" for r x y
    2.28 +      by (auto intro!: blinfun_eqI simp: blinfun.bilinear_simps)
    2.29 +    from _ nonneg_bounded show "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K"
    2.30 +      by (rule ex_reg) (auto intro!: onorm_bound simp: norm_blinfun.rep_eq ac_simps)
    2.31 +  qed
    2.32 +qed (auto simp: assms intro!: blinfun.comp)
    2.33 +
    2.34 +lemma transfer_bounded_bilinear_bounded_linear[transfer_rule]:
    2.35 +  "(rel_fun (rel_fun op = (pcr_blinfun op = op =)) op =) bounded_bilinear bounded_linear"
    2.36 +  by (auto simp: pcr_blinfun_def cr_blinfun_def rel_fun_def OO_def
    2.37 +    intro!: transfer_bounded_bilinear_bounded_linearI)
    2.38  
    2.39  context bounded_bilinear
    2.40  begin
    2.41 @@ -614,14 +623,14 @@
    2.42  declare prod_left.rep_eq[simp]
    2.43  
    2.44  lemma bounded_linear_prod_left[bounded_linear]: "bounded_linear prod_left"
    2.45 -  by (rule bounded_linear_bounded_bilinear_blinfun_applyI) (auto simp: bounded_bilinear_axioms)
    2.46 +  by transfer (rule flip)
    2.47  
    2.48  lift_definition prod_right::"'a \<Rightarrow> 'b \<Rightarrow>\<^sub>L 'c" is "(\<lambda>a b. prod a b)"
    2.49    by (rule bounded_linear_right)
    2.50  declare prod_right.rep_eq[simp]
    2.51  
    2.52  lemma bounded_linear_prod_right[bounded_linear]: "bounded_linear prod_right"
    2.53 -  by (rule bounded_linear_bounded_bilinear_blinfun_applyI) (auto simp: flip)
    2.54 +  by transfer (rule bounded_bilinear_axioms)
    2.55  
    2.56  end
    2.57  
    2.58 @@ -678,8 +687,7 @@
    2.59  declare blinfun_inner_right.rep_eq[simp]
    2.60  
    2.61  lemma bounded_linear_blinfun_inner_right[bounded_linear]: "bounded_linear blinfun_inner_right"
    2.62 -  by (rule bounded_linear_bounded_bilinear_blinfun_applyI)
    2.63 -    (auto simp: bounded_bilinear.flip[OF bounded_bilinear_inner])
    2.64 +  by transfer (rule bounded_bilinear_inner)
    2.65  
    2.66  
    2.67  lift_definition blinfun_inner_left::"'a::real_inner \<Rightarrow> 'a \<Rightarrow>\<^sub>L real" is "\<lambda>x y. y \<bullet> x"
    2.68 @@ -687,7 +695,7 @@
    2.69  declare blinfun_inner_left.rep_eq[simp]
    2.70  
    2.71  lemma bounded_linear_blinfun_inner_left[bounded_linear]: "bounded_linear blinfun_inner_left"
    2.72 -  by (rule bounded_linear_bounded_bilinear_blinfun_applyI) (auto simp: bounded_bilinear_inner)
    2.73 +  by transfer (rule bounded_bilinear.flip[OF bounded_bilinear_inner])
    2.74  
    2.75  
    2.76  lift_definition blinfun_scaleR_right::"real \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a::real_normed_vector" is "op *\<^sub>R"
    2.77 @@ -695,8 +703,7 @@
    2.78  declare blinfun_scaleR_right.rep_eq[simp]
    2.79  
    2.80  lemma bounded_linear_blinfun_scaleR_right[bounded_linear]: "bounded_linear blinfun_scaleR_right"
    2.81 -  by (rule bounded_linear_bounded_bilinear_blinfun_applyI)
    2.82 -    (auto simp: bounded_bilinear.flip[OF bounded_bilinear_scaleR])
    2.83 +  by transfer (rule bounded_bilinear_scaleR)
    2.84  
    2.85  
    2.86  lift_definition blinfun_scaleR_left::"'a::real_normed_vector \<Rightarrow> real \<Rightarrow>\<^sub>L 'a" is "\<lambda>x y. y *\<^sub>R x"
    2.87 @@ -704,7 +711,7 @@
    2.88  lemmas [simp] = blinfun_scaleR_left.rep_eq
    2.89  
    2.90  lemma bounded_linear_blinfun_scaleR_left[bounded_linear]: "bounded_linear blinfun_scaleR_left"
    2.91 -  by (rule bounded_linear_bounded_bilinear_blinfun_applyI) (auto simp: bounded_bilinear_scaleR)
    2.92 +  by transfer (rule bounded_bilinear.flip[OF bounded_bilinear_scaleR])
    2.93  
    2.94  
    2.95  lift_definition blinfun_mult_right::"'a \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a::real_normed_algebra" is "op *"
    2.96 @@ -712,8 +719,7 @@
    2.97  declare blinfun_mult_right.rep_eq[simp]
    2.98  
    2.99  lemma bounded_linear_blinfun_mult_right[bounded_linear]: "bounded_linear blinfun_mult_right"
   2.100 -  by (rule bounded_linear_bounded_bilinear_blinfun_applyI)
   2.101 -    (auto simp: bounded_bilinear.flip[OF bounded_bilinear_mult])
   2.102 +  by transfer (rule bounded_bilinear_mult)
   2.103  
   2.104  
   2.105  lift_definition blinfun_mult_left::"'a::real_normed_algebra \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a" is "\<lambda>x y. y * x"
   2.106 @@ -721,6 +727,6 @@
   2.107  lemmas [simp] = blinfun_mult_left.rep_eq
   2.108  
   2.109  lemma bounded_linear_blinfun_mult_left[bounded_linear]: "bounded_linear blinfun_mult_left"
   2.110 -  by (rule bounded_linear_bounded_bilinear_blinfun_applyI) (auto simp: bounded_bilinear_mult)
   2.111 +  by transfer (rule bounded_bilinear.flip[OF bounded_bilinear_mult])
   2.112  
   2.113  end
     3.1 --- a/src/HOL/Real_Vector_Spaces.thy	Tue Dec 22 21:58:27 2015 +0100
     3.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Wed Dec 23 14:36:45 2015 +0100
     3.3 @@ -1435,6 +1435,43 @@
     3.4    "(x ** y - a ** b) = (x - a) ** (y - b) + (x - a) ** b + a ** (y - b)"
     3.5  by (simp add: diff_left diff_right)
     3.6  
     3.7 +lemma flip: "bounded_bilinear (\<lambda>x y. y ** x)"
     3.8 +  apply standard
     3.9 +  apply (rule add_right)
    3.10 +  apply (rule add_left)
    3.11 +  apply (rule scaleR_right)
    3.12 +  apply (rule scaleR_left)
    3.13 +  apply (subst mult.commute)
    3.14 +  using bounded
    3.15 +  apply blast
    3.16 +  done
    3.17 +
    3.18 +lemma comp1:
    3.19 +  assumes "bounded_linear g"
    3.20 +  shows "bounded_bilinear (\<lambda>x. op ** (g x))"
    3.21 +proof unfold_locales
    3.22 +  interpret g: bounded_linear g by fact
    3.23 +  show "\<And>a a' b. g (a + a') ** b = g a ** b + g a' ** b"
    3.24 +    "\<And>a b b'. g a ** (b + b') = g a ** b + g a ** b'"
    3.25 +    "\<And>r a b. g (r *\<^sub>R a) ** b = r *\<^sub>R (g a ** b)"
    3.26 +    "\<And>a r b. g a ** (r *\<^sub>R b) = r *\<^sub>R (g a ** b)"
    3.27 +    by (auto simp: g.add add_left add_right g.scaleR scaleR_left scaleR_right)
    3.28 +  from g.nonneg_bounded nonneg_bounded
    3.29 +  obtain K L
    3.30 +  where nn: "0 \<le> K" "0 \<le> L"
    3.31 +    and K: "\<And>x. norm (g x) \<le> norm x * K"
    3.32 +    and L: "\<And>a b. norm (a ** b) \<le> norm a * norm b * L"
    3.33 +    by auto
    3.34 +  have "norm (g a ** b) \<le> norm a * K * norm b * L" for a b
    3.35 +    by (auto intro!:  order_trans[OF K] order_trans[OF L] mult_mono simp: nn)
    3.36 +  then show "\<exists>K. \<forall>a b. norm (g a ** b) \<le> norm a * norm b * K"
    3.37 +    by (auto intro!: exI[where x="K * L"] simp: ac_simps)
    3.38 +qed
    3.39 +
    3.40 +lemma comp:
    3.41 +  "bounded_linear f \<Longrightarrow> bounded_linear g \<Longrightarrow> bounded_bilinear (\<lambda>x y. f x ** g y)"
    3.42 +  by (rule bounded_bilinear.flip[OF bounded_bilinear.comp1[OF bounded_bilinear.flip[OF comp1]]])
    3.43 +
    3.44  end
    3.45  
    3.46  lemma bounded_linear_ident[simp]: "bounded_linear (\<lambda>x. x)"