# HG changeset patch
# User hoelzl
# Date 1349863938 -7200
# Node ID 199d1d5bb17e65344fde047d1fd136ad8d7dc560
# Parent  970964690b3d795ef239e115398126b3761c8261
tuned product measurability

diff -r 970964690b3d -r 199d1d5bb17e src/HOL/Probability/Binary_Product_Measure.thy
--- a/src/HOL/Probability/Binary_Product_Measure.thy	Wed Oct 10 12:12:17 2012 +0200
+++ b/src/HOL/Probability/Binary_Product_Measure.thy	Wed Oct 10 12:12:18 2012 +0200
@@ -43,6 +43,10 @@
   unfolding pair_measure_def using space_closed[of A] space_closed[of B]
   by (intro sets_measure_of) auto
 
+lemma sets_pair_measure_cong[cong]:
+  "sets M1 = sets M1' \<Longrightarrow> sets M2 = sets M2' \<Longrightarrow> sets (M1 \<Otimes>\<^isub>M M2) = sets (M1' \<Otimes>\<^isub>M M2')"
+  unfolding sets_pair_measure by (simp cong: sets_eq_imp_space_eq)
+
 lemma pair_measureI[intro, simp]:
   "x \<in> sets A \<Longrightarrow> y \<in> sets B \<Longrightarrow> x \<times> y \<in> sets (A \<Otimes>\<^isub>M B)"
   by (auto simp: sets_pair_measure)
@@ -54,21 +58,30 @@
   unfolding pair_measure_def using 1 2
   by (intro measurable_measure_of) (auto dest: sets_into_space)
 
+lemma measurable_Pair:
+  assumes f: "f \<in> measurable M M1" and g: "g \<in> measurable M M2"
+  shows "(\<lambda>x. (f x, g x)) \<in> measurable M (M1 \<Otimes>\<^isub>M M2)"
+proof (rule measurable_pair_measureI)
+  show "(\<lambda>x. (f x, g x)) \<in> space M \<rightarrow> space M1 \<times> space M2"
+    using f g by (auto simp: measurable_def)
+  fix A B assume *: "A \<in> sets M1" "B \<in> sets M2"
+  have "(\<lambda>x. (f x, g x)) -` (A \<times> B) \<inter> space M = (f -` A \<inter> space M) \<inter> (g -` B \<inter> space M)"
+    by auto
+  also have "\<dots> \<in> sets M"
+    by (rule Int) (auto intro!: measurable_sets * f g)
+  finally show "(\<lambda>x. (f x, g x)) -` (A \<times> B) \<inter> space M \<in> sets M" .
+qed
+
+lemma measurable_pair:
+  assumes "(fst \<circ> f) \<in> measurable M M1" "(snd \<circ> f) \<in> measurable M M2"
+  shows "f \<in> measurable M (M1 \<Otimes>\<^isub>M M2)"
+  using measurable_Pair[OF assms] by simp
+
 lemma measurable_fst[intro!, simp]: "fst \<in> measurable (M1 \<Otimes>\<^isub>M M2) M1"
-  unfolding measurable_def
-proof safe
-  fix A assume A: "A \<in> sets M1"
-  from this[THEN sets_into_space] have "fst -` A \<inter> space M1 \<times> space M2 = A \<times> space M2" by auto
-  with A show "fst -` A \<inter> space (M1 \<Otimes>\<^isub>M M2) \<in> sets (M1 \<Otimes>\<^isub>M M2)" by (simp add: space_pair_measure)
-qed (simp add: space_pair_measure)
+  by (auto simp: fst_vimage_eq_Times space_pair_measure sets_into_space times_Int_times measurable_def)
 
 lemma measurable_snd[intro!, simp]: "snd \<in> measurable (M1 \<Otimes>\<^isub>M M2) M2"
-  unfolding measurable_def
-proof safe
-  fix A assume A: "A \<in> sets M2"
-  from this[THEN sets_into_space] have "snd -` A \<inter> space M1 \<times> space M2 = space M1 \<times> A" by auto
-  with A show "snd -` A \<inter> space (M1 \<Otimes>\<^isub>M M2) \<in> sets (M1 \<Otimes>\<^isub>M M2)" by (simp add: space_pair_measure)
-qed (simp add: space_pair_measure)
+  by (auto simp: snd_vimage_eq_Times space_pair_measure sets_into_space times_Int_times measurable_def)
 
 lemma measurable_fst': "f \<in> measurable M (N \<Otimes>\<^isub>M P) \<Longrightarrow> (\<lambda>x. fst (f x)) \<in> measurable M N"
   using measurable_comp[OF _ measurable_fst] by (auto simp: comp_def)
@@ -84,55 +97,29 @@
 
 lemma measurable_pair_iff:
   "f \<in> measurable M (M1 \<Otimes>\<^isub>M M2) \<longleftrightarrow> (fst \<circ> f) \<in> measurable M M1 \<and> (snd \<circ> f) \<in> measurable M M2"
-proof safe
-  assume f: "(fst \<circ> f) \<in> measurable M M1" and s: "(snd \<circ> f) \<in> measurable M M2"
-  show "f \<in> measurable M (M1 \<Otimes>\<^isub>M M2)"
-  proof (rule measurable_pair_measureI)
-    show "f \<in> space M \<rightarrow> space M1 \<times> space M2"
-      using f s by (auto simp: mem_Times_iff measurable_def comp_def)
-    fix A B assume "A \<in> sets M1" "B \<in> sets M2"
-    moreover have "(fst \<circ> f) -` A \<inter> space M \<in> sets M" "(snd \<circ> f) -` B \<inter> space M \<in> sets M"
-      using f `A \<in> sets M1` s `B \<in> sets M2` by (auto simp: measurable_sets)
-    moreover have "f -` (A \<times> B) \<inter> space M = ((fst \<circ> f) -` A \<inter> space M) \<inter> ((snd \<circ> f) -` B \<inter> space M)"
-      by (auto simp: vimage_Times)
-    ultimately show "f -` (A \<times> B) \<inter> space M \<in> sets M" by auto
-  qed
-qed auto
+  using measurable_pair[of f M M1 M2] by auto
 
-lemma measurable_pair:
-  "(fst \<circ> f) \<in> measurable M M1 \<Longrightarrow> (snd \<circ> f) \<in> measurable M M2 \<Longrightarrow> f \<in> measurable M (M1 \<Otimes>\<^isub>M M2)"
-  unfolding measurable_pair_iff by simp
+lemma measurable_split_conv:
+  "(\<lambda>(x, y). f x y) \<in> measurable A B \<longleftrightarrow> (\<lambda>x. f (fst x) (snd x)) \<in> measurable A B"
+  by (intro arg_cong2[where f="op \<in>"]) auto
 
 lemma measurable_pair_swap': "(\<lambda>(x,y). (y, x)) \<in> measurable (M1 \<Otimes>\<^isub>M M2) (M2 \<Otimes>\<^isub>M M1)"
-proof (rule measurable_pair_measureI)
-  fix A B assume "A \<in> sets M2" "B \<in> sets M1"
-  moreover then have "(\<lambda>(x, y). (y, x)) -` (A \<times> B) \<inter> space (M1 \<Otimes>\<^isub>M M2) = B \<times> A"
-    by (auto dest: sets_into_space simp: space_pair_measure)
-  ultimately show "(\<lambda>(x, y). (y, x)) -` (A \<times> B) \<inter> space (M1 \<Otimes>\<^isub>M M2) \<in> sets (M1 \<Otimes>\<^isub>M M2)"
-    by auto
-qed (auto simp add: space_pair_measure)
+  by (auto intro!: measurable_Pair simp: measurable_split_conv)
 
 lemma measurable_pair_swap:
   assumes f: "f \<in> measurable (M1 \<Otimes>\<^isub>M M2) M" shows "(\<lambda>(x,y). f (y, x)) \<in> measurable (M2 \<Otimes>\<^isub>M M1) M"
-proof -
-  have "(\<lambda>x. f (case x of (x, y) \<Rightarrow> (y, x))) = (\<lambda>(x, y). f (y, x))" by auto
-  then show ?thesis
-    using measurable_comp[OF measurable_pair_swap' f] by (simp add: comp_def)
-qed
+  using measurable_comp[OF measurable_Pair f] by (auto simp: measurable_split_conv comp_def)
 
 lemma measurable_pair_swap_iff:
   "f \<in> measurable (M2 \<Otimes>\<^isub>M M1) M \<longleftrightarrow> (\<lambda>(x,y). f (y,x)) \<in> measurable (M1 \<Otimes>\<^isub>M M2) M"
   using measurable_pair_swap[of "\<lambda>(x,y). f (y, x)"]
   by (auto intro!: measurable_pair_swap)
 
+lemma measurable_ident[intro, simp]: "(\<lambda>x. x) \<in> measurable M M"
+  unfolding measurable_def by auto
+
 lemma measurable_Pair1': "x \<in> space M1 \<Longrightarrow> Pair x \<in> measurable M2 (M1 \<Otimes>\<^isub>M M2)"
-proof (rule measurable_pair_measureI)
-  fix A B assume "A \<in> sets M1" "B \<in> sets M2"
-  moreover then have "Pair x -` (A \<times> B) \<inter> space M2 = (if x \<in> A then B else {})"
-    by (auto dest: sets_into_space simp: space_pair_measure)
-  ultimately show "Pair x -` (A \<times> B) \<inter> space M2 \<in> sets M2"
-    by auto
-qed (auto simp add: space_pair_measure)
+  by (auto intro!: measurable_Pair)
 
 lemma sets_Pair1: assumes A: "A \<in> sets (M1 \<Otimes>\<^isub>M M2)" shows "Pair x -` A \<in> sets M2"
 proof -
@@ -144,8 +131,7 @@
 qed
 
 lemma measurable_Pair2': "y \<in> space M2 \<Longrightarrow> (\<lambda>x. (x, y)) \<in> measurable M1 (M1 \<Otimes>\<^isub>M M2)"
-  using measurable_comp[OF measurable_Pair1' measurable_pair_swap', of y M2 M1]
-  by (simp add: comp_def)
+  by (auto intro!: measurable_Pair)
 
 lemma sets_Pair2: assumes A: "A \<in> sets (M1 \<Otimes>\<^isub>M M2)" shows "(\<lambda>x. (x, y)) -` A \<in> sets M1"
 proof -
@@ -172,46 +158,131 @@
   unfolding Int_stable_def
   by safe (auto simp add: times_Int_times)
 
-lemma finite_measure_cut_measurable:
-  assumes "sigma_finite_measure M1" "finite_measure M2"
-  assumes "Q \<in> sets (M1 \<Otimes>\<^isub>M M2)"
-  shows "(\<lambda>x. emeasure M2 (Pair x -` Q)) \<in> borel_measurable M1"
+lemma (in finite_measure) finite_measure_cut_measurable:
+  assumes "Q \<in> sets (N \<Otimes>\<^isub>M M)"
+  shows "(\<lambda>x. emeasure M (Pair x -` Q)) \<in> borel_measurable N"
     (is "?s Q \<in> _")
 proof -
-  interpret M1: sigma_finite_measure M1 by fact
-  interpret M2: finite_measure M2 by fact
-  let ?\<Omega> = "space M1 \<times> space M2" and ?D = "{A\<in>sets (M1 \<Otimes>\<^isub>M M2). ?s A \<in> borel_measurable M1}"
+  let ?\<Omega> = "space N \<times> space M" and ?D = "{A\<in>sets (N \<Otimes>\<^isub>M M). ?s A \<in> borel_measurable N}"
   note space_pair_measure[simp]
   interpret dynkin_system ?\<Omega> ?D
   proof (intro dynkin_systemI)
     fix A assume "A \<in> ?D" then show "A \<subseteq> ?\<Omega>"
-      using sets_into_space[of A "M1 \<Otimes>\<^isub>M M2"] by simp
+      using sets_into_space[of A "N \<Otimes>\<^isub>M M"] by simp
   next
     from top show "?\<Omega> \<in> ?D"
       by (auto simp add: if_distrib intro!: measurable_If)
   next
     fix A assume "A \<in> ?D"
-    with sets_into_space have "\<And>x. emeasure M2 (Pair x -` (?\<Omega> - A)) =
-        (if x \<in> space M1 then emeasure M2 (space M2) - ?s A x else 0)"
+    with sets_into_space have "\<And>x. emeasure M (Pair x -` (?\<Omega> - A)) =
+        (if x \<in> space N then emeasure M (space M) - ?s A x else 0)"
       by (auto intro!: emeasure_compl simp: vimage_Diff sets_Pair1)
     with `A \<in> ?D` top show "?\<Omega> - A \<in> ?D"
       by (auto intro!: measurable_If)
   next
-    fix F :: "nat \<Rightarrow> ('a\<times>'b) set" assume "disjoint_family F" "range F \<subseteq> ?D"
-    moreover then have "\<And>x. emeasure M2 (\<Union>i. Pair x -` F i) = (\<Sum>i. ?s (F i) x)"
+    fix F :: "nat \<Rightarrow> ('b\<times>'a) set" assume "disjoint_family F" "range F \<subseteq> ?D"
+    moreover then have "\<And>x. emeasure M (\<Union>i. Pair x -` F i) = (\<Sum>i. ?s (F i) x)"
       by (intro suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def sets_Pair1)
     ultimately show "(\<Union>i. F i) \<in> ?D"
       by (auto simp: vimage_UN intro!: borel_measurable_psuminf)
   qed
-  let ?G = "{a \<times> b | a b. a \<in> sets M1 \<and> b \<in> sets M2}"
+  let ?G = "{a \<times> b | a b. a \<in> sets N \<and> b \<in> sets M}"
   have "sigma_sets ?\<Omega> ?G = ?D"
   proof (rule dynkin_lemma)
     show "?G \<subseteq> ?D"
       by (auto simp: if_distrib Int_def[symmetric] intro!: measurable_If)
   qed (auto simp: sets_pair_measure  Int_stable_pair_measure_generator)
-  with `Q \<in> sets (M1 \<Otimes>\<^isub>M M2)` have "Q \<in> ?D"
+  with `Q \<in> sets (N \<Otimes>\<^isub>M M)` have "Q \<in> ?D"
     by (simp add: sets_pair_measure[symmetric])
-  then show "?s Q \<in> borel_measurable M1" by simp
+  then show "?s Q \<in> borel_measurable N" by simp
+qed
+
+lemma (in sigma_finite_measure) measurable_emeasure_Pair:
+  assumes Q: "Q \<in> sets (N \<Otimes>\<^isub>M M)" shows "(\<lambda>x. emeasure M (Pair x -` Q)) \<in> borel_measurable N" (is "?s Q \<in> _")
+proof -
+  from sigma_finite_disjoint guess F . note F = this
+  then have F_sets: "\<And>i. F i \<in> sets M" by auto
+  let ?C = "\<lambda>x i. F i \<inter> Pair x -` Q"
+  { fix i
+    have [simp]: "space N \<times> F i \<inter> space N \<times> space M = space N \<times> F i"
+      using F sets_into_space by auto
+    let ?R = "density M (indicator (F i))"
+    have "finite_measure ?R"
+      using F by (intro finite_measureI) (auto simp: emeasure_restricted subset_eq)
+    then have "(\<lambda>x. emeasure ?R (Pair x -` (space N \<times> space ?R \<inter> Q))) \<in> borel_measurable N"
+     by (rule finite_measure.finite_measure_cut_measurable) (auto intro: Q)
+    moreover have "\<And>x. emeasure ?R (Pair x -` (space N \<times> space ?R \<inter> Q))
+        = emeasure M (F i \<inter> Pair x -` (space N \<times> space ?R \<inter> Q))"
+      using Q F_sets by (intro emeasure_restricted) (auto intro: sets_Pair1)
+    moreover have "\<And>x. F i \<inter> Pair x -` (space N \<times> space ?R \<inter> Q) = ?C x i"
+      using sets_into_space[OF Q] by (auto simp: space_pair_measure)
+    ultimately have "(\<lambda>x. emeasure M (?C x i)) \<in> borel_measurable N"
+      by simp }
+  moreover
+  { fix x
+    have "(\<Sum>i. emeasure M (?C x i)) = emeasure M (\<Union>i. ?C x i)"
+    proof (intro suminf_emeasure)
+      show "range (?C x) \<subseteq> sets M"
+        using F `Q \<in> sets (N \<Otimes>\<^isub>M M)` by (auto intro!: sets_Pair1)
+      have "disjoint_family F" using F by auto
+      show "disjoint_family (?C x)"
+        by (rule disjoint_family_on_bisimulation[OF `disjoint_family F`]) auto
+    qed
+    also have "(\<Union>i. ?C x i) = Pair x -` Q"
+      using F sets_into_space[OF `Q \<in> sets (N \<Otimes>\<^isub>M M)`]
+      by (auto simp: space_pair_measure)
+    finally have "emeasure M (Pair x -` Q) = (\<Sum>i. emeasure M (?C x i))"
+      by simp }
+  ultimately show ?thesis using `Q \<in> sets (N \<Otimes>\<^isub>M M)` F_sets
+    by auto
+qed
+
+lemma (in sigma_finite_measure) emeasure_pair_measure:
+  assumes "X \<in> sets (N \<Otimes>\<^isub>M M)"
+  shows "emeasure (N \<Otimes>\<^isub>M M) X = (\<integral>\<^isup>+ x. \<integral>\<^isup>+ y. indicator X (x, y) \<partial>M \<partial>N)" (is "_ = ?\<mu> X")
+proof (rule emeasure_measure_of[OF pair_measure_def])
+  show "positive (sets (N \<Otimes>\<^isub>M M)) ?\<mu>"
+    by (auto simp: positive_def positive_integral_positive)
+  have eq[simp]: "\<And>A x y. indicator A (x, y) = indicator (Pair x -` A) y"
+    by (auto simp: indicator_def)
+  show "countably_additive (sets (N \<Otimes>\<^isub>M M)) ?\<mu>"
+  proof (rule countably_additiveI)
+    fix F :: "nat \<Rightarrow> ('b \<times> 'a) set" assume F: "range F \<subseteq> sets (N \<Otimes>\<^isub>M M)" "disjoint_family F"
+    from F have *: "\<And>i. F i \<in> sets (N \<Otimes>\<^isub>M M)" "(\<Union>i. F i) \<in> sets (N \<Otimes>\<^isub>M M)" by auto
+    moreover from F have "\<And>i. (\<lambda>x. emeasure M (Pair x -` F i)) \<in> borel_measurable N"
+      by (intro measurable_emeasure_Pair) auto
+    moreover have "\<And>x. disjoint_family (\<lambda>i. Pair x -` F i)"
+      by (intro disjoint_family_on_bisimulation[OF F(2)]) auto
+    moreover have "\<And>x. range (\<lambda>i. Pair x -` F i) \<subseteq> sets M"
+      using F by (auto simp: sets_Pair1)
+    ultimately show "(\<Sum>n. ?\<mu> (F n)) = ?\<mu> (\<Union>i. F i)"
+      by (auto simp add: vimage_UN positive_integral_suminf[symmetric] suminf_emeasure subset_eq emeasure_nonneg sets_Pair1
+               intro!: positive_integral_cong positive_integral_indicator[symmetric])
+  qed
+  show "{a \<times> b |a b. a \<in> sets N \<and> b \<in> sets M} \<subseteq> Pow (space N \<times> space M)"
+    using space_closed[of N] space_closed[of M] by auto
+qed fact
+
+lemma (in sigma_finite_measure) emeasure_pair_measure_alt:
+  assumes X: "X \<in> sets (N \<Otimes>\<^isub>M M)"
+  shows "emeasure (N  \<Otimes>\<^isub>M M) X = (\<integral>\<^isup>+x. emeasure M (Pair x -` X) \<partial>N)"
+proof -
+  have [simp]: "\<And>x y. indicator X (x, y) = indicator (Pair x -` X) y"
+    by (auto simp: indicator_def)
+  show ?thesis
+    using X by (auto intro!: positive_integral_cong simp: emeasure_pair_measure sets_Pair1)
+qed
+
+lemma (in sigma_finite_measure) emeasure_pair_measure_Times:
+  assumes A: "A \<in> sets N" and B: "B \<in> sets M"
+  shows "emeasure (N \<Otimes>\<^isub>M M) (A \<times> B) = emeasure N A * emeasure M B"
+proof -
+  have "emeasure (N \<Otimes>\<^isub>M M) (A \<times> B) = (\<integral>\<^isup>+x. emeasure M B * indicator A x \<partial>N)"
+    using A B by (auto intro!: positive_integral_cong simp: emeasure_pair_measure_alt)
+  also have "\<dots> = emeasure M B * emeasure N A"
+    using A by (simp add: emeasure_nonneg positive_integral_cmult_indicator)
+  finally show ?thesis
+    by (simp add: ac_simps)
 qed
 
 subsection {* Binary products of $\sigma$-finite emeasure spaces *}
@@ -219,114 +290,21 @@
 locale pair_sigma_finite = M1: sigma_finite_measure M1 + M2: sigma_finite_measure M2
   for M1 :: "'a measure" and M2 :: "'b measure"
 
-lemma sets_pair_measure_cong[cong]:
-  "sets M1 = sets M1' \<Longrightarrow> sets M2 = sets M2' \<Longrightarrow> sets (M1 \<Otimes>\<^isub>M M2) = sets (M1' \<Otimes>\<^isub>M M2')"
-  unfolding sets_pair_measure by (simp cong: sets_eq_imp_space_eq)
-
 lemma (in pair_sigma_finite) measurable_emeasure_Pair1:
-  assumes Q: "Q \<in> sets (M1 \<Otimes>\<^isub>M M2)" shows "(\<lambda>x. emeasure M2 (Pair x -` Q)) \<in> borel_measurable M1" (is "?s Q \<in> _")
-proof -
-  from M2.sigma_finite_disjoint guess F . note F = this
-  then have F_sets: "\<And>i. F i \<in> sets M2" by auto
-  have M1: "sigma_finite_measure M1" ..
-  let ?C = "\<lambda>x i. F i \<inter> Pair x -` Q"
-  { fix i
-    have [simp]: "space M1 \<times> F i \<inter> space M1 \<times> space M2 = space M1 \<times> F i"
-      using F sets_into_space by auto
-    let ?R = "density M2 (indicator (F i))"
-    have "(\<lambda>x. emeasure ?R (Pair x -` (space M1 \<times> space ?R \<inter> Q))) \<in> borel_measurable M1"
-    proof (intro finite_measure_cut_measurable[OF M1])
-      show "finite_measure ?R"
-        using F by (intro finite_measureI) (auto simp: emeasure_restricted subset_eq)
-      show "(space M1 \<times> space ?R) \<inter> Q \<in> sets (M1 \<Otimes>\<^isub>M ?R)"
-        using Q by (simp add: Int)
-    qed
-    moreover have "\<And>x. emeasure ?R (Pair x -` (space M1 \<times> space ?R \<inter> Q))
-        = emeasure M2 (F i \<inter> Pair x -` (space M1 \<times> space ?R \<inter> Q))"
-      using Q F_sets by (intro emeasure_restricted) (auto intro: sets_Pair1)
-    moreover have "\<And>x. F i \<inter> Pair x -` (space M1 \<times> space ?R \<inter> Q) = ?C x i"
-      using sets_into_space[OF Q] by (auto simp: space_pair_measure)
-    ultimately have "(\<lambda>x. emeasure M2 (?C x i)) \<in> borel_measurable M1"
-      by simp }
-  moreover
-  { fix x
-    have "(\<Sum>i. emeasure M2 (?C x i)) = emeasure M2 (\<Union>i. ?C x i)"
-    proof (intro suminf_emeasure)
-      show "range (?C x) \<subseteq> sets M2"
-        using F `Q \<in> sets (M1 \<Otimes>\<^isub>M M2)` by (auto intro!: sets_Pair1)
-      have "disjoint_family F" using F by auto
-      show "disjoint_family (?C x)"
-        by (rule disjoint_family_on_bisimulation[OF `disjoint_family F`]) auto
-    qed
-    also have "(\<Union>i. ?C x i) = Pair x -` Q"
-      using F sets_into_space[OF `Q \<in> sets (M1 \<Otimes>\<^isub>M M2)`]
-      by (auto simp: space_pair_measure)
-    finally have "emeasure M2 (Pair x -` Q) = (\<Sum>i. emeasure M2 (?C x i))"
-      by simp }
-  ultimately show ?thesis using `Q \<in> sets (M1 \<Otimes>\<^isub>M M2)` F_sets
-    by auto
-qed
+  "Q \<in> sets (M1 \<Otimes>\<^isub>M M2) \<Longrightarrow> (\<lambda>x. emeasure M2 (Pair x -` Q)) \<in> borel_measurable M1"
+  using M2.measurable_emeasure_Pair .
 
 lemma (in pair_sigma_finite) measurable_emeasure_Pair2:
   assumes Q: "Q \<in> sets (M1 \<Otimes>\<^isub>M M2)" shows "(\<lambda>y. emeasure M1 ((\<lambda>x. (x, y)) -` Q)) \<in> borel_measurable M2"
 proof -
-  interpret Q: pair_sigma_finite M2 M1 by default
   have "(\<lambda>(x, y). (y, x)) -` Q \<inter> space (M2 \<Otimes>\<^isub>M M1) \<in> sets (M2 \<Otimes>\<^isub>M M1)"
     using Q measurable_pair_swap' by (auto intro: measurable_sets)
-  note Q.measurable_emeasure_Pair1[OF this]
+  note M1.measurable_emeasure_Pair[OF this]
   moreover have "\<And>y. Pair y -` ((\<lambda>(x, y). (y, x)) -` Q \<inter> space (M2 \<Otimes>\<^isub>M M1)) = (\<lambda>x. (x, y)) -` Q"
     using Q[THEN sets_into_space] by (auto simp: space_pair_measure)
   ultimately show ?thesis by simp
 qed
 
-lemma (in pair_sigma_finite) emeasure_pair_measure:
-  assumes "X \<in> sets (M1 \<Otimes>\<^isub>M M2)"
-  shows "emeasure (M1 \<Otimes>\<^isub>M M2) X = (\<integral>\<^isup>+ x. \<integral>\<^isup>+ y. indicator X (x, y) \<partial>M2 \<partial>M1)" (is "_ = ?\<mu> X")
-proof (rule emeasure_measure_of[OF pair_measure_def])
-  show "positive (sets (M1 \<Otimes>\<^isub>M M2)) ?\<mu>"
-    by (auto simp: positive_def positive_integral_positive)
-  have eq[simp]: "\<And>A x y. indicator A (x, y) = indicator (Pair x -` A) y"
-    by (auto simp: indicator_def)
-  show "countably_additive (sets (M1 \<Otimes>\<^isub>M M2)) ?\<mu>"
-  proof (rule countably_additiveI)
-    fix F :: "nat \<Rightarrow> ('a \<times> 'b) set" assume F: "range F \<subseteq> sets (M1 \<Otimes>\<^isub>M M2)" "disjoint_family F"
-    from F have *: "\<And>i. F i \<in> sets (M1 \<Otimes>\<^isub>M M2)" "(\<Union>i. F i) \<in> sets (M1 \<Otimes>\<^isub>M M2)" by auto
-    moreover from F have "\<And>i. (\<lambda>x. emeasure M2 (Pair x -` F i)) \<in> borel_measurable M1"
-      by (intro measurable_emeasure_Pair1) auto
-    moreover have "\<And>x. disjoint_family (\<lambda>i. Pair x -` F i)"
-      by (intro disjoint_family_on_bisimulation[OF F(2)]) auto
-    moreover have "\<And>x. range (\<lambda>i. Pair x -` F i) \<subseteq> sets M2"
-      using F by (auto simp: sets_Pair1)
-    ultimately show "(\<Sum>n. ?\<mu> (F n)) = ?\<mu> (\<Union>i. F i)"
-      by (auto simp add: vimage_UN positive_integral_suminf[symmetric] suminf_emeasure subset_eq emeasure_nonneg sets_Pair1
-               intro!: positive_integral_cong positive_integral_indicator[symmetric])
-  qed
-  show "{a \<times> b |a b. a \<in> sets M1 \<and> b \<in> sets M2} \<subseteq> Pow (space M1 \<times> space M2)"
-    using space_closed[of M1] space_closed[of M2] by auto
-qed fact
-
-lemma (in pair_sigma_finite) emeasure_pair_measure_alt:
-  assumes X: "X \<in> sets (M1 \<Otimes>\<^isub>M M2)"
-  shows "emeasure (M1  \<Otimes>\<^isub>M M2) X = (\<integral>\<^isup>+x. emeasure M2 (Pair x -` X) \<partial>M1)"
-proof -
-  have [simp]: "\<And>x y. indicator X (x, y) = indicator (Pair x -` X) y"
-    by (auto simp: indicator_def)
-  show ?thesis
-    using X by (auto intro!: positive_integral_cong simp: emeasure_pair_measure sets_Pair1)
-qed
-
-lemma (in pair_sigma_finite) emeasure_pair_measure_Times:
-  assumes A: "A \<in> sets M1" and B: "B \<in> sets M2"
-  shows "emeasure (M1 \<Otimes>\<^isub>M M2) (A \<times> B) = emeasure M1 A * emeasure M2 B"
-proof -
-  have "emeasure (M1 \<Otimes>\<^isub>M M2) (A \<times> B) = (\<integral>\<^isup>+x. emeasure M2 B * indicator A x \<partial>M1)"
-    using A B by (auto intro!: positive_integral_cong simp: emeasure_pair_measure_alt)
-  also have "\<dots> = emeasure M2 B * emeasure M1 A"
-    using A by (simp add: emeasure_nonneg positive_integral_cmult_indicator)
-  finally show ?thesis
-    by (simp add: ac_simps)
-qed
-
 lemma (in pair_sigma_finite) sigma_finite_up_in_pair_measure_generator:
   defines "E \<equiv> {A \<times> B | A B. A \<in> sets M1 \<and> B \<in> sets M2}"
   shows "\<exists>F::nat \<Rightarrow> ('a \<times> 'b) set. range F \<subseteq> E \<and> incseq F \<and> (\<Union>i. F i) = space M1 \<times> space M2 \<and>
@@ -396,7 +374,6 @@
 lemma (in pair_sigma_finite) distr_pair_swap:
   "M1 \<Otimes>\<^isub>M M2 = distr (M2 \<Otimes>\<^isub>M M1) (M1 \<Otimes>\<^isub>M M2) (\<lambda>(x, y). (y, x))" (is "?P = ?D")
 proof -
-  interpret Q: pair_sigma_finite M2 M1 by default
   from sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('a \<times> 'b) set" .. note F = this
   let ?E = "{a \<times> b |a b. a \<in> sets M1 \<and> b \<in> sets M2}"
   show ?thesis
@@ -416,7 +393,7 @@
     have "(\<lambda>(y, x). (x, y)) -` X \<inter> space (M2 \<Otimes>\<^isub>M M1) = B \<times> A"
       using sets_into_space[OF A] sets_into_space[OF B] by (auto simp: space_pair_measure)
     with A B show "emeasure (M1 \<Otimes>\<^isub>M M2) X = emeasure ?D X"
-      by (simp add: emeasure_pair_measure_Times Q.emeasure_pair_measure_Times emeasure_distr
+      by (simp add: M2.emeasure_pair_measure_Times M1.emeasure_pair_measure_Times emeasure_distr
                     measurable_pair_swap' ac_simps)
   qed
 qed
@@ -426,13 +403,84 @@
   shows "emeasure (M1 \<Otimes>\<^isub>M M2) A = (\<integral>\<^isup>+y. emeasure M1 ((\<lambda>x. (x, y)) -` A) \<partial>M2)"
     (is "_ = ?\<nu> A")
 proof -
-  interpret Q: pair_sigma_finite M2 M1 by default
   have [simp]: "\<And>y. (Pair y -` ((\<lambda>(x, y). (y, x)) -` A \<inter> space (M2 \<Otimes>\<^isub>M M1))) = (\<lambda>x. (x, y)) -` A"
     using sets_into_space[OF A] by (auto simp: space_pair_measure)
   show ?thesis using A
     by (subst distr_pair_swap)
        (simp_all del: vimage_Int add: measurable_sets[OF measurable_pair_swap']
-                 Q.emeasure_pair_measure_alt emeasure_distr[OF measurable_pair_swap' A])
+                 M1.emeasure_pair_measure_alt emeasure_distr[OF measurable_pair_swap' A])
+qed
+
+lemma (in pair_sigma_finite) AE_pair:
+  assumes "AE x in (M1 \<Otimes>\<^isub>M M2). Q x"
+  shows "AE x in M1. (AE y in M2. Q (x, y))"
+proof -
+  obtain N where N: "N \<in> sets (M1 \<Otimes>\<^isub>M M2)" "emeasure (M1 \<Otimes>\<^isub>M M2) N = 0" "{x\<in>space (M1 \<Otimes>\<^isub>M M2). \<not> Q x} \<subseteq> N"
+    using assms unfolding eventually_ae_filter by auto
+  show ?thesis
+  proof (rule AE_I)
+    from N measurable_emeasure_Pair1[OF `N \<in> sets (M1 \<Otimes>\<^isub>M M2)`]
+    show "emeasure M1 {x\<in>space M1. emeasure M2 (Pair x -` N) \<noteq> 0} = 0"
+      by (auto simp: M2.emeasure_pair_measure_alt positive_integral_0_iff emeasure_nonneg)
+    show "{x \<in> space M1. emeasure M2 (Pair x -` N) \<noteq> 0} \<in> sets M1"
+      by (intro borel_measurable_ereal_neq_const measurable_emeasure_Pair1 N)
+    { fix x assume "x \<in> space M1" "emeasure M2 (Pair x -` N) = 0"
+      have "AE y in M2. Q (x, y)"
+      proof (rule AE_I)
+        show "emeasure M2 (Pair x -` N) = 0" by fact
+        show "Pair x -` N \<in> sets M2" using N(1) by (rule sets_Pair1)
+        show "{y \<in> space M2. \<not> Q (x, y)} \<subseteq> Pair x -` N"
+          using N `x \<in> space M1` unfolding space_pair_measure by auto
+      qed }
+    then show "{x \<in> space M1. \<not> (AE y in M2. Q (x, y))} \<subseteq> {x \<in> space M1. emeasure M2 (Pair x -` N) \<noteq> 0}"
+      by auto
+  qed
+qed
+
+lemma (in pair_sigma_finite) AE_pair_measure:
+  assumes "{x\<in>space (M1 \<Otimes>\<^isub>M M2). P x} \<in> sets (M1 \<Otimes>\<^isub>M M2)"
+  assumes ae: "AE x in M1. AE y in M2. P (x, y)"
+  shows "AE x in M1 \<Otimes>\<^isub>M M2. P x"
+proof (subst AE_iff_measurable[OF _ refl])
+  show "{x\<in>space (M1 \<Otimes>\<^isub>M M2). \<not> P x} \<in> sets (M1 \<Otimes>\<^isub>M M2)"
+    by (rule sets_Collect) fact
+  then have "emeasure (M1 \<Otimes>\<^isub>M M2) {x \<in> space (M1 \<Otimes>\<^isub>M M2). \<not> P x} =
+      (\<integral>\<^isup>+ x. \<integral>\<^isup>+ y. indicator {x \<in> space (M1 \<Otimes>\<^isub>M M2). \<not> P x} (x, y) \<partial>M2 \<partial>M1)"
+    by (simp add: M2.emeasure_pair_measure)
+  also have "\<dots> = (\<integral>\<^isup>+ x. \<integral>\<^isup>+ y. 0 \<partial>M2 \<partial>M1)"
+    using ae
+    apply (safe intro!: positive_integral_cong_AE)
+    apply (intro AE_I2)
+    apply (safe intro!: positive_integral_cong_AE)
+    apply auto
+    done
+  finally show "emeasure (M1 \<Otimes>\<^isub>M M2) {x \<in> space (M1 \<Otimes>\<^isub>M M2). \<not> P x} = 0" by simp
+qed
+
+lemma (in pair_sigma_finite) AE_pair_iff:
+  "{x\<in>space (M1 \<Otimes>\<^isub>M M2). P (fst x) (snd x)} \<in> sets (M1 \<Otimes>\<^isub>M M2) \<Longrightarrow>
+    (AE x in M1. AE y in M2. P x y) \<longleftrightarrow> (AE x in (M1 \<Otimes>\<^isub>M M2). P (fst x) (snd x))"
+  using AE_pair[of "\<lambda>x. P (fst x) (snd x)"] AE_pair_measure[of "\<lambda>x. P (fst x) (snd x)"] by auto
+
+lemma (in pair_sigma_finite) AE_commute:
+  assumes P: "{x\<in>space (M1 \<Otimes>\<^isub>M M2). P (fst x) (snd x)} \<in> sets (M1 \<Otimes>\<^isub>M M2)"
+  shows "(AE x in M1. AE y in M2. P x y) \<longleftrightarrow> (AE y in M2. AE x in M1. P x y)"
+proof -
+  interpret Q: pair_sigma_finite M2 M1 ..
+  have [simp]: "\<And>x. (fst (case x of (x, y) \<Rightarrow> (y, x))) = snd x" "\<And>x. (snd (case x of (x, y) \<Rightarrow> (y, x))) = fst x"
+    by auto
+  have "{x \<in> space (M2 \<Otimes>\<^isub>M M1). P (snd x) (fst x)} =
+    (\<lambda>(x, y). (y, x)) -` {x \<in> space (M1 \<Otimes>\<^isub>M M2). P (fst x) (snd x)} \<inter> space (M2 \<Otimes>\<^isub>M M1)"
+    by (auto simp: space_pair_measure)
+  also have "\<dots> \<in> sets (M2 \<Otimes>\<^isub>M M1)"
+    by (intro sets_pair_swap P)
+  finally show ?thesis
+    apply (subst AE_pair_iff[OF P])
+    apply (subst distr_pair_swap)
+    apply (subst AE_distr_iff[OF measurable_pair_swap' P])
+    apply (subst Q.AE_pair_iff)
+    apply simp_all
+    done
 qed
 
 section "Fubinis theorem"
@@ -494,7 +542,7 @@
                        positive_integral_cmult
                        positive_integral_cong[OF eq]
                        positive_integral_eq_simple_integral[OF f]
-                       emeasure_pair_measure_alt[symmetric])
+                       M2.emeasure_pair_measure_alt[symmetric])
 qed
 
 lemma (in pair_sigma_finite) positive_integral_fst_measurable:
@@ -558,96 +606,6 @@
   unfolding positive_integral_snd_measurable[OF assms]
   unfolding positive_integral_fst_measurable[OF assms] ..
 
-lemma (in pair_sigma_finite) AE_pair:
-  assumes "AE x in (M1 \<Otimes>\<^isub>M M2). Q x"
-  shows "AE x in M1. (AE y in M2. Q (x, y))"
-proof -
-  obtain N where N: "N \<in> sets (M1 \<Otimes>\<^isub>M M2)" "emeasure (M1 \<Otimes>\<^isub>M M2) N = 0" "{x\<in>space (M1 \<Otimes>\<^isub>M M2). \<not> Q x} \<subseteq> N"
-    using assms unfolding eventually_ae_filter by auto
-  show ?thesis
-  proof (rule AE_I)
-    from N measurable_emeasure_Pair1[OF `N \<in> sets (M1 \<Otimes>\<^isub>M M2)`]
-    show "emeasure M1 {x\<in>space M1. emeasure M2 (Pair x -` N) \<noteq> 0} = 0"
-      by (auto simp: emeasure_pair_measure_alt positive_integral_0_iff emeasure_nonneg)
-    show "{x \<in> space M1. emeasure M2 (Pair x -` N) \<noteq> 0} \<in> sets M1"
-      by (intro borel_measurable_ereal_neq_const measurable_emeasure_Pair1 N)
-    { fix x assume "x \<in> space M1" "emeasure M2 (Pair x -` N) = 0"
-      have "AE y in M2. Q (x, y)"
-      proof (rule AE_I)
-        show "emeasure M2 (Pair x -` N) = 0" by fact
-        show "Pair x -` N \<in> sets M2" using N(1) by (rule sets_Pair1)
-        show "{y \<in> space M2. \<not> Q (x, y)} \<subseteq> Pair x -` N"
-          using N `x \<in> space M1` unfolding space_pair_measure by auto
-      qed }
-    then show "{x \<in> space M1. \<not> (AE y in M2. Q (x, y))} \<subseteq> {x \<in> space M1. emeasure M2 (Pair x -` N) \<noteq> 0}"
-      by auto
-  qed
-qed
-
-lemma (in pair_sigma_finite) AE_pair_measure:
-  assumes "{x\<in>space (M1 \<Otimes>\<^isub>M M2). P x} \<in> sets (M1 \<Otimes>\<^isub>M M2)"
-  assumes ae: "AE x in M1. AE y in M2. P (x, y)"
-  shows "AE x in M1 \<Otimes>\<^isub>M M2. P x"
-proof (subst AE_iff_measurable[OF _ refl])
-  show "{x\<in>space (M1 \<Otimes>\<^isub>M M2). \<not> P x} \<in> sets (M1 \<Otimes>\<^isub>M M2)"
-    by (rule sets_Collect) fact
-  then have "emeasure (M1 \<Otimes>\<^isub>M M2) {x \<in> space (M1 \<Otimes>\<^isub>M M2). \<not> P x} =
-      (\<integral>\<^isup>+ x. \<integral>\<^isup>+ y. indicator {x \<in> space (M1 \<Otimes>\<^isub>M M2). \<not> P x} (x, y) \<partial>M2 \<partial>M1)"
-    by (simp add: emeasure_pair_measure)
-  also have "\<dots> = (\<integral>\<^isup>+ x. \<integral>\<^isup>+ y. 0 \<partial>M2 \<partial>M1)"
-    using ae
-    apply (safe intro!: positive_integral_cong_AE)
-    apply (intro AE_I2)
-    apply (safe intro!: positive_integral_cong_AE)
-    apply auto
-    done
-  finally show "emeasure (M1 \<Otimes>\<^isub>M M2) {x \<in> space (M1 \<Otimes>\<^isub>M M2). \<not> P x} = 0" by simp
-qed
-
-lemma (in pair_sigma_finite) AE_pair_iff:
-  "{x\<in>space (M1 \<Otimes>\<^isub>M M2). P (fst x) (snd x)} \<in> sets (M1 \<Otimes>\<^isub>M M2) \<Longrightarrow>
-    (AE x in M1. AE y in M2. P x y) \<longleftrightarrow> (AE x in (M1 \<Otimes>\<^isub>M M2). P (fst x) (snd x))"
-  using AE_pair[of "\<lambda>x. P (fst x) (snd x)"] AE_pair_measure[of "\<lambda>x. P (fst x) (snd x)"] by auto
-
-lemma AE_distr_iff:
-  assumes f: "f \<in> measurable M N" and P: "{x \<in> space N. P x} \<in> sets N"
-  shows "(AE x in distr M N f. P x) \<longleftrightarrow> (AE x in M. P (f x))"
-proof (subst (1 2) AE_iff_measurable[OF _ refl])
-  from P show "{x \<in> space (distr M N f). \<not> P x} \<in> sets (distr M N f)"
-    by (auto intro!: sets_Collect_neg)
-  moreover
-  have "f -` {x \<in> space N. P x} \<inter> space M = {x \<in> space M. P (f x)}"
-    using f by (auto dest: measurable_space)
-  then show "{x \<in> space M. \<not> P (f x)} \<in> sets M"
-    using measurable_sets[OF f P] by (auto intro!: sets_Collect_neg)
-  moreover have "f -` {x\<in>space N. \<not> P x} \<inter> space M = {x \<in> space M. \<not> P (f x)}"
-    using f by (auto dest: measurable_space)
-  ultimately show "(emeasure (distr M N f) {x \<in> space (distr M N f). \<not> P x} = 0) =
-    (emeasure M {x \<in> space M. \<not> P (f x)} = 0)"
-    using f by (simp add: emeasure_distr)
-qed
-
-lemma (in pair_sigma_finite) AE_commute:
-  assumes P: "{x\<in>space (M1 \<Otimes>\<^isub>M M2). P (fst x) (snd x)} \<in> sets (M1 \<Otimes>\<^isub>M M2)"
-  shows "(AE x in M1. AE y in M2. P x y) \<longleftrightarrow> (AE y in M2. AE x in M1. P x y)"
-proof -
-  interpret Q: pair_sigma_finite M2 M1 ..
-  have [simp]: "\<And>x. (fst (case x of (x, y) \<Rightarrow> (y, x))) = snd x" "\<And>x. (snd (case x of (x, y) \<Rightarrow> (y, x))) = fst x"
-    by auto
-  have "{x \<in> space (M2 \<Otimes>\<^isub>M M1). P (snd x) (fst x)} =
-    (\<lambda>(x, y). (y, x)) -` {x \<in> space (M1 \<Otimes>\<^isub>M M2). P (fst x) (snd x)} \<inter> space (M2 \<Otimes>\<^isub>M M1)"
-    by (auto simp: space_pair_measure)
-  also have "\<dots> \<in> sets (M2 \<Otimes>\<^isub>M M1)"
-    by (intro sets_pair_swap P)
-  finally show ?thesis
-    apply (subst AE_pair_iff[OF P])
-    apply (subst distr_pair_swap)
-    apply (subst AE_distr_iff[OF measurable_pair_swap' P])
-    apply (subst Q.AE_pair_iff)
-    apply simp_all
-    done
-qed
-
 lemma (in pair_sigma_finite) integrable_product_swap:
   assumes "integrable (M1 \<Otimes>\<^isub>M M2) f"
   shows "integrable (M2 \<Otimes>\<^isub>M M1) (\<lambda>(x,y). f (y,x))"
@@ -817,7 +775,7 @@
     by (intro finite_subset[OF _ B]) auto
   have fin_X: "finite X" using X_subset by (rule finite_subset) (auto simp: A B)
   show "emeasure ?P X = emeasure ?C X"
-    apply (subst P.emeasure_pair_measure_alt[OF X])
+    apply (subst B.emeasure_pair_measure_alt[OF X])
     apply (subst emeasure_count_space)
     using X_subset apply auto []
     apply (simp add: fin_Pair emeasure_count_space X_subset fin_X)
@@ -861,7 +819,7 @@
     by simp
 
   show "emeasure ?L A = emeasure ?R A"
-    apply (subst L.emeasure_pair_measure[OF A])
+    apply (subst D2.emeasure_pair_measure[OF A])
     apply (subst emeasure_density)
         using f_fst g_snd apply (simp add: split_beta')
       using A apply simp
@@ -924,7 +882,7 @@
     by (auto simp: measurable_pair_iff)
   fix A assume A: "A \<in> sets ?P"
   then have "emeasure ?P A = (\<integral>\<^isup>+x. emeasure (distr N T g) (Pair x -` A) \<partial>distr M S f)"
-    by (rule ST.emeasure_pair_measure_alt)
+    by (rule T.emeasure_pair_measure_alt)
   also have "\<dots> = (\<integral>\<^isup>+x. emeasure N (g -` (Pair x -` A) \<inter> space N) \<partial>distr M S f)"
     using g A by (simp add: sets_Pair1 emeasure_distr)
   also have "\<dots> = (\<integral>\<^isup>+x. emeasure N (g -` (Pair (f x) -` A) \<inter> space N) \<partial>M)"
@@ -933,7 +891,7 @@
   also have "\<dots> = (\<integral>\<^isup>+x. emeasure N (Pair x -` ((\<lambda>(x, y). (f x, g y)) -` A \<inter> space (M \<Otimes>\<^isub>M N))) \<partial>M)"
     by (intro positive_integral_cong arg_cong2[where f=emeasure]) (auto simp: space_pair_measure)
   also have "\<dots> = emeasure (M \<Otimes>\<^isub>M N) ((\<lambda>(x, y). (f x, g y)) -` A \<inter> space (M \<Otimes>\<^isub>M N))"
-    using fg by (intro MN.emeasure_pair_measure_alt[symmetric] measurable_sets[OF _ A])
+    using fg by (intro N.emeasure_pair_measure_alt[symmetric] measurable_sets[OF _ A])
                 (auto cong: measurable_cong')
   also have "\<dots> = emeasure ?D A"
     using fg A by (subst emeasure_distr) auto
diff -r 970964690b3d -r 199d1d5bb17e src/HOL/Probability/Finite_Product_Measure.thy
--- a/src/HOL/Probability/Finite_Product_Measure.thy	Wed Oct 10 12:12:17 2012 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Wed Oct 10 12:12:18 2012 +0200
@@ -504,8 +504,7 @@
 qed (insert `i \<in> I`, auto simp: space_PiM)
 
 lemma measurable_add_dim:
-  assumes "i \<notin> I"
-  shows "(\<lambda>(f, y). f(i := y)) \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) (Pi\<^isub>M (insert i I) M)"
+  "(\<lambda>(f, y). f(i := y)) \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) (Pi\<^isub>M (insert i I) M)"
     (is "?f \<in> measurable ?P ?I")
 proof (rule measurable_PiM_single)
   fix j A assume j: "j \<in> insert i I" and A: "A \<in> sets (M j)"
@@ -519,19 +518,18 @@
 qed (auto simp: space_pair_measure space_PiM)
 
 lemma measurable_merge:
-  assumes "I \<inter> J = {}"
-  shows "(\<lambda>(x, y). merge I x J y) \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) (Pi\<^isub>M (I \<union> J) M)"
+  "(\<lambda>(x, y). merge I x J y) \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) (Pi\<^isub>M (I \<union> J) M)"
     (is "?f \<in> measurable ?P ?U")
 proof (rule measurable_PiM_single)
   fix i A assume A: "A \<in> sets (M i)" "i \<in> I \<union> J"
-  then have "{\<omega> \<in> space ?P. prod_case (\<lambda>x. merge I x J) \<omega> i \<in> A} =
+  then have "{\<omega> \<in> space ?P. prod_case (\<lambda>x y. merge I x J y) \<omega> i \<in> A} =
     (if i \<in> I then ((\<lambda>x. x i) \<circ> fst) -` A \<inter> space ?P else ((\<lambda>x. x i) \<circ> snd) -` A \<inter> space ?P)"
-    using `I \<inter> J = {}` by auto
+    by (auto simp: merge_def)
   also have "\<dots> \<in> sets ?P"
     using A
     by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton])
-  finally show "{\<omega> \<in> space ?P. prod_case (\<lambda>x. merge I x J) \<omega> i \<in> A} \<in> sets ?P" .
-qed (insert assms, auto simp: space_pair_measure space_PiM)
+  finally show "{\<omega> \<in> space ?P. prod_case (\<lambda>x y. merge I x J y) \<omega> i \<in> A} \<in> sets ?P" .
+qed (auto simp: space_pair_measure space_PiM Pi_iff merge_def extensional_def)
 
 lemma measurable_restrict:
   assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> measurable N (M i)"
@@ -587,12 +585,9 @@
   qed
 qed
 
-lemma (in product_sigma_finite)
-  assumes "finite I"
-  shows sigma_finite: "sigma_finite_measure (PiM I M)"
-  and emeasure_PiM:
-    "\<And>A. (\<And>i. i\<in>I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> emeasure (PiM I M) (Pi\<^isub>E I A) = (\<Prod>i\<in>I. emeasure (M i) (A i))"
-using `finite I` proof induct
+lemma (in product_sigma_finite) emeasure_PiM:
+  "finite I \<Longrightarrow> (\<And>i. i\<in>I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> emeasure (PiM I M) (Pi\<^isub>E I A) = (\<Prod>i\<in>I. emeasure (M i) (A i))"
+proof (induct I arbitrary: A rule: finite_induct)
   case empty
   let ?\<mu> = "\<lambda>A. if A = {} then 0 else (1::ereal)"
   have "prod_algebra {} M = {{\<lambda>_. undefined}}"
@@ -610,21 +605,13 @@
   qed (auto simp: prod_emb_def)
   also have *: "(prod_emb {} M {} (\<Pi>\<^isub>E i\<in>{}. {})) = {\<lambda>_. undefined}"
     by (auto simp: prod_emb_def)
-  finally have emeasure_eq: "emeasure (Pi\<^isub>M {} M) {\<lambda>_. undefined} = 1" .
-
-  interpret finite_measure "PiM {} M"
-    by default (simp add: space_PiM emeasure_eq)
-  case 1 show ?case ..
-
-  case 2 show ?case
-    using emeasure_eq * by simp
+  finally show ?case
+    using * by simp
 next
   case (insert i I)
   interpret finite_product_sigma_finite M I by default fact
   have "finite (insert i I)" using `finite I` by auto
   interpret I': finite_product_sigma_finite M "insert i I" by default fact
-  interpret I: sigma_finite_measure "PiM I M" by fact
-  interpret P: pair_sigma_finite "PiM I M" "M i" ..
   let ?h = "(\<lambda>(f, y). f(i := y))"
 
   let ?P = "distr (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) (Pi\<^isub>M (insert i I) M) ?h"
@@ -632,67 +619,73 @@
   let ?I = "{j \<in> insert i I. emeasure (M j) (space (M j)) \<noteq> 1}"
   let ?f = "\<lambda>J E j. if j \<in> J then emeasure (M j) (E j) else emeasure (M j) (space (M j))"
 
-  { case 2
-    have "emeasure (Pi\<^isub>M (insert i I) M) (prod_emb (insert i I) M (insert i I) (Pi\<^isub>E (insert i I) A)) =
-      (\<Prod>i\<in>insert i I. emeasure (M i) (A i))"
-    proof (subst emeasure_extend_measure_Pair[OF PiM_def])
-      fix J E assume "(J \<noteq> {} \<or> insert i I = {}) \<and> finite J \<and> J \<subseteq> insert i I \<and> E \<in> (\<Pi> j\<in>J. sets (M j))"
-      then have J: "J \<noteq> {}" "finite J" "J \<subseteq> insert i I" and E: "\<forall>j\<in>J. E j \<in> sets (M j)" by auto
-      let ?p = "prod_emb (insert i I) M J (Pi\<^isub>E J E)"
-      let ?p' = "prod_emb I M (J - {i}) (\<Pi>\<^isub>E j\<in>J-{i}. E j)"
-      have "?\<mu> ?p =
-        emeasure (Pi\<^isub>M I M \<Otimes>\<^isub>M (M i)) (?h -` ?p \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M M i))"
-        by (intro emeasure_distr measurable_add_dim sets_PiM_I) fact+
-      also have "?h -` ?p \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) = ?p' \<times> (if i \<in> J then E i else space (M i))"
-        using J E[rule_format, THEN sets_into_space]
-        by (force simp: space_pair_measure space_PiM Pi_iff prod_emb_iff split: split_if_asm)
-      also have "emeasure (Pi\<^isub>M I M \<Otimes>\<^isub>M (M i)) (?p' \<times> (if i \<in> J then E i else space (M i))) =
-        emeasure (Pi\<^isub>M I M) ?p' * emeasure (M i) (if i \<in> J then (E i) else space (M i))"
-        using J E by (intro P.emeasure_pair_measure_Times sets_PiM_I) auto
-      also have "?p' = (\<Pi>\<^isub>E j\<in>I. if j \<in> J-{i} then E j else space (M j))"
-        using J E[rule_format, THEN sets_into_space]
-        by (auto simp: prod_emb_iff Pi_iff split: split_if_asm) blast+
-      also have "emeasure (Pi\<^isub>M I M) (\<Pi>\<^isub>E j\<in>I. if j \<in> J-{i} then E j else space (M j)) =
-        (\<Prod> j\<in>I. if j \<in> J-{i} then emeasure (M j) (E j) else emeasure (M j) (space (M j)))"
-        using E by (subst insert) (auto intro!: setprod_cong)
-      also have "(\<Prod>j\<in>I. if j \<in> J - {i} then emeasure (M j) (E j) else emeasure (M j) (space (M j))) *
-         emeasure (M i) (if i \<in> J then E i else space (M i)) = (\<Prod>j\<in>insert i I. ?f J E j)"
-        using insert by (auto simp: mult_commute intro!: arg_cong2[where f="op *"] setprod_cong)
-      also have "\<dots> = (\<Prod>j\<in>J \<union> ?I. ?f J E j)"
-        using insert(1,2) J E by (intro setprod_mono_one_right) auto
-      finally show "?\<mu> ?p = \<dots>" .
+  have "emeasure (Pi\<^isub>M (insert i I) M) (prod_emb (insert i I) M (insert i I) (Pi\<^isub>E (insert i I) A)) =
+    (\<Prod>i\<in>insert i I. emeasure (M i) (A i))"
+  proof (subst emeasure_extend_measure_Pair[OF PiM_def])
+    fix J E assume "(J \<noteq> {} \<or> insert i I = {}) \<and> finite J \<and> J \<subseteq> insert i I \<and> E \<in> (\<Pi> j\<in>J. sets (M j))"
+    then have J: "J \<noteq> {}" "finite J" "J \<subseteq> insert i I" and E: "\<forall>j\<in>J. E j \<in> sets (M j)" by auto
+    let ?p = "prod_emb (insert i I) M J (Pi\<^isub>E J E)"
+    let ?p' = "prod_emb I M (J - {i}) (\<Pi>\<^isub>E j\<in>J-{i}. E j)"
+    have "?\<mu> ?p =
+      emeasure (Pi\<^isub>M I M \<Otimes>\<^isub>M (M i)) (?h -` ?p \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M M i))"
+      by (intro emeasure_distr measurable_add_dim sets_PiM_I) fact+
+    also have "?h -` ?p \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) = ?p' \<times> (if i \<in> J then E i else space (M i))"
+      using J E[rule_format, THEN sets_into_space]
+      by (force simp: space_pair_measure space_PiM Pi_iff prod_emb_iff split: split_if_asm)
+    also have "emeasure (Pi\<^isub>M I M \<Otimes>\<^isub>M (M i)) (?p' \<times> (if i \<in> J then E i else space (M i))) =
+      emeasure (Pi\<^isub>M I M) ?p' * emeasure (M i) (if i \<in> J then (E i) else space (M i))"
+      using J E by (intro M.emeasure_pair_measure_Times sets_PiM_I) auto
+    also have "?p' = (\<Pi>\<^isub>E j\<in>I. if j \<in> J-{i} then E j else space (M j))"
+      using J E[rule_format, THEN sets_into_space]
+      by (auto simp: prod_emb_iff Pi_iff split: split_if_asm) blast+
+    also have "emeasure (Pi\<^isub>M I M) (\<Pi>\<^isub>E j\<in>I. if j \<in> J-{i} then E j else space (M j)) =
+      (\<Prod> j\<in>I. if j \<in> J-{i} then emeasure (M j) (E j) else emeasure (M j) (space (M j)))"
+      using E by (subst insert) (auto intro!: setprod_cong)
+    also have "(\<Prod>j\<in>I. if j \<in> J - {i} then emeasure (M j) (E j) else emeasure (M j) (space (M j))) *
+       emeasure (M i) (if i \<in> J then E i else space (M i)) = (\<Prod>j\<in>insert i I. ?f J E j)"
+      using insert by (auto simp: mult_commute intro!: arg_cong2[where f="op *"] setprod_cong)
+    also have "\<dots> = (\<Prod>j\<in>J \<union> ?I. ?f J E j)"
+      using insert(1,2) J E by (intro setprod_mono_one_right) auto
+    finally show "?\<mu> ?p = \<dots>" .
 
-      show "prod_emb (insert i I) M J (Pi\<^isub>E J E) \<in> Pow (\<Pi>\<^isub>E i\<in>insert i I. space (M i))"
-        using J E[rule_format, THEN sets_into_space] by (auto simp: prod_emb_iff)
-    next
-      show "positive (sets (Pi\<^isub>M (insert i I) M)) ?\<mu>" "countably_additive (sets (Pi\<^isub>M (insert i I) M)) ?\<mu>"
-        using emeasure_positive[of ?P] emeasure_countably_additive[of ?P] by simp_all
-    next
-      show "(insert i I \<noteq> {} \<or> insert i I = {}) \<and> finite (insert i I) \<and>
-        insert i I \<subseteq> insert i I \<and> A \<in> (\<Pi> j\<in>insert i I. sets (M j))"
-        using insert(1,2) 2 by auto
-    qed (auto intro!: setprod_cong)
-    with 2[THEN sets_into_space] show ?case by (subst (asm) prod_emb_PiE_same_index) auto }
-  note product = this
+    show "prod_emb (insert i I) M J (Pi\<^isub>E J E) \<in> Pow (\<Pi>\<^isub>E i\<in>insert i I. space (M i))"
+      using J E[rule_format, THEN sets_into_space] by (auto simp: prod_emb_iff)
+  next
+    show "positive (sets (Pi\<^isub>M (insert i I) M)) ?\<mu>" "countably_additive (sets (Pi\<^isub>M (insert i I) M)) ?\<mu>"
+      using emeasure_positive[of ?P] emeasure_countably_additive[of ?P] by simp_all
+  next
+    show "(insert i I \<noteq> {} \<or> insert i I = {}) \<and> finite (insert i I) \<and>
+      insert i I \<subseteq> insert i I \<and> A \<in> (\<Pi> j\<in>insert i I. sets (M j))"
+      using insert by auto
+  qed (auto intro!: setprod_cong)
+  with insert show ?case
+    by (subst (asm) prod_emb_PiE_same_index) (auto intro!: sets_into_space)
+qed
 
-  from I'.sigma_finite_pairs guess F :: "'i \<Rightarrow> nat \<Rightarrow> 'a set" ..
-  then have F: "\<And>j. j \<in> insert i I \<Longrightarrow> range (F j) \<subseteq> sets (M j)"
-    "incseq (\<lambda>k. \<Pi>\<^isub>E j \<in> insert i I. F j k)"
-    "(\<Union>k. \<Pi>\<^isub>E j \<in> insert i I. F j k) = space (Pi\<^isub>M (insert i I) M)"
-    "\<And>k. \<And>j. j \<in> insert i I \<Longrightarrow> emeasure (M j) (F j k) \<noteq> \<infinity>"
+lemma (in product_sigma_finite) sigma_finite: 
+  assumes "finite I"
+  shows "sigma_finite_measure (PiM I M)"
+proof -
+  interpret finite_product_sigma_finite M I by default fact
+
+  from sigma_finite_pairs guess F :: "'i \<Rightarrow> nat \<Rightarrow> 'a set" ..
+  then have F: "\<And>j. j \<in> I \<Longrightarrow> range (F j) \<subseteq> sets (M j)"
+    "incseq (\<lambda>k. \<Pi>\<^isub>E j \<in> I. F j k)"
+    "(\<Union>k. \<Pi>\<^isub>E j \<in> I. F j k) = space (Pi\<^isub>M I M)"
+    "\<And>k. \<And>j. j \<in> I \<Longrightarrow> emeasure (M j) (F j k) \<noteq> \<infinity>"
     by blast+
-  let ?F = "\<lambda>k. \<Pi>\<^isub>E j \<in> insert i I. F j k"
+  let ?F = "\<lambda>k. \<Pi>\<^isub>E j \<in> I. F j k"
 
-  case 1 show ?case
+  show ?thesis
   proof (unfold_locales, intro exI[of _ ?F] conjI allI)
-    show "range ?F \<subseteq> sets (Pi\<^isub>M (insert i I) M)" using F(1) insert(1,2) by auto
+    show "range ?F \<subseteq> sets (Pi\<^isub>M I M)" using F(1) `finite I` by auto
   next
-    from F(3) show "(\<Union>i. ?F i) = space (Pi\<^isub>M (insert i I) M)" by simp
+    from F(3) show "(\<Union>i. ?F i) = space (Pi\<^isub>M I M)" by simp
   next
     fix j
-    from F `finite I` setprod_PInf[of "insert i I", OF emeasure_nonneg, of M]
-    show "emeasure (\<Pi>\<^isub>M i\<in>insert i I. M i) (?F j) \<noteq> \<infinity>"
-      by (subst product) auto
+    from F `finite I` setprod_PInf[of I, OF emeasure_nonneg, of M]
+    show "emeasure (\<Pi>\<^isub>M i\<in>I. M i) (?F j) \<noteq> \<infinity>"
+      by (subst emeasure_PiM) auto
   qed
 qed
 
@@ -786,7 +779,7 @@
       using A by (intro emeasure_distr measurable_merge) (auto simp: sets_PiM)
     also have "emeasure ?B ?X = (\<Prod>i\<in>I. emeasure (M i) (F i)) * (\<Prod>i\<in>J. emeasure (M i) (F i))"
       using `finite J` `finite I` F X
-      by (simp add: P.emeasure_pair_measure_Times I.measure_times J.measure_times Pi_iff)
+      by (simp add: J.emeasure_pair_measure_Times I.measure_times J.measure_times Pi_iff)
     also have "\<dots> = (\<Prod>i\<in>I \<union> J. emeasure (M i) (F i))"
       using `finite J` `finite I` `I \<inter> J = {}`  by (simp add: setprod_Un_one)
     also have "\<dots> = emeasure ?P (Pi\<^isub>E (I \<union> J) F)"
@@ -806,10 +799,10 @@
   interpret J: finite_product_sigma_finite M J by default fact
   interpret P: pair_sigma_finite "Pi\<^isub>M I M" "Pi\<^isub>M J M" by default
   have P_borel: "(\<lambda>x. f (case x of (x, y) \<Rightarrow> merge I x J y)) \<in> borel_measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M)"
-    using measurable_comp[OF measurable_merge[OF IJ(1)] f] by (simp add: comp_def)
+    using measurable_comp[OF measurable_merge f] by (simp add: comp_def)
   show ?thesis
     apply (subst distr_merge[OF IJ, symmetric])
-    apply (subst positive_integral_distr[OF measurable_merge f, OF IJ(1)])
+    apply (subst positive_integral_distr[OF measurable_merge f])
     apply (subst P.positive_integral_fst_measurable(2)[symmetric, OF P_borel])
     apply simp
     done
@@ -914,17 +907,42 @@
   from f have f_borel: "f \<in> borel_measurable (Pi\<^isub>M (I \<union> J) M)"
     by auto
   have P_borel: "(\<lambda>x. f (case x of (x, y) \<Rightarrow> merge I x J y)) \<in> borel_measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M)"
-    using measurable_comp[OF measurable_merge[OF IJ(1)] f_borel] by (simp add: comp_def)
+    using measurable_comp[OF measurable_merge f_borel] by (simp add: comp_def)
   have f_int: "integrable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) ?f"
-    by (rule integrable_distr[OF measurable_merge[OF IJ]]) (simp add: distr_merge[OF IJ fin] f)
+    by (rule integrable_distr[OF measurable_merge]) (simp add: distr_merge[OF IJ fin] f)
   show ?thesis
     apply (subst distr_merge[symmetric, OF IJ fin])
-    apply (subst integral_distr[OF measurable_merge[OF IJ] f_borel])
+    apply (subst integral_distr[OF measurable_merge f_borel])
     apply (subst P.integrable_fst_measurable(2)[symmetric, OF f_int])
     apply simp
     done
 qed
 
+lemma (in product_sigma_finite)
+  assumes IJ: "I \<inter> J = {}" "finite I" "finite J" and A: "A \<in> sets (Pi\<^isub>M (I \<union> J) M)"
+  shows emeasure_fold_integral:
+    "emeasure (Pi\<^isub>M (I \<union> J) M) A = (\<integral>\<^isup>+x. emeasure (Pi\<^isub>M J M) (merge I x J -` A \<inter> space (Pi\<^isub>M J M)) \<partial>Pi\<^isub>M I M)" (is ?I)
+    and emeasure_fold_measurable:
+    "(\<lambda>x. emeasure (Pi\<^isub>M J M) (merge I x J -` A \<inter> space (Pi\<^isub>M J M))) \<in> borel_measurable (Pi\<^isub>M I M)" (is ?B)
+proof -
+  interpret I: finite_product_sigma_finite M I by default fact
+  interpret J: finite_product_sigma_finite M J by default fact
+  interpret IJ: pair_sigma_finite "Pi\<^isub>M I M" "Pi\<^isub>M J M" ..
+  have merge: "(\<lambda>(x, y). merge I x J y) -` A \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) \<in> sets (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M)"
+    by (intro measurable_sets[OF _ A] measurable_merge assms)
+
+  show ?I
+    apply (subst distr_merge[symmetric, OF IJ])
+    apply (subst emeasure_distr[OF measurable_merge A])
+    apply (subst J.emeasure_pair_measure_alt[OF merge])
+    apply (auto intro!: positive_integral_cong arg_cong2[where f=emeasure] simp: space_pair_measure)
+    done
+
+  show ?B
+    using IJ.measurable_emeasure_Pair1[OF merge]
+    by (simp add: vimage_compose[symmetric] comp_def space_pair_measure cong: measurable_cong)
+qed
+
 lemma (in product_sigma_finite) product_integral_insert:
   assumes I: "finite I" "i \<notin> I"
     and f: "integrable (Pi\<^isub>M (insert i I) M) f"
@@ -999,6 +1017,56 @@
     by (simp add: * insert integral_multc integral_cmult[OF prod] subset_insertI)
 qed
 
+lemma sets_Collect_single:
+  "i \<in> I \<Longrightarrow> A \<in> sets (M i) \<Longrightarrow> { x \<in> space (Pi\<^isub>M I M). x i \<in> A } \<in> sets (Pi\<^isub>M I M)"
+  unfolding sets_PiM_single
+  by (auto intro!: sigma_sets.Basic exI[of _ i] exI[of _ A]) (auto simp: space_PiM)
+
+lemma sigma_prod_algebra_sigma_eq_infinite:
+  fixes E :: "'i \<Rightarrow> 'a set set"
+  assumes S_mono: "\<And>i. i \<in> I \<Longrightarrow> incseq (S i)"
+    and S_union: "\<And>i. i \<in> I \<Longrightarrow> (\<Union>j. S i j) = space (M i)"
+    and S_in_E: "\<And>i. i \<in> I \<Longrightarrow> range (S i) \<subseteq> E i"
+  assumes E_closed: "\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> Pow (space (M i))"
+    and E_generates: "\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sigma_sets (space (M i)) (E i)"
+  defines "P == {{f\<in>\<Pi>\<^isub>E i\<in>I. space (M i). f i \<in> A} | i A. i \<in> I \<and> A \<in> E i}"
+  shows "sets (PiM I M) = sigma_sets (space (PiM I M)) P"
+proof
+  let ?P = "sigma (space (Pi\<^isub>M I M)) P"
+  have P_closed: "P \<subseteq> Pow (space (Pi\<^isub>M I M))"
+    using E_closed by (auto simp: space_PiM P_def Pi_iff subset_eq)
+  then have space_P: "space ?P = (\<Pi>\<^isub>E i\<in>I. space (M i))"
+    by (simp add: space_PiM)
+  have "sets (PiM I M) =
+      sigma_sets (space ?P) {{f \<in> \<Pi>\<^isub>E i\<in>I. space (M i). f i \<in> A} |i A. i \<in> I \<and> A \<in> sets (M i)}"
+    using sets_PiM_single[of I M] by (simp add: space_P)
+  also have "\<dots> \<subseteq> sets (sigma (space (PiM I M)) P)"
+  proof (safe intro!: sigma_sets_subset)
+    fix i A assume "i \<in> I" and A: "A \<in> sets (M i)"
+    then have "(\<lambda>x. x i) \<in> measurable ?P (sigma (space (M i)) (E i))"
+      apply (subst measurable_iff_measure_of)
+      apply (simp_all add: P_closed)
+      using E_closed
+      apply (force simp: subset_eq space_PiM)
+      apply (force simp: subset_eq space_PiM)
+      apply (auto simp: P_def intro!: sigma_sets.Basic exI[of _ i])
+      apply (rule_tac x=Aa in exI)
+      apply (auto simp: space_PiM)
+      done
+    from measurable_sets[OF this, of A] A `i \<in> I` E_closed
+    have "(\<lambda>x. x i) -` A \<inter> space ?P \<in> sets ?P"
+      by (simp add: E_generates)
+    also have "(\<lambda>x. x i) -` A \<inter> space ?P = {f \<in> \<Pi>\<^isub>E i\<in>I. space (M i). f i \<in> A}"
+      using P_closed by (auto simp: space_PiM)
+    finally show "\<dots> \<in> sets ?P" .
+  qed
+  finally show "sets (PiM I M) \<subseteq> sigma_sets (space (PiM I M)) P"
+    by (simp add: P_closed)
+  show "sigma_sets (space (PiM I M)) P \<subseteq> sets (PiM I M)"
+    unfolding P_def space_PiM[symmetric]
+    by (intro sigma_sets_subset) (auto simp: E_generates sets_Collect_single)
+qed
+
 lemma sigma_prod_algebra_sigma_eq:
   fixes E :: "'i \<Rightarrow> 'a set set"
   assumes "finite I"
diff -r 970964690b3d -r 199d1d5bb17e src/HOL/Probability/Independent_Family.thy
--- a/src/HOL/Probability/Independent_Family.thy	Wed Oct 10 12:12:17 2012 +0200
+++ b/src/HOL/Probability/Independent_Family.thy	Wed Oct 10 12:12:18 2012 +0200
@@ -1035,7 +1035,7 @@
     fix X assume "X \<in> ?E"
     then obtain A B where X[simp]: "X = A \<times> B" and A: "A \<in> sets M1" and B: "B \<in> sets M2" by auto
     then have "emeasure ?P X = emeasure M1 A * emeasure M2 B"
-       by (simp add: emeasure_pair_measure_Times)
+       by (simp add: M2.emeasure_pair_measure_Times)
     also have "\<dots> = emeasure M (A \<times> B)"
       using A B emeasure by auto
     finally show "emeasure ?P X = emeasure M X"
@@ -1143,7 +1143,7 @@
       also have "\<dots> = emeasure (?S \<Otimes>\<^isub>M ?T) (A \<times> B)"
         unfolding `?S \<Otimes>\<^isub>M ?T = ?J` ..
       also have "\<dots> = emeasure ?S A * emeasure ?T B"
-        using ab by (simp add: XY.emeasure_pair_measure_Times)
+        using ab by (simp add: Y.emeasure_pair_measure_Times)
       finally show "prob ((X -` A \<inter> space M) \<inter> (Y -` B \<inter> space M)) =
         prob (X -` A \<inter> space M) * prob (Y -` B \<inter> space M)"
         using rvs ab by (simp add: emeasure_eq_measure emeasure_distr)
diff -r 970964690b3d -r 199d1d5bb17e src/HOL/Probability/Infinite_Product_Measure.thy
--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Oct 10 12:12:17 2012 +0200
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Oct 10 12:12:18 2012 +0200
@@ -8,31 +8,6 @@
   imports Probability_Measure Caratheodory
 begin
 
-lemma (in product_sigma_finite)
-  assumes IJ: "I \<inter> J = {}" "finite I" "finite J" and A: "A \<in> sets (Pi\<^isub>M (I \<union> J) M)"
-  shows emeasure_fold_integral:
-    "emeasure (Pi\<^isub>M (I \<union> J) M) A = (\<integral>\<^isup>+x. emeasure (Pi\<^isub>M J M) (merge I x J -` A \<inter> space (Pi\<^isub>M J M)) \<partial>Pi\<^isub>M I M)" (is ?I)
-    and emeasure_fold_measurable:
-    "(\<lambda>x. emeasure (Pi\<^isub>M J M) (merge I x J -` A \<inter> space (Pi\<^isub>M J M))) \<in> borel_measurable (Pi\<^isub>M I M)" (is ?B)
-proof -
-  interpret I: finite_product_sigma_finite M I by default fact
-  interpret J: finite_product_sigma_finite M J by default fact
-  interpret IJ: pair_sigma_finite "Pi\<^isub>M I M" "Pi\<^isub>M J M" ..
-  have merge: "(\<lambda>(x, y). merge I x J y) -` A \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) \<in> sets (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M)"
-    by (intro measurable_sets[OF _ A] measurable_merge assms)
-
-  show ?I
-    apply (subst distr_merge[symmetric, OF IJ])
-    apply (subst emeasure_distr[OF measurable_merge[OF IJ(1)] A])
-    apply (subst IJ.emeasure_pair_measure_alt[OF merge])
-    apply (auto intro!: positive_integral_cong arg_cong2[where f=emeasure] simp: space_pair_measure)
-    done
-
-  show ?B
-    using IJ.measurable_emeasure_Pair1[OF merge]
-    by (simp add: vimage_compose[symmetric] comp_def space_pair_measure cong: measurable_cong)
-qed
-
 lemma restrict_extensional_sub[intro]: "A \<subseteq> B \<Longrightarrow> restrict f A \<in> extensional B"
   unfolding restrict_def extensional_def by auto
 
diff -r 970964690b3d -r 199d1d5bb17e src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Wed Oct 10 12:12:17 2012 +0200
+++ b/src/HOL/Probability/Information.thy	Wed Oct 10 12:12:18 2012 +0200
@@ -194,7 +194,7 @@
   unfolding KL_divergence_def
 proof (subst integral_density)
   show "entropy_density b M (density M (\<lambda>x. ereal (f x))) \<in> borel_measurable M"
-    using f `1 < b`
+    using f
     by (auto simp: comp_def entropy_density_def intro!: borel_measurable_log borel_measurable_RN_deriv_density)
   have "density M (RN_deriv M (density M f)) = density M f"
     using f by (intro density_RN_deriv_density) auto
diff -r 970964690b3d -r 199d1d5bb17e src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Wed Oct 10 12:12:17 2012 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy	Wed Oct 10 12:12:18 2012 +0200
@@ -407,7 +407,7 @@
 sublocale pair_prob_space \<subseteq> P: prob_space "M1 \<Otimes>\<^isub>M M2"
 proof
   show "emeasure (M1 \<Otimes>\<^isub>M M2) (space (M1 \<Otimes>\<^isub>M M2)) = 1"
-    by (simp add: emeasure_pair_measure_Times M1.emeasure_space_1 M2.emeasure_space_1 space_pair_measure)
+    by (simp add: M2.emeasure_pair_measure_Times M1.emeasure_space_1 M2.emeasure_space_1 space_pair_measure)
 qed
 
 locale product_prob_space = product_sigma_finite M for M :: "'i \<Rightarrow> 'a measure" +