270 by (intro measurable_cong nn_integral_cong cong) |
270 by (intro measurable_cong nn_integral_cong cong) |
271 (auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq) |
271 (auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq) |
272 ultimately show ?case by simp |
272 ultimately show ?case by simp |
273 next |
273 next |
274 case (set B) |
274 case (set B) |
275 moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. indicator B M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. emeasure M' B) \<in> ?B" |
275 then have "(\<lambda>M'. \<integral>\<^sup>+M''. indicator B M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. emeasure M' B) \<in> ?B" |
276 by (intro measurable_cong nn_integral_indicator) (simp add: space_subprob_algebra) |
276 by (intro measurable_cong nn_integral_indicator) (simp add: space_subprob_algebra) |
277 ultimately show ?case |
277 with set show ?case |
278 by (simp add: measurable_emeasure_subprob_algebra) |
278 by (simp add: measurable_emeasure_subprob_algebra) |
279 next |
279 next |
280 case (mult f c) |
280 case (mult f c) |
281 moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. c * f M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. c * \<integral>\<^sup>+M''. f M'' \<partial>M') \<in> ?B" |
281 then have "(\<lambda>M'. \<integral>\<^sup>+M''. c * f M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. c * \<integral>\<^sup>+M''. f M'' \<partial>M') \<in> ?B" |
282 by (intro measurable_cong nn_integral_cmult) (auto simp add: space_subprob_algebra) |
282 by (intro measurable_cong nn_integral_cmult) (auto simp add: space_subprob_algebra) |
283 ultimately show ?case |
283 with mult show ?case |
284 by simp |
284 by simp |
285 next |
285 next |
286 case (add f g) |
286 case (add f g) |
287 moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. f M'' + g M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. (\<integral>\<^sup>+M''. f M'' \<partial>M') + (\<integral>\<^sup>+M''. g M'' \<partial>M')) \<in> ?B" |
287 then have "(\<lambda>M'. \<integral>\<^sup>+M''. f M'' + g M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. (\<integral>\<^sup>+M''. f M'' \<partial>M') + (\<integral>\<^sup>+M''. g M'' \<partial>M')) \<in> ?B" |
288 by (intro measurable_cong nn_integral_add) (auto simp add: space_subprob_algebra) |
288 by (intro measurable_cong nn_integral_add) (auto simp add: space_subprob_algebra) |
289 ultimately show ?case |
289 with add show ?case |
290 by (simp add: ac_simps) |
290 by (simp add: ac_simps) |
291 next |
291 next |
292 case (seq F) |
292 case (seq F) |
293 moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. (SUP i. F i) M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. SUP i. (\<integral>\<^sup>+M''. F i M'' \<partial>M')) \<in> ?B" |
293 then have "(\<lambda>M'. \<integral>\<^sup>+M''. (SUP i. F i) M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. SUP i. (\<integral>\<^sup>+M''. F i M'' \<partial>M')) \<in> ?B" |
294 unfolding SUP_apply |
294 unfolding SUP_apply |
295 by (intro measurable_cong nn_integral_monotone_convergence_SUP) (auto simp add: space_subprob_algebra) |
295 by (intro measurable_cong nn_integral_monotone_convergence_SUP) (auto simp add: space_subprob_algebra) |
296 ultimately show ?case |
296 with seq show ?case |
297 by (simp add: ac_simps) |
297 by (simp add: ac_simps) |
298 qed |
298 qed |
299 |
299 |
300 lemma measurable_distr: |
300 lemma measurable_distr: |
301 assumes [measurable]: "f \<in> measurable M N" |
301 assumes [measurable]: "f \<in> measurable M N" |
791 (auto simp add: space_subprob_algebra dest!: sets_eq_imp_space_eq) |
791 (auto simp add: space_subprob_algebra dest!: sets_eq_imp_space_eq) |
792 ultimately show ?case |
792 ultimately show ?case |
793 by simp |
793 by simp |
794 next |
794 next |
795 case (set A) |
795 case (set A) |
796 moreover with M have "(\<integral>\<^sup>+ M'. integral\<^sup>N M' (indicator A) \<partial>M) = (\<integral>\<^sup>+ M'. emeasure M' A \<partial>M)" |
796 with M have "(\<integral>\<^sup>+ M'. integral\<^sup>N M' (indicator A) \<partial>M) = (\<integral>\<^sup>+ M'. emeasure M' A \<partial>M)" |
797 by (intro nn_integral_cong nn_integral_indicator) |
797 by (intro nn_integral_cong nn_integral_indicator) |
798 (auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq) |
798 (auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq) |
799 ultimately show ?case |
799 with set show ?case |
800 using M by (simp add: emeasure_join) |
800 using M by (simp add: emeasure_join) |
801 next |
801 next |
802 case (mult f c) |
802 case (mult f c) |
803 have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. c * f x \<partial>M' \<partial>M) = (\<integral>\<^sup>+ M'. c * \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)" |
803 have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. c * f x \<partial>M' \<partial>M) = (\<integral>\<^sup>+ M'. c * \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)" |
804 using mult M M[THEN sets_eq_imp_space_eq] |
804 using mult M M[THEN sets_eq_imp_space_eq] |