equal
deleted
inserted
replaced
793 have P_borel: "(\<lambda>x. f (merge I J x)) \<in> borel_measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M)" |
793 have P_borel: "(\<lambda>x. f (merge I J x)) \<in> borel_measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M)" |
794 using measurable_comp[OF measurable_merge f] by (simp add: comp_def) |
794 using measurable_comp[OF measurable_merge f] by (simp add: comp_def) |
795 show ?thesis |
795 show ?thesis |
796 apply (subst distr_merge[OF IJ, symmetric]) |
796 apply (subst distr_merge[OF IJ, symmetric]) |
797 apply (subst positive_integral_distr[OF measurable_merge f]) |
797 apply (subst positive_integral_distr[OF measurable_merge f]) |
798 apply (subst P.positive_integral_fst_measurable(2)[symmetric, OF P_borel]) |
798 apply (subst J.positive_integral_fst_measurable(2)[symmetric, OF P_borel]) |
799 apply simp |
799 apply simp |
800 done |
800 done |
801 qed |
801 qed |
802 |
802 |
803 lemma (in product_sigma_finite) distr_singleton: |
803 lemma (in product_sigma_finite) distr_singleton: |