joint distribution of independent variables

--- a/src/HOL/Probability/Independent_Family.thy	Wed Oct 10 12:12:30 2012 +0200
+++ b/src/HOL/Probability/Independent_Family.thy	Wed Oct 10 12:12:31 2012 +0200
@@ -1170,4 +1170,12 @@
   qed
 qed
 
+lemma (in prob_space) distributed_joint_indep:
+  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
+  assumes X: "distributed M S X Px" and Y: "distributed M T Y Py"
+  assumes indep: "indep_var S X T Y"
+  shows "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) (\<lambda>(x, y). Px x * Py y)"
+  using indep_var_distribution_eq[of S X T Y] indep
+  by (intro distributed_joint_indep'[OF S T X Y]) auto
+
 end

--- a/src/HOL/Probability/Lebesgue_Integration.thy	Wed Oct 10 12:12:30 2012 +0200
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Wed Oct 10 12:12:31 2012 +0200
@@ -2611,9 +2611,14 @@
 qed
 
 lemma emeasure_point_measure_finite:
-  "finite A \<Longrightarrow> (\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> X \<subseteq> A \<Longrightarrow> emeasure (point_measure A f) X = (\<Sum>a|a\<in>X. f a)"
+  "finite A \<Longrightarrow> (\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> X \<subseteq> A \<Longrightarrow> emeasure (point_measure A f) X = (\<Sum>a\<in>X. f a)"
   by (subst emeasure_point_measure) (auto dest: finite_subset intro!: setsum_mono_zero_left simp: less_le)
 
+lemma emeasure_point_measure_finite2:
+  "X \<subseteq> A \<Longrightarrow> finite X \<Longrightarrow> (\<And>i. i \<in> X \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> emeasure (point_measure A f) X = (\<Sum>a\<in>X. f a)"
+  by (subst emeasure_point_measure)
+     (auto dest: finite_subset intro!: setsum_mono_zero_left simp: less_le)
+
 lemma null_sets_point_measure_iff:
   "X \<in> null_sets (point_measure A f) \<longleftrightarrow> X \<subseteq> A \<and> (\<forall>x\<in>X. f x \<le> 0)"
  by (auto simp: AE_count_space null_sets_density_iff point_measure_def)

--- a/src/HOL/Probability/Probability_Measure.thy	Wed Oct 10 12:12:30 2012 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy	Wed Oct 10 12:12:31 2012 +0200
@@ -723,6 +723,54 @@
   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)
 
+lemma (in prob_space) distributed_joint_indep':
+  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
+  assumes X: "distributed M S X Px" and Y: "distributed M T Y Py"
+  assumes indep: "distr M S X \<Otimes>\<^isub>M distr M T Y = distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
+  shows "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) (\<lambda>(x, y). Px x * Py y)"
+  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
+
+  interpret X: prob_space "density S Px"
+    unfolding distributed_distr_eq_density[OF X, symmetric]
+    using distributed_measurable[OF X]
+    by (rule prob_space_distr)
+  have sf_X: "sigma_finite_measure (density S Px)" ..
+
+  interpret Y: prob_space "density T Py"
+    unfolding distributed_distr_eq_density[OF Y, symmetric]
+    using distributed_measurable[OF Y]
+    by (rule prob_space_distr)
+  have sf_Y: "sigma_finite_measure (density T Py)" ..
+
+  show "distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) = density (S \<Otimes>\<^isub>M T) (\<lambda>(x, y). Px x * Py y)"
+    unfolding indep[symmetric] distributed_distr_eq_density[OF X] distributed_distr_eq_density[OF Y]
+    using distributed_borel_measurable[OF X] distributed_AE[OF X]
+    using distributed_borel_measurable[OF Y] distributed_AE[OF Y]
+    by (rule pair_measure_density[OF _ _ _ _ S T sf_X sf_Y])
+
+  show "random_variable (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
+    using distributed_measurable[OF X] distributed_measurable[OF Y]
+    by (auto intro: measurable_Pair)
+
+  show Pxy: "(\<lambda>(x, y). Px x * Py y) \<in> borel_measurable (S \<Otimes>\<^isub>M T)"
+    by (auto simp: split_beta' 
+             intro!: measurable_compose[OF _ distributed_borel_measurable[OF X]]
+                     measurable_compose[OF _ distributed_borel_measurable[OF Y]])
+
+  show "AE x in S \<Otimes>\<^isub>M T. 0 \<le> (case x of (x, y) \<Rightarrow> Px x * Py y)"
+    apply (intro ST.AE_pair_measure borel_measurable_ereal_le Pxy borel_measurable_const)
+    using distributed_AE[OF X]
+    apply eventually_elim
+    using distributed_AE[OF Y]
+    apply eventually_elim
+    apply auto
+    done
+qed
+
 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)"