# HG changeset patch
# User hoelzl
# Date 1291661696 -3600
# Node ID bea75746dc9dae3b53e5fdc9e3e3cc74c0580d5a
# Parent  8b2cd85ecf11914f13c119e775ad83cf2205e4ec
folding on arbitrary Lebesgue integrable functions

diff -r 8b2cd85ecf11 -r bea75746dc9d src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Mon Dec 06 19:54:53 2010 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Mon Dec 06 19:54:56 2010 +0100
@@ -847,6 +847,15 @@
     by (simp add: borel_measurable_iff_ge)
 qed
 
+lemma (in sigma_algebra) borel_measurable_setsum[simp, intro]:
+  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
+  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
+  shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
+proof cases
+  assume "finite S"
+  thus ?thesis using assms by induct auto
+qed simp
+
 lemma (in sigma_algebra) borel_measurable_square:
   fixes f :: "'a \<Rightarrow> real"
   assumes f: "f \<in> borel_measurable M"
@@ -930,6 +939,15 @@
     using 1 2 by simp
 qed
 
+lemma (in sigma_algebra) borel_measurable_setprod[simp, intro]:
+  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
+  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
+  shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
+proof cases
+  assume "finite S"
+  thus ?thesis using assms by induct auto
+qed simp
+
 lemma (in sigma_algebra) borel_measurable_diff[simp, intro]:
   fixes f :: "'a \<Rightarrow> real"
   assumes f: "f \<in> borel_measurable M"
@@ -937,15 +955,6 @@
   shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
   unfolding diff_minus using assms by fast
 
-lemma (in sigma_algebra) borel_measurable_setsum[simp, intro]:
-  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
-  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
-  shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
-proof cases
-  assume "finite S"
-  thus ?thesis using assms by induct auto
-qed simp
-
 lemma (in sigma_algebra) borel_measurable_inverse[simp, intro]:
   fixes f :: "'a \<Rightarrow> real"
   assumes "f \<in> borel_measurable M"
@@ -1007,6 +1016,11 @@
   show ?thesis unfolding * using assms by auto
 qed
 
+lemma borel_measurable_nth[simp, intro]:
+  "(\<lambda>x::real^'n. x $ i) \<in> borel_measurable borel"
+  using borel_measurable_euclidean_component
+  unfolding nth_conv_component by auto
+
 section "Borel space over the real line with infinity"
 
 lemma borel_Real_measurable:
diff -r 8b2cd85ecf11 -r bea75746dc9d src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Mon Dec 06 19:54:53 2010 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Mon Dec 06 19:54:56 2010 +0100
@@ -2034,6 +2034,15 @@
     using assms(2) by (cases ?thesis) auto
 qed
 
+lemma (in measure_space) positive_integral_omega_AE:
+  assumes "f \<in> borel_measurable M" "positive_integral f \<noteq> \<omega>" shows "AE x. f x \<noteq> \<omega>"
+proof (rule AE_I)
+  show "\<mu> (f -` {\<omega>} \<inter> space M) = 0"
+    by (rule positive_integral_omega[OF assms])
+  show "f -` {\<omega>} \<inter> space M \<in> sets M"
+    using assms by (auto intro: borel_measurable_vimage)
+qed auto
+
 lemma (in measure_space) simple_integral_omega:
   assumes "simple_function f"
   and "simple_integral f \<noteq> \<omega>"
@@ -2044,6 +2053,23 @@
     using assms by (simp add: positive_integral_eq_simple_integral)
 qed
 
+lemma (in measure_space) integral_real:
+  fixes f :: "'a \<Rightarrow> pextreal"
+  assumes "AE x. f x \<noteq> \<omega>"
+  shows "integral (\<lambda>x. real (f x)) = real (positive_integral f)" (is ?plus)
+    and "integral (\<lambda>x. - real (f x)) = - real (positive_integral f)" (is ?minus)
+proof -
+  have "positive_integral (\<lambda>x. Real (real (f x))) = positive_integral f"
+    apply (rule positive_integral_cong_AE)
+    apply (rule AE_mp[OF assms(1)])
+    by (auto intro!: AE_cong simp: Real_real)
+  moreover
+  have "positive_integral (\<lambda>x. Real (- real (f x))) = positive_integral (\<lambda>x. 0)"
+    by (intro positive_integral_cong) auto
+  ultimately show ?plus ?minus
+    by (auto simp: integral_def integrable_def)
+qed
+
 lemma (in measure_space) integral_dominated_convergence:
   assumes u: "\<And>i. integrable (u i)" and bound: "\<And>x j. x\<in>space M \<Longrightarrow> \<bar>u j x\<bar> \<le> w x"
   and w: "integrable w" "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> w x"
diff -r 8b2cd85ecf11 -r bea75746dc9d src/HOL/Probability/Product_Measure.thy
--- a/src/HOL/Probability/Product_Measure.thy	Mon Dec 06 19:54:53 2010 +0100
+++ b/src/HOL/Probability/Product_Measure.thy	Mon Dec 06 19:54:56 2010 +0100
@@ -14,6 +14,9 @@
 lemma case_prod_distrib: "f (case x of (x, y) \<Rightarrow> g x y) = (case x of (x, y) \<Rightarrow> f (g x y))"
   by (cases x) simp
 
+lemma split_beta': "(\<lambda>(x,y). f x y) = (\<lambda>x. f (fst x) (snd x))"
+  by (auto simp: fun_eq_iff)
+
 abbreviation
   "Pi\<^isub>E A B \<equiv> Pi A B \<inter> extensional A"
 
@@ -819,6 +822,147 @@
   qed
 qed
 
+lemma (in pair_sigma_finite) positive_integral_product_swap:
+  "measure_space.positive_integral
+    (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) f =
+  positive_integral (\<lambda>(x,y). f (y,x))"
+proof -
+  interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
+  have t: "(\<lambda>y. case case y of (y, x) \<Rightarrow> (x, y) of (x, y) \<Rightarrow> f (y, x)) = f"
+    by (auto simp: fun_eq_iff)
+  have bij: "bij_betw (\<lambda>(x, y). (y, x)) (space M2 \<times> space M1) (space P)"
+    by (auto intro!: inj_onI simp: space_pair_algebra bij_betw_def)
+  show ?thesis
+    unfolding positive_integral_vimage[OF bij, of "\<lambda>(y,x). f (x,y)"]
+    unfolding pair_sigma_algebra_swap[symmetric] t
+  proof (rule Q.positive_integral_cong_measure[symmetric])
+    fix A assume "A \<in> sets Q.P"
+    from this Q.sets_pair_sigma_algebra_swap[OF this]
+    show "pair_measure ((\<lambda>(x, y). (y, x)) ` A) = Q.pair_measure A"
+      by (auto intro!: M1.positive_integral_cong arg_cong[where f=\<mu>2]
+               simp: pair_measure_alt Q.pair_measure_alt2)
+  qed
+qed
+
+lemma (in pair_sigma_algebra) measurable_product_swap:
+  "f \<in> measurable (sigma (pair_algebra M2 M1)) M \<longleftrightarrow> (\<lambda>(x,y). f (y,x)) \<in> measurable P M"
+proof -
+  interpret Q: pair_sigma_algebra M2 M1 by default
+  show ?thesis
+    using pair_sigma_algebra_measurable[of "\<lambda>(x,y). f (y, x)"]
+    by (auto intro!: pair_sigma_algebra_measurable Q.pair_sigma_algebra_measurable iffI)
+qed
+
+lemma (in pair_sigma_finite) integrable_product_swap:
+  "measure_space.integrable
+    (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) f \<longleftrightarrow>
+  integrable (\<lambda>(x,y). f (y,x))"
+proof -
+  interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
+  show ?thesis
+    unfolding Q.integrable_def integrable_def
+    unfolding positive_integral_product_swap
+    unfolding measurable_product_swap
+    by (simp add: case_prod_distrib)
+qed
+
+lemma (in pair_sigma_finite) integral_product_swap:
+  "measure_space.integral
+    (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) f =
+  integral (\<lambda>(x,y). f (y,x))"
+proof -
+  interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
+  show ?thesis
+    unfolding integral_def Q.integral_def positive_integral_product_swap
+    by (simp add: case_prod_distrib)
+qed
+
+lemma (in pair_sigma_finite) integrable_fst_measurable:
+  assumes f: "integrable f"
+  shows "M1.almost_everywhere (\<lambda>x. M2.integrable (\<lambda> y. f (x, y)))" (is "?AE")
+    and "M1.integral (\<lambda> x. M2.integral (\<lambda> y. f (x, y))) = integral f" (is "?INT")
+proof -
+  let "?pf x" = "Real (f x)" and "?nf x" = "Real (- f x)"
+  have
+    borel: "?nf \<in> borel_measurable P""?pf \<in> borel_measurable P" and
+    int: "positive_integral ?nf \<noteq> \<omega>" "positive_integral ?pf \<noteq> \<omega>"
+    using assms by auto
+  have "M1.positive_integral (\<lambda>x. M2.positive_integral (\<lambda>y. Real (f (x, y)))) \<noteq> \<omega>"
+     "M1.positive_integral (\<lambda>x. M2.positive_integral (\<lambda>y. Real (- f (x, y)))) \<noteq> \<omega>"
+    using borel[THEN positive_integral_fst_measurable(1)] int
+    unfolding borel[THEN positive_integral_fst_measurable(2)] by simp_all
+  with borel[THEN positive_integral_fst_measurable(1)]
+  have AE: "M1.almost_everywhere (\<lambda>x. M2.positive_integral (\<lambda>y. Real (f (x, y))) \<noteq> \<omega>)"
+    "M1.almost_everywhere (\<lambda>x. M2.positive_integral (\<lambda>y. Real (- f (x, y))) \<noteq> \<omega>)"
+    by (auto intro!: M1.positive_integral_omega_AE)
+  then show ?AE
+    apply (rule M1.AE_mp[OF _ M1.AE_mp])
+    apply (rule M1.AE_cong)
+    using assms unfolding M2.integrable_def
+    by (auto intro!: measurable_pair_image_snd)
+  have "M1.integrable
+     (\<lambda>x. real (M2.positive_integral (\<lambda>xa. Real (f (x, xa)))))" (is "M1.integrable ?f")
+  proof (unfold M1.integrable_def, intro conjI)
+    show "?f \<in> borel_measurable M1"
+      using borel by (auto intro!: M1.borel_measurable_real positive_integral_fst_measurable)
+    have "M1.positive_integral (\<lambda>x. Real (?f x)) =
+        M1.positive_integral (\<lambda>x. M2.positive_integral (\<lambda>xa. Real (f (x, xa))))"
+      apply (rule M1.positive_integral_cong_AE)
+      apply (rule M1.AE_mp[OF AE(1)])
+      apply (rule M1.AE_cong)
+      by (auto simp: Real_real)
+    then show "M1.positive_integral (\<lambda>x. Real (?f x)) \<noteq> \<omega>"
+      using positive_integral_fst_measurable[OF borel(2)] int by simp
+    have "M1.positive_integral (\<lambda>x. Real (- ?f x)) = M1.positive_integral (\<lambda>x. 0)"
+      by (intro M1.positive_integral_cong) simp
+    then show "M1.positive_integral (\<lambda>x. Real (- ?f x)) \<noteq> \<omega>" by simp
+  qed
+  moreover have "M1.integrable
+     (\<lambda>x. real (M2.positive_integral (\<lambda>xa. Real (- f (x, xa)))))" (is "M1.integrable ?f")
+  proof (unfold M1.integrable_def, intro conjI)
+    show "?f \<in> borel_measurable M1"
+      using borel by (auto intro!: M1.borel_measurable_real positive_integral_fst_measurable)
+    have "M1.positive_integral (\<lambda>x. Real (?f x)) =
+        M1.positive_integral (\<lambda>x. M2.positive_integral (\<lambda>xa. Real (- f (x, xa))))"
+      apply (rule M1.positive_integral_cong_AE)
+      apply (rule M1.AE_mp[OF AE(2)])
+      apply (rule M1.AE_cong)
+      by (auto simp: Real_real)
+    then show "M1.positive_integral (\<lambda>x. Real (?f x)) \<noteq> \<omega>"
+      using positive_integral_fst_measurable[OF borel(1)] int by simp
+    have "M1.positive_integral (\<lambda>x. Real (- ?f x)) = M1.positive_integral (\<lambda>x. 0)"
+      by (intro M1.positive_integral_cong) simp
+    then show "M1.positive_integral (\<lambda>x. Real (- ?f x)) \<noteq> \<omega>" by simp
+  qed
+  ultimately show ?INT
+    unfolding M2.integral_def integral_def
+      borel[THEN positive_integral_fst_measurable(2), symmetric]
+    by (simp add: M1.integral_real[OF AE(1)] M1.integral_real[OF AE(2)])
+qed
+
+lemma (in pair_sigma_finite) integrable_snd_measurable:
+  assumes f: "integrable f"
+  shows "M2.almost_everywhere (\<lambda>y. M1.integrable (\<lambda>x. f (x, y)))" (is "?AE")
+    and "M2.integral (\<lambda>y. M1.integral (\<lambda>x. f (x, y))) = integral f" (is "?INT")
+proof -
+  interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
+  have Q_int: "Q.integrable (\<lambda>(x, y). f (y, x))"
+    using f unfolding integrable_product_swap by simp
+  show ?INT
+    using Q.integrable_fst_measurable(2)[OF Q_int]
+    unfolding integral_product_swap by simp
+  show ?AE
+    using Q.integrable_fst_measurable(1)[OF Q_int]
+    by simp
+qed
+
+lemma (in pair_sigma_finite) Fubini_integral:
+  assumes f: "integrable f"
+  shows "M2.integral (\<lambda>y. M1.integral (\<lambda>x. f (x, y))) =
+      M1.integral (\<lambda>x. M2.integral (\<lambda>y. f (x, y)))"
+  unfolding integrable_snd_measurable[OF assms]
+  unfolding integrable_fst_measurable[OF assms] ..
+
 section "Finite product spaces"
 
 section "Products"
@@ -891,6 +1035,16 @@
   qed
 qed auto
 
+lemma borel_measurable_product_component:
+  assumes "i \<in> I"
+  shows "(\<lambda>x. x i) \<in> borel_measurable (sigma (product_algebra (\<lambda>x. borel) I))"
+proof -
+  have *: "\<And>A. (\<lambda>x. x i) -` A \<inter> extensional I = (\<Pi>\<^isub>E j\<in>I. if j = i then A else UNIV)"
+    using `i \<in> I` by (auto elim!: PiE)
+  show ?thesis
+    by (auto simp: * measurable_def product_algebra_def)
+qed
+
 section "Generating set generates also product algebra"
 
 lemma pair_sigma_algebra_sigma:
@@ -1414,11 +1568,14 @@
        (auto simp: pair_algebra_def dest: extensional_restrict)
 qed
 
-lemma (in product_sigma_finite) measure_fold_left:
+lemma (in product_sigma_finite) measure_fold:
   assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
-  and f: "f \<in> borel_measurable (sigma (product_algebra M (I \<union> J)))"
-  shows "product_positive_integral (I \<union> J) f =
-    product_positive_integral I (\<lambda>x. product_positive_integral J (\<lambda>y. f (merge I x J y)))"
+  assumes A: "A \<in> sets (sigma (product_algebra M (I \<union> J)))"
+  shows "pair_sigma_finite.pair_measure
+     (sigma (product_algebra M I)) (product_measure I)
+     (sigma (product_algebra M J)) (product_measure J)
+     ((\<lambda>x. ((\<lambda>i\<in>I. x i), (\<lambda>i\<in>J. x i))) ` A) =
+   product_measure (I \<union> J) A"
 proof -
   interpret I: finite_product_sigma_finite M \<mu> I by default fact
   interpret J: finite_product_sigma_finite M \<mu> J by default fact
@@ -1426,28 +1583,17 @@
   interpret IJ: finite_product_sigma_finite M \<mu> "I \<union> J" by default fact
   interpret P: pair_sigma_finite I.P I.measure J.P J.measure by default
   let ?f = "\<lambda>x. ((\<lambda>i\<in>I. x i), (\<lambda>i\<in>J. x i))"
-  have P_borel: "(\<lambda>x. f (case x of (x, y) \<Rightarrow> merge I x J y)) \<in> borel_measurable P.P"
-    by (subst product_product_vimage_algebra_eq[OF IJ fin, symmetric])
-       (auto simp: space_pair_algebra intro!: IJ.measurable_vimage f)
-  have split_f_image[simp]: "\<And>F. ?f ` (Pi\<^isub>E (I \<union> J) F) = (Pi\<^isub>E I F) \<times> (Pi\<^isub>E J F)"
-    apply auto apply (rule_tac x="merge I a J b" in image_eqI)
-    by (auto dest: extensional_restrict)
-  have "IJ.positive_integral f =  IJ.positive_integral (\<lambda>x. f (restrict x (I \<union> J)))"
-    by (auto intro!: IJ.positive_integral_cong arg_cong[where f=f] dest!: extensional_restrict)
-  also have "\<dots> = I.positive_integral (\<lambda>x. J.positive_integral (\<lambda>y. f (merge I x J y)))"
-    unfolding P.positive_integral_fst_measurable[OF P_borel, simplified]
-    unfolding P.positive_integral_vimage[unfolded space_sigma, OF bij_betw_restrict_I_J[OF IJ]]
-    unfolding product_product_vimage_algebra[OF IJ fin]
-  proof (simp, rule IJ.positive_integral_cong_measure[symmetric])
-    fix A assume *: "A \<in> sets IJ.P"
     from IJ.sigma_finite_pairs obtain F where
       F: "\<And>i. i\<in> I \<union> J \<Longrightarrow> range (F i) \<subseteq> sets (M i)"
          "(\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k) \<up> space IJ.G"
          "\<And>k. \<forall>i\<in>I\<union>J. \<mu> i (F i k) \<noteq> \<omega>"
       by auto
     let ?F = "\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k"
+  have split_f_image[simp]: "\<And>F. ?f ` (Pi\<^isub>E (I \<union> J) F) = (Pi\<^isub>E I F) \<times> (Pi\<^isub>E J F)"
+    apply auto apply (rule_tac x="merge I a J b" in image_eqI)
+    by (auto dest: extensional_restrict)
     show "P.pair_measure (?f ` A) = IJ.measure A"
-    proof (rule measure_unique_Int_stable[OF _ _ _ _ _ _ _ _ *])
+  proof (rule measure_unique_Int_stable[OF _ _ _ _ _ _ _ _ A])
       show "Int_stable IJ.G" by (simp add: PiE_Int Int_stable_def product_algebra_def) auto
       show "range ?F \<subseteq> sets IJ.G" using F by (simp add: image_subset_iff product_algebra_def)
       show "?F \<up> space IJ.G " using F(2) by simp
@@ -1480,10 +1626,36 @@
         using `finite I` F by (simp add: setprod_\<omega>)
     qed simp
   qed
+
+lemma (in product_sigma_finite) product_positive_integral_fold:
+  assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
+  and f: "f \<in> borel_measurable (sigma (product_algebra M (I \<union> J)))"
+  shows "product_positive_integral (I \<union> J) f =
+    product_positive_integral I (\<lambda>x. product_positive_integral J (\<lambda>y. f (merge I x J y)))"
+proof -
+  interpret I: finite_product_sigma_finite M \<mu> I by default fact
+  interpret J: finite_product_sigma_finite M \<mu> J by default fact
+  have "finite (I \<union> J)" using fin by auto
+  interpret IJ: finite_product_sigma_finite M \<mu> "I \<union> J" by default fact
+  interpret P: pair_sigma_finite I.P I.measure J.P J.measure by default
+  let ?f = "\<lambda>x. ((\<lambda>i\<in>I. x i), (\<lambda>i\<in>J. x i))"
+  have P_borel: "(\<lambda>x. f (case x of (x, y) \<Rightarrow> merge I x J y)) \<in> borel_measurable P.P"
+    by (subst product_product_vimage_algebra_eq[OF IJ fin, symmetric])
+       (auto simp: space_pair_algebra intro!: IJ.measurable_vimage f)
+  have "IJ.positive_integral f =  IJ.positive_integral (\<lambda>x. f (restrict x (I \<union> J)))"
+    by (auto intro!: IJ.positive_integral_cong arg_cong[where f=f] dest!: extensional_restrict)
+  also have "\<dots> = I.positive_integral (\<lambda>x. J.positive_integral (\<lambda>y. f (merge I x J y)))"
+    unfolding P.positive_integral_fst_measurable[OF P_borel, simplified]
+    unfolding P.positive_integral_vimage[unfolded space_sigma, OF bij_betw_restrict_I_J[OF IJ]]
+    unfolding product_product_vimage_algebra[OF IJ fin]
+    apply simp
+    apply (rule IJ.positive_integral_cong_measure[symmetric])
+    apply (rule measure_fold)
+    using assms by auto
   finally show ?thesis .
 qed
 
-lemma (in product_sigma_finite) finite_pair_measure_singleton:
+lemma (in product_sigma_finite) product_positive_integral_singleton:
   assumes f: "f \<in> borel_measurable (M i)"
   shows "product_positive_integral {i} (\<lambda>x. f (x i)) = M.positive_integral i f"
 proof -
@@ -1515,6 +1687,98 @@
   qed simp
 qed
 
+lemma (in product_sigma_finite) product_integral_singleton:
+  assumes f: "f \<in> borel_measurable (M i)"
+  shows "product_integral {i} (\<lambda>x. f (x i)) = M.integral i f"
+proof -
+  interpret I: finite_product_sigma_finite M \<mu> "{i}" by default simp
+  have *: "(\<lambda>x. Real (f x)) \<in> borel_measurable (M i)"
+    "(\<lambda>x. Real (- f x)) \<in> borel_measurable (M i)"
+    using assms by auto
+  show ?thesis
+    unfolding I.integral_def integral_def
+    unfolding *[THEN product_positive_integral_singleton] ..
+qed
+
+lemma (in product_sigma_finite) borel_measurable_merge_iff:
+  assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
+  shows "f \<in> measurable (sigma (pair_algebra
+      (sigma (product_algebra M I)) (sigma (product_algebra M J)))) M' \<longleftrightarrow>
+    (\<lambda>x. f (restrict x I, restrict x J)) \<in> measurable (sigma (product_algebra M (I \<union> J))) M'"
+proof -
+  interpret I: finite_product_sigma_finite M \<mu> I by default fact
+  interpret J: finite_product_sigma_finite M \<mu> J by default fact
+  have "finite (I \<union> J)" using fin by auto
+  interpret IJ: finite_product_sigma_finite M \<mu> "I \<union> J" by default fact
+  interpret P: pair_sigma_finite I.P I.measure J.P J.measure by default
+  let ?f = "\<lambda>x. (restrict x I, restrict x J)"
+  let ?S = "space (product_algebra M (I \<union> J))"
+  { fix p assume p: "p \<in> space (pair_algebra I.P J.P)"
+    have "?f (the_inv_into ?S ?f p) = p"
+    proof (intro f_the_inv_into_f[where f="?f"] inj_onI ext)
+      fix x y t assume "x \<in> ?S" "y \<in> ?S" "?f x = ?f y"
+      show "x t = y t"
+      proof cases
+        assume "t \<in> I \<union> J" then show ?thesis using `?f x = ?f y`
+          by (auto simp: restrict_def fun_eq_iff split: split_if_asm)
+      next
+        assume "t \<notin> I \<union> J" then show ?thesis
+          using `x \<in> ?S` `y \<in> ?S` by (auto simp: space_pair_algebra extensional_def)
+      qed
+    next
+      show "p \<in> ?f ` ?S" using p
+        by (intro image_eqI[of _ _ "merge I (fst p) J (snd p)"])
+           (auto simp: space_pair_algebra extensional_restrict)
+    qed }
+  note restrict = this
+  show ?thesis
+    apply (subst product_product_vimage_algebra[OF assms, symmetric])
+    apply (subst P.measurable_vimage_iff_inv)
+    using bij_betw_restrict_I_J[OF IJ, of M] apply simp
+    apply (rule measurable_cong)
+    by (auto simp del: space_product_algebra simp: restrict)
+qed
+
+lemma (in product_sigma_finite) product_integral_fold:
+  assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
+  and f: "measure_space.integrable (sigma (product_algebra M (I \<union> J))) (product_measure (I \<union> J)) f"
+  shows "product_integral (I \<union> J) f =
+    product_integral I (\<lambda>x. product_integral J (\<lambda>y. f (merge I x J y)))"
+proof -
+  interpret I: finite_product_sigma_finite M \<mu> I by default fact
+  interpret J: finite_product_sigma_finite M \<mu> J by default fact
+  have "finite (I \<union> J)" using fin by auto
+  interpret IJ: finite_product_sigma_finite M \<mu> "I \<union> J" by default fact
+  interpret P: pair_sigma_finite I.P I.measure J.P J.measure by default
+  let ?f = "\<lambda>(x,y). f (merge I x J y)"
+  have f_borel: "f \<in> borel_measurable IJ.P"
+     "(\<lambda>x. Real (f x)) \<in> borel_measurable IJ.P"
+     "(\<lambda>x. Real (- f x)) \<in> borel_measurable IJ.P"
+    using f unfolding integrable_def by auto
+  have f_restrict: "(\<lambda>x. f (restrict x (I \<union> J))) \<in> borel_measurable IJ.P"
+    by (rule measurable_cong[THEN iffD2, OF _ f_borel(1)])
+       (auto intro!: arg_cong[where f=f] simp: extensional_restrict)
+  then have f'_borel:
+    "(\<lambda>x. Real (?f x)) \<in> borel_measurable P.P"
+    "(\<lambda>x. Real (- ?f x)) \<in> borel_measurable P.P"
+    unfolding borel_measurable_merge_iff[OF IJ fin]
+    by simp_all
+  have PI:
+    "P.positive_integral (\<lambda>x. Real (?f x)) = IJ.positive_integral (\<lambda>x. Real (f x))"
+    "P.positive_integral (\<lambda>x. Real (- ?f x)) = IJ.positive_integral (\<lambda>x. Real (- f x))"
+    using f'_borel[THEN P.positive_integral_fst_measurable(2)]
+    using f_borel(2,3)[THEN product_positive_integral_fold[OF assms(1-3)]]
+    by simp_all
+  have "P.integrable ?f" using `IJ.integrable f`
+    unfolding P.integrable_def IJ.integrable_def
+    unfolding borel_measurable_merge_iff[OF IJ fin]
+    using f_restrict PI by simp_all
+  show ?thesis
+    unfolding P.integrable_fst_measurable(2)[OF `P.integrable ?f`, simplified]
+    unfolding IJ.integral_def P.integral_def
+    unfolding PI by simp
+qed
+
 section "Products on finite spaces"
 
 lemma sigma_sets_pair_algebra_finite: