changeset 41661 baf1964bc468 parent 41544 c3b977fee8a3 child 41689 3e39b0e730d6
```--- 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>"```