# HG changeset patch
# User hoelzl
# Date 1298457721 -3600
# Node ID 2f8f2685e0c08cc051bb0407f1030f9d1cfa43ae
# Parent  d5b294734373b8884ba8f68d7060c982faabd53f# Parent  563bea92b2c05af525a5e5933a1e931a746daf16
merged

diff -r d5b294734373 -r 2f8f2685e0c0 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Feb 23 11:23:26 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Feb 23 11:42:01 2011 +0100
@@ -530,8 +530,8 @@
   shows "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f'') (at x) \<Longrightarrow> f' = f''"
   unfolding FDERIV_conv_has_derivative [symmetric]
   by (rule FDERIV_unique)
- 
-lemma "isCont f x = continuous (at x) f" unfolding isCont_def LIM_def
+
+lemma continuous_isCont: "isCont f x = continuous (at x) f" unfolding isCont_def LIM_def
   unfolding continuous_at Lim_at unfolding dist_nz by auto
 
 lemma frechet_derivative_unique_within_closed_interval: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"
diff -r d5b294734373 -r 2f8f2685e0c0 src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Wed Feb 23 11:23:26 2011 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Wed Feb 23 11:42:01 2011 +0100
@@ -48,6 +48,9 @@
   thus ?thesis by simp
 qed
 
+lemma borel_comp[intro,simp]: "A \<in> sets borel \<Longrightarrow> - A \<in> sets borel"
+  unfolding Compl_eq_Diff_UNIV by (intro borel.Diff) auto
+
 lemma (in sigma_algebra) borel_measurable_vimage:
   fixes f :: "'a \<Rightarrow> 'x::t2_space"
   assumes borel: "f \<in> borel_measurable M"
@@ -1118,6 +1121,73 @@
     using * ** by auto
 qed
 
+lemma borel_measurable_continuous_on1:
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::t1_space"
+  assumes "continuous_on UNIV f"
+  shows "f \<in> borel_measurable borel"
+  apply(rule borel.borel_measurableI)
+  using continuous_open_preimage[OF assms] unfolding vimage_def by auto
+
+lemma borel_measurable_continuous_on:
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::t1_space"
+  assumes cont: "continuous_on A f" "open A" and f: "f -` {c} \<inter> A \<in> sets borel"
+  shows "(\<lambda>x. if x \<in> A then f x else c) \<in> borel_measurable borel" (is "?f \<in> _")
+proof (rule borel.borel_measurableI)
+  fix S :: "'b set" assume "open S"
+  then have "open {x\<in>A. f x \<in> S - {c}}"
+    by (intro continuous_open_preimage[OF cont]) auto
+  then have *: "{x\<in>A. f x \<in> S - {c}} \<in> sets borel" by auto
+  show "?f -` S \<inter> space borel \<in> sets borel"
+  proof cases
+    assume "c \<in> S"
+    then have "?f -` S = {x\<in>A. f x \<in> S - {c}} \<union> (f -` {c} \<inter> A) \<union> -A"
+      by auto
+    with * show "?f -` S \<inter> space borel \<in> sets borel"
+      using `open A` f by (auto intro!: borel.Un)
+  next
+    assume "c \<notin> S"
+    then have "?f -` S = {x\<in>A. f x \<in> S - {c}}" by (auto split: split_if_asm)
+    with * show "?f -` S \<inter> space borel \<in> sets borel" by auto
+  qed
+qed
+
+lemma borel_measurable_borel_log: assumes "1 < b" shows "log b \<in> borel_measurable borel"
+proof -
+  { fix x :: real assume x: "x \<le> 0"
+    { fix x::real assume "x \<le> 0" then have "\<And>u. exp u = x \<longleftrightarrow> False" by auto }
+    from this[of x] x this[of 0] have "log b 0 = log b x"
+      by (auto simp: ln_def log_def) }
+  note log_imp = this
+  have "(\<lambda>x. if x \<in> {0<..} then log b x else log b 0) \<in> borel_measurable borel"
+  proof (rule borel_measurable_continuous_on)
+    show "continuous_on {0<..} (log b)"
+      by (auto intro!: continuous_at_imp_continuous_on DERIV_log DERIV_isCont
+               simp: continuous_isCont[symmetric])
+    show "open ({0<..}::real set)" by auto
+    show "log b -` {log b 0} \<inter> {0<..} \<in> sets borel"
+    proof cases
+      assume "log b -` {log b 0} \<inter> {0<..} = {}"
+      then show ?thesis by simp
+    next
+      assume "log b -` {log b 0} \<inter> {0<..} \<noteq> {}"
+      then obtain x where "0 < x" "log b x = log b 0" by auto
+      with log_inj[OF `1 < b`] have "log b -` {log b 0} \<inter> {0<..} = {x}"
+        by (auto simp: inj_on_def)
+      then show ?thesis by simp
+    qed
+  qed
+  also have "(\<lambda>x. if x \<in> {0<..} then log b x else log b 0) = log b"
+    by (simp add: fun_eq_iff not_less log_imp)
+  finally show ?thesis .
+qed
+
+lemma (in sigma_algebra) borel_measurable_log[simp,intro]:
+  assumes f: "f \<in> borel_measurable M" and "1 < b"
+  shows "(\<lambda>x. log b (f x)) \<in> borel_measurable M"
+  using measurable_comp[OF f borel_measurable_borel_log[OF `1 < b`]]
+  by (simp add: comp_def)
+
+
 lemma (in sigma_algebra) less_eq_ge_measurable:
   fixes f :: "'a \<Rightarrow> 'c::linorder"
   shows "{x\<in>space M. a < f x} \<in> sets M \<longleftrightarrow> {x\<in>space M. f x \<le> a} \<in> sets M"
diff -r d5b294734373 -r 2f8f2685e0c0 src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Wed Feb 23 11:23:26 2011 +0100
+++ b/src/HOL/Probability/Information.thy	Wed Feb 23 11:42:01 2011 +0100
@@ -167,6 +167,53 @@
 definition
   "KL_divergence b M \<nu> = \<integral>x. log b (real (RN_deriv M \<nu> x)) \<partial>M\<lparr>measure := \<nu>\<rparr>"
 
+lemma (in sigma_finite_measure) KL_divergence_vimage:
+  assumes T: "T \<in> measure_preserving M M'"
+    and T': "T' \<in> measure_preserving (M'\<lparr> measure := \<nu>' \<rparr>) (M\<lparr> measure := \<nu> \<rparr>)"
+    and inv: "\<And>x. x \<in> space M \<Longrightarrow> T' (T x) = x"
+    and inv': "\<And>x. x \<in> space M' \<Longrightarrow> T (T' x) = x"
+  and \<nu>': "measure_space (M'\<lparr>measure := \<nu>'\<rparr>)" "measure_space.absolutely_continuous M' \<nu>'"
+  and "1 < b"
+  shows "KL_divergence b M' \<nu>' = KL_divergence b M \<nu>"
+proof -
+  interpret \<nu>': measure_space "M'\<lparr>measure := \<nu>'\<rparr>" by fact
+  have M: "measure_space (M\<lparr> measure := \<nu>\<rparr>)"
+    by (rule \<nu>'.measure_space_vimage[OF _ T'], simp) default
+  have "sigma_algebra (M'\<lparr> measure := \<nu>'\<rparr>)" by default
+  then have saM': "sigma_algebra M'" by simp
+  then interpret M': measure_space M' by (rule measure_space_vimage) fact
+  have ac: "absolutely_continuous \<nu>" unfolding absolutely_continuous_def
+  proof safe
+    fix N assume N: "N \<in> sets M" and N_0: "\<mu> N = 0"
+    then have N': "T' -` N \<inter> space M' \<in> sets M'"
+      using T' by (auto simp: measurable_def measure_preserving_def)
+    have "T -` (T' -` N \<inter> space M') \<inter> space M = N"
+      using inv T N sets_into_space[OF N] by (auto simp: measurable_def measure_preserving_def)
+    then have "measure M' (T' -` N \<inter> space M') = 0"
+      using measure_preservingD[OF T N'] N_0 by auto
+    with \<nu>'(2) N' show "\<nu> N = 0" using measure_preservingD[OF T', of N] N
+      unfolding M'.absolutely_continuous_def measurable_def by auto
+  qed
+
+  have sa: "sigma_algebra (M\<lparr>measure := \<nu>\<rparr>)" by simp default
+  have AE: "AE x. RN_deriv M' \<nu>' (T x) = RN_deriv M \<nu> x"
+    by (rule RN_deriv_vimage[OF T T' inv \<nu>'])
+  show ?thesis
+    unfolding KL_divergence_def
+  proof (subst \<nu>'.integral_vimage[OF sa T'])
+    show "(\<lambda>x. log b (real (RN_deriv M \<nu> x))) \<in> borel_measurable (M\<lparr>measure := \<nu>\<rparr>)"
+      by (auto intro!: RN_deriv[OF M ac] borel_measurable_log[OF _ `1 < b`])
+    have "(\<integral> x. log b (real (RN_deriv M' \<nu>' x)) \<partial>M'\<lparr>measure := \<nu>'\<rparr>) =
+      (\<integral> x. log b (real (RN_deriv M' \<nu>' (T (T' x)))) \<partial>M'\<lparr>measure := \<nu>'\<rparr>)" (is "?l = _")
+      using inv' by (auto intro!: \<nu>'.integral_cong)
+    also have "\<dots> = (\<integral> x. log b (real (RN_deriv M \<nu> (T' x))) \<partial>M'\<lparr>measure := \<nu>'\<rparr>)" (is "_ = ?r")
+      using M ac AE
+      by (intro \<nu>'.integral_cong_AE \<nu>'.almost_everywhere_vimage[OF sa T'] absolutely_continuous_AE[OF M])
+         (auto elim!: AE_mp)
+    finally show "?l = ?r" .
+  qed
+qed
+
 lemma (in sigma_finite_measure) KL_divergence_cong:
   assumes "measure_space (M\<lparr>measure := \<nu>\<rparr>)" (is "measure_space ?\<nu>")
   assumes [simp]: "sets N = sets M" "space N = space M"
@@ -236,18 +283,6 @@
     \<lparr> space = X`space M, sets = Pow (X`space M), measure = distribution X \<rparr>
     \<lparr> space = Y`space M, sets = Pow (Y`space M), measure = distribution Y \<rparr> X Y"
 
-lemma algebra_measure_update[simp]:
-  "algebra (M'\<lparr>measure := m\<rparr>) \<longleftrightarrow> algebra M'"
-  unfolding algebra_def by simp
-
-lemma sigma_algebra_measure_update[simp]:
-  "sigma_algebra (M'\<lparr>measure := m\<rparr>) \<longleftrightarrow> sigma_algebra M'"
-  unfolding sigma_algebra_def sigma_algebra_axioms_def by simp
-
-lemma finite_sigma_algebra_measure_update[simp]:
-  "finite_sigma_algebra (M'\<lparr>measure := m\<rparr>) \<longleftrightarrow> finite_sigma_algebra M'"
-  unfolding finite_sigma_algebra_def finite_sigma_algebra_axioms_def by simp
-
 lemma (in prob_space) finite_variables_absolutely_continuous:
   assumes X: "finite_random_variable S X" and Y: "finite_random_variable T Y"
   shows "measure_space.absolutely_continuous
@@ -313,6 +348,32 @@
     unfolding mutual_information_def .
 qed
 
+lemma (in information_space) mutual_information_commute_generic:
+  assumes X: "random_variable S X" and Y: "random_variable T Y"
+  assumes ac: "measure_space.absolutely_continuous
+    (S\<lparr>measure := distribution X\<rparr> \<Otimes>\<^isub>M T\<lparr>measure := distribution Y\<rparr>) (joint_distribution X Y)"
+  shows "mutual_information b S T X Y = mutual_information b T S Y X"
+proof -
+  let ?S = "S\<lparr>measure := distribution X\<rparr>" and ?T = "T\<lparr>measure := distribution Y\<rparr>"
+  interpret S: prob_space ?S using X by (rule distribution_prob_space)
+  interpret T: prob_space ?T using Y by (rule distribution_prob_space)
+  interpret P: pair_prob_space ?S ?T ..
+  interpret Q: pair_prob_space ?T ?S ..
+  show ?thesis
+    unfolding mutual_information_def
+  proof (intro Q.KL_divergence_vimage[OF Q.measure_preserving_swap _ _ _ _ ac b_gt_1])
+    show "(\<lambda>(x,y). (y,x)) \<in> measure_preserving
+      (P.P \<lparr> measure := joint_distribution X Y\<rparr>) (Q.P \<lparr> measure := joint_distribution Y X\<rparr>)"
+      using X Y unfolding measurable_def
+      unfolding measure_preserving_def using P.pair_sigma_algebra_swap_measurable
+      by (auto simp add: space_pair_measure distribution_def intro!: arg_cong[where f=\<mu>])
+    have "prob_space (P.P\<lparr> measure := joint_distribution X Y\<rparr>)"
+      using X Y by (auto intro!: distribution_prob_space random_variable_pairI)
+    then show "measure_space (P.P\<lparr> measure := joint_distribution X Y\<rparr>)"
+      unfolding prob_space_def by simp
+  qed auto
+qed
+
 lemma (in information_space) mutual_information_commute:
   assumes X: "finite_random_variable S X" and Y: "finite_random_variable T Y"
   shows "mutual_information b S T X Y = mutual_information b T S Y X"
@@ -323,7 +384,7 @@
 lemma (in information_space) mutual_information_commute_simple:
   assumes X: "simple_function M X" and Y: "simple_function M Y"
   shows "\<I>(X;Y) = \<I>(Y;X)"
-  by (intro X Y simple_function_imp_finite_random_variable mutual_information_commute)
+  by (intro mutual_information_commute X Y simple_function_imp_finite_random_variable)
 
 lemma (in information_space) mutual_information_eq:
   assumes "simple_function M X" "simple_function M Y"
diff -r d5b294734373 -r 2f8f2685e0c0 src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Wed Feb 23 11:23:26 2011 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Wed Feb 23 11:42:01 2011 +0100
@@ -821,30 +821,33 @@
   shows "integral\<^isup>S N = integral\<^isup>S M"
   unfolding simple_integral_def_raw by simp
 
+lemma measure_preservingD:
+  "T \<in> measure_preserving A B \<Longrightarrow> X \<in> sets B \<Longrightarrow> measure A (T -` X \<inter> space A) = measure B X"
+  unfolding measure_preserving_def by auto
+
 lemma (in measure_space) simple_integral_vimage:
-  assumes T: "sigma_algebra M'" "T \<in> measurable M M'"
+  assumes T: "sigma_algebra M'" "T \<in> measure_preserving M M'"
     and f: "simple_function M' f"
-    and \<nu>: "\<And>A. A \<in> sets M' \<Longrightarrow> measure M' A = \<mu> (T -` A \<inter> space M)"
   shows "integral\<^isup>S M' f = (\<integral>\<^isup>S x. f (T x) \<partial>M)"
 proof -
-  interpret T: measure_space M' using \<nu> by (rule measure_space_vimage[OF T])
+  interpret T: measure_space M' by (rule measure_space_vimage[OF T])
   show "integral\<^isup>S M' f = (\<integral>\<^isup>S x. f (T x) \<partial>M)"
     unfolding simple_integral_def
   proof (intro setsum_mono_zero_cong_right ballI)
     show "(\<lambda>x. f (T x)) ` space M \<subseteq> f ` space M'"
-      using T unfolding measurable_def by auto
+      using T unfolding measurable_def measure_preserving_def by auto
     show "finite (f ` space M')"
       using f unfolding simple_function_def by auto
   next
     fix i assume "i \<in> f ` space M' - (\<lambda>x. f (T x)) ` space M"
     then have "T -` (f -` {i} \<inter> space M') \<inter> space M = {}" by (auto simp: image_iff)
-    with f[THEN T.simple_functionD(2), THEN \<nu>]
+    with f[THEN T.simple_functionD(2), THEN measure_preservingD[OF T(2)], of "{i}"]
     show "i * T.\<mu> (f -` {i} \<inter> space M') = 0" by simp
   next
     fix i assume "i \<in> (\<lambda>x. f (T x)) ` space M"
     then have "T -` (f -` {i} \<inter> space M') \<inter> space M = (\<lambda>x. f (T x)) -` {i} \<inter> space M"
-      using T unfolding measurable_def by auto
-    with f[THEN T.simple_functionD(2), THEN \<nu>]
+      using T unfolding measurable_def measure_preserving_def by auto
+    with f[THEN T.simple_functionD(2), THEN measure_preservingD[OF T(2)], of "{i}"]
     show "i * T.\<mu> (f -` {i} \<inter> space M') = i * \<mu> ((\<lambda>x. f (T x)) -` {i} \<inter> space M)"
       by auto
   qed
@@ -1195,20 +1198,23 @@
   using positive_integral_isoton[OF `f \<up> u` e(1)[THEN borel_measurable_simple_function]]
   unfolding positive_integral_eq_simple_integral[OF e] .
 
+lemma measure_preservingD2:
+  "f \<in> measure_preserving A B \<Longrightarrow> f \<in> measurable A B"
+  unfolding measure_preserving_def by auto
+
 lemma (in measure_space) positive_integral_vimage:
-  assumes T: "sigma_algebra M'" "T \<in> measurable M M'" and f: "f \<in> borel_measurable M'"
-    and \<nu>: "\<And>A. A \<in> sets M' \<Longrightarrow> measure M' A = \<mu> (T -` A \<inter> space M)"
+  assumes T: "sigma_algebra M'" "T \<in> measure_preserving M M'" and f: "f \<in> borel_measurable M'"
   shows "integral\<^isup>P M' f = (\<integral>\<^isup>+ x. f (T x) \<partial>M)"
 proof -
-  interpret T: measure_space M' using \<nu> by (rule measure_space_vimage[OF T])
+  interpret T: measure_space M' by (rule measure_space_vimage[OF T])
   obtain f' where f': "f' \<up> f" "\<And>i. simple_function M' (f' i)"
     using T.borel_measurable_implies_simple_function_sequence[OF f] by blast
   then have f: "(\<lambda>i x. f' i (T x)) \<up> (\<lambda>x. f (T x))" "\<And>i. simple_function M (\<lambda>x. f' i (T x))"
-    using simple_function_vimage[OF T] unfolding isoton_fun_expand by auto
+    using simple_function_vimage[OF T(1) measure_preservingD2[OF T(2)]] unfolding isoton_fun_expand by auto
   show "integral\<^isup>P M' f = (\<integral>\<^isup>+ x. f (T x) \<partial>M)"
     using positive_integral_isoton_simple[OF f]
     using T.positive_integral_isoton_simple[OF f']
-    by (simp add: simple_integral_vimage[OF T f'(2) \<nu>] isoton_def)
+    by (simp add: simple_integral_vimage[OF T f'(2)] isoton_def)
 qed
 
 lemma (in measure_space) positive_integral_linear:
@@ -1604,20 +1610,33 @@
 qed
 
 lemma (in measure_space) integral_vimage:
-  assumes T: "sigma_algebra M'" "T \<in> measurable M M'"
-    and \<nu>: "\<And>A. A \<in> sets M' \<Longrightarrow> measure M' A = \<mu> (T -` A \<inter> space M)"
-  assumes f: "integrable M' f"
-  shows "integrable M (\<lambda>x. f (T x))" (is ?P)
-    and "integral\<^isup>L M' f = (\<integral>x. f (T x) \<partial>M)" (is ?I)
+  assumes T: "sigma_algebra M'" "T \<in> measure_preserving M M'"
+  assumes f: "f \<in> borel_measurable M'"
+  shows "integral\<^isup>L M' f = (\<integral>x. f (T x) \<partial>M)"
 proof -
-  interpret T: measure_space M' using \<nu> by (rule measure_space_vimage[OF T])
-  from measurable_comp[OF T(2), of f borel]
+  interpret T: measure_space M' by (rule measure_space_vimage[OF T])
+  from measurable_comp[OF measure_preservingD2[OF T(2)], of f borel]
   have borel: "(\<lambda>x. Real (f x)) \<in> borel_measurable M'" "(\<lambda>x. Real (- f x)) \<in> borel_measurable M'"
     and "(\<lambda>x. f (T x)) \<in> borel_measurable M"
-    using f unfolding integrable_def by (auto simp: comp_def)
-  then show ?P ?I
+    using f by (auto simp: comp_def)
+  then show ?thesis
     using f unfolding lebesgue_integral_def integrable_def
-    by (auto simp: borel[THEN positive_integral_vimage[OF T], OF \<nu>])
+    by (auto simp: borel[THEN positive_integral_vimage[OF T]])
+qed
+
+lemma (in measure_space) integrable_vimage:
+  assumes T: "sigma_algebra M'" "T \<in> measure_preserving M M'"
+  assumes f: "integrable M' f"
+  shows "integrable M (\<lambda>x. f (T x))"
+proof -
+  interpret T: measure_space M' by (rule measure_space_vimage[OF T])
+  from measurable_comp[OF measure_preservingD2[OF T(2)], of f borel]
+  have borel: "(\<lambda>x. Real (f x)) \<in> borel_measurable M'" "(\<lambda>x. Real (- f x)) \<in> borel_measurable M'"
+    and "(\<lambda>x. f (T x)) \<in> borel_measurable M"
+    using f by (auto simp: comp_def)
+  then show ?thesis
+    using f unfolding lebesgue_integral_def integrable_def
+    by (auto simp: borel[THEN positive_integral_vimage[OF T]])
 qed
 
 lemma (in measure_space) integral_minus[intro, simp]:
diff -r d5b294734373 -r 2f8f2685e0c0 src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Wed Feb 23 11:23:26 2011 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Wed Feb 23 11:42:01 2011 +0100
@@ -733,13 +733,6 @@
     unfolding lebesgue_integral_eq_borel[OF borel] by simp
 qed
 
-lemma continuous_on_imp_borel_measurable:
-  fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::ordered_euclidean_space"
-  assumes "continuous_on UNIV f"
-  shows "f \<in> borel_measurable borel"
-  apply(rule borel.borel_measurableI)
-  using continuous_open_preimage[OF assms] unfolding vimage_def by auto
-
 subsection {* Equivalence between product spaces and euclidean spaces *}
 
 definition e2p :: "'a::ordered_euclidean_space \<Rightarrow> (nat \<Rightarrow> real)" where
@@ -759,13 +752,13 @@
 interpretation lborel_product: product_sigma_finite "\<lambda>x. lborel::real measure_space"
   by default
 
-interpretation lborel_space: finite_product_sigma_finite "\<lambda>x. lborel::real measure_space" "{..<DIM('a::ordered_euclidean_space)}"
+interpretation lborel_space: finite_product_sigma_finite "\<lambda>x. lborel::real measure_space" "{..<n}" for n :: nat
   where "space lborel = UNIV"
   and "sets lborel = sets borel"
   and "measure lborel = lebesgue.\<mu>"
   and "measurable lborel = measurable borel"
 proof -
-  show "finite_product_sigma_finite (\<lambda>x. lborel::real measure_space) {..<DIM('a::ordered_euclidean_space)}"
+  show "finite_product_sigma_finite (\<lambda>x. lborel::real measure_space) {..<n}"
     by default simp
 qed simp_all
 
@@ -836,7 +829,7 @@
 lemma lborel_eq_lborel_space:
   fixes A :: "('a::ordered_euclidean_space) set"
   assumes "A \<in> sets borel"
-  shows "lborel.\<mu> A = lborel_space.\<mu> TYPE('a) (p2e -` A \<inter> (space (lborel_space.P TYPE('a))))"
+  shows "lborel.\<mu> A = lborel_space.\<mu> DIM('a) (p2e -` A \<inter> (space (lborel_space.P DIM('a))))"
     (is "_ = measure ?P (?T A)")
 proof (rule measure_unique_Int_stable_vimage)
   show "measure_space ?P" by default
@@ -871,27 +864,36 @@
     qed simp }
 qed
 
+lemma measure_preserving_p2e:
+  "p2e \<in> measure_preserving (\<Pi>\<^isub>M i\<in>{..<DIM('a)}. (lborel :: real measure_space))
+    (lborel::'a::ordered_euclidean_space measure_space)" (is "_ \<in> measure_preserving ?P ?E")
+proof
+  show "p2e \<in> measurable ?P ?E"
+    using measurable_p2e by (simp add: measurable_def)
+  fix A :: "'a set" assume "A \<in> sets lborel"
+  then show "lborel_space.\<mu> DIM('a) (p2e -` A \<inter> (space (lborel_space.P DIM('a)))) = lborel.\<mu> A"
+    by (intro lborel_eq_lborel_space[symmetric]) simp
+qed
+
 lemma lebesgue_eq_lborel_space_in_borel:
   fixes A :: "('a::ordered_euclidean_space) set"
   assumes A: "A \<in> sets borel"
-  shows "lebesgue.\<mu> A = lborel_space.\<mu> TYPE('a) (p2e -` A \<inter> (space (lborel_space.P TYPE('a))))"
+  shows "lebesgue.\<mu> A = lborel_space.\<mu> DIM('a) (p2e -` A \<inter> (space (lborel_space.P DIM('a))))"
   using lborel_eq_lborel_space[OF A] by simp
 
 lemma borel_fubini_positiv_integral:
   fixes f :: "'a::ordered_euclidean_space \<Rightarrow> pextreal"
   assumes f: "f \<in> borel_measurable borel"
-  shows "integral\<^isup>P lborel f = \<integral>\<^isup>+x. f (p2e x) \<partial>(lborel_space.P TYPE('a))"
-proof (rule lborel_space.positive_integral_vimage[OF _ _ _ lborel_eq_lborel_space])
-  show "sigma_algebra lborel" by default
-  show "p2e \<in> measurable (lborel_space.P TYPE('a)) (lborel :: 'a measure_space)"
-       "f \<in> borel_measurable lborel"
-    using measurable_p2e f by (simp_all add: measurable_def)
-qed simp
+  shows "integral\<^isup>P lborel f = \<integral>\<^isup>+x. f (p2e x) \<partial>(lborel_space.P DIM('a))"
+proof (rule lborel_space.positive_integral_vimage[OF _ measure_preserving_p2e _])
+  show "f \<in> borel_measurable lborel"
+    using f by (simp_all add: measurable_def)
+qed default
 
 lemma borel_fubini_integrable:
   fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real"
   shows "integrable lborel f \<longleftrightarrow>
-    integrable (lborel_space.P TYPE('a)) (\<lambda>x. f (p2e x))"
+    integrable (lborel_space.P DIM('a)) (\<lambda>x. f (p2e x))"
     (is "_ \<longleftrightarrow> integrable ?B ?f")
 proof
   assume "integrable lborel f"
@@ -916,7 +918,7 @@
 lemma borel_fubini:
   fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real"
   assumes f: "f \<in> borel_measurable borel"
-  shows "integral\<^isup>L lborel f = \<integral>x. f (p2e x) \<partial>(lborel_space.P TYPE('a))"
+  shows "integral\<^isup>L lborel f = \<integral>x. f (p2e x) \<partial>(lborel_space.P DIM('a))"
   using f by (simp add: borel_fubini_positiv_integral lebesgue_integral_def)
 
 end
diff -r d5b294734373 -r 2f8f2685e0c0 src/HOL/Probability/Measure.thy
--- a/src/HOL/Probability/Measure.thy	Wed Feb 23 11:23:26 2011 +0100
+++ b/src/HOL/Probability/Measure.thy	Wed Feb 23 11:42:01 2011 +0100
@@ -16,6 +16,23 @@
 lemma measure_sigma[simp]: "measure (sigma A) = measure A"
   unfolding sigma_def by simp
 
+lemma algebra_measure_update[simp]:
+  "algebra (M'\<lparr>measure := m\<rparr>) \<longleftrightarrow> algebra M'"
+  unfolding algebra_def by simp
+
+lemma sigma_algebra_measure_update[simp]:
+  "sigma_algebra (M'\<lparr>measure := m\<rparr>) \<longleftrightarrow> sigma_algebra M'"
+  unfolding sigma_algebra_def sigma_algebra_axioms_def by simp
+
+lemma finite_sigma_algebra_measure_update[simp]:
+  "finite_sigma_algebra (M'\<lparr>measure := m\<rparr>) \<longleftrightarrow> finite_sigma_algebra M'"
+  unfolding finite_sigma_algebra_def finite_sigma_algebra_axioms_def by simp
+
+lemma measurable_cancel_measure[simp]:
+  "measurable M1 (M2\<lparr>measure := m2\<rparr>) = measurable M1 M2"
+  "measurable (M2\<lparr>measure := m1\<rparr>) M1 = measurable M2 M1"
+  unfolding measurable_def by auto
+
 lemma inj_on_image_eq_iff:
   assumes "inj_on f S"
   assumes "A \<subseteq> S" "B \<subseteq> S"
@@ -624,59 +641,6 @@
   ultimately show ?thesis by (simp add: isoton_def)
 qed
 
-lemma (in measure_space) measure_space_vimage:
-  fixes M' :: "('c, 'd) measure_space_scheme"
-  assumes T: "sigma_algebra M'" "T \<in> measurable M M'"
-    and \<nu>: "\<And>A. A \<in> sets M' \<Longrightarrow> measure M' A = \<mu> (T -` A \<inter> space M)"
-  shows "measure_space M'"
-proof -
-  interpret M': sigma_algebra M' by fact
-  show ?thesis
-  proof
-    show "measure M' {} = 0" using \<nu>[of "{}"] by simp
-
-    show "countably_additive M' (measure M')"
-    proof (intro countably_additiveI)
-      fix A :: "nat \<Rightarrow> 'c set" assume "range A \<subseteq> sets M'" "disjoint_family A"
-      then have A: "\<And>i. A i \<in> sets M'" "(\<Union>i. A i) \<in> sets M'" by auto
-      then have *: "range (\<lambda>i. T -` (A i) \<inter> space M) \<subseteq> sets M"
-        using `T \<in> measurable M M'` by (auto simp: measurable_def)
-      moreover have "(\<Union>i. T -`  A i \<inter> space M) \<in> sets M"
-        using * by blast
-      moreover have **: "disjoint_family (\<lambda>i. T -` A i \<inter> space M)"
-        using `disjoint_family A` by (auto simp: disjoint_family_on_def)
-      ultimately show "(\<Sum>\<^isub>\<infinity> i. measure M' (A i)) = measure M' (\<Union>i. A i)"
-        using measure_countably_additive[OF _ **] A
-        by (auto simp: comp_def vimage_UN \<nu>)
-    qed
-  qed
-qed
-
-lemma measure_unique_Int_stable_vimage:
-  fixes A :: "nat \<Rightarrow> 'a set"
-  assumes E: "Int_stable E"
-  and A: "range A \<subseteq> sets E" "A \<up> space E" "\<And>i. measure M (A i) \<noteq> \<omega>"
-  and N: "measure_space N" "T \<in> measurable N M"
-  and M: "measure_space M" "sets (sigma E) = sets M" "space E = space M"
-  and eq: "\<And>X. X \<in> sets E \<Longrightarrow> measure M X = measure N (T -` X \<inter> space N)"
-  assumes X: "X \<in> sets (sigma E)"
-  shows "measure M X = measure N (T -` X \<inter> space N)"
-proof (rule measure_unique_Int_stable[OF E A(1,2) _ _ eq _ X])
-  interpret M: measure_space M by fact
-  interpret N: measure_space N by fact
-  let "?T X" = "T -` X \<inter> space N"
-  show "measure_space \<lparr>space = space E, sets = sets (sigma E), measure = measure M\<rparr>"
-    by (rule M.measure_space_cong) (auto simp: M)
-  show "measure_space \<lparr>space = space E, sets = sets (sigma E), measure = \<lambda>X. measure N (?T X)\<rparr>" (is "measure_space ?E")
-  proof (rule N.measure_space_vimage)
-    show "sigma_algebra ?E"
-      by (rule M.sigma_algebra_cong) (auto simp: M)
-    show "T \<in> measurable N ?E"
-      using `T \<in> measurable N M` by (auto simp: M measurable_def)
-  qed simp
-  show "\<And>i. M.\<mu> (A i) \<noteq> \<omega>" by fact
-qed
-
 section "@{text \<mu>}-null sets"
 
 abbreviation (in measure_space) "null_sets \<equiv> {N\<in>sets M. \<mu> N = 0}"
@@ -991,6 +955,105 @@
   qed force+
 qed
 
+section {* Measure preserving *}
+
+definition "measure_preserving A B =
+    {f \<in> measurable A B. (\<forall>y \<in> sets B. measure A (f -` y \<inter> space A) = measure B y)}"
+
+lemma measure_preservingI[intro?]:
+  assumes "f \<in> measurable A B"
+    and "\<And>y. y \<in> sets B \<Longrightarrow> measure A (f -` y \<inter> space A) = measure B y"
+  shows "f \<in> measure_preserving A B"
+  unfolding measure_preserving_def using assms by auto
+
+lemma (in measure_space) measure_space_vimage:
+  fixes M' :: "('c, 'd) measure_space_scheme"
+  assumes T: "sigma_algebra M'" "T \<in> measure_preserving M M'"
+  shows "measure_space M'"
+proof -
+  interpret M': sigma_algebra M' by fact
+  show ?thesis
+  proof
+    show "measure M' {} = 0" using T by (force simp: measure_preserving_def)
+
+    show "countably_additive M' (measure M')"
+    proof (intro countably_additiveI)
+      fix A :: "nat \<Rightarrow> 'c set" assume "range A \<subseteq> sets M'" "disjoint_family A"
+      then have A: "\<And>i. A i \<in> sets M'" "(\<Union>i. A i) \<in> sets M'" by auto
+      then have *: "range (\<lambda>i. T -` (A i) \<inter> space M) \<subseteq> sets M"
+        using T by (auto simp: measurable_def measure_preserving_def)
+      moreover have "(\<Union>i. T -`  A i \<inter> space M) \<in> sets M"
+        using * by blast
+      moreover have **: "disjoint_family (\<lambda>i. T -` A i \<inter> space M)"
+        using `disjoint_family A` by (auto simp: disjoint_family_on_def)
+      ultimately show "(\<Sum>\<^isub>\<infinity> i. measure M' (A i)) = measure M' (\<Union>i. A i)"
+        using measure_countably_additive[OF _ **] A T
+        by (auto simp: comp_def vimage_UN measure_preserving_def)
+    qed
+  qed
+qed
+
+lemma (in measure_space) almost_everywhere_vimage:
+  assumes T: "sigma_algebra M'" "T \<in> measure_preserving M M'"
+    and AE: "measure_space.almost_everywhere M' P"
+  shows "AE x. P (T x)"
+proof -
+  interpret M': measure_space M' using T by (rule measure_space_vimage)
+  from AE[THEN M'.AE_E] guess N .
+  then show ?thesis
+    unfolding almost_everywhere_def M'.almost_everywhere_def
+    using T(2) unfolding measurable_def measure_preserving_def
+    by (intro bexI[of _ "T -` N \<inter> space M"]) auto
+qed
+
+lemma measure_unique_Int_stable_vimage:
+  fixes A :: "nat \<Rightarrow> 'a set"
+  assumes E: "Int_stable E"
+  and A: "range A \<subseteq> sets E" "A \<up> space E" "\<And>i. measure M (A i) \<noteq> \<omega>"
+  and N: "measure_space N" "T \<in> measurable N M"
+  and M: "measure_space M" "sets (sigma E) = sets M" "space E = space M"
+  and eq: "\<And>X. X \<in> sets E \<Longrightarrow> measure M X = measure N (T -` X \<inter> space N)"
+  assumes X: "X \<in> sets (sigma E)"
+  shows "measure M X = measure N (T -` X \<inter> space N)"
+proof (rule measure_unique_Int_stable[OF E A(1,2) _ _ eq _ X])
+  interpret M: measure_space M by fact
+  interpret N: measure_space N by fact
+  let "?T X" = "T -` X \<inter> space N"
+  show "measure_space \<lparr>space = space E, sets = sets (sigma E), measure = measure M\<rparr>"
+    by (rule M.measure_space_cong) (auto simp: M)
+  show "measure_space \<lparr>space = space E, sets = sets (sigma E), measure = \<lambda>X. measure N (?T X)\<rparr>" (is "measure_space ?E")
+  proof (rule N.measure_space_vimage)
+    show "sigma_algebra ?E"
+      by (rule M.sigma_algebra_cong) (auto simp: M)
+    show "T \<in> measure_preserving N ?E"
+      using `T \<in> measurable N M` by (auto simp: M measurable_def measure_preserving_def)
+  qed
+  show "\<And>i. M.\<mu> (A i) \<noteq> \<omega>" by fact
+qed
+
+lemma (in measure_space) measure_preserving_Int_stable:
+  fixes A :: "nat \<Rightarrow> 'a set"
+  assumes E: "Int_stable E" "range A \<subseteq> sets E" "A \<up> space E" "\<And>i. measure E (A i) \<noteq> \<omega>"
+  and N: "measure_space (sigma E)"
+  and T: "T \<in> measure_preserving M E"
+  shows "T \<in> measure_preserving M (sigma E)"
+proof
+  interpret E: measure_space "sigma E" by fact
+  show "T \<in> measurable M (sigma E)"
+    using T E.sets_into_space
+    by (intro measurable_sigma) (auto simp: measure_preserving_def measurable_def)
+  fix X assume "X \<in> sets (sigma E)"
+  show "\<mu> (T -` X \<inter> space M) = E.\<mu> X"
+  proof (rule measure_unique_Int_stable_vimage[symmetric])
+    show "sets (sigma E) = sets (sigma E)" "space E = space (sigma E)"
+      "\<And>i. E.\<mu> (A i) \<noteq> \<omega>" using E by auto
+    show "measure_space M" by default
+  next
+    fix X assume "X \<in> sets E" then show "E.\<mu> X = \<mu> (T -` X \<inter> space M)"
+      using T unfolding measure_preserving_def by auto
+  qed fact+
+qed
+
 section "Real measure values"
 
 lemma (in measure_space) real_measure_Union:
@@ -1230,11 +1293,6 @@
   using measure_inter_full_set[OF assms(1,2) finite_measure assms(3)] assms
   by auto
 
-section {* Measure preserving *}
-
-definition "measure_preserving A B =
-    {f \<in> measurable A B. (\<forall>y \<in> sets B. measure A (f -` y \<inter> space A) = measure B y)}"
-
 lemma (in finite_measure) measure_preserving_lift:
   fixes f :: "'a \<Rightarrow> 'c" and A :: "('c, 'd) measure_space_scheme"
   assumes "algebra A" "finite_measure (sigma A)" (is "finite_measure ?sA")
diff -r d5b294734373 -r 2f8f2685e0c0 src/HOL/Probability/Probability_Space.thy
--- a/src/HOL/Probability/Probability_Space.thy	Wed Feb 23 11:23:26 2011 +0100
+++ b/src/HOL/Probability/Probability_Space.thy	Wed Feb 23 11:42:01 2011 +0100
@@ -198,7 +198,7 @@
   interpret S: measure_space "S\<lparr>measure := distribution X\<rparr>"
     unfolding distribution_def using assms
     by (intro measure_space_vimage)
-       (auto intro!: sigma_algebra.sigma_algebra_cong[of S])
+       (auto intro!: sigma_algebra.sigma_algebra_cong[of S] simp: measure_preserving_def)
   show ?thesis
   proof (default, simp)
     have "X -` space S \<inter> space M = space M"
diff -r d5b294734373 -r 2f8f2685e0c0 src/HOL/Probability/Product_Measure.thy
--- a/src/HOL/Probability/Product_Measure.thy	Wed Feb 23 11:23:26 2011 +0100
+++ b/src/HOL/Probability/Product_Measure.thy	Wed Feb 23 11:42:01 2011 +0100
@@ -2,14 +2,6 @@
 imports Lebesgue_Integration
 begin
 
-lemma measurable_cancel_measure2[simp]:
-  "measurable M1 (M2\<lparr>measure := m\<rparr>) = measurable M1 M2"
-  unfolding measurable_def by auto
-
-lemma measurable_cancel_measure1[simp]:
-  "measurable (M1\<lparr>measure := m\<rparr>) M2 = measurable M1 M2"
-  unfolding measurable_def by auto
-
 lemma sigma_sets_subseteq: assumes "A \<subseteq> B" shows "sigma_sets X A \<subseteq> sigma_sets X B"
 proof
   fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B"
@@ -926,20 +918,27 @@
     unfolding F_SUPR by simp
 qed
 
+lemma (in pair_sigma_finite) measure_preserving_swap:
+  "(\<lambda>(x,y). (y, x)) \<in> measure_preserving (M1 \<Otimes>\<^isub>M M2) (M2 \<Otimes>\<^isub>M M1)"
+proof
+  interpret Q: pair_sigma_finite M2 M1 by default
+  show *: "(\<lambda>(x,y). (y, x)) \<in> measurable (M1 \<Otimes>\<^isub>M M2) (M2 \<Otimes>\<^isub>M M1)"
+    using pair_sigma_algebra_swap_measurable .
+  fix X assume "X \<in> sets (M2 \<Otimes>\<^isub>M M1)"
+  from measurable_sets[OF * this] this Q.sets_into_space[OF this]
+  show "measure (M1 \<Otimes>\<^isub>M M2) ((\<lambda>(x, y). (y, x)) -` X \<inter> space P) = measure (M2 \<Otimes>\<^isub>M M1) X"
+    by (auto intro!: M1.positive_integral_cong arg_cong[where f="M2.\<mu>"]
+      simp: pair_measure_alt Q.pair_measure_alt2 space_pair_measure)
+qed
+
 lemma (in pair_sigma_finite) positive_integral_product_swap:
   assumes f: "f \<in> borel_measurable P"
   shows "(\<integral>\<^isup>+x. f (case x of (x,y)\<Rightarrow>(y,x)) \<partial>(M2 \<Otimes>\<^isub>M M1)) = integral\<^isup>P P f"
 proof -
   interpret Q: pair_sigma_finite M2 M1 by default
   have "sigma_algebra P" by default
-  show ?thesis
-  proof (intro Q.positive_integral_vimage[symmetric] Q.pair_sigma_algebra_swap_measurable)
-    fix A assume "A \<in> sets P"
-    from Q.pair_sigma_algebra_swap_measurable[THEN measurable_sets, OF this] this sets_into_space[OF this]
-    show "\<mu> A = Q.\<mu> ((\<lambda>(x, y). (y, x)) -` A \<inter> space (M2 \<Otimes>\<^isub>M M1))"
-      by (auto intro!: M1.positive_integral_cong arg_cong[where f="M2.\<mu>"]
-               simp: pair_measure_alt Q.pair_measure_alt2 space_pair_measure)
-  qed fact+
+  with f show ?thesis
+    by (subst Q.positive_integral_vimage[OF _ Q.measure_preserving_swap]) auto
 qed
 
 lemma (in pair_sigma_finite) positive_integral_snd_measurable:
@@ -1405,7 +1404,8 @@
     fix i k show "\<mu> i (F i k) \<noteq> \<omega>" by fact
   next
     fix A assume "A \<in> (\<Union>i. ?F i)" then show "A \<in> space G"
-      using `\<And>i. range (F i) \<subseteq> sets (M i)` M.sets_into_space by auto blast
+      using `\<And>i. range (F i) \<subseteq> sets (M i)` M.sets_into_space
+      by (force simp: image_subset_iff)
   next
     fix f assume "f \<in> space G"
     with Pi_UN[OF finite_index, of "\<lambda>k i. F i k"]
@@ -1418,6 +1418,19 @@
   qed
 qed
 
+lemma sets_pair_cancel_measure[simp]:
+  "sets (M1\<lparr>measure := m1\<rparr> \<Otimes>\<^isub>M M2) = sets (M1 \<Otimes>\<^isub>M M2)"
+  "sets (M1 \<Otimes>\<^isub>M M2\<lparr>measure := m2\<rparr>) = sets (M1 \<Otimes>\<^isub>M M2)"
+  unfolding pair_measure_def pair_measure_generator_def sets_sigma
+  by simp_all
+
+lemma measurable_pair_cancel_measure[simp]:
+  "measurable (M1\<lparr>measure := m1\<rparr> \<Otimes>\<^isub>M M2) M = measurable (M1 \<Otimes>\<^isub>M M2) M"
+  "measurable (M1 \<Otimes>\<^isub>M M2\<lparr>measure := m2\<rparr>) M = measurable (M1 \<Otimes>\<^isub>M M2) M"
+  "measurable M (M1\<lparr>measure := m3\<rparr> \<Otimes>\<^isub>M M2) = measurable M (M1 \<Otimes>\<^isub>M M2)"
+  "measurable M (M1 \<Otimes>\<^isub>M M2\<lparr>measure := m4\<rparr>) = measurable M (M1 \<Otimes>\<^isub>M M2)"
+  unfolding measurable_def by (auto simp add: space_pair_measure)
+
 lemma (in product_sigma_finite) product_measure_exists:
   assumes "finite I"
   shows "\<exists>\<nu>. sigma_finite_measure (sigma (product_algebra_generator I M) \<lparr> measure := \<nu> \<rparr>) \<and>
@@ -1455,8 +1468,7 @@
     by (rule I'.sigma_algebra_cong) simp_all
   interpret I'': measure_space "I'.P\<lparr> measure := ?\<nu> \<rparr>"
     using measurable_add_dim[OF `i \<notin> I`]
-    by (intro P.measure_space_vimage[OF I'])
-       (simp_all add: measurable_def pair_measure_def pair_measure_generator_def sets_sigma)
+    by (intro P.measure_space_vimage[OF I']) (auto simp add: measure_preserving_def)
   show ?case
   proof (intro exI[of _ ?\<nu>] conjI ballI)
     let "?m A" = "measure (Pi\<^isub>M I M\<lparr>measure := \<nu>\<rparr> \<Otimes>\<^isub>M M i) (?h -` A \<inter> space P.P)"
@@ -1602,32 +1614,44 @@
   qed
 qed
 
+lemma (in product_sigma_finite) measure_preserving_merge:
+  assumes IJ: "I \<inter> J = {}" and "finite I" "finite J"
+  shows "(\<lambda>(x,y). merge I x J y) \<in> measure_preserving (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) (Pi\<^isub>M (I \<union> J) M)"
+  by (intro measure_preservingI measurable_merge[OF IJ] measure_fold[symmetric] assms)
+
 lemma (in product_sigma_finite) product_positive_integral_fold:
-  assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
+  assumes IJ[simp]: "I \<inter> J = {}" "finite I" "finite J"
   and f: "f \<in> borel_measurable (Pi\<^isub>M (I \<union> J) M)"
   shows "integral\<^isup>P (Pi\<^isub>M (I \<union> J) M) f =
     (\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (merge I x J y) \<partial>(Pi\<^isub>M J M)) \<partial>(Pi\<^isub>M I M))"
 proof -
   interpret I: finite_product_sigma_finite M I by default fact
   interpret J: finite_product_sigma_finite M J by default fact
-  have "finite (I \<union> J)" using fin by auto
-  interpret IJ: finite_product_sigma_finite M "I \<union> J" by default fact
-  interpret P: pair_sigma_finite I.P J.P by default
+  interpret P: pair_sigma_finite "Pi\<^isub>M I M" "Pi\<^isub>M J M" by default
+  interpret IJ: finite_product_sigma_finite M "I \<union> J" by default simp
   have P_borel: "(\<lambda>x. f (case x of (x, y) \<Rightarrow> merge I x J y)) \<in> borel_measurable P.P"
-    using measurable_comp[OF measurable_merge[OF IJ] f] by (simp add: comp_def)
+    using measurable_comp[OF measurable_merge[OF IJ(1)] f] by (simp add: comp_def)
   show ?thesis
     unfolding P.positive_integral_fst_measurable[OF P_borel, simplified]
   proof (rule P.positive_integral_vimage)
     show "sigma_algebra IJ.P" by default
-    show "(\<lambda>(x, y). merge I x J y) \<in> measurable P.P IJ.P" by (rule measurable_merge[OF IJ])
+    show "(\<lambda>(x, y). merge I x J y) \<in> measure_preserving P.P IJ.P"
+      using IJ by (rule measure_preserving_merge)
     show "f \<in> borel_measurable IJ.P" using f by simp
-  next
-    fix A assume "A \<in> sets (Pi\<^isub>M (I \<union> J) M)"
-    then show "IJ.\<mu> A = P.\<mu> ((\<lambda>(x,y). merge I x J y) -` A \<inter> space P.P)"
-      using measure_fold[OF IJ fin] by simp
   qed
 qed
 
+lemma (in product_sigma_finite) measure_preserving_component_singelton:
+  "(\<lambda>x. x i) \<in> measure_preserving (Pi\<^isub>M {i} M) (M i)"
+proof (intro measure_preservingI measurable_component_singleton)
+  interpret I: finite_product_sigma_finite M "{i}" by default simp
+  fix A let ?P = "(\<lambda>x. x i) -` A \<inter> space I.P"
+  assume A: "A \<in> sets (M i)"
+  then have *: "?P = {i} \<rightarrow>\<^isub>E A" using sets_into_space by auto
+  show "I.\<mu> ?P = M.\<mu> i A" unfolding *
+    using A I.measure_times[of "\<lambda>_. A"] by auto
+qed auto
+
 lemma (in product_sigma_finite) product_positive_integral_singleton:
   assumes f: "f \<in> borel_measurable (M i)"
   shows "integral\<^isup>P (Pi\<^isub>M {i} M) (\<lambda>x. f (x i)) = integral\<^isup>P (M i) f"
@@ -1636,14 +1660,9 @@
   show ?thesis
   proof (rule I.positive_integral_vimage[symmetric])
     show "sigma_algebra (M i)" by (rule sigma_algebras)
-    show "(\<lambda>x. x i) \<in> measurable (Pi\<^isub>M {i} M) (M i)" by (rule measurable_component_singleton) auto
+    show "(\<lambda>x. x i) \<in> measure_preserving (Pi\<^isub>M {i} M) (M i)"
+      by (rule measure_preserving_component_singelton)
     show "f \<in> borel_measurable (M i)" by fact
-  next
-    fix A let ?P = "(\<lambda>x. x i) -` A \<inter> space I.P"
-    assume A: "A \<in> sets (M i)"
-    then have *: "?P = {i} \<rightarrow>\<^isub>E A" using sets_into_space by auto
-    show "M.\<mu> i A = I.\<mu> ?P" unfolding *
-      using A I.measure_times[of "\<lambda>_. A"] by auto
   qed
 qed
 
@@ -1723,14 +1742,14 @@
   show ?thesis
   proof (subst P.integrable_fst_measurable(2)[of ?f, simplified])
     have 1: "sigma_algebra IJ.P" by default
-    have 2: "?M \<in> measurable P.P IJ.P" using measurable_merge[OF IJ] .
-    have 3: "\<And>A. A \<in> sets IJ.P \<Longrightarrow> IJ.\<mu> A = P.\<mu> (?M -` A \<inter> space P.P)"
-      by (rule measure_fold[OF IJ fin])
-    have 4: "integrable (Pi\<^isub>M (I \<union> J) M) f" by fact
+    have 2: "?M \<in> measure_preserving P.P IJ.P" using measure_preserving_merge[OF assms(1,2,3)] .
+    have 3: "integrable (Pi\<^isub>M (I \<union> J) M) f" by fact
+    then have 4: "f \<in> borel_measurable (Pi\<^isub>M (I \<union> J) M)"
+      by (simp add: integrable_def)
     show "integrable P.P ?f"
-      by (rule P.integral_vimage[where f=f, OF 1 2 3 4])
+      by (rule P.integrable_vimage[where f=f, OF 1 2 3])
     show "integral\<^isup>L IJ.P f = integral\<^isup>L P.P ?f"
-      by (rule P.integral_vimage[where f=f, OF 1 2 3 4])
+      by (rule P.integral_vimage[where f=f, OF 1 2 4])
   qed
 qed
 
diff -r d5b294734373 -r 2f8f2685e0c0 src/HOL/Probability/Radon_Nikodym.thy
--- a/src/HOL/Probability/Radon_Nikodym.thy	Wed Feb 23 11:23:26 2011 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Wed Feb 23 11:42:01 2011 +0100
@@ -74,7 +74,7 @@
 definition (in measure_space)
   "absolutely_continuous \<nu> = (\<forall>N\<in>null_sets. \<nu> N = (0 :: pextreal))"
 
-lemma (in sigma_finite_measure) absolutely_continuous_AE:
+lemma (in measure_space) absolutely_continuous_AE:
   assumes "measure_space M'" and [simp]: "sets M' = sets M" "space M' = space M"
     and "absolutely_continuous (measure M')" "AE x. P x"
   shows "measure_space.almost_everywhere M' P"
@@ -1113,6 +1113,76 @@
     unfolding eq[OF A, symmetric] RN_deriv(2)[OF \<nu> A, symmetric] ..
 qed
 
+lemma (in sigma_finite_measure) RN_deriv_vimage:
+  assumes T: "T \<in> measure_preserving M M'"
+    and T': "T' \<in> measure_preserving (M'\<lparr> measure := \<nu>' \<rparr>) (M\<lparr> measure := \<nu> \<rparr>)"
+    and inv: "\<And>x. x \<in> space M \<Longrightarrow> T' (T x) = x"
+  and \<nu>': "measure_space (M'\<lparr>measure := \<nu>'\<rparr>)" "measure_space.absolutely_continuous M' \<nu>'"
+  shows "AE x. RN_deriv M' \<nu>' (T x) = RN_deriv M \<nu> x"
+proof (rule RN_deriv_unique)
+  interpret \<nu>': measure_space "M'\<lparr>measure := \<nu>'\<rparr>" by fact
+  show "measure_space (M\<lparr> measure := \<nu>\<rparr>)"
+    by (rule \<nu>'.measure_space_vimage[OF _ T'], simp) default
+  interpret M': measure_space M'
+  proof (rule measure_space_vimage)
+    have "sigma_algebra (M'\<lparr> measure := \<nu>'\<rparr>)" by default
+    then show "sigma_algebra M'" by simp
+  qed fact
+  show "absolutely_continuous \<nu>" unfolding absolutely_continuous_def
+  proof safe
+    fix N assume N: "N \<in> sets M" and N_0: "\<mu> N = 0"
+    then have N': "T' -` N \<inter> space M' \<in> sets M'"
+      using T' by (auto simp: measurable_def measure_preserving_def)
+    have "T -` (T' -` N \<inter> space M') \<inter> space M = N"
+      using inv T N sets_into_space[OF N] by (auto simp: measurable_def measure_preserving_def)
+    then have "measure M' (T' -` N \<inter> space M') = 0"
+      using measure_preservingD[OF T N'] N_0 by auto
+    with \<nu>'(2) N' show "\<nu> N = 0" using measure_preservingD[OF T', of N] N
+      unfolding M'.absolutely_continuous_def measurable_def by auto
+  qed
+  interpret M': sigma_finite_measure M'
+  proof
+    from sigma_finite guess F .. note F = this
+    show "\<exists>A::nat \<Rightarrow> 'c set. range A \<subseteq> sets M' \<and> (\<Union>i. A i) = space M' \<and> (\<forall>i. M'.\<mu> (A i) \<noteq> \<omega>)"
+    proof (intro exI conjI allI)
+      show *: "range (\<lambda>i. T' -` F i \<inter> space M') \<subseteq> sets M'"
+        using F T' by (auto simp: measurable_def measure_preserving_def)
+      show "(\<Union>i. T' -` F i \<inter> space M') = space M'"
+        using F T' by (force simp: measurable_def measure_preserving_def)
+      fix i
+      have "T' -` F i \<inter> space M' \<in> sets M'" using * by auto
+      note measure_preservingD[OF T this, symmetric]
+      moreover
+      have Fi: "F i \<in> sets M" using F by auto
+      then have "T -` (T' -` F i \<inter> space M') \<inter> space M = F i"
+        using T inv sets_into_space[OF Fi]
+        by (auto simp: measurable_def measure_preserving_def)
+      ultimately show "measure M' (T' -` F i \<inter> space M') \<noteq> \<omega>"
+        using F by simp
+    qed
+  qed
+  have "(RN_deriv M' \<nu>') \<circ> T \<in> borel_measurable M"
+    by (intro measurable_comp[where b=M'] M'.RN_deriv(1) measure_preservingD2[OF T]) fact+
+  then show "(\<lambda>x. RN_deriv M' \<nu>' (T x)) \<in> borel_measurable M"
+    by (simp add: comp_def)
+  fix A let ?A = "T' -` A \<inter> space M'"
+  assume A: "A \<in> sets M"
+  then have A': "?A \<in> sets M'" using T' unfolding measurable_def measure_preserving_def
+    by auto
+  from A have "\<nu> A = \<nu>' ?A" using T'[THEN measure_preservingD] by simp
+  also have "\<dots> = \<integral>\<^isup>+ x. RN_deriv M' \<nu>' x * indicator ?A x \<partial>M'"
+    using A' by (rule M'.RN_deriv(2)[OF \<nu>'])
+  also have "\<dots> = \<integral>\<^isup>+ x. RN_deriv M' \<nu>' (T x) * indicator ?A (T x) \<partial>M"
+  proof (rule positive_integral_vimage)
+    show "sigma_algebra M'" by default
+    show "(\<lambda>x. RN_deriv M' \<nu>' x * indicator (T' -` A \<inter> space M') x) \<in> borel_measurable M'"
+      by (auto intro!: A' M'.RN_deriv(1)[OF \<nu>'])
+  qed fact
+  also have "\<dots> = \<integral>\<^isup>+ x. RN_deriv M' \<nu>' (T x) * indicator A x \<partial>M"
+    using T inv by (auto intro!: positive_integral_cong simp: measure_preserving_def measurable_def indicator_def)
+  finally show "\<nu> A = \<integral>\<^isup>+ x. RN_deriv M' \<nu>' (T x) * indicator A x \<partial>M" .
+qed
+
 lemma (in sigma_finite_measure) RN_deriv_finite:
   assumes sfm: "sigma_finite_measure (M\<lparr>measure := \<nu>\<rparr>)" and ac: "absolutely_continuous \<nu>"
   shows "AE x. RN_deriv M \<nu> x \<noteq> \<omega>"