src/HOL/Probability/Probability_Mass_Function.thy
changeset 59024 5fcfeae84b96
parent 59023 4999a616336c
child 59048 7dc8ac6f0895
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Fri Nov 21 12:11:44 2014 +0100
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Fri Nov 21 12:24:59 2014 +0100
     1.3 @@ -603,6 +603,12 @@
     1.4      by (intro subprob_space.measure_bind[where N="count_space UNIV", OF N]) auto
     1.5  qed (auto simp: Transfer.Rel_def rel_fun_def cr_pmf_def)
     1.6  
     1.7 +lemma set_pmf_join_pmf: "set_pmf (join_pmf f) = (\<Union>p\<in>set_pmf f. set_pmf p)"
     1.8 +apply(simp add: set_eq_iff set_pmf_iff pmf_join)
     1.9 +apply(subst integral_nonneg_eq_0_iff_AE)
    1.10 +apply(auto simp add: pmf_le_1 pmf_nonneg AE_measure_pmf_iff intro!: measure_pmf.integrable_const_bound[where B=1])
    1.11 +done
    1.12 +
    1.13  lift_definition return_pmf :: "'a \<Rightarrow> 'a pmf" is "return (count_space UNIV)"
    1.14    by (auto intro!: prob_space_return simp: AE_return measure_return)
    1.15