# HG changeset patch
# User Andreas Lochbihler
# Date 1423566626 -3600
# Node ID f71732294f299af6935bb469390b5a8a9a726fcb
# Parent fd5d23cc0e977381f5571ab26a259b25aab81cf9
tune proof
diff -r fd5d23cc0e97 -r f71732294f29 src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy Tue Feb 10 12:05:21 2015 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Tue Feb 10 12:10:26 2015 +0100
@@ -279,6 +279,9 @@
using measure_pmf.emeasure_space_1 by simp
qed
+lemma emeasure_pmf_UNIV [simp]: "emeasure (measure_pmf M) UNIV = 1"
+using measure_pmf.emeasure_space_1[of M] by simp
+
lemma in_null_sets_measure_pmfI:
"A \ set_pmf p = {} \ A \ null_sets (measure_pmf p)"
using emeasure_eq_0_AE[where ?P="\x. x \ A" and M="measure_pmf p"]
@@ -1064,19 +1067,14 @@
unfolding pqr_def
proof (subst pmf_embed_pmf)
have "(\\<^sup>+ x. ereal ((\(y, x, z). assign y x z) x) \count_space UNIV) =
- (\\<^sup>+ x. ereal ((\(y, x, z). assign y x z) x) \(count_space ((\((x, y), z). (y, x, z)) ` (pq \ r))))"
- by (force simp add: pmf_eq_0_set_pmf r set_map_pmf split: split_indicator
- intro!: nn_integral_count_space_eq assign_eq_0_outside)
- also have "\ = (\\<^sup>+ x. ereal ((\((x, y), z). assign y x z) x) \(count_space (pq \ r)))"
- by (subst nn_integral_bij_count_space[OF inj_on_imp_bij_betw, symmetric])
- (auto simp: inj_on_def intro!: nn_integral_cong)
- also have "\ = (\\<^sup>+ xy. \\<^sup>+z. ereal ((\((x, y), z). assign y x z) (xy, z)) \count_space r \count_space pq)"
- by (subst sigma_finite_measure.nn_integral_fst)
- (auto simp: pair_measure_countable sigma_finite_measure_count_space_countable)
- also have "\ = (\\<^sup>+ xy. \\<^sup>+z. ereal ((\((x, y), z). assign y x z) (xy, z)) \count_space UNIV \count_space pq)"
- by (intro nn_integral_cong nn_integral_count_space_eq)
- (force simp: r set_map_pmf pmf_eq_0_set_pmf intro!: assign_eq_0_outside)+
- also have "\ = (\\<^sup>+ z. ?pq (snd z) (fst z) \count_space pq)"
+ (\\<^sup>+ x. ereal ((\(y, x, z). assign y x z) x) \count_space ((\((x, y), z). (y, x, z)) ` UNIV))"
+ by(rule nn_integral_count_space_eq)(auto simp add: image_def)
+ also have "\ = \\<^sup>+ x. ereal ((\((x, y), z). assign y x z) x) \count_space UNIV"
+ by(subst nn_integral_bij_count_space[OF inj_on_imp_bij_betw, symmetric])
+ (auto simp add: inj_on_def split_beta)
+ also have "\ = (\\<^sup>+ xy. \\<^sup>+ z. ereal ((\((x, y), z). assign y x z) (xy, z)) \count_space UNIV \count_space UNIV)"
+ by(subst nn_integral_fst_count_space) simp
+ also have "\ = (\\<^sup>+ z. ?pq (snd z) (fst z) \count_space UNIV)"
by (subst nn_integral_assign2[symmetric]) (auto intro!: nn_integral_cong)
finally show "(\\<^sup>+ x. ereal ((\(y, x, z). assign y x z) x) \count_space UNIV) = 1"
by (simp add: nn_integral_pmf emeasure_pmf)