--- a/src/HOL/Probability/Bochner_Integration.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Probability/Bochner_Integration.thy Sun Sep 13 22:56:52 2015 +0200
@@ -2549,7 +2549,7 @@
assumes "integrable (M1 \<Otimes>\<^sub>M M2) f"
shows "integrable (M2 \<Otimes>\<^sub>M M1) (\<lambda>(x,y). f (y,x))"
proof -
- interpret Q: pair_sigma_finite M2 M1 by default
+ interpret Q: pair_sigma_finite M2 M1 ..
have *: "(\<lambda>(x,y). f (y,x)) = (\<lambda>x. f (case x of (x,y)\<Rightarrow>(y,x)))" by (auto simp: fun_eq_iff)
show ?thesis unfolding *
by (rule integrable_distr[OF measurable_pair_swap'])
@@ -2560,7 +2560,7 @@
fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
shows "integrable (M2 \<Otimes>\<^sub>M M1) (\<lambda>(x,y). f (y,x)) \<longleftrightarrow> integrable (M1 \<Otimes>\<^sub>M M2) f"
proof -
- interpret Q: pair_sigma_finite M2 M1 by default
+ interpret Q: pair_sigma_finite M2 M1 ..
from Q.integrable_product_swap[of "\<lambda>(x,y). f (y,x)"] integrable_product_swap[of f]
show ?thesis by auto
qed
@@ -2751,7 +2751,7 @@
and integrable_snd: "integrable M2 (\<lambda>y. \<integral>x. f x y \<partial>M1)" (is "?INT")
and integral_snd: "(\<integral>y. (\<integral>x. f x y \<partial>M1) \<partial>M2) = integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) (split f)" (is "?EQ")
proof -
- interpret Q: pair_sigma_finite M2 M1 by default
+ interpret Q: pair_sigma_finite M2 M1 ..
have Q_int: "integrable (M2 \<Otimes>\<^sub>M M1) (\<lambda>(x, y). f y x)"
using f unfolding integrable_product_swap_iff[symmetric] by simp
show ?AE using Q.AE_integrable_fst'[OF Q_int] by simp
@@ -2780,11 +2780,11 @@
and f: "integrable (Pi\<^sub>M (I \<union> J) M) f"
shows "integral\<^sup>L (Pi\<^sub>M (I \<union> J) M) f = (\<integral>x. (\<integral>y. f (merge I J (x, y)) \<partial>Pi\<^sub>M J M) \<partial>Pi\<^sub>M I M)"
proof -
- interpret I: finite_product_sigma_finite M I by default fact
- interpret J: finite_product_sigma_finite M J by default fact
+ interpret I: finite_product_sigma_finite M I by standard fact
+ interpret J: finite_product_sigma_finite M J by standard fact
have "finite (I \<union> J)" using fin by auto
- interpret IJ: finite_product_sigma_finite M "I \<union> J" by default fact
- interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" by default
+ interpret IJ: finite_product_sigma_finite M "I \<union> J" by standard fact
+ interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" ..
let ?M = "merge I J"
let ?f = "\<lambda>x. f (?M x)"
from f have f_borel: "f \<in> borel_measurable (Pi\<^sub>M (I \<union> J) M)"
@@ -2830,7 +2830,7 @@
assumes [simp]: "finite I" and integrable: "\<And>i. i \<in> I \<Longrightarrow> integrable (M i) (f i)"
shows "integrable (Pi\<^sub>M I M) (\<lambda>x. (\<Prod>i\<in>I. f i (x i)))" (is "integrable _ ?f")
proof (unfold integrable_iff_bounded, intro conjI)
- interpret finite_product_sigma_finite M I by default fact
+ interpret finite_product_sigma_finite M I by standard fact
show "?f \<in> borel_measurable (Pi\<^sub>M I M)"
using assms by simp
@@ -2859,7 +2859,7 @@
then have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow>
integrable (Pi\<^sub>M J M) (\<lambda>x. (\<Prod>i\<in>J. f i (x i)))"
by (intro product_integrable_setprod insert(4)) (auto intro: finite_subset)
- interpret I: finite_product_sigma_finite M I by default fact
+ interpret I: finite_product_sigma_finite M I by standard fact
have *: "\<And>x y. (\<Prod>j\<in>I. f j (if j = i then y else x j)) = (\<Prod>j\<in>I. f j (x j))"
using `i \<notin> I` by (auto intro!: setprod.cong)
show ?case