# HG changeset patch
# User hoelzl
# Date 1291886537 -3600
# Node ID ababba14c965c5f98ec2b09fe9d6eff521702954
# Parent  1dc7652ce404e538f084499b3f6844729b41f113# Parent  a1abfa4e2b44b17abc703743244a8980244b91e2
merged

diff -r 1dc7652ce404 -r ababba14c965 src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Thu Dec 09 08:46:04 2010 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Thu Dec 09 10:22:17 2010 +0100
@@ -1347,6 +1347,16 @@
     by (auto intro!: measurable_If)
 qed
 
+lemma (in sigma_algebra) borel_measurable_pextreal_setsum[simp, intro]:
+  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> pextreal"
+  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 add: borel_measurable_const)
+
 lemma (in sigma_algebra) borel_measurable_pextreal_times[intro, simp]:
   fixes f :: "'a \<Rightarrow> pextreal" assumes "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
@@ -1359,15 +1369,14 @@
     by (auto intro!: measurable_If)
 qed
 
-lemma (in sigma_algebra) borel_measurable_pextreal_setsum[simp, intro]:
+lemma (in sigma_algebra) borel_measurable_pextreal_setprod[simp, intro]:
   fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> pextreal"
   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"
+  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 add: borel_measurable_const)
+  thus ?thesis using assms by induct auto
+qed simp
 
 lemma (in sigma_algebra) borel_measurable_pextreal_min[simp, intro]:
   fixes f g :: "'a \<Rightarrow> pextreal"
@@ -1386,7 +1395,7 @@
 lemma (in sigma_algebra) borel_measurable_SUP[simp, intro]:
   fixes f :: "'d\<Colon>countable \<Rightarrow> 'a \<Rightarrow> pextreal"
   assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
-  shows "(SUP i : A. f i) \<in> borel_measurable M" (is "?sup \<in> borel_measurable M")
+  shows "(\<lambda>x. SUP i : A. f i x) \<in> borel_measurable M" (is "?sup \<in> borel_measurable M")
   unfolding borel_measurable_pextreal_iff_greater
 proof safe
   fix a
@@ -1399,7 +1408,7 @@
 lemma (in sigma_algebra) borel_measurable_INF[simp, intro]:
   fixes f :: "'d :: countable \<Rightarrow> 'a \<Rightarrow> pextreal"
   assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
-  shows "(INF i : A. f i) \<in> borel_measurable M" (is "?inf \<in> borel_measurable M")
+  shows "(\<lambda>x. INF i : A. f i x) \<in> borel_measurable M" (is "?inf \<in> borel_measurable M")
   unfolding borel_measurable_pextreal_iff_less
 proof safe
   fix a
@@ -1423,20 +1432,10 @@
     using assms by auto
 qed
 
-lemma INFI_fun_expand:
-  "(INF y:A. f y) = (\<lambda>x. (INF y:A. f y x))"
-  by (simp add: fun_eq_iff INFI_apply)
-
-lemma SUPR_fun_expand:
-  "(SUP y:A. f y) = (\<lambda>x. (SUP y:A. f y x))"
-  by (simp add: fun_eq_iff SUPR_apply)
-
 lemma (in sigma_algebra) borel_measurable_psuminf[simp, intro]:
   assumes "\<And>i. f i \<in> borel_measurable M"
   shows "(\<lambda>x. (\<Sum>\<^isub>\<infinity> i. f i x)) \<in> borel_measurable M"
-  using assms unfolding psuminf_def
-  by (auto intro!: borel_measurable_SUP [unfolded SUPR_fun_expand])
-
+  using assms unfolding psuminf_def by auto
 
 section "LIMSEQ is borel measurable"
 
@@ -1459,13 +1458,12 @@
   note eq = this
   have *: "\<And>x. real (Real (u' x)) - real (Real (- u' x)) = u' x"
     by auto
-  have "(SUP n. INF m. (\<lambda>x. Real (u (n + m) x))) \<in> borel_measurable M"
-       "(SUP n. INF m. (\<lambda>x. Real (- u (n + m) x))) \<in> borel_measurable M"
-    using u by (auto intro: borel_measurable_SUP borel_measurable_INF borel_measurable_Real)
+  have "(\<lambda>x. SUP n. INF m. Real (u (n + m) x)) \<in> borel_measurable M"
+       "(\<lambda>x. SUP n. INF m. Real (- u (n + m) x)) \<in> borel_measurable M"
+    using u by auto
   with eq[THEN measurable_cong, of M "\<lambda>x. x" borel]
   have "(\<lambda>x. Real (u' x)) \<in> borel_measurable M"
-       "(\<lambda>x. Real (- u' x)) \<in> borel_measurable M"
-    unfolding SUPR_fun_expand INFI_fun_expand by auto
+       "(\<lambda>x. Real (- u' x)) \<in> borel_measurable M" by auto
   note this[THEN borel_measurable_real]
   from borel_measurable_diff[OF this]
   show ?thesis unfolding * .
diff -r 1dc7652ce404 -r ababba14c965 src/HOL/Probability/Complete_Measure.thy
--- a/src/HOL/Probability/Complete_Measure.thy	Thu Dec 09 08:46:04 2010 +0100
+++ b/src/HOL/Probability/Complete_Measure.thy	Thu Dec 09 10:22:17 2010 +0100
@@ -257,17 +257,14 @@
   show ?thesis
   proof (intro bexI)
     from AE[unfolded all_AE_countable]
-    show "AE x. g x = (SUP i. f' i) x" (is "AE x. g x = ?f x")
+    show "AE x. g x = (SUP i. f' i x)" (is "AE x. g x = ?f x")
     proof (rule AE_mp, safe intro!: AE_cong)
       fix x assume eq: "\<forall>i. f i x = f' i x"
-      have "g x = (SUP i. f i x)"
-        using `f \<up> g` unfolding isoton_def SUPR_fun_expand by auto
-      then show "g x = ?f x"
-        using eq unfolding SUPR_fun_expand by auto
+      moreover have "g = SUPR UNIV f" using `f \<up> g` unfolding isoton_def by simp
+      ultimately show "g x = ?f x" by (simp add: SUPR_apply)
     qed
     show "?f \<in> borel_measurable M"
-      using sf by (auto intro!: borel_measurable_SUP
-        intro: borel_measurable_simple_function)
+      using sf by (auto intro: borel_measurable_simple_function)
   qed
 qed
 
diff -r 1dc7652ce404 -r ababba14c965 src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Thu Dec 09 08:46:04 2010 +0100
+++ b/src/HOL/Probability/Information.thy	Thu Dec 09 10:22:17 2010 +0100
@@ -188,7 +188,7 @@
     using f by (rule \<nu>.measure_space_isomorphic)
 
   let ?RN = "sigma_finite_measure.RN_deriv ?M ?\<mu> ?\<nu>"
-  from RN_deriv_vimage[OF f \<nu>]
+  from RN_deriv_vimage[OF f[THEN bij_inv_the_inv_into] \<nu>]
   have *: "\<nu>.almost_everywhere (\<lambda>x. ?RN (the_inv_into S f x) = RN_deriv \<nu> x)"
     by (rule absolutely_continuous_AE[OF \<nu>])
 
diff -r 1dc7652ce404 -r ababba14c965 src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Thu Dec 09 08:46:04 2010 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Thu Dec 09 10:22:17 2010 +0100
@@ -1069,16 +1069,16 @@
 
 lemma (in measure_space) positive_integral_vimage_inv:
   fixes g :: "'d \<Rightarrow> pextreal" and f :: "'d \<Rightarrow> 'a"
-  assumes f: "bij_betw f S (space M)"
+  assumes f: "bij_inv S (space M) f h"
   shows "measure_space.positive_integral (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) g =
-      positive_integral (\<lambda>x. g (the_inv_into S f x))"
+      positive_integral (\<lambda>x. g (h x))"
 proof -
   interpret v: measure_space "vimage_algebra S f" "\<lambda>A. \<mu> (f ` A)"
-    using f by (rule measure_space_isomorphic)
+    using f by (rule measure_space_isomorphic[OF bij_inv_bij_betw(1)])
   show ?thesis
-    unfolding positive_integral_vimage[OF f, of "\<lambda>x. g (the_inv_into S f x)"]
-    using f[unfolded bij_betw_def]
-    by (auto intro!: v.positive_integral_cong simp: the_inv_into_f_f)
+    unfolding positive_integral_vimage[OF f[THEN bij_inv_bij_betw(1)], of "\<lambda>x. g (h x)"]
+    using f[unfolded bij_inv_def]
+    by (auto intro!: v.positive_integral_cong)
 qed
 
 lemma (in measure_space) positive_integral_SUP_approx:
@@ -1176,8 +1176,6 @@
     apply (rule positive_integral_mono)
     using `f \<up> u` unfolding isoton_def le_fun_def by auto
 next
-  have "u \<in> borel_measurable M"
-    using borel_measurable_SUP[of UNIV f] assms by (auto simp: isoton_def)
   have u: "u = (SUP i. f i)" using `f \<up> u` unfolding isoton_def by auto
 
   show "(SUP i. positive_integral (f i)) = positive_integral u"
@@ -1198,8 +1196,6 @@
   shows "(SUP i. positive_integral (f i)) = positive_integral (\<lambda>x. SUP i. f i x)"
     (is "_ = positive_integral ?u")
 proof -
-  have "?u \<in> borel_measurable M"
-    using borel_measurable_SUP[of _ f] assms by (simp add: SUPR_fun_expand)
   show ?thesis
   proof (rule antisym)
     show "(SUP j. positive_integral (f j)) \<le> positive_integral ?u"
@@ -1209,9 +1205,9 @@
     have "\<And>i. rf i \<in> borel_measurable M" unfolding rf_def
       using assms by (simp cong: measurable_cong)
     moreover have iso: "rf \<up> ru" using assms unfolding rf_def ru_def
-      unfolding isoton_def SUPR_fun_expand le_fun_def fun_eq_iff
+      unfolding isoton_def le_fun_def fun_eq_iff SUPR_apply
       using SUP_const[OF UNIV_not_empty]
-      by (auto simp: restrict_def le_fun_def SUPR_fun_expand fun_eq_iff)
+      by (auto simp: restrict_def le_fun_def fun_eq_iff)
     ultimately have "positive_integral ru \<le> (SUP i. positive_integral (rf i))"
       unfolding positive_integral_alt[of ru]
       by (auto simp: le_fun_def intro!: SUP_leI positive_integral_SUP_approx)
@@ -1283,6 +1279,11 @@
   shows "positive_integral (\<lambda>x. c * f x) = c * positive_integral f"
   using positive_integral_linear[OF assms, of "\<lambda>x. 0" c] by auto
 
+lemma (in measure_space) positive_integral_multc:
+  assumes "f \<in> borel_measurable M"
+  shows "positive_integral (\<lambda>x. f x * c) = positive_integral f * c"
+  unfolding mult_commute[of _ c] positive_integral_cmult[OF assms] by simp
+
 lemma (in measure_space) positive_integral_indicator[simp]:
   "A \<in> sets M \<Longrightarrow> positive_integral (\<lambda>x. indicator A x) = \<mu> A"
 by (subst positive_integral_eq_simple_integral) (auto simp: simple_function_indicator simple_integral_indicator)
@@ -1349,24 +1350,16 @@
 lemma (in measure_space) positive_integral_lim_INF:
   fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> pextreal"
   assumes "\<And>i. u i \<in> borel_measurable M"
-  shows "positive_integral (SUP n. INF m. u (m + n)) \<le>
+  shows "positive_integral (\<lambda>x. SUP n. INF m. u (m + n) x) \<le>
     (SUP n. INF m. positive_integral (u (m + n)))"
 proof -
-  have "(SUP n. INF m. u (m + n)) \<in> borel_measurable M"
-    by (auto intro!: borel_measurable_SUP borel_measurable_INF assms)
-
-  have "(\<lambda>n. INF m. u (m + n)) \<up> (SUP n. INF m. u (m + n))"
-  proof (unfold isoton_def, safe intro!: INF_mono bexI)
-    fix i m show "u (Suc m + i) \<le> u (m + Suc i)" by simp
-  qed simp
-  from positive_integral_isoton[OF this] assms
-  have "positive_integral (SUP n. INF m. u (m + n)) =
-    (SUP n. positive_integral (INF m. u (m + n)))"
-    unfolding isoton_def by (simp add: borel_measurable_INF)
+  have "positive_integral (\<lambda>x. SUP n. INF m. u (m + n) x)
+      = (SUP n. positive_integral (\<lambda>x. INF m. u (m + n) x))"
+    using assms
+    by (intro positive_integral_monotone_convergence_SUP[symmetric] INF_mono)
+       (auto simp del: add_Suc simp add: add_Suc[symmetric])
   also have "\<dots> \<le> (SUP n. INF m. positive_integral (u (m + n)))"
-    apply (rule SUP_mono)
-    apply (rule_tac x=n in bexI)
-    by (auto intro!: positive_integral_mono INFI_bound INF_leI exI simp: INFI_fun_expand)
+    by (auto intro!: SUP_mono bexI le_INFI positive_integral_mono INF_leI)
   finally show ?thesis .
 qed
 
@@ -1763,6 +1756,11 @@
   thus ?P ?I by auto
 qed
 
+lemma (in measure_space) integral_multc:
+  assumes "integrable f"
+  shows "integral (\<lambda>x. f x * c) = integral f * c"
+  unfolding mult_commute[of _ c] integral_cmult[OF assms] ..
+
 lemma (in measure_space) integral_mono_AE:
   assumes fg: "integrable f" "integrable g"
   and mono: "AE t. f t \<le> g t"
@@ -1950,10 +1948,10 @@
 
   have borel_f: "\<And>i. (\<lambda>x. Real (f i x)) \<in> borel_measurable M"
     using i unfolding integrable_def by auto
-  hence "(SUP i. (\<lambda>x. Real (f i x))) \<in> borel_measurable M"
+  hence "(\<lambda>x. SUP i. Real (f i x)) \<in> borel_measurable M"
     by auto
   hence borel_u: "u \<in> borel_measurable M"
-    using pos_u by (auto simp: borel_measurable_Real_eq SUPR_fun_expand SUP_F)
+    using pos_u by (auto simp: borel_measurable_Real_eq SUP_F)
 
   have integral_eq: "\<And>n. positive_integral (\<lambda>x. Real (f n x)) = Real (integral (f n))"
     using i unfolding integral_def integrable_def by (auto simp: Real_real)
@@ -2134,8 +2132,8 @@
     thus ?thesis by simp
   next
     assume neq_0: "positive_integral (\<lambda>x. Real (2 * w x)) \<noteq> 0"
-    have "positive_integral (\<lambda>x. Real (2 * w x)) = positive_integral (SUP n. INF m. (\<lambda>x. Real (?diff (m + n) x)))"
-    proof (rule positive_integral_cong, unfold SUPR_fun_expand INFI_fun_expand, subst add_commute)
+    have "positive_integral (\<lambda>x. Real (2 * w x)) = positive_integral (\<lambda>x. SUP n. INF m. Real (?diff (m + n) x))"
+    proof (rule positive_integral_cong, subst add_commute)
       fix x assume x: "x \<in> space M"
       show "Real (2 * w x) = (SUP n. INF m. Real (?diff (n + m) x))"
       proof (rule LIMSEQ_imp_lim_INF[symmetric])
diff -r 1dc7652ce404 -r ababba14c965 src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Thu Dec 09 08:46:04 2010 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Thu Dec 09 10:22:17 2010 +0100
@@ -552,10 +552,10 @@
 proof -
   from positive_integral_isoton[unfolded isoton_fun_expand isoton_iff_Lim_mono, of f u]
   show ?ilim using mono lim i by auto
-  have "(SUP i. f i) = u" using mono lim SUP_Lim_pextreal
-    unfolding fun_eq_iff SUPR_fun_expand mono_def by auto
-  moreover have "(SUP i. f i) \<in> borel_measurable M"
-    using i by (rule borel_measurable_SUP)
+  have "\<And>x. (SUP i. f i x) = u x" using mono lim SUP_Lim_pextreal
+    unfolding fun_eq_iff mono_def by auto
+  moreover have "(\<lambda>x. SUP i. f i x) \<in> borel_measurable M"
+    using i by auto
   ultimately show "u \<in> borel_measurable M" by simp
 qed
 
@@ -647,44 +647,20 @@
 definition p2e :: "(nat \<Rightarrow> real) \<Rightarrow> 'a::ordered_euclidean_space" where
   "p2e x = (\<chi>\<chi> i. x i)"
 
-lemma bij_euclidean_component:
-  "bij_betw (e2p::'a::ordered_euclidean_space \<Rightarrow> _) (UNIV :: 'a set)
-  ({..<DIM('a)} \<rightarrow>\<^isub>E (UNIV :: real set))"
-  unfolding bij_betw_def e2p_def_raw
-proof let ?e = "\<lambda>x.\<lambda>i\<in>{..<DIM('a::ordered_euclidean_space)}. (x::'a)$$i"
-  show "inj ?e" unfolding inj_on_def restrict_def apply(subst euclidean_eq) apply safe
-    apply(drule_tac x=i in fun_cong) by auto
-  { fix x::"nat \<Rightarrow> real" assume x:"\<forall>i. i \<notin> {..<DIM('a)} \<longrightarrow> x i = undefined"
-    hence "x = ?e (\<chi>\<chi> i. x i)" apply-apply(rule,case_tac "xa<DIM('a)") by auto
-    hence "x \<in> range ?e" by fastsimp
-  } thus "range ?e = ({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)}"
-    unfolding extensional_def using DIM_positive by auto
-qed
+lemma e2p_p2e[simp]:
+  "x \<in> extensional {..<DIM('a)} \<Longrightarrow> e2p (p2e x::'a::ordered_euclidean_space) = x"
+  by (auto simp: fun_eq_iff extensional_def p2e_def e2p_def)
 
-lemma bij_p2e:
-  "bij_betw (p2e::_ \<Rightarrow> 'a::ordered_euclidean_space) ({..<DIM('a)} \<rightarrow>\<^isub>E (UNIV :: real set))
-  (UNIV :: 'a set)" (is "bij_betw ?p ?U _")
-  unfolding bij_betw_def
-proof show "inj_on ?p ?U" unfolding inj_on_def p2e_def
-    apply(subst euclidean_eq) apply(safe,rule) unfolding extensional_def
-    apply(case_tac "xa<DIM('a)") by auto
-  { fix x::'a have "x \<in> ?p ` extensional {..<DIM('a)}"
-      unfolding image_iff apply(rule_tac x="\<lambda>i. if i<DIM('a) then x$$i else undefined" in bexI)
-      apply(subst euclidean_eq,safe) unfolding p2e_def extensional_def by auto
-  } thus "?p ` ?U = UNIV" by auto
-qed
+lemma p2e_e2p[simp]:
+  "p2e (e2p x) = (x::'a::ordered_euclidean_space)"
+  by (auto simp: euclidean_eq[where 'a='a] p2e_def e2p_def)
 
-lemma e2p_p2e[simp]: fixes z::"'a::ordered_euclidean_space"
-  assumes "x \<in> extensional {..<DIM('a)}"
-  shows "e2p (p2e x::'a) = x"
-proof fix i::nat
-  show "e2p (p2e x::'a) i = x i" unfolding e2p_def p2e_def restrict_def
-    using assms unfolding extensional_def by auto
-qed
-
-lemma p2e_e2p[simp]: fixes x::"'a::ordered_euclidean_space"
-  shows "p2e (e2p x) = x"
-  apply(subst euclidean_eq) unfolding e2p_def p2e_def restrict_def by auto
+lemma bij_inv_p2e_e2p:
+  shows "bij_inv ({..<DIM('a)} \<rightarrow>\<^isub>E UNIV) (UNIV :: 'a::ordered_euclidean_space set)
+     p2e e2p" (is "bij_inv ?P ?U _ _")
+proof (rule bij_invI)
+  show "p2e \<in> ?P \<rightarrow> ?U" "e2p \<in> ?U \<rightarrow> ?P" by (auto simp: e2p_def)
+qed auto
 
 interpretation borel_product: product_sigma_finite "\<lambda>x. borel::real algebra" "\<lambda>x. lmeasure"
   by default
@@ -692,71 +668,80 @@
 lemma cube_subset_Suc[intro]: "cube n \<subseteq> cube (Suc n)"
   unfolding cube_def_raw subset_eq apply safe unfolding mem_interval by auto
 
-lemma borel_vimage_algebra_eq:
-  "sigma_algebra.vimage_algebra
-         (borel :: ('a::ordered_euclidean_space) algebra) ({..<DIM('a)} \<rightarrow>\<^isub>E UNIV) p2e =
-  sigma (product_algebra (\<lambda>x. \<lparr> space = UNIV::real set, sets = range (\<lambda>a. {..<a}) \<rparr>) {..<DIM('a)} )"
-proof- note bor = borel_eq_lessThan
-  def F \<equiv> "product_algebra (\<lambda>x. \<lparr> space = UNIV::real set, sets = range (\<lambda>a. {..<a}) \<rparr>) {..<DIM('a)}"
-  def E \<equiv> "\<lparr>space = (UNIV::'a set), sets = range lessThan\<rparr>"
-  have *:"(({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)}) = space F" unfolding F_def by auto
-  show ?thesis unfolding F_def[symmetric] * bor
-  proof(rule vimage_algebra_sigma,unfold E_def[symmetric])
-    show "sets E \<subseteq> Pow (space E)" "p2e \<in> space F \<rightarrow> space E" unfolding E_def by auto
-  next fix A assume "A \<in> sets F"
-    hence A:"A \<in> (Pi\<^isub>E {..<DIM('a)}) ` ({..<DIM('a)} \<rightarrow> range lessThan)"
-      unfolding F_def product_algebra_def algebra.simps .
-    then guess B unfolding image_iff .. note B=this
-    hence "\<forall>x<DIM('a). B x \<in> range lessThan" by auto
-    hence "\<forall>x. \<exists>xa. x<DIM('a) \<longrightarrow> B x = {..<xa}" unfolding image_iff by auto
-    from choice[OF this] guess b .. note b=this
-    hence b':"\<forall>i<DIM('a). Sup (B i) = b i" using Sup_lessThan by auto
+lemma Pi_iff: "f \<in> Pi I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i)"
+  unfolding Pi_def by auto
 
-    show "A \<in> (\<lambda>X. p2e -` X \<inter> space F) ` sets E" unfolding image_iff B
-    proof(rule_tac x="{..< \<chi>\<chi> i. Sup (B i)}" in bexI)
-      show "Pi\<^isub>E {..<DIM('a)} B = p2e -` {..<(\<chi>\<chi> i. Sup (B i))::'a} \<inter> space F"
-        unfolding F_def E_def product_algebra_def algebra.simps
-      proof(rule,unfold subset_eq,rule_tac[!] ballI)
-        fix x assume "x \<in> Pi\<^isub>E {..<DIM('a)} B"
-        hence *:"\<forall>i<DIM('a). x i < b i" "\<forall>i\<ge>DIM('a). x i = undefined"
-          unfolding Pi_def extensional_def using b by auto
-        have "(p2e x::'a) < (\<chi>\<chi> i. Sup (B i))" unfolding less_prod_def eucl_less[of "p2e x"]
-          apply safe unfolding euclidean_lambda_beta b'[rule_format] p2e_def using * by auto
-        moreover have "x \<in> extensional {..<DIM('a)}"
-          using *(2) unfolding extensional_def by auto
-        ultimately show "x \<in> p2e -` {..<(\<chi>\<chi> i. Sup (B i)) ::'a} \<inter>
-          (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})" by auto
-      next fix x assume as:"x \<in> p2e -` {..<(\<chi>\<chi> i. Sup (B i))::'a} \<inter>
-          (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})"
-        hence "p2e x < ((\<chi>\<chi> i. Sup (B i))::'a)" by auto
-        hence "\<forall>i<DIM('a). x i \<in> B i" apply-apply(subst(asm) eucl_less)
-          unfolding p2e_def using b b' by auto
-        thus "x \<in> Pi\<^isub>E {..<DIM('a)} B" using as unfolding Pi_def extensional_def by auto
-      qed
-      show "{..<(\<chi>\<chi> i. Sup (B i))::'a} \<in> sets E" unfolding E_def algebra.simps by auto
-    qed
-  next fix A assume "A \<in> sets E"
-    then guess a unfolding E_def algebra.simps image_iff .. note a = this(2)
-    def B \<equiv> "\<lambda>i. {..<a $$ i}"
-    show "p2e -` A \<inter> space F \<in> sets F" unfolding F_def
-      unfolding product_algebra_def algebra.simps image_iff
-      apply(rule_tac x=B in bexI) apply rule unfolding subset_eq apply(rule_tac[1-2] ballI)
-    proof- show "B \<in> {..<DIM('a)} \<rightarrow> range lessThan" unfolding B_def by auto
-      fix x assume as:"x \<in> p2e -` A \<inter> (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})"
-      hence "p2e x \<in> A" by auto
-      hence "\<forall>i<DIM('a). x i \<in> B i" unfolding B_def a lessThan_iff
-        apply-apply(subst (asm) eucl_less) unfolding p2e_def by auto
-      thus "x \<in> Pi\<^isub>E {..<DIM('a)} B" using as unfolding Pi_def extensional_def by auto
-    next fix x assume x:"x \<in> Pi\<^isub>E {..<DIM('a)} B"
-      moreover have "p2e x \<in> A" unfolding a lessThan_iff p2e_def apply(subst eucl_less)
-        using x unfolding Pi_def extensional_def B_def by auto
-      ultimately show "x \<in> p2e -` A \<inter> (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})" by auto
-    qed
-  qed
+lemma measurable_e2p_on_generator:
+  "e2p \<in> measurable \<lparr> space = UNIV::'a set, sets = range lessThan \<rparr>
+  (product_algebra
+    (\<lambda>x. \<lparr> space = UNIV::real set, sets = range lessThan \<rparr>)
+    {..<DIM('a::ordered_euclidean_space)})"
+  (is "e2p \<in> measurable ?E ?P")
+proof (unfold measurable_def, intro CollectI conjI ballI)
+  show "e2p \<in> space ?E \<rightarrow> space ?P" by (auto simp: e2p_def)
+  fix A assume "A \<in> sets ?P"
+  then obtain E where A: "A = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. E i)"
+    and "E \<in> {..<DIM('a)} \<rightarrow> (range lessThan)"
+    by (auto elim!: product_algebraE)
+  then have "\<forall>i\<in>{..<DIM('a)}. \<exists>xs. E i = {..< xs}" by auto
+  from this[THEN bchoice] guess xs ..
+  then have A_eq: "A = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {..< xs i})"
+    using A by auto
+  have "e2p -` A = {..< (\<chi>\<chi> i. xs i) :: 'a}"
+    using DIM_positive by (auto simp add: Pi_iff set_eq_iff e2p_def A_eq
+      euclidean_eq[where 'a='a] eucl_less[where 'a='a])
+  then show "e2p -` A \<inter> space ?E \<in> sets ?E" by simp
 qed
 
+lemma measurable_p2e_on_generator:
+  "p2e \<in> measurable
+    (product_algebra
+      (\<lambda>x. \<lparr> space = UNIV::real set, sets = range lessThan \<rparr>)
+      {..<DIM('a::ordered_euclidean_space)})
+    \<lparr> space = UNIV::'a set, sets = range lessThan \<rparr>"
+  (is "p2e \<in> measurable ?P ?E")
+proof (unfold measurable_def, intro CollectI conjI ballI)
+  show "p2e \<in> space ?P \<rightarrow> space ?E" by simp
+  fix A assume "A \<in> sets ?E"
+  then obtain x where "A = {..<x}" by auto
+  then have "p2e -` A \<inter> space ?P = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {..< x $$ i})"
+    using DIM_positive
+    by (auto simp: Pi_iff set_eq_iff p2e_def
+                   euclidean_eq[where 'a='a] eucl_less[where 'a='a])
+  then show "p2e -` A \<inter> space ?P \<in> sets ?P" by auto
+qed
+
+lemma borel_vimage_algebra_eq:
+  defines "F \<equiv> product_algebra (\<lambda>x. \<lparr> space = (UNIV::real set), sets = range lessThan \<rparr>) {..<DIM('a::ordered_euclidean_space)}"
+  shows "sigma_algebra.vimage_algebra (borel::'a::ordered_euclidean_space algebra) (space (sigma F)) p2e = sigma F"
+  unfolding borel_eq_lessThan
+proof (intro vimage_algebra_sigma)
+  let ?E = "\<lparr>space = (UNIV::'a set), sets = range lessThan\<rparr>"
+  show "bij_inv (space (sigma F)) (space (sigma ?E)) p2e e2p"
+    using bij_inv_p2e_e2p unfolding F_def by simp
+  show "sets F \<subseteq> Pow (space F)" "sets ?E \<subseteq> Pow (space ?E)" unfolding F_def
+    by (intro product_algebra_sets_into_space) auto
+  show "p2e \<in> measurable F ?E"
+    "e2p \<in> measurable ?E F"
+    unfolding F_def using measurable_p2e_on_generator measurable_e2p_on_generator by auto
+qed
+
+lemma product_borel_eq_vimage:
+  "sigma (product_algebra (\<lambda>x. borel) {..<DIM('a::ordered_euclidean_space)}) =
+  sigma_algebra.vimage_algebra borel (extensional {..<DIM('a)})
+  (p2e:: _ \<Rightarrow> 'a::ordered_euclidean_space)"
+  unfolding borel_vimage_algebra_eq[simplified]
+  unfolding borel_eq_lessThan
+  apply(subst sigma_product_algebra_sigma_eq[where S="\<lambda>i. \<lambda>n. lessThan (real n)"])
+  unfolding lessThan_iff
+proof- fix i assume i:"i<DIM('a)"
+  show "(\<lambda>n. {..<real n}) \<up> space \<lparr>space = UNIV, sets = range lessThan\<rparr>"
+    by(auto intro!:real_arch_lt isotoneI)
+qed auto
+
 lemma e2p_Int:"e2p ` A \<inter> e2p ` B = e2p ` (A \<inter> B)" (is "?L = ?R")
-  apply(rule image_Int[THEN sym]) using bij_euclidean_component
+  apply(rule image_Int[THEN sym])
+  using bij_inv_p2e_e2p[THEN bij_inv_bij_betw(2)]
   unfolding bij_betw_def by auto
 
 lemma Int_stable_cuboids: fixes x::"'a::ordered_euclidean_space"
@@ -775,18 +760,6 @@
   unfolding Int_stable_def algebra.select_convs
   apply safe unfolding inter_interval by auto
 
-lemma product_borel_eq_vimage:
-  "sigma (product_algebra (\<lambda>x. borel) {..<DIM('a::ordered_euclidean_space)}) =
-  sigma_algebra.vimage_algebra borel (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})
-  (p2e:: _ \<Rightarrow> 'a::ordered_euclidean_space)"
-  unfolding borel_vimage_algebra_eq unfolding borel_eq_lessThan
-  apply(subst sigma_product_algebra_sigma_eq[where S="\<lambda>i. \<lambda>n. lessThan (real n)"])
-  unfolding lessThan_iff
-proof- fix i assume i:"i<DIM('a)"
-  show "(\<lambda>n. {..<real n}) \<up> space \<lparr>space = UNIV, sets = range lessThan\<rparr>"
-    by(auto intro!:real_arch_lt isotoneI)
-qed auto
-
 lemma inj_on_disjoint_family_on: assumes "disjoint_family_on A S" "inj f"
   shows "disjoint_family_on (\<lambda>x. f ` A x) S"
   unfolding disjoint_family_on_def
@@ -808,12 +781,12 @@
   unfolding e2p_def by auto
 
 lemma e2p_image_vimage: fixes A::"'a::ordered_euclidean_space set"
-  shows "e2p ` A = p2e -` A \<inter> (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})"
+  shows "e2p ` A = p2e -` A \<inter> extensional {..<DIM('a)}"
 proof(rule set_eqI,rule)
   fix x assume "x \<in> e2p ` A" then guess y unfolding image_iff .. note y=this
-  show "x \<in> p2e -` A \<inter> (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})"
+  show "x \<in> p2e -` A \<inter> extensional {..<DIM('a)}"
     apply safe apply(rule vimageI[OF _ y(1)]) unfolding y p2e_e2p by auto
-next fix x assume "x \<in> p2e -` A \<inter> (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})"
+next fix x assume "x \<in> p2e -` A \<inter> extensional {..<DIM('a)}"
   thus "x \<in> e2p ` A" unfolding image_iff apply(rule_tac x="p2e x" in bexI) apply(subst e2p_p2e) by auto
 qed
 
@@ -879,17 +852,15 @@
       qed
 
       show "disjoint_family (\<lambda>n. e2p ` A n)" apply(rule inj_on_disjoint_family_on)
-        using bij_euclidean_component using A(2) unfolding bij_betw_def by auto
+        using bij_inv_p2e_e2p[THEN bij_inv_bij_betw(2)] using A(2) unfolding bij_betw_def by auto
       show "(\<Union>n. e2p ` A n) \<in> sets (sigma (product_algebra (\<lambda>x. borel) {..<DIM('a)}))"
         unfolding product_borel_eq_vimage borel.in_vimage_algebra
       proof(rule bexI[OF _ A(3)],rule set_eqI,rule)
         fix x assume x:"x \<in> (\<Union>n. e2p ` A n)" hence "p2e x \<in> (\<Union>i. A i)" by auto
         moreover have "x \<in> extensional {..<DIM('a)}"
           using x unfolding extensional_def e2p_def_raw by auto
-        ultimately show "x \<in> p2e -` (\<Union>i. A i) \<inter> (({..<DIM('a)} \<rightarrow> UNIV) \<inter>
-          extensional {..<DIM('a)})" by auto
-      next fix x assume x:"x \<in> p2e -` (\<Union>i. A i) \<inter> (({..<DIM('a)} \<rightarrow> UNIV) \<inter>
-          extensional {..<DIM('a)})"
+        ultimately show "x \<in> p2e -` (\<Union>i. A i) \<inter> extensional {..<DIM('a)}" by auto
+      next fix x assume x:"x \<in> p2e -` (\<Union>i. A i) \<inter> extensional {..<DIM('a)}"
         hence "p2e x \<in> (\<Union>i. A i)" by auto
         hence "\<exists>n. x \<in> e2p ` A n" apply safe apply(rule_tac x=i in exI)
           unfolding image_iff apply(rule_tac x="p2e x" in bexI)
@@ -925,23 +896,20 @@
   assumes f: "f \<in> borel_measurable borel"
   shows "borel.positive_integral f =
           borel_product.product_positive_integral {..<DIM('a)} (f \<circ> p2e)"
-proof- def U \<equiv> "(({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)}):: (nat \<Rightarrow> real) set"
+proof- def U \<equiv> "extensional {..<DIM('a)} :: (nat \<Rightarrow> real) set"
   interpret fprod: finite_product_sigma_finite "\<lambda>x. borel" "\<lambda>x. lmeasure" "{..<DIM('a)}" by default auto
-  have "\<And>x. \<exists>i::nat. x < real i" by (metis real_arch_lt)
-  hence "(\<lambda>n::nat. {..<real n}) \<up> UNIV" apply-apply(rule isotoneI) by auto
-  hence *:"sigma_algebra.vimage_algebra borel U (p2e:: _ \<Rightarrow> 'a)
+  have *:"sigma_algebra.vimage_algebra borel U (p2e:: _ \<Rightarrow> 'a)
     = sigma (product_algebra (\<lambda>x. borel) {..<DIM('a)})"
-    unfolding U_def apply-apply(subst borel_vimage_algebra_eq)
-    apply(subst sigma_product_algebra_sigma_eq[where S="\<lambda>x. \<lambda>n. {..<(\<chi>\<chi> i. real n)}", THEN sym])
-    unfolding borel_eq_lessThan[THEN sym] by auto
-  show ?thesis unfolding borel.positive_integral_vimage[unfolded space_borel,OF bij_p2e]
+    unfolding U_def product_borel_eq_vimage[symmetric] ..
+  show ?thesis
+    unfolding borel.positive_integral_vimage[unfolded space_borel, OF bij_inv_p2e_e2p[THEN bij_inv_bij_betw(1)]]
     apply(subst fprod.positive_integral_cong_measure[THEN sym, of "\<lambda>A. lmeasure (p2e ` A)"])
     unfolding U_def[symmetric] *[THEN sym] o_def
   proof- fix A assume A:"A \<in> sets (sigma_algebra.vimage_algebra borel U (p2e ::_ \<Rightarrow> 'a))"
     hence *:"A \<subseteq> extensional {..<DIM('a)}" unfolding U_def by auto
-    from A guess B unfolding borel.in_vimage_algebra U_def .. note B=this
-    have "(p2e ` A::'a set) \<in> sets borel" unfolding B apply(subst Int_left_commute)
-      apply(subst Int_absorb1) unfolding p2e_inv_extensional[of B,THEN sym] using B(1) by auto
+    from A guess B unfolding borel.in_vimage_algebra U_def ..
+    then have "(p2e ` A::'a set) \<in> sets borel"
+      by (simp add: p2e_inv_extensional[of B, symmetric])
     from lmeasure_measure_eq_borel_prod[OF this] show "lmeasure (p2e ` A::'a set) =
       finite_product_sigma_finite.measure (\<lambda>x. borel) (\<lambda>x. lmeasure) {..<DIM('a)} A"
       unfolding e2p_p2e'[OF *] .
diff -r 1dc7652ce404 -r ababba14c965 src/HOL/Probability/Positive_Extended_Real.thy
--- a/src/HOL/Probability/Positive_Extended_Real.thy	Thu Dec 09 08:46:04 2010 +0100
+++ b/src/HOL/Probability/Positive_Extended_Real.thy	Thu Dec 09 10:22:17 2010 +0100
@@ -260,6 +260,9 @@
 qed
 end
 
+lemma Real_minus_abs[simp]: "Real (- \<bar>x\<bar>) = 0"
+  by simp
+
 lemma pextreal_plus_eq_\<omega>[simp]: "(a :: pextreal) + b = \<omega> \<longleftrightarrow> a = \<omega> \<or> b = \<omega>"
   by (cases a, cases b) auto
 
diff -r 1dc7652ce404 -r ababba14c965 src/HOL/Probability/Probability_Space.thy
--- a/src/HOL/Probability/Probability_Space.thy	Thu Dec 09 08:46:04 2010 +0100
+++ b/src/HOL/Probability/Probability_Space.thy	Thu Dec 09 10:22:17 2010 +0100
@@ -352,7 +352,7 @@
   show "sigma_algebra (sigma (pair_algebra MX MY))" by default
   have sa: "sigma_algebra M" by default
   show "(\<lambda>x. (X x, Y x)) \<in> measurable M (sigma (pair_algebra MX MY))"
-    unfolding P.measurable_pair[OF sa] using assms by (simp add: comp_def)
+    unfolding P.measurable_pair_iff[OF sa] using assms by (simp add: comp_def)
 qed
 
 lemma (in prob_space) distribution_order:
@@ -410,8 +410,9 @@
       assume A: "range A \<subseteq> sets XY.P" and df: "disjoint_family A"
       have "(\<Sum>\<^isub>\<infinity>n. \<mu> (?X (A n))) = \<mu> (\<Union>x. ?X (A x))"
       proof (intro measure_countably_additive)
-        from assms have *: "(\<lambda>x. (X x, Y x)) \<in> measurable M XY.P"
-          by (intro XY.measurable_prod_sigma) (simp_all add: comp_def, default)
+        have "sigma_algebra M" by default
+        then have *: "(\<lambda>x. (X x, Y x)) \<in> measurable M XY.P"
+          using assms by (simp add: XY.measurable_pair comp_def)
         show "range (\<lambda>n. ?X (A n)) \<subseteq> events"
           using measurable_sets[OF *] A by auto
         show "disjoint_family (\<lambda>n. ?X (A n))"
@@ -503,7 +504,7 @@
   show "finite_sigma_algebra (sigma (pair_algebra MX MY))" by default
   have sa: "sigma_algebra M" by default
   show "(\<lambda>x. (X x, Y x)) \<in> measurable M (sigma (pair_algebra MX MY))"
-    unfolding P.measurable_pair[OF sa] using assms by (simp add: comp_def)
+    unfolding P.measurable_pair_iff[OF sa] using assms by (simp add: comp_def)
 qed
 
 lemma (in prob_space) finite_random_variable_imp_sets:
@@ -640,7 +641,7 @@
   proof
     fix x assume "x \<in> space XY.P"
     moreover have "(\<lambda>x. (X x, Y x)) \<in> measurable M XY.P"
-      using X Y by (subst XY.measurable_pair) (simp_all add: o_def, default)
+      using X Y by (intro XY.measurable_pair) (simp_all add: o_def, default)
     ultimately have "(\<lambda>x. (X x, Y x)) -` {x} \<inter> space M \<in> sets M"
       unfolding measurable_def by simp
     then show "joint_distribution X Y {x} \<noteq> \<omega>"
@@ -1068,13 +1069,13 @@
 
   show "\<exists>g\<in>borel_measurable M'. \<forall>x\<in>space M. Z x = g (Y x)"
   proof (intro ballI bexI)
-    show "(SUP i. g i) \<in> borel_measurable M'"
+    show "(\<lambda>x. SUP i. g i x) \<in> borel_measurable M'"
       using g by (auto intro: M'.borel_measurable_simple_function)
     fix x assume "x \<in> space M"
     have "Z x = (SUP i. f i) x" using `f \<up> Z` unfolding isoton_def by simp
-    also have "\<dots> = (SUP i. g i) (Y x)" unfolding SUPR_fun_expand
+    also have "\<dots> = (SUP i. g i (Y x))" unfolding SUPR_apply
       using g `x \<in> space M` by simp
-    finally show "Z x = (SUP i. g i) (Y x)" .
+    finally show "Z x = (SUP i. g i (Y x))" .
   qed
 qed
 
diff -r 1dc7652ce404 -r ababba14c965 src/HOL/Probability/Product_Measure.thy
--- a/src/HOL/Probability/Product_Measure.thy	Thu Dec 09 08:46:04 2010 +0100
+++ b/src/HOL/Probability/Product_Measure.thy	Thu Dec 09 10:22:17 2010 +0100
@@ -92,6 +92,12 @@
   shows "a \<in> extensional (insert i I)"
   using assms unfolding extensional_def by auto
 
+lemma merge_singleton[simp]: "i \<notin> I \<Longrightarrow> merge I x {i} y = restrict (x(i := y i)) (insert i I)"
+  unfolding merge_def by (auto simp: fun_eq_iff)
+
+lemma Pi_Int: "Pi I E \<inter> Pi I F = (\<Pi> i\<in>I. E i \<inter> F i)"
+  by auto
+
 lemma PiE_Int: "(Pi\<^isub>E I A) \<inter> (Pi\<^isub>E I B) = Pi\<^isub>E I (\<lambda>x. A x \<inter> B x)"
   by auto
 
@@ -107,6 +113,64 @@
 lemma Pi_cancel_fupd[simp]: "i \<notin> I \<Longrightarrow> x(i := a) \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
   by (auto simp: Pi_def)
 
+lemma restrict_vimage:
+  assumes "I \<inter> J = {}"
+  shows "(\<lambda>x. (restrict x I, restrict x J)) -` (Pi\<^isub>E I E \<times> Pi\<^isub>E J F) = Pi (I \<union> J) (merge I E J F)"
+  using assms by (auto simp: restrict_Pi_cancel)
+
+lemma merge_vimage:
+  assumes "I \<inter> J = {}"
+  shows "(\<lambda>(x,y). merge I x J y) -` Pi\<^isub>E (I \<union> J) E = Pi I E \<times> Pi J E"
+  using assms by (auto simp: restrict_Pi_cancel)
+
+lemma restrict_fupd[simp]: "i \<notin> I \<Longrightarrow> restrict (f (i := x)) I = restrict f I"
+  by (auto simp: restrict_def intro!: ext)
+
+lemma merge_restrict[simp]:
+  "merge I (restrict x I) J y = merge I x J y"
+  "merge I x J (restrict y J) = merge I x J y"
+  unfolding merge_def by (auto intro!: ext)
+
+lemma merge_x_x_eq_restrict[simp]:
+  "merge I x J x = restrict x (I \<union> J)"
+  unfolding merge_def by (auto intro!: ext)
+
+lemma Pi_fupd_iff: "i \<in> I \<Longrightarrow> f \<in> Pi I (B(i := A)) \<longleftrightarrow> f \<in> Pi (I - {i}) B \<and> f i \<in> A"
+  apply auto
+  apply (drule_tac x=x in Pi_mem)
+  apply (simp_all split: split_if_asm)
+  apply (drule_tac x=i in Pi_mem)
+  apply (auto dest!: Pi_mem)
+  done
+
+lemma Pi_UN:
+  fixes A :: "nat \<Rightarrow> 'i \<Rightarrow> 'a set"
+  assumes "finite I" and mono: "\<And>i n m. i \<in> I \<Longrightarrow> n \<le> m \<Longrightarrow> A n i \<subseteq> A m i"
+  shows "(\<Union>n. Pi I (A n)) = (\<Pi> i\<in>I. \<Union>n. A n i)"
+proof (intro set_eqI iffI)
+  fix f assume "f \<in> (\<Pi> i\<in>I. \<Union>n. A n i)"
+  then have "\<forall>i\<in>I. \<exists>n. f i \<in> A n i" by auto
+  from bchoice[OF this] obtain n where n: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> (A (n i) i)" by auto
+  obtain k where k: "\<And>i. i \<in> I \<Longrightarrow> n i \<le> k"
+    using `finite I` finite_nat_set_iff_bounded_le[of "n`I"] by auto
+  have "f \<in> Pi I (A k)"
+  proof (intro Pi_I)
+    fix i assume "i \<in> I"
+    from mono[OF this, of "n i" k] k[OF this] n[OF this]
+    show "f i \<in> A k i" by auto
+  qed
+  then show "f \<in> (\<Union>n. Pi I (A n))" by auto
+qed auto
+
+lemma PiE_cong:
+  assumes "\<And>i. i\<in>I \<Longrightarrow> A i = B i"
+  shows "Pi\<^isub>E I A = Pi\<^isub>E I B"
+  using assms by (auto intro!: Pi_cong)
+
+lemma restrict_upd[simp]:
+  "i \<notin> I \<Longrightarrow> (restrict f I)(i := y) = restrict (f(i := y)) (insert i I)"
+  by (auto simp: fun_eq_iff)
+
 section "Binary products"
 
 definition
@@ -134,6 +198,14 @@
   "space (pair_algebra A B) = space A \<times> space B"
   by (simp add: pair_algebra_def)
 
+lemma sets_pair_algebra: "sets (pair_algebra N M) = (\<lambda>(x, y). x \<times> y) ` (sets N \<times> sets M)"
+  unfolding pair_algebra_def by auto
+
+lemma pair_algebra_sets_into_space:
+  assumes "sets M \<subseteq> Pow (space M)" "sets N \<subseteq> Pow (space N)"
+  shows "sets (pair_algebra M N) \<subseteq> Pow (space (pair_algebra M N))"
+  using assms by (auto simp: pair_algebra_def)
+
 lemma pair_algebra_Int_snd:
   assumes "sets S1 \<subseteq> Pow (space S1)"
   shows "pair_algebra S1 (algebra.restricted_space S2 A) =
@@ -176,7 +248,7 @@
   then show ?fst ?snd by auto
 qed
 
-lemma (in pair_sigma_algebra) measurable_pair:
+lemma (in pair_sigma_algebra) measurable_pair_iff:
   assumes "sigma_algebra M"
   shows "f \<in> measurable M P \<longleftrightarrow>
     (fst \<circ> f) \<in> measurable M M1 \<and> (snd \<circ> f) \<in> measurable M M2"
@@ -205,42 +277,11 @@
   qed
 qed
 
-lemma (in pair_sigma_algebra) measurable_prod_sigma:
+lemma (in pair_sigma_algebra) measurable_pair:
   assumes "sigma_algebra M"
-  assumes 1: "(fst \<circ> f) \<in> measurable M M1" and 2: "(snd \<circ> f) \<in> measurable M M2"
+  assumes "(fst \<circ> f) \<in> measurable M M1" "(snd \<circ> f) \<in> measurable M M2"
   shows "f \<in> measurable M P"
-proof -
-  interpret M: sigma_algebra M by fact
-  from 1 have fn1: "fst \<circ> f \<in> space M \<rightarrow> space M1"
-     and q1: "\<forall>y\<in>sets M1. (fst \<circ> f) -` y \<inter> space M \<in> sets M"
-    by (auto simp add: measurable_def)
-  from 2 have fn2: "snd \<circ> f \<in> space M \<rightarrow> space M2"
-     and q2: "\<forall>y\<in>sets M2. (snd \<circ> f) -` y \<inter> space M \<in> sets M"
-    by (auto simp add: measurable_def)
-  show ?thesis
-  proof (rule M.measurable_sigma)
-    show "sets E \<subseteq> Pow (space E)"
-      using M1.space_closed M2.space_closed
-      by (auto simp add: sigma_algebra_iff pair_algebra_def)
-  next
-    show "f \<in> space M \<rightarrow> space E"
-      by (simp add: space_pair_algebra) (rule prod_final [OF fn1 fn2])
-  next
-    fix z
-    assume z: "z \<in> sets E"
-    thus "f -` z \<inter> space M \<in> sets M"
-    proof (auto simp add: pair_algebra_def vimage_Times)
-      fix x y
-      assume x: "x \<in> sets M1" and y: "y \<in> sets M2"
-      have "(fst \<circ> f) -` x \<inter> (snd \<circ> f) -` y \<inter> space M =
-            ((fst \<circ> f) -` x \<inter> space M) \<inter> ((snd \<circ> f) -` y \<inter> space M)"
-        by blast
-      also have "...  \<in> sets M" using x y q1 q2
-        by blast
-      finally show "(fst \<circ> f) -` x \<inter> (snd \<circ> f) -` y \<inter> space M \<in> sets M" .
-    qed
-  qed
-qed
+  unfolding measurable_pair_iff[OF assms(1)] using assms(2,3) by simp
 
 lemma pair_algebraE:
   assumes "X \<in> sets (pair_algebra M1 M2)"
@@ -726,11 +767,11 @@
   then have F_borel: "\<And>i. F i \<in> borel_measurable P"
     and F_mono: "\<And>i x. F i x \<le> F (Suc i) x"
     and F_SUPR: "\<And>x. (SUP i. F i x) = f x"
-    unfolding isoton_def le_fun_def SUPR_fun_expand
+    unfolding isoton_fun_expand unfolding isoton_def le_fun_def
     by (auto intro: borel_measurable_simple_function)
   note sf = simple_function_cut[OF F(1)]
-  then have "(SUP i. ?C (F i)) \<in> borel_measurable M1"
-    using F(1) by (auto intro!: M1.borel_measurable_SUP)
+  then have "(\<lambda>x. SUP i. ?C (F i) x) \<in> borel_measurable M1"
+    using F(1) by auto
   moreover
   { fix x assume "x \<in> space M1"
     have isotone: "(\<lambda> i y. F i (x, y)) \<up> (\<lambda>y. f (x, y))"
@@ -742,7 +783,7 @@
       by (simp add: isoton_def) }
   note SUPR_C = this
   ultimately show "?C f \<in> borel_measurable M1"
-    unfolding SUPR_fun_expand by (simp cong: measurable_cong)
+    by (simp cong: measurable_cong)
   have "positive_integral (\<lambda>x. SUP i. F i x) = (SUP i. positive_integral (F i))"
     using F_borel F_mono
     by (auto intro!: positive_integral_monotone_convergence_SUP[symmetric])
@@ -1003,10 +1044,25 @@
 sublocale finite_product_sigma_algebra \<subseteq> sigma_algebra P
   using product_algebra_into_space by (rule sigma_algebra_sigma)
 
+lemma product_algebraE:
+  assumes "A \<in> sets (product_algebra M I)"
+  obtains E where "A = Pi\<^isub>E I E" "E \<in> (\<Pi> i\<in>I. sets (M i))"
+  using assms unfolding product_algebra_def by auto
+
+lemma product_algebraI[intro]:
+  assumes "E \<in> (\<Pi> i\<in>I. sets (M i))"
+  shows "Pi\<^isub>E I E \<in> sets (product_algebra M I)"
+  using assms unfolding product_algebra_def by auto
+
 lemma space_product_algebra[simp]:
   "space (product_algebra M I) = Pi\<^isub>E I (\<lambda>i. space (M i))"
   unfolding product_algebra_def by simp
 
+lemma product_algebra_sets_into_space:
+  assumes "\<And>i. i\<in>I \<Longrightarrow> sets (M i) \<subseteq> Pow (space (M i))"
+  shows "sets (product_algebra M I) \<subseteq> Pow (space (product_algebra M I))"
+  using assms by (auto simp: product_algebra_def) blast
+
 lemma (in finite_product_sigma_algebra) P_empty:
   "I = {} \<Longrightarrow> P = \<lparr> space = {\<lambda>k. undefined}, sets = { {}, {\<lambda>k. undefined} }\<rparr>"
   unfolding product_algebra_def by (simp add: sigma_def image_constant)
@@ -1015,34 +1071,122 @@
   "\<lbrakk> \<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i) \<rbrakk> \<Longrightarrow> Pi\<^isub>E I A \<in> sets P"
   by (auto simp: product_algebra_def sets_sigma intro!: sigma_sets.Basic)
 
-lemma bij_betw_prod_fold:
-  assumes "i \<notin> I"
-  shows "bij_betw (\<lambda>x. (x(i:=undefined), x i)) (\<Pi>\<^isub>E j\<in>insert i I. space (M j)) ((\<Pi>\<^isub>E j\<in>I. space (M j)) \<times> space (M i))"
-    (is "bij_betw ?f ?P ?F")
-    using `i \<notin> I`
-proof (unfold bij_betw_def, intro conjI set_eqI iffI)
-  show "inj_on ?f ?P"
-  proof (safe intro!: inj_onI ext)
-    fix a b x assume "a(i:=undefined) = b(i:=undefined)" "a i = b i"
-    then show "a x = b x"
-      by (cases "x = i") (auto simp: fun_eq_iff split: split_if_asm)
+lemma (in product_sigma_algebra) bij_inv_restrict_merge:
+  assumes [simp]: "I \<inter> J = {}"
+  shows "bij_inv
+    (space (sigma (product_algebra M (I \<union> J))))
+    (space (sigma (pair_algebra (product_algebra M I) (product_algebra M J))))
+    (\<lambda>x. (restrict x I, restrict x J)) (\<lambda>(x, y). merge I x J y)"
+  by (rule bij_invI) (auto simp: space_pair_algebra extensional_restrict)
+
+lemma (in product_sigma_algebra) bij_inv_singleton:
+  "bij_inv (space (sigma (product_algebra M {i}))) (space (M i))
+    (\<lambda>x. x i) (\<lambda>x. (\<lambda>j\<in>{i}. x))"
+  by (rule bij_invI) (auto simp: restrict_def extensional_def fun_eq_iff)
+
+lemma (in product_sigma_algebra) bij_inv_restrict_insert:
+  assumes [simp]: "i \<notin> I"
+  shows "bij_inv
+    (space (sigma (product_algebra M (insert i I))))
+    (space (sigma (pair_algebra (product_algebra M I) (M i))))
+    (\<lambda>x. (restrict x I, x i)) (\<lambda>(x, y). x(i := y))"
+  by (rule bij_invI) (auto simp: space_pair_algebra extensional_restrict)
+
+lemma (in product_sigma_algebra) measurable_restrict_on_generating:
+  assumes [simp]: "I \<inter> J = {}"
+  shows "(\<lambda>x. (restrict x I, restrict x J)) \<in> measurable
+    (product_algebra M (I \<union> J))
+    (pair_algebra (product_algebra M I) (product_algebra M J))"
+    (is "?R \<in> measurable ?IJ ?P")
+proof (unfold measurable_def, intro CollectI conjI ballI)
+  show "?R \<in> space ?IJ \<rightarrow> space ?P" by (auto simp: space_pair_algebra)
+  { fix F E assume "E \<in> (\<Pi> i\<in>I. sets (M i))" "F \<in> (\<Pi> i\<in>J. sets (M i))"
+    then have "Pi (I \<union> J) (merge I E J F) \<inter> (\<Pi>\<^isub>E i\<in>I \<union> J. space (M i)) =
+        Pi\<^isub>E (I \<union> J) (merge I E J F)"
+      using M.sets_into_space by auto blast+ }
+  note this[simp]
+  show "\<And>A. A \<in> sets ?P \<Longrightarrow> ?R -` A \<inter> space ?IJ \<in> sets ?IJ"
+    by (force elim!: pair_algebraE product_algebraE
+              simp del: vimage_Int simp: restrict_vimage merge_vimage space_pair_algebra)
+  qed
+
+lemma (in product_sigma_algebra) measurable_merge_on_generating:
+  assumes [simp]: "I \<inter> J = {}"
+  shows "(\<lambda>(x, y). merge I x J y) \<in> measurable
+    (pair_algebra (product_algebra M I) (product_algebra M J))
+    (product_algebra M (I \<union> J))"
+    (is "?M \<in> measurable ?P ?IJ")
+proof (unfold measurable_def, intro CollectI conjI ballI)
+  show "?M \<in> space ?P \<rightarrow> space ?IJ" by (auto simp: space_pair_algebra)
+  { fix E assume "E \<in> (\<Pi> i\<in>I. sets (M i))" "E \<in> (\<Pi> i\<in>J. sets (M i))"
+    then have "Pi I E \<times> Pi J E \<inter> (\<Pi>\<^isub>E i\<in>I. space (M i)) \<times> (\<Pi>\<^isub>E i\<in>J. space (M i)) =
+        Pi\<^isub>E I E \<times> Pi\<^isub>E J E"
+      using M.sets_into_space by auto blast+ }
+  note this[simp]
+  show "\<And>A. A \<in> sets ?IJ \<Longrightarrow> ?M -` A \<inter> space ?P \<in> sets ?P"
+    by (force elim!: pair_algebraE product_algebraE
+              simp del: vimage_Int simp: restrict_vimage merge_vimage space_pair_algebra)
   qed
-next
-  fix X assume *: "X \<in> ?F" show "X \<in> ?f ` ?P"
-  proof (cases X)
-    case (Pair a b) with * `i \<notin> I` show ?thesis
-      by (auto intro!: image_eqI[where x="a (i := b)"] ext simp: extensional_def)
-  qed
-qed auto
+
+lemma (in product_sigma_algebra) measurable_singleton_on_generator:
+  "(\<lambda>x. \<lambda>j\<in>{i}. x) \<in> measurable (M i) (product_algebra M {i})"
+  (is "?f \<in> measurable _ ?P")
+proof (unfold measurable_def, intro CollectI conjI)
+  show "?f \<in> space (M i) \<rightarrow> space ?P" by auto
+  have "\<And>E. E i \<in> sets (M i) \<Longrightarrow> ?f -` Pi\<^isub>E {i} E \<inter> space (M i) = E i"
+    using M.sets_into_space by auto
+  then show "\<forall>A \<in> sets ?P. ?f -` A \<inter> space (M i) \<in> sets (M i)"
+    by (auto elim!: product_algebraE)
+qed
+
+lemma (in product_sigma_algebra) measurable_component_on_generator:
+  assumes "i \<in> I" shows "(\<lambda>x. x i) \<in> measurable (product_algebra M I) (M i)"
+  (is "?f \<in> measurable ?P _")
+proof (unfold measurable_def, intro CollectI conjI ballI)
+  show "?f \<in> space ?P \<rightarrow> space (M i)" using `i \<in> I` by auto
+  fix A assume "A \<in> sets (M i)"
+  moreover then have "(\<lambda>x. x i) -` A \<inter> (\<Pi>\<^isub>E i\<in>I. space (M i)) =
+      (\<Pi>\<^isub>E j\<in>I. if i = j then A else space (M j))"
+    using M.sets_into_space `i \<in> I`
+    by (fastsimp dest: Pi_mem split: split_if_asm)
+  ultimately show "?f -` A \<inter> space ?P \<in> sets ?P"
+    by (auto intro!: product_algebraI)
+qed
 
-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)
+lemma (in product_sigma_algebra) measurable_restrict_singleton_on_generating:
+  assumes [simp]: "i \<notin> I"
+  shows "(\<lambda>x. (restrict x I, x i)) \<in> measurable
+    (product_algebra M (insert i I))
+    (pair_algebra (product_algebra M I) (M i))"
+    (is "?R \<in> measurable ?I ?P")
+proof (unfold measurable_def, intro CollectI conjI ballI)
+  show "?R \<in> space ?I \<rightarrow> space ?P" by (auto simp: space_pair_algebra)
+  { fix E F assume "E \<in> (\<Pi> i\<in>I. sets (M i))" "F \<in> sets (M i)"
+    then have "(\<lambda>x. (restrict x I, x i)) -` (Pi\<^isub>E I E \<times> F) \<inter> (\<Pi>\<^isub>E i\<in>insert i I. space (M i)) =
+        Pi\<^isub>E (insert i I) (E(i := F))"
+      using M.sets_into_space using `i\<notin>I` by (auto simp: restrict_Pi_cancel) blast+ }
+  note this[simp]
+  show "\<And>A. A \<in> sets ?P \<Longrightarrow> ?R -` A \<inter> space ?I \<in> sets ?I"
+    by (force elim!: pair_algebraE product_algebraE
+              simp del: vimage_Int simp: space_pair_algebra)
+qed
+
+lemma (in product_sigma_algebra) measurable_merge_singleton_on_generating:
+  assumes [simp]: "i \<notin> I"
+  shows "(\<lambda>(x, y). x(i := y)) \<in> measurable
+    (pair_algebra (product_algebra M I) (M i))
+    (product_algebra M (insert i I))"
+    (is "?M \<in> measurable ?P ?IJ")
+proof (unfold measurable_def, intro CollectI conjI ballI)
+  show "?M \<in> space ?P \<rightarrow> space ?IJ" by (auto simp: space_pair_algebra)
+  { fix E assume "E \<in> (\<Pi> i\<in>I. sets (M i))" "E i \<in> sets (M i)"
+    then have "(\<lambda>(x, y). x(i := y)) -` Pi\<^isub>E (insert i I) E \<inter> (\<Pi>\<^isub>E i\<in>I. space (M i)) \<times> space (M i) =
+        Pi\<^isub>E I E \<times> E i"
+      using M.sets_into_space by auto blast+ }
+  note this[simp]
+  show "\<And>A. A \<in> sets ?IJ \<Longrightarrow> ?M -` A \<inter> space ?P \<in> sets ?P"
+    by (force elim!: pair_algebraE product_algebraE
+              simp del: vimage_Int simp: space_pair_algebra)
 qed
 
 section "Generating set generates also product algebra"
@@ -1108,38 +1252,6 @@
     by (simp add: pair_algebra_def sigma_def)
 qed
 
-lemma Pi_fupd_iff: "i \<in> I \<Longrightarrow> f \<in> Pi I (B(i := A)) \<longleftrightarrow> f \<in> Pi (I - {i}) B \<and> f i \<in> A"
-  apply auto
-  apply (drule_tac x=x in Pi_mem)
-  apply (simp_all split: split_if_asm)
-  apply (drule_tac x=i in Pi_mem)
-  apply (auto dest!: Pi_mem)
-  done
-
-lemma Pi_UN:
-  fixes A :: "nat \<Rightarrow> 'i \<Rightarrow> 'a set"
-  assumes "finite I" and mono: "\<And>i n m. i \<in> I \<Longrightarrow> n \<le> m \<Longrightarrow> A n i \<subseteq> A m i"
-  shows "(\<Union>n. Pi I (A n)) = (\<Pi> i\<in>I. \<Union>n. A n i)"
-proof (intro set_eqI iffI)
-  fix f assume "f \<in> (\<Pi> i\<in>I. \<Union>n. A n i)"
-  then have "\<forall>i\<in>I. \<exists>n. f i \<in> A n i" by auto
-  from bchoice[OF this] obtain n where n: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> (A (n i) i)" by auto
-  obtain k where k: "\<And>i. i \<in> I \<Longrightarrow> n i \<le> k"
-    using `finite I` finite_nat_set_iff_bounded_le[of "n`I"] by auto
-  have "f \<in> Pi I (A k)"
-  proof (intro Pi_I)
-    fix i assume "i \<in> I"
-    from mono[OF this, of "n i" k] k[OF this] n[OF this]
-    show "f i \<in> A k i" by auto
-  qed
-  then show "f \<in> (\<Union>n. Pi I (A n))" by auto
-qed auto
-
-lemma PiE_cong:
-  assumes "\<And>i. i\<in>I \<Longrightarrow> A i = B i"
-  shows "Pi\<^isub>E I A = Pi\<^isub>E I B"
-  using assms by (auto intro!: Pi_cong)
-
 lemma sigma_product_algebra_sigma_eq:
   assumes "finite I"
   assumes isotone: "\<And>i. i \<in> I \<Longrightarrow> (S i) \<up> (space (E i))"
@@ -1209,150 +1321,163 @@
     by (simp add: product_algebra_def sigma_def)
 qed
 
-lemma (in finite_product_sigma_algebra) pair_sigma_algebra_finite_product_space:
-  "sigma (pair_algebra P (M i)) = sigma (pair_algebra G (M i))"
-proof -
-  have "sigma (pair_algebra P (M i)) = sigma (pair_algebra P (sigma (M i)))" by simp
-  also have "\<dots> = sigma (pair_algebra G (M i))"
-  proof (rule pair_sigma_algebra_sigma)
-    show "(\<lambda>_. \<Pi>\<^isub>E i\<in>I. space (M i)) \<up> space G"
-      "(\<lambda>_. space (M i)) \<up> space (M i)"
-      by (simp_all add: isoton_const)
-    show "range (\<lambda>_. \<Pi>\<^isub>E i\<in>I. space (M i)) \<subseteq> sets G" "range (\<lambda>_. space (M i)) \<subseteq> sets (M i)"
-      by (auto intro!: image_eqI[where x="\<lambda>i\<in>I. space (M i)"] dest: Pi_mem
-               simp: product_algebra_def)
-    show "sets G \<subseteq> Pow (space G)" "sets (M i) \<subseteq> Pow (space (M i))"
-      using product_algebra_into_space M.sets_into_space by auto
-  qed
-  finally show ?thesis .
-qed
-
-lemma sets_pair_algebra: "sets (pair_algebra N M) = (\<lambda>(x, y). x \<times> y) ` (sets N \<times> sets M)"
-  unfolding pair_algebra_def by auto
-
-lemma (in finite_product_sigma_algebra) sigma_pair_algebra_sigma_eq:
+lemma (in product_sigma_algebra) sigma_pair_algebra_sigma_eq:
   "sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J))) =
    sigma (pair_algebra (product_algebra M I) (product_algebra M J))"
   using M.sets_into_space
   by (intro pair_sigma_algebra_sigma[of "\<lambda>_. \<Pi>\<^isub>E i\<in>I. space (M i)", of _ "\<lambda>_. \<Pi>\<^isub>E i\<in>J. space (M i)"])
      (auto simp: isoton_const product_algebra_def, blast+)
 
+lemma (in product_sigma_algebra) sigma_pair_algebra_product_singleton:
+  "sigma (pair_algebra (sigma (product_algebra M I)) (M i)) =
+   sigma (pair_algebra (product_algebra M I) (M i))"
+  using M.sets_into_space apply (subst M.sigma_eq[symmetric])
+  by (intro pair_sigma_algebra_sigma[of "\<lambda>_. \<Pi>\<^isub>E i\<in>I. space (M i)" _ "\<lambda>_. space (M i)"])
+     (auto simp: isoton_const product_algebra_def, blast+)
+
+lemma (in product_sigma_algebra) measurable_restrict:
+  assumes [simp]: "I \<inter> J = {}"
+  shows "(\<lambda>x. (restrict x I, restrict x J)) \<in> measurable
+    (sigma (product_algebra M (I \<union> J)))
+    (sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J))))"
+  unfolding sigma_pair_algebra_sigma_eq using M.sets_into_space
+  by (intro measurable_sigma_sigma measurable_restrict_on_generating
+            pair_algebra_sets_into_space product_algebra_sets_into_space)
+     auto
+
+lemma (in product_sigma_algebra) measurable_merge:
+  assumes [simp]: "I \<inter> J = {}"
+  shows "(\<lambda>(x, y). merge I x J y) \<in> measurable
+    (sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J))))
+    (sigma (product_algebra M (I \<union> J)))"
+  unfolding sigma_pair_algebra_sigma_eq using M.sets_into_space
+  by (intro measurable_sigma_sigma measurable_merge_on_generating
+            pair_algebra_sets_into_space product_algebra_sets_into_space)
+     auto
+
 lemma (in product_sigma_algebra) product_product_vimage_algebra:
-  assumes [simp]: "I \<inter> J = {}" and "finite I" "finite J"
+  assumes [simp]: "I \<inter> J = {}"
   shows "sigma_algebra.vimage_algebra
     (sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J))))
-    (space (product_algebra M (I \<union> J))) (\<lambda>x. ((\<lambda>i\<in>I. x i), (\<lambda>i\<in>J. x i))) =
+    (space (sigma (product_algebra M (I \<union> J)))) (\<lambda>x. ((\<lambda>i\<in>I. x i), (\<lambda>i\<in>J. x i))) =
     sigma (product_algebra M (I \<union> J))"
-    (is "sigma_algebra.vimage_algebra _ (space ?IJ) ?f = sigma ?IJ")
-proof -
-  have "finite (I \<union> J)" using assms by auto
-  interpret I: finite_product_sigma_algebra M I by default fact
-  interpret J: finite_product_sigma_algebra M J by default fact
-  interpret IJ: finite_product_sigma_algebra M "I \<union> J" by default fact
-  interpret pair_sigma_algebra I.P J.P by default
+  unfolding sigma_pair_algebra_sigma_eq using sets_into_space
+  by (intro vimage_algebra_sigma[OF bij_inv_restrict_merge]
+            pair_algebra_sets_into_space product_algebra_sets_into_space
+            measurable_merge_on_generating measurable_restrict_on_generating)
+     auto
+
+lemma (in product_sigma_algebra) pair_product_product_vimage_algebra:
+  assumes [simp]: "I \<inter> J = {}"
+  shows "sigma_algebra.vimage_algebra (sigma (product_algebra M (I \<union> J)))
+    (space (sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J))))) (\<lambda>(x,y). merge I x J y) =
+    (sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J))))"
+  unfolding sigma_pair_algebra_sigma_eq using sets_into_space
+  by (intro vimage_algebra_sigma[OF bij_inv_restrict_merge[symmetric]]
+            pair_algebra_sets_into_space product_algebra_sets_into_space
+            measurable_merge_on_generating measurable_restrict_on_generating)
+     auto
+
+lemma (in product_sigma_algebra) pair_product_singleton_vimage_algebra:
+  assumes [simp]: "i \<notin> I"
+  shows "sigma_algebra.vimage_algebra (sigma (pair_algebra (sigma (product_algebra M I)) (M i)))
+    (space (sigma (product_algebra M (insert i I)))) (\<lambda>x. (restrict x I, x i)) =
+    (sigma (product_algebra M (insert i I)))"
+  unfolding sigma_pair_algebra_product_singleton using sets_into_space
+  by (intro vimage_algebra_sigma[OF bij_inv_restrict_insert]
+            pair_algebra_sets_into_space product_algebra_sets_into_space
+            measurable_merge_singleton_on_generating measurable_restrict_singleton_on_generating)
+      auto
 
-  show "vimage_algebra (space ?IJ) ?f = sigma ?IJ"
-    unfolding I.sigma_pair_algebra_sigma_eq
-  proof (rule vimage_algebra_sigma)
-    from M.sets_into_space
-    show "sets (pair_algebra I.G J.G) \<subseteq> Pow (space (pair_algebra I.G J.G))"
-      by (auto simp: sets_pair_algebra space_pair_algebra product_algebra_def) blast+
-    show "?f \<in> space IJ.G \<rightarrow> space (pair_algebra I.G J.G)"
-      by (auto simp: space_pair_algebra product_algebra_def)
-    let ?F = "\<lambda>A. ?f -` A \<inter> (space IJ.G)"
-    let ?s = "\<lambda>I. Pi\<^isub>E I ` (\<Pi> i\<in>I. sets (M i))"
-    { fix A assume "A \<in> sets IJ.G"
-      then obtain F where A: "A = Pi\<^isub>E (I \<union> J) F" "F \<in> (\<Pi> i\<in>I. sets (M i))" "F \<in> (\<Pi> i\<in>J. sets (M i))"
-        by (auto simp: product_algebra_def)
-      show "A \<in> ?F ` sets (pair_algebra I.G J.G)"
-          using A M.sets_into_space
-          by (auto simp: restrict_Pi_cancel product_algebra_def
-                   intro!: image_eqI[where x="Pi\<^isub>E I F \<times> Pi\<^isub>E J F"]) blast+ }
-    { fix A assume "A \<in> sets (pair_algebra I.G J.G)"
-      then obtain E F where A: "A = Pi\<^isub>E I E \<times> Pi\<^isub>E J F" "E \<in> (\<Pi> i\<in>I. sets (M i))" "F \<in> (\<Pi> i\<in>J. sets (M i))"
-        by (auto simp: product_algebra_def sets_pair_algebra)
-      then show "?F A \<in> sets IJ.G"
-          using A M.sets_into_space
-          by (auto simp: restrict_Pi_cancel product_algebra_def
-                   intro!: image_eqI[where x="merge I E J F"]) blast+ }
-  qed
-qed
+lemma (in product_sigma_algebra) singleton_vimage_algebra:
+  "sigma_algebra.vimage_algebra (sigma (product_algebra M {i})) (space (M i)) (\<lambda>x. \<lambda>j\<in>{i}. x) = M i"
+  using sets_into_space
+  by (intro vimage_algebra_sigma[of "M i", unfolded M.sigma_eq, OF bij_inv_singleton[symmetric]]
+             product_algebra_sets_into_space measurable_singleton_on_generator measurable_component_on_generator)
+     auto
+
+lemma (in product_sigma_algebra) measurable_restrict_iff:
+  assumes IJ[simp]: "I \<inter> 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'"
+  using M.sets_into_space
+  apply (subst pair_product_product_vimage_algebra[OF IJ, symmetric])
+  apply (subst sigma_pair_algebra_sigma_eq)
+  apply (subst sigma_algebra.measurable_vimage_iff_inv[OF _
+      bij_inv_restrict_merge[symmetric]])
+  apply (intro sigma_algebra_sigma product_algebra_sets_into_space)
+  by auto
 
-lemma (in finite_product_sigma_algebra) sigma_pair_algebra_sigma_M_eq:
-  "sigma (pair_algebra P (M i)) = sigma (pair_algebra G (M i))"
+lemma (in product_sigma_algebra) measurable_merge_iff:
+  assumes IJ: "I \<inter> J = {}"
+  shows "f \<in> measurable (sigma (product_algebra M (I \<union> J))) M' \<longleftrightarrow>
+    (\<lambda>(x, y). f (merge I x J y)) \<in>
+      measurable (sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J)))) M'"
+  unfolding measurable_restrict_iff[OF IJ]
+  by (rule measurable_cong) (auto intro!: arg_cong[where f=f] simp: extensional_restrict)
+
+lemma (in product_sigma_algebra) measurable_component:
+  assumes "i \<in> I" and f: "f \<in> measurable (M i) M'"
+  shows "(\<lambda>x. f (x i)) \<in> measurable (sigma (product_algebra M I)) M'"
+    (is "?f \<in> measurable ?P M'")
 proof -
-  have "sigma (pair_algebra P (sigma (M i))) = sigma (pair_algebra G (M i))"
-    using M.sets_into_space
-    by (intro pair_sigma_algebra_sigma[of "\<lambda>_. \<Pi>\<^isub>E i\<in>I. space (M i)", of _ "\<lambda>_. space (M i)"])
-       (auto simp: isoton_const product_algebra_def, blast+)
-  then show ?thesis by simp
+  have "f \<circ> (\<lambda>x. x i) \<in> measurable ?P M'"
+    apply (rule measurable_comp[OF _ f])
+    using measurable_up_sigma[of "product_algebra M I" "M i"]
+    using measurable_component_on_generator[OF `i \<in> I`]
+    by auto
+  then show "?f \<in> measurable ?P M'" by (simp add: comp_def)
 qed
 
-lemma (in product_sigma_algebra) product_singleton_vimage_algebra_eq:
-  assumes [simp]: "i \<notin> I" "finite I"
-  shows "sigma_algebra.vimage_algebra
-    (sigma (pair_algebra (sigma (product_algebra M I)) (M i)))
-    (space (product_algebra M (insert i I))) (\<lambda>x. ((\<lambda>i\<in>I. x i), x i)) =
-    sigma (product_algebra M (insert i I))"
-    (is "sigma_algebra.vimage_algebra _ (space ?I') ?f = sigma ?I'")
-proof -
-  have "finite (insert i I)" using assms by auto
-  interpret I: finite_product_sigma_algebra M I by default fact
-  interpret I': finite_product_sigma_algebra M "insert i I" by default fact
-  interpret pair_sigma_algebra I.P "M i" by default
-  show "vimage_algebra (space ?I') ?f = sigma ?I'"
-    unfolding I.sigma_pair_algebra_sigma_M_eq
-  proof (rule vimage_algebra_sigma)
-    from M.sets_into_space
-    show "sets (pair_algebra I.G (M i)) \<subseteq> Pow (space (pair_algebra I.G (M i)))"
-      by (auto simp: sets_pair_algebra space_pair_algebra product_algebra_def) blast
-    show "?f \<in> space I'.G \<rightarrow> space (pair_algebra I.G (M i))"
-      by (auto simp: space_pair_algebra product_algebra_def)
-    let ?F = "\<lambda>A. ?f -` A \<inter> (space I'.G)"
-    { fix A assume "A \<in> sets I'.G"
-      then obtain F where A: "A = Pi\<^isub>E (insert i I) F" "F \<in> (\<Pi> i\<in>I. sets (M i))" "F i \<in> sets (M i)"
-        by (auto simp: product_algebra_def)
-      show "A \<in> ?F ` sets (pair_algebra I.G (M i))"
-          using A M.sets_into_space
-          by (auto simp: restrict_Pi_cancel product_algebra_def
-                   intro!: image_eqI[where x="Pi\<^isub>E I F \<times> F i"]) blast+ }
-    { fix A assume "A \<in> sets (pair_algebra I.G (M i))"
-      then obtain E F where A: "A = Pi\<^isub>E I E \<times> F" "E \<in> (\<Pi> i\<in>I. sets (M i))" "F \<in> sets (M i)"
-        by (auto simp: product_algebra_def sets_pair_algebra)
-      then show "?F A \<in> sets I'.G"
-          using A M.sets_into_space
-          by (auto simp: restrict_Pi_cancel product_algebra_def
-                   intro!: image_eqI[where x="E(i:= F)"]) blast+ }
+lemma (in product_sigma_algebra) measurable_component_singleton:
+  "(\<lambda>x. f (x i)) \<in> measurable (sigma (product_algebra M {i})) M' \<longleftrightarrow>
+    f \<in> measurable (M i) M'"
+  using sets_into_space
+  apply (subst singleton_vimage_algebra[symmetric])
+  apply (subst sigma_algebra.measurable_vimage_iff_inv[OF _ bij_inv_singleton[symmetric]])
+  by (auto intro!: sigma_algebra_sigma product_algebra_sets_into_space)
+
+lemma (in product_sigma_algebra) measurable_component_iff:
+  assumes "i \<in> I" and not_empty: "\<forall>i\<in>I. space (M i) \<noteq> {}"
+  shows "(\<lambda>x. f (x i)) \<in> measurable (sigma (product_algebra M I)) M' \<longleftrightarrow>
+    f \<in> measurable (M i) M'"
+    (is "?f \<in> measurable ?P M' \<longleftrightarrow> _")
+proof
+  assume "f \<in> measurable (M i) M'" then show "?f \<in> measurable ?P M'"
+    by (rule measurable_component[OF `i \<in> I`])
+next
+  assume f: "?f \<in> measurable ?P M'"
+  def t \<equiv> "\<lambda>i. SOME x. x \<in> space (M i)"
+  have t: "\<And>i. i\<in>I \<Longrightarrow> t i \<in> space (M i)"
+     unfolding t_def using not_empty by (rule_tac someI_ex) auto
+  have "?f \<circ> (\<lambda>x. (\<lambda>j\<in>I. if j = i then x else t j)) \<in> measurable (M i) M'"
+    (is "?f \<circ> ?t \<in> measurable _ _")
+  proof (rule measurable_comp[OF _ f])
+    have "?t \<in> measurable (M i) (product_algebra M I)"
+    proof (unfold measurable_def, intro CollectI conjI ballI)
+      from t show "?t \<in> space (M i) \<rightarrow> (space (product_algebra M I))" by auto
+    next
+      fix A assume A: "A \<in> sets (product_algebra M I)"
+      { fix E assume "E \<in> (\<Pi> i\<in>I. sets (M i))"
+        then have "?t -` Pi\<^isub>E I E \<inter> space (M i) = (if (\<forall>j\<in>I-{i}. t j \<in> E j) then E i else {})"
+          using `i \<in> I` sets_into_space by (auto dest: Pi_mem[where B=E]) }
+      note * = this
+      with A `i \<in> I` show "?t -` A \<inter> space (M i) \<in> sets (M i)"
+        by (auto elim!: product_algebraE simp del: vimage_Int)
+    qed
+    also have "\<dots> \<subseteq> measurable (M i) (sigma (product_algebra M I))"
+      using M.sets_into_space by (intro measurable_subset) (auto simp: product_algebra_def, blast)
+    finally show "?t \<in> measurable (M i) (sigma (product_algebra M I))" .
   qed
+  then show "f \<in> measurable (M i) M'" unfolding comp_def using `i \<in> I` by simp
 qed
 
-lemma restrict_fupd[simp]: "i \<notin> I \<Longrightarrow> restrict (f (i := x)) I = restrict f I"
-  by (auto simp: restrict_def intro!: ext)
-
-lemma bij_betw_restrict_I_i:
-  "i \<notin> I \<Longrightarrow> bij_betw (\<lambda>x. (restrict x I, x i))
-    (space (product_algebra M (insert i I)))
-    (space (pair_algebra (sigma (product_algebra M I)) (M i)))"
-  by (intro bij_betwI[where g="(\<lambda>(x,y). x(i:=y))"])
-     (auto simp: space_pair_algebra extensional_def intro!: ext)
-
-lemma (in product_sigma_algebra) product_singleton_vimage_algebra_inv_eq:
-  assumes [simp]: "i \<notin> I" "finite I"
-  shows "sigma_algebra.vimage_algebra
-    (sigma (product_algebra M (insert i I)))
-    (space (pair_algebra (sigma (product_algebra M I)) (M i))) (\<lambda>(x,y). x(i:=y)) =
-    sigma (pair_algebra (sigma (product_algebra M I)) (M i))"
-proof -
-  have "finite (insert i I)" using `finite I` by auto
-  interpret I: finite_product_sigma_algebra M I by default fact
-  interpret I': finite_product_sigma_algebra M "insert i I" by default fact
-  interpret pair_sigma_algebra I.P "M i" by default
-  show ?thesis
-    unfolding product_singleton_vimage_algebra_eq[OF assms, symmetric]
-    using bij_betw_restrict_I_i[OF `i \<notin> I`, of M]
-    by (rule vimage_vimage_inv[unfolded space_sigma])
-       (auto simp: space_pair_algebra product_algebra_def dest: extensional_restrict)
-qed
+lemma (in product_sigma_algebra) measurable_singleton:
+  shows "f \<in> measurable (sigma (product_algebra M {i})) M' \<longleftrightarrow>
+    (\<lambda>x. f (\<lambda>j\<in>{i}. x)) \<in> measurable (M i) M'"
+  using sets_into_space unfolding measurable_component_singleton[symmetric]
+  by (auto intro!: measurable_cong arg_cong[where f=f] simp: fun_eq_iff extensional_def)
 
 locale product_sigma_finite =
   fixes M :: "'i \<Rightarrow> 'a algebra" and \<mu> :: "'i \<Rightarrow> 'a set \<Rightarrow> pextreal"
@@ -1427,9 +1552,10 @@
   let ?h = "\<lambda>x. (restrict x I, x i)"
   let ?\<nu> = "\<lambda>A. P.pair_measure (?h ` A)"
   interpret I': measure_space "sigma (product_algebra M (insert i I))" ?\<nu>
-    unfolding product_singleton_vimage_algebra_eq[OF `i \<notin> I` `finite I`, symmetric]
-    using bij_betw_restrict_I_i[OF `i \<notin> I`, of M]
-    by (intro P.measure_space_isomorphic) auto
+    apply (subst pair_product_singleton_vimage_algebra[OF `i \<notin> I`, symmetric])
+    apply (intro P.measure_space_isomorphic bij_inv_bij_betw)
+    unfolding sigma_pair_algebra_product_singleton
+    by (rule bij_inv_restrict_insert[OF `i \<notin> I`])
   show ?case
   proof (intro exI[of _ ?\<nu>] conjI ballI)
     { fix A assume A: "A \<in> (\<Pi> i\<in>insert i I. sets (M i))"
@@ -1512,6 +1638,17 @@
   "product_integral I \<equiv>
     measure_space.integral (sigma (product_algebra M I)) (product_measure I)"
 
+abbreviation (in product_sigma_finite)
+  "product_integrable I \<equiv>
+    measure_space.integrable (sigma (product_algebra M I)) (product_measure I)"
+
+lemma (in product_sigma_finite) product_measure_empty[simp]:
+  "product_measure {} {\<lambda>x. undefined} = 1"
+proof -
+  interpret finite_product_sigma_finite M \<mu> "{}" by default auto
+  from measure_times[of "\<lambda>x. {}"] show ?thesis by simp
+qed
+
 lemma (in product_sigma_finite) positive_integral_empty:
   "product_positive_integral {} f = f (\<lambda>k. undefined)"
 proof -
@@ -1528,46 +1665,6 @@
   qed
 qed
 
-lemma merge_restrict[simp]:
-  "merge I (restrict x I) J y = merge I x J y"
-  "merge I x J (restrict y J) = merge I x J y"
-  unfolding merge_def by (auto intro!: ext)
-
-lemma merge_x_x_eq_restrict[simp]:
-  "merge I x J x = restrict x (I \<union> J)"
-  unfolding merge_def by (auto intro!: ext)
-
-lemma bij_betw_restrict_I_J:
-  "I \<inter> J = {} \<Longrightarrow> bij_betw (\<lambda>x. (restrict x I, restrict x J))
-    (space (product_algebra M (I \<union> J)))
-    (space (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J))))"
-  by (intro bij_betwI[where g="\<lambda>(x,y). merge I x J y"])
-     (auto dest: extensional_restrict simp: space_pair_algebra)
-
-lemma (in product_sigma_algebra) product_product_vimage_algebra_eq:
-  assumes [simp]: "I \<inter> J = {}" and "finite I" "finite J"
-  shows "sigma_algebra.vimage_algebra
-    (sigma (product_algebra M (I \<union> J)))
-    (space (sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J)))))
-    (\<lambda>(x, y). merge I x J y) =
-    sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J)))"
-  (is "sigma_algebra.vimage_algebra ?IJ ?S ?m = ?P")
-proof -
-  interpret I: finite_product_sigma_algebra M I by default fact
-  interpret J: finite_product_sigma_algebra M J by default fact
-  have "finite (I \<union> J)" using assms by auto
-  interpret IJ: finite_product_sigma_algebra M "I \<union> J" by default fact
-  interpret P: pair_sigma_algebra I.P J.P by default
-
-  let ?g = "\<lambda>x. (restrict x I, restrict x J)"
-  let ?f = "\<lambda>(x, y). merge I x J y"
-  show "IJ.vimage_algebra (space P.P) ?f = P.P"
-    using bij_betw_restrict_I_J[OF `I \<inter> J = {}`]
-    by (subst P.vimage_vimage_inv[of ?g "space IJ.G" ?f,
-                   unfolded product_product_vimage_algebra[OF assms]])
-       (auto simp: pair_algebra_def dest: extensional_restrict)
-qed
-
 lemma (in product_sigma_finite) measure_fold:
   assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
   assumes A: "A \<in> sets (sigma (product_algebra M (I \<union> J)))"
@@ -1598,9 +1695,10 @@
       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
       show "measure_space IJ.P (\<lambda>A. P.pair_measure (?f ` A))"
-        unfolding product_product_vimage_algebra[OF IJ fin, symmetric]
-        using bij_betw_restrict_I_J[OF IJ, of M]
-        by (auto intro!: P.measure_space_isomorphic)
+      apply (subst product_product_vimage_algebra[OF IJ, symmetric])
+      apply (intro P.measure_space_isomorphic bij_inv_bij_betw)
+      unfolding sigma_pair_algebra_sigma_eq
+      by (rule bij_inv_restrict_merge[OF `I \<inter> J = {}`])
       show "measure_space IJ.P IJ.measure" by fact
     next
       fix A assume "A \<in> sets IJ.G"
@@ -1640,14 +1738,16 @@
   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)
+    unfolding case_prod_distrib measurable_merge_iff[OF IJ, symmetric] using f .
+  have bij: "bij_betw ?f (space IJ.P) (space P.P)"
+    unfolding sigma_pair_algebra_sigma_eq
+    by (intro bij_inv_bij_betw) (rule bij_inv_restrict_merge[OF IJ])
   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]
+    unfolding P.positive_integral_vimage[OF bij]
+    unfolding product_product_vimage_algebra[OF IJ]
     apply simp
     apply (rule IJ.positive_integral_cong_measure[symmetric])
     apply (rule measure_fold)
@@ -1687,6 +1787,59 @@
   qed simp
 qed
 
+lemma (in product_sigma_finite) product_positive_integral_insert:
+  assumes [simp]: "finite I" "i \<notin> I"
+    and f: "f \<in> borel_measurable (sigma (product_algebra M (insert i I)))"
+  shows "product_positive_integral (insert i I) f
+    = product_positive_integral I (\<lambda>x. M.positive_integral i (\<lambda>y. f (x(i:=y))))"
+proof -
+  interpret I: finite_product_sigma_finite M \<mu> I by default auto
+  interpret i: finite_product_sigma_finite M \<mu> "{i}" by default auto
+  interpret P: pair_sigma_algebra I.P i.P ..
+  have IJ: "I \<inter> {i} = {}" by auto
+  show ?thesis
+    unfolding product_positive_integral_fold[OF IJ, simplified, OF f]
+  proof (rule I.positive_integral_cong, subst product_positive_integral_singleton)
+    fix x assume x: "x \<in> space I.P"
+    let "?f y" = "f (restrict (x(i := y)) (insert i I))"
+    have f'_eq: "\<And>y. ?f y = f (x(i := y))"
+      using x by (auto intro!: arg_cong[where f=f] simp: fun_eq_iff extensional_def)
+    note fP = f[unfolded measurable_merge_iff[OF IJ, simplified]]
+    show "?f \<in> borel_measurable (M i)"
+      using P.measurable_pair_image_snd[OF fP x]
+      unfolding measurable_singleton f'_eq by (simp add: f'_eq)
+    show "M.positive_integral i ?f = M.positive_integral i (\<lambda>y. f (x(i := y)))"
+      unfolding f'_eq by simp
+  qed
+qed
+
+lemma (in product_sigma_finite) product_positive_integral_setprod:
+  fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> pextreal"
+  assumes "finite I" and borel: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable (M i)"
+  shows "product_positive_integral I (\<lambda>x. (\<Prod>i\<in>I. f i (x i))) =
+    (\<Prod>i\<in>I. M.positive_integral i (f i))"
+using assms proof induct
+  case empty
+  interpret finite_product_sigma_finite M \<mu> "{}" by default auto
+  then show ?case by simp
+next
+  case (insert i I)
+  note `finite I`[intro, simp]
+  interpret I: finite_product_sigma_finite M \<mu> I by default auto
+  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 insert by (auto intro!: setprod_cong)
+  have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow>
+    (\<lambda>x. (\<Prod>i\<in>J. f i (x i))) \<in> borel_measurable (sigma (product_algebra M J))"
+    using sets_into_space insert
+    by (intro sigma_algebra.borel_measurable_pextreal_setprod
+              sigma_algebra_sigma product_algebra_sets_into_space
+              measurable_component)
+       auto
+  show ?case
+    by (simp add: product_positive_integral_insert[OF insert(1,2) prod])
+       (simp add: insert I.positive_integral_cmult M.positive_integral_multc * prod subset_insertI)
+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"
@@ -1700,45 +1853,6 @@
     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"
@@ -1761,7 +1875,7 @@
   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]
+    unfolding measurable_restrict_iff[OF IJ]
     by simp_all
   have PI:
     "P.positive_integral (\<lambda>x. Real (?f x)) = IJ.positive_integral (\<lambda>x. Real (f x))"
@@ -1771,7 +1885,7 @@
     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]
+    unfolding measurable_restrict_iff[OF IJ]
     using f_restrict PI by simp_all
   show ?thesis
     unfolding P.integrable_fst_measurable(2)[OF `P.integrable ?f`, simplified]
@@ -1779,6 +1893,84 @@
     unfolding PI by simp
 qed
 
+lemma (in product_sigma_finite) product_integral_insert:
+  assumes [simp]: "finite I" "i \<notin> I"
+    and f: "measure_space.integrable (sigma (product_algebra M (insert i I))) (product_measure (insert i I)) f"
+  shows "product_integral (insert i I) f
+    = product_integral I (\<lambda>x. M.integral i (\<lambda>y. f (x(i:=y))))"
+proof -
+  interpret I: finite_product_sigma_finite M \<mu> I by default auto
+  interpret I': finite_product_sigma_finite M \<mu> "insert i I" by default auto
+  interpret i: finite_product_sigma_finite M \<mu> "{i}" by default auto
+  interpret P: pair_sigma_algebra I.P i.P ..
+  have IJ: "I \<inter> {i} = {}" by auto
+  show ?thesis
+    unfolding product_integral_fold[OF IJ, simplified, OF f]
+  proof (rule I.integral_cong, subst product_integral_singleton)
+    fix x assume x: "x \<in> space I.P"
+    let "?f y" = "f (restrict (x(i := y)) (insert i I))"
+    have f'_eq: "\<And>y. ?f y = f (x(i := y))"
+      using x by (auto intro!: arg_cong[where f=f] simp: fun_eq_iff extensional_def)
+    have "f \<in> borel_measurable I'.P" using f unfolding I'.integrable_def by auto
+    note fP = this[unfolded measurable_merge_iff[OF IJ, simplified]]
+    show "?f \<in> borel_measurable (M i)"
+      using P.measurable_pair_image_snd[OF fP x]
+      unfolding measurable_singleton f'_eq by (simp add: f'_eq)
+    show "M.integral i ?f = M.integral i (\<lambda>y. f (x(i := y)))"
+      unfolding f'_eq by simp
+  qed
+qed
+
+lemma (in product_sigma_finite) product_integrable_setprod:
+  fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> real"
+  assumes [simp]: "finite I" and integrable: "\<And>i. i \<in> I \<Longrightarrow> M.integrable i (f i)"
+  shows "product_integrable I (\<lambda>x. (\<Prod>i\<in>I. f i (x i)))" (is "product_integrable I ?f")
+proof -
+  interpret finite_product_sigma_finite M \<mu> I by default fact
+  have f: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable (M i)"
+    using integrable unfolding M.integrable_def by auto
+  then have borel: "?f \<in> borel_measurable P"
+    by (intro borel_measurable_setprod measurable_component) auto
+  moreover have "integrable (\<lambda>x. \<bar>\<Prod>i\<in>I. f i (x i)\<bar>)"
+  proof (unfold integrable_def, intro conjI)
+    show "(\<lambda>x. abs (?f x)) \<in> borel_measurable P"
+      using borel by auto
+    have "positive_integral (\<lambda>x. Real (abs (?f x))) =
+      positive_integral (\<lambda>x. \<Prod>i\<in>I. Real (abs (f i (x i))))"
+      by (simp add: Real_setprod abs_setprod)
+    also have "\<dots> = (\<Prod>i\<in>I. M.positive_integral i (\<lambda>x. Real (abs (f i x))))"
+      using f by (subst product_positive_integral_setprod) auto
+    also have "\<dots> < \<omega>"
+      using integrable[THEN M.integrable_abs]
+      unfolding pextreal_less_\<omega> setprod_\<omega> M.integrable_def by simp
+    finally show "positive_integral (\<lambda>x. Real (abs (?f x))) \<noteq> \<omega>" by auto
+    show "positive_integral (\<lambda>x. Real (- abs (?f x))) \<noteq> \<omega>" by simp
+  qed
+  ultimately show ?thesis
+    by (rule integrable_abs_iff[THEN iffD1])
+qed
+
+lemma (in product_sigma_finite) product_integral_setprod:
+  fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> real"
+  assumes "finite I" "I \<noteq> {}" and integrable: "\<And>i. i \<in> I \<Longrightarrow> M.integrable i (f i)"
+  shows "product_integral I (\<lambda>x. (\<Prod>i\<in>I. f i (x i))) = (\<Prod>i\<in>I. M.integral i (f i))"
+using assms proof (induct rule: finite_ne_induct)
+  case (singleton i)
+  then show ?case by (simp add: product_integral_singleton integrable_def)
+next
+  case (insert i I)
+  then have iI: "finite (insert i I)" by auto
+  then have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow>
+    product_integrable J (\<lambda>x. (\<Prod>i\<in>J. f i (x i)))"
+    by (intro product_integrable_setprod insert(5)) (auto intro: finite_subset)
+  interpret I: finite_product_sigma_finite M \<mu> I by default 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
+    unfolding product_integral_insert[OF insert(1,3) prod[OF subset_refl]]
+    by (simp add: * insert integral_multc I.integral_cmult[OF prod] subset_insertI)
+qed
+
 section "Products on finite spaces"
 
 lemma sigma_sets_pair_algebra_finite:
diff -r 1dc7652ce404 -r ababba14c965 src/HOL/Probability/Radon_Nikodym.thy
--- a/src/HOL/Probability/Radon_Nikodym.thy	Thu Dec 09 08:46:04 2010 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Thu Dec 09 10:22:17 2010 +0100
@@ -323,9 +323,10 @@
   { fix f g assume  "f \<up> g" and f: "\<And>i. f i \<in> G"
     have "g \<in> G" unfolding G_def
     proof safe
-      from `f \<up> g` have [simp]: "g = (SUP i. f i)" unfolding isoton_def by simp
+      from `f \<up> g` have [simp]: "g = (\<lambda>x. SUP i. f i x)"
+        unfolding isoton_def fun_eq_iff SUPR_apply by simp
       have f_borel: "\<And>i. f i \<in> borel_measurable M" using f unfolding G_def by simp
-      thus "g \<in> borel_measurable M" by (auto intro!: borel_measurable_SUP)
+      thus "g \<in> borel_measurable M" by auto
       fix A assume "A \<in> sets M"
       hence "\<And>i. (\<lambda>x. f i x * indicator A x) \<in> borel_measurable M"
         using f_borel by (auto intro!: borel_measurable_indicator)
@@ -1103,42 +1104,36 @@
     unfolding eq[OF A, symmetric] RN_deriv(2)[OF \<nu> A, symmetric] ..
 qed
 
-lemma the_inv_into_in:
-  assumes "inj_on f A" and x: "x \<in> f`A"
-  shows "the_inv_into A f x \<in> A"
-  using assms by (auto simp: the_inv_into_f_f)
-
 lemma (in sigma_finite_measure) RN_deriv_vimage:
   fixes f :: "'b \<Rightarrow> 'a"
-  assumes f: "bij_betw f S (space M)"
+  assumes f: "bij_inv S (space M) f g"
   assumes \<nu>: "measure_space M \<nu>" "absolutely_continuous \<nu>"
   shows "AE x.
-    sigma_finite_measure.RN_deriv (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) (\<lambda>A. \<nu> (f ` A)) (the_inv_into S f x) = RN_deriv \<nu> x"
+    sigma_finite_measure.RN_deriv (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) (\<lambda>A. \<nu> (f ` A)) (g x) = RN_deriv \<nu> x"
 proof (rule RN_deriv_unique[OF \<nu>])
   interpret sf: sigma_finite_measure "vimage_algebra S f" "\<lambda>A. \<mu> (f ` A)"
-    using f by (rule sigma_finite_measure_isomorphic)
+    using f by (rule sigma_finite_measure_isomorphic[OF bij_inv_bij_betw(1)])
   interpret \<nu>: measure_space M \<nu> using \<nu>(1) .
   have \<nu>': "measure_space (vimage_algebra S f) (\<lambda>A. \<nu> (f ` A))"
-    using f by (rule \<nu>.measure_space_isomorphic)
+    using f by (rule \<nu>.measure_space_isomorphic[OF bij_inv_bij_betw(1)])
   { fix A assume "A \<in> sets M" then have "f ` (f -` A \<inter> S) = A"
-      using sets_into_space f[unfolded bij_betw_def]
+      using sets_into_space f[THEN bij_inv_bij_betw(1), unfolded bij_betw_def]
       by (intro image_vimage_inter_eq[where T="space M"]) auto }
   note A_f = this
   then have ac: "sf.absolutely_continuous (\<lambda>A. \<nu> (f ` A))"
     using \<nu>(2) by (auto simp: sf.absolutely_continuous_def absolutely_continuous_def)
-  show "(\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (the_inv_into S f x)) \<in> borel_measurable M"
+  show "(\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x)) \<in> borel_measurable M"
     using sf.RN_deriv(1)[OF \<nu>' ac]
     unfolding measurable_vimage_iff_inv[OF f] comp_def .
   fix A assume "A \<in> sets M"
-  then have *: "\<And>x. x \<in> space M \<Longrightarrow> indicator (f -` A \<inter> S) (the_inv_into S f x) = (indicator A x :: pextreal)"
-    using f[unfolded bij_betw_def]
-    unfolding indicator_def by (auto simp: f_the_inv_into_f the_inv_into_in)
+  then have *: "\<And>x. x \<in> space M \<Longrightarrow> indicator (f -` A \<inter> S) (g x) = (indicator A x :: pextreal)"
+    using f by (auto simp: bij_inv_def indicator_def)
   have "\<nu> (f ` (f -` A \<inter> S)) = sf.positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) x * indicator (f -` A \<inter> S) x)"
     using `A \<in> sets M` by (force intro!: sf.RN_deriv(2)[OF \<nu>' ac])
-  also have "\<dots> = positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (the_inv_into S f x) * indicator A x)"
+  also have "\<dots> = positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)"
     unfolding positive_integral_vimage_inv[OF f]
     by (simp add: * cong: positive_integral_cong)
-  finally show "\<nu> A = positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (the_inv_into S f x) * indicator A x)"
+  finally show "\<nu> A = positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)"
     unfolding A_f[OF `A \<in> sets M`] .
 qed
 
diff -r 1dc7652ce404 -r ababba14c965 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Thu Dec 09 08:46:04 2010 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Thu Dec 09 10:22:17 2010 +0100
@@ -806,13 +806,6 @@
        (simp_all add: f_the_inv_into_f cong: measurable_cong)
 qed
 
-lemma (in sigma_algebra) measurable_vimage_iff_inv:
-  fixes f :: "'b \<Rightarrow> 'a" assumes f: "bij_betw f S (space M)"
-  shows "g \<in> measurable (vimage_algebra S f) M' \<longleftrightarrow> (g \<circ> the_inv_into S f) \<in> measurable M M'"
-  unfolding measurable_vimage_iff[OF f]
-  using f[unfolded bij_betw_def]
-  by (auto intro!: measurable_cong simp add: the_inv_into_f_f)
-
 lemma sigma_sets_vimage:
   assumes "f \<in> S' \<rightarrow> S" and "A \<subseteq> Pow S"
   shows "sigma_sets S' ((\<lambda>X. f -` X \<inter> S') ` A) = (\<lambda>X. f -` X \<inter> S') ` sigma_sets S A"
@@ -871,22 +864,6 @@
   qed
 qed
 
-lemma vimage_algebra_sigma:
-  assumes E: "sets E \<subseteq> Pow (space E)"
-    and f: "f \<in> space F \<rightarrow> space E"
-    and "\<And>A. A \<in> sets F \<Longrightarrow> A \<in> (\<lambda>X. f -` X \<inter> space F) ` sets E"
-    and "\<And>A. A \<in> sets E \<Longrightarrow> f -` A \<inter> space F \<in> sets F"
-  shows "sigma_algebra.vimage_algebra (sigma E) (space F) f = sigma F"
-proof -
-  interpret sigma_algebra "sigma E"
-    using assms by (intro sigma_algebra_sigma) auto
-  have eq: "sets F = (\<lambda>X. f -` X \<inter> space F) ` sets E"
-    using assms by auto
-  show "vimage_algebra (space F) f = sigma F"
-    unfolding vimage_algebra_def using assms
-    by (simp add: sigma_def eq sigma_sets_vimage)
-qed
-
 section {* Conditional space *}
 
 definition (in algebra)
@@ -1420,6 +1397,8 @@
     using E by simp
 qed
 
+subsection "Sigma algebras on finite sets"
+
 locale finite_sigma_algebra = sigma_algebra +
   assumes finite_space: "finite (space M)"
   and sets_eq_Pow[simp]: "sets M = Pow (space M)"
@@ -1438,4 +1417,92 @@
     by (auto simp: image_space_def)
 qed
 
+subsection "Bijective functions with inverse"
+
+definition "bij_inv A B f g \<longleftrightarrow>
+  f \<in> A \<rightarrow> B \<and> g \<in> B \<rightarrow> A \<and> (\<forall>x\<in>A. g (f x) = x) \<and> (\<forall>x\<in>B. f (g x) = x)"
+
+lemma bij_inv_symmetric[sym]: "bij_inv A B f g \<Longrightarrow> bij_inv B A g f"
+  unfolding bij_inv_def by auto
+
+lemma bij_invI:
+  assumes "f \<in> A \<rightarrow> B" "g \<in> B \<rightarrow> A"
+  and "\<And>x. x \<in> A \<Longrightarrow> g (f x) = x"
+  and "\<And>x. x \<in> B \<Longrightarrow> f (g x) = x"
+  shows "bij_inv A B f g"
+  using assms unfolding bij_inv_def by auto
+
+lemma bij_invE:
+  assumes "bij_inv A B f g"
+    "\<lbrakk> f \<in> A \<rightarrow> B ; g \<in> B \<rightarrow> A ;
+        (\<And>x. x \<in> A \<Longrightarrow> g (f x) = x) ;
+        (\<And>x. x \<in> B \<Longrightarrow> f (g x) = x) \<rbrakk> \<Longrightarrow> P"
+  shows P
+  using assms unfolding bij_inv_def by auto
+
+lemma bij_inv_bij_betw:
+  assumes "bij_inv A B f g"
+  shows "bij_betw f A B" "bij_betw g B A"
+  using assms by (auto intro: bij_betwI elim!: bij_invE)
+
+lemma bij_inv_vimage_vimage:
+  assumes "bij_inv A B f e"
+  shows "f -` (e -` X \<inter> B) \<inter> A = X \<inter> A"
+  using assms by (auto elim!: bij_invE)
+
+lemma (in sigma_algebra) measurable_vimage_iff_inv:
+  fixes f :: "'b \<Rightarrow> 'a" assumes "bij_inv S (space M) f g"
+  shows "h \<in> measurable (vimage_algebra S f) M' \<longleftrightarrow> (\<lambda>x. h (g x)) \<in> measurable M M'"
+  unfolding measurable_vimage_iff[OF bij_inv_bij_betw(1), OF assms]
+proof (rule measurable_cong)
+  fix w assume "w \<in> space (vimage_algebra S f)"
+  then have "w \<in> S" by auto
+  then show "h w = ((\<lambda>x. h (g x)) \<circ> f) w"
+    using assms by (auto elim: bij_invE)
+qed
+
+lemma vimage_algebra_sigma:
+  assumes bi: "bij_inv (space (sigma F)) (space (sigma E)) f e"
+    and "sets E \<subseteq> Pow (space E)" and F: "sets F \<subseteq> Pow (space F)"
+    and "f \<in> measurable F E" "e \<in> measurable E F"
+  shows "sigma_algebra.vimage_algebra (sigma E) (space (sigma F)) f = sigma F"
+proof -
+  interpret sigma_algebra "sigma E"
+    using assms by (intro sigma_algebra_sigma) auto
+  have eq: "sets F = (\<lambda>X. f -` X \<inter> space F) ` sets E"
+  proof safe
+    fix X assume "X \<in> sets F"
+    then have "e -` X \<inter> space E \<in> sets E"
+      using `e \<in> measurable E F` unfolding measurable_def by auto
+    then show "X \<in>(\<lambda>Y. f -` Y \<inter> space F) ` sets E"
+      apply (rule rev_image_eqI)
+      unfolding bij_inv_vimage_vimage[OF bi[simplified]]
+      using F `X \<in> sets F` by auto
+  next
+    fix X assume "X \<in> sets E" then show "f -` X \<inter> space F \<in> sets F"
+      using `f \<in> measurable F E` unfolding measurable_def by auto
+  qed
+  show "vimage_algebra (space (sigma F)) f = sigma F"
+    unfolding vimage_algebra_def
+    using assms by (auto simp: bij_inv_def eq sigma_sets_vimage[symmetric] sigma_def)
+qed
+
+lemma measurable_sigma_sigma:
+  assumes M: "sets M \<subseteq> Pow (space M)" and N: "sets N \<subseteq> Pow (space N)"
+  shows "f \<in> measurable M N \<Longrightarrow> f \<in> measurable (sigma M) (sigma N)"
+  using sigma_algebra.measurable_subset[OF sigma_algebra_sigma[OF M], of N]
+  using measurable_up_sigma[of M N] N by auto
+
+lemma bij_inv_the_inv_into:
+  assumes "bij_betw f A B" shows "bij_inv A B f (the_inv_into A f)"
+proof (rule bij_invI)
+  show "the_inv_into A f \<in> B \<rightarrow> A"
+    using bij_betw_the_inv_into[OF assms] by (rule bij_betw_imp_funcset)
+  show "f \<in> A \<rightarrow> B" using assms by (rule bij_betw_imp_funcset)
+  show "\<And>x. x \<in> A \<Longrightarrow> the_inv_into A f (f x) = x"
+    "\<And>x. x \<in> B \<Longrightarrow> f (the_inv_into A f x) = x"
+    using the_inv_into_f_f[of f A] f_the_inv_into_f[of f A]
+    using assms by (auto simp: bij_betw_def)
+qed
+
 end