--- a/src/HOL/Probability/Information.thy Fri Jan 21 10:43:09 2011 +0100
+++ b/src/HOL/Probability/Information.thy Tue Jan 25 09:45:45 2011 +0100
@@ -180,30 +180,6 @@
by (simp add: cong \<nu>.integral_cong_measure[OF cong(2)])
qed
-lemma (in sigma_finite_measure) KL_divergence_vimage:
- assumes f: "bij_betw f S (space M)"
- assumes \<nu>: "measure_space M \<nu>" "absolutely_continuous \<nu>"
- shows "KL_divergence b (vimage_algebra S f) (\<lambda>A. \<nu> (f ` A)) (\<lambda>A. \<mu> (f ` A)) = KL_divergence b M \<nu> \<mu>"
- (is "KL_divergence b ?M ?\<nu> ?\<mu> = _")
-proof -
- interpret \<nu>: measure_space M \<nu> by fact
- interpret v: measure_space ?M ?\<nu>
- using f by (rule \<nu>.measure_space_isomorphic)
-
- let ?RN = "sigma_finite_measure.RN_deriv ?M ?\<mu> ?\<nu>"
- from RN_deriv_vimage[OF f[THEN bij_inv_the_inv_into] \<nu>]
- have *: "\<nu>.almost_everywhere (\<lambda>x. ?RN (the_inv_into S f x) = RN_deriv \<nu> x)"
- by (rule absolutely_continuous_AE[OF \<nu>])
-
- show ?thesis
- unfolding KL_divergence_def \<nu>.integral_vimage_inv[OF f]
- apply (rule \<nu>.integral_cong_AE)
- apply (rule \<nu>.AE_mp[OF *])
- apply (rule \<nu>.AE_cong)
- apply simp
- done
-qed
-
lemma (in finite_measure_space) KL_divergence_eq_finite:
assumes v: "finite_measure_space M \<nu>"
assumes ac: "absolutely_continuous \<nu>"
@@ -259,50 +235,6 @@
\<lparr> space = X`space M, sets = Pow (X`space M) \<rparr>
\<lparr> space = Y`space M, sets = Pow (Y`space M) \<rparr> X Y"
-lemma (in information_space) mutual_information_commute_generic:
- assumes X: "random_variable S X" and Y: "random_variable T Y"
- assumes ac: "measure_space.absolutely_continuous (sigma (pair_algebra S T))
- (pair_sigma_finite.pair_measure S (distribution X) T (distribution Y)) (joint_distribution X Y)"
- shows "mutual_information b S T X Y = mutual_information b T S Y X"
-proof -
- interpret P: prob_space "sigma (pair_algebra S T)" "joint_distribution X Y"
- using random_variable_pairI[OF X Y] by (rule distribution_prob_space)
- interpret Q: prob_space "sigma (pair_algebra T S)" "joint_distribution Y X"
- using random_variable_pairI[OF Y X] by (rule distribution_prob_space)
- interpret X: prob_space S "distribution X" using X by (rule distribution_prob_space)
- interpret Y: prob_space T "distribution Y" using Y by (rule distribution_prob_space)
- interpret ST: pair_sigma_finite S "distribution X" T "distribution Y" by default
- interpret TS: pair_sigma_finite T "distribution Y" S "distribution X" by default
-
- have ST: "measure_space (sigma (pair_algebra S T)) (joint_distribution X Y)" by default
- have TS: "measure_space (sigma (pair_algebra T S)) (joint_distribution Y X)" by default
-
- have bij_ST: "bij_betw (\<lambda>(x, y). (y, x)) (space (sigma (pair_algebra S T))) (space (sigma (pair_algebra T S)))"
- by (auto intro!: inj_onI simp: space_pair_algebra bij_betw_def)
- have bij_TS: "bij_betw (\<lambda>(x, y). (y, x)) (space (sigma (pair_algebra T S))) (space (sigma (pair_algebra S T)))"
- by (auto intro!: inj_onI simp: space_pair_algebra bij_betw_def)
-
- { fix A
- have "joint_distribution X Y ((\<lambda>(x, y). (y, x)) ` A) = joint_distribution Y X A"
- unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>]) }
- note jd_commute = this
-
- { fix A assume A: "A \<in> sets (sigma (pair_algebra T S))"
- have *: "\<And>x y. indicator ((\<lambda>(x, y). (y, x)) ` A) (x, y) = (indicator A (y, x) :: pextreal)"
- unfolding indicator_def by auto
- have "ST.pair_measure ((\<lambda>(x, y). (y, x)) ` A) = TS.pair_measure A"
- unfolding ST.pair_measure_def TS.pair_measure_def
- using A by (auto simp add: TS.Fubini[symmetric] *) }
- note pair_measure_commute = this
-
- show ?thesis
- unfolding mutual_information_def
- unfolding ST.KL_divergence_vimage[OF bij_TS ST ac, symmetric]
- unfolding space_sigma space_pair_algebra jd_commute
- unfolding ST.pair_sigma_algebra_swap[symmetric]
- by (simp cong: TS.KL_divergence_cong[OF TS] add: pair_measure_commute)
-qed
-
lemma (in prob_space) finite_variables_absolutely_continuous:
assumes X: "finite_random_variable S X" and Y: "finite_random_variable T Y"
shows "measure_space.absolutely_continuous (sigma (pair_algebra S T))
@@ -330,16 +262,6 @@
qed
qed
-lemma (in information_space) mutual_information_commute:
- assumes X: "finite_random_variable S X" and Y: "finite_random_variable T Y"
- shows "mutual_information b S T X Y = mutual_information b T S Y X"
- by (intro finite_random_variableD X Y mutual_information_commute_generic finite_variables_absolutely_continuous)
-
-lemma (in information_space) mutual_information_commute_simple:
- assumes X: "simple_function X" and Y: "simple_function Y"
- shows "\<I>(X;Y) = \<I>(Y;X)"
- by (intro X Y simple_function_imp_finite_random_variable mutual_information_commute)
-
lemma (in information_space)
assumes MX: "finite_random_variable MX X"
assumes MY: "finite_random_variable MY Y"
@@ -371,6 +293,18 @@
unfolding mutual_information_def .
qed
+lemma (in information_space) mutual_information_commute:
+ assumes X: "finite_random_variable S X" and Y: "finite_random_variable T Y"
+ shows "mutual_information b S T X Y = mutual_information b T S Y X"
+ unfolding mutual_information_generic_eq[OF X Y] mutual_information_generic_eq[OF Y X]
+ unfolding joint_distribution_commute_singleton[of X Y]
+ by (auto simp add: ac_simps intro!: setsum_reindex_cong[OF swap_inj_on])
+
+lemma (in information_space) mutual_information_commute_simple:
+ assumes X: "simple_function X" and Y: "simple_function Y"
+ shows "\<I>(X;Y) = \<I>(Y;X)"
+ by (intro X Y simple_function_imp_finite_random_variable mutual_information_commute)
+
lemma (in information_space) mutual_information_eq:
assumes "simple_function X" "simple_function Y"
shows "\<I>(X;Y) = (\<Sum> (x,y) \<in> X ` space M \<times> Y ` space M.
--- a/src/HOL/Probability/Lebesgue_Integration.thy Fri Jan 21 10:43:09 2011 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Tue Jan 25 09:45:45 2011 +0100
@@ -471,20 +471,26 @@
unfolding sigma_algebra.simple_function_def[OF N_subalgebra(3)]
by auto
-lemma (in sigma_algebra) simple_function_vimage:
- fixes g :: "'a \<Rightarrow> pextreal" and f :: "'d \<Rightarrow> 'a"
- assumes g: "simple_function g" and f: "f \<in> S \<rightarrow> space M"
- shows "sigma_algebra.simple_function (vimage_algebra S f) (\<lambda>x. g (f x))"
-proof -
- have subset: "(\<lambda>x. g (f x)) ` S \<subseteq> g ` space M"
- using f by auto
- interpret V: sigma_algebra "vimage_algebra S f"
- using f by (rule sigma_algebra_vimage)
- show ?thesis using g
- unfolding simple_function_eq_borel_measurable
- unfolding V.simple_function_eq_borel_measurable
- using measurable_vimage[OF _ f, of g borel]
- using finite_subset[OF subset] by auto
+lemma (in measure_space) simple_function_vimage:
+ assumes T: "sigma_algebra M'" "T \<in> measurable M M'"
+ and f: "sigma_algebra.simple_function M' f"
+ shows "simple_function (\<lambda>x. f (T x))"
+proof (intro simple_function_def[THEN iffD2] conjI ballI)
+ interpret T: sigma_algebra M' by fact
+ have "(\<lambda>x. f (T x)) ` space M \<subseteq> f ` space M'"
+ using T unfolding measurable_def by auto
+ then show "finite ((\<lambda>x. f (T x)) ` space M)"
+ using f unfolding T.simple_function_def by (auto intro: finite_subset)
+ fix i assume i: "i \<in> (\<lambda>x. f (T x)) ` space M"
+ then have "i \<in> f ` space M'"
+ using T unfolding measurable_def by auto
+ then have "f -` {i} \<inter> space M' \<in> sets M'"
+ using f unfolding T.simple_function_def by auto
+ then have "T -` (f -` {i} \<inter> space M') \<inter> space M \<in> sets M"
+ using T unfolding measurable_def by auto
+ also have "T -` (f -` {i} \<inter> space M') \<inter> space M = (\<lambda>x. f (T x)) -` {i} \<inter> space M"
+ using T unfolding measurable_def by auto
+ finally show "(\<lambda>x. f (T x)) -` {i} \<inter> space M \<in> sets M" .
qed
section "Simple integral"
@@ -816,28 +822,30 @@
unfolding measure_space.simple_integral_def_raw[OF N] by simp
lemma (in measure_space) simple_integral_vimage:
- fixes g :: "'a \<Rightarrow> pextreal" and f :: "'d \<Rightarrow> 'a"
- assumes f: "bij_betw f S (space M)"
- shows "simple_integral g =
- measure_space.simple_integral (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) (\<lambda>x. g (f x))"
- (is "_ = measure_space.simple_integral ?T ?\<mu> _")
+ assumes T: "sigma_algebra M'" "T \<in> measurable M M'"
+ and f: "sigma_algebra.simple_function M' f"
+ shows "measure_space.simple_integral M' (\<lambda>A. \<mu> (T -` A \<inter> space M)) f = (\<integral>\<^isup>S x. f (T x))"
+ (is "measure_space.simple_integral M' ?nu f = _")
proof -
- from f interpret T: measure_space ?T ?\<mu> by (rule measure_space_isomorphic)
- have surj: "f`S = space M"
- using f unfolding bij_betw_def by simp
- have *: "(\<lambda>x. g (f x)) ` S = g ` f ` S" by auto
- have **: "f`S = space M" using f unfolding bij_betw_def by auto
- { fix x assume "x \<in> space M"
- have "(f ` ((\<lambda>x. g (f x)) -` {g x} \<inter> S)) =
- (f ` (f -` (g -` {g x}) \<inter> S))" by auto
- also have "f -` (g -` {g x}) \<inter> S = f -` (g -` {g x} \<inter> space M) \<inter> S"
- using f unfolding bij_betw_def by auto
- also have "(f ` (f -` (g -` {g x} \<inter> space M) \<inter> S)) = g -` {g x} \<inter> space M"
- using ** by (intro image_vimage_inter_eq) auto
- finally have "(f ` ((\<lambda>x. g (f x)) -` {g x} \<inter> S)) = g -` {g x} \<inter> space M" by auto }
- then show ?thesis using assms
- unfolding simple_integral_def T.simple_integral_def bij_betw_def
- by (auto simp add: * intro!: setsum_cong)
+ interpret T: measure_space M' ?nu using T by (rule measure_space_vimage) auto
+ show "T.simple_integral f = (\<integral>\<^isup>S x. f (T x))"
+ unfolding simple_integral_def T.simple_integral_def
+ proof (intro setsum_mono_zero_cong_right ballI)
+ show "(\<lambda>x. f (T x)) ` space M \<subseteq> f ` space M'"
+ using T unfolding measurable_def by auto
+ show "finite (f ` space M')"
+ using f unfolding T.simple_function_def by auto
+ next
+ fix i assume "i \<in> f ` space M' - (\<lambda>x. f (T x)) ` space M"
+ then have "T -` (f -` {i} \<inter> space M') \<inter> space M = {}" by (auto simp: image_iff)
+ then show "i * \<mu> (T -` (f -` {i} \<inter> space M') \<inter> space M) = 0" by simp
+ next
+ fix i assume "i \<in> (\<lambda>x. f (T x)) ` space M"
+ then have "T -` (f -` {i} \<inter> space M') \<inter> space M = (\<lambda>x. f (T x)) -` {i} \<inter> space M"
+ using T unfolding measurable_def by auto
+ then show "i * \<mu> (T -` (f -` {i} \<inter> space M') \<inter> space M) = i * \<mu> ((\<lambda>x. f (T x)) -` {i} \<inter> space M)"
+ by auto
+ qed
qed
section "Continuous posititve integration"
@@ -1016,71 +1024,6 @@
shows "f ` A = g ` B"
using assms by blast
-lemma (in measure_space) positive_integral_vimage:
- fixes g :: "'a \<Rightarrow> pextreal" and f :: "'d \<Rightarrow> 'a"
- assumes f: "bij_betw f S (space M)"
- shows "positive_integral g =
- measure_space.positive_integral (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) (\<lambda>x. g (f x))"
- (is "_ = measure_space.positive_integral ?T ?\<mu> _")
-proof -
- from f interpret T: measure_space ?T ?\<mu> by (rule measure_space_isomorphic)
- have f_fun: "f \<in> S \<rightarrow> space M" using assms unfolding bij_betw_def by auto
- from assms have inv: "bij_betw (the_inv_into S f) (space M) S"
- by (rule bij_betw_the_inv_into)
- then have inv_fun: "the_inv_into S f \<in> space M \<rightarrow> S" unfolding bij_betw_def by auto
- have surj: "f`S = space M"
- using f unfolding bij_betw_def by simp
- have inj: "inj_on f S"
- using f unfolding bij_betw_def by simp
- have inv_f: "\<And>x. x \<in> space M \<Longrightarrow> f (the_inv_into S f x) = x"
- using f_the_inv_into_f[of f S] f unfolding bij_betw_def by auto
- from simple_integral_vimage[OF assms, symmetric]
- have *: "simple_integral = T.simple_integral \<circ> (\<lambda>g. g \<circ> f)" by (simp add: comp_def)
- show ?thesis
- unfolding positive_integral_alt1 T.positive_integral_alt1 SUPR_def * image_compose
- proof (safe intro!: arg_cong[where f=Sup] image_set_cong, simp_all add: comp_def)
- fix g' :: "'a \<Rightarrow> pextreal" assume "simple_function g'" "\<forall>x\<in>space M. g' x \<le> g x \<and> g' x \<noteq> \<omega>"
- 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>
- T.simple_integral (\<lambda>x. g' (f x)) = T.simple_integral h"
- using f unfolding bij_betw_def
- by (auto intro!: exI[of _ "\<lambda>x. g' (f x)"]
- simp add: le_fun_def simple_function_vimage[OF _ f_fun])
- next
- 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>"
- let ?g = "\<lambda>x. g' (the_inv_into S f x)"
- show "\<exists>h. simple_function h \<and> (\<forall>x\<in>space M. h x \<le> g x \<and> h x \<noteq> \<omega>) \<and>
- T.simple_integral g' = T.simple_integral (\<lambda>x. h (f x))"
- proof (intro exI[of _ ?g] conjI ballI)
- { fix x assume x: "x \<in> space M"
- then have "the_inv_into S f x \<in> S" using inv_fun by auto
- 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>"
- by auto
- then show "g' (the_inv_into S f x) \<le> g x" "g' (the_inv_into S f x) \<noteq> \<omega>"
- using f_the_inv_into_f[of f S x] x f unfolding bij_betw_def by auto }
- note vimage_vimage_inv[OF f inv_f inv_fun, simp]
- from T.simple_function_vimage[OF g'(1), unfolded space_vimage_algebra, OF inv_fun]
- show "simple_function (\<lambda>x. g' (the_inv_into S f x))"
- unfolding simple_function_def by (simp add: simple_function_def)
- show "T.simple_integral g' = T.simple_integral (\<lambda>x. ?g (f x))"
- using the_inv_into_f_f[OF inj] by (auto intro!: T.simple_integral_cong)
- qed
- qed
-qed
-
-lemma (in measure_space) positive_integral_vimage_inv:
- fixes g :: "'d \<Rightarrow> pextreal" and f :: "'d \<Rightarrow> 'a"
- assumes f: "bij_inv S (space M) f h"
- shows "measure_space.positive_integral (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) g =
- (\<integral>\<^isup>+x. g (h x))"
-proof -
- interpret v: measure_space "vimage_algebra S f" "\<lambda>A. \<mu> (f ` A)"
- using f by (rule measure_space_isomorphic[OF bij_inv_bij_betw(1)])
- show ?thesis
- unfolding positive_integral_vimage[OF f[THEN bij_inv_bij_betw(1)], of "\<lambda>x. g (h x)"]
- using f[unfolded bij_inv_def]
- by (auto intro!: v.positive_integral_cong)
-qed
-
lemma (in measure_space) positive_integral_SUP_approx:
assumes "f \<up> s"
and f: "\<And>i. f i \<in> borel_measurable M"
@@ -1245,6 +1188,23 @@
using positive_integral_isoton[OF `f \<up> u` e(1)[THEN borel_measurable_simple_function]]
unfolding positive_integral_eq_simple_integral[OF e] .
+lemma (in measure_space) positive_integral_vimage:
+ assumes T: "sigma_algebra M'" "T \<in> measurable M M'" and f: "f \<in> borel_measurable M'"
+ shows "measure_space.positive_integral M' (\<lambda>A. \<mu> (T -` A \<inter> space M)) f = (\<integral>\<^isup>+ x. f (T x))"
+ (is "measure_space.positive_integral M' ?nu f = _")
+proof -
+ interpret T: measure_space M' ?nu using T by (rule measure_space_vimage) auto
+ obtain f' where f': "f' \<up> f" "\<And>i. T.simple_function (f' i)"
+ using T.borel_measurable_implies_simple_function_sequence[OF f] by blast
+ then have f: "(\<lambda>i x. f' i (T x)) \<up> (\<lambda>x. f (T x))" "\<And>i. simple_function (\<lambda>x. f' i (T x))"
+ using simple_function_vimage[OF T] unfolding isoton_fun_expand by auto
+ show "T.positive_integral f = (\<integral>\<^isup>+ x. f (T x))"
+ using positive_integral_isoton_simple[OF f]
+ using T.positive_integral_isoton_simple[OF f']
+ unfolding simple_integral_vimage[OF T f'(2)] isoton_def
+ by simp
+qed
+
lemma (in measure_space) positive_integral_linear:
assumes f: "f \<in> borel_measurable M"
and g: "g \<in> borel_measurable M"
@@ -1614,21 +1574,21 @@
thus ?thesis by (simp del: Real_eq_0 add: integral_def)
qed
-lemma (in measure_space) integral_vimage_inv:
- assumes f: "bij_betw f S (space M)"
- 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))"
+lemma (in measure_space) integral_vimage:
+ assumes T: "sigma_algebra M'" "T \<in> measurable M M'"
+ assumes f: "measure_space.integrable M' (\<lambda>A. \<mu> (T -` A \<inter> space M)) f"
+ shows "integrable (\<lambda>x. f (T x))" (is ?P)
+ and "measure_space.integral M' (\<lambda>A. \<mu> (T -` A \<inter> space M)) f = (\<integral>x. f (T x))" (is ?I)
proof -
- interpret v: measure_space "vimage_algebra S f" "\<lambda>A. \<mu> (f ` A)"
- using f by (rule measure_space_isomorphic)
- have "\<And>x. x \<in> space (vimage_algebra S f) \<Longrightarrow> the_inv_into S f (f x) = x"
- using f[unfolded bij_betw_def] by (simp add: the_inv_into_f_f)
- then have *: "v.positive_integral (\<lambda>x. Real (g (the_inv_into S f (f x)))) = v.positive_integral (\<lambda>x. Real (g x))"
- "v.positive_integral (\<lambda>x. Real (- g (the_inv_into S f (f x)))) = v.positive_integral (\<lambda>x. Real (- g x))"
- by (auto intro!: v.positive_integral_cong)
- show ?thesis
- unfolding integral_def v.integral_def
- unfolding positive_integral_vimage[OF f]
- by (simp add: *)
+ interpret T: measure_space M' "\<lambda>A. \<mu> (T -` A \<inter> space M)"
+ using T by (rule measure_space_vimage) auto
+ from measurable_comp[OF T(2), of f borel]
+ have borel: "(\<lambda>x. Real (f x)) \<in> borel_measurable M'" "(\<lambda>x. Real (- f x)) \<in> borel_measurable M'"
+ and "(\<lambda>x. f (T x)) \<in> borel_measurable M"
+ using f unfolding T.integrable_def by (auto simp: comp_def)
+ then show ?P ?I
+ using f unfolding T.integral_def integral_def T.integrable_def integrable_def
+ unfolding borel[THEN positive_integral_vimage[OF T]] by auto
qed
lemma (in measure_space) integral_minus[intro, simp]:
--- a/src/HOL/Probability/Lebesgue_Measure.thy Fri Jan 21 10:43:09 2011 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Tue Jan 25 09:45:45 2011 +0100
@@ -45,6 +45,8 @@
definition lebesgue :: "'a::ordered_euclidean_space algebra" where
"lebesgue = \<lparr> space = UNIV, sets = {A. \<forall>n. (indicator A :: 'a \<Rightarrow> real) integrable_on cube n} \<rparr>"
+definition "lmeasure A = (SUP n. Real (integral (cube n) (indicator A)))"
+
lemma space_lebesgue[simp]: "space lebesgue = UNIV"
unfolding lebesgue_def by simp
@@ -104,8 +106,6 @@
qed (auto intro: LIMSEQ_indicator_UN simp: cube_def)
qed simp
-definition "lmeasure A = (SUP n. Real (integral (cube n) (indicator A)))"
-
interpretation lebesgue: measure_space lebesgue lmeasure
proof
have *: "indicator {} = (\<lambda>x. 0 :: real)" by (simp add: fun_eq_iff)
@@ -736,6 +736,21 @@
show "p2e \<in> ?P \<rightarrow> ?U" "e2p \<in> ?U \<rightarrow> ?P" by (auto simp: e2p_def)
qed auto
+declare restrict_extensional[intro]
+
+lemma e2p_extensional[intro]:"e2p (y::'a::ordered_euclidean_space) \<in> extensional {..<DIM('a)}"
+ unfolding e2p_def by auto
+
+lemma e2p_image_vimage: fixes A::"'a::ordered_euclidean_space set"
+ shows "e2p ` A = p2e -` A \<inter> extensional {..<DIM('a)}"
+proof(rule set_eqI,rule)
+ fix x assume "x \<in> e2p ` A" then guess y unfolding image_iff .. note y=this
+ show "x \<in> p2e -` A \<inter> extensional {..<DIM('a)}"
+ apply safe apply(rule vimageI[OF _ y(1)]) unfolding y p2e_e2p by auto
+next fix x assume "x \<in> p2e -` A \<inter> extensional {..<DIM('a)}"
+ thus "x \<in> e2p ` A" unfolding image_iff apply(rule_tac x="p2e x" in bexI) apply(subst e2p_p2e) by auto
+qed
+
interpretation borel_product: product_sigma_finite "\<lambda>x. borel::real algebra" "\<lambda>x. lmeasure"
by default
@@ -767,6 +782,14 @@
then show "e2p -` A \<inter> space ?E \<in> sets ?E" by simp
qed
+lemma measurable_e2p:
+ "e2p \<in> measurable (borel::'a algebra)
+ (sigma (product_algebra (\<lambda>x. borel :: real algebra) {..<DIM('a::ordered_euclidean_space)}))"
+ using measurable_e2p_on_generator[where 'a='a] unfolding borel_eq_lessThan
+ by (subst sigma_product_algebra_sigma_eq[where S="\<lambda>_ i. {..<real i}"])
+ (auto intro!: measurable_sigma_sigma isotoneI real_arch_lt
+ simp: product_algebra_def)
+
lemma measurable_p2e_on_generator:
"p2e \<in> measurable
(product_algebra
@@ -785,33 +808,13 @@
then show "p2e -` A \<inter> space ?P \<in> sets ?P" by auto
qed
-lemma borel_vimage_algebra_eq:
- defines "F \<equiv> product_algebra (\<lambda>x. \<lparr> space = (UNIV::real set), sets = range lessThan \<rparr>) {..<DIM('a::ordered_euclidean_space)}"
- shows "sigma_algebra.vimage_algebra (borel::'a::ordered_euclidean_space algebra) (space (sigma F)) p2e = sigma F"
- unfolding borel_eq_lessThan
-proof (intro vimage_algebra_sigma)
- let ?E = "\<lparr>space = (UNIV::'a set), sets = range lessThan\<rparr>"
- show "bij_inv (space (sigma F)) (space (sigma ?E)) p2e e2p"
- using bij_inv_p2e_e2p unfolding F_def by simp
- show "sets F \<subseteq> Pow (space F)" "sets ?E \<subseteq> Pow (space ?E)" unfolding F_def
- by (intro product_algebra_sets_into_space) auto
- show "p2e \<in> measurable F ?E"
- "e2p \<in> measurable ?E F"
- unfolding F_def using measurable_p2e_on_generator measurable_e2p_on_generator by auto
-qed
-
-lemma product_borel_eq_vimage:
- "sigma (product_algebra (\<lambda>x. borel) {..<DIM('a::ordered_euclidean_space)}) =
- sigma_algebra.vimage_algebra borel (extensional {..<DIM('a)})
- (p2e:: _ \<Rightarrow> 'a::ordered_euclidean_space)"
- unfolding borel_vimage_algebra_eq[simplified]
- unfolding borel_eq_lessThan
- apply(subst sigma_product_algebra_sigma_eq[where S="\<lambda>i. \<lambda>n. lessThan (real n)"])
- unfolding lessThan_iff
-proof- fix i assume i:"i<DIM('a)"
- show "(\<lambda>n. {..<real n}) \<up> space \<lparr>space = UNIV, sets = range lessThan\<rparr>"
- by(auto intro!:real_arch_lt isotoneI)
-qed auto
+lemma measurable_p2e:
+ "p2e \<in> measurable (sigma (product_algebra (\<lambda>x. borel :: real algebra) {..<DIM('a::ordered_euclidean_space)}))
+ (borel::'a algebra)"
+ using measurable_p2e_on_generator[where 'a='a] unfolding borel_eq_lessThan
+ by (subst sigma_product_algebra_sigma_eq[where S="\<lambda>_ i. {..<real i}"])
+ (auto intro!: measurable_sigma_sigma isotoneI real_arch_lt
+ simp: product_algebra_def)
lemma e2p_Int:"e2p ` A \<inter> e2p ` B = e2p ` (A \<inter> B)" (is "?L = ?R")
apply(rule image_Int[THEN sym])
@@ -834,42 +837,12 @@
unfolding Int_stable_def algebra.select_convs
apply safe unfolding inter_interval by auto
-lemma inj_on_disjoint_family_on: assumes "disjoint_family_on A S" "inj f"
- shows "disjoint_family_on (\<lambda>x. f ` A x) S"
- unfolding disjoint_family_on_def
-proof(rule,rule,rule)
- fix x1 x2 assume x:"x1 \<in> S" "x2 \<in> S" "x1 \<noteq> x2"
- show "f ` A x1 \<inter> f ` A x2 = {}"
- proof(rule ccontr) case goal1
- then obtain z where z:"z \<in> f ` A x1 \<inter> f ` A x2" by auto
- then obtain z1 z2 where z12:"z1 \<in> A x1" "z2 \<in> A x2" "f z1 = z" "f z2 = z" by auto
- hence "z1 = z2" using assms(2) unfolding inj_on_def by blast
- hence "x1 = x2" using z12(1-2) using assms[unfolded disjoint_family_on_def] using x by auto
- thus False using x(3) by auto
- qed
-qed
-
-declare restrict_extensional[intro]
-
-lemma e2p_extensional[intro]:"e2p (y::'a::ordered_euclidean_space) \<in> extensional {..<DIM('a)}"
- unfolding e2p_def by auto
-
-lemma e2p_image_vimage: fixes A::"'a::ordered_euclidean_space set"
- shows "e2p ` A = p2e -` A \<inter> extensional {..<DIM('a)}"
-proof(rule set_eqI,rule)
- fix x assume "x \<in> e2p ` A" then guess y unfolding image_iff .. note y=this
- show "x \<in> p2e -` A \<inter> extensional {..<DIM('a)}"
- apply safe apply(rule vimageI[OF _ y(1)]) unfolding y p2e_e2p by auto
-next fix x assume "x \<in> p2e -` A \<inter> extensional {..<DIM('a)}"
- thus "x \<in> e2p ` A" unfolding image_iff apply(rule_tac x="p2e x" in bexI) apply(subst e2p_p2e) by auto
-qed
-
lemma lmeasure_measure_eq_borel_prod:
fixes A :: "('a::ordered_euclidean_space) set"
assumes "A \<in> sets borel"
shows "lmeasure A = borel_product.product_measure {..<DIM('a)} (e2p ` A :: (nat \<Rightarrow> real) set)"
proof (rule measure_unique_Int_stable[where X=A and A=cube])
- interpret fprod: finite_product_sigma_finite "\<lambda>x. borel" "\<lambda>x. lmeasure" "{..<DIM('a)}" by default auto
+ interpret fprod: finite_product_sigma_finite "\<lambda>x. borel :: real algebra" "\<lambda>x. lmeasure" "{..<DIM('a)}" by default auto
show "Int_stable \<lparr> space = UNIV :: 'a set, sets = range (\<lambda>(a,b). {a..b}) \<rparr>"
(is "Int_stable ?E" ) using Int_stable_cuboids' .
show "borel = sigma ?E" using borel_eq_atLeastAtMost .
@@ -906,64 +879,19 @@
show "measure_space borel lmeasure" by default
show "measure_space borel
(\<lambda>a::'a set. finite_product_sigma_finite.measure (\<lambda>x. borel) (\<lambda>x. lmeasure) {..<DIM('a)} (e2p ` a))"
- apply default unfolding countably_additive_def
- proof safe fix A::"nat \<Rightarrow> 'a set" assume A:"range A \<subseteq> sets borel" "disjoint_family A"
- "(\<Union>i. A i) \<in> sets borel"
- note fprod.ca[unfolded countably_additive_def,rule_format]
- note ca = this[of "\<lambda> n. e2p ` (A n)"]
- show "(\<Sum>\<^isub>\<infinity>n. finite_product_sigma_finite.measure
- (\<lambda>x. borel) (\<lambda>x. lmeasure) {..<DIM('a)} (e2p ` A n)) =
- finite_product_sigma_finite.measure (\<lambda>x. borel)
- (\<lambda>x. lmeasure) {..<DIM('a)} (e2p ` (\<Union>i. A i))" unfolding image_UN
- proof(rule ca) show "range (\<lambda>n. e2p ` A n) \<subseteq> sets
- (sigma (product_algebra (\<lambda>x. borel) {..<DIM('a)}))"
- unfolding product_borel_eq_vimage
- proof case goal1
- then guess y unfolding image_iff .. note y=this(2)
- show ?case unfolding borel.in_vimage_algebra y apply-
- apply(rule_tac x="A y" in bexI,rule e2p_image_vimage)
- using A(1) by auto
- qed
-
- show "disjoint_family (\<lambda>n. e2p ` A n)" apply(rule inj_on_disjoint_family_on)
- using bij_inv_p2e_e2p[THEN bij_inv_bij_betw(2)] using A(2) unfolding bij_betw_def by auto
- show "(\<Union>n. e2p ` A n) \<in> sets (sigma (product_algebra (\<lambda>x. borel) {..<DIM('a)}))"
- unfolding product_borel_eq_vimage borel.in_vimage_algebra
- proof(rule bexI[OF _ A(3)],rule set_eqI,rule)
- fix x assume x:"x \<in> (\<Union>n. e2p ` A n)" hence "p2e x \<in> (\<Union>i. A i)" by auto
- moreover have "x \<in> extensional {..<DIM('a)}"
- using x unfolding extensional_def e2p_def_raw by auto
- ultimately show "x \<in> p2e -` (\<Union>i. A i) \<inter> extensional {..<DIM('a)}" by auto
- next fix x assume x:"x \<in> p2e -` (\<Union>i. A i) \<inter> extensional {..<DIM('a)}"
- hence "p2e x \<in> (\<Union>i. A i)" by auto
- hence "\<exists>n. x \<in> e2p ` A n" apply safe apply(rule_tac x=i in exI)
- unfolding image_iff apply(rule_tac x="p2e x" in bexI)
- apply(subst e2p_p2e) using x by auto
- thus "x \<in> (\<Union>n. e2p ` A n)" by auto
- qed
- qed
- qed auto
+ proof (rule fprod.measure_space_vimage)
+ show "sigma_algebra borel" by default
+ show "(p2e :: (nat \<Rightarrow> real) \<Rightarrow> 'a) \<in> measurable fprod.P borel" by (rule measurable_p2e)
+ fix A :: "'a set" assume "A \<in> sets borel"
+ show "fprod.measure (e2p ` A) = fprod.measure (p2e -` A \<inter> space fprod.P)"
+ by (simp add: e2p_image_vimage)
+ qed
qed
-lemma e2p_p2e'[simp]: fixes x::"'a::ordered_euclidean_space"
- assumes "A \<subseteq> extensional {..<DIM('a)}"
- shows "e2p ` (p2e ` A ::'a set) = A"
- apply(rule set_eqI) unfolding image_iff Bex_def apply safe defer
- apply(rule_tac x="p2e x" in exI,safe) using assms by auto
-
-lemma range_p2e:"range (p2e::_\<Rightarrow>'a::ordered_euclidean_space) = UNIV"
- apply safe defer unfolding image_iff apply(rule_tac x="\<lambda>i. x $$ i" in bexI)
- unfolding p2e_def by auto
-
-lemma p2e_inv_extensional:"(A::'a::ordered_euclidean_space set)
- = p2e ` (p2e -` A \<inter> extensional {..<DIM('a)})"
- unfolding p2e_def_raw apply safe unfolding image_iff
-proof- fix x assume "x\<in>A"
- let ?y = "\<lambda>i. if i<DIM('a) then x$$i else undefined"
- have *:"Chi ?y = x" apply(subst euclidean_eq) by auto
- show "\<exists>xa\<in>Chi -` A \<inter> extensional {..<DIM('a)}. x = Chi xa" apply(rule_tac x="?y" in bexI)
- apply(subst euclidean_eq) unfolding extensional_def using `x\<in>A` by(auto simp: *)
-qed
+lemma range_e2p:"range (e2p::'a::ordered_euclidean_space \<Rightarrow> _) = extensional {..<DIM('a)}"
+ unfolding e2p_def_raw
+ apply auto
+ by (rule_tac x="\<chi>\<chi> i. x i" in image_eqI) (auto simp: fun_eq_iff extensional_def)
lemma borel_fubini_positiv_integral:
fixes f :: "'a::ordered_euclidean_space \<Rightarrow> pextreal"
@@ -972,22 +900,27 @@
borel_product.product_positive_integral {..<DIM('a)} (f \<circ> p2e)"
proof- def U \<equiv> "extensional {..<DIM('a)} :: (nat \<Rightarrow> real) set"
interpret fprod: finite_product_sigma_finite "\<lambda>x. borel" "\<lambda>x. lmeasure" "{..<DIM('a)}" by default auto
- have *:"sigma_algebra.vimage_algebra borel U (p2e:: _ \<Rightarrow> 'a)
- = sigma (product_algebra (\<lambda>x. borel) {..<DIM('a)})"
- unfolding U_def product_borel_eq_vimage[symmetric] ..
show ?thesis
- unfolding borel.positive_integral_vimage[unfolded space_borel, OF bij_inv_p2e_e2p[THEN bij_inv_bij_betw(1)]]
- apply(subst fprod.positive_integral_cong_measure[THEN sym, of "\<lambda>A. lmeasure (p2e ` A)"])
- unfolding U_def[symmetric] *[THEN sym] o_def
- proof- fix A assume A:"A \<in> sets (sigma_algebra.vimage_algebra borel U (p2e ::_ \<Rightarrow> 'a))"
- hence *:"A \<subseteq> extensional {..<DIM('a)}" unfolding U_def by auto
- from A guess B unfolding borel.in_vimage_algebra U_def ..
- then have "(p2e ` A::'a set) \<in> sets borel"
- by (simp add: p2e_inv_extensional[of B, symmetric])
- from lmeasure_measure_eq_borel_prod[OF this] show "lmeasure (p2e ` A::'a set) =
- finite_product_sigma_finite.measure (\<lambda>x. borel) (\<lambda>x. lmeasure) {..<DIM('a)} A"
- unfolding e2p_p2e'[OF *] .
- qed auto
+ proof (subst borel.positive_integral_vimage[symmetric, of _ "e2p :: 'a \<Rightarrow> _" "(\<lambda>x. f (p2e x))", unfolded p2e_e2p])
+ show "(e2p :: 'a \<Rightarrow> _) \<in> measurable borel fprod.P" by (rule measurable_e2p)
+ show "sigma_algebra fprod.P" by default
+ from measurable_comp[OF measurable_p2e f]
+ show "(\<lambda>x. f (p2e x)) \<in> borel_measurable fprod.P" by (simp add: comp_def)
+ let "?L A" = "lmeasure ((e2p::'a \<Rightarrow> (nat \<Rightarrow> real)) -` A \<inter> space borel)"
+ show "measure_space.positive_integral fprod.P ?L (\<lambda>x. f (p2e x)) =
+ fprod.positive_integral (f \<circ> p2e)"
+ unfolding comp_def
+ proof (rule fprod.positive_integral_cong_measure)
+ fix A :: "(nat \<Rightarrow> real) set" assume "A \<in> sets fprod.P"
+ then have A: "(e2p::'a \<Rightarrow> (nat \<Rightarrow> real)) -` A \<inter> space borel \<in> sets borel"
+ by (rule measurable_sets[OF measurable_e2p])
+ have [simp]: "A \<inter> extensional {..<DIM('a)} = A"
+ using `A \<in> sets fprod.P`[THEN fprod.sets_into_space] by auto
+ show "?L A = fprod.measure A"
+ unfolding lmeasure_measure_eq_borel_prod[OF A]
+ by (simp add: range_e2p)
+ qed
+ qed
qed
lemma borel_fubini:
--- a/src/HOL/Probability/Measure.thy Fri Jan 21 10:43:09 2011 +0100
+++ b/src/HOL/Probability/Measure.thy Tue Jan 25 09:45:45 2011 +0100
@@ -525,6 +525,15 @@
qed
qed
+lemma True
+proof
+ fix x a b :: nat
+ have "\<And>x a b :: int. x dvd a \<Longrightarrow> x dvd (a + b) \<Longrightarrow> x dvd b"
+ by (metis dvd_mult_div_cancel zadd_commute zdvd_reduce)
+ then have "x dvd a \<Longrightarrow> x dvd (a + b) \<Longrightarrow> x dvd b"
+ unfolding zdvd_int[of x] zadd_int[symmetric] .
+qed
+
lemma measure_unique_Int_stable:
fixes M E :: "'a algebra" and A :: "nat \<Rightarrow> 'a set"
assumes "Int_stable E" "M = sigma E"
@@ -608,45 +617,6 @@
ultimately show ?thesis by (simp add: isoton_def)
qed
-section "Isomorphisms between measure spaces"
-
-lemma (in measure_space) measure_space_isomorphic:
- fixes f :: "'c \<Rightarrow> 'a"
- assumes "bij_betw f S (space M)"
- shows "measure_space (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A))"
- (is "measure_space ?T ?\<mu>")
-proof -
- have "f \<in> S \<rightarrow> space M" using assms unfolding bij_betw_def by auto
- then interpret T: sigma_algebra ?T by (rule sigma_algebra_vimage)
- show ?thesis
- proof
- show "\<mu> (f`{}) = 0" by simp
- show "countably_additive ?T (\<lambda>A. \<mu> (f ` A))"
- proof (unfold countably_additive_def, intro allI impI)
- fix A :: "nat \<Rightarrow> 'c set" assume "range A \<subseteq> sets ?T" "disjoint_family A"
- then have "\<forall>i. \<exists>F'. F' \<in> sets M \<and> A i = f -` F' \<inter> S"
- by (auto simp: image_iff image_subset_iff Bex_def vimage_algebra_def)
- 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
- then have [simp]: "\<And>i. f ` (A i) = F i"
- using sets_into_space assms
- by (force intro!: image_vimage_inter_eq[where T="space M"] simp: bij_betw_def)
- have "disjoint_family F"
- proof (intro disjoint_family_on_bisimulation[OF `disjoint_family A`])
- fix n m assume "A n \<inter> A m = {}"
- then have "f -` (F n \<inter> F m) \<inter> S = {}" unfolding A by auto
- moreover
- have "F n \<in> sets M" "F m \<in> sets M" using F by auto
- then have "f`S = space M" "F n \<inter> F m \<subseteq> space M"
- using sets_into_space assms by (auto simp: bij_betw_def)
- note image_vimage_inter_eq[OF this, symmetric]
- ultimately show "F n \<inter> F m = {}" by simp
- qed
- with F show "(\<Sum>\<^isub>\<infinity> i. \<mu> (f ` A i)) = \<mu> (f ` (\<Union>i. A i))"
- by (auto simp add: image_UN intro!: measure_countably_additive)
- qed
- qed
-qed
-
section "@{text \<mu>}-null sets"
abbreviation (in measure_space) "null_sets \<equiv> {N\<in>sets M. \<mu> N = 0}"
@@ -803,23 +773,17 @@
lemma (in measure_space) AE_conjI:
assumes AE_P: "AE x. P x" and AE_Q: "AE x. Q x"
shows "AE x. P x \<and> Q x"
-proof -
- from AE_P obtain A where P: "{x\<in>space M. \<not> P x} \<subseteq> A"
- and A: "A \<in> sets M" "\<mu> A = 0"
- by (auto elim!: AE_E)
-
- from AE_Q obtain B where Q: "{x\<in>space M. \<not> Q x} \<subseteq> B"
- and B: "B \<in> sets M" "\<mu> B = 0"
- by (auto elim!: AE_E)
+ apply (rule AE_mp[OF AE_P])
+ apply (rule AE_mp[OF AE_Q])
+ by simp
- show ?thesis
- proof (intro AE_I)
- show "A \<union> B \<in> sets M" "\<mu> (A \<union> B) = 0" using A B
- using measure_subadditive[of A B] by auto
- show "{x\<in>space M. \<not> (P x \<and> Q x)} \<subseteq> A \<union> B"
- using P Q by auto
- qed
-qed
+lemma (in measure_space) AE_conj_iff[simp]:
+ shows "(AE x. P x \<and> Q x) \<longleftrightarrow> (AE x. P x) \<and> (AE x. Q x)"
+proof (intro conjI iffI AE_conjI)
+ assume *: "AE x. P x \<and> Q x"
+ from * show "AE x. P x" by (rule AE_mp) auto
+ from * show "AE x. Q x" by (rule AE_mp) auto
+qed auto
lemma (in measure_space) AE_E2:
assumes "AE x. P x" "{x\<in>space M. P x} \<in> sets M"
@@ -845,14 +809,6 @@
by (rule AE_mp[OF AE_space]) auto
qed
-lemma (in measure_space) AE_conj_iff[simp]:
- shows "(AE x. P x \<and> Q x) \<longleftrightarrow> (AE x. P x) \<and> (AE x. Q x)"
-proof (intro conjI iffI AE_conjI)
- assume *: "AE x. P x \<and> Q x"
- from * show "AE x. P x" by (rule AE_mp) auto
- from * show "AE x. Q x" by (rule AE_mp) auto
-qed auto
-
lemma (in measure_space) all_AE_countable:
"(\<forall>i::'i::countable. AE x. P i x) \<longleftrightarrow> (AE x. \<forall>i. P i x)"
proof
@@ -893,27 +849,28 @@
lemma (in measure_space) measure_space_vimage:
fixes M' :: "'b algebra"
- assumes "f \<in> measurable M M'"
- and "sigma_algebra M'"
- shows "measure_space M' (\<lambda>A. \<mu> (f -` A \<inter> space M))" (is "measure_space M' ?T")
+ assumes T: "sigma_algebra M'" "T \<in> measurable M M'"
+ and \<nu>: "\<And>A. A \<in> sets M' \<Longrightarrow> \<nu> A = \<mu> (T -` A \<inter> space M)"
+ shows "measure_space M' \<nu>"
proof -
interpret M': sigma_algebra M' by fact
-
show ?thesis
proof
- show "?T {} = 0" by simp
+ show "\<nu> {} = 0" using \<nu>[of "{}"] by simp
- show "countably_additive M' ?T"
- proof (unfold countably_additive_def, safe)
+ show "countably_additive M' \<nu>"
+ proof (intro countably_additive_def[THEN iffD2] allI impI)
fix A :: "nat \<Rightarrow> 'b set" assume "range A \<subseteq> sets M'" "disjoint_family A"
- hence *: "\<And>i. f -` (A i) \<inter> space M \<in> sets M"
- using `f \<in> measurable M M'` by (auto simp: measurable_def)
- moreover have "(\<Union>i. f -` A i \<inter> space M) \<in> sets M"
+ then have A: "\<And>i. A i \<in> sets M'" "(\<Union>i. A i) \<in> sets M'" by auto
+ then have *: "range (\<lambda>i. T -` (A i) \<inter> space M) \<subseteq> sets M"
+ using `T \<in> measurable M M'` by (auto simp: measurable_def)
+ moreover have "(\<Union>i. T -` A i \<inter> space M) \<in> sets M"
using * by blast
- moreover have **: "disjoint_family (\<lambda>i. f -` A i \<inter> space M)"
+ moreover have **: "disjoint_family (\<lambda>i. T -` A i \<inter> space M)"
using `disjoint_family A` by (auto simp: disjoint_family_on_def)
- ultimately show "(\<Sum>\<^isub>\<infinity> i. ?T (A i)) = ?T (\<Union>i. A i)"
- using measure_countably_additive[OF _ **] by (auto simp: comp_def vimage_UN)
+ ultimately show "(\<Sum>\<^isub>\<infinity> i. \<nu> (A i)) = \<nu> (\<Union>i. A i)"
+ using measure_countably_additive[OF _ **] A
+ by (auto simp: comp_def vimage_UN \<nu>)
qed
qed
qed
@@ -1020,29 +977,6 @@
qed force+
qed
-lemma (in sigma_finite_measure) sigma_finite_measure_isomorphic:
- assumes f: "bij_betw f S (space M)"
- shows "sigma_finite_measure (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A))"
-proof -
- interpret M: measure_space "vimage_algebra S f" "\<lambda>A. \<mu> (f ` A)"
- using f by (rule measure_space_isomorphic)
- show ?thesis
- proof default
- from sigma_finite guess A::"nat \<Rightarrow> 'a set" .. note A = this
- 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>)"
- proof (intro exI conjI)
- show "(\<Union>i::nat. f -` A i \<inter> S) = space (vimage_algebra S f)"
- using A f[THEN bij_betw_imp_funcset] by (auto simp: vimage_UN[symmetric])
- show "range (\<lambda>i. f -` A i \<inter> S) \<subseteq> sets (vimage_algebra S f)"
- using A by (auto simp: vimage_algebra_def)
- have "\<And>i. f ` (f -` A i \<inter> S) = A i"
- using f A sets_into_space
- by (intro image_vimage_inter_eq) (auto simp: bij_betw_def)
- then show "\<forall>i. \<mu> (f ` (f -` A i \<inter> S)) \<noteq> \<omega>" using A by simp
- qed
- qed
-qed
-
section "Real measure values"
lemma (in measure_space) real_measure_Union:
--- a/src/HOL/Probability/Probability_Space.thy Fri Jan 21 10:43:09 2011 +0100
+++ b/src/HOL/Probability/Probability_Space.thy Tue Jan 25 09:45:45 2011 +0100
@@ -195,8 +195,8 @@
assumes "random_variable S X"
shows "prob_space S (distribution X)"
proof -
- interpret S: measure_space S "distribution X"
- using measure_space_vimage[of X S] assms unfolding distribution_def by simp
+ interpret S: measure_space S "distribution X" unfolding distribution_def
+ using assms by (intro measure_space_vimage) auto
show ?thesis
proof
have "X -` space S \<inter> space M = space M"
--- a/src/HOL/Probability/Product_Measure.thy Fri Jan 21 10:43:09 2011 +0100
+++ b/src/HOL/Probability/Product_Measure.thy Tue Jan 25 09:45:45 2011 +0100
@@ -523,22 +523,6 @@
unfolding * by (rule measurable_comp)
qed
-lemma (in pair_sigma_algebra) pair_sigma_algebra_swap:
- "sigma (pair_algebra M2 M1) = (vimage_algebra (space M2 \<times> space M1) (\<lambda>(x, y). (y, x)))"
- unfolding vimage_algebra_def
- apply (simp add: sets_sigma)
- apply (subst sigma_sets_vimage[symmetric])
- apply (fastsimp simp: pair_algebra_def)
- using M1.sets_into_space M2.sets_into_space apply (fastsimp simp: pair_algebra_def)
-proof -
- have "(\<lambda>X. (\<lambda>(x, y). (y, x)) -` X \<inter> space M2 \<times> space M1) ` sets E
- = sets (pair_algebra M2 M1)" (is "?S = _")
- by (rule pair_algebra_swap)
- then show "sigma (pair_algebra M2 M1) = \<lparr>space = space M2 \<times> space M1,
- sets = sigma_sets (space M2 \<times> space M1) ?S\<rparr>"
- by (simp add: pair_algebra_def sigma_def)
-qed
-
definition (in pair_sigma_finite)
"pair_measure A = M1.positive_integral (\<lambda>x.
M2.positive_integral (\<lambda>y. indicator A (x, y)))"
@@ -644,6 +628,17 @@
qed
qed
+lemma (in pair_sigma_algebra) sets_swap:
+ assumes "A \<in> sets P"
+ shows "(\<lambda>(x, y). (y, x)) -` A \<inter> space (sigma (pair_algebra M2 M1)) \<in> sets (sigma (pair_algebra M2 M1))"
+ (is "_ -` A \<inter> space ?Q \<in> sets ?Q")
+proof -
+ have *: "(\<lambda>(x, y). (y, x)) -` A \<inter> space ?Q = (\<lambda>(x, y). (y, x)) ` A"
+ using `A \<in> sets P` sets_into_space by (auto simp: space_pair_algebra)
+ show ?thesis
+ unfolding * using assms by (rule sets_pair_sigma_algebra_swap)
+qed
+
lemma (in pair_sigma_finite) pair_measure_alt2:
assumes "A \<in> sets P"
shows "pair_measure A = M2.positive_integral (\<lambda>y. \<mu>1 ((\<lambda>x. (x, y)) -` A))"
@@ -656,29 +651,20 @@
show "range F \<subseteq> sets E" "F \<up> space E" "\<And>i. pair_measure (F i) \<noteq> \<omega>"
using F by auto
show "measure_space P pair_measure" by default
- next
+ interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
+ have P: "sigma_algebra P" by default
show "measure_space P ?\<nu>"
- proof
- show "?\<nu> {} = 0" by auto
- show "countably_additive P ?\<nu>"
- unfolding countably_additive_def
- proof (intro allI impI)
- fix F :: "nat \<Rightarrow> ('a \<times> 'b) set"
- assume F: "range F \<subseteq> sets P" "disjoint_family F"
- from F have *: "\<And>i. F i \<in> sets P" "(\<Union>i. F i) \<in> sets P" by auto
- moreover from F have "\<And>i. (\<lambda>y. \<mu>1 ((\<lambda>x. (x, y)) -` F i)) \<in> borel_measurable M2"
- by (intro measure_cut_measurable_snd) auto
- moreover have "\<And>y. disjoint_family (\<lambda>i. (\<lambda>x. (x, y)) -` F i)"
- by (intro disjoint_family_on_bisimulation[OF F(2)]) auto
- moreover have "\<And>y. y \<in> space M2 \<Longrightarrow> range (\<lambda>i. (\<lambda>x. (x, y)) -` F i) \<subseteq> sets M1"
- using F by (auto intro!: measurable_cut_snd)
- ultimately show "(\<Sum>\<^isub>\<infinity>n. ?\<nu> (F n)) = ?\<nu> (\<Union>i. F i)"
- by (simp add: vimage_UN M2.positive_integral_psuminf[symmetric]
- M1.measure_countably_additive
- cong: M2.positive_integral_cong)
- qed
+ apply (rule Q.measure_space_vimage[OF P])
+ apply (rule Q.pair_sigma_algebra_swap_measurable)
+ proof -
+ fix A assume "A \<in> sets P"
+ from sets_swap[OF this]
+ show "M2.positive_integral (\<lambda>y. \<mu>1 ((\<lambda>x. (x, y)) -` A)) =
+ Q.pair_measure ((\<lambda>(x, y). (y, x)) -` A \<inter> space Q.P)"
+ using sets_into_space[OF `A \<in> sets P`]
+ by (auto simp add: Q.pair_measure_alt space_pair_algebra
+ intro!: M2.positive_integral_cong arg_cong[where f=\<mu>1])
qed
- next
fix X assume "X \<in> sets E"
then obtain A B where X: "X = A \<times> B" and AB: "A \<in> sets M1" "B \<in> sets M2"
unfolding pair_algebra_def by auto
@@ -802,31 +788,40 @@
unfolding F_SUPR by simp
qed
+lemma (in pair_sigma_finite) positive_integral_product_swap:
+ assumes f: "f \<in> borel_measurable P"
+ shows "measure_space.positive_integral
+ (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))) =
+ positive_integral f"
+proof -
+ interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
+ have P: "sigma_algebra P" by default
+ show ?thesis
+ unfolding Q.positive_integral_vimage[OF P Q.pair_sigma_algebra_swap_measurable f, symmetric]
+ proof (rule positive_integral_cong_measure)
+ fix A
+ assume A: "A \<in> sets P"
+ from Q.pair_sigma_algebra_swap_measurable[THEN measurable_sets, OF this] this sets_into_space[OF this]
+ show "Q.pair_measure ((\<lambda>(x, y). (y, x)) -` A \<inter> space Q.P) = pair_measure A"
+ by (auto intro!: M1.positive_integral_cong arg_cong[where f=\<mu>2]
+ simp: pair_measure_alt Q.pair_measure_alt2 space_pair_algebra)
+ qed
+qed
+
lemma (in pair_sigma_finite) positive_integral_snd_measurable:
assumes f: "f \<in> borel_measurable P"
shows "M2.positive_integral (\<lambda>y. M1.positive_integral (\<lambda>x. f (x, y))) =
positive_integral f"
proof -
interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
- have s: "\<And>x y. (case (x, y) of (x, y) \<Rightarrow> f (y, x)) = f (y, x)" by simp
- 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)
- have bij: "bij_betw (\<lambda>(x, y). (y, x)) (space M2 \<times> space M1) (space P)"
- by (auto intro!: inj_onI simp: space_pair_algebra bij_betw_def)
note pair_sigma_algebra_measurable[OF f]
from Q.positive_integral_fst_measurable[OF this]
have "M2.positive_integral (\<lambda>y. M1.positive_integral (\<lambda>x. f (x, y))) =
Q.positive_integral (\<lambda>(x, y). f (y, x))"
by simp
- also have "\<dots> = positive_integral f"
- unfolding positive_integral_vimage[OF bij, of f] t
- unfolding pair_sigma_algebra_swap[symmetric]
- proof (rule Q.positive_integral_cong_measure[symmetric])
- fix A assume "A \<in> sets Q.P"
- from this Q.sets_pair_sigma_algebra_swap[OF this]
- show "pair_measure ((\<lambda>(x, y). (y, x)) ` A) = Q.pair_measure A"
- by (auto intro!: M1.positive_integral_cong arg_cong[where f=\<mu>2]
- simp: pair_measure_alt Q.pair_measure_alt2)
- qed
+ also have "Q.positive_integral (\<lambda>(x, y). f (y, x)) = positive_integral f"
+ unfolding positive_integral_product_swap[OF f, symmetric]
+ by (auto intro!: Q.positive_integral_cong)
finally show ?thesis .
qed
@@ -863,28 +858,6 @@
qed
qed
-lemma (in pair_sigma_finite) positive_integral_product_swap:
- "measure_space.positive_integral
- (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) f =
- positive_integral (\<lambda>(x,y). f (y,x))"
-proof -
- interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
- have t: "(\<lambda>y. case case y of (y, x) \<Rightarrow> (x, y) of (x, y) \<Rightarrow> f (y, x)) = f"
- by (auto simp: fun_eq_iff)
- have bij: "bij_betw (\<lambda>(x, y). (y, x)) (space M2 \<times> space M1) (space P)"
- by (auto intro!: inj_onI simp: space_pair_algebra bij_betw_def)
- show ?thesis
- unfolding positive_integral_vimage[OF bij, of "\<lambda>(y,x). f (x,y)"]
- unfolding pair_sigma_algebra_swap[symmetric] t
- proof (rule Q.positive_integral_cong_measure[symmetric])
- fix A assume "A \<in> sets Q.P"
- from this Q.sets_pair_sigma_algebra_swap[OF this]
- show "pair_measure ((\<lambda>(x, y). (y, x)) ` A) = Q.pair_measure A"
- by (auto intro!: M1.positive_integral_cong arg_cong[where f=\<mu>2]
- simp: pair_measure_alt Q.pair_measure_alt2)
- qed
-qed
-
lemma (in pair_sigma_algebra) measurable_product_swap:
"f \<in> measurable (sigma (pair_algebra M2 M1)) M \<longleftrightarrow> (\<lambda>(x,y). f (y,x)) \<in> measurable P M"
proof -
@@ -895,27 +868,42 @@
qed
lemma (in pair_sigma_finite) integrable_product_swap:
- "measure_space.integrable
- (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) f \<longleftrightarrow>
- integrable (\<lambda>(x,y). f (y,x))"
+ assumes "integrable f"
+ shows "measure_space.integrable
+ (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) (\<lambda>(x,y). f (y,x))"
proof -
interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
- show ?thesis
- unfolding Q.integrable_def integrable_def
- unfolding positive_integral_product_swap
- unfolding measurable_product_swap
- by (simp add: case_prod_distrib)
+ have *: "(\<lambda>(x,y). f (y,x)) = (\<lambda>x. f (case x of (x,y)\<Rightarrow>(y,x)))" by (auto simp: fun_eq_iff)
+ show ?thesis unfolding *
+ using assms unfolding Q.integrable_def integrable_def
+ apply (subst (1 2) positive_integral_product_swap)
+ using `integrable f` unfolding integrable_def
+ by (auto simp: *[symmetric] Q.measurable_product_swap[symmetric])
+qed
+
+lemma (in pair_sigma_finite) integrable_product_swap_iff:
+ "measure_space.integrable
+ (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) (\<lambda>(x,y). f (y,x)) \<longleftrightarrow>
+ integrable f"
+proof -
+ interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
+ from Q.integrable_product_swap[of "\<lambda>(x,y). f (y,x)"] integrable_product_swap[of f]
+ show ?thesis by auto
qed
lemma (in pair_sigma_finite) integral_product_swap:
- "measure_space.integral
- (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) f =
- integral (\<lambda>(x,y). f (y,x))"
+ assumes "integrable f"
+ shows "measure_space.integral
+ (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) (\<lambda>(x,y). f (y,x)) =
+ integral f"
proof -
interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
+ have *: "(\<lambda>(x,y). f (y,x)) = (\<lambda>x. f (case x of (x,y)\<Rightarrow>(y,x)))" by (auto simp: fun_eq_iff)
show ?thesis
- unfolding integral_def Q.integral_def positive_integral_product_swap
- by (simp add: case_prod_distrib)
+ unfolding integral_def Q.integral_def *
+ apply (subst (1 2) positive_integral_product_swap)
+ using `integrable f` unfolding integrable_def
+ by (auto simp: *[symmetric] Q.measurable_product_swap[symmetric])
qed
lemma (in pair_sigma_finite) integrable_fst_measurable:
@@ -988,10 +976,10 @@
proof -
interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
have Q_int: "Q.integrable (\<lambda>(x, y). f (y, x))"
- using f unfolding integrable_product_swap by simp
+ using f unfolding integrable_product_swap_iff .
show ?INT
using Q.integrable_fst_measurable(2)[OF Q_int]
- unfolding integral_product_swap by simp
+ using integral_product_swap[OF f] by simp
show ?AE
using Q.integrable_fst_measurable(1)[OF Q_int]
by simp
@@ -1355,18 +1343,6 @@
pair_algebra_sets_into_space product_algebra_sets_into_space)
auto
-lemma (in product_sigma_algebra) product_product_vimage_algebra:
- assumes [simp]: "I \<inter> J = {}"
- shows "sigma_algebra.vimage_algebra
- (sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J))))
- (space (sigma (product_algebra M (I \<union> J)))) (\<lambda>x. ((\<lambda>i\<in>I. x i), (\<lambda>i\<in>J. x i))) =
- sigma (product_algebra M (I \<union> J))"
- unfolding sigma_pair_algebra_sigma_eq using sets_into_space
- by (intro vimage_algebra_sigma[OF bij_inv_restrict_merge]
- pair_algebra_sets_into_space product_algebra_sets_into_space
- measurable_merge_on_generating measurable_restrict_on_generating)
- auto
-
lemma (in product_sigma_algebra) pair_product_product_vimage_algebra:
assumes [simp]: "I \<inter> J = {}"
shows "sigma_algebra.vimage_algebra (sigma (product_algebra M (I \<union> J)))
@@ -1378,24 +1354,6 @@
measurable_merge_on_generating measurable_restrict_on_generating)
auto
-lemma (in product_sigma_algebra) pair_product_singleton_vimage_algebra:
- assumes [simp]: "i \<notin> I"
- shows "sigma_algebra.vimage_algebra (sigma (pair_algebra (sigma (product_algebra M I)) (M i)))
- (space (sigma (product_algebra M (insert i I)))) (\<lambda>x. (restrict x I, x i)) =
- (sigma (product_algebra M (insert i I)))"
- unfolding sigma_pair_algebra_product_singleton using sets_into_space
- by (intro vimage_algebra_sigma[OF bij_inv_restrict_insert]
- pair_algebra_sets_into_space product_algebra_sets_into_space
- measurable_merge_singleton_on_generating measurable_restrict_singleton_on_generating)
- auto
-
-lemma (in product_sigma_algebra) singleton_vimage_algebra:
- "sigma_algebra.vimage_algebra (sigma (product_algebra M {i})) (space (M i)) (\<lambda>x. \<lambda>j\<in>{i}. x) = M i"
- using sets_into_space
- by (intro vimage_algebra_sigma[of "M i", unfolded M.sigma_eq, OF bij_inv_singleton[symmetric]]
- product_algebra_sets_into_space measurable_singleton_on_generator measurable_component_on_generator)
- auto
-
lemma (in product_sigma_algebra) measurable_restrict_iff:
assumes IJ[simp]: "I \<inter> J = {}"
shows "f \<in> measurable (sigma (pair_algebra
@@ -1430,6 +1388,13 @@
then show "?f \<in> measurable ?P M'" by (simp add: comp_def)
qed
+lemma (in product_sigma_algebra) singleton_vimage_algebra:
+ "sigma_algebra.vimage_algebra (sigma (product_algebra M {i})) (space (M i)) (\<lambda>x. \<lambda>j\<in>{i}. x) = M i"
+ using sets_into_space
+ by (intro vimage_algebra_sigma[of "M i", unfolded M.sigma_eq, OF bij_inv_singleton[symmetric]]
+ product_algebra_sets_into_space measurable_singleton_on_generator measurable_component_on_generator)
+ auto
+
lemma (in product_sigma_algebra) measurable_component_singleton:
"(\<lambda>x. f (x i)) \<in> measurable (sigma (product_algebra M {i})) M' \<longleftrightarrow>
f \<in> measurable (M i) M'"
@@ -1479,6 +1444,55 @@
using sets_into_space unfolding measurable_component_singleton[symmetric]
by (auto intro!: measurable_cong arg_cong[where f=f] simp: fun_eq_iff extensional_def)
+
+lemma (in pair_sigma_algebra) measurable_pair_split:
+ assumes "sigma_algebra M1'" "sigma_algebra M2'"
+ assumes f: "f \<in> measurable M1 M1'" and g: "g \<in> measurable M2 M2'"
+ shows "(\<lambda>(x, y). (f x, g y)) \<in> measurable P (sigma (pair_algebra M1' M2'))"
+proof (rule measurable_sigma)
+ interpret M1': sigma_algebra M1' by fact
+ interpret M2': sigma_algebra M2' by fact
+ interpret Q: pair_sigma_algebra M1' M2' by default
+ show "sets Q.E \<subseteq> Pow (space Q.E)"
+ using M1'.sets_into_space M2'.sets_into_space by (auto simp: pair_algebra_def)
+ show "(\<lambda>(x, y). (f x, g y)) \<in> space P \<rightarrow> space Q.E"
+ using f g unfolding measurable_def pair_algebra_def by auto
+ fix A assume "A \<in> sets Q.E"
+ then obtain X Y where A: "A = X \<times> Y" "X \<in> sets M1'" "Y \<in> sets M2'"
+ unfolding pair_algebra_def by auto
+ then have *: "(\<lambda>(x, y). (f x, g y)) -` A \<inter> space P =
+ (f -` X \<inter> space M1) \<times> (g -` Y \<inter> space M2)"
+ by (auto simp: pair_algebra_def)
+ then show "(\<lambda>(x, y). (f x, g y)) -` A \<inter> space P \<in> sets P"
+ using f g A unfolding measurable_def *
+ by (auto intro!: pair_algebraI in_sigma)
+qed
+
+lemma (in product_sigma_algebra) measurable_add_dim:
+ assumes "i \<notin> I" "finite I"
+ shows "(\<lambda>(f, y). f(i := y)) \<in> measurable (sigma (pair_algebra (sigma (product_algebra M I)) (M i)))
+ (sigma (product_algebra M (insert i I)))"
+proof (subst measurable_cong)
+ interpret I: finite_product_sigma_algebra M I by default fact
+ interpret i: finite_product_sigma_algebra M "{i}" by default auto
+ interpret Ii: pair_sigma_algebra I.P "M i" by default
+ interpret Ii': pair_sigma_algebra I.P i.P by default
+ have disj: "I \<inter> {i} = {}" using `i \<notin> I` by auto
+ have "(\<lambda>(x, y). (id x, \<lambda>_\<in>{i}. y)) \<in> measurable Ii.P Ii'.P"
+ proof (intro Ii.measurable_pair_split I.measurable_ident)
+ show "(\<lambda>y. \<lambda>_\<in>{i}. y) \<in> measurable (M i) i.P"
+ apply (rule measurable_singleton[THEN iffD1])
+ using i.measurable_ident unfolding id_def .
+ qed default
+ from measurable_comp[OF this measurable_merge[OF disj]]
+ show "(\<lambda>(x, y). merge I x {i} y) \<circ> (\<lambda>(x, y). (id x, \<lambda>_\<in>{i}. y))
+ \<in> measurable (sigma (pair_algebra I.P (M i))) (sigma (product_algebra M (insert i I)))"
+ (is "?f \<in> _") by simp
+ fix x assume "x \<in> space Ii.P"
+ with assms show "(\<lambda>(f, y). f(i := y)) x = ?f x"
+ by (cases x) (simp add: merge_def fun_eq_iff pair_algebra_def extensional_def)
+qed
+
locale product_sigma_finite =
fixes M :: "'i \<Rightarrow> 'a algebra" and \<mu> :: "'i \<Rightarrow> 'a set \<Rightarrow> pextreal"
assumes sigma_finite_measures: "\<And>i. sigma_finite_measure (M i) (\<mu> i)"
@@ -1549,29 +1563,24 @@
interpret I: sigma_finite_measure P \<nu> by fact
interpret P: pair_sigma_finite P \<nu> "M i" "\<mu> i" ..
- let ?h = "\<lambda>x. (restrict x I, x i)"
- let ?\<nu> = "\<lambda>A. P.pair_measure (?h ` A)"
+ let ?h = "(\<lambda>(f, y). f(i := y))"
+ let ?\<nu> = "\<lambda>A. P.pair_measure (?h -` A \<inter> space P.P)"
+ have I': "sigma_algebra I'.P" by default
interpret I': measure_space "sigma (product_algebra M (insert i I))" ?\<nu>
- apply (subst pair_product_singleton_vimage_algebra[OF `i \<notin> I`, symmetric])
- apply (intro P.measure_space_isomorphic bij_inv_bij_betw)
- unfolding sigma_pair_algebra_product_singleton
- by (rule bij_inv_restrict_insert[OF `i \<notin> I`])
+ apply (rule P.measure_space_vimage[OF I'])
+ apply (rule measurable_add_dim[OF `i \<notin> I` `finite I`])
+ by simp
show ?case
proof (intro exI[of _ ?\<nu>] conjI ballI)
{ fix A assume A: "A \<in> (\<Pi> i\<in>insert i I. sets (M i))"
- moreover then have "A \<in> (\<Pi> i\<in>I. sets (M i))" by auto
- moreover have "(\<lambda>x. (restrict x I, x i)) ` Pi\<^isub>E (insert i I) A = Pi\<^isub>E I A \<times> A i"
- using `i \<notin> I`
- apply auto
- apply (rule_tac x="a(i:=b)" in image_eqI)
- apply (auto simp: extensional_def fun_eq_iff)
- done
- ultimately show "?\<nu> (Pi\<^isub>E (insert i I) A) = (\<Prod>i\<in>insert i I. \<mu> i (A i))"
- apply simp
+ then have *: "?h -` Pi\<^isub>E (insert i I) A \<inter> space P.P = Pi\<^isub>E I A \<times> A i"
+ using `i \<notin> I` M.sets_into_space by (auto simp: pair_algebra_def) blast
+ show "?\<nu> (Pi\<^isub>E (insert i I) A) = (\<Prod>i\<in>insert i I. \<mu> i (A i))"
+ unfolding * using A
apply (subst P.pair_measure_times)
- apply fastsimp
- apply fastsimp
- using `i \<notin> I` `finite I` prod[of A] by (auto simp: ac_simps) }
+ using A apply fastsimp
+ using A apply fastsimp
+ using `i \<notin> I` `finite I` prod[of A] A by (auto simp: ac_simps) }
note product = this
show "sigma_finite_measure I'.P ?\<nu>"
proof
@@ -1671,7 +1680,7 @@
shows "pair_sigma_finite.pair_measure
(sigma (product_algebra M I)) (product_measure I)
(sigma (product_algebra M J)) (product_measure J)
- ((\<lambda>x. ((\<lambda>i\<in>I. x i), (\<lambda>i\<in>J. x i))) ` A) =
+ ((\<lambda>(x,y). merge I x J y) -` A \<inter> space (sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J))))) =
product_measure (I \<union> J) A"
proof -
interpret I: finite_product_sigma_finite M \<mu> I by default fact
@@ -1679,51 +1688,52 @@
have "finite (I \<union> J)" using fin by auto
interpret IJ: finite_product_sigma_finite M \<mu> "I \<union> J" by default fact
interpret P: pair_sigma_finite I.P I.measure J.P J.measure by default
- let ?f = "\<lambda>x. ((\<lambda>i\<in>I. x i), (\<lambda>i\<in>J. x i))"
- from IJ.sigma_finite_pairs obtain F where
- F: "\<And>i. i\<in> I \<union> J \<Longrightarrow> range (F i) \<subseteq> sets (M i)"
- "(\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k) \<up> space IJ.G"
- "\<And>k. \<forall>i\<in>I\<union>J. \<mu> i (F i k) \<noteq> \<omega>"
- by auto
- let ?F = "\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k"
- 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)"
- apply auto apply (rule_tac x="merge I a J b" in image_eqI)
- by (auto dest: extensional_restrict)
- show "P.pair_measure (?f ` A) = IJ.measure A"
+ let ?g = "\<lambda>(x,y). merge I x J y"
+ let "?X S" = "?g -` S \<inter> space P.P"
+ from IJ.sigma_finite_pairs obtain F where
+ F: "\<And>i. i\<in> I \<union> J \<Longrightarrow> range (F i) \<subseteq> sets (M i)"
+ "(\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k) \<up> space IJ.G"
+ "\<And>k. \<forall>i\<in>I\<union>J. \<mu> i (F i k) \<noteq> \<omega>"
+ by auto
+ let ?F = "\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k"
+ show "P.pair_measure (?X A) = IJ.measure A"
proof (rule measure_unique_Int_stable[OF _ _ _ _ _ _ _ _ A])
- show "Int_stable IJ.G" by (simp add: PiE_Int Int_stable_def product_algebra_def) auto
- show "range ?F \<subseteq> sets IJ.G" using F by (simp add: image_subset_iff product_algebra_def)
- show "?F \<up> space IJ.G " using F(2) by simp
- show "measure_space IJ.P (\<lambda>A. P.pair_measure (?f ` A))"
- apply (subst product_product_vimage_algebra[OF IJ, symmetric])
- apply (intro P.measure_space_isomorphic bij_inv_bij_betw)
- unfolding sigma_pair_algebra_sigma_eq
- by (rule bij_inv_restrict_merge[OF `I \<inter> J = {}`])
- show "measure_space IJ.P IJ.measure" by fact
- next
- fix A assume "A \<in> sets IJ.G"
- 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))"
- by (auto simp: product_algebra_def)
- 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)"
- by auto
- have "P.pair_measure (?f ` A) = (\<Prod>i\<in>I. \<mu> i (F i)) * (\<Prod>i\<in>J. \<mu> i (F i))"
- using `finite J` `finite I` F
- by (simp add: P.pair_measure_times I.measure_times J.measure_times)
- also have "\<dots> = (\<Prod>i\<in>I \<union> J. \<mu> i (F i))"
- using `finite J` `finite I` `I \<inter> J = {}` by (simp add: setprod_Un_one)
- also have "\<dots> = IJ.measure A"
- using `finite J` `finite I` F unfolding A
- by (intro IJ.measure_times[symmetric]) auto
- finally show "P.pair_measure (?f ` A) = IJ.measure A" .
- next
- fix k
- have "\<And>i. i \<in> I \<union> J \<Longrightarrow> F i k \<in> sets (M i)" using F by auto
- 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))"
- by (simp add: P.pair_measure_times I.measure_times J.measure_times)
- then show "P.pair_measure (?f ` ?F k) \<noteq> \<omega>"
- using `finite I` F by (simp add: setprod_\<omega>)
- qed simp
- qed
+ show "Int_stable IJ.G" by (simp add: PiE_Int Int_stable_def product_algebra_def) auto
+ show "range ?F \<subseteq> sets IJ.G" using F by (simp add: image_subset_iff product_algebra_def)
+ show "?F \<up> space IJ.G " using F(2) by simp
+ have "sigma_algebra IJ.P" by default
+ then show "measure_space IJ.P (\<lambda>A. P.pair_measure (?X A))"
+ apply (rule P.measure_space_vimage)
+ apply (rule measurable_merge[OF `I \<inter> J = {}`])
+ by simp
+ show "measure_space IJ.P IJ.measure" by fact
+ next
+ fix A assume "A \<in> sets IJ.G"
+ then obtain F where A[simp]: "A = Pi\<^isub>E (I \<union> J) F"
+ and F: "\<And>i. i \<in> I \<union> J \<Longrightarrow> F i \<in> sets (M i)"
+ by (auto simp: product_algebra_def)
+ then have "?X A = (Pi\<^isub>E I F \<times> Pi\<^isub>E J F)"
+ using sets_into_space by (auto simp: space_pair_algebra) blast+
+ then have "P.pair_measure (?X A) = (\<Prod>i\<in>I. \<mu> i (F i)) * (\<Prod>i\<in>J. \<mu> i (F i))"
+ using `finite J` `finite I` F
+ by (simp add: P.pair_measure_times I.measure_times J.measure_times)
+ also have "\<dots> = (\<Prod>i\<in>I \<union> J. \<mu> i (F i))"
+ using `finite J` `finite I` `I \<inter> J = {}` by (simp add: setprod_Un_one)
+ also have "\<dots> = IJ.measure A"
+ using `finite J` `finite I` F unfolding A
+ by (intro IJ.measure_times[symmetric]) auto
+ finally show "P.pair_measure (?X A) = IJ.measure A" .
+ next
+ fix k
+ have k: "\<And>i. i \<in> I \<union> J \<Longrightarrow> F i k \<in> sets (M i)" using F by auto
+ then have "?X (?F k) = (\<Pi>\<^isub>E i\<in>I. F i k) \<times> (\<Pi>\<^isub>E i\<in>J. F i k)"
+ using sets_into_space by (auto simp: space_pair_algebra) blast+
+ 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))"
+ by (simp add: P.pair_measure_times I.measure_times J.measure_times)
+ then show "P.pair_measure (?X (?F k)) \<noteq> \<omega>"
+ using `finite I` F by (simp add: setprod_\<omega>)
+ qed simp
+qed
lemma (in product_sigma_finite) product_positive_integral_fold:
assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
@@ -1736,23 +1746,18 @@
have "finite (I \<union> J)" using fin by auto
interpret IJ: finite_product_sigma_finite M \<mu> "I \<union> J" by default fact
interpret P: pair_sigma_finite I.P I.measure J.P J.measure by default
- let ?f = "\<lambda>x. ((\<lambda>i\<in>I. x i), (\<lambda>i\<in>J. x i))"
have P_borel: "(\<lambda>x. f (case x of (x, y) \<Rightarrow> merge I x J y)) \<in> borel_measurable P.P"
unfolding case_prod_distrib measurable_merge_iff[OF IJ, symmetric] using f .
- have bij: "bij_betw ?f (space IJ.P) (space P.P)"
- unfolding sigma_pair_algebra_sigma_eq
- by (intro bij_inv_bij_betw) (rule bij_inv_restrict_merge[OF IJ])
- have "IJ.positive_integral f = IJ.positive_integral (\<lambda>x. f (restrict x (I \<union> J)))"
- by (auto intro!: IJ.positive_integral_cong arg_cong[where f=f] dest!: extensional_restrict)
- also have "\<dots> = I.positive_integral (\<lambda>x. J.positive_integral (\<lambda>y. f (merge I x J y)))"
+ show ?thesis
unfolding P.positive_integral_fst_measurable[OF P_borel, simplified]
- unfolding P.positive_integral_vimage[OF bij]
- unfolding product_product_vimage_algebra[OF IJ]
- apply simp
- apply (rule IJ.positive_integral_cong_measure[symmetric])
- apply (rule measure_fold)
- using assms by auto
- finally show ?thesis .
+ apply (subst IJ.positive_integral_cong_measure[symmetric])
+ apply (rule measure_fold[OF IJ fin])
+ apply assumption
+ proof (rule P.positive_integral_vimage)
+ show "sigma_algebra IJ.P" by default
+ show "(\<lambda>(x, y). merge I x J y) \<in> measurable P.P IJ.P" by (rule measurable_merge[OF IJ])
+ show "f \<in> borel_measurable IJ.P" using f .
+ qed
qed
lemma (in product_sigma_finite) product_positive_integral_singleton:
@@ -1760,31 +1765,18 @@
shows "product_positive_integral {i} (\<lambda>x. f (x i)) = M.positive_integral i f"
proof -
interpret I: finite_product_sigma_finite M \<mu> "{i}" by default simp
- have bij: "bij_betw (\<lambda>x. \<lambda>j\<in>{i}. x) (space (M i)) (space I.P)"
- by (auto intro!: bij_betwI ext simp: extensional_def)
- 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)"
- proof (subst image_cong, rule refl)
- fix x assume "x \<in> (\<Pi> i\<in>{i}. sets (M i))"
- then show "(\<lambda>x. \<lambda>j\<in>{i}. x) -` Pi\<^isub>E {i} x \<inter> space (M i) = x i"
- using sets_into_space by auto
- qed auto
- have vimage: "I.vimage_algebra (space (M i)) (\<lambda>x. \<lambda>j\<in>{i}. x) = M i"
- unfolding I.vimage_algebra_def
- unfolding product_sigma_algebra_def sets_sigma
- apply (subst sigma_sets_vimage[symmetric])
- apply (simp_all add: image_image sigma_sets_eq product_algebra_def * del: vimage_Int)
- using sets_into_space by blast
+ have T: "(\<lambda>x. x i) \<in> measurable (sigma (product_algebra M {i})) (M i)"
+ using measurable_component_singleton[of "\<lambda>x. x" i]
+ measurable_ident[unfolded id_def] by auto
show "I.positive_integral (\<lambda>x. f (x i)) = M.positive_integral i f"
- unfolding I.positive_integral_vimage[OF bij]
- unfolding vimage
- apply (subst positive_integral_cong_measure)
- proof -
- fix A assume A: "A \<in> sets (M i)"
- have "(\<lambda>x. \<lambda>j\<in>{i}. x) ` A = (\<Pi>\<^isub>E i\<in>{i}. A)"
- by (auto intro!: image_eqI ext[where 'b='a] simp: extensional_def)
- with A show "product_measure {i} ((\<lambda>x. \<lambda>j\<in>{i}. x) ` A) = \<mu> i A"
- using I.measure_times[of "\<lambda>i. A"] by simp
- qed simp
+ unfolding I.positive_integral_vimage[OF sigma_algebras T f, symmetric]
+ proof (rule positive_integral_cong_measure)
+ fix A let ?P = "(\<lambda>x. x i) -` A \<inter> space (sigma (product_algebra M {i}))"
+ assume A: "A \<in> sets (M i)"
+ then have *: "?P = {i} \<rightarrow>\<^isub>E A" using sets_into_space by auto
+ show "product_measure {i} ?P = \<mu> i A" unfolding *
+ using A I.measure_times[of "\<lambda>_. A"] by auto
+ qed
qed
lemma (in product_sigma_finite) product_positive_integral_insert:
--- a/src/HOL/Probability/Radon_Nikodym.thy Fri Jan 21 10:43:09 2011 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy Tue Jan 25 09:45:45 2011 +0100
@@ -1104,38 +1104,6 @@
unfolding eq[OF A, symmetric] RN_deriv(2)[OF \<nu> A, symmetric] ..
qed
-lemma (in sigma_finite_measure) RN_deriv_vimage:
- fixes f :: "'b \<Rightarrow> 'a"
- assumes f: "bij_inv S (space M) f g"
- assumes \<nu>: "measure_space M \<nu>" "absolutely_continuous \<nu>"
- shows "AE x.
- sigma_finite_measure.RN_deriv (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) (\<lambda>A. \<nu> (f ` A)) (g x) = RN_deriv \<nu> x"
-proof (rule RN_deriv_unique[OF \<nu>])
- interpret sf: sigma_finite_measure "vimage_algebra S f" "\<lambda>A. \<mu> (f ` A)"
- using f by (rule sigma_finite_measure_isomorphic[OF bij_inv_bij_betw(1)])
- interpret \<nu>: measure_space M \<nu> using \<nu>(1) .
- have \<nu>': "measure_space (vimage_algebra S f) (\<lambda>A. \<nu> (f ` A))"
- using f by (rule \<nu>.measure_space_isomorphic[OF bij_inv_bij_betw(1)])
- { fix A assume "A \<in> sets M" then have "f ` (f -` A \<inter> S) = A"
- using sets_into_space f[THEN bij_inv_bij_betw(1), unfolded bij_betw_def]
- by (intro image_vimage_inter_eq[where T="space M"]) auto }
- note A_f = this
- then have ac: "sf.absolutely_continuous (\<lambda>A. \<nu> (f ` A))"
- using \<nu>(2) by (auto simp: sf.absolutely_continuous_def absolutely_continuous_def)
- show "(\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x)) \<in> borel_measurable M"
- using sf.RN_deriv(1)[OF \<nu>' ac]
- unfolding measurable_vimage_iff_inv[OF f] comp_def .
- fix A assume "A \<in> sets M"
- then have *: "\<And>x. x \<in> space M \<Longrightarrow> indicator (f -` A \<inter> S) (g x) = (indicator A x :: pextreal)"
- using f by (auto simp: bij_inv_def indicator_def)
- have "\<nu> (f ` (f -` A \<inter> S)) = sf.positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) x * indicator (f -` A \<inter> S) x)"
- using `A \<in> sets M` by (force intro!: sf.RN_deriv(2)[OF \<nu>' ac])
- also have "\<dots> = (\<integral>\<^isup>+x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)"
- unfolding positive_integral_vimage_inv[OF f]
- by (simp add: * cong: positive_integral_cong)
- finally show "\<nu> A = (\<integral>\<^isup>+x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)"
- unfolding A_f[OF `A \<in> sets M`] .
-qed
lemma (in sigma_finite_measure) RN_deriv_finite:
assumes sfm: "sigma_finite_measure M \<nu>" and ac: "absolutely_continuous \<nu>"