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>"
```