author hoelzl Mon Jan 24 22:29:50 2011 +0100 (2011-01-24) changeset 41661 baf1964bc468 parent 41660 7795aaab6038 child 41662 621fa31e1dbd
use pre-image measure, instead of image
```     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.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.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.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>"
```