# HG changeset patch
# User hoelzl
# Date 1349863946 -7200
# Node ID 3c10763f5cb42ed41ff7f0ebea71702314671f8a
# Parent  d8de705b48d4ca476f40239a056c56549255efb2
show and use distributed_swap and distributed_jointI

diff -r d8de705b48d4 -r 3c10763f5cb4 src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Wed Oct 10 12:12:25 2012 +0200
+++ b/src/HOL/Probability/Information.thy	Wed Oct 10 12:12:26 2012 +0200
@@ -566,14 +566,13 @@
   entropy_Pow ("\<H>'(_')") where
   "\<H>(X) \<equiv> entropy b (count_space (X`space M)) X"
 
-lemma (in information_space) entropy_distr:
+lemma (in information_space)
   fixes X :: "'a \<Rightarrow> 'b"
   assumes X: "distributed M MX X f"
-  shows "entropy b MX X = - (\<integral>x. f x * log b (f x) \<partial>MX)"
-  unfolding entropy_def KL_divergence_def entropy_density_def comp_def
-proof (subst integral_cong_AE)
+  shows entropy_distr: "entropy b MX X = - (\<integral>x. f x * log b (f x) \<partial>MX)" (is ?eq)
+proof -
   note D = distributed_measurable[OF X] distributed_borel_measurable[OF X] distributed_AE[OF X]
-  interpret X: prob_space "distr M MX X"
+    interpret X: prob_space "distr M MX X"
     using D(1) by (rule prob_space_distr)
 
   have sf: "sigma_finite_measure (distr M MX X)" by default
@@ -582,7 +581,8 @@
     by (intro RN_deriv_unique_sigma_finite)
        (auto intro: divide_nonneg_nonneg measure_nonneg
              simp: distributed_distr_eq_density[symmetric, OF X] sf)
-  show "AE x in distr M MX X. log b (real (RN_deriv MX (distr M MX X) x)) =
+
+  have ae_eq: "AE x in distr M MX X. log b (real (RN_deriv MX (distr M MX X) x)) =
     log b (f x)"
     unfolding distributed_distr_eq_density[OF X]
     apply (subst AE_density)
@@ -591,12 +591,20 @@
     apply (subst (asm) eq_commute)
     apply auto
     done
-  show "- (\<integral> x. log b (f x) \<partial>distr M MX X) = - (\<integral> x. f x * log b (f x) \<partial>MX)"
+
+  have int_eq: "- (\<integral> x. log b (f x) \<partial>distr M MX X) = - (\<integral> x. f x * log b (f x) \<partial>MX)"
     unfolding distributed_distr_eq_density[OF X]
     using D
     by (subst integral_density)
        (auto simp: borel_measurable_ereal_iff)
-qed 
+
+  show ?eq
+    unfolding entropy_def KL_divergence_def entropy_density_def comp_def
+    apply (subst integral_cong_AE)
+    apply (rule ae_eq)
+    apply (rule int_eq)
+    done
+qed
 
 lemma (in prob_space) distributed_imp_emeasure_nonzero:
   assumes X: "distributed M MX X Px"
@@ -896,7 +904,7 @@
     using Pz by (intro TP.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
 
   have aeX3: "AE y in T \<Otimes>\<^isub>M P. (\<integral>\<^isup>+ x. ereal (Pxz (x, snd y)) \<partial>S) = ereal (Pz (snd y))"
-    using Pz distributed_marginal_eq_joint[OF P S Px Pz Pxz]
+    using Pz distributed_marginal_eq_joint2[OF P S Pz Pxz]
     apply (intro TP.AE_pair_measure)
     apply (auto simp: comp_def measurable_split_conv
                 intro!: measurable_snd'' borel_measurable_ereal_eq borel_measurable_ereal
@@ -1110,7 +1118,7 @@
   conditional_entropy_Pow ("\<H>'(_ | _')") where
   "\<H>(X | Y) \<equiv> conditional_entropy b (count_space (X`space M)) (count_space (Y`space M)) X Y"
 
-lemma (in information_space) conditional_entropy_generic_eq:
+lemma (in information_space)
   fixes Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"
   assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
   assumes Px: "distributed M S X Px"
@@ -1118,14 +1126,15 @@
   assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
   assumes I1: "integrable (S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Pxy x))"
   assumes I2: "integrable (S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Py (snd x)))"
-  shows "conditional_entropy b S T X Y = - (\<integral>(x, y). Pxy (x, y) * log b (Pxy (x, y) / Py y) \<partial>(S \<Otimes>\<^isub>M T))"
+  shows conditional_entropy_generic_eq: "conditional_entropy b S T X Y = - (\<integral>(x, y). Pxy (x, y) * log b (Pxy (x, y) / Py y) \<partial>(S \<Otimes>\<^isub>M T))" (is ?eq)
 proof -
   interpret S: sigma_finite_measure S by fact
   interpret T: sigma_finite_measure T by fact
   interpret ST: pair_sigma_finite S T ..
   have ST: "sigma_finite_measure (S \<Otimes>\<^isub>M T)" ..
 
-  interpret Pxy: prob_space "density (S \<Otimes>\<^isub>M T) Pxy"
+  let ?P = "density (S \<Otimes>\<^isub>M T) Pxy"
+  interpret Pxy: prob_space ?P
     unfolding Pxy[THEN distributed_distr_eq_density, symmetric]
     using Pxy[THEN distributed_measurable] by (rule prob_space_distr)
 
@@ -1140,23 +1149,23 @@
     by (subst distributed_transform_integral[OF Pxy Py, where T=snd]) (auto intro!: integral_cong)
   finally have e_eq: "entropy b T Y = - (\<integral>(x,y). Pxy (x,y) * log b (Py y) \<partial>(S \<Otimes>\<^isub>M T))" .
   
-  have "AE x in S \<Otimes>\<^isub>M T. Px (fst x) = 0 \<longrightarrow> Pxy x = 0"
+  have ae1: "AE x in S \<Otimes>\<^isub>M T. Px (fst x) = 0 \<longrightarrow> Pxy x = 0"
     by (intro subdensity_real[of fst, OF _ Pxy Px]) (auto intro: measurable_Pair)
-  moreover have "AE x in S \<Otimes>\<^isub>M T. Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
+  moreover have ae2: "AE x in S \<Otimes>\<^isub>M T. Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
     by (intro subdensity_real[of snd, OF _ Pxy Py]) (auto intro: measurable_Pair)
-  moreover have "AE x in S \<Otimes>\<^isub>M T. 0 \<le> Px (fst x)"
+  moreover have ae3: "AE x in S \<Otimes>\<^isub>M T. 0 \<le> Px (fst x)"
     using Px by (intro ST.AE_pair_measure) (auto simp: comp_def intro!: measurable_fst'' dest: distributed_real_AE distributed_real_measurable)
-  moreover have "AE x in S \<Otimes>\<^isub>M T. 0 \<le> Py (snd x)"
+  moreover have ae4: "AE x in S \<Otimes>\<^isub>M T. 0 \<le> Py (snd x)"
     using Py by (intro ST.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
-  moreover note Pxy[THEN distributed_real_AE]
+  moreover note ae5 = Pxy[THEN distributed_real_AE]
   ultimately have pos: "AE x in S \<Otimes>\<^isub>M T. 0 \<le> Pxy x \<and> 0 \<le> Px (fst x) \<and> 0 \<le> Py (snd x) \<and>
     (Pxy x = 0 \<or> (Pxy x \<noteq> 0 \<longrightarrow> 0 < Pxy x \<and> 0 < Px (fst x) \<and> 0 < Py (snd x)))"
     by eventually_elim auto
 
-  from pos have "AE x in S \<Otimes>\<^isub>M T.
+  from pos have ae: "AE x in S \<Otimes>\<^isub>M T.
      Pxy x * log b (Pxy x) - Pxy x * log b (Py (snd x)) = Pxy x * log b (Pxy x / Py (snd x))"
     by eventually_elim (auto simp: log_simps mult_pos_pos field_simps b_gt_1)
-  with I1 I2 show ?thesis
+  with I1 I2 show ?eq
     unfolding conditional_entropy_def
     apply (subst e_eq)
     apply (subst entropy_distr[OF Pxy])
diff -r d8de705b48d4 -r 3c10763f5cb4 src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Wed Oct 10 12:12:25 2012 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy	Wed Oct 10 12:12:26 2012 +0200
@@ -506,6 +506,16 @@
   shows "AE x in P. g (T x) = 0 \<longrightarrow> f x = 0"
   using subdensity[OF T, of M X "\<lambda>x. ereal (f x)" Y "\<lambda>x. ereal (g x)"] assms by auto
 
+lemma distributed_emeasure:
+  "distributed M N X f \<Longrightarrow> A \<in> sets N \<Longrightarrow> emeasure M (X -` A \<inter> space M) = (\<integral>\<^isup>+x. f x * indicator A x \<partial>N)"
+  by (auto simp: distributed_measurable distributed_AE distributed_borel_measurable
+                 distributed_distr_eq_density[symmetric] emeasure_density[symmetric] emeasure_distr)
+
+lemma distributed_positive_integral:
+  "distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> (\<integral>\<^isup>+x. f x * g x \<partial>N) = (\<integral>\<^isup>+x. g (X x) \<partial>M)"
+  by (auto simp: distributed_measurable distributed_AE distributed_borel_measurable
+                 distributed_distr_eq_density[symmetric] positive_integral_density[symmetric] positive_integral_distr)
+
 lemma distributed_integral:
   "distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> (\<integral>x. f x * g x \<partial>N) = (\<integral>x. g (X x) \<partial>M)"
   by (auto simp: distributed_real_measurable distributed_real_AE distributed_measurable
@@ -526,54 +536,116 @@
   finally show ?thesis .
 qed
 
-lemma distributed_marginal_eq_joint:
-  assumes T: "sigma_finite_measure T"
-  assumes S: "sigma_finite_measure S"
+lemma (in prob_space) distributed_unique:
   assumes Px: "distributed M S X Px"
-  assumes Py: "distributed M T Y Py"
-  assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
-  shows "AE y in T. Py y = (\<integral>\<^isup>+x. Pxy (x, y) \<partial>S)"
-proof (rule sigma_finite_measure.density_unique[OF T])
-  interpret ST: pair_sigma_finite S T using S T unfolding pair_sigma_finite_def by simp
-  show "Py \<in> borel_measurable T" "AE y in T. 0 \<le> Py y"
-    "(\<lambda>x. \<integral>\<^isup>+ xa. Pxy (xa, x) \<partial>S) \<in> borel_measurable T" "AE y in T. 0 \<le> \<integral>\<^isup>+ x. Pxy (x, y) \<partial>S"
-    using Pxy[THEN distributed_borel_measurable]
-    by (auto intro!: Py[THEN distributed_borel_measurable] Py[THEN distributed_AE]
-                     ST.positive_integral_snd_measurable' positive_integral_positive)
+  assumes Py: "distributed M S X Py"
+  shows "AE x in S. Px x = Py x"
+proof -
+  interpret X: prob_space "distr M S X"
+    using distributed_measurable[OF Px] by (rule prob_space_distr)
+  have "sigma_finite_measure (distr M S X)" ..
+  with sigma_finite_density_unique[of Px S Py ] Px Py
+  show ?thesis
+    by (auto simp: distributed_def)
+qed
+
+lemma (in prob_space) distributed_jointI:
+  assumes "sigma_finite_measure S" "sigma_finite_measure T"
+  assumes X[simp]: "X \<in> measurable M S" and Y[simp]: "Y \<in> measurable M T"
+  assumes f[simp]: "f \<in> borel_measurable (S \<Otimes>\<^isub>M T)" "AE x in S \<Otimes>\<^isub>M T. 0 \<le> f x"
+  assumes eq: "\<And>A B. A \<in> sets S \<Longrightarrow> B \<in> sets T \<Longrightarrow> 
+    emeasure M {x \<in> space M. X x \<in> A \<and> Y x \<in> B} = (\<integral>\<^isup>+x. (\<integral>\<^isup>+y. f (x, y) * indicator B y \<partial>T) * indicator A x \<partial>S)"
+  shows "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) f"
+  unfolding distributed_def
+proof safe
+  interpret S: sigma_finite_measure S by fact
+  interpret T: sigma_finite_measure T by fact
+  interpret ST: pair_sigma_finite S T by default
 
-  show "density T Py = density T (\<lambda>x. \<integral>\<^isup>+ xa. Pxy (xa, x) \<partial>S)"
-  proof (rule measure_eqI)
-    fix A assume A: "A \<in> sets (density T Py)"
-    have *: "\<And>x y. x \<in> space S \<Longrightarrow> indicator (space S \<times> A) (x, y) = indicator A y"
-      by (auto simp: indicator_def)
-    have "emeasure (density T Py) A = emeasure (distr M T Y) A"
-      unfolding Py[THEN distributed_distr_eq_density] ..
-    also have "\<dots> = emeasure (distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))) (space S \<times> A)"
-      using A Px Py Pxy
-      by (subst (1 2) emeasure_distr)
-         (auto dest: measurable_space distributed_measurable intro!: arg_cong[where f="emeasure M"])
-    also have "\<dots> = emeasure (density (S \<Otimes>\<^isub>M T) Pxy) (space S \<times> A)"
-      unfolding Pxy[THEN distributed_distr_eq_density] ..
-    also have "\<dots> = (\<integral>\<^isup>+ x. Pxy x * indicator (space S \<times> A) x \<partial>(S \<Otimes>\<^isub>M T))"
-      using A Pxy by (simp add: emeasure_density distributed_borel_measurable)
-    also have "\<dots> = (\<integral>\<^isup>+y. \<integral>\<^isup>+x. Pxy (x, y) * indicator (space S \<times> A) (x, y) \<partial>S \<partial>T)"
-      using A Pxy
-      by (subst ST.positive_integral_snd_measurable) (simp_all add: emeasure_density distributed_borel_measurable)
-    also have "\<dots> = (\<integral>\<^isup>+y. (\<integral>\<^isup>+x. Pxy (x, y) \<partial>S) * indicator A y \<partial>T)"
-      using measurable_comp[OF measurable_Pair1[OF measurable_ident] distributed_borel_measurable[OF Pxy]]
-      using distributed_borel_measurable[OF Pxy] distributed_AE[OF Pxy, THEN ST.AE_pair]
-      by (subst (asm) ST.AE_commute) (auto intro!: positive_integral_cong_AE positive_integral_multc cong: positive_integral_cong simp: * comp_def)
-    also have "\<dots> = emeasure (density T (\<lambda>x. \<integral>\<^isup>+ xa. Pxy (xa, x) \<partial>S)) A"
-      using A by (intro emeasure_density[symmetric])  (auto intro!: ST.positive_integral_snd_measurable' Pxy[THEN distributed_borel_measurable])
-    finally show "emeasure (density T Py) A = emeasure (density T (\<lambda>x. \<integral>\<^isup>+ xa. Pxy (xa, x) \<partial>S)) A" .
-  qed simp
+  from ST.sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('b \<times> 'c) set" .. note F = this
+  let ?E = "{a \<times> b |a b. a \<in> sets S \<and> b \<in> sets T}"
+  let ?P = "S \<Otimes>\<^isub>M T"
+  show "distr M ?P (\<lambda>x. (X x, Y x)) = density ?P f" (is "?L = ?R")
+  proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of S T]])
+    show "?E \<subseteq> Pow (space ?P)"
+      using space_closed[of S] space_closed[of T] by (auto simp: space_pair_measure)
+    show "sets ?L = sigma_sets (space ?P) ?E"
+      by (simp add: sets_pair_measure space_pair_measure)
+    then show "sets ?R = sigma_sets (space ?P) ?E"
+      by simp
+  next
+    interpret L: prob_space ?L
+      by (rule prob_space_distr) (auto intro!: measurable_Pair)
+    show "range F \<subseteq> ?E" "(\<Union>i. F i) = space ?P" "\<And>i. emeasure ?L (F i) \<noteq> \<infinity>"
+      using F by (auto simp: space_pair_measure)
+  next
+    fix E assume "E \<in> ?E"
+    then obtain A B where E[simp]: "E = A \<times> B" and A[simp]: "A \<in> sets S" and B[simp]: "B \<in> sets T" by auto
+    have "emeasure ?L E = emeasure M {x \<in> space M. X x \<in> A \<and> Y x \<in> B}"
+      by (auto intro!: arg_cong[where f="emeasure M"] simp add: emeasure_distr measurable_Pair)
+    also have "\<dots> = (\<integral>\<^isup>+x. (\<integral>\<^isup>+y. (f (x, y) * indicator B y) * indicator A x \<partial>T) \<partial>S)"
+      by (auto simp add: eq measurable_Pair measurable_compose[OF _ f(1)] positive_integral_multc
+               intro!: positive_integral_cong)
+    also have "\<dots> = emeasure ?R E"
+      by (auto simp add: emeasure_density ST.positive_integral_fst_measurable(2)[symmetric]
+               intro!: positive_integral_cong split: split_indicator)
+    finally show "emeasure ?L E = emeasure ?R E" .
+  qed
+qed (auto intro!: measurable_Pair)
+
+lemma (in prob_space) distributed_swap:
+  assumes "sigma_finite_measure S" "sigma_finite_measure T"
+  assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
+  shows "distributed M (T \<Otimes>\<^isub>M S) (\<lambda>x. (Y x, X x)) (\<lambda>(x, y). Pxy (y, x))"
+proof -
+  interpret S: sigma_finite_measure S by fact
+  interpret T: sigma_finite_measure T by fact
+  interpret ST: pair_sigma_finite S T by default
+  interpret TS: pair_sigma_finite T S by default
+
+  note measurable_Pxy = measurable_compose[OF _ distributed_borel_measurable[OF Pxy]]
+  show ?thesis 
+    apply (subst TS.distr_pair_swap)
+    unfolding distributed_def
+  proof safe
+    let ?D = "distr (S \<Otimes>\<^isub>M T) (T \<Otimes>\<^isub>M S) (\<lambda>(x, y). (y, x))"
+    show 1: "(\<lambda>(x, y). Pxy (y, x)) \<in> borel_measurable ?D"
+      by (auto simp: measurable_split_conv intro!: measurable_Pair measurable_Pxy)
+    with Pxy
+    show "AE x in distr (S \<Otimes>\<^isub>M T) (T \<Otimes>\<^isub>M S) (\<lambda>(x, y). (y, x)). 0 \<le> (case x of (x, y) \<Rightarrow> Pxy (y, x))"
+      by (subst AE_distr_iff)
+         (auto dest!: distributed_AE
+               simp: measurable_split_conv split_beta
+               intro!: measurable_Pair borel_measurable_ereal_le)
+    show 2: "random_variable (distr (S \<Otimes>\<^isub>M T) (T \<Otimes>\<^isub>M S) (\<lambda>(x, y). (y, x))) (\<lambda>x. (Y x, X x))"
+      using measurable_compose[OF distributed_measurable[OF Pxy] measurable_fst]
+      using measurable_compose[OF distributed_measurable[OF Pxy] measurable_snd]
+      by (auto intro!: measurable_Pair)
+    { fix A assume A: "A \<in> sets (T \<Otimes>\<^isub>M S)"
+      let ?B = "(\<lambda>(x, y). (y, x)) -` A \<inter> space (S \<Otimes>\<^isub>M T)"
+      from sets_into_space[OF A]
+      have "emeasure M ((\<lambda>x. (Y x, X x)) -` A \<inter> space M) =
+        emeasure M ((\<lambda>x. (X x, Y x)) -` ?B \<inter> space M)"
+        by (auto intro!: arg_cong2[where f=emeasure] simp: space_pair_measure)
+      also have "\<dots> = (\<integral>\<^isup>+ x. Pxy x * indicator ?B x \<partial>(S \<Otimes>\<^isub>M T))"
+        using Pxy A by (intro distributed_emeasure measurable_sets) (auto simp: measurable_split_conv measurable_Pair)
+      finally have "emeasure M ((\<lambda>x. (Y x, X x)) -` A \<inter> space M) =
+        (\<integral>\<^isup>+ x. Pxy x * indicator A (snd x, fst x) \<partial>(S \<Otimes>\<^isub>M T))"
+        by (auto intro!: positive_integral_cong split: split_indicator) }
+    note * = this
+    show "distr M ?D (\<lambda>x. (Y x, X x)) = density ?D (\<lambda>(x, y). Pxy (y, x))"
+      apply (intro measure_eqI)
+      apply (simp_all add: emeasure_distr[OF 2] emeasure_density[OF 1])
+      apply (subst positive_integral_distr)
+      apply (auto intro!: measurable_pair measurable_Pxy * simp: comp_def split_beta)
+      done
+  qed
 qed
 
 lemma (in prob_space) distr_marginal1:
-  fixes Pxy :: "('b \<times> 'c) \<Rightarrow> real"
   assumes "sigma_finite_measure S" "sigma_finite_measure T"
   assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
-  defines "Px \<equiv> \<lambda>x. real (\<integral>\<^isup>+z. Pxy (x, z) \<partial>T)"
+  defines "Px \<equiv> \<lambda>x. (\<integral>\<^isup>+z. Pxy (x, z) \<partial>T)"
   shows "distributed M S X Px"
   unfolding distributed_def
 proof safe
@@ -588,18 +660,15 @@
   from XY have Y: "Y \<in> measurable M T"
     unfolding measurable_pair_iff by (simp add: comp_def)
 
-  from Pxy show borel: "(\<lambda>x. ereal (Px x)) \<in> borel_measurable S"
-    by (auto intro!: ST.positive_integral_fst_measurable borel_measurable_real_of_ereal dest!: distributed_real_measurable simp: Px_def)
+  from Pxy show borel: "Px \<in> borel_measurable S"
+    by (auto intro!: ST.positive_integral_fst_measurable dest!: distributed_borel_measurable simp: Px_def)
 
   interpret Pxy: prob_space "distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
     using XY by (rule prob_space_distr)
-  have "(\<integral>\<^isup>+ x. max 0 (ereal (- Pxy x)) \<partial>(S \<Otimes>\<^isub>M T)) = (\<integral>\<^isup>+ x. 0 \<partial>(S \<Otimes>\<^isub>M T))"
+  have "(\<integral>\<^isup>+ x. max 0 (- Pxy x) \<partial>(S \<Otimes>\<^isub>M T)) = (\<integral>\<^isup>+ x. 0 \<partial>(S \<Otimes>\<^isub>M T))"
     using Pxy
-    by (intro positive_integral_cong_AE) (auto simp: max_def dest: distributed_real_measurable distributed_real_AE)
-  then have Pxy_integrable: "integrable (S \<Otimes>\<^isub>M T) Pxy"
-    using Pxy Pxy.emeasure_space_1
-    by (simp add: integrable_def emeasure_density positive_integral_max_0 distributed_def borel_measurable_ereal_iff cong: positive_integral_cong)
-    
+    by (intro positive_integral_cong_AE) (auto simp: max_def dest: distributed_borel_measurable distributed_AE)
+
   show "distr M S X = density S Px"
   proof (rule measure_eqI)
     fix A assume A: "A \<in> sets (distr M S X)"
@@ -608,31 +677,52 @@
                intro!: arg_cong[where f="emeasure M"] dest: measurable_space)
     also have "\<dots> = emeasure (density (S \<Otimes>\<^isub>M T) Pxy) (A \<times> space T)"
       using Pxy by (simp add: distributed_def)
-    also have "\<dots> = \<integral>\<^isup>+ x. \<integral>\<^isup>+ y. ereal (Pxy (x, y)) * indicator (A \<times> space T) (x, y) \<partial>T \<partial>S"
+    also have "\<dots> = \<integral>\<^isup>+ x. \<integral>\<^isup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T \<partial>S"
       using A borel Pxy
       by (simp add: emeasure_density ST.positive_integral_fst_measurable(2)[symmetric] distributed_def)
-    also have "\<dots> = \<integral>\<^isup>+ x. ereal (Px x) * indicator A x \<partial>S"
+    also have "\<dots> = \<integral>\<^isup>+ x. Px x * indicator A x \<partial>S"
       apply (rule positive_integral_cong_AE)
-      using Pxy[THEN distributed_real_AE, THEN ST.AE_pair] ST.integrable_fst_measurable(1)[OF Pxy_integrable] AE_space
+      using Pxy[THEN distributed_AE, THEN ST.AE_pair] AE_space
     proof eventually_elim
-      fix x assume "x \<in> space S" "AE y in T. 0 \<le> Pxy (x, y)" and i: "integrable T (\<lambda>y. Pxy (x, y))"
+      fix x assume "x \<in> space S" "AE y in T. 0 \<le> Pxy (x, y)"
       moreover have eq: "\<And>y. y \<in> space T \<Longrightarrow> indicator (A \<times> space T) (x, y) = indicator A x"
         by (auto simp: indicator_def)
-      ultimately have "(\<integral>\<^isup>+ y. ereal (Pxy (x, y)) * indicator (A \<times> space T) (x, y) \<partial>T) =
-          (\<integral>\<^isup>+ y. ereal (Pxy (x, y)) \<partial>T) * indicator A x"
-        using Pxy[THEN distributed_real_measurable] by (simp add: eq positive_integral_multc measurable_Pair2 cong: positive_integral_cong)
-      also have "(\<integral>\<^isup>+ y. ereal (Pxy (x, y)) \<partial>T) = Px x"
-        using i by (simp add: Px_def ereal_real integrable_def positive_integral_positive)
-      finally show "(\<integral>\<^isup>+ y. ereal (Pxy (x, y)) * indicator (A \<times> space T) (x, y) \<partial>T) = ereal (Px x) * indicator A x" .
+      ultimately have "(\<integral>\<^isup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T) = (\<integral>\<^isup>+ y. Pxy (x, y) \<partial>T) * indicator A x"
+        using Pxy[THEN distributed_borel_measurable] by (simp add: eq positive_integral_multc measurable_Pair2 cong: positive_integral_cong)
+      also have "(\<integral>\<^isup>+ y. Pxy (x, y) \<partial>T) = Px x"
+        by (simp add: Px_def ereal_real positive_integral_positive)
+      finally show "(\<integral>\<^isup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T) = Px x * indicator A x" .
     qed
     finally show "emeasure (distr M S X) A = emeasure (density S Px) A"
       using A borel Pxy by (simp add: emeasure_density)
   qed simp
   
-  show "AE x in S. 0 \<le> ereal (Px x)"
+  show "AE x in S. 0 \<le> Px x"
     by (simp add: Px_def positive_integral_positive real_of_ereal_pos)
 qed
 
+lemma (in prob_space) distr_marginal2:
+  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
+  assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
+  shows "distributed M T Y (\<lambda>y. (\<integral>\<^isup>+x. Pxy (x, y) \<partial>S))"
+  using distr_marginal1[OF T S distributed_swap[OF S T]] Pxy by simp
+
+lemma (in prob_space) distributed_marginal_eq_joint1:
+  assumes T: "sigma_finite_measure T"
+  assumes S: "sigma_finite_measure S"
+  assumes Px: "distributed M S X Px"
+  assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
+  shows "AE x in S. Px x = (\<integral>\<^isup>+y. Pxy (x, y) \<partial>T)"
+  using Px distr_marginal1[OF S T Pxy] by (rule distributed_unique)
+
+lemma (in prob_space) distributed_marginal_eq_joint2:
+  assumes T: "sigma_finite_measure T"
+  assumes S: "sigma_finite_measure S"
+  assumes Py: "distributed M T Y Py"
+  assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
+  shows "AE y in T. Py y = (\<integral>\<^isup>+x. Pxy (x, y) \<partial>S)"
+  using Py distr_marginal2[OF S T Pxy] by (rule distributed_unique)
+
 definition
   "simple_distributed M X f \<longleftrightarrow> distributed M (count_space (X`space M)) X (\<lambda>x. ereal (f x)) \<and>
     finite (X`space M)"
@@ -795,19 +885,21 @@
   note Px = simple_distributedI[OF Px refl]
   have *: "\<And>f A. setsum (\<lambda>x. max 0 (ereal (f x))) A = ereal (setsum (\<lambda>x. max 0 (f x)) A)"
     by (simp add: setsum_ereal[symmetric] zero_ereal_def)
-  from distributed_marginal_eq_joint[OF sigma_finite_measure_count_space_finite sigma_finite_measure_count_space_finite
-    simple_distributed[OF Px] simple_distributed[OF Py] simple_distributed_joint[OF Pxy],
+  from distributed_marginal_eq_joint2[OF
+    sigma_finite_measure_count_space_finite
+    sigma_finite_measure_count_space_finite
+    simple_distributed[OF Py] simple_distributed_joint[OF Pxy],
     OF Py[THEN simple_distributed_finite] Px[THEN simple_distributed_finite]]
-    y Px[THEN simple_distributed_finite] Py[THEN simple_distributed_finite]
+    y
+    Px[THEN simple_distributed_finite]
+    Py[THEN simple_distributed_finite]
     Pxy[THEN simple_distributed, THEN distributed_real_AE]
   show ?thesis
     unfolding AE_count_space
-    apply (elim ballE[where x=y])
     apply (auto simp add: positive_integral_count_space_finite * intro!: setsum_cong split: split_max)
     done
 qed
 
-
 lemma prob_space_uniform_measure:
   assumes A: "emeasure M A \<noteq> 0" "emeasure M A \<noteq> \<infinity>"
   shows "prob_space (uniform_measure M A)"