src/HOL/Probability/Radon_Nikodym.thy
changeset 43340 60e181c4eae4
parent 42866 b0746bd57a41
child 43556 0d78c8d31d0d
     1.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Thu Jun 09 13:55:11 2011 +0200
     1.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Thu Jun 09 14:04:34 2011 +0200
     1.3 @@ -1311,6 +1311,59 @@
     1.4      by (auto simp: RN_deriv_positive_integral[OF ms \<nu>(2)])
     1.5  qed
     1.6  
     1.7 +lemma (in sigma_finite_measure) real_RN_deriv:
     1.8 +  assumes "finite_measure (M\<lparr>measure := \<nu>\<rparr>)" (is "finite_measure ?\<nu>")
     1.9 +  assumes ac: "absolutely_continuous \<nu>"
    1.10 +  obtains D where "D \<in> borel_measurable M"
    1.11 +    and "AE x. RN_deriv M \<nu> x = extreal (D x)"
    1.12 +    and "AE x in M\<lparr>measure := \<nu>\<rparr>. 0 < D x"
    1.13 +    and "\<And>x. 0 \<le> D x"
    1.14 +proof
    1.15 +  interpret \<nu>: finite_measure ?\<nu> by fact
    1.16 +  have ms: "measure_space ?\<nu>" by default
    1.17 +  note RN = RN_deriv[OF ms ac]
    1.18 +
    1.19 +  let ?RN = "\<lambda>t. {x \<in> space M. RN_deriv M \<nu> x = t}"
    1.20 +
    1.21 +  show "(\<lambda>x. real (RN_deriv M \<nu> x)) \<in> borel_measurable M"
    1.22 +    using RN by auto
    1.23 +
    1.24 +  have "\<nu> (?RN \<infinity>) = (\<integral>\<^isup>+ x. RN_deriv M \<nu> x * indicator (?RN \<infinity>) x \<partial>M)"
    1.25 +    using RN by auto
    1.26 +  also have "\<dots> = (\<integral>\<^isup>+ x. \<infinity> * indicator (?RN \<infinity>) x \<partial>M)"
    1.27 +    by (intro positive_integral_cong) (auto simp: indicator_def)
    1.28 +  also have "\<dots> = \<infinity> * \<mu> (?RN \<infinity>)"
    1.29 +    using RN by (intro positive_integral_cmult_indicator) auto
    1.30 +  finally have eq: "\<nu> (?RN \<infinity>) = \<infinity> * \<mu> (?RN \<infinity>)" .
    1.31 +  moreover
    1.32 +  have "\<mu> (?RN \<infinity>) = 0"
    1.33 +  proof (rule ccontr)
    1.34 +    assume "\<mu> {x \<in> space M. RN_deriv M \<nu> x = \<infinity>} \<noteq> 0"
    1.35 +    moreover from RN have "0 \<le> \<mu> {x \<in> space M. RN_deriv M \<nu> x = \<infinity>}" by auto
    1.36 +    ultimately have "0 < \<mu> {x \<in> space M. RN_deriv M \<nu> x = \<infinity>}" by auto
    1.37 +    with eq have "\<nu> (?RN \<infinity>) = \<infinity>" by simp
    1.38 +    with \<nu>.finite_measure[of "?RN \<infinity>"] RN show False by auto
    1.39 +  qed
    1.40 +  ultimately have "AE x. RN_deriv M \<nu> x < \<infinity>"
    1.41 +    using RN by (intro AE_iff_measurable[THEN iffD2]) auto
    1.42 +  then show "AE x. RN_deriv M \<nu> x = extreal (real (RN_deriv M \<nu> x))"
    1.43 +    using RN(3) by (auto simp: extreal_real)
    1.44 +  then have eq: "AE x in (M\<lparr>measure := \<nu>\<rparr>) . RN_deriv M \<nu> x = extreal (real (RN_deriv M \<nu> x))"
    1.45 +    using ac absolutely_continuous_AE[OF ms] by auto
    1.46 +
    1.47 +  show "\<And>x. 0 \<le> real (RN_deriv M \<nu> x)"
    1.48 +    using RN by (auto intro: real_of_extreal_pos)
    1.49 +
    1.50 +  have "\<nu> (?RN 0) = (\<integral>\<^isup>+ x. RN_deriv M \<nu> x * indicator (?RN 0) x \<partial>M)"
    1.51 +    using RN by auto
    1.52 +  also have "\<dots> = (\<integral>\<^isup>+ x. 0 \<partial>M)"
    1.53 +    by (intro positive_integral_cong) (auto simp: indicator_def)
    1.54 +  finally have "AE x in (M\<lparr>measure := \<nu>\<rparr>). RN_deriv M \<nu> x \<noteq> 0"
    1.55 +    using RN by (intro \<nu>.AE_iff_measurable[THEN iffD2]) auto
    1.56 +  with RN(3) eq show "AE x in (M\<lparr>measure := \<nu>\<rparr>). 0 < real (RN_deriv M \<nu> x)"
    1.57 +    by (auto simp: zero_less_real_of_extreal le_less)
    1.58 +qed
    1.59 +
    1.60  lemma (in sigma_finite_measure) RN_deriv_singleton:
    1.61    assumes "measure_space (M\<lparr>measure := \<nu>\<rparr>)"
    1.62    and ac: "absolutely_continuous \<nu>"