author Andreas Lochbihler Tue Feb 10 12:10:26 2015 +0100 (2015-02-10) changeset 59490 f71732294f29 parent 59489 fd5d23cc0e97 child 59491 40f570f9a284
tune proof
1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Feb 10 12:05:21 2015 +0100
1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Feb 10 12:10:26 2015 +0100
1.3 @@ -279,6 +279,9 @@
1.4      using measure_pmf.emeasure_space_1 by simp
1.5  qed
1.7 +lemma emeasure_pmf_UNIV [simp]: "emeasure (measure_pmf M) UNIV = 1"
1.8 +using measure_pmf.emeasure_space_1[of M] by simp
1.9 +
1.10  lemma in_null_sets_measure_pmfI:
1.11    "A \<inter> set_pmf p = {} \<Longrightarrow> A \<in> null_sets (measure_pmf p)"
1.12  using emeasure_eq_0_AE[where ?P="\<lambda>x. x \<in> A" and M="measure_pmf p"]
1.13 @@ -1064,19 +1067,14 @@
1.14          unfolding pqr_def
1.15        proof (subst pmf_embed_pmf)
1.16          have "(\<integral>\<^sup>+ x. ereal ((\<lambda>(y, x, z). assign y x z) x) \<partial>count_space UNIV) =
1.17 -          (\<integral>\<^sup>+ x. ereal ((\<lambda>(y, x, z). assign y x z) x) \<partial>(count_space ((\<lambda>((x, y), z). (y, x, z)) ` (pq \<times> r))))"
1.18 -          by (force simp add: pmf_eq_0_set_pmf r set_map_pmf split: split_indicator
1.19 -                    intro!: nn_integral_count_space_eq assign_eq_0_outside)
1.20 -        also have "\<dots> = (\<integral>\<^sup>+ x. ereal ((\<lambda>((x, y), z). assign y x z) x) \<partial>(count_space (pq \<times> r)))"
1.21 -          by (subst nn_integral_bij_count_space[OF inj_on_imp_bij_betw, symmetric])
1.22 -             (auto simp: inj_on_def intro!: nn_integral_cong)
1.23 -        also have "\<dots> = (\<integral>\<^sup>+ xy. \<integral>\<^sup>+z. ereal ((\<lambda>((x, y), z). assign y x z) (xy, z)) \<partial>count_space r \<partial>count_space pq)"
1.24 -          by (subst sigma_finite_measure.nn_integral_fst)
1.25 -             (auto simp: pair_measure_countable sigma_finite_measure_count_space_countable)
1.26 -        also have "\<dots> = (\<integral>\<^sup>+ xy. \<integral>\<^sup>+z. ereal ((\<lambda>((x, y), z). assign y x z) (xy, z)) \<partial>count_space UNIV \<partial>count_space pq)"
1.27 -          by (intro nn_integral_cong nn_integral_count_space_eq)
1.28 -             (force simp: r set_map_pmf pmf_eq_0_set_pmf intro!: assign_eq_0_outside)+
1.29 -        also have "\<dots> = (\<integral>\<^sup>+ z. ?pq (snd z) (fst z) \<partial>count_space pq)"
1.30 +              (\<integral>\<^sup>+ x. ereal ((\<lambda>(y, x, z). assign y x z) x) \<partial>count_space ((\<lambda>((x, y), z). (y, x, z)) ` UNIV))"
1.31 +          by(rule nn_integral_count_space_eq)(auto simp add: image_def)
1.32 +        also have "\<dots> = \<integral>\<^sup>+ x. ereal ((\<lambda>((x, y), z). assign y x z) x) \<partial>count_space UNIV"
1.33 +          by(subst nn_integral_bij_count_space[OF inj_on_imp_bij_betw, symmetric])
1.34 +            (auto simp add: inj_on_def split_beta)
1.35 +        also have "\<dots> = (\<integral>\<^sup>+ xy. \<integral>\<^sup>+ z. ereal ((\<lambda>((x, y), z). assign y x z) (xy, z)) \<partial>count_space UNIV \<partial>count_space UNIV)"
1.36 +          by(subst nn_integral_fst_count_space) simp
1.37 +        also have "\<dots> = (\<integral>\<^sup>+ z. ?pq (snd z) (fst z) \<partial>count_space UNIV)"
1.38            by (subst nn_integral_assign2[symmetric]) (auto intro!: nn_integral_cong)
1.39          finally show "(\<integral>\<^sup>+ x. ereal ((\<lambda>(y, x, z). assign y x z) x) \<partial>count_space UNIV) = 1"
1.40            by (simp add: nn_integral_pmf emeasure_pmf)