author hoelzl Wed, 08 Dec 2010 16:15:14 +0100 changeset 41095 c335d880ff82 parent 41086 b4cccce25d9a child 41096 843c40bbc379
cleanup bijectivity btw. product spaces and pairs
```--- a/src/HOL/Probability/Information.thy	Wed Dec 08 18:07:04 2010 +0100
+++ b/src/HOL/Probability/Information.thy	Wed Dec 08 16:15:14 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>])
```
```--- a/src/HOL/Probability/Lebesgue_Integration.thy	Wed Dec 08 18:07:04 2010 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Wed Dec 08 16:15:14 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:```
```--- a/src/HOL/Probability/Lebesgue_Measure.thy	Wed Dec 08 18:07:04 2010 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Wed Dec 08 16:15:14 2010 +0100
@@ -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 *] .```
```--- a/src/HOL/Probability/Probability_Space.thy	Wed Dec 08 18:07:04 2010 +0100
+++ b/src/HOL/Probability/Probability_Space.thy	Wed Dec 08 16:15:14 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))"
-        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>"```
```--- a/src/HOL/Probability/Product_Measure.thy	Wed Dec 08 18:07:04 2010 +0100
+++ b/src/HOL/Probability/Product_Measure.thy	Wed Dec 08 16:15:14 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"

+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)"
@@ -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 @@
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 @@
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)"
-    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))"
@@ -1528,46 +1654,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 +1684,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 +1727,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)
@@ -1700,45 +1789,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 +1811,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 +1821,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]```
```--- a/src/HOL/Probability/Radon_Nikodym.thy	Wed Dec 08 18:07:04 2010 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Wed Dec 08 16:15:14 2010 +0100
@@ -1103,42 +1103,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
```
```--- a/src/HOL/Probability/Sigma_Algebra.thy	Wed Dec 08 18:07:04 2010 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Wed Dec 08 16:15:14 2010 +0100
@@ -806,13 +806,6 @@
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```