src/HOL/Probability/Radon_Nikodym.thy
changeset 41661 baf1964bc468
parent 41544 c3b977fee8a3
child 41689 3e39b0e730d6
     1.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Fri Jan 21 11:39:26 2011 +0100
     1.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Mon Jan 24 22:29:50 2011 +0100
     1.3 @@ -1104,38 +1104,6 @@
     1.4      unfolding eq[OF A, symmetric] RN_deriv(2)[OF \<nu> A, symmetric] ..
     1.5  qed
     1.6  
     1.7 -lemma (in sigma_finite_measure) RN_deriv_vimage:
     1.8 -  fixes f :: "'b \<Rightarrow> 'a"
     1.9 -  assumes f: "bij_inv S (space M) f g"
    1.10 -  assumes \<nu>: "measure_space M \<nu>" "absolutely_continuous \<nu>"
    1.11 -  shows "AE x.
    1.12 -    sigma_finite_measure.RN_deriv (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) (\<lambda>A. \<nu> (f ` A)) (g x) = RN_deriv \<nu> x"
    1.13 -proof (rule RN_deriv_unique[OF \<nu>])
    1.14 -  interpret sf: sigma_finite_measure "vimage_algebra S f" "\<lambda>A. \<mu> (f ` A)"
    1.15 -    using f by (rule sigma_finite_measure_isomorphic[OF bij_inv_bij_betw(1)])
    1.16 -  interpret \<nu>: measure_space M \<nu> using \<nu>(1) .
    1.17 -  have \<nu>': "measure_space (vimage_algebra S f) (\<lambda>A. \<nu> (f ` A))"
    1.18 -    using f by (rule \<nu>.measure_space_isomorphic[OF bij_inv_bij_betw(1)])
    1.19 -  { fix A assume "A \<in> sets M" then have "f ` (f -` A \<inter> S) = A"
    1.20 -      using sets_into_space f[THEN bij_inv_bij_betw(1), unfolded bij_betw_def]
    1.21 -      by (intro image_vimage_inter_eq[where T="space M"]) auto }
    1.22 -  note A_f = this
    1.23 -  then have ac: "sf.absolutely_continuous (\<lambda>A. \<nu> (f ` A))"
    1.24 -    using \<nu>(2) by (auto simp: sf.absolutely_continuous_def absolutely_continuous_def)
    1.25 -  show "(\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x)) \<in> borel_measurable M"
    1.26 -    using sf.RN_deriv(1)[OF \<nu>' ac]
    1.27 -    unfolding measurable_vimage_iff_inv[OF f] comp_def .
    1.28 -  fix A assume "A \<in> sets M"
    1.29 -  then have *: "\<And>x. x \<in> space M \<Longrightarrow> indicator (f -` A \<inter> S) (g x) = (indicator A x :: pextreal)"
    1.30 -    using f by (auto simp: bij_inv_def indicator_def)
    1.31 -  have "\<nu> (f ` (f -` A \<inter> S)) = sf.positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) x * indicator (f -` A \<inter> S) x)"
    1.32 -    using `A \<in> sets M` by (force intro!: sf.RN_deriv(2)[OF \<nu>' ac])
    1.33 -  also have "\<dots> = (\<integral>\<^isup>+x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)"
    1.34 -    unfolding positive_integral_vimage_inv[OF f]
    1.35 -    by (simp add: * cong: positive_integral_cong)
    1.36 -  finally show "\<nu> A = (\<integral>\<^isup>+x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)"
    1.37 -    unfolding A_f[OF `A \<in> sets M`] .
    1.38 -qed
    1.39  
    1.40  lemma (in sigma_finite_measure) RN_deriv_finite:
    1.41    assumes sfm: "sigma_finite_measure M \<nu>" and ac: "absolutely_continuous \<nu>"