src/HOL/Probability/Probability_Mass_Function.thy
changeset 59092 d469103c0737
parent 59053 43e07797269b
child 59093 2b106e58a177
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Thu Dec 04 21:28:35 2014 +0100
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Fri Dec 05 12:06:18 2014 +0100
     1.3 @@ -385,7 +385,7 @@
     1.4      by (simp split: split_indicator)
     1.5    show "AE x in density (count_space UNIV) (ereal \<circ> f).
     1.6      measure (density (count_space UNIV) (ereal \<circ> f)) {x} \<noteq> 0"
     1.7 -    by (simp add: AE_density nonneg emeasure_density measure_def nn_integral_cmult_indicator)
     1.8 +    by (simp add: AE_density nonneg measure_def emeasure_density max_def)
     1.9    show "prob_space (density (count_space UNIV) (ereal \<circ> f))"
    1.10      by default (simp add: emeasure_density prob)
    1.11  qed simp
    1.12 @@ -395,7 +395,7 @@
    1.13    have *[simp]: "\<And>x y. ereal (f y) * indicator {x} y = ereal (f x) * indicator {x} y"
    1.14      by (simp split: split_indicator)
    1.15    fix x show "measure (density (count_space UNIV) (ereal \<circ> f)) {x} = f x"
    1.16 -    by transfer (simp add: measure_def emeasure_density nn_integral_cmult_indicator nonneg)
    1.17 +    by transfer (simp add: measure_def emeasure_density nonneg max_def)
    1.18  qed
    1.19  
    1.20  end