721 assumes Py: "distributed M T Y Py" |
721 assumes Py: "distributed M T Y Py" |
722 assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy" |
722 assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy" |
723 shows "AE y in T. Py y = (\<integral>\<^isup>+x. Pxy (x, y) \<partial>S)" |
723 shows "AE y in T. Py y = (\<integral>\<^isup>+x. Pxy (x, y) \<partial>S)" |
724 using Py distr_marginal2[OF S T Pxy] by (rule distributed_unique) |
724 using Py distr_marginal2[OF S T Pxy] by (rule distributed_unique) |
725 |
725 |
|
726 lemma (in prob_space) distributed_joint_indep': |
|
727 assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T" |
|
728 assumes X: "distributed M S X Px" and Y: "distributed M T Y Py" |
|
729 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))" |
|
730 shows "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) (\<lambda>(x, y). Px x * Py y)" |
|
731 unfolding distributed_def |
|
732 proof safe |
|
733 interpret S: sigma_finite_measure S by fact |
|
734 interpret T: sigma_finite_measure T by fact |
|
735 interpret ST: pair_sigma_finite S T by default |
|
736 |
|
737 interpret X: prob_space "density S Px" |
|
738 unfolding distributed_distr_eq_density[OF X, symmetric] |
|
739 using distributed_measurable[OF X] |
|
740 by (rule prob_space_distr) |
|
741 have sf_X: "sigma_finite_measure (density S Px)" .. |
|
742 |
|
743 interpret Y: prob_space "density T Py" |
|
744 unfolding distributed_distr_eq_density[OF Y, symmetric] |
|
745 using distributed_measurable[OF Y] |
|
746 by (rule prob_space_distr) |
|
747 have sf_Y: "sigma_finite_measure (density T Py)" .. |
|
748 |
|
749 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)" |
|
750 unfolding indep[symmetric] distributed_distr_eq_density[OF X] distributed_distr_eq_density[OF Y] |
|
751 using distributed_borel_measurable[OF X] distributed_AE[OF X] |
|
752 using distributed_borel_measurable[OF Y] distributed_AE[OF Y] |
|
753 by (rule pair_measure_density[OF _ _ _ _ S T sf_X sf_Y]) |
|
754 |
|
755 show "random_variable (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))" |
|
756 using distributed_measurable[OF X] distributed_measurable[OF Y] |
|
757 by (auto intro: measurable_Pair) |
|
758 |
|
759 show Pxy: "(\<lambda>(x, y). Px x * Py y) \<in> borel_measurable (S \<Otimes>\<^isub>M T)" |
|
760 by (auto simp: split_beta' |
|
761 intro!: measurable_compose[OF _ distributed_borel_measurable[OF X]] |
|
762 measurable_compose[OF _ distributed_borel_measurable[OF Y]]) |
|
763 |
|
764 show "AE x in S \<Otimes>\<^isub>M T. 0 \<le> (case x of (x, y) \<Rightarrow> Px x * Py y)" |
|
765 apply (intro ST.AE_pair_measure borel_measurable_ereal_le Pxy borel_measurable_const) |
|
766 using distributed_AE[OF X] |
|
767 apply eventually_elim |
|
768 using distributed_AE[OF Y] |
|
769 apply eventually_elim |
|
770 apply auto |
|
771 done |
|
772 qed |
|
773 |
726 definition |
774 definition |
727 "simple_distributed M X f \<longleftrightarrow> distributed M (count_space (X`space M)) X (\<lambda>x. ereal (f x)) \<and> |
775 "simple_distributed M X f \<longleftrightarrow> distributed M (count_space (X`space M)) X (\<lambda>x. ereal (f x)) \<and> |
728 finite (X`space M)" |
776 finite (X`space M)" |
729 |
777 |
730 lemma simple_distributed: |
778 lemma simple_distributed: |