# HG changeset patch
# User hoelzl
# Date 1349863939 -7200
# Node ID bbbc0f49278024234268eed9534bdf2e839c0065
# Parent  6ac97ab9b295da4099f6ce164fe676f781ae3708
sigma_finite_iff_density_finite does not require a positive density function

diff -r 6ac97ab9b295 -r bbbc0f492780 src/HOL/Probability/Radon_Nikodym.thy
--- a/src/HOL/Probability/Radon_Nikodym.thy	Wed Oct 10 12:12:18 2012 +0200
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Wed Oct 10 12:12:19 2012 +0200
@@ -933,7 +933,7 @@
   shows "density M f = density M f' \<longleftrightarrow> (AE x in M. f x = f' x)"
   using density_unique[OF assms] density_cong[OF f f'] by auto
 
-lemma (in sigma_finite_measure) sigma_finite_iff_density_finite:
+lemma (in sigma_finite_measure) sigma_finite_iff_density_finite':
   assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
   shows "sigma_finite_measure (density M f) \<longleftrightarrow> (AE x in M. f x \<noteq> \<infinity>)"
     (is "sigma_finite_measure ?N \<longleftrightarrow> _")
@@ -1019,6 +1019,13 @@
   qed
 qed
 
+lemma (in sigma_finite_measure) sigma_finite_iff_density_finite:
+  "f \<in> borel_measurable M \<Longrightarrow> sigma_finite_measure (density M f) \<longleftrightarrow> (AE x in M. f x \<noteq> \<infinity>)"
+  apply (subst density_max_0)
+  apply (subst sigma_finite_iff_density_finite')
+  apply (auto simp: max_def intro!: measurable_If)
+  done
+
 section "Radon-Nikodym derivative"
 
 definition