--- a/src/HOL/Analysis/Lebesgue_Measure.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Wed Jan 10 15:25:09 2018 +0100
@@ -750,10 +750,10 @@
finally show "lebesgue = density (distr lebesgue lebesgue T) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>))" .
qed
-lemma lebesgue_measurable_scaling[measurable]: "op *\<^sub>R x \<in> lebesgue \<rightarrow>\<^sub>M lebesgue"
+lemma lebesgue_measurable_scaling[measurable]: "( *\<^sub>R) x \<in> lebesgue \<rightarrow>\<^sub>M lebesgue"
proof cases
assume "x = 0"
- then have "op *\<^sub>R x = (\<lambda>x. 0::'a)"
+ then have "( *\<^sub>R) x = (\<lambda>x. 0::'a)"
by (auto simp: fun_eq_iff)
then show ?thesis by auto
next
@@ -843,9 +843,9 @@
lemma lborel_distr_mult:
assumes "(c::real) \<noteq> 0"
- shows "distr lborel borel (op * c) = density lborel (\<lambda>_. inverse \<bar>c\<bar>)"
+ shows "distr lborel borel (( * ) c) = density lborel (\<lambda>_. inverse \<bar>c\<bar>)"
proof-
- have "distr lborel borel (op * c) = distr lborel lborel (op * c)" by (simp cong: distr_cong)
+ have "distr lborel borel (( * ) c) = distr lborel lborel (( * ) c)" by (simp cong: distr_cong)
also from assms have "... = density lborel (\<lambda>_. inverse \<bar>c\<bar>)"
by (subst lborel_real_affine[of "inverse c" 0]) (auto simp: o_def distr_density_distr)
finally show ?thesis .
@@ -853,18 +853,18 @@
lemma lborel_distr_mult':
assumes "(c::real) \<noteq> 0"
- shows "lborel = density (distr lborel borel (op * c)) (\<lambda>_. \<bar>c\<bar>)"
+ shows "lborel = density (distr lborel borel (( * ) c)) (\<lambda>_. \<bar>c\<bar>)"
proof-
have "lborel = density lborel (\<lambda>_. 1)" by (rule density_1[symmetric])
also from assms have "(\<lambda>_. 1 :: ennreal) = (\<lambda>_. inverse \<bar>c\<bar> * \<bar>c\<bar>)" by (intro ext) simp
also have "density lborel ... = density (density lborel (\<lambda>_. inverse \<bar>c\<bar>)) (\<lambda>_. \<bar>c\<bar>)"
by (subst density_density_eq) (auto simp: ennreal_mult)
- also from assms have "density lborel (\<lambda>_. inverse \<bar>c\<bar>) = distr lborel borel (op * c)"
+ also from assms have "density lborel (\<lambda>_. inverse \<bar>c\<bar>) = distr lborel borel (( * ) c)"
by (rule lborel_distr_mult[symmetric])
finally show ?thesis .
qed
-lemma lborel_distr_plus: "distr lborel borel (op + c) = (lborel :: real measure)"
+lemma lborel_distr_plus: "distr lborel borel ((+) c) = (lborel :: real measure)"
by (subst lborel_real_affine[of 1 c]) (auto simp: density_1 one_ennreal_def[symmetric])
interpretation lborel: sigma_finite_measure lborel
@@ -885,7 +885,7 @@
"box (la, lb) (ua, ub) = box la ua \<times> box lb ub"
using lu[of _ 0] lu[of 0] by (auto intro!: inj_onI simp add: Basis_prod_def ball_Un box_def)
show "emeasure (lborel \<Otimes>\<^sub>M lborel) (box (la, lb) (ua, ub)) =
- ennreal (prod (op \<bullet> ((ua, ub) - (la, lb))) Basis)"
+ ennreal (prod ((\<bullet>) ((ua, ub) - (la, lb))) Basis)"
by (simp add: lborel.emeasure_pair_measure_Times Basis_prod_def prod.union_disjoint
prod.reindex ennreal_mult inner_diff_left prod_nonneg)
qed (simp add: borel_prod[symmetric])
@@ -994,7 +994,7 @@
let ?f = "\<lambda>n. root DIM('a) (Suc n)"
- have vimage_eq_image: "op *\<^sub>R (?f n) -` S = op *\<^sub>R (1 / ?f n) ` S" for n
+ have vimage_eq_image: "( *\<^sub>R) (?f n) -` S = ( *\<^sub>R) (1 / ?f n) ` S" for n
apply safe
subgoal for x by (rule image_eqI[of _ _ "?f n *\<^sub>R x"]) auto
subgoal by auto
@@ -1016,20 +1016,20 @@
by (intro summable_iff_suminf_neq_top) (auto simp add: inverse_eq_divide)
then have "top * emeasure lebesgue S = (\<Sum>n. (1 / ?f n)^DIM('a) * emeasure lebesgue S)"
unfolding ennreal_suminf_multc eq by simp
- also have "\<dots> = (\<Sum>n. emeasure lebesgue (op *\<^sub>R (?f n) -` S))"
+ also have "\<dots> = (\<Sum>n. emeasure lebesgue (( *\<^sub>R) (?f n) -` S))"
unfolding vimage_eq_image using emeasure_lebesgue_affine[of "1 / ?f n" 0 S for n] by simp
- also have "\<dots> = emeasure lebesgue (\<Union>n. op *\<^sub>R (?f n) -` S)"
+ also have "\<dots> = emeasure lebesgue (\<Union>n. ( *\<^sub>R) (?f n) -` S)"
proof (intro suminf_emeasure)
- show "disjoint_family (\<lambda>n. op *\<^sub>R (?f n) -` S)"
+ show "disjoint_family (\<lambda>n. ( *\<^sub>R) (?f n) -` S)"
unfolding disjoint_family_on_def
proof safe
fix m n :: nat and x assume "m \<noteq> n" "?f m *\<^sub>R x \<in> S" "?f n *\<^sub>R x \<in> S"
with eq1[of "?f m / ?f n" "?f n *\<^sub>R x"] show "x \<in> {}"
by auto
qed
- have "op *\<^sub>R (?f i) -` S \<in> sets lebesgue" for i
+ have "( *\<^sub>R) (?f i) -` S \<in> sets lebesgue" for i
using measurable_sets[OF lebesgue_measurable_scaling[of "?f i"] S] by auto
- then show "range (\<lambda>i. op *\<^sub>R (?f i) -` S) \<subseteq> sets lebesgue"
+ then show "range (\<lambda>i. ( *\<^sub>R) (?f i) -` S) \<subseteq> sets lebesgue"
by auto
qed
also have "\<dots> \<le> emeasure lebesgue (ball 0 M :: 'a set)"