author immler Wed Dec 23 14:36:45 2015 +0100 (2015-12-23) changeset 61916 7950ae6d3266 parent 61915 e9812a95d108 child 61920 0df21d79fe32
transfer rule for bounded_linear of blinfun
```     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.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.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.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)"
```