# HG changeset patch # User hoelzl # Date 1349863951 -7200 # Node ID 9f2fb9b25a770b70f884270e6acf76676fd108e2 # Parent 3c7b5988e09409caff2433746ddfe4b07a0b98e6 joint distribution of independent variables diff -r 3c7b5988e094 -r 9f2fb9b25a77 src/HOL/Probability/Independent_Family.thy --- 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 \\<^isub>M T) (\x. (X x, Y x)) (\(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 diff -r 3c7b5988e094 -r 9f2fb9b25a77 src/HOL/Probability/Lebesgue_Integration.thy --- 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 \ (\i. i \ A \ 0 \ f i) \ X \ A \ emeasure (point_measure A f) X = (\a|a\X. f a)" + "finite A \ (\i. i \ A \ 0 \ f i) \ X \ A \ emeasure (point_measure A f) X = (\a\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 \ A \ finite X \ (\i. i \ X \ 0 \ f i) \ emeasure (point_measure A f) X = (\a\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 \ null_sets (point_measure A f) \ X \ A \ (\x\X. f x \ 0)" by (auto simp: AE_count_space null_sets_density_iff point_measure_def) diff -r 3c7b5988e094 -r 9f2fb9b25a77 src/HOL/Probability/Probability_Measure.thy --- 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 = (\\<^isup>+x. Pxy (x, y) \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 \\<^isub>M distr M T Y = distr M (S \\<^isub>M T) (\x. (X x, Y x))" + shows "distributed M (S \\<^isub>M T) (\x. (X x, Y x)) (\(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 \\<^isub>M T) (\x. (X x, Y x)) = density (S \\<^isub>M T) (\(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 \\<^isub>M T) (\x. (X x, Y x))" + using distributed_measurable[OF X] distributed_measurable[OF Y] + by (auto intro: measurable_Pair) + + show Pxy: "(\(x, y). Px x * Py y) \ borel_measurable (S \\<^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 \\<^isub>M T. 0 \ (case x of (x, y) \ 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 \ distributed M (count_space (X`space M)) X (\x. ereal (f x)) \ finite (X`space M)"