1.1 --- a/src/HOL/Probability/Information.thy Fri Jan 21 10:43:09 2011 +0100
1.2 +++ b/src/HOL/Probability/Information.thy Tue Jan 25 09:45:45 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 10:43:09 2011 +0100
2.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy Tue Jan 25 09:45:45 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 10:43:09 2011 +0100
3.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy Tue Jan 25 09:45:45 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 10:43:09 2011 +0100
4.2 +++ b/src/HOL/Probability/Measure.thy Tue Jan 25 09:45:45 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 @@ -803,23 +773,17 @@
4.66 lemma (in measure_space) AE_conjI:
4.67 assumes AE_P: "AE x. P x" and AE_Q: "AE x. Q x"
4.68 shows "AE x. P x \<and> Q x"
4.69 -proof -
4.70 - from AE_P obtain A where P: "{x\<in>space M. \<not> P x} \<subseteq> A"
4.71 - and A: "A \<in> sets M" "\<mu> A = 0"
4.72 - by (auto elim!: AE_E)
4.73 + apply (rule AE_mp[OF AE_P])
4.74 + apply (rule AE_mp[OF AE_Q])
4.75 + by simp
4.76
4.77 - from AE_Q obtain B where Q: "{x\<in>space M. \<not> Q x} \<subseteq> B"
4.78 - and B: "B \<in> sets M" "\<mu> B = 0"
4.79 - by (auto elim!: AE_E)
4.80 -
4.81 - show ?thesis
4.82 - proof (intro AE_I)
4.83 - show "A \<union> B \<in> sets M" "\<mu> (A \<union> B) = 0" using A B
4.84 - using measure_subadditive[of A B] by auto
4.85 - show "{x\<in>space M. \<not> (P x \<and> Q x)} \<subseteq> A \<union> B"
4.86 - using P Q by auto
4.87 - qed
4.88 -qed
4.89 +lemma (in measure_space) AE_conj_iff[simp]:
4.90 + shows "(AE x. P x \<and> Q x) \<longleftrightarrow> (AE x. P x) \<and> (AE x. Q x)"
4.91 +proof (intro conjI iffI AE_conjI)
4.92 + assume *: "AE x. P x \<and> Q x"
4.93 + from * show "AE x. P x" by (rule AE_mp) auto
4.94 + from * show "AE x. Q x" by (rule AE_mp) auto
4.95 +qed auto
4.96
4.97 lemma (in measure_space) AE_E2:
4.98 assumes "AE x. P x" "{x\<in>space M. P x} \<in> sets M"
4.99 @@ -845,14 +809,6 @@
4.100 by (rule AE_mp[OF AE_space]) auto
4.101 qed
4.102
4.103 -lemma (in measure_space) AE_conj_iff[simp]:
4.104 - shows "(AE x. P x \<and> Q x) \<longleftrightarrow> (AE x. P x) \<and> (AE x. Q x)"
4.105 -proof (intro conjI iffI AE_conjI)
4.106 - assume *: "AE x. P x \<and> Q x"
4.107 - from * show "AE x. P x" by (rule AE_mp) auto
4.108 - from * show "AE x. Q x" by (rule AE_mp) auto
4.109 -qed auto
4.110 -
4.111 lemma (in measure_space) all_AE_countable:
4.112 "(\<forall>i::'i::countable. AE x. P i x) \<longleftrightarrow> (AE x. \<forall>i. P i x)"
4.113 proof
4.114 @@ -893,27 +849,28 @@
4.115
4.116 lemma (in measure_space) measure_space_vimage:
4.117 fixes M' :: "'b algebra"
4.118 - assumes "f \<in> measurable M M'"
4.119 - and "sigma_algebra M'"
4.120 - shows "measure_space M' (\<lambda>A. \<mu> (f -` A \<inter> space M))" (is "measure_space M' ?T")
4.121 + assumes T: "sigma_algebra M'" "T \<in> measurable M M'"
4.122 + and \<nu>: "\<And>A. A \<in> sets M' \<Longrightarrow> \<nu> A = \<mu> (T -` A \<inter> space M)"
4.123 + shows "measure_space M' \<nu>"
4.124 proof -
4.125 interpret M': sigma_algebra M' by fact
4.126 -
4.127 show ?thesis
4.128 proof
4.129 - show "?T {} = 0" by simp
4.130 + show "\<nu> {} = 0" using \<nu>[of "{}"] by simp
4.131
4.132 - show "countably_additive M' ?T"
4.133 - proof (unfold countably_additive_def, safe)
4.134 + show "countably_additive M' \<nu>"
4.135 + proof (intro countably_additive_def[THEN iffD2] allI impI)
4.136 fix A :: "nat \<Rightarrow> 'b set" assume "range A \<subseteq> sets M'" "disjoint_family A"
4.137 - hence *: "\<And>i. f -` (A i) \<inter> space M \<in> sets M"
4.138 - using `f \<in> measurable M M'` by (auto simp: measurable_def)
4.139 - moreover have "(\<Union>i. f -` A i \<inter> space M) \<in> sets M"
4.140 + then have A: "\<And>i. A i \<in> sets M'" "(\<Union>i. A i) \<in> sets M'" by auto
4.141 + then have *: "range (\<lambda>i. T -` (A i) \<inter> space M) \<subseteq> sets M"
4.142 + using `T \<in> measurable M M'` by (auto simp: measurable_def)
4.143 + moreover have "(\<Union>i. T -` A i \<inter> space M) \<in> sets M"
4.144 using * by blast
4.145 - moreover have **: "disjoint_family (\<lambda>i. f -` A i \<inter> space M)"
4.146 + moreover have **: "disjoint_family (\<lambda>i. T -` A i \<inter> space M)"
4.147 using `disjoint_family A` by (auto simp: disjoint_family_on_def)
4.148 - ultimately show "(\<Sum>\<^isub>\<infinity> i. ?T (A i)) = ?T (\<Union>i. A i)"
4.149 - using measure_countably_additive[OF _ **] by (auto simp: comp_def vimage_UN)
4.150 + ultimately show "(\<Sum>\<^isub>\<infinity> i. \<nu> (A i)) = \<nu> (\<Union>i. A i)"
4.151 + using measure_countably_additive[OF _ **] A
4.152 + by (auto simp: comp_def vimage_UN \<nu>)
4.153 qed
4.154 qed
4.155 qed
4.156 @@ -1020,29 +977,6 @@
4.157 qed force+
4.158 qed
4.159
4.160 -lemma (in sigma_finite_measure) sigma_finite_measure_isomorphic:
4.161 - assumes f: "bij_betw f S (space M)"
4.162 - shows "sigma_finite_measure (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A))"
4.163 -proof -
4.164 - interpret M: measure_space "vimage_algebra S f" "\<lambda>A. \<mu> (f ` A)"
4.165 - using f by (rule measure_space_isomorphic)
4.166 - show ?thesis
4.167 - proof default
4.168 - from sigma_finite guess A::"nat \<Rightarrow> 'a set" .. note A = this
4.169 - 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.170 - proof (intro exI conjI)
4.171 - show "(\<Union>i::nat. f -` A i \<inter> S) = space (vimage_algebra S f)"
4.172 - using A f[THEN bij_betw_imp_funcset] by (auto simp: vimage_UN[symmetric])
4.173 - show "range (\<lambda>i. f -` A i \<inter> S) \<subseteq> sets (vimage_algebra S f)"
4.174 - using A by (auto simp: vimage_algebra_def)
4.175 - have "\<And>i. f ` (f -` A i \<inter> S) = A i"
4.176 - using f A sets_into_space
4.177 - by (intro image_vimage_inter_eq) (auto simp: bij_betw_def)
4.178 - then show "\<forall>i. \<mu> (f ` (f -` A i \<inter> S)) \<noteq> \<omega>" using A by simp
4.179 - qed
4.180 - qed
4.181 -qed
4.182 -
4.183 section "Real measure values"
4.184
4.185 lemma (in measure_space) real_measure_Union:
5.1 --- a/src/HOL/Probability/Probability_Space.thy Fri Jan 21 10:43:09 2011 +0100
5.2 +++ b/src/HOL/Probability/Probability_Space.thy Tue Jan 25 09:45:45 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 10:43:09 2011 +0100
6.2 +++ b/src/HOL/Probability/Product_Measure.thy Tue Jan 25 09:45:45 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 @@ -656,29 +651,20 @@
6.45 show "range F \<subseteq> sets E" "F \<up> space E" "\<And>i. pair_measure (F i) \<noteq> \<omega>"
6.46 using F by auto
6.47 show "measure_space P pair_measure" by default
6.48 - next
6.49 + interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
6.50 + have P: "sigma_algebra P" by default
6.51 show "measure_space P ?\<nu>"
6.52 - proof
6.53 - show "?\<nu> {} = 0" by auto
6.54 - show "countably_additive P ?\<nu>"
6.55 - unfolding countably_additive_def
6.56 - proof (intro allI impI)
6.57 - fix F :: "nat \<Rightarrow> ('a \<times> 'b) set"
6.58 - assume F: "range F \<subseteq> sets P" "disjoint_family F"
6.59 - from F have *: "\<And>i. F i \<in> sets P" "(\<Union>i. F i) \<in> sets P" by auto
6.60 - moreover from F have "\<And>i. (\<lambda>y. \<mu>1 ((\<lambda>x. (x, y)) -` F i)) \<in> borel_measurable M2"
6.61 - by (intro measure_cut_measurable_snd) auto
6.62 - moreover have "\<And>y. disjoint_family (\<lambda>i. (\<lambda>x. (x, y)) -` F i)"
6.63 - by (intro disjoint_family_on_bisimulation[OF F(2)]) auto
6.64 - moreover have "\<And>y. y \<in> space M2 \<Longrightarrow> range (\<lambda>i. (\<lambda>x. (x, y)) -` F i) \<subseteq> sets M1"
6.65 - using F by (auto intro!: measurable_cut_snd)
6.66 - ultimately show "(\<Sum>\<^isub>\<infinity>n. ?\<nu> (F n)) = ?\<nu> (\<Union>i. F i)"
6.67 - by (simp add: vimage_UN M2.positive_integral_psuminf[symmetric]
6.68 - M1.measure_countably_additive
6.69 - cong: M2.positive_integral_cong)
6.70 - qed
6.71 + apply (rule Q.measure_space_vimage[OF P])
6.72 + apply (rule Q.pair_sigma_algebra_swap_measurable)
6.73 + proof -
6.74 + fix A assume "A \<in> sets P"
6.75 + from sets_swap[OF this]
6.76 + show "M2.positive_integral (\<lambda>y. \<mu>1 ((\<lambda>x. (x, y)) -` A)) =
6.77 + Q.pair_measure ((\<lambda>(x, y). (y, x)) -` A \<inter> space Q.P)"
6.78 + using sets_into_space[OF `A \<in> sets P`]
6.79 + by (auto simp add: Q.pair_measure_alt space_pair_algebra
6.80 + intro!: M2.positive_integral_cong arg_cong[where f=\<mu>1])
6.81 qed
6.82 - next
6.83 fix X assume "X \<in> sets E"
6.84 then obtain A B where X: "X = A \<times> B" and AB: "A \<in> sets M1" "B \<in> sets M2"
6.85 unfolding pair_algebra_def by auto
6.86 @@ -802,31 +788,40 @@
6.87 unfolding F_SUPR by simp
6.88 qed
6.89
6.90 +lemma (in pair_sigma_finite) positive_integral_product_swap:
6.91 + assumes f: "f \<in> borel_measurable P"
6.92 + shows "measure_space.positive_integral
6.93 + (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.94 + positive_integral f"
6.95 +proof -
6.96 + interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
6.97 + have P: "sigma_algebra P" by default
6.98 + show ?thesis
6.99 + unfolding Q.positive_integral_vimage[OF P Q.pair_sigma_algebra_swap_measurable f, symmetric]
6.100 + proof (rule positive_integral_cong_measure)
6.101 + fix A
6.102 + assume A: "A \<in> sets P"
6.103 + from Q.pair_sigma_algebra_swap_measurable[THEN measurable_sets, OF this] this sets_into_space[OF this]
6.104 + show "Q.pair_measure ((\<lambda>(x, y). (y, x)) -` A \<inter> space Q.P) = pair_measure A"
6.105 + by (auto intro!: M1.positive_integral_cong arg_cong[where f=\<mu>2]
6.106 + simp: pair_measure_alt Q.pair_measure_alt2 space_pair_algebra)
6.107 + qed
6.108 +qed
6.109 +
6.110 lemma (in pair_sigma_finite) positive_integral_snd_measurable:
6.111 assumes f: "f \<in> borel_measurable P"
6.112 shows "M2.positive_integral (\<lambda>y. M1.positive_integral (\<lambda>x. f (x, y))) =
6.113 positive_integral f"
6.114 proof -
6.115 interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
6.116 - have s: "\<And>x y. (case (x, y) of (x, y) \<Rightarrow> f (y, x)) = f (y, x)" by simp
6.117 - 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.118 - have bij: "bij_betw (\<lambda>(x, y). (y, x)) (space M2 \<times> space M1) (space P)"
6.119 - by (auto intro!: inj_onI simp: space_pair_algebra bij_betw_def)
6.120 note pair_sigma_algebra_measurable[OF f]
6.121 from Q.positive_integral_fst_measurable[OF this]
6.122 have "M2.positive_integral (\<lambda>y. M1.positive_integral (\<lambda>x. f (x, y))) =
6.123 Q.positive_integral (\<lambda>(x, y). f (y, x))"
6.124 by simp
6.125 - also have "\<dots> = positive_integral f"
6.126 - unfolding positive_integral_vimage[OF bij, of f] t
6.127 - unfolding pair_sigma_algebra_swap[symmetric]
6.128 - proof (rule Q.positive_integral_cong_measure[symmetric])
6.129 - fix A assume "A \<in> sets Q.P"
6.130 - from this Q.sets_pair_sigma_algebra_swap[OF this]
6.131 - show "pair_measure ((\<lambda>(x, y). (y, x)) ` A) = Q.pair_measure A"
6.132 - by (auto intro!: M1.positive_integral_cong arg_cong[where f=\<mu>2]
6.133 - simp: pair_measure_alt Q.pair_measure_alt2)
6.134 - qed
6.135 + also have "Q.positive_integral (\<lambda>(x, y). f (y, x)) = positive_integral f"
6.136 + unfolding positive_integral_product_swap[OF f, symmetric]
6.137 + by (auto intro!: Q.positive_integral_cong)
6.138 finally show ?thesis .
6.139 qed
6.140
6.141 @@ -863,28 +858,6 @@
6.142 qed
6.143 qed
6.144
6.145 -lemma (in pair_sigma_finite) positive_integral_product_swap:
6.146 - "measure_space.positive_integral
6.147 - (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) f =
6.148 - positive_integral (\<lambda>(x,y). f (y,x))"
6.149 -proof -
6.150 - interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
6.151 - have t: "(\<lambda>y. case case y of (y, x) \<Rightarrow> (x, y) of (x, y) \<Rightarrow> f (y, x)) = f"
6.152 - by (auto simp: fun_eq_iff)
6.153 - have bij: "bij_betw (\<lambda>(x, y). (y, x)) (space M2 \<times> space M1) (space P)"
6.154 - by (auto intro!: inj_onI simp: space_pair_algebra bij_betw_def)
6.155 - show ?thesis
6.156 - unfolding positive_integral_vimage[OF bij, of "\<lambda>(y,x). f (x,y)"]
6.157 - unfolding pair_sigma_algebra_swap[symmetric] t
6.158 - proof (rule Q.positive_integral_cong_measure[symmetric])
6.159 - fix A assume "A \<in> sets Q.P"
6.160 - from this Q.sets_pair_sigma_algebra_swap[OF this]
6.161 - show "pair_measure ((\<lambda>(x, y). (y, x)) ` A) = Q.pair_measure A"
6.162 - by (auto intro!: M1.positive_integral_cong arg_cong[where f=\<mu>2]
6.163 - simp: pair_measure_alt Q.pair_measure_alt2)
6.164 - qed
6.165 -qed
6.166 -
6.167 lemma (in pair_sigma_algebra) measurable_product_swap:
6.168 "f \<in> measurable (sigma (pair_algebra M2 M1)) M \<longleftrightarrow> (\<lambda>(x,y). f (y,x)) \<in> measurable P M"
6.169 proof -
6.170 @@ -895,27 +868,42 @@
6.171 qed
6.172
6.173 lemma (in pair_sigma_finite) integrable_product_swap:
6.174 - "measure_space.integrable
6.175 - (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) f \<longleftrightarrow>
6.176 - integrable (\<lambda>(x,y). f (y,x))"
6.177 + assumes "integrable f"
6.178 + shows "measure_space.integrable
6.179 + (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) (\<lambda>(x,y). f (y,x))"
6.180 proof -
6.181 interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
6.182 - show ?thesis
6.183 - unfolding Q.integrable_def integrable_def
6.184 - unfolding positive_integral_product_swap
6.185 - unfolding measurable_product_swap
6.186 - by (simp add: case_prod_distrib)
6.187 + 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.188 + show ?thesis unfolding *
6.189 + using assms unfolding Q.integrable_def integrable_def
6.190 + apply (subst (1 2) positive_integral_product_swap)
6.191 + using `integrable f` unfolding integrable_def
6.192 + by (auto simp: *[symmetric] Q.measurable_product_swap[symmetric])
6.193 +qed
6.194 +
6.195 +lemma (in pair_sigma_finite) integrable_product_swap_iff:
6.196 + "measure_space.integrable
6.197 + (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) (\<lambda>(x,y). f (y,x)) \<longleftrightarrow>
6.198 + integrable f"
6.199 +proof -
6.200 + interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
6.201 + from Q.integrable_product_swap[of "\<lambda>(x,y). f (y,x)"] integrable_product_swap[of f]
6.202 + show ?thesis by auto
6.203 qed
6.204
6.205 lemma (in pair_sigma_finite) integral_product_swap:
6.206 - "measure_space.integral
6.207 - (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) f =
6.208 - integral (\<lambda>(x,y). f (y,x))"
6.209 + assumes "integrable f"
6.210 + shows "measure_space.integral
6.211 + (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) (\<lambda>(x,y). f (y,x)) =
6.212 + integral f"
6.213 proof -
6.214 interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
6.215 + 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.216 show ?thesis
6.217 - unfolding integral_def Q.integral_def positive_integral_product_swap
6.218 - by (simp add: case_prod_distrib)
6.219 + unfolding integral_def Q.integral_def *
6.220 + apply (subst (1 2) positive_integral_product_swap)
6.221 + using `integrable f` unfolding integrable_def
6.222 + by (auto simp: *[symmetric] Q.measurable_product_swap[symmetric])
6.223 qed
6.224
6.225 lemma (in pair_sigma_finite) integrable_fst_measurable:
6.226 @@ -988,10 +976,10 @@
6.227 proof -
6.228 interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
6.229 have Q_int: "Q.integrable (\<lambda>(x, y). f (y, x))"
6.230 - using f unfolding integrable_product_swap by simp
6.231 + using f unfolding integrable_product_swap_iff .
6.232 show ?INT
6.233 using Q.integrable_fst_measurable(2)[OF Q_int]
6.234 - unfolding integral_product_swap by simp
6.235 + using integral_product_swap[OF f] by simp
6.236 show ?AE
6.237 using Q.integrable_fst_measurable(1)[OF Q_int]
6.238 by simp
6.239 @@ -1355,18 +1343,6 @@
6.240 pair_algebra_sets_into_space product_algebra_sets_into_space)
6.241 auto
6.242
6.243 -lemma (in product_sigma_algebra) product_product_vimage_algebra:
6.244 - assumes [simp]: "I \<inter> J = {}"
6.245 - shows "sigma_algebra.vimage_algebra
6.246 - (sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J))))
6.247 - (space (sigma (product_algebra M (I \<union> J)))) (\<lambda>x. ((\<lambda>i\<in>I. x i), (\<lambda>i\<in>J. x i))) =
6.248 - sigma (product_algebra M (I \<union> J))"
6.249 - unfolding sigma_pair_algebra_sigma_eq using sets_into_space
6.250 - by (intro vimage_algebra_sigma[OF bij_inv_restrict_merge]
6.251 - pair_algebra_sets_into_space product_algebra_sets_into_space
6.252 - measurable_merge_on_generating measurable_restrict_on_generating)
6.253 - auto
6.254 -
6.255 lemma (in product_sigma_algebra) pair_product_product_vimage_algebra:
6.256 assumes [simp]: "I \<inter> J = {}"
6.257 shows "sigma_algebra.vimage_algebra (sigma (product_algebra M (I \<union> J)))
6.258 @@ -1378,24 +1354,6 @@
6.259 measurable_merge_on_generating measurable_restrict_on_generating)
6.260 auto
6.261
6.262 -lemma (in product_sigma_algebra) pair_product_singleton_vimage_algebra:
6.263 - assumes [simp]: "i \<notin> I"
6.264 - shows "sigma_algebra.vimage_algebra (sigma (pair_algebra (sigma (product_algebra M I)) (M i)))
6.265 - (space (sigma (product_algebra M (insert i I)))) (\<lambda>x. (restrict x I, x i)) =
6.266 - (sigma (product_algebra M (insert i I)))"
6.267 - unfolding sigma_pair_algebra_product_singleton using sets_into_space
6.268 - by (intro vimage_algebra_sigma[OF bij_inv_restrict_insert]
6.269 - pair_algebra_sets_into_space product_algebra_sets_into_space
6.270 - measurable_merge_singleton_on_generating measurable_restrict_singleton_on_generating)
6.271 - auto
6.272 -
6.273 -lemma (in product_sigma_algebra) singleton_vimage_algebra:
6.274 - "sigma_algebra.vimage_algebra (sigma (product_algebra M {i})) (space (M i)) (\<lambda>x. \<lambda>j\<in>{i}. x) = M i"
6.275 - using sets_into_space
6.276 - by (intro vimage_algebra_sigma[of "M i", unfolded M.sigma_eq, OF bij_inv_singleton[symmetric]]
6.277 - product_algebra_sets_into_space measurable_singleton_on_generator measurable_component_on_generator)
6.278 - auto
6.279 -
6.280 lemma (in product_sigma_algebra) measurable_restrict_iff:
6.281 assumes IJ[simp]: "I \<inter> J = {}"
6.282 shows "f \<in> measurable (sigma (pair_algebra
6.283 @@ -1430,6 +1388,13 @@
6.284 then show "?f \<in> measurable ?P M'" by (simp add: comp_def)
6.285 qed
6.286
6.287 +lemma (in product_sigma_algebra) singleton_vimage_algebra:
6.288 + "sigma_algebra.vimage_algebra (sigma (product_algebra M {i})) (space (M i)) (\<lambda>x. \<lambda>j\<in>{i}. x) = M i"
6.289 + using sets_into_space
6.290 + by (intro vimage_algebra_sigma[of "M i", unfolded M.sigma_eq, OF bij_inv_singleton[symmetric]]
6.291 + product_algebra_sets_into_space measurable_singleton_on_generator measurable_component_on_generator)
6.292 + auto
6.293 +
6.294 lemma (in product_sigma_algebra) measurable_component_singleton:
6.295 "(\<lambda>x. f (x i)) \<in> measurable (sigma (product_algebra M {i})) M' \<longleftrightarrow>
6.296 f \<in> measurable (M i) M'"
6.297 @@ -1479,6 +1444,55 @@
6.298 using sets_into_space unfolding measurable_component_singleton[symmetric]
6.299 by (auto intro!: measurable_cong arg_cong[where f=f] simp: fun_eq_iff extensional_def)
6.300
6.301 +
6.302 +lemma (in pair_sigma_algebra) measurable_pair_split:
6.303 + assumes "sigma_algebra M1'" "sigma_algebra M2'"
6.304 + assumes f: "f \<in> measurable M1 M1'" and g: "g \<in> measurable M2 M2'"
6.305 + shows "(\<lambda>(x, y). (f x, g y)) \<in> measurable P (sigma (pair_algebra M1' M2'))"
6.306 +proof (rule measurable_sigma)
6.307 + interpret M1': sigma_algebra M1' by fact
6.308 + interpret M2': sigma_algebra M2' by fact
6.309 + interpret Q: pair_sigma_algebra M1' M2' by default
6.310 + show "sets Q.E \<subseteq> Pow (space Q.E)"
6.311 + using M1'.sets_into_space M2'.sets_into_space by (auto simp: pair_algebra_def)
6.312 + show "(\<lambda>(x, y). (f x, g y)) \<in> space P \<rightarrow> space Q.E"
6.313 + using f g unfolding measurable_def pair_algebra_def by auto
6.314 + fix A assume "A \<in> sets Q.E"
6.315 + then obtain X Y where A: "A = X \<times> Y" "X \<in> sets M1'" "Y \<in> sets M2'"
6.316 + unfolding pair_algebra_def by auto
6.317 + then have *: "(\<lambda>(x, y). (f x, g y)) -` A \<inter> space P =
6.318 + (f -` X \<inter> space M1) \<times> (g -` Y \<inter> space M2)"
6.319 + by (auto simp: pair_algebra_def)
6.320 + then show "(\<lambda>(x, y). (f x, g y)) -` A \<inter> space P \<in> sets P"
6.321 + using f g A unfolding measurable_def *
6.322 + by (auto intro!: pair_algebraI in_sigma)
6.323 +qed
6.324 +
6.325 +lemma (in product_sigma_algebra) measurable_add_dim:
6.326 + assumes "i \<notin> I" "finite I"
6.327 + shows "(\<lambda>(f, y). f(i := y)) \<in> measurable (sigma (pair_algebra (sigma (product_algebra M I)) (M i)))
6.328 + (sigma (product_algebra M (insert i I)))"
6.329 +proof (subst measurable_cong)
6.330 + interpret I: finite_product_sigma_algebra M I by default fact
6.331 + interpret i: finite_product_sigma_algebra M "{i}" by default auto
6.332 + interpret Ii: pair_sigma_algebra I.P "M i" by default
6.333 + interpret Ii': pair_sigma_algebra I.P i.P by default
6.334 + have disj: "I \<inter> {i} = {}" using `i \<notin> I` by auto
6.335 + have "(\<lambda>(x, y). (id x, \<lambda>_\<in>{i}. y)) \<in> measurable Ii.P Ii'.P"
6.336 + proof (intro Ii.measurable_pair_split I.measurable_ident)
6.337 + show "(\<lambda>y. \<lambda>_\<in>{i}. y) \<in> measurable (M i) i.P"
6.338 + apply (rule measurable_singleton[THEN iffD1])
6.339 + using i.measurable_ident unfolding id_def .
6.340 + qed default
6.341 + from measurable_comp[OF this measurable_merge[OF disj]]
6.342 + show "(\<lambda>(x, y). merge I x {i} y) \<circ> (\<lambda>(x, y). (id x, \<lambda>_\<in>{i}. y))
6.343 + \<in> measurable (sigma (pair_algebra I.P (M i))) (sigma (product_algebra M (insert i I)))"
6.344 + (is "?f \<in> _") by simp
6.345 + fix x assume "x \<in> space Ii.P"
6.346 + with assms show "(\<lambda>(f, y). f(i := y)) x = ?f x"
6.347 + by (cases x) (simp add: merge_def fun_eq_iff pair_algebra_def extensional_def)
6.348 +qed
6.349 +
6.350 locale product_sigma_finite =
6.351 fixes M :: "'i \<Rightarrow> 'a algebra" and \<mu> :: "'i \<Rightarrow> 'a set \<Rightarrow> pextreal"
6.352 assumes sigma_finite_measures: "\<And>i. sigma_finite_measure (M i) (\<mu> i)"
6.353 @@ -1549,29 +1563,24 @@
6.354 interpret I: sigma_finite_measure P \<nu> by fact
6.355 interpret P: pair_sigma_finite P \<nu> "M i" "\<mu> i" ..
6.356
6.357 - let ?h = "\<lambda>x. (restrict x I, x i)"
6.358 - let ?\<nu> = "\<lambda>A. P.pair_measure (?h ` A)"
6.359 + let ?h = "(\<lambda>(f, y). f(i := y))"
6.360 + let ?\<nu> = "\<lambda>A. P.pair_measure (?h -` A \<inter> space P.P)"
6.361 + have I': "sigma_algebra I'.P" by default
6.362 interpret I': measure_space "sigma (product_algebra M (insert i I))" ?\<nu>
6.363 - apply (subst pair_product_singleton_vimage_algebra[OF `i \<notin> I`, symmetric])
6.364 - apply (intro P.measure_space_isomorphic bij_inv_bij_betw)
6.365 - unfolding sigma_pair_algebra_product_singleton
6.366 - by (rule bij_inv_restrict_insert[OF `i \<notin> I`])
6.367 + apply (rule P.measure_space_vimage[OF I'])
6.368 + apply (rule measurable_add_dim[OF `i \<notin> I` `finite I`])
6.369 + by simp
6.370 show ?case
6.371 proof (intro exI[of _ ?\<nu>] conjI ballI)
6.372 { fix A assume A: "A \<in> (\<Pi> i\<in>insert i I. sets (M i))"
6.373 - moreover then have "A \<in> (\<Pi> i\<in>I. sets (M i))" by auto
6.374 - 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.375 - using `i \<notin> I`
6.376 - apply auto
6.377 - apply (rule_tac x="a(i:=b)" in image_eqI)
6.378 - apply (auto simp: extensional_def fun_eq_iff)
6.379 - done
6.380 - ultimately show "?\<nu> (Pi\<^isub>E (insert i I) A) = (\<Prod>i\<in>insert i I. \<mu> i (A i))"
6.381 - apply simp
6.382 + then have *: "?h -` Pi\<^isub>E (insert i I) A \<inter> space P.P = Pi\<^isub>E I A \<times> A i"
6.383 + using `i \<notin> I` M.sets_into_space by (auto simp: pair_algebra_def) blast
6.384 + show "?\<nu> (Pi\<^isub>E (insert i I) A) = (\<Prod>i\<in>insert i I. \<mu> i (A i))"
6.385 + unfolding * using A
6.386 apply (subst P.pair_measure_times)
6.387 - apply fastsimp
6.388 - apply fastsimp
6.389 - using `i \<notin> I` `finite I` prod[of A] by (auto simp: ac_simps) }
6.390 + using A apply fastsimp
6.391 + using A apply fastsimp
6.392 + using `i \<notin> I` `finite I` prod[of A] A by (auto simp: ac_simps) }
6.393 note product = this
6.394 show "sigma_finite_measure I'.P ?\<nu>"
6.395 proof
6.396 @@ -1671,7 +1680,7 @@
6.397 shows "pair_sigma_finite.pair_measure
6.398 (sigma (product_algebra M I)) (product_measure I)
6.399 (sigma (product_algebra M J)) (product_measure J)
6.400 - ((\<lambda>x. ((\<lambda>i\<in>I. x i), (\<lambda>i\<in>J. x i))) ` A) =
6.401 + ((\<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.402 product_measure (I \<union> J) A"
6.403 proof -
6.404 interpret I: finite_product_sigma_finite M \<mu> I by default fact
6.405 @@ -1679,51 +1688,52 @@
6.406 have "finite (I \<union> J)" using fin by auto
6.407 interpret IJ: finite_product_sigma_finite M \<mu> "I \<union> J" by default fact
6.408 interpret P: pair_sigma_finite I.P I.measure J.P J.measure by default
6.409 - let ?f = "\<lambda>x. ((\<lambda>i\<in>I. x i), (\<lambda>i\<in>J. x i))"
6.410 - from IJ.sigma_finite_pairs obtain F where
6.411 - F: "\<And>i. i\<in> I \<union> J \<Longrightarrow> range (F i) \<subseteq> sets (M i)"
6.412 - "(\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k) \<up> space IJ.G"
6.413 - "\<And>k. \<forall>i\<in>I\<union>J. \<mu> i (F i k) \<noteq> \<omega>"
6.414 - by auto
6.415 - let ?F = "\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k"
6.416 - 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.417 - apply auto apply (rule_tac x="merge I a J b" in image_eqI)
6.418 - by (auto dest: extensional_restrict)
6.419 - show "P.pair_measure (?f ` A) = IJ.measure A"
6.420 + let ?g = "\<lambda>(x,y). merge I x J y"
6.421 + let "?X S" = "?g -` S \<inter> space P.P"
6.422 + from IJ.sigma_finite_pairs obtain F where
6.423 + F: "\<And>i. i\<in> I \<union> J \<Longrightarrow> range (F i) \<subseteq> sets (M i)"
6.424 + "(\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k) \<up> space IJ.G"
6.425 + "\<And>k. \<forall>i\<in>I\<union>J. \<mu> i (F i k) \<noteq> \<omega>"
6.426 + by auto
6.427 + let ?F = "\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k"
6.428 + show "P.pair_measure (?X A) = IJ.measure A"
6.429 proof (rule measure_unique_Int_stable[OF _ _ _ _ _ _ _ _ A])
6.430 - show "Int_stable IJ.G" by (simp add: PiE_Int Int_stable_def product_algebra_def) auto
6.431 - show "range ?F \<subseteq> sets IJ.G" using F by (simp add: image_subset_iff product_algebra_def)
6.432 - show "?F \<up> space IJ.G " using F(2) by simp
6.433 - show "measure_space IJ.P (\<lambda>A. P.pair_measure (?f ` A))"
6.434 - apply (subst product_product_vimage_algebra[OF IJ, symmetric])
6.435 - apply (intro P.measure_space_isomorphic bij_inv_bij_betw)
6.436 - unfolding sigma_pair_algebra_sigma_eq
6.437 - by (rule bij_inv_restrict_merge[OF `I \<inter> J = {}`])
6.438 - show "measure_space IJ.P IJ.measure" by fact
6.439 - next
6.440 - fix A assume "A \<in> sets IJ.G"
6.441 - 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.442 - by (auto simp: product_algebra_def)
6.443 - 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.444 - by auto
6.445 - have "P.pair_measure (?f ` A) = (\<Prod>i\<in>I. \<mu> i (F i)) * (\<Prod>i\<in>J. \<mu> i (F i))"
6.446 - using `finite J` `finite I` F
6.447 - by (simp add: P.pair_measure_times I.measure_times J.measure_times)
6.448 - also have "\<dots> = (\<Prod>i\<in>I \<union> J. \<mu> i (F i))"
6.449 - using `finite J` `finite I` `I \<inter> J = {}` by (simp add: setprod_Un_one)
6.450 - also have "\<dots> = IJ.measure A"
6.451 - using `finite J` `finite I` F unfolding A
6.452 - by (intro IJ.measure_times[symmetric]) auto
6.453 - finally show "P.pair_measure (?f ` A) = IJ.measure A" .
6.454 - next
6.455 - fix k
6.456 - have "\<And>i. i \<in> I \<union> J \<Longrightarrow> F i k \<in> sets (M i)" using F by auto
6.457 - 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.458 - by (simp add: P.pair_measure_times I.measure_times J.measure_times)
6.459 - then show "P.pair_measure (?f ` ?F k) \<noteq> \<omega>"
6.460 - using `finite I` F by (simp add: setprod_\<omega>)
6.461 - qed simp
6.462 - qed
6.463 + show "Int_stable IJ.G" by (simp add: PiE_Int Int_stable_def product_algebra_def) auto
6.464 + show "range ?F \<subseteq> sets IJ.G" using F by (simp add: image_subset_iff product_algebra_def)
6.465 + show "?F \<up> space IJ.G " using F(2) by simp
6.466 + have "sigma_algebra IJ.P" by default
6.467 + then show "measure_space IJ.P (\<lambda>A. P.pair_measure (?X A))"
6.468 + apply (rule P.measure_space_vimage)
6.469 + apply (rule measurable_merge[OF `I \<inter> J = {}`])
6.470 + by simp
6.471 + show "measure_space IJ.P IJ.measure" by fact
6.472 + next
6.473 + fix A assume "A \<in> sets IJ.G"
6.474 + then obtain F where A[simp]: "A = Pi\<^isub>E (I \<union> J) F"
6.475 + and F: "\<And>i. i \<in> I \<union> J \<Longrightarrow> F i \<in> sets (M i)"
6.476 + by (auto simp: product_algebra_def)
6.477 + then have "?X A = (Pi\<^isub>E I F \<times> Pi\<^isub>E J F)"
6.478 + using sets_into_space by (auto simp: space_pair_algebra) blast+
6.479 + then have "P.pair_measure (?X A) = (\<Prod>i\<in>I. \<mu> i (F i)) * (\<Prod>i\<in>J. \<mu> i (F i))"
6.480 + using `finite J` `finite I` F
6.481 + by (simp add: P.pair_measure_times I.measure_times J.measure_times)
6.482 + also have "\<dots> = (\<Prod>i\<in>I \<union> J. \<mu> i (F i))"
6.483 + using `finite J` `finite I` `I \<inter> J = {}` by (simp add: setprod_Un_one)
6.484 + also have "\<dots> = IJ.measure A"
6.485 + using `finite J` `finite I` F unfolding A
6.486 + by (intro IJ.measure_times[symmetric]) auto
6.487 + finally show "P.pair_measure (?X A) = IJ.measure A" .
6.488 + next
6.489 + fix k
6.490 + have k: "\<And>i. i \<in> I \<union> J \<Longrightarrow> F i k \<in> sets (M i)" using F by auto
6.491 + 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.492 + using sets_into_space by (auto simp: space_pair_algebra) blast+
6.493 + 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.494 + by (simp add: P.pair_measure_times I.measure_times J.measure_times)
6.495 + then show "P.pair_measure (?X (?F k)) \<noteq> \<omega>"
6.496 + using `finite I` F by (simp add: setprod_\<omega>)
6.497 + qed simp
6.498 +qed
6.499
6.500 lemma (in product_sigma_finite) product_positive_integral_fold:
6.501 assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
6.502 @@ -1736,23 +1746,18 @@
6.503 have "finite (I \<union> J)" using fin by auto
6.504 interpret IJ: finite_product_sigma_finite M \<mu> "I \<union> J" by default fact
6.505 interpret P: pair_sigma_finite I.P I.measure J.P J.measure by default
6.506 - let ?f = "\<lambda>x. ((\<lambda>i\<in>I. x i), (\<lambda>i\<in>J. x i))"
6.507 have P_borel: "(\<lambda>x. f (case x of (x, y) \<Rightarrow> merge I x J y)) \<in> borel_measurable P.P"
6.508 unfolding case_prod_distrib measurable_merge_iff[OF IJ, symmetric] using f .
6.509 - have bij: "bij_betw ?f (space IJ.P) (space P.P)"
6.510 - unfolding sigma_pair_algebra_sigma_eq
6.511 - by (intro bij_inv_bij_betw) (rule bij_inv_restrict_merge[OF IJ])
6.512 - have "IJ.positive_integral f = IJ.positive_integral (\<lambda>x. f (restrict x (I \<union> J)))"
6.513 - by (auto intro!: IJ.positive_integral_cong arg_cong[where f=f] dest!: extensional_restrict)
6.514 - also have "\<dots> = I.positive_integral (\<lambda>x. J.positive_integral (\<lambda>y. f (merge I x J y)))"
6.515 + show ?thesis
6.516 unfolding P.positive_integral_fst_measurable[OF P_borel, simplified]
6.517 - unfolding P.positive_integral_vimage[OF bij]
6.518 - unfolding product_product_vimage_algebra[OF IJ]
6.519 - apply simp
6.520 - apply (rule IJ.positive_integral_cong_measure[symmetric])
6.521 - apply (rule measure_fold)
6.522 - using assms by auto
6.523 - finally show ?thesis .
6.524 + apply (subst IJ.positive_integral_cong_measure[symmetric])
6.525 + apply (rule measure_fold[OF IJ fin])
6.526 + apply assumption
6.527 + proof (rule P.positive_integral_vimage)
6.528 + show "sigma_algebra IJ.P" by default
6.529 + show "(\<lambda>(x, y). merge I x J y) \<in> measurable P.P IJ.P" by (rule measurable_merge[OF IJ])
6.530 + show "f \<in> borel_measurable IJ.P" using f .
6.531 + qed
6.532 qed
6.533
6.534 lemma (in product_sigma_finite) product_positive_integral_singleton:
6.535 @@ -1760,31 +1765,18 @@
6.536 shows "product_positive_integral {i} (\<lambda>x. f (x i)) = M.positive_integral i f"
6.537 proof -
6.538 interpret I: finite_product_sigma_finite M \<mu> "{i}" by default simp
6.539 - have bij: "bij_betw (\<lambda>x. \<lambda>j\<in>{i}. x) (space (M i)) (space I.P)"
6.540 - by (auto intro!: bij_betwI ext simp: extensional_def)
6.541 - 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.542 - proof (subst image_cong, rule refl)
6.543 - fix x assume "x \<in> (\<Pi> i\<in>{i}. sets (M i))"
6.544 - then show "(\<lambda>x. \<lambda>j\<in>{i}. x) -` Pi\<^isub>E {i} x \<inter> space (M i) = x i"
6.545 - using sets_into_space by auto
6.546 - qed auto
6.547 - have vimage: "I.vimage_algebra (space (M i)) (\<lambda>x. \<lambda>j\<in>{i}. x) = M i"
6.548 - unfolding I.vimage_algebra_def
6.549 - unfolding product_sigma_algebra_def sets_sigma
6.550 - apply (subst sigma_sets_vimage[symmetric])
6.551 - apply (simp_all add: image_image sigma_sets_eq product_algebra_def * del: vimage_Int)
6.552 - using sets_into_space by blast
6.553 + have T: "(\<lambda>x. x i) \<in> measurable (sigma (product_algebra M {i})) (M i)"
6.554 + using measurable_component_singleton[of "\<lambda>x. x" i]
6.555 + measurable_ident[unfolded id_def] by auto
6.556 show "I.positive_integral (\<lambda>x. f (x i)) = M.positive_integral i f"
6.557 - unfolding I.positive_integral_vimage[OF bij]
6.558 - unfolding vimage
6.559 - apply (subst positive_integral_cong_measure)
6.560 - proof -
6.561 - fix A assume A: "A \<in> sets (M i)"
6.562 - have "(\<lambda>x. \<lambda>j\<in>{i}. x) ` A = (\<Pi>\<^isub>E i\<in>{i}. A)"
6.563 - by (auto intro!: image_eqI ext[where 'b='a] simp: extensional_def)
6.564 - with A show "product_measure {i} ((\<lambda>x. \<lambda>j\<in>{i}. x) ` A) = \<mu> i A"
6.565 - using I.measure_times[of "\<lambda>i. A"] by simp
6.566 - qed simp
6.567 + unfolding I.positive_integral_vimage[OF sigma_algebras T f, symmetric]
6.568 + proof (rule positive_integral_cong_measure)
6.569 + fix A let ?P = "(\<lambda>x. x i) -` A \<inter> space (sigma (product_algebra M {i}))"
6.570 + assume A: "A \<in> sets (M i)"
6.571 + then have *: "?P = {i} \<rightarrow>\<^isub>E A" using sets_into_space by auto
6.572 + show "product_measure {i} ?P = \<mu> i A" unfolding *
6.573 + using A I.measure_times[of "\<lambda>_. A"] by auto
6.574 + qed
6.575 qed
6.576
6.577 lemma (in product_sigma_finite) product_positive_integral_insert:
7.1 --- a/src/HOL/Probability/Radon_Nikodym.thy Fri Jan 21 10:43:09 2011 +0100
7.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy Tue Jan 25 09:45:45 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>"