--- a/src/HOL/Probability/Radon_Nikodym.thy Fri Jan 21 11:39:26 2011 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy Mon Jan 24 22:29:50 2011 +0100
@@ -1104,38 +1104,6 @@
unfolding eq[OF A, symmetric] RN_deriv(2)[OF \<nu> A, symmetric] ..
qed
-lemma (in sigma_finite_measure) RN_deriv_vimage:
- fixes f :: "'b \<Rightarrow> 'a"
- assumes f: "bij_inv S (space M) f g"
- assumes \<nu>: "measure_space M \<nu>" "absolutely_continuous \<nu>"
- shows "AE x.
- 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"
-proof (rule RN_deriv_unique[OF \<nu>])
- interpret sf: sigma_finite_measure "vimage_algebra S f" "\<lambda>A. \<mu> (f ` A)"
- using f by (rule sigma_finite_measure_isomorphic[OF bij_inv_bij_betw(1)])
- interpret \<nu>: measure_space M \<nu> using \<nu>(1) .
- have \<nu>': "measure_space (vimage_algebra S f) (\<lambda>A. \<nu> (f ` A))"
- using f by (rule \<nu>.measure_space_isomorphic[OF bij_inv_bij_betw(1)])
- { fix A assume "A \<in> sets M" then have "f ` (f -` A \<inter> S) = A"
- using sets_into_space f[THEN bij_inv_bij_betw(1), unfolded bij_betw_def]
- by (intro image_vimage_inter_eq[where T="space M"]) auto }
- note A_f = this
- then have ac: "sf.absolutely_continuous (\<lambda>A. \<nu> (f ` A))"
- using \<nu>(2) by (auto simp: sf.absolutely_continuous_def absolutely_continuous_def)
- show "(\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x)) \<in> borel_measurable M"
- using sf.RN_deriv(1)[OF \<nu>' ac]
- unfolding measurable_vimage_iff_inv[OF f] comp_def .
- fix A assume "A \<in> sets M"
- then have *: "\<And>x. x \<in> space M \<Longrightarrow> indicator (f -` A \<inter> S) (g x) = (indicator A x :: pextreal)"
- using f by (auto simp: bij_inv_def indicator_def)
- 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)"
- using `A \<in> sets M` by (force intro!: sf.RN_deriv(2)[OF \<nu>' ac])
- also have "\<dots> = (\<integral>\<^isup>+x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)"
- unfolding positive_integral_vimage_inv[OF f]
- by (simp add: * cong: positive_integral_cong)
- finally show "\<nu> A = (\<integral>\<^isup>+x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)"
- unfolding A_f[OF `A \<in> sets M`] .
-qed
lemma (in sigma_finite_measure) RN_deriv_finite:
assumes sfm: "sigma_finite_measure M \<nu>" and ac: "absolutely_continuous \<nu>"