use pre-image measure, instead of image
authorhoelzl
Mon Jan 24 22:29:50 2011 +0100 (2011-01-24)
changeset 41661baf1964bc468
parent 41660 7795aaab6038
child 41662 621fa31e1dbd
use pre-image measure, instead of image
src/HOL/Probability/Information.thy
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Probability/Lebesgue_Measure.thy
src/HOL/Probability/Measure.thy
src/HOL/Probability/Probability_Space.thy
src/HOL/Probability/Product_Measure.thy
src/HOL/Probability/Radon_Nikodym.thy
     1.1 --- a/src/HOL/Probability/Information.thy	Fri Jan 21 11:39:26 2011 +0100
     1.2 +++ b/src/HOL/Probability/Information.thy	Mon Jan 24 22:29:50 2011 +0100
     1.3 @@ -180,30 +180,6 @@
     1.4      by (simp add: cong \<nu>.integral_cong_measure[OF cong(2)])
     1.5  qed
     1.6  
     1.7 -lemma (in sigma_finite_measure) KL_divergence_vimage:
     1.8 -  assumes f: "bij_betw f S (space M)"
     1.9 -  assumes \<nu>: "measure_space M \<nu>" "absolutely_continuous \<nu>"
    1.10 -  shows "KL_divergence b (vimage_algebra S f) (\<lambda>A. \<nu> (f ` A)) (\<lambda>A. \<mu> (f ` A)) = KL_divergence b M \<nu> \<mu>"
    1.11 -    (is "KL_divergence b ?M ?\<nu> ?\<mu> = _")
    1.12 -proof -
    1.13 -  interpret \<nu>: measure_space M \<nu> by fact
    1.14 -  interpret v: measure_space ?M ?\<nu>
    1.15 -    using f by (rule \<nu>.measure_space_isomorphic)
    1.16 -
    1.17 -  let ?RN = "sigma_finite_measure.RN_deriv ?M ?\<mu> ?\<nu>"
    1.18 -  from RN_deriv_vimage[OF f[THEN bij_inv_the_inv_into] \<nu>]
    1.19 -  have *: "\<nu>.almost_everywhere (\<lambda>x. ?RN (the_inv_into S f x) = RN_deriv \<nu> x)"
    1.20 -    by (rule absolutely_continuous_AE[OF \<nu>])
    1.21 -
    1.22 -  show ?thesis
    1.23 -    unfolding KL_divergence_def \<nu>.integral_vimage_inv[OF f]
    1.24 -    apply (rule \<nu>.integral_cong_AE)
    1.25 -    apply (rule \<nu>.AE_mp[OF *])
    1.26 -    apply (rule \<nu>.AE_cong)
    1.27 -    apply simp
    1.28 -    done
    1.29 -qed
    1.30 -
    1.31  lemma (in finite_measure_space) KL_divergence_eq_finite:
    1.32    assumes v: "finite_measure_space M \<nu>"
    1.33    assumes ac: "absolutely_continuous \<nu>"
    1.34 @@ -259,50 +235,6 @@
    1.35      \<lparr> space = X`space M, sets = Pow (X`space M) \<rparr>
    1.36      \<lparr> space = Y`space M, sets = Pow (Y`space M) \<rparr> X Y"
    1.37  
    1.38 -lemma (in information_space) mutual_information_commute_generic:
    1.39 -  assumes X: "random_variable S X" and Y: "random_variable T Y"
    1.40 -  assumes ac: "measure_space.absolutely_continuous (sigma (pair_algebra S T))
    1.41 -   (pair_sigma_finite.pair_measure S (distribution X) T (distribution Y)) (joint_distribution X Y)"
    1.42 -  shows "mutual_information b S T X Y = mutual_information b T S Y X"
    1.43 -proof -
    1.44 -  interpret P: prob_space "sigma (pair_algebra S T)" "joint_distribution X Y"
    1.45 -    using random_variable_pairI[OF X Y] by (rule distribution_prob_space)
    1.46 -  interpret Q: prob_space "sigma (pair_algebra T S)" "joint_distribution Y X"
    1.47 -    using random_variable_pairI[OF Y X] by (rule distribution_prob_space)
    1.48 -  interpret X: prob_space S "distribution X" using X by (rule distribution_prob_space)
    1.49 -  interpret Y: prob_space T "distribution Y" using Y by (rule distribution_prob_space)
    1.50 -  interpret ST: pair_sigma_finite S "distribution X" T "distribution Y" by default
    1.51 -  interpret TS: pair_sigma_finite T "distribution Y" S "distribution X" by default
    1.52 -
    1.53 -  have ST: "measure_space (sigma (pair_algebra S T)) (joint_distribution X Y)" by default
    1.54 -  have TS: "measure_space (sigma (pair_algebra T S)) (joint_distribution Y X)" by default
    1.55 -
    1.56 -  have bij_ST: "bij_betw (\<lambda>(x, y). (y, x)) (space (sigma (pair_algebra S T))) (space (sigma (pair_algebra T S)))"
    1.57 -    by (auto intro!: inj_onI simp: space_pair_algebra bij_betw_def)
    1.58 -  have bij_TS: "bij_betw (\<lambda>(x, y). (y, x)) (space (sigma (pair_algebra T S))) (space (sigma (pair_algebra S T)))"
    1.59 -    by (auto intro!: inj_onI simp: space_pair_algebra bij_betw_def)
    1.60 -
    1.61 -  { fix A
    1.62 -    have "joint_distribution X Y ((\<lambda>(x, y). (y, x)) ` A) = joint_distribution Y X A"
    1.63 -      unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>]) }
    1.64 -  note jd_commute = this
    1.65 -
    1.66 -  { fix A assume A: "A \<in> sets (sigma (pair_algebra T S))"
    1.67 -    have *: "\<And>x y. indicator ((\<lambda>(x, y). (y, x)) ` A) (x, y) = (indicator A (y, x) :: pextreal)"
    1.68 -      unfolding indicator_def by auto
    1.69 -    have "ST.pair_measure ((\<lambda>(x, y). (y, x)) ` A) = TS.pair_measure A"
    1.70 -      unfolding ST.pair_measure_def TS.pair_measure_def
    1.71 -      using A by (auto simp add: TS.Fubini[symmetric] *) }
    1.72 -  note pair_measure_commute = this
    1.73 -
    1.74 -  show ?thesis
    1.75 -    unfolding mutual_information_def
    1.76 -    unfolding ST.KL_divergence_vimage[OF bij_TS ST ac, symmetric]
    1.77 -    unfolding space_sigma space_pair_algebra jd_commute
    1.78 -    unfolding ST.pair_sigma_algebra_swap[symmetric]
    1.79 -    by (simp cong: TS.KL_divergence_cong[OF TS] add: pair_measure_commute)
    1.80 -qed
    1.81 -
    1.82  lemma (in prob_space) finite_variables_absolutely_continuous:
    1.83    assumes X: "finite_random_variable S X" and Y: "finite_random_variable T Y"
    1.84    shows "measure_space.absolutely_continuous (sigma (pair_algebra S T))
    1.85 @@ -330,16 +262,6 @@
    1.86    qed
    1.87  qed
    1.88  
    1.89 -lemma (in information_space) mutual_information_commute:
    1.90 -  assumes X: "finite_random_variable S X" and Y: "finite_random_variable T Y"
    1.91 -  shows "mutual_information b S T X Y = mutual_information b T S Y X"
    1.92 -  by (intro finite_random_variableD X Y mutual_information_commute_generic finite_variables_absolutely_continuous)
    1.93 -
    1.94 -lemma (in information_space) mutual_information_commute_simple:
    1.95 -  assumes X: "simple_function X" and Y: "simple_function Y"
    1.96 -  shows "\<I>(X;Y) = \<I>(Y;X)"
    1.97 -  by (intro X Y simple_function_imp_finite_random_variable mutual_information_commute)
    1.98 -
    1.99  lemma (in information_space)
   1.100    assumes MX: "finite_random_variable MX X"
   1.101    assumes MY: "finite_random_variable MY Y"
   1.102 @@ -371,6 +293,18 @@
   1.103      unfolding mutual_information_def .
   1.104  qed
   1.105  
   1.106 +lemma (in information_space) mutual_information_commute:
   1.107 +  assumes X: "finite_random_variable S X" and Y: "finite_random_variable T Y"
   1.108 +  shows "mutual_information b S T X Y = mutual_information b T S Y X"
   1.109 +  unfolding mutual_information_generic_eq[OF X Y] mutual_information_generic_eq[OF Y X]
   1.110 +  unfolding joint_distribution_commute_singleton[of X Y]
   1.111 +  by (auto simp add: ac_simps intro!: setsum_reindex_cong[OF swap_inj_on])
   1.112 +
   1.113 +lemma (in information_space) mutual_information_commute_simple:
   1.114 +  assumes X: "simple_function X" and Y: "simple_function Y"
   1.115 +  shows "\<I>(X;Y) = \<I>(Y;X)"
   1.116 +  by (intro X Y simple_function_imp_finite_random_variable mutual_information_commute)
   1.117 +
   1.118  lemma (in information_space) mutual_information_eq:
   1.119    assumes "simple_function X" "simple_function Y"
   1.120    shows "\<I>(X;Y) = (\<Sum> (x,y) \<in> X ` space M \<times> Y ` space M.
     2.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Fri Jan 21 11:39:26 2011 +0100
     2.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Mon Jan 24 22:29:50 2011 +0100
     2.3 @@ -471,20 +471,26 @@
     2.4    unfolding sigma_algebra.simple_function_def[OF N_subalgebra(3)]
     2.5    by auto
     2.6  
     2.7 -lemma (in sigma_algebra) simple_function_vimage:
     2.8 -  fixes g :: "'a \<Rightarrow> pextreal" and f :: "'d \<Rightarrow> 'a"
     2.9 -  assumes g: "simple_function g" and f: "f \<in> S \<rightarrow> space M"
    2.10 -  shows "sigma_algebra.simple_function (vimage_algebra S f) (\<lambda>x. g (f x))"
    2.11 -proof -
    2.12 -  have subset: "(\<lambda>x. g (f x)) ` S \<subseteq> g ` space M"
    2.13 -    using f by auto
    2.14 -  interpret V: sigma_algebra "vimage_algebra S f"
    2.15 -    using f by (rule sigma_algebra_vimage)
    2.16 -  show ?thesis using g
    2.17 -    unfolding simple_function_eq_borel_measurable
    2.18 -    unfolding V.simple_function_eq_borel_measurable
    2.19 -    using measurable_vimage[OF _ f, of g borel]
    2.20 -    using finite_subset[OF subset] by auto
    2.21 +lemma (in measure_space) simple_function_vimage:
    2.22 +  assumes T: "sigma_algebra M'" "T \<in> measurable M M'"
    2.23 +    and f: "sigma_algebra.simple_function M' f"
    2.24 +  shows "simple_function (\<lambda>x. f (T x))"
    2.25 +proof (intro simple_function_def[THEN iffD2] conjI ballI)
    2.26 +  interpret T: sigma_algebra M' by fact
    2.27 +  have "(\<lambda>x. f (T x)) ` space M \<subseteq> f ` space M'"
    2.28 +    using T unfolding measurable_def by auto
    2.29 +  then show "finite ((\<lambda>x. f (T x)) ` space M)"
    2.30 +    using f unfolding T.simple_function_def by (auto intro: finite_subset)
    2.31 +  fix i assume i: "i \<in> (\<lambda>x. f (T x)) ` space M"
    2.32 +  then have "i \<in> f ` space M'"
    2.33 +    using T unfolding measurable_def by auto
    2.34 +  then have "f -` {i} \<inter> space M' \<in> sets M'"
    2.35 +    using f unfolding T.simple_function_def by auto
    2.36 +  then have "T -` (f -` {i} \<inter> space M') \<inter> space M \<in> sets M"
    2.37 +    using T unfolding measurable_def by auto
    2.38 +  also have "T -` (f -` {i} \<inter> space M') \<inter> space M = (\<lambda>x. f (T x)) -` {i} \<inter> space M"
    2.39 +    using T unfolding measurable_def by auto
    2.40 +  finally show "(\<lambda>x. f (T x)) -` {i} \<inter> space M \<in> sets M" .
    2.41  qed
    2.42  
    2.43  section "Simple integral"
    2.44 @@ -816,28 +822,30 @@
    2.45    unfolding measure_space.simple_integral_def_raw[OF N] by simp
    2.46  
    2.47  lemma (in measure_space) simple_integral_vimage:
    2.48 -  fixes g :: "'a \<Rightarrow> pextreal" and f :: "'d \<Rightarrow> 'a"
    2.49 -  assumes f: "bij_betw f S (space M)"
    2.50 -  shows "simple_integral g =
    2.51 -         measure_space.simple_integral (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) (\<lambda>x. g (f x))"
    2.52 -    (is "_ = measure_space.simple_integral ?T ?\<mu> _")
    2.53 +  assumes T: "sigma_algebra M'" "T \<in> measurable M M'"
    2.54 +    and f: "sigma_algebra.simple_function M' f"
    2.55 +  shows "measure_space.simple_integral M' (\<lambda>A. \<mu> (T -` A \<inter> space M)) f = (\<integral>\<^isup>S x. f (T x))"
    2.56 +    (is "measure_space.simple_integral M' ?nu f = _")
    2.57  proof -
    2.58 -  from f interpret T: measure_space ?T ?\<mu> by (rule measure_space_isomorphic)
    2.59 -  have surj: "f`S = space M"
    2.60 -    using f unfolding bij_betw_def by simp
    2.61 -  have *: "(\<lambda>x. g (f x)) ` S = g ` f ` S" by auto
    2.62 -  have **: "f`S = space M" using f unfolding bij_betw_def by auto
    2.63 -  { fix x assume "x \<in> space M"
    2.64 -    have "(f ` ((\<lambda>x. g (f x)) -` {g x} \<inter> S)) =
    2.65 -      (f ` (f -` (g -` {g x}) \<inter> S))" by auto
    2.66 -    also have "f -` (g -` {g x}) \<inter> S = f -` (g -` {g x} \<inter> space M) \<inter> S"
    2.67 -      using f unfolding bij_betw_def by auto
    2.68 -    also have "(f ` (f -` (g -` {g x} \<inter> space M) \<inter> S)) = g -` {g x} \<inter> space M"
    2.69 -      using ** by (intro image_vimage_inter_eq) auto
    2.70 -    finally have "(f ` ((\<lambda>x. g (f x)) -` {g x} \<inter> S)) = g -` {g x} \<inter> space M" by auto }
    2.71 -  then show ?thesis using assms
    2.72 -    unfolding simple_integral_def T.simple_integral_def bij_betw_def
    2.73 -    by (auto simp add: * intro!: setsum_cong)
    2.74 +  interpret T: measure_space M' ?nu using T by (rule measure_space_vimage) auto
    2.75 +  show "T.simple_integral f = (\<integral>\<^isup>S x. f (T x))"
    2.76 +    unfolding simple_integral_def T.simple_integral_def
    2.77 +  proof (intro setsum_mono_zero_cong_right ballI)
    2.78 +    show "(\<lambda>x. f (T x)) ` space M \<subseteq> f ` space M'"
    2.79 +      using T unfolding measurable_def by auto
    2.80 +    show "finite (f ` space M')"
    2.81 +      using f unfolding T.simple_function_def by auto
    2.82 +  next
    2.83 +    fix i assume "i \<in> f ` space M' - (\<lambda>x. f (T x)) ` space M"
    2.84 +    then have "T -` (f -` {i} \<inter> space M') \<inter> space M = {}" by (auto simp: image_iff)
    2.85 +    then show "i * \<mu> (T -` (f -` {i} \<inter> space M') \<inter> space M) = 0" by simp
    2.86 +  next
    2.87 +    fix i assume "i \<in> (\<lambda>x. f (T x)) ` space M"
    2.88 +    then have "T -` (f -` {i} \<inter> space M') \<inter> space M = (\<lambda>x. f (T x)) -` {i} \<inter> space M"
    2.89 +      using T unfolding measurable_def by auto
    2.90 +    then show "i * \<mu> (T -` (f -` {i} \<inter> space M') \<inter> space M) = i * \<mu> ((\<lambda>x. f (T x)) -` {i} \<inter> space M)"
    2.91 +      by auto
    2.92 +  qed
    2.93  qed
    2.94  
    2.95  section "Continuous posititve integration"
    2.96 @@ -1016,71 +1024,6 @@
    2.97    shows "f ` A = g ` B"
    2.98    using assms by blast
    2.99  
   2.100 -lemma (in measure_space) positive_integral_vimage:
   2.101 -  fixes g :: "'a \<Rightarrow> pextreal" and f :: "'d \<Rightarrow> 'a"
   2.102 -  assumes f: "bij_betw f S (space M)"
   2.103 -  shows "positive_integral g =
   2.104 -         measure_space.positive_integral (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) (\<lambda>x. g (f x))"
   2.105 -    (is "_ = measure_space.positive_integral ?T ?\<mu> _")
   2.106 -proof -
   2.107 -  from f interpret T: measure_space ?T ?\<mu> by (rule measure_space_isomorphic)
   2.108 -  have f_fun: "f \<in> S \<rightarrow> space M" using assms unfolding bij_betw_def by auto
   2.109 -  from assms have inv: "bij_betw (the_inv_into S f) (space M) S"
   2.110 -    by (rule bij_betw_the_inv_into)
   2.111 -  then have inv_fun: "the_inv_into S f \<in> space M \<rightarrow> S" unfolding bij_betw_def by auto
   2.112 -  have surj: "f`S = space M"
   2.113 -    using f unfolding bij_betw_def by simp
   2.114 -  have inj: "inj_on f S"
   2.115 -    using f unfolding bij_betw_def by simp
   2.116 -  have inv_f: "\<And>x. x \<in> space M \<Longrightarrow> f (the_inv_into S f x) = x"
   2.117 -    using f_the_inv_into_f[of f S] f unfolding bij_betw_def by auto
   2.118 -  from simple_integral_vimage[OF assms, symmetric]
   2.119 -  have *: "simple_integral = T.simple_integral \<circ> (\<lambda>g. g \<circ> f)" by (simp add: comp_def)
   2.120 -  show ?thesis
   2.121 -    unfolding positive_integral_alt1 T.positive_integral_alt1 SUPR_def * image_compose
   2.122 -  proof (safe intro!: arg_cong[where f=Sup] image_set_cong, simp_all add: comp_def)
   2.123 -    fix g' :: "'a \<Rightarrow> pextreal" assume "simple_function g'" "\<forall>x\<in>space M. g' x \<le> g x \<and> g' x \<noteq> \<omega>"
   2.124 -    then show "\<exists>h. T.simple_function h \<and> (\<forall>x\<in>S. h x \<le> g (f x) \<and> h x \<noteq> \<omega>) \<and>
   2.125 -                   T.simple_integral (\<lambda>x. g' (f x)) = T.simple_integral h"
   2.126 -      using f unfolding bij_betw_def
   2.127 -      by (auto intro!: exI[of _ "\<lambda>x. g' (f x)"]
   2.128 -               simp add: le_fun_def simple_function_vimage[OF _ f_fun])
   2.129 -  next
   2.130 -    fix g' :: "'d \<Rightarrow> pextreal" assume g': "T.simple_function g'" "\<forall>x\<in>S. g' x \<le> g (f x) \<and> g' x \<noteq> \<omega>"
   2.131 -    let ?g = "\<lambda>x. g' (the_inv_into S f x)"
   2.132 -    show "\<exists>h. simple_function h \<and> (\<forall>x\<in>space M. h x \<le> g x \<and> h x \<noteq> \<omega>) \<and>
   2.133 -              T.simple_integral g' = T.simple_integral (\<lambda>x. h (f x))"
   2.134 -    proof (intro exI[of _ ?g] conjI ballI)
   2.135 -      { fix x assume x: "x \<in> space M"
   2.136 -        then have "the_inv_into S f x \<in> S" using inv_fun by auto
   2.137 -        with g' have "g' (the_inv_into S f x) \<le> g (f (the_inv_into S f x)) \<and> g' (the_inv_into S f x) \<noteq> \<omega>"
   2.138 -          by auto
   2.139 -        then show "g' (the_inv_into S f x) \<le> g x" "g' (the_inv_into S f x) \<noteq> \<omega>"
   2.140 -          using f_the_inv_into_f[of f S x] x f unfolding bij_betw_def by auto }
   2.141 -      note vimage_vimage_inv[OF f inv_f inv_fun, simp]
   2.142 -      from T.simple_function_vimage[OF g'(1), unfolded space_vimage_algebra, OF inv_fun]
   2.143 -      show "simple_function (\<lambda>x. g' (the_inv_into S f x))"
   2.144 -        unfolding simple_function_def by (simp add: simple_function_def)
   2.145 -      show "T.simple_integral g' = T.simple_integral (\<lambda>x. ?g (f x))"
   2.146 -        using the_inv_into_f_f[OF inj] by (auto intro!: T.simple_integral_cong)
   2.147 -    qed
   2.148 -  qed
   2.149 -qed
   2.150 -
   2.151 -lemma (in measure_space) positive_integral_vimage_inv:
   2.152 -  fixes g :: "'d \<Rightarrow> pextreal" and f :: "'d \<Rightarrow> 'a"
   2.153 -  assumes f: "bij_inv S (space M) f h"
   2.154 -  shows "measure_space.positive_integral (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) g =
   2.155 -      (\<integral>\<^isup>+x. g (h x))"
   2.156 -proof -
   2.157 -  interpret v: measure_space "vimage_algebra S f" "\<lambda>A. \<mu> (f ` A)"
   2.158 -    using f by (rule measure_space_isomorphic[OF bij_inv_bij_betw(1)])
   2.159 -  show ?thesis
   2.160 -    unfolding positive_integral_vimage[OF f[THEN bij_inv_bij_betw(1)], of "\<lambda>x. g (h x)"]
   2.161 -    using f[unfolded bij_inv_def]
   2.162 -    by (auto intro!: v.positive_integral_cong)
   2.163 -qed
   2.164 -
   2.165  lemma (in measure_space) positive_integral_SUP_approx:
   2.166    assumes "f \<up> s"
   2.167    and f: "\<And>i. f i \<in> borel_measurable M"
   2.168 @@ -1245,6 +1188,23 @@
   2.169    using positive_integral_isoton[OF `f \<up> u` e(1)[THEN borel_measurable_simple_function]]
   2.170    unfolding positive_integral_eq_simple_integral[OF e] .
   2.171  
   2.172 +lemma (in measure_space) positive_integral_vimage:
   2.173 +  assumes T: "sigma_algebra M'" "T \<in> measurable M M'" and f: "f \<in> borel_measurable M'"
   2.174 +  shows "measure_space.positive_integral M' (\<lambda>A. \<mu> (T -` A \<inter> space M)) f = (\<integral>\<^isup>+ x. f (T x))"
   2.175 +    (is "measure_space.positive_integral M' ?nu f = _")
   2.176 +proof -
   2.177 +  interpret T: measure_space M' ?nu using T by (rule measure_space_vimage) auto
   2.178 +  obtain f' where f': "f' \<up> f" "\<And>i. T.simple_function (f' i)"
   2.179 +    using T.borel_measurable_implies_simple_function_sequence[OF f] by blast
   2.180 +  then have f: "(\<lambda>i x. f' i (T x)) \<up> (\<lambda>x. f (T x))" "\<And>i. simple_function (\<lambda>x. f' i (T x))"
   2.181 +    using simple_function_vimage[OF T] unfolding isoton_fun_expand by auto
   2.182 +  show "T.positive_integral f = (\<integral>\<^isup>+ x. f (T x))"
   2.183 +    using positive_integral_isoton_simple[OF f]
   2.184 +    using T.positive_integral_isoton_simple[OF f']
   2.185 +    unfolding simple_integral_vimage[OF T f'(2)] isoton_def
   2.186 +    by simp
   2.187 +qed
   2.188 +
   2.189  lemma (in measure_space) positive_integral_linear:
   2.190    assumes f: "f \<in> borel_measurable M"
   2.191    and g: "g \<in> borel_measurable M"
   2.192 @@ -1614,21 +1574,21 @@
   2.193    thus ?thesis by (simp del: Real_eq_0 add: integral_def)
   2.194  qed
   2.195  
   2.196 -lemma (in measure_space) integral_vimage_inv:
   2.197 -  assumes f: "bij_betw f S (space M)"
   2.198 -  shows "measure_space.integral (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) (\<lambda>x. g x) = (\<integral>x. g (the_inv_into S f x))"
   2.199 +lemma (in measure_space) integral_vimage:
   2.200 +  assumes T: "sigma_algebra M'" "T \<in> measurable M M'"
   2.201 +  assumes f: "measure_space.integrable M' (\<lambda>A. \<mu> (T -` A \<inter> space M)) f"
   2.202 +  shows "integrable (\<lambda>x. f (T x))" (is ?P)
   2.203 +    and "measure_space.integral M' (\<lambda>A. \<mu> (T -` A \<inter> space M)) f = (\<integral>x. f (T x))" (is ?I)
   2.204  proof -
   2.205 -  interpret v: measure_space "vimage_algebra S f" "\<lambda>A. \<mu> (f ` A)"
   2.206 -    using f by (rule measure_space_isomorphic)
   2.207 -  have "\<And>x. x \<in> space (vimage_algebra S f) \<Longrightarrow> the_inv_into S f (f x) = x"
   2.208 -    using f[unfolded bij_betw_def] by (simp add: the_inv_into_f_f)
   2.209 -  then have *: "v.positive_integral (\<lambda>x. Real (g (the_inv_into S f (f x)))) = v.positive_integral (\<lambda>x. Real (g x))"
   2.210 -     "v.positive_integral (\<lambda>x. Real (- g (the_inv_into S f (f x)))) = v.positive_integral (\<lambda>x. Real (- g x))"
   2.211 -    by (auto intro!: v.positive_integral_cong)
   2.212 -  show ?thesis
   2.213 -    unfolding integral_def v.integral_def
   2.214 -    unfolding positive_integral_vimage[OF f]
   2.215 -    by (simp add: *)
   2.216 +  interpret T: measure_space M' "\<lambda>A. \<mu> (T -` A \<inter> space M)"
   2.217 +    using T by (rule measure_space_vimage) auto
   2.218 +  from measurable_comp[OF T(2), of f borel]
   2.219 +  have borel: "(\<lambda>x. Real (f x)) \<in> borel_measurable M'" "(\<lambda>x. Real (- f x)) \<in> borel_measurable M'"
   2.220 +    and "(\<lambda>x. f (T x)) \<in> borel_measurable M"
   2.221 +    using f unfolding T.integrable_def by (auto simp: comp_def)
   2.222 +  then show ?P ?I
   2.223 +    using f unfolding T.integral_def integral_def T.integrable_def integrable_def
   2.224 +    unfolding borel[THEN positive_integral_vimage[OF T]] by auto
   2.225  qed
   2.226  
   2.227  lemma (in measure_space) integral_minus[intro, simp]:
     3.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Fri Jan 21 11:39:26 2011 +0100
     3.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Mon Jan 24 22:29:50 2011 +0100
     3.3 @@ -45,6 +45,8 @@
     3.4  definition lebesgue :: "'a::ordered_euclidean_space algebra" where
     3.5    "lebesgue = \<lparr> space = UNIV, sets = {A. \<forall>n. (indicator A :: 'a \<Rightarrow> real) integrable_on cube n} \<rparr>"
     3.6  
     3.7 +definition "lmeasure A = (SUP n. Real (integral (cube n) (indicator A)))"
     3.8 +
     3.9  lemma space_lebesgue[simp]: "space lebesgue = UNIV"
    3.10    unfolding lebesgue_def by simp
    3.11  
    3.12 @@ -104,8 +106,6 @@
    3.13    qed (auto intro: LIMSEQ_indicator_UN simp: cube_def)
    3.14  qed simp
    3.15  
    3.16 -definition "lmeasure A = (SUP n. Real (integral (cube n) (indicator A)))"
    3.17 -
    3.18  interpretation lebesgue: measure_space lebesgue lmeasure
    3.19  proof
    3.20    have *: "indicator {} = (\<lambda>x. 0 :: real)" by (simp add: fun_eq_iff)
    3.21 @@ -736,6 +736,21 @@
    3.22    show "p2e \<in> ?P \<rightarrow> ?U" "e2p \<in> ?U \<rightarrow> ?P" by (auto simp: e2p_def)
    3.23  qed auto
    3.24  
    3.25 +declare restrict_extensional[intro]
    3.26 +
    3.27 +lemma e2p_extensional[intro]:"e2p (y::'a::ordered_euclidean_space) \<in> extensional {..<DIM('a)}"
    3.28 +  unfolding e2p_def by auto
    3.29 +
    3.30 +lemma e2p_image_vimage: fixes A::"'a::ordered_euclidean_space set"
    3.31 +  shows "e2p ` A = p2e -` A \<inter> extensional {..<DIM('a)}"
    3.32 +proof(rule set_eqI,rule)
    3.33 +  fix x assume "x \<in> e2p ` A" then guess y unfolding image_iff .. note y=this
    3.34 +  show "x \<in> p2e -` A \<inter> extensional {..<DIM('a)}"
    3.35 +    apply safe apply(rule vimageI[OF _ y(1)]) unfolding y p2e_e2p by auto
    3.36 +next fix x assume "x \<in> p2e -` A \<inter> extensional {..<DIM('a)}"
    3.37 +  thus "x \<in> e2p ` A" unfolding image_iff apply(rule_tac x="p2e x" in bexI) apply(subst e2p_p2e) by auto
    3.38 +qed
    3.39 +
    3.40  interpretation borel_product: product_sigma_finite "\<lambda>x. borel::real algebra" "\<lambda>x. lmeasure"
    3.41    by default
    3.42  
    3.43 @@ -767,6 +782,14 @@
    3.44    then show "e2p -` A \<inter> space ?E \<in> sets ?E" by simp
    3.45  qed
    3.46  
    3.47 +lemma measurable_e2p:
    3.48 +  "e2p \<in> measurable (borel::'a algebra)
    3.49 +                    (sigma (product_algebra (\<lambda>x. borel :: real algebra) {..<DIM('a::ordered_euclidean_space)}))"
    3.50 +  using measurable_e2p_on_generator[where 'a='a] unfolding borel_eq_lessThan
    3.51 +  by (subst sigma_product_algebra_sigma_eq[where S="\<lambda>_ i. {..<real i}"])
    3.52 +     (auto intro!: measurable_sigma_sigma isotoneI real_arch_lt
    3.53 +           simp: product_algebra_def)
    3.54 +
    3.55  lemma measurable_p2e_on_generator:
    3.56    "p2e \<in> measurable
    3.57      (product_algebra
    3.58 @@ -785,33 +808,13 @@
    3.59    then show "p2e -` A \<inter> space ?P \<in> sets ?P" by auto
    3.60  qed
    3.61  
    3.62 -lemma borel_vimage_algebra_eq:
    3.63 -  defines "F \<equiv> product_algebra (\<lambda>x. \<lparr> space = (UNIV::real set), sets = range lessThan \<rparr>) {..<DIM('a::ordered_euclidean_space)}"
    3.64 -  shows "sigma_algebra.vimage_algebra (borel::'a::ordered_euclidean_space algebra) (space (sigma F)) p2e = sigma F"
    3.65 -  unfolding borel_eq_lessThan
    3.66 -proof (intro vimage_algebra_sigma)
    3.67 -  let ?E = "\<lparr>space = (UNIV::'a set), sets = range lessThan\<rparr>"
    3.68 -  show "bij_inv (space (sigma F)) (space (sigma ?E)) p2e e2p"
    3.69 -    using bij_inv_p2e_e2p unfolding F_def by simp
    3.70 -  show "sets F \<subseteq> Pow (space F)" "sets ?E \<subseteq> Pow (space ?E)" unfolding F_def
    3.71 -    by (intro product_algebra_sets_into_space) auto
    3.72 -  show "p2e \<in> measurable F ?E"
    3.73 -    "e2p \<in> measurable ?E F"
    3.74 -    unfolding F_def using measurable_p2e_on_generator measurable_e2p_on_generator by auto
    3.75 -qed
    3.76 -
    3.77 -lemma product_borel_eq_vimage:
    3.78 -  "sigma (product_algebra (\<lambda>x. borel) {..<DIM('a::ordered_euclidean_space)}) =
    3.79 -  sigma_algebra.vimage_algebra borel (extensional {..<DIM('a)})
    3.80 -  (p2e:: _ \<Rightarrow> 'a::ordered_euclidean_space)"
    3.81 -  unfolding borel_vimage_algebra_eq[simplified]
    3.82 -  unfolding borel_eq_lessThan
    3.83 -  apply(subst sigma_product_algebra_sigma_eq[where S="\<lambda>i. \<lambda>n. lessThan (real n)"])
    3.84 -  unfolding lessThan_iff
    3.85 -proof- fix i assume i:"i<DIM('a)"
    3.86 -  show "(\<lambda>n. {..<real n}) \<up> space \<lparr>space = UNIV, sets = range lessThan\<rparr>"
    3.87 -    by(auto intro!:real_arch_lt isotoneI)
    3.88 -qed auto
    3.89 +lemma measurable_p2e:
    3.90 +  "p2e \<in> measurable (sigma (product_algebra (\<lambda>x. borel :: real algebra) {..<DIM('a::ordered_euclidean_space)}))
    3.91 +                    (borel::'a algebra)"
    3.92 +  using measurable_p2e_on_generator[where 'a='a] unfolding borel_eq_lessThan
    3.93 +  by (subst sigma_product_algebra_sigma_eq[where S="\<lambda>_ i. {..<real i}"])
    3.94 +     (auto intro!: measurable_sigma_sigma isotoneI real_arch_lt
    3.95 +           simp: product_algebra_def)
    3.96  
    3.97  lemma e2p_Int:"e2p ` A \<inter> e2p ` B = e2p ` (A \<inter> B)" (is "?L = ?R")
    3.98    apply(rule image_Int[THEN sym])
    3.99 @@ -834,42 +837,12 @@
   3.100    unfolding Int_stable_def algebra.select_convs
   3.101    apply safe unfolding inter_interval by auto
   3.102  
   3.103 -lemma inj_on_disjoint_family_on: assumes "disjoint_family_on A S" "inj f"
   3.104 -  shows "disjoint_family_on (\<lambda>x. f ` A x) S"
   3.105 -  unfolding disjoint_family_on_def
   3.106 -proof(rule,rule,rule)
   3.107 -  fix x1 x2 assume x:"x1 \<in> S" "x2 \<in> S" "x1 \<noteq> x2"
   3.108 -  show "f ` A x1 \<inter> f ` A x2 = {}"
   3.109 -  proof(rule ccontr) case goal1
   3.110 -    then obtain z where z:"z \<in> f ` A x1 \<inter> f ` A x2" by auto
   3.111 -    then obtain z1 z2 where z12:"z1 \<in> A x1" "z2 \<in> A x2" "f z1 = z" "f z2 = z" by auto
   3.112 -    hence "z1 = z2" using assms(2) unfolding inj_on_def by blast
   3.113 -    hence "x1 = x2" using z12(1-2) using assms[unfolded disjoint_family_on_def] using x by auto
   3.114 -    thus False using x(3) by auto
   3.115 -  qed
   3.116 -qed
   3.117 -
   3.118 -declare restrict_extensional[intro]
   3.119 -
   3.120 -lemma e2p_extensional[intro]:"e2p (y::'a::ordered_euclidean_space) \<in> extensional {..<DIM('a)}"
   3.121 -  unfolding e2p_def by auto
   3.122 -
   3.123 -lemma e2p_image_vimage: fixes A::"'a::ordered_euclidean_space set"
   3.124 -  shows "e2p ` A = p2e -` A \<inter> extensional {..<DIM('a)}"
   3.125 -proof(rule set_eqI,rule)
   3.126 -  fix x assume "x \<in> e2p ` A" then guess y unfolding image_iff .. note y=this
   3.127 -  show "x \<in> p2e -` A \<inter> extensional {..<DIM('a)}"
   3.128 -    apply safe apply(rule vimageI[OF _ y(1)]) unfolding y p2e_e2p by auto
   3.129 -next fix x assume "x \<in> p2e -` A \<inter> extensional {..<DIM('a)}"
   3.130 -  thus "x \<in> e2p ` A" unfolding image_iff apply(rule_tac x="p2e x" in bexI) apply(subst e2p_p2e) by auto
   3.131 -qed
   3.132 -
   3.133  lemma lmeasure_measure_eq_borel_prod:
   3.134    fixes A :: "('a::ordered_euclidean_space) set"
   3.135    assumes "A \<in> sets borel"
   3.136    shows "lmeasure A = borel_product.product_measure {..<DIM('a)} (e2p ` A :: (nat \<Rightarrow> real) set)"
   3.137  proof (rule measure_unique_Int_stable[where X=A and A=cube])
   3.138 -  interpret fprod: finite_product_sigma_finite "\<lambda>x. borel" "\<lambda>x. lmeasure" "{..<DIM('a)}" by default auto
   3.139 +  interpret fprod: finite_product_sigma_finite "\<lambda>x. borel :: real algebra" "\<lambda>x. lmeasure" "{..<DIM('a)}" by default auto
   3.140    show "Int_stable \<lparr> space = UNIV :: 'a set, sets = range (\<lambda>(a,b). {a..b}) \<rparr>"
   3.141      (is "Int_stable ?E" ) using Int_stable_cuboids' .
   3.142    show "borel = sigma ?E" using borel_eq_atLeastAtMost .
   3.143 @@ -906,64 +879,19 @@
   3.144    show "measure_space borel lmeasure" by default
   3.145    show "measure_space borel
   3.146       (\<lambda>a::'a set. finite_product_sigma_finite.measure (\<lambda>x. borel) (\<lambda>x. lmeasure) {..<DIM('a)} (e2p ` a))"
   3.147 -    apply default unfolding countably_additive_def
   3.148 -  proof safe fix A::"nat \<Rightarrow> 'a set" assume A:"range A \<subseteq> sets borel" "disjoint_family A"
   3.149 -      "(\<Union>i. A i) \<in> sets borel"
   3.150 -    note fprod.ca[unfolded countably_additive_def,rule_format]
   3.151 -    note ca = this[of "\<lambda> n. e2p ` (A n)"]
   3.152 -    show "(\<Sum>\<^isub>\<infinity>n. finite_product_sigma_finite.measure
   3.153 -        (\<lambda>x. borel) (\<lambda>x. lmeasure) {..<DIM('a)} (e2p ` A n)) =
   3.154 -           finite_product_sigma_finite.measure (\<lambda>x. borel)
   3.155 -            (\<lambda>x. lmeasure) {..<DIM('a)} (e2p ` (\<Union>i. A i))" unfolding image_UN
   3.156 -    proof(rule ca) show "range (\<lambda>n. e2p ` A n) \<subseteq> sets
   3.157 -       (sigma (product_algebra (\<lambda>x. borel) {..<DIM('a)}))"
   3.158 -        unfolding product_borel_eq_vimage
   3.159 -      proof case goal1
   3.160 -        then guess y unfolding image_iff .. note y=this(2)
   3.161 -        show ?case unfolding borel.in_vimage_algebra y apply-
   3.162 -          apply(rule_tac x="A y" in bexI,rule e2p_image_vimage)
   3.163 -          using A(1) by auto
   3.164 -      qed
   3.165 -
   3.166 -      show "disjoint_family (\<lambda>n. e2p ` A n)" apply(rule inj_on_disjoint_family_on)
   3.167 -        using bij_inv_p2e_e2p[THEN bij_inv_bij_betw(2)] using A(2) unfolding bij_betw_def by auto
   3.168 -      show "(\<Union>n. e2p ` A n) \<in> sets (sigma (product_algebra (\<lambda>x. borel) {..<DIM('a)}))"
   3.169 -        unfolding product_borel_eq_vimage borel.in_vimage_algebra
   3.170 -      proof(rule bexI[OF _ A(3)],rule set_eqI,rule)
   3.171 -        fix x assume x:"x \<in> (\<Union>n. e2p ` A n)" hence "p2e x \<in> (\<Union>i. A i)" by auto
   3.172 -        moreover have "x \<in> extensional {..<DIM('a)}"
   3.173 -          using x unfolding extensional_def e2p_def_raw by auto
   3.174 -        ultimately show "x \<in> p2e -` (\<Union>i. A i) \<inter> extensional {..<DIM('a)}" by auto
   3.175 -      next fix x assume x:"x \<in> p2e -` (\<Union>i. A i) \<inter> extensional {..<DIM('a)}"
   3.176 -        hence "p2e x \<in> (\<Union>i. A i)" by auto
   3.177 -        hence "\<exists>n. x \<in> e2p ` A n" apply safe apply(rule_tac x=i in exI)
   3.178 -          unfolding image_iff apply(rule_tac x="p2e x" in bexI)
   3.179 -          apply(subst e2p_p2e) using x by auto
   3.180 -        thus "x \<in> (\<Union>n. e2p ` A n)" by auto
   3.181 -      qed
   3.182 -    qed
   3.183 -  qed auto
   3.184 +  proof (rule fprod.measure_space_vimage)
   3.185 +    show "sigma_algebra borel" by default
   3.186 +    show "(p2e :: (nat \<Rightarrow> real) \<Rightarrow> 'a) \<in> measurable fprod.P borel" by (rule measurable_p2e)
   3.187 +    fix A :: "'a set" assume "A \<in> sets borel"
   3.188 +    show "fprod.measure (e2p ` A) = fprod.measure (p2e -` A \<inter> space fprod.P)"
   3.189 +      by (simp add: e2p_image_vimage)
   3.190 +  qed
   3.191  qed
   3.192  
   3.193 -lemma e2p_p2e'[simp]: fixes x::"'a::ordered_euclidean_space"
   3.194 -  assumes "A \<subseteq> extensional {..<DIM('a)}"
   3.195 -  shows "e2p ` (p2e ` A ::'a set) = A"
   3.196 -  apply(rule set_eqI) unfolding image_iff Bex_def apply safe defer
   3.197 -  apply(rule_tac x="p2e x" in exI,safe) using assms by auto
   3.198 -
   3.199 -lemma range_p2e:"range (p2e::_\<Rightarrow>'a::ordered_euclidean_space) = UNIV"
   3.200 -  apply safe defer unfolding image_iff apply(rule_tac x="\<lambda>i. x $$ i" in bexI)
   3.201 -  unfolding p2e_def by auto
   3.202 -
   3.203 -lemma p2e_inv_extensional:"(A::'a::ordered_euclidean_space set)
   3.204 -  = p2e ` (p2e -` A \<inter> extensional {..<DIM('a)})"
   3.205 -  unfolding p2e_def_raw apply safe unfolding image_iff
   3.206 -proof- fix x assume "x\<in>A"
   3.207 -  let ?y = "\<lambda>i. if i<DIM('a) then x$$i else undefined"
   3.208 -  have *:"Chi ?y = x" apply(subst euclidean_eq) by auto
   3.209 -  show "\<exists>xa\<in>Chi -` A \<inter> extensional {..<DIM('a)}. x = Chi xa" apply(rule_tac x="?y" in bexI)
   3.210 -    apply(subst euclidean_eq) unfolding extensional_def using `x\<in>A` by(auto simp: *)
   3.211 -qed
   3.212 +lemma range_e2p:"range (e2p::'a::ordered_euclidean_space \<Rightarrow> _) = extensional {..<DIM('a)}"
   3.213 +  unfolding e2p_def_raw
   3.214 +  apply auto
   3.215 +  by (rule_tac x="\<chi>\<chi> i. x i" in image_eqI) (auto simp: fun_eq_iff extensional_def)
   3.216  
   3.217  lemma borel_fubini_positiv_integral:
   3.218    fixes f :: "'a::ordered_euclidean_space \<Rightarrow> pextreal"
   3.219 @@ -972,22 +900,27 @@
   3.220            borel_product.product_positive_integral {..<DIM('a)} (f \<circ> p2e)"
   3.221  proof- def U \<equiv> "extensional {..<DIM('a)} :: (nat \<Rightarrow> real) set"
   3.222    interpret fprod: finite_product_sigma_finite "\<lambda>x. borel" "\<lambda>x. lmeasure" "{..<DIM('a)}" by default auto
   3.223 -  have *:"sigma_algebra.vimage_algebra borel U (p2e:: _ \<Rightarrow> 'a)
   3.224 -    = sigma (product_algebra (\<lambda>x. borel) {..<DIM('a)})"
   3.225 -    unfolding U_def product_borel_eq_vimage[symmetric] ..
   3.226    show ?thesis
   3.227 -    unfolding borel.positive_integral_vimage[unfolded space_borel, OF bij_inv_p2e_e2p[THEN bij_inv_bij_betw(1)]]
   3.228 -    apply(subst fprod.positive_integral_cong_measure[THEN sym, of "\<lambda>A. lmeasure (p2e ` A)"])
   3.229 -    unfolding U_def[symmetric] *[THEN sym] o_def
   3.230 -  proof- fix A assume A:"A \<in> sets (sigma_algebra.vimage_algebra borel U (p2e ::_ \<Rightarrow> 'a))"
   3.231 -    hence *:"A \<subseteq> extensional {..<DIM('a)}" unfolding U_def by auto
   3.232 -    from A guess B unfolding borel.in_vimage_algebra U_def ..
   3.233 -    then have "(p2e ` A::'a set) \<in> sets borel"
   3.234 -      by (simp add: p2e_inv_extensional[of B, symmetric])
   3.235 -    from lmeasure_measure_eq_borel_prod[OF this] show "lmeasure (p2e ` A::'a set) =
   3.236 -      finite_product_sigma_finite.measure (\<lambda>x. borel) (\<lambda>x. lmeasure) {..<DIM('a)} A"
   3.237 -      unfolding e2p_p2e'[OF *] .
   3.238 -  qed auto
   3.239 +  proof (subst borel.positive_integral_vimage[symmetric, of _ "e2p :: 'a \<Rightarrow> _" "(\<lambda>x. f (p2e x))", unfolded p2e_e2p])
   3.240 +    show "(e2p :: 'a \<Rightarrow> _) \<in> measurable borel fprod.P" by (rule measurable_e2p)
   3.241 +    show "sigma_algebra fprod.P" by default
   3.242 +    from measurable_comp[OF measurable_p2e f]
   3.243 +    show "(\<lambda>x. f (p2e x)) \<in> borel_measurable fprod.P" by (simp add: comp_def)
   3.244 +    let "?L A" = "lmeasure ((e2p::'a \<Rightarrow> (nat \<Rightarrow> real)) -` A \<inter> space borel)"
   3.245 +    show "measure_space.positive_integral fprod.P ?L (\<lambda>x. f (p2e x)) =
   3.246 +      fprod.positive_integral (f \<circ> p2e)"
   3.247 +      unfolding comp_def
   3.248 +    proof (rule fprod.positive_integral_cong_measure)
   3.249 +      fix A :: "(nat \<Rightarrow> real) set" assume "A \<in> sets fprod.P"
   3.250 +      then have A: "(e2p::'a \<Rightarrow> (nat \<Rightarrow> real)) -` A \<inter> space borel \<in> sets borel"
   3.251 +        by (rule measurable_sets[OF measurable_e2p])
   3.252 +      have [simp]: "A \<inter> extensional {..<DIM('a)} = A"
   3.253 +        using `A \<in> sets fprod.P`[THEN fprod.sets_into_space] by auto
   3.254 +      show "?L A = fprod.measure A"
   3.255 +        unfolding lmeasure_measure_eq_borel_prod[OF A]
   3.256 +        by (simp add: range_e2p)
   3.257 +    qed
   3.258 +  qed
   3.259  qed
   3.260  
   3.261  lemma borel_fubini:
     4.1 --- a/src/HOL/Probability/Measure.thy	Fri Jan 21 11:39:26 2011 +0100
     4.2 +++ b/src/HOL/Probability/Measure.thy	Mon Jan 24 22:29:50 2011 +0100
     4.3 @@ -525,6 +525,15 @@
     4.4    qed
     4.5  qed
     4.6  
     4.7 +lemma True
     4.8 +proof
     4.9 +  fix x a b :: nat
    4.10 +  have "\<And>x a b :: int. x dvd a \<Longrightarrow> x dvd (a + b) \<Longrightarrow> x dvd b"
    4.11 +    by (metis dvd_mult_div_cancel zadd_commute zdvd_reduce)
    4.12 +  then have "x dvd a \<Longrightarrow> x dvd (a + b) \<Longrightarrow> x dvd b"
    4.13 +    unfolding zdvd_int[of x] zadd_int[symmetric] .
    4.14 +qed
    4.15 +
    4.16  lemma measure_unique_Int_stable:
    4.17    fixes M E :: "'a algebra" and A :: "nat \<Rightarrow> 'a set"
    4.18    assumes "Int_stable E" "M = sigma E"
    4.19 @@ -608,45 +617,6 @@
    4.20    ultimately show ?thesis by (simp add: isoton_def)
    4.21  qed
    4.22  
    4.23 -section "Isomorphisms between measure spaces"
    4.24 -
    4.25 -lemma (in measure_space) measure_space_isomorphic:
    4.26 -  fixes f :: "'c \<Rightarrow> 'a"
    4.27 -  assumes "bij_betw f S (space M)"
    4.28 -  shows "measure_space (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A))"
    4.29 -    (is "measure_space ?T ?\<mu>")
    4.30 -proof -
    4.31 -  have "f \<in> S \<rightarrow> space M" using assms unfolding bij_betw_def by auto
    4.32 -  then interpret T: sigma_algebra ?T by (rule sigma_algebra_vimage)
    4.33 -  show ?thesis
    4.34 -  proof
    4.35 -    show "\<mu> (f`{}) = 0" by simp
    4.36 -    show "countably_additive ?T (\<lambda>A. \<mu> (f ` A))"
    4.37 -    proof (unfold countably_additive_def, intro allI impI)
    4.38 -      fix A :: "nat \<Rightarrow> 'c set" assume "range A \<subseteq> sets ?T" "disjoint_family A"
    4.39 -      then have "\<forall>i. \<exists>F'. F' \<in> sets M \<and> A i = f -` F' \<inter> S"
    4.40 -        by (auto simp: image_iff image_subset_iff Bex_def vimage_algebra_def)
    4.41 -      from choice[OF this] obtain F where F: "\<And>i. F i \<in> sets M" and A: "\<And>i. A i = f -` F i \<inter> S" by auto
    4.42 -      then have [simp]: "\<And>i. f ` (A i) = F i"
    4.43 -        using sets_into_space assms
    4.44 -        by (force intro!: image_vimage_inter_eq[where T="space M"] simp: bij_betw_def)
    4.45 -      have "disjoint_family F"
    4.46 -      proof (intro disjoint_family_on_bisimulation[OF `disjoint_family A`])
    4.47 -        fix n m assume "A n \<inter> A m = {}"
    4.48 -        then have "f -` (F n \<inter> F m) \<inter> S = {}" unfolding A by auto
    4.49 -        moreover
    4.50 -        have "F n \<in> sets M" "F m \<in> sets M" using F by auto
    4.51 -        then have "f`S = space M" "F n \<inter> F m \<subseteq> space M"
    4.52 -          using sets_into_space assms by (auto simp: bij_betw_def)
    4.53 -        note image_vimage_inter_eq[OF this, symmetric]
    4.54 -        ultimately show "F n \<inter> F m = {}" by simp
    4.55 -      qed
    4.56 -      with F show "(\<Sum>\<^isub>\<infinity> i. \<mu> (f ` A i)) = \<mu> (f ` (\<Union>i. A i))"
    4.57 -        by (auto simp add: image_UN intro!: measure_countably_additive)
    4.58 -    qed
    4.59 -  qed
    4.60 -qed
    4.61 -
    4.62  section "@{text \<mu>}-null sets"
    4.63  
    4.64  abbreviation (in measure_space) "null_sets \<equiv> {N\<in>sets M. \<mu> N = 0}"
    4.65 @@ -879,27 +849,28 @@
    4.66  
    4.67  lemma (in measure_space) measure_space_vimage:
    4.68    fixes M' :: "'b algebra"
    4.69 -  assumes "f \<in> measurable M M'"
    4.70 -  and "sigma_algebra M'"
    4.71 -  shows "measure_space M' (\<lambda>A. \<mu> (f -` A \<inter> space M))" (is "measure_space M' ?T")
    4.72 +  assumes T: "sigma_algebra M'" "T \<in> measurable M M'"
    4.73 +    and \<nu>: "\<And>A. A \<in> sets M' \<Longrightarrow> \<nu> A = \<mu> (T -` A \<inter> space M)"
    4.74 +  shows "measure_space M' \<nu>"
    4.75  proof -
    4.76    interpret M': sigma_algebra M' by fact
    4.77 -
    4.78    show ?thesis
    4.79    proof
    4.80 -    show "?T {} = 0" by simp
    4.81 +    show "\<nu> {} = 0" using \<nu>[of "{}"] by simp
    4.82  
    4.83 -    show "countably_additive M' ?T"
    4.84 -    proof (unfold countably_additive_def, safe)
    4.85 +    show "countably_additive M' \<nu>"
    4.86 +    proof (intro countably_additive_def[THEN iffD2] allI impI)
    4.87        fix A :: "nat \<Rightarrow> 'b set" assume "range A \<subseteq> sets M'" "disjoint_family A"
    4.88 -      hence *: "\<And>i. f -` (A i) \<inter> space M \<in> sets M"
    4.89 -        using `f \<in> measurable M M'` by (auto simp: measurable_def)
    4.90 -      moreover have "(\<Union>i. f -`  A i \<inter> space M) \<in> sets M"
    4.91 +      then have A: "\<And>i. A i \<in> sets M'" "(\<Union>i. A i) \<in> sets M'" by auto
    4.92 +      then have *: "range (\<lambda>i. T -` (A i) \<inter> space M) \<subseteq> sets M"
    4.93 +        using `T \<in> measurable M M'` by (auto simp: measurable_def)
    4.94 +      moreover have "(\<Union>i. T -`  A i \<inter> space M) \<in> sets M"
    4.95          using * by blast
    4.96 -      moreover have **: "disjoint_family (\<lambda>i. f -` A i \<inter> space M)"
    4.97 +      moreover have **: "disjoint_family (\<lambda>i. T -` A i \<inter> space M)"
    4.98          using `disjoint_family A` by (auto simp: disjoint_family_on_def)
    4.99 -      ultimately show "(\<Sum>\<^isub>\<infinity> i. ?T (A i)) = ?T (\<Union>i. A i)"
   4.100 -        using measure_countably_additive[OF _ **] by (auto simp: comp_def vimage_UN)
   4.101 +      ultimately show "(\<Sum>\<^isub>\<infinity> i. \<nu> (A i)) = \<nu> (\<Union>i. A i)"
   4.102 +        using measure_countably_additive[OF _ **] A
   4.103 +        by (auto simp: comp_def vimage_UN \<nu>)
   4.104      qed
   4.105    qed
   4.106  qed
   4.107 @@ -1006,29 +977,6 @@
   4.108    qed force+
   4.109  qed
   4.110  
   4.111 -lemma (in sigma_finite_measure) sigma_finite_measure_isomorphic:
   4.112 -  assumes f: "bij_betw f S (space M)"
   4.113 -  shows "sigma_finite_measure (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A))"
   4.114 -proof -
   4.115 -  interpret M: measure_space "vimage_algebra S f" "\<lambda>A. \<mu> (f ` A)"
   4.116 -    using f by (rule measure_space_isomorphic)
   4.117 -  show ?thesis
   4.118 -  proof default
   4.119 -    from sigma_finite guess A::"nat \<Rightarrow> 'a set" .. note A = this
   4.120 -    show "\<exists>A::nat\<Rightarrow>'b set. range A \<subseteq> sets (vimage_algebra S f) \<and> (\<Union>i. A i) = space (vimage_algebra S f) \<and> (\<forall>i. \<mu> (f ` A i) \<noteq> \<omega>)"
   4.121 -    proof (intro exI conjI)
   4.122 -      show "(\<Union>i::nat. f -` A i \<inter> S) = space (vimage_algebra S f)"
   4.123 -        using A f[THEN bij_betw_imp_funcset] by (auto simp: vimage_UN[symmetric])
   4.124 -      show "range (\<lambda>i. f -` A i \<inter> S) \<subseteq> sets (vimage_algebra S f)"
   4.125 -        using A by (auto simp: vimage_algebra_def)
   4.126 -      have "\<And>i. f ` (f -` A i \<inter> S) = A i"
   4.127 -        using f A sets_into_space
   4.128 -        by (intro image_vimage_inter_eq) (auto simp: bij_betw_def)
   4.129 -      then show "\<forall>i. \<mu> (f ` (f -` A i \<inter> S)) \<noteq> \<omega>"  using A by simp
   4.130 -    qed
   4.131 -  qed
   4.132 -qed
   4.133 -
   4.134  section "Real measure values"
   4.135  
   4.136  lemma (in measure_space) real_measure_Union:
     5.1 --- a/src/HOL/Probability/Probability_Space.thy	Fri Jan 21 11:39:26 2011 +0100
     5.2 +++ b/src/HOL/Probability/Probability_Space.thy	Mon Jan 24 22:29:50 2011 +0100
     5.3 @@ -195,8 +195,8 @@
     5.4    assumes "random_variable S X"
     5.5    shows "prob_space S (distribution X)"
     5.6  proof -
     5.7 -  interpret S: measure_space S "distribution X"
     5.8 -    using measure_space_vimage[of X S] assms unfolding distribution_def by simp
     5.9 +  interpret S: measure_space S "distribution X" unfolding distribution_def
    5.10 +    using assms by (intro measure_space_vimage) auto
    5.11    show ?thesis
    5.12    proof
    5.13      have "X -` space S \<inter> space M = space M"
     6.1 --- a/src/HOL/Probability/Product_Measure.thy	Fri Jan 21 11:39:26 2011 +0100
     6.2 +++ b/src/HOL/Probability/Product_Measure.thy	Mon Jan 24 22:29:50 2011 +0100
     6.3 @@ -523,22 +523,6 @@
     6.4      unfolding * by (rule measurable_comp)
     6.5  qed
     6.6  
     6.7 -lemma (in pair_sigma_algebra) pair_sigma_algebra_swap:
     6.8 -  "sigma (pair_algebra M2 M1) = (vimage_algebra (space M2 \<times> space M1) (\<lambda>(x, y). (y, x)))"
     6.9 -  unfolding vimage_algebra_def
    6.10 -  apply (simp add: sets_sigma)
    6.11 -  apply (subst sigma_sets_vimage[symmetric])
    6.12 -  apply (fastsimp simp: pair_algebra_def)
    6.13 -  using M1.sets_into_space M2.sets_into_space apply (fastsimp simp: pair_algebra_def)
    6.14 -proof -
    6.15 -  have "(\<lambda>X. (\<lambda>(x, y). (y, x)) -` X \<inter> space M2 \<times> space M1) ` sets E
    6.16 -    = sets (pair_algebra M2 M1)" (is "?S = _")
    6.17 -    by (rule pair_algebra_swap)
    6.18 -  then show "sigma (pair_algebra M2 M1) = \<lparr>space = space M2 \<times> space M1,
    6.19 -       sets = sigma_sets (space M2 \<times> space M1) ?S\<rparr>"
    6.20 -    by (simp add: pair_algebra_def sigma_def)
    6.21 -qed
    6.22 -
    6.23  definition (in pair_sigma_finite)
    6.24    "pair_measure A = M1.positive_integral (\<lambda>x.
    6.25      M2.positive_integral (\<lambda>y. indicator A (x, y)))"
    6.26 @@ -644,6 +628,17 @@
    6.27    qed
    6.28  qed
    6.29  
    6.30 +lemma (in pair_sigma_algebra) sets_swap:
    6.31 +  assumes "A \<in> sets P"
    6.32 +  shows "(\<lambda>(x, y). (y, x)) -` A \<inter> space (sigma (pair_algebra M2 M1)) \<in> sets (sigma (pair_algebra M2 M1))"
    6.33 +    (is "_ -` A \<inter> space ?Q \<in> sets ?Q")
    6.34 +proof -
    6.35 +  have *: "(\<lambda>(x, y). (y, x)) -` A \<inter> space ?Q = (\<lambda>(x, y). (y, x)) ` A"
    6.36 +    using `A \<in> sets P` sets_into_space by (auto simp: space_pair_algebra)
    6.37 +  show ?thesis
    6.38 +    unfolding * using assms by (rule sets_pair_sigma_algebra_swap)
    6.39 +qed
    6.40 +
    6.41  lemma (in pair_sigma_finite) pair_measure_alt2:
    6.42    assumes "A \<in> sets P"
    6.43    shows "pair_measure A = M2.positive_integral (\<lambda>y. \<mu>1 ((\<lambda>x. (x, y)) -` A))"
    6.44 @@ -657,13 +652,19 @@
    6.45        using F by auto
    6.46      show "measure_space P pair_measure" by default
    6.47      interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
    6.48 -    have space_P: "space P = space M1 \<times> space M2" unfolding pair_algebra_def by simp
    6.49 -    have "measure_space (Q.vimage_algebra (space P) (\<lambda>(x,y). (y,x))) (\<lambda>A. Q.pair_measure ((\<lambda>(x,y). (y,x)) ` A))"
    6.50 -      by (rule Q.measure_space_isomorphic) (auto simp add: pair_algebra_def bij_betw_def intro!: inj_onI)
    6.51 -    then show "measure_space P ?\<nu>" unfolding space_P Q.pair_sigma_algebra_swap[symmetric]
    6.52 -      by (rule measure_space.measure_space_cong)
    6.53 -         (auto intro!: M2.positive_integral_cong arg_cong[where f=\<mu>1]
    6.54 -               simp: Q.pair_measure_alt inj_vimage_image_eq sets_pair_sigma_algebra_swap)
    6.55 +    have P: "sigma_algebra P" by default
    6.56 +    show "measure_space P ?\<nu>"
    6.57 +      apply (rule Q.measure_space_vimage[OF P])
    6.58 +      apply (rule Q.pair_sigma_algebra_swap_measurable)
    6.59 +    proof -
    6.60 +      fix A assume "A \<in> sets P"
    6.61 +      from sets_swap[OF this]
    6.62 +      show "M2.positive_integral (\<lambda>y. \<mu>1 ((\<lambda>x. (x, y)) -` A)) =
    6.63 +            Q.pair_measure ((\<lambda>(x, y). (y, x)) -` A \<inter> space Q.P)"
    6.64 +        using sets_into_space[OF `A \<in> sets P`]
    6.65 +        by (auto simp add: Q.pair_measure_alt space_pair_algebra
    6.66 +                 intro!: M2.positive_integral_cong arg_cong[where f=\<mu>1])
    6.67 +    qed
    6.68      fix X assume "X \<in> sets E"
    6.69      then obtain A B where X: "X = A \<times> B" and AB: "A \<in> sets M1" "B \<in> sets M2"
    6.70        unfolding pair_algebra_def by auto
    6.71 @@ -787,31 +788,40 @@
    6.72      unfolding F_SUPR by simp
    6.73  qed
    6.74  
    6.75 +lemma (in pair_sigma_finite) positive_integral_product_swap:
    6.76 +  assumes f: "f \<in> borel_measurable P"
    6.77 +  shows "measure_space.positive_integral
    6.78 +    (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) (\<lambda>x. f (case x of (x,y)\<Rightarrow>(y,x))) =
    6.79 +  positive_integral f"
    6.80 +proof -
    6.81 +  interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
    6.82 +  have P: "sigma_algebra P" by default
    6.83 +  show ?thesis
    6.84 +    unfolding Q.positive_integral_vimage[OF P Q.pair_sigma_algebra_swap_measurable f, symmetric]
    6.85 +  proof (rule positive_integral_cong_measure)
    6.86 +    fix A
    6.87 +    assume A: "A \<in> sets P"
    6.88 +    from Q.pair_sigma_algebra_swap_measurable[THEN measurable_sets, OF this] this sets_into_space[OF this]
    6.89 +    show "Q.pair_measure ((\<lambda>(x, y). (y, x)) -` A \<inter> space Q.P) = pair_measure A"
    6.90 +      by (auto intro!: M1.positive_integral_cong arg_cong[where f=\<mu>2]
    6.91 +               simp: pair_measure_alt Q.pair_measure_alt2 space_pair_algebra)
    6.92 +  qed
    6.93 +qed
    6.94 +
    6.95  lemma (in pair_sigma_finite) positive_integral_snd_measurable:
    6.96    assumes f: "f \<in> borel_measurable P"
    6.97    shows "M2.positive_integral (\<lambda>y. M1.positive_integral (\<lambda>x. f (x, y))) =
    6.98        positive_integral f"
    6.99  proof -
   6.100    interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
   6.101 -  have s: "\<And>x y. (case (x, y) of (x, y) \<Rightarrow> f (y, x)) = f (y, x)" by simp
   6.102 -  have t: "(\<lambda>x. f (case x of (x, y) \<Rightarrow> (y, x))) = (\<lambda>(x, y). f (y, x))" by (auto simp: fun_eq_iff)
   6.103 -  have bij: "bij_betw (\<lambda>(x, y). (y, x)) (space M2 \<times> space M1) (space P)"
   6.104 -    by (auto intro!: inj_onI simp: space_pair_algebra bij_betw_def)
   6.105    note pair_sigma_algebra_measurable[OF f]
   6.106    from Q.positive_integral_fst_measurable[OF this]
   6.107    have "M2.positive_integral (\<lambda>y. M1.positive_integral (\<lambda>x. f (x, y))) =
   6.108      Q.positive_integral (\<lambda>(x, y). f (y, x))"
   6.109      by simp
   6.110 -  also have "\<dots> = positive_integral f"
   6.111 -    unfolding positive_integral_vimage[OF bij, of f] t
   6.112 -    unfolding pair_sigma_algebra_swap[symmetric]
   6.113 -  proof (rule Q.positive_integral_cong_measure[symmetric])
   6.114 -    fix A assume "A \<in> sets Q.P"
   6.115 -    from this Q.sets_pair_sigma_algebra_swap[OF this]
   6.116 -    show "pair_measure ((\<lambda>(x, y). (y, x)) ` A) = Q.pair_measure A"
   6.117 -      by (auto intro!: M1.positive_integral_cong arg_cong[where f=\<mu>2]
   6.118 -               simp: pair_measure_alt Q.pair_measure_alt2)
   6.119 -  qed
   6.120 +  also have "Q.positive_integral (\<lambda>(x, y). f (y, x)) = positive_integral f"
   6.121 +    unfolding positive_integral_product_swap[OF f, symmetric]
   6.122 +    by (auto intro!: Q.positive_integral_cong)
   6.123    finally show ?thesis .
   6.124  qed
   6.125  
   6.126 @@ -848,28 +858,6 @@
   6.127    qed
   6.128  qed
   6.129  
   6.130 -lemma (in pair_sigma_finite) positive_integral_product_swap:
   6.131 -  "measure_space.positive_integral
   6.132 -    (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) f =
   6.133 -  positive_integral (\<lambda>(x,y). f (y,x))"
   6.134 -proof -
   6.135 -  interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
   6.136 -  have t: "(\<lambda>y. case case y of (y, x) \<Rightarrow> (x, y) of (x, y) \<Rightarrow> f (y, x)) = f"
   6.137 -    by (auto simp: fun_eq_iff)
   6.138 -  have bij: "bij_betw (\<lambda>(x, y). (y, x)) (space M2 \<times> space M1) (space P)"
   6.139 -    by (auto intro!: inj_onI simp: space_pair_algebra bij_betw_def)
   6.140 -  show ?thesis
   6.141 -    unfolding positive_integral_vimage[OF bij, of "\<lambda>(y,x). f (x,y)"]
   6.142 -    unfolding pair_sigma_algebra_swap[symmetric] t
   6.143 -  proof (rule Q.positive_integral_cong_measure[symmetric])
   6.144 -    fix A assume "A \<in> sets Q.P"
   6.145 -    from this Q.sets_pair_sigma_algebra_swap[OF this]
   6.146 -    show "pair_measure ((\<lambda>(x, y). (y, x)) ` A) = Q.pair_measure A"
   6.147 -      by (auto intro!: M1.positive_integral_cong arg_cong[where f=\<mu>2]
   6.148 -               simp: pair_measure_alt Q.pair_measure_alt2)
   6.149 -  qed
   6.150 -qed
   6.151 -
   6.152  lemma (in pair_sigma_algebra) measurable_product_swap:
   6.153    "f \<in> measurable (sigma (pair_algebra M2 M1)) M \<longleftrightarrow> (\<lambda>(x,y). f (y,x)) \<in> measurable P M"
   6.154  proof -
   6.155 @@ -880,27 +868,42 @@
   6.156  qed
   6.157  
   6.158  lemma (in pair_sigma_finite) integrable_product_swap:
   6.159 -  "measure_space.integrable
   6.160 -    (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) f \<longleftrightarrow>
   6.161 -  integrable (\<lambda>(x,y). f (y,x))"
   6.162 +  assumes "integrable f"
   6.163 +  shows "measure_space.integrable
   6.164 +    (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) (\<lambda>(x,y). f (y,x))"
   6.165  proof -
   6.166    interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
   6.167 -  show ?thesis
   6.168 -    unfolding Q.integrable_def integrable_def
   6.169 -    unfolding positive_integral_product_swap
   6.170 -    unfolding measurable_product_swap
   6.171 -    by (simp add: case_prod_distrib)
   6.172 +  have *: "(\<lambda>(x,y). f (y,x)) = (\<lambda>x. f (case x of (x,y)\<Rightarrow>(y,x)))" by (auto simp: fun_eq_iff)
   6.173 +  show ?thesis unfolding *
   6.174 +    using assms unfolding Q.integrable_def integrable_def
   6.175 +    apply (subst (1 2) positive_integral_product_swap)
   6.176 +    using `integrable f` unfolding integrable_def
   6.177 +    by (auto simp: *[symmetric] Q.measurable_product_swap[symmetric])
   6.178 +qed
   6.179 +
   6.180 +lemma (in pair_sigma_finite) integrable_product_swap_iff:
   6.181 +  "measure_space.integrable
   6.182 +    (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) (\<lambda>(x,y). f (y,x)) \<longleftrightarrow>
   6.183 +  integrable f"
   6.184 +proof -
   6.185 +  interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
   6.186 +  from Q.integrable_product_swap[of "\<lambda>(x,y). f (y,x)"] integrable_product_swap[of f]
   6.187 +  show ?thesis by auto
   6.188  qed
   6.189  
   6.190  lemma (in pair_sigma_finite) integral_product_swap:
   6.191 -  "measure_space.integral
   6.192 -    (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) f =
   6.193 -  integral (\<lambda>(x,y). f (y,x))"
   6.194 +  assumes "integrable f"
   6.195 +  shows "measure_space.integral
   6.196 +    (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) (\<lambda>(x,y). f (y,x)) =
   6.197 +  integral f"
   6.198  proof -
   6.199    interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
   6.200 +  have *: "(\<lambda>(x,y). f (y,x)) = (\<lambda>x. f (case x of (x,y)\<Rightarrow>(y,x)))" by (auto simp: fun_eq_iff)
   6.201    show ?thesis
   6.202 -    unfolding integral_def Q.integral_def positive_integral_product_swap
   6.203 -    by (simp add: case_prod_distrib)
   6.204 +    unfolding integral_def Q.integral_def *
   6.205 +    apply (subst (1 2) positive_integral_product_swap)
   6.206 +    using `integrable f` unfolding integrable_def
   6.207 +    by (auto simp: *[symmetric] Q.measurable_product_swap[symmetric])
   6.208  qed
   6.209  
   6.210  lemma (in pair_sigma_finite) integrable_fst_measurable:
   6.211 @@ -973,10 +976,10 @@
   6.212  proof -
   6.213    interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
   6.214    have Q_int: "Q.integrable (\<lambda>(x, y). f (y, x))"
   6.215 -    using f unfolding integrable_product_swap by simp
   6.216 +    using f unfolding integrable_product_swap_iff .
   6.217    show ?INT
   6.218      using Q.integrable_fst_measurable(2)[OF Q_int]
   6.219 -    unfolding integral_product_swap by simp
   6.220 +    using integral_product_swap[OF f] by simp
   6.221    show ?AE
   6.222      using Q.integrable_fst_measurable(1)[OF Q_int]
   6.223      by simp
   6.224 @@ -1340,18 +1343,6 @@
   6.225              pair_algebra_sets_into_space product_algebra_sets_into_space)
   6.226       auto
   6.227  
   6.228 -lemma (in product_sigma_algebra) product_product_vimage_algebra:
   6.229 -  assumes [simp]: "I \<inter> J = {}"
   6.230 -  shows "sigma_algebra.vimage_algebra
   6.231 -    (sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J))))
   6.232 -    (space (sigma (product_algebra M (I \<union> J)))) (\<lambda>x. ((\<lambda>i\<in>I. x i), (\<lambda>i\<in>J. x i))) =
   6.233 -    sigma (product_algebra M (I \<union> J))"
   6.234 -  unfolding sigma_pair_algebra_sigma_eq using sets_into_space
   6.235 -  by (intro vimage_algebra_sigma[OF bij_inv_restrict_merge]
   6.236 -            pair_algebra_sets_into_space product_algebra_sets_into_space
   6.237 -            measurable_merge_on_generating measurable_restrict_on_generating)
   6.238 -     auto
   6.239 -
   6.240  lemma (in product_sigma_algebra) pair_product_product_vimage_algebra:
   6.241    assumes [simp]: "I \<inter> J = {}"
   6.242    shows "sigma_algebra.vimage_algebra (sigma (product_algebra M (I \<union> J)))
   6.243 @@ -1363,24 +1354,6 @@
   6.244              measurable_merge_on_generating measurable_restrict_on_generating)
   6.245       auto
   6.246  
   6.247 -lemma (in product_sigma_algebra) pair_product_singleton_vimage_algebra:
   6.248 -  assumes [simp]: "i \<notin> I"
   6.249 -  shows "sigma_algebra.vimage_algebra (sigma (pair_algebra (sigma (product_algebra M I)) (M i)))
   6.250 -    (space (sigma (product_algebra M (insert i I)))) (\<lambda>x. (restrict x I, x i)) =
   6.251 -    (sigma (product_algebra M (insert i I)))"
   6.252 -  unfolding sigma_pair_algebra_product_singleton using sets_into_space
   6.253 -  by (intro vimage_algebra_sigma[OF bij_inv_restrict_insert]
   6.254 -            pair_algebra_sets_into_space product_algebra_sets_into_space
   6.255 -            measurable_merge_singleton_on_generating measurable_restrict_singleton_on_generating)
   6.256 -      auto
   6.257 -
   6.258 -lemma (in product_sigma_algebra) singleton_vimage_algebra:
   6.259 -  "sigma_algebra.vimage_algebra (sigma (product_algebra M {i})) (space (M i)) (\<lambda>x. \<lambda>j\<in>{i}. x) = M i"
   6.260 -  using sets_into_space
   6.261 -  by (intro vimage_algebra_sigma[of "M i", unfolded M.sigma_eq, OF bij_inv_singleton[symmetric]]
   6.262 -             product_algebra_sets_into_space measurable_singleton_on_generator measurable_component_on_generator)
   6.263 -     auto
   6.264 -
   6.265  lemma (in product_sigma_algebra) measurable_restrict_iff:
   6.266    assumes IJ[simp]: "I \<inter> J = {}"
   6.267    shows "f \<in> measurable (sigma (pair_algebra
   6.268 @@ -1415,6 +1388,13 @@
   6.269    then show "?f \<in> measurable ?P M'" by (simp add: comp_def)
   6.270  qed
   6.271  
   6.272 +lemma (in product_sigma_algebra) singleton_vimage_algebra:
   6.273 +  "sigma_algebra.vimage_algebra (sigma (product_algebra M {i})) (space (M i)) (\<lambda>x. \<lambda>j\<in>{i}. x) = M i"
   6.274 +  using sets_into_space
   6.275 +  by (intro vimage_algebra_sigma[of "M i", unfolded M.sigma_eq, OF bij_inv_singleton[symmetric]]
   6.276 +            product_algebra_sets_into_space measurable_singleton_on_generator measurable_component_on_generator)
   6.277 +     auto
   6.278 +
   6.279  lemma (in product_sigma_algebra) measurable_component_singleton:
   6.280    "(\<lambda>x. f (x i)) \<in> measurable (sigma (product_algebra M {i})) M' \<longleftrightarrow>
   6.281      f \<in> measurable (M i) M'"
   6.282 @@ -1464,6 +1444,55 @@
   6.283    using sets_into_space unfolding measurable_component_singleton[symmetric]
   6.284    by (auto intro!: measurable_cong arg_cong[where f=f] simp: fun_eq_iff extensional_def)
   6.285  
   6.286 +
   6.287 +lemma (in pair_sigma_algebra) measurable_pair_split:
   6.288 +  assumes "sigma_algebra M1'" "sigma_algebra M2'"
   6.289 +  assumes f: "f \<in> measurable M1 M1'" and g: "g \<in> measurable M2 M2'"
   6.290 +  shows "(\<lambda>(x, y). (f x, g y)) \<in> measurable P (sigma (pair_algebra M1' M2'))"
   6.291 +proof (rule measurable_sigma)
   6.292 +  interpret M1': sigma_algebra M1' by fact
   6.293 +  interpret M2': sigma_algebra M2' by fact
   6.294 +  interpret Q: pair_sigma_algebra M1' M2' by default
   6.295 +  show "sets Q.E \<subseteq> Pow (space Q.E)"
   6.296 +    using M1'.sets_into_space M2'.sets_into_space by (auto simp: pair_algebra_def)
   6.297 +  show "(\<lambda>(x, y). (f x, g y)) \<in> space P \<rightarrow> space Q.E"
   6.298 +    using f g unfolding measurable_def pair_algebra_def by auto
   6.299 +  fix A assume "A \<in> sets Q.E"
   6.300 +  then obtain X Y where A: "A = X \<times> Y" "X \<in> sets M1'" "Y \<in> sets M2'"
   6.301 +    unfolding pair_algebra_def by auto
   6.302 +  then have *: "(\<lambda>(x, y). (f x, g y)) -` A \<inter> space P =
   6.303 +      (f -` X \<inter> space M1) \<times> (g -` Y \<inter> space M2)"
   6.304 +    by (auto simp: pair_algebra_def)
   6.305 +  then show "(\<lambda>(x, y). (f x, g y)) -` A \<inter> space P \<in> sets P"
   6.306 +    using f g A unfolding measurable_def *
   6.307 +    by (auto intro!: pair_algebraI in_sigma)
   6.308 +qed
   6.309 +
   6.310 +lemma (in product_sigma_algebra) measurable_add_dim:
   6.311 +  assumes "i \<notin> I" "finite I"
   6.312 +  shows "(\<lambda>(f, y). f(i := y)) \<in> measurable (sigma (pair_algebra (sigma (product_algebra M I)) (M i)))
   6.313 +                         (sigma (product_algebra M (insert i I)))"
   6.314 +proof (subst measurable_cong)
   6.315 +  interpret I: finite_product_sigma_algebra M I by default fact
   6.316 +  interpret i: finite_product_sigma_algebra M "{i}" by default auto
   6.317 +  interpret Ii: pair_sigma_algebra I.P "M i" by default
   6.318 +  interpret Ii': pair_sigma_algebra I.P i.P by default
   6.319 +  have disj: "I \<inter> {i} = {}" using `i \<notin> I` by auto
   6.320 +  have "(\<lambda>(x, y). (id x, \<lambda>_\<in>{i}. y)) \<in> measurable Ii.P Ii'.P"
   6.321 +  proof (intro Ii.measurable_pair_split I.measurable_ident)
   6.322 +    show "(\<lambda>y. \<lambda>_\<in>{i}. y) \<in> measurable (M i) i.P"
   6.323 +      apply (rule measurable_singleton[THEN iffD1])
   6.324 +      using i.measurable_ident unfolding id_def .
   6.325 +  qed default
   6.326 +  from measurable_comp[OF this measurable_merge[OF disj]]
   6.327 +  show "(\<lambda>(x, y). merge I x {i} y) \<circ> (\<lambda>(x, y). (id x, \<lambda>_\<in>{i}. y))
   6.328 +    \<in> measurable (sigma (pair_algebra I.P (M i))) (sigma (product_algebra M (insert i I)))"
   6.329 +    (is "?f \<in> _") by simp
   6.330 +  fix x assume "x \<in> space Ii.P"
   6.331 +  with assms show "(\<lambda>(f, y). f(i := y)) x = ?f x"
   6.332 +    by (cases x) (simp add: merge_def fun_eq_iff pair_algebra_def extensional_def)
   6.333 +qed
   6.334 +
   6.335  locale product_sigma_finite =
   6.336    fixes M :: "'i \<Rightarrow> 'a algebra" and \<mu> :: "'i \<Rightarrow> 'a set \<Rightarrow> pextreal"
   6.337    assumes sigma_finite_measures: "\<And>i. sigma_finite_measure (M i) (\<mu> i)"
   6.338 @@ -1534,29 +1563,24 @@
   6.339    interpret I: sigma_finite_measure P \<nu> by fact
   6.340    interpret P: pair_sigma_finite P \<nu> "M i" "\<mu> i" ..
   6.341  
   6.342 -  let ?h = "\<lambda>x. (restrict x I, x i)"
   6.343 -  let ?\<nu> = "\<lambda>A. P.pair_measure (?h ` A)"
   6.344 +  let ?h = "(\<lambda>(f, y). f(i := y))"
   6.345 +  let ?\<nu> = "\<lambda>A. P.pair_measure (?h -` A \<inter> space P.P)"
   6.346 +  have I': "sigma_algebra I'.P" by default
   6.347    interpret I': measure_space "sigma (product_algebra M (insert i I))" ?\<nu>
   6.348 -    apply (subst pair_product_singleton_vimage_algebra[OF `i \<notin> I`, symmetric])
   6.349 -    apply (intro P.measure_space_isomorphic bij_inv_bij_betw)
   6.350 -    unfolding sigma_pair_algebra_product_singleton
   6.351 -    by (rule bij_inv_restrict_insert[OF `i \<notin> I`])
   6.352 +    apply (rule P.measure_space_vimage[OF I'])
   6.353 +    apply (rule measurable_add_dim[OF `i \<notin> I` `finite I`])
   6.354 +    by simp
   6.355    show ?case
   6.356    proof (intro exI[of _ ?\<nu>] conjI ballI)
   6.357      { fix A assume A: "A \<in> (\<Pi> i\<in>insert i I. sets (M i))"
   6.358 -      moreover then have "A \<in> (\<Pi> i\<in>I. sets (M i))" by auto
   6.359 -      moreover have "(\<lambda>x. (restrict x I, x i)) ` Pi\<^isub>E (insert i I) A = Pi\<^isub>E I A \<times> A i"
   6.360 -        using `i \<notin> I`
   6.361 -        apply auto
   6.362 -        apply (rule_tac x="a(i:=b)" in image_eqI)
   6.363 -        apply (auto simp: extensional_def fun_eq_iff)
   6.364 -        done
   6.365 -      ultimately show "?\<nu> (Pi\<^isub>E (insert i I) A) = (\<Prod>i\<in>insert i I. \<mu> i (A i))"
   6.366 -        apply simp
   6.367 +      then have *: "?h -` Pi\<^isub>E (insert i I) A \<inter> space P.P = Pi\<^isub>E I A \<times> A i"
   6.368 +        using `i \<notin> I` M.sets_into_space by (auto simp: pair_algebra_def) blast
   6.369 +      show "?\<nu> (Pi\<^isub>E (insert i I) A) = (\<Prod>i\<in>insert i I. \<mu> i (A i))"
   6.370 +        unfolding * using A
   6.371          apply (subst P.pair_measure_times)
   6.372 -        apply fastsimp
   6.373 -        apply fastsimp
   6.374 -        using `i \<notin> I` `finite I` prod[of A] by (auto simp: ac_simps) }
   6.375 +        using A apply fastsimp
   6.376 +        using A apply fastsimp
   6.377 +        using `i \<notin> I` `finite I` prod[of A] A by (auto simp: ac_simps) }
   6.378      note product = this
   6.379      show "sigma_finite_measure I'.P ?\<nu>"
   6.380      proof
   6.381 @@ -1656,7 +1680,7 @@
   6.382    shows "pair_sigma_finite.pair_measure
   6.383       (sigma (product_algebra M I)) (product_measure I)
   6.384       (sigma (product_algebra M J)) (product_measure J)
   6.385 -     ((\<lambda>x. ((\<lambda>i\<in>I. x i), (\<lambda>i\<in>J. x i))) ` A) =
   6.386 +     ((\<lambda>(x,y). merge I x J y) -` A \<inter> space (sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J))))) =
   6.387     product_measure (I \<union> J) A"
   6.388  proof -
   6.389    interpret I: finite_product_sigma_finite M \<mu> I by default fact
   6.390 @@ -1664,51 +1688,52 @@
   6.391    have "finite (I \<union> J)" using fin by auto
   6.392    interpret IJ: finite_product_sigma_finite M \<mu> "I \<union> J" by default fact
   6.393    interpret P: pair_sigma_finite I.P I.measure J.P J.measure by default
   6.394 -  let ?f = "\<lambda>x. ((\<lambda>i\<in>I. x i), (\<lambda>i\<in>J. x i))"
   6.395 -    from IJ.sigma_finite_pairs obtain F where
   6.396 -      F: "\<And>i. i\<in> I \<union> J \<Longrightarrow> range (F i) \<subseteq> sets (M i)"
   6.397 -         "(\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k) \<up> space IJ.G"
   6.398 -         "\<And>k. \<forall>i\<in>I\<union>J. \<mu> i (F i k) \<noteq> \<omega>"
   6.399 -      by auto
   6.400 -    let ?F = "\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k"
   6.401 -  have split_f_image[simp]: "\<And>F. ?f ` (Pi\<^isub>E (I \<union> J) F) = (Pi\<^isub>E I F) \<times> (Pi\<^isub>E J F)"
   6.402 -    apply auto apply (rule_tac x="merge I a J b" in image_eqI)
   6.403 -    by (auto dest: extensional_restrict)
   6.404 -    show "P.pair_measure (?f ` A) = IJ.measure A"
   6.405 +  let ?g = "\<lambda>(x,y). merge I x J y"
   6.406 +  let "?X S" = "?g -` S \<inter> space P.P"
   6.407 +  from IJ.sigma_finite_pairs obtain F where
   6.408 +    F: "\<And>i. i\<in> I \<union> J \<Longrightarrow> range (F i) \<subseteq> sets (M i)"
   6.409 +       "(\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k) \<up> space IJ.G"
   6.410 +       "\<And>k. \<forall>i\<in>I\<union>J. \<mu> i (F i k) \<noteq> \<omega>"
   6.411 +    by auto
   6.412 +  let ?F = "\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k"
   6.413 +  show "P.pair_measure (?X A) = IJ.measure A"
   6.414    proof (rule measure_unique_Int_stable[OF _ _ _ _ _ _ _ _ A])
   6.415 -      show "Int_stable IJ.G" by (simp add: PiE_Int Int_stable_def product_algebra_def) auto
   6.416 -      show "range ?F \<subseteq> sets IJ.G" using F by (simp add: image_subset_iff product_algebra_def)
   6.417 -      show "?F \<up> space IJ.G " using F(2) by simp
   6.418 -      show "measure_space IJ.P (\<lambda>A. P.pair_measure (?f ` A))"
   6.419 -      apply (subst product_product_vimage_algebra[OF IJ, symmetric])
   6.420 -      apply (intro P.measure_space_isomorphic bij_inv_bij_betw)
   6.421 -      unfolding sigma_pair_algebra_sigma_eq
   6.422 -      by (rule bij_inv_restrict_merge[OF `I \<inter> J = {}`])
   6.423 -      show "measure_space IJ.P IJ.measure" by fact
   6.424 -    next
   6.425 -      fix A assume "A \<in> sets IJ.G"
   6.426 -      then obtain F where A[simp]: "A = Pi\<^isub>E (I \<union> J) F" "F \<in> (\<Pi> i\<in>I \<union> J. sets (M i))"
   6.427 -        by (auto simp: product_algebra_def)
   6.428 -      then have F: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> sets (M i)" "\<And>i. i \<in> J \<Longrightarrow> F i \<in> sets (M i)"
   6.429 -        by auto
   6.430 -      have "P.pair_measure (?f ` A) = (\<Prod>i\<in>I. \<mu> i (F i)) * (\<Prod>i\<in>J. \<mu> i (F i))"
   6.431 -        using `finite J` `finite I` F
   6.432 -        by (simp add: P.pair_measure_times I.measure_times J.measure_times)
   6.433 -      also have "\<dots> = (\<Prod>i\<in>I \<union> J. \<mu> i (F i))"
   6.434 -        using `finite J` `finite I` `I \<inter> J = {}`  by (simp add: setprod_Un_one)
   6.435 -      also have "\<dots> = IJ.measure A"
   6.436 -        using `finite J` `finite I` F unfolding A
   6.437 -        by (intro IJ.measure_times[symmetric]) auto
   6.438 -      finally show "P.pair_measure (?f ` A) = IJ.measure A" .
   6.439 -    next
   6.440 -      fix k
   6.441 -      have "\<And>i. i \<in> I \<union> J \<Longrightarrow> F i k \<in> sets (M i)" using F by auto
   6.442 -      then have "P.pair_measure (?f ` ?F k) = (\<Prod>i\<in>I. \<mu> i (F i k)) * (\<Prod>i\<in>J. \<mu> i (F i k))"
   6.443 -        by (simp add: P.pair_measure_times I.measure_times J.measure_times)
   6.444 -      then show "P.pair_measure (?f ` ?F k) \<noteq> \<omega>"
   6.445 -        using `finite I` F by (simp add: setprod_\<omega>)
   6.446 -    qed simp
   6.447 -  qed
   6.448 +    show "Int_stable IJ.G" by (simp add: PiE_Int Int_stable_def product_algebra_def) auto
   6.449 +    show "range ?F \<subseteq> sets IJ.G" using F by (simp add: image_subset_iff product_algebra_def)
   6.450 +    show "?F \<up> space IJ.G " using F(2) by simp
   6.451 +    have "sigma_algebra IJ.P" by default
   6.452 +    then show "measure_space IJ.P (\<lambda>A. P.pair_measure (?X A))"
   6.453 +      apply (rule P.measure_space_vimage)
   6.454 +      apply (rule measurable_merge[OF `I \<inter> J = {}`])
   6.455 +      by simp
   6.456 +    show "measure_space IJ.P IJ.measure" by fact
   6.457 +  next
   6.458 +    fix A assume "A \<in> sets IJ.G"
   6.459 +    then obtain F where A[simp]: "A = Pi\<^isub>E (I \<union> J) F"
   6.460 +      and F: "\<And>i. i \<in> I \<union> J \<Longrightarrow> F i \<in> sets (M i)"
   6.461 +      by (auto simp: product_algebra_def)
   6.462 +    then have "?X A = (Pi\<^isub>E I F \<times> Pi\<^isub>E J F)"
   6.463 +      using sets_into_space by (auto simp: space_pair_algebra) blast+
   6.464 +    then have "P.pair_measure (?X A) = (\<Prod>i\<in>I. \<mu> i (F i)) * (\<Prod>i\<in>J. \<mu> i (F i))"
   6.465 +      using `finite J` `finite I` F
   6.466 +      by (simp add: P.pair_measure_times I.measure_times J.measure_times)
   6.467 +    also have "\<dots> = (\<Prod>i\<in>I \<union> J. \<mu> i (F i))"
   6.468 +      using `finite J` `finite I` `I \<inter> J = {}`  by (simp add: setprod_Un_one)
   6.469 +    also have "\<dots> = IJ.measure A"
   6.470 +      using `finite J` `finite I` F unfolding A
   6.471 +      by (intro IJ.measure_times[symmetric]) auto
   6.472 +    finally show "P.pair_measure (?X A) = IJ.measure A" .
   6.473 +  next
   6.474 +    fix k
   6.475 +    have k: "\<And>i. i \<in> I \<union> J \<Longrightarrow> F i k \<in> sets (M i)" using F by auto
   6.476 +    then have "?X (?F k) = (\<Pi>\<^isub>E i\<in>I. F i k) \<times> (\<Pi>\<^isub>E i\<in>J. F i k)"
   6.477 +      using sets_into_space by (auto simp: space_pair_algebra) blast+
   6.478 +    with k have "P.pair_measure (?X (?F k)) = (\<Prod>i\<in>I. \<mu> i (F i k)) * (\<Prod>i\<in>J. \<mu> i (F i k))"
   6.479 +     by (simp add: P.pair_measure_times I.measure_times J.measure_times)
   6.480 +    then show "P.pair_measure (?X (?F k)) \<noteq> \<omega>"
   6.481 +      using `finite I` F by (simp add: setprod_\<omega>)
   6.482 +  qed simp
   6.483 +qed
   6.484  
   6.485  lemma (in product_sigma_finite) product_positive_integral_fold:
   6.486    assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
   6.487 @@ -1721,23 +1746,18 @@
   6.488    have "finite (I \<union> J)" using fin by auto
   6.489    interpret IJ: finite_product_sigma_finite M \<mu> "I \<union> J" by default fact
   6.490    interpret P: pair_sigma_finite I.P I.measure J.P J.measure by default
   6.491 -  let ?f = "\<lambda>x. ((\<lambda>i\<in>I. x i), (\<lambda>i\<in>J. x i))"
   6.492    have P_borel: "(\<lambda>x. f (case x of (x, y) \<Rightarrow> merge I x J y)) \<in> borel_measurable P.P"
   6.493      unfolding case_prod_distrib measurable_merge_iff[OF IJ, symmetric] using f .
   6.494 -  have bij: "bij_betw ?f (space IJ.P) (space P.P)"
   6.495 -    unfolding sigma_pair_algebra_sigma_eq
   6.496 -    by (intro bij_inv_bij_betw) (rule bij_inv_restrict_merge[OF IJ])
   6.497 -  have "IJ.positive_integral f =  IJ.positive_integral (\<lambda>x. f (restrict x (I \<union> J)))"
   6.498 -    by (auto intro!: IJ.positive_integral_cong arg_cong[where f=f] dest!: extensional_restrict)
   6.499 -  also have "\<dots> = I.positive_integral (\<lambda>x. J.positive_integral (\<lambda>y. f (merge I x J y)))"
   6.500 +  show ?thesis
   6.501      unfolding P.positive_integral_fst_measurable[OF P_borel, simplified]
   6.502 -    unfolding P.positive_integral_vimage[OF bij]
   6.503 -    unfolding product_product_vimage_algebra[OF IJ]
   6.504 -    apply simp
   6.505 -    apply (rule IJ.positive_integral_cong_measure[symmetric])
   6.506 -    apply (rule measure_fold)
   6.507 -    using assms by auto
   6.508 -  finally show ?thesis .
   6.509 +    apply (subst IJ.positive_integral_cong_measure[symmetric])
   6.510 +    apply (rule measure_fold[OF IJ fin])
   6.511 +    apply assumption
   6.512 +  proof (rule P.positive_integral_vimage)
   6.513 +    show "sigma_algebra IJ.P" by default
   6.514 +    show "(\<lambda>(x, y). merge I x J y) \<in> measurable P.P IJ.P" by (rule measurable_merge[OF IJ])
   6.515 +    show "f \<in> borel_measurable IJ.P" using f .
   6.516 +  qed
   6.517  qed
   6.518  
   6.519  lemma (in product_sigma_finite) product_positive_integral_singleton:
   6.520 @@ -1745,31 +1765,18 @@
   6.521    shows "product_positive_integral {i} (\<lambda>x. f (x i)) = M.positive_integral i f"
   6.522  proof -
   6.523    interpret I: finite_product_sigma_finite M \<mu> "{i}" by default simp
   6.524 -  have bij: "bij_betw (\<lambda>x. \<lambda>j\<in>{i}. x) (space (M i)) (space I.P)"
   6.525 -    by (auto intro!: bij_betwI ext simp: extensional_def)
   6.526 -  have *: "(\<lambda>x. (\<lambda>x. \<lambda>j\<in>{i}. x) -` Pi\<^isub>E {i} x \<inter> space (M i)) ` (\<Pi> i\<in>{i}. sets (M i)) = sets (M i)"
   6.527 -  proof (subst image_cong, rule refl)
   6.528 -    fix x assume "x \<in> (\<Pi> i\<in>{i}. sets (M i))"
   6.529 -    then show "(\<lambda>x. \<lambda>j\<in>{i}. x) -` Pi\<^isub>E {i} x \<inter> space (M i) = x i"
   6.530 -      using sets_into_space by auto
   6.531 -  qed auto
   6.532 -  have vimage: "I.vimage_algebra (space (M i)) (\<lambda>x. \<lambda>j\<in>{i}. x) = M i"
   6.533 -    unfolding I.vimage_algebra_def
   6.534 -    unfolding product_sigma_algebra_def sets_sigma
   6.535 -    apply (subst sigma_sets_vimage[symmetric])
   6.536 -    apply (simp_all add: image_image sigma_sets_eq product_algebra_def * del: vimage_Int)
   6.537 -    using sets_into_space by blast
   6.538 +  have T: "(\<lambda>x. x i) \<in> measurable (sigma (product_algebra M {i})) (M i)"
   6.539 +    using measurable_component_singleton[of "\<lambda>x. x" i]
   6.540 +          measurable_ident[unfolded id_def] by auto
   6.541    show "I.positive_integral (\<lambda>x. f (x i)) = M.positive_integral i f"
   6.542 -    unfolding I.positive_integral_vimage[OF bij]
   6.543 -    unfolding vimage
   6.544 -    apply (subst positive_integral_cong_measure)
   6.545 -  proof -
   6.546 -    fix A assume A: "A \<in> sets (M i)"
   6.547 -    have "(\<lambda>x. \<lambda>j\<in>{i}. x) ` A = (\<Pi>\<^isub>E i\<in>{i}. A)"
   6.548 -      by (auto intro!: image_eqI ext[where 'b='a] simp: extensional_def)
   6.549 -    with A show "product_measure {i} ((\<lambda>x. \<lambda>j\<in>{i}. x) ` A) = \<mu> i A"
   6.550 -      using I.measure_times[of "\<lambda>i. A"] by simp
   6.551 -  qed simp
   6.552 +    unfolding I.positive_integral_vimage[OF sigma_algebras T f, symmetric]
   6.553 +  proof (rule positive_integral_cong_measure)
   6.554 +    fix A let ?P = "(\<lambda>x. x i) -` A \<inter> space (sigma (product_algebra M {i}))"
   6.555 +    assume A: "A \<in> sets (M i)"
   6.556 +    then have *: "?P = {i} \<rightarrow>\<^isub>E A" using sets_into_space by auto
   6.557 +    show "product_measure {i} ?P = \<mu> i A" unfolding *
   6.558 +      using A I.measure_times[of "\<lambda>_. A"] by auto
   6.559 +  qed
   6.560  qed
   6.561  
   6.562  lemma (in product_sigma_finite) product_positive_integral_insert:
     7.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Fri Jan 21 11:39:26 2011 +0100
     7.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Mon Jan 24 22:29:50 2011 +0100
     7.3 @@ -1104,38 +1104,6 @@
     7.4      unfolding eq[OF A, symmetric] RN_deriv(2)[OF \<nu> A, symmetric] ..
     7.5  qed
     7.6  
     7.7 -lemma (in sigma_finite_measure) RN_deriv_vimage:
     7.8 -  fixes f :: "'b \<Rightarrow> 'a"
     7.9 -  assumes f: "bij_inv S (space M) f g"
    7.10 -  assumes \<nu>: "measure_space M \<nu>" "absolutely_continuous \<nu>"
    7.11 -  shows "AE x.
    7.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"
    7.13 -proof (rule RN_deriv_unique[OF \<nu>])
    7.14 -  interpret sf: sigma_finite_measure "vimage_algebra S f" "\<lambda>A. \<mu> (f ` A)"
    7.15 -    using f by (rule sigma_finite_measure_isomorphic[OF bij_inv_bij_betw(1)])
    7.16 -  interpret \<nu>: measure_space M \<nu> using \<nu>(1) .
    7.17 -  have \<nu>': "measure_space (vimage_algebra S f) (\<lambda>A. \<nu> (f ` A))"
    7.18 -    using f by (rule \<nu>.measure_space_isomorphic[OF bij_inv_bij_betw(1)])
    7.19 -  { fix A assume "A \<in> sets M" then have "f ` (f -` A \<inter> S) = A"
    7.20 -      using sets_into_space f[THEN bij_inv_bij_betw(1), unfolded bij_betw_def]
    7.21 -      by (intro image_vimage_inter_eq[where T="space M"]) auto }
    7.22 -  note A_f = this
    7.23 -  then have ac: "sf.absolutely_continuous (\<lambda>A. \<nu> (f ` A))"
    7.24 -    using \<nu>(2) by (auto simp: sf.absolutely_continuous_def absolutely_continuous_def)
    7.25 -  show "(\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x)) \<in> borel_measurable M"
    7.26 -    using sf.RN_deriv(1)[OF \<nu>' ac]
    7.27 -    unfolding measurable_vimage_iff_inv[OF f] comp_def .
    7.28 -  fix A assume "A \<in> sets M"
    7.29 -  then have *: "\<And>x. x \<in> space M \<Longrightarrow> indicator (f -` A \<inter> S) (g x) = (indicator A x :: pextreal)"
    7.30 -    using f by (auto simp: bij_inv_def indicator_def)
    7.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)"
    7.32 -    using `A \<in> sets M` by (force intro!: sf.RN_deriv(2)[OF \<nu>' ac])
    7.33 -  also have "\<dots> = (\<integral>\<^isup>+x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)"
    7.34 -    unfolding positive_integral_vimage_inv[OF f]
    7.35 -    by (simp add: * cong: positive_integral_cong)
    7.36 -  finally show "\<nu> A = (\<integral>\<^isup>+x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)"
    7.37 -    unfolding A_f[OF `A \<in> sets M`] .
    7.38 -qed
    7.39  
    7.40  lemma (in sigma_finite_measure) RN_deriv_finite:
    7.41    assumes sfm: "sigma_finite_measure M \<nu>" and ac: "absolutely_continuous \<nu>"