src/HOL/Probability/Radon_Nikodym.thy
changeset 49778 bbbc0f492780
parent 47694 05663f75964c
child 49785 0a8adca22974
     1.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Wed Oct 10 12:12:18 2012 +0200
     1.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Wed Oct 10 12:12:19 2012 +0200
     1.3 @@ -933,7 +933,7 @@
     1.4    shows "density M f = density M f' \<longleftrightarrow> (AE x in M. f x = f' x)"
     1.5    using density_unique[OF assms] density_cong[OF f f'] by auto
     1.6  
     1.7 -lemma (in sigma_finite_measure) sigma_finite_iff_density_finite:
     1.8 +lemma (in sigma_finite_measure) sigma_finite_iff_density_finite':
     1.9    assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
    1.10    shows "sigma_finite_measure (density M f) \<longleftrightarrow> (AE x in M. f x \<noteq> \<infinity>)"
    1.11      (is "sigma_finite_measure ?N \<longleftrightarrow> _")
    1.12 @@ -1019,6 +1019,13 @@
    1.13    qed
    1.14  qed
    1.15  
    1.16 +lemma (in sigma_finite_measure) sigma_finite_iff_density_finite:
    1.17 +  "f \<in> borel_measurable M \<Longrightarrow> sigma_finite_measure (density M f) \<longleftrightarrow> (AE x in M. f x \<noteq> \<infinity>)"
    1.18 +  apply (subst density_max_0)
    1.19 +  apply (subst sigma_finite_iff_density_finite')
    1.20 +  apply (auto simp: max_def intro!: measurable_If)
    1.21 +  done
    1.22 +
    1.23  section "Radon-Nikodym derivative"
    1.24  
    1.25  definition