joint distribution of independent variables
authorhoelzl
Wed Oct 10 12:12:31 2012 +0200 (2012-10-10)
changeset 497959f2fb9b25a77
parent 49794 3c7b5988e094
child 49796 182fa22e7ee8
joint distribution of independent variables
src/HOL/Probability/Independent_Family.thy
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Probability/Probability_Measure.thy
     1.1 --- a/src/HOL/Probability/Independent_Family.thy	Wed Oct 10 12:12:30 2012 +0200
     1.2 +++ b/src/HOL/Probability/Independent_Family.thy	Wed Oct 10 12:12:31 2012 +0200
     1.3 @@ -1170,4 +1170,12 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 +lemma (in prob_space) distributed_joint_indep:
     1.8 +  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
     1.9 +  assumes X: "distributed M S X Px" and Y: "distributed M T Y Py"
    1.10 +  assumes indep: "indep_var S X T Y"
    1.11 +  shows "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) (\<lambda>(x, y). Px x * Py y)"
    1.12 +  using indep_var_distribution_eq[of S X T Y] indep
    1.13 +  by (intro distributed_joint_indep'[OF S T X Y]) auto
    1.14 +
    1.15  end
     2.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Wed Oct 10 12:12:30 2012 +0200
     2.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Wed Oct 10 12:12:31 2012 +0200
     2.3 @@ -2611,9 +2611,14 @@
     2.4  qed
     2.5  
     2.6  lemma emeasure_point_measure_finite:
     2.7 -  "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)"
     2.8 +  "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)"
     2.9    by (subst emeasure_point_measure) (auto dest: finite_subset intro!: setsum_mono_zero_left simp: less_le)
    2.10  
    2.11 +lemma emeasure_point_measure_finite2:
    2.12 +  "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)"
    2.13 +  by (subst emeasure_point_measure)
    2.14 +     (auto dest: finite_subset intro!: setsum_mono_zero_left simp: less_le)
    2.15 +
    2.16  lemma null_sets_point_measure_iff:
    2.17    "X \<in> null_sets (point_measure A f) \<longleftrightarrow> X \<subseteq> A \<and> (\<forall>x\<in>X. f x \<le> 0)"
    2.18   by (auto simp: AE_count_space null_sets_density_iff point_measure_def)
     3.1 --- a/src/HOL/Probability/Probability_Measure.thy	Wed Oct 10 12:12:30 2012 +0200
     3.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Wed Oct 10 12:12:31 2012 +0200
     3.3 @@ -723,6 +723,54 @@
     3.4    shows "AE y in T. Py y = (\<integral>\<^isup>+x. Pxy (x, y) \<partial>S)"
     3.5    using Py distr_marginal2[OF S T Pxy] by (rule distributed_unique)
     3.6  
     3.7 +lemma (in prob_space) distributed_joint_indep':
     3.8 +  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
     3.9 +  assumes X: "distributed M S X Px" and Y: "distributed M T Y Py"
    3.10 +  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))"
    3.11 +  shows "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) (\<lambda>(x, y). Px x * Py y)"
    3.12 +  unfolding distributed_def
    3.13 +proof safe
    3.14 +  interpret S: sigma_finite_measure S by fact
    3.15 +  interpret T: sigma_finite_measure T by fact
    3.16 +  interpret ST: pair_sigma_finite S T by default
    3.17 +
    3.18 +  interpret X: prob_space "density S Px"
    3.19 +    unfolding distributed_distr_eq_density[OF X, symmetric]
    3.20 +    using distributed_measurable[OF X]
    3.21 +    by (rule prob_space_distr)
    3.22 +  have sf_X: "sigma_finite_measure (density S Px)" ..
    3.23 +
    3.24 +  interpret Y: prob_space "density T Py"
    3.25 +    unfolding distributed_distr_eq_density[OF Y, symmetric]
    3.26 +    using distributed_measurable[OF Y]
    3.27 +    by (rule prob_space_distr)
    3.28 +  have sf_Y: "sigma_finite_measure (density T Py)" ..
    3.29 +
    3.30 +  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)"
    3.31 +    unfolding indep[symmetric] distributed_distr_eq_density[OF X] distributed_distr_eq_density[OF Y]
    3.32 +    using distributed_borel_measurable[OF X] distributed_AE[OF X]
    3.33 +    using distributed_borel_measurable[OF Y] distributed_AE[OF Y]
    3.34 +    by (rule pair_measure_density[OF _ _ _ _ S T sf_X sf_Y])
    3.35 +
    3.36 +  show "random_variable (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
    3.37 +    using distributed_measurable[OF X] distributed_measurable[OF Y]
    3.38 +    by (auto intro: measurable_Pair)
    3.39 +
    3.40 +  show Pxy: "(\<lambda>(x, y). Px x * Py y) \<in> borel_measurable (S \<Otimes>\<^isub>M T)"
    3.41 +    by (auto simp: split_beta' 
    3.42 +             intro!: measurable_compose[OF _ distributed_borel_measurable[OF X]]
    3.43 +                     measurable_compose[OF _ distributed_borel_measurable[OF Y]])
    3.44 +
    3.45 +  show "AE x in S \<Otimes>\<^isub>M T. 0 \<le> (case x of (x, y) \<Rightarrow> Px x * Py y)"
    3.46 +    apply (intro ST.AE_pair_measure borel_measurable_ereal_le Pxy borel_measurable_const)
    3.47 +    using distributed_AE[OF X]
    3.48 +    apply eventually_elim
    3.49 +    using distributed_AE[OF Y]
    3.50 +    apply eventually_elim
    3.51 +    apply auto
    3.52 +    done
    3.53 +qed
    3.54 +
    3.55  definition
    3.56    "simple_distributed M X f \<longleftrightarrow> distributed M (count_space (X`space M)) X (\<lambda>x. ereal (f x)) \<and>
    3.57      finite (X`space M)"