--- a/src/HOL/Probability/Lebesgue_Integration.thy Wed Feb 23 11:33:45 2011 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Wed Feb 23 11:40:12 2011 +0100
@@ -821,30 +821,33 @@
shows "integral\<^isup>S N = integral\<^isup>S M"
unfolding simple_integral_def_raw by simp
+lemma measure_preservingD:
+ "T \<in> measure_preserving A B \<Longrightarrow> X \<in> sets B \<Longrightarrow> measure A (T -` X \<inter> space A) = measure B X"
+ unfolding measure_preserving_def by auto
+
lemma (in measure_space) simple_integral_vimage:
- assumes T: "sigma_algebra M'" "T \<in> measurable M M'"
+ assumes T: "sigma_algebra M'" "T \<in> measure_preserving M M'"
and f: "simple_function M' f"
- and \<nu>: "\<And>A. A \<in> sets M' \<Longrightarrow> measure M' A = \<mu> (T -` A \<inter> space M)"
shows "integral\<^isup>S M' f = (\<integral>\<^isup>S x. f (T x) \<partial>M)"
proof -
- interpret T: measure_space M' using \<nu> by (rule measure_space_vimage[OF T])
+ interpret T: measure_space M' by (rule measure_space_vimage[OF T])
show "integral\<^isup>S M' f = (\<integral>\<^isup>S x. f (T x) \<partial>M)"
unfolding simple_integral_def
proof (intro setsum_mono_zero_cong_right ballI)
show "(\<lambda>x. f (T x)) ` space M \<subseteq> f ` space M'"
- using T unfolding measurable_def by auto
+ using T unfolding measurable_def measure_preserving_def by auto
show "finite (f ` space M')"
using f unfolding simple_function_def by auto
next
fix i assume "i \<in> f ` space M' - (\<lambda>x. f (T x)) ` space M"
then have "T -` (f -` {i} \<inter> space M') \<inter> space M = {}" by (auto simp: image_iff)
- with f[THEN T.simple_functionD(2), THEN \<nu>]
+ with f[THEN T.simple_functionD(2), THEN measure_preservingD[OF T(2)], of "{i}"]
show "i * T.\<mu> (f -` {i} \<inter> space M') = 0" by simp
next
fix i assume "i \<in> (\<lambda>x. f (T x)) ` space M"
then have "T -` (f -` {i} \<inter> space M') \<inter> space M = (\<lambda>x. f (T x)) -` {i} \<inter> space M"
- using T unfolding measurable_def by auto
- with f[THEN T.simple_functionD(2), THEN \<nu>]
+ using T unfolding measurable_def measure_preserving_def by auto
+ with f[THEN T.simple_functionD(2), THEN measure_preservingD[OF T(2)], of "{i}"]
show "i * T.\<mu> (f -` {i} \<inter> space M') = i * \<mu> ((\<lambda>x. f (T x)) -` {i} \<inter> space M)"
by auto
qed
@@ -1195,20 +1198,23 @@
using positive_integral_isoton[OF `f \<up> u` e(1)[THEN borel_measurable_simple_function]]
unfolding positive_integral_eq_simple_integral[OF e] .
+lemma measure_preservingD2:
+ "f \<in> measure_preserving A B \<Longrightarrow> f \<in> measurable A B"
+ unfolding measure_preserving_def by auto
+
lemma (in measure_space) positive_integral_vimage:
- assumes T: "sigma_algebra M'" "T \<in> measurable M M'" and f: "f \<in> borel_measurable M'"
- and \<nu>: "\<And>A. A \<in> sets M' \<Longrightarrow> measure M' A = \<mu> (T -` A \<inter> space M)"
+ assumes T: "sigma_algebra M'" "T \<in> measure_preserving M M'" and f: "f \<in> borel_measurable M'"
shows "integral\<^isup>P M' f = (\<integral>\<^isup>+ x. f (T x) \<partial>M)"
proof -
- interpret T: measure_space M' using \<nu> by (rule measure_space_vimage[OF T])
+ interpret T: measure_space M' by (rule measure_space_vimage[OF T])
obtain f' where f': "f' \<up> f" "\<And>i. simple_function M' (f' i)"
using T.borel_measurable_implies_simple_function_sequence[OF f] by blast
then have f: "(\<lambda>i x. f' i (T x)) \<up> (\<lambda>x. f (T x))" "\<And>i. simple_function M (\<lambda>x. f' i (T x))"
- using simple_function_vimage[OF T] unfolding isoton_fun_expand by auto
+ using simple_function_vimage[OF T(1) measure_preservingD2[OF T(2)]] unfolding isoton_fun_expand by auto
show "integral\<^isup>P M' f = (\<integral>\<^isup>+ x. f (T x) \<partial>M)"
using positive_integral_isoton_simple[OF f]
using T.positive_integral_isoton_simple[OF f']
- by (simp add: simple_integral_vimage[OF T f'(2) \<nu>] isoton_def)
+ by (simp add: simple_integral_vimage[OF T f'(2)] isoton_def)
qed
lemma (in measure_space) positive_integral_linear:
@@ -1604,20 +1610,33 @@
qed
lemma (in measure_space) integral_vimage:
- assumes T: "sigma_algebra M'" "T \<in> measurable M M'"
- and \<nu>: "\<And>A. A \<in> sets M' \<Longrightarrow> measure M' A = \<mu> (T -` A \<inter> space M)"
- assumes f: "integrable M' f"
- shows "integrable M (\<lambda>x. f (T x))" (is ?P)
- and "integral\<^isup>L M' f = (\<integral>x. f (T x) \<partial>M)" (is ?I)
+ assumes T: "sigma_algebra M'" "T \<in> measure_preserving M M'"
+ assumes f: "f \<in> borel_measurable M'"
+ shows "integral\<^isup>L M' f = (\<integral>x. f (T x) \<partial>M)"
proof -
- interpret T: measure_space M' using \<nu> by (rule measure_space_vimage[OF T])
- from measurable_comp[OF T(2), of f borel]
+ interpret T: measure_space M' by (rule measure_space_vimage[OF T])
+ from measurable_comp[OF measure_preservingD2[OF T(2)], of f borel]
have borel: "(\<lambda>x. Real (f x)) \<in> borel_measurable M'" "(\<lambda>x. Real (- f x)) \<in> borel_measurable M'"
and "(\<lambda>x. f (T x)) \<in> borel_measurable M"
- using f unfolding integrable_def by (auto simp: comp_def)
- then show ?P ?I
+ using f by (auto simp: comp_def)
+ then show ?thesis
using f unfolding lebesgue_integral_def integrable_def
- by (auto simp: borel[THEN positive_integral_vimage[OF T], OF \<nu>])
+ by (auto simp: borel[THEN positive_integral_vimage[OF T]])
+qed
+
+lemma (in measure_space) integrable_vimage:
+ assumes T: "sigma_algebra M'" "T \<in> measure_preserving M M'"
+ assumes f: "integrable M' f"
+ shows "integrable M (\<lambda>x. f (T x))"
+proof -
+ interpret T: measure_space M' by (rule measure_space_vimage[OF T])
+ from measurable_comp[OF measure_preservingD2[OF T(2)], of f borel]
+ have borel: "(\<lambda>x. Real (f x)) \<in> borel_measurable M'" "(\<lambda>x. Real (- f x)) \<in> borel_measurable M'"
+ and "(\<lambda>x. f (T x)) \<in> borel_measurable M"
+ using f by (auto simp: comp_def)
+ then show ?thesis
+ using f unfolding lebesgue_integral_def integrable_def
+ by (auto simp: borel[THEN positive_integral_vimage[OF T]])
qed
lemma (in measure_space) integral_minus[intro, simp]:
--- a/src/HOL/Probability/Lebesgue_Measure.thy Wed Feb 23 11:33:45 2011 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Wed Feb 23 11:40:12 2011 +0100
@@ -733,13 +733,6 @@
unfolding lebesgue_integral_eq_borel[OF borel] by simp
qed
-lemma continuous_on_imp_borel_measurable:
- fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::ordered_euclidean_space"
- assumes "continuous_on UNIV f"
- shows "f \<in> borel_measurable borel"
- apply(rule borel.borel_measurableI)
- using continuous_open_preimage[OF assms] unfolding vimage_def by auto
-
subsection {* Equivalence between product spaces and euclidean spaces *}
definition e2p :: "'a::ordered_euclidean_space \<Rightarrow> (nat \<Rightarrow> real)" where
@@ -759,13 +752,13 @@
interpretation lborel_product: product_sigma_finite "\<lambda>x. lborel::real measure_space"
by default
-interpretation lborel_space: finite_product_sigma_finite "\<lambda>x. lborel::real measure_space" "{..<DIM('a::ordered_euclidean_space)}"
+interpretation lborel_space: finite_product_sigma_finite "\<lambda>x. lborel::real measure_space" "{..<n}" for n :: nat
where "space lborel = UNIV"
and "sets lborel = sets borel"
and "measure lborel = lebesgue.\<mu>"
and "measurable lborel = measurable borel"
proof -
- show "finite_product_sigma_finite (\<lambda>x. lborel::real measure_space) {..<DIM('a::ordered_euclidean_space)}"
+ show "finite_product_sigma_finite (\<lambda>x. lborel::real measure_space) {..<n}"
by default simp
qed simp_all
@@ -836,7 +829,7 @@
lemma lborel_eq_lborel_space:
fixes A :: "('a::ordered_euclidean_space) set"
assumes "A \<in> sets borel"
- shows "lborel.\<mu> A = lborel_space.\<mu> TYPE('a) (p2e -` A \<inter> (space (lborel_space.P TYPE('a))))"
+ shows "lborel.\<mu> A = lborel_space.\<mu> DIM('a) (p2e -` A \<inter> (space (lborel_space.P DIM('a))))"
(is "_ = measure ?P (?T A)")
proof (rule measure_unique_Int_stable_vimage)
show "measure_space ?P" by default
@@ -871,27 +864,36 @@
qed simp }
qed
+lemma measure_preserving_p2e:
+ "p2e \<in> measure_preserving (\<Pi>\<^isub>M i\<in>{..<DIM('a)}. (lborel :: real measure_space))
+ (lborel::'a::ordered_euclidean_space measure_space)" (is "_ \<in> measure_preserving ?P ?E")
+proof
+ show "p2e \<in> measurable ?P ?E"
+ using measurable_p2e by (simp add: measurable_def)
+ fix A :: "'a set" assume "A \<in> sets lborel"
+ then show "lborel_space.\<mu> DIM('a) (p2e -` A \<inter> (space (lborel_space.P DIM('a)))) = lborel.\<mu> A"
+ by (intro lborel_eq_lborel_space[symmetric]) simp
+qed
+
lemma lebesgue_eq_lborel_space_in_borel:
fixes A :: "('a::ordered_euclidean_space) set"
assumes A: "A \<in> sets borel"
- shows "lebesgue.\<mu> A = lborel_space.\<mu> TYPE('a) (p2e -` A \<inter> (space (lborel_space.P TYPE('a))))"
+ shows "lebesgue.\<mu> A = lborel_space.\<mu> DIM('a) (p2e -` A \<inter> (space (lborel_space.P DIM('a))))"
using lborel_eq_lborel_space[OF A] by simp
lemma borel_fubini_positiv_integral:
fixes f :: "'a::ordered_euclidean_space \<Rightarrow> pextreal"
assumes f: "f \<in> borel_measurable borel"
- shows "integral\<^isup>P lborel f = \<integral>\<^isup>+x. f (p2e x) \<partial>(lborel_space.P TYPE('a))"
-proof (rule lborel_space.positive_integral_vimage[OF _ _ _ lborel_eq_lborel_space])
- show "sigma_algebra lborel" by default
- show "p2e \<in> measurable (lborel_space.P TYPE('a)) (lborel :: 'a measure_space)"
- "f \<in> borel_measurable lborel"
- using measurable_p2e f by (simp_all add: measurable_def)
-qed simp
+ shows "integral\<^isup>P lborel f = \<integral>\<^isup>+x. f (p2e x) \<partial>(lborel_space.P DIM('a))"
+proof (rule lborel_space.positive_integral_vimage[OF _ measure_preserving_p2e _])
+ show "f \<in> borel_measurable lborel"
+ using f by (simp_all add: measurable_def)
+qed default
lemma borel_fubini_integrable:
fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real"
shows "integrable lborel f \<longleftrightarrow>
- integrable (lborel_space.P TYPE('a)) (\<lambda>x. f (p2e x))"
+ integrable (lborel_space.P DIM('a)) (\<lambda>x. f (p2e x))"
(is "_ \<longleftrightarrow> integrable ?B ?f")
proof
assume "integrable lborel f"
@@ -916,7 +918,7 @@
lemma borel_fubini:
fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real"
assumes f: "f \<in> borel_measurable borel"
- shows "integral\<^isup>L lborel f = \<integral>x. f (p2e x) \<partial>(lborel_space.P TYPE('a))"
+ shows "integral\<^isup>L lborel f = \<integral>x. f (p2e x) \<partial>(lborel_space.P DIM('a))"
using f by (simp add: borel_fubini_positiv_integral lebesgue_integral_def)
end
--- a/src/HOL/Probability/Measure.thy Wed Feb 23 11:33:45 2011 +0100
+++ b/src/HOL/Probability/Measure.thy Wed Feb 23 11:40:12 2011 +0100
@@ -16,6 +16,23 @@
lemma measure_sigma[simp]: "measure (sigma A) = measure A"
unfolding sigma_def by simp
+lemma algebra_measure_update[simp]:
+ "algebra (M'\<lparr>measure := m\<rparr>) \<longleftrightarrow> algebra M'"
+ unfolding algebra_def by simp
+
+lemma sigma_algebra_measure_update[simp]:
+ "sigma_algebra (M'\<lparr>measure := m\<rparr>) \<longleftrightarrow> sigma_algebra M'"
+ unfolding sigma_algebra_def sigma_algebra_axioms_def by simp
+
+lemma finite_sigma_algebra_measure_update[simp]:
+ "finite_sigma_algebra (M'\<lparr>measure := m\<rparr>) \<longleftrightarrow> finite_sigma_algebra M'"
+ unfolding finite_sigma_algebra_def finite_sigma_algebra_axioms_def by simp
+
+lemma measurable_cancel_measure[simp]:
+ "measurable M1 (M2\<lparr>measure := m2\<rparr>) = measurable M1 M2"
+ "measurable (M2\<lparr>measure := m1\<rparr>) M1 = measurable M2 M1"
+ unfolding measurable_def by auto
+
lemma inj_on_image_eq_iff:
assumes "inj_on f S"
assumes "A \<subseteq> S" "B \<subseteq> S"
@@ -624,59 +641,6 @@
ultimately show ?thesis by (simp add: isoton_def)
qed
-lemma (in measure_space) measure_space_vimage:
- fixes M' :: "('c, 'd) measure_space_scheme"
- assumes T: "sigma_algebra M'" "T \<in> measurable M M'"
- and \<nu>: "\<And>A. A \<in> sets M' \<Longrightarrow> measure M' A = \<mu> (T -` A \<inter> space M)"
- shows "measure_space M'"
-proof -
- interpret M': sigma_algebra M' by fact
- show ?thesis
- proof
- show "measure M' {} = 0" using \<nu>[of "{}"] by simp
-
- show "countably_additive M' (measure M')"
- proof (intro countably_additiveI)
- fix A :: "nat \<Rightarrow> 'c set" assume "range A \<subseteq> sets M'" "disjoint_family A"
- then have A: "\<And>i. A i \<in> sets M'" "(\<Union>i. A i) \<in> sets M'" by auto
- then have *: "range (\<lambda>i. T -` (A i) \<inter> space M) \<subseteq> sets M"
- using `T \<in> measurable M M'` by (auto simp: measurable_def)
- moreover have "(\<Union>i. T -` A i \<inter> space M) \<in> sets M"
- using * by blast
- moreover have **: "disjoint_family (\<lambda>i. T -` A i \<inter> space M)"
- using `disjoint_family A` by (auto simp: disjoint_family_on_def)
- ultimately show "(\<Sum>\<^isub>\<infinity> i. measure M' (A i)) = measure M' (\<Union>i. A i)"
- using measure_countably_additive[OF _ **] A
- by (auto simp: comp_def vimage_UN \<nu>)
- qed
- qed
-qed
-
-lemma measure_unique_Int_stable_vimage:
- fixes A :: "nat \<Rightarrow> 'a set"
- assumes E: "Int_stable E"
- and A: "range A \<subseteq> sets E" "A \<up> space E" "\<And>i. measure M (A i) \<noteq> \<omega>"
- and N: "measure_space N" "T \<in> measurable N M"
- and M: "measure_space M" "sets (sigma E) = sets M" "space E = space M"
- and eq: "\<And>X. X \<in> sets E \<Longrightarrow> measure M X = measure N (T -` X \<inter> space N)"
- assumes X: "X \<in> sets (sigma E)"
- shows "measure M X = measure N (T -` X \<inter> space N)"
-proof (rule measure_unique_Int_stable[OF E A(1,2) _ _ eq _ X])
- interpret M: measure_space M by fact
- interpret N: measure_space N by fact
- let "?T X" = "T -` X \<inter> space N"
- show "measure_space \<lparr>space = space E, sets = sets (sigma E), measure = measure M\<rparr>"
- by (rule M.measure_space_cong) (auto simp: M)
- show "measure_space \<lparr>space = space E, sets = sets (sigma E), measure = \<lambda>X. measure N (?T X)\<rparr>" (is "measure_space ?E")
- proof (rule N.measure_space_vimage)
- show "sigma_algebra ?E"
- by (rule M.sigma_algebra_cong) (auto simp: M)
- show "T \<in> measurable N ?E"
- using `T \<in> measurable N M` by (auto simp: M measurable_def)
- qed simp
- show "\<And>i. M.\<mu> (A i) \<noteq> \<omega>" by fact
-qed
-
section "@{text \<mu>}-null sets"
abbreviation (in measure_space) "null_sets \<equiv> {N\<in>sets M. \<mu> N = 0}"
@@ -991,6 +955,105 @@
qed force+
qed
+section {* Measure preserving *}
+
+definition "measure_preserving A B =
+ {f \<in> measurable A B. (\<forall>y \<in> sets B. measure A (f -` y \<inter> space A) = measure B y)}"
+
+lemma measure_preservingI[intro?]:
+ assumes "f \<in> measurable A B"
+ and "\<And>y. y \<in> sets B \<Longrightarrow> measure A (f -` y \<inter> space A) = measure B y"
+ shows "f \<in> measure_preserving A B"
+ unfolding measure_preserving_def using assms by auto
+
+lemma (in measure_space) measure_space_vimage:
+ fixes M' :: "('c, 'd) measure_space_scheme"
+ assumes T: "sigma_algebra M'" "T \<in> measure_preserving M M'"
+ shows "measure_space M'"
+proof -
+ interpret M': sigma_algebra M' by fact
+ show ?thesis
+ proof
+ show "measure M' {} = 0" using T by (force simp: measure_preserving_def)
+
+ show "countably_additive M' (measure M')"
+ proof (intro countably_additiveI)
+ fix A :: "nat \<Rightarrow> 'c set" assume "range A \<subseteq> sets M'" "disjoint_family A"
+ then have A: "\<And>i. A i \<in> sets M'" "(\<Union>i. A i) \<in> sets M'" by auto
+ then have *: "range (\<lambda>i. T -` (A i) \<inter> space M) \<subseteq> sets M"
+ using T by (auto simp: measurable_def measure_preserving_def)
+ moreover have "(\<Union>i. T -` A i \<inter> space M) \<in> sets M"
+ using * by blast
+ moreover have **: "disjoint_family (\<lambda>i. T -` A i \<inter> space M)"
+ using `disjoint_family A` by (auto simp: disjoint_family_on_def)
+ ultimately show "(\<Sum>\<^isub>\<infinity> i. measure M' (A i)) = measure M' (\<Union>i. A i)"
+ using measure_countably_additive[OF _ **] A T
+ by (auto simp: comp_def vimage_UN measure_preserving_def)
+ qed
+ qed
+qed
+
+lemma (in measure_space) almost_everywhere_vimage:
+ assumes T: "sigma_algebra M'" "T \<in> measure_preserving M M'"
+ and AE: "measure_space.almost_everywhere M' P"
+ shows "AE x. P (T x)"
+proof -
+ interpret M': measure_space M' using T by (rule measure_space_vimage)
+ from AE[THEN M'.AE_E] guess N .
+ then show ?thesis
+ unfolding almost_everywhere_def M'.almost_everywhere_def
+ using T(2) unfolding measurable_def measure_preserving_def
+ by (intro bexI[of _ "T -` N \<inter> space M"]) auto
+qed
+
+lemma measure_unique_Int_stable_vimage:
+ fixes A :: "nat \<Rightarrow> 'a set"
+ assumes E: "Int_stable E"
+ and A: "range A \<subseteq> sets E" "A \<up> space E" "\<And>i. measure M (A i) \<noteq> \<omega>"
+ and N: "measure_space N" "T \<in> measurable N M"
+ and M: "measure_space M" "sets (sigma E) = sets M" "space E = space M"
+ and eq: "\<And>X. X \<in> sets E \<Longrightarrow> measure M X = measure N (T -` X \<inter> space N)"
+ assumes X: "X \<in> sets (sigma E)"
+ shows "measure M X = measure N (T -` X \<inter> space N)"
+proof (rule measure_unique_Int_stable[OF E A(1,2) _ _ eq _ X])
+ interpret M: measure_space M by fact
+ interpret N: measure_space N by fact
+ let "?T X" = "T -` X \<inter> space N"
+ show "measure_space \<lparr>space = space E, sets = sets (sigma E), measure = measure M\<rparr>"
+ by (rule M.measure_space_cong) (auto simp: M)
+ show "measure_space \<lparr>space = space E, sets = sets (sigma E), measure = \<lambda>X. measure N (?T X)\<rparr>" (is "measure_space ?E")
+ proof (rule N.measure_space_vimage)
+ show "sigma_algebra ?E"
+ by (rule M.sigma_algebra_cong) (auto simp: M)
+ show "T \<in> measure_preserving N ?E"
+ using `T \<in> measurable N M` by (auto simp: M measurable_def measure_preserving_def)
+ qed
+ show "\<And>i. M.\<mu> (A i) \<noteq> \<omega>" by fact
+qed
+
+lemma (in measure_space) measure_preserving_Int_stable:
+ fixes A :: "nat \<Rightarrow> 'a set"
+ assumes E: "Int_stable E" "range A \<subseteq> sets E" "A \<up> space E" "\<And>i. measure E (A i) \<noteq> \<omega>"
+ and N: "measure_space (sigma E)"
+ and T: "T \<in> measure_preserving M E"
+ shows "T \<in> measure_preserving M (sigma E)"
+proof
+ interpret E: measure_space "sigma E" by fact
+ show "T \<in> measurable M (sigma E)"
+ using T E.sets_into_space
+ by (intro measurable_sigma) (auto simp: measure_preserving_def measurable_def)
+ fix X assume "X \<in> sets (sigma E)"
+ show "\<mu> (T -` X \<inter> space M) = E.\<mu> X"
+ proof (rule measure_unique_Int_stable_vimage[symmetric])
+ show "sets (sigma E) = sets (sigma E)" "space E = space (sigma E)"
+ "\<And>i. E.\<mu> (A i) \<noteq> \<omega>" using E by auto
+ show "measure_space M" by default
+ next
+ fix X assume "X \<in> sets E" then show "E.\<mu> X = \<mu> (T -` X \<inter> space M)"
+ using T unfolding measure_preserving_def by auto
+ qed fact+
+qed
+
section "Real measure values"
lemma (in measure_space) real_measure_Union:
@@ -1230,11 +1293,6 @@
using measure_inter_full_set[OF assms(1,2) finite_measure assms(3)] assms
by auto
-section {* Measure preserving *}
-
-definition "measure_preserving A B =
- {f \<in> measurable A B. (\<forall>y \<in> sets B. measure A (f -` y \<inter> space A) = measure B y)}"
-
lemma (in finite_measure) measure_preserving_lift:
fixes f :: "'a \<Rightarrow> 'c" and A :: "('c, 'd) measure_space_scheme"
assumes "algebra A" "finite_measure (sigma A)" (is "finite_measure ?sA")
--- a/src/HOL/Probability/Probability_Space.thy Wed Feb 23 11:33:45 2011 +0100
+++ b/src/HOL/Probability/Probability_Space.thy Wed Feb 23 11:40:12 2011 +0100
@@ -198,7 +198,7 @@
interpret S: measure_space "S\<lparr>measure := distribution X\<rparr>"
unfolding distribution_def using assms
by (intro measure_space_vimage)
- (auto intro!: sigma_algebra.sigma_algebra_cong[of S])
+ (auto intro!: sigma_algebra.sigma_algebra_cong[of S] simp: measure_preserving_def)
show ?thesis
proof (default, simp)
have "X -` space S \<inter> space M = space M"
--- a/src/HOL/Probability/Product_Measure.thy Wed Feb 23 11:33:45 2011 +0100
+++ b/src/HOL/Probability/Product_Measure.thy Wed Feb 23 11:40:12 2011 +0100
@@ -2,14 +2,6 @@
imports Lebesgue_Integration
begin
-lemma measurable_cancel_measure2[simp]:
- "measurable M1 (M2\<lparr>measure := m\<rparr>) = measurable M1 M2"
- unfolding measurable_def by auto
-
-lemma measurable_cancel_measure1[simp]:
- "measurable (M1\<lparr>measure := m\<rparr>) M2 = measurable M1 M2"
- unfolding measurable_def by auto
-
lemma sigma_sets_subseteq: assumes "A \<subseteq> B" shows "sigma_sets X A \<subseteq> sigma_sets X B"
proof
fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B"
@@ -926,20 +918,27 @@
unfolding F_SUPR by simp
qed
+lemma (in pair_sigma_finite) measure_preserving_swap:
+ "(\<lambda>(x,y). (y, x)) \<in> measure_preserving (M1 \<Otimes>\<^isub>M M2) (M2 \<Otimes>\<^isub>M M1)"
+proof
+ interpret Q: pair_sigma_finite M2 M1 by default
+ show *: "(\<lambda>(x,y). (y, x)) \<in> measurable (M1 \<Otimes>\<^isub>M M2) (M2 \<Otimes>\<^isub>M M1)"
+ using pair_sigma_algebra_swap_measurable .
+ fix X assume "X \<in> sets (M2 \<Otimes>\<^isub>M M1)"
+ from measurable_sets[OF * this] this Q.sets_into_space[OF this]
+ show "measure (M1 \<Otimes>\<^isub>M M2) ((\<lambda>(x, y). (y, x)) -` X \<inter> space P) = measure (M2 \<Otimes>\<^isub>M M1) X"
+ by (auto intro!: M1.positive_integral_cong arg_cong[where f="M2.\<mu>"]
+ simp: pair_measure_alt Q.pair_measure_alt2 space_pair_measure)
+qed
+
lemma (in pair_sigma_finite) positive_integral_product_swap:
assumes f: "f \<in> borel_measurable P"
shows "(\<integral>\<^isup>+x. f (case x of (x,y)\<Rightarrow>(y,x)) \<partial>(M2 \<Otimes>\<^isub>M M1)) = integral\<^isup>P P f"
proof -
interpret Q: pair_sigma_finite M2 M1 by default
have "sigma_algebra P" by default
- show ?thesis
- proof (intro Q.positive_integral_vimage[symmetric] Q.pair_sigma_algebra_swap_measurable)
- fix A assume "A \<in> sets P"
- from Q.pair_sigma_algebra_swap_measurable[THEN measurable_sets, OF this] this sets_into_space[OF this]
- show "\<mu> A = Q.\<mu> ((\<lambda>(x, y). (y, x)) -` A \<inter> space (M2 \<Otimes>\<^isub>M M1))"
- by (auto intro!: M1.positive_integral_cong arg_cong[where f="M2.\<mu>"]
- simp: pair_measure_alt Q.pair_measure_alt2 space_pair_measure)
- qed fact+
+ with f show ?thesis
+ by (subst Q.positive_integral_vimage[OF _ Q.measure_preserving_swap]) auto
qed
lemma (in pair_sigma_finite) positive_integral_snd_measurable:
@@ -1405,7 +1404,8 @@
fix i k show "\<mu> i (F i k) \<noteq> \<omega>" by fact
next
fix A assume "A \<in> (\<Union>i. ?F i)" then show "A \<in> space G"
- using `\<And>i. range (F i) \<subseteq> sets (M i)` M.sets_into_space by auto blast
+ using `\<And>i. range (F i) \<subseteq> sets (M i)` M.sets_into_space
+ by (force simp: image_subset_iff)
next
fix f assume "f \<in> space G"
with Pi_UN[OF finite_index, of "\<lambda>k i. F i k"]
@@ -1418,6 +1418,19 @@
qed
qed
+lemma sets_pair_cancel_measure[simp]:
+ "sets (M1\<lparr>measure := m1\<rparr> \<Otimes>\<^isub>M M2) = sets (M1 \<Otimes>\<^isub>M M2)"
+ "sets (M1 \<Otimes>\<^isub>M M2\<lparr>measure := m2\<rparr>) = sets (M1 \<Otimes>\<^isub>M M2)"
+ unfolding pair_measure_def pair_measure_generator_def sets_sigma
+ by simp_all
+
+lemma measurable_pair_cancel_measure[simp]:
+ "measurable (M1\<lparr>measure := m1\<rparr> \<Otimes>\<^isub>M M2) M = measurable (M1 \<Otimes>\<^isub>M M2) M"
+ "measurable (M1 \<Otimes>\<^isub>M M2\<lparr>measure := m2\<rparr>) M = measurable (M1 \<Otimes>\<^isub>M M2) M"
+ "measurable M (M1\<lparr>measure := m3\<rparr> \<Otimes>\<^isub>M M2) = measurable M (M1 \<Otimes>\<^isub>M M2)"
+ "measurable M (M1 \<Otimes>\<^isub>M M2\<lparr>measure := m4\<rparr>) = measurable M (M1 \<Otimes>\<^isub>M M2)"
+ unfolding measurable_def by (auto simp add: space_pair_measure)
+
lemma (in product_sigma_finite) product_measure_exists:
assumes "finite I"
shows "\<exists>\<nu>. sigma_finite_measure (sigma (product_algebra_generator I M) \<lparr> measure := \<nu> \<rparr>) \<and>
@@ -1455,8 +1468,7 @@
by (rule I'.sigma_algebra_cong) simp_all
interpret I'': measure_space "I'.P\<lparr> measure := ?\<nu> \<rparr>"
using measurable_add_dim[OF `i \<notin> I`]
- by (intro P.measure_space_vimage[OF I'])
- (simp_all add: measurable_def pair_measure_def pair_measure_generator_def sets_sigma)
+ by (intro P.measure_space_vimage[OF I']) (auto simp add: measure_preserving_def)
show ?case
proof (intro exI[of _ ?\<nu>] conjI ballI)
let "?m A" = "measure (Pi\<^isub>M I M\<lparr>measure := \<nu>\<rparr> \<Otimes>\<^isub>M M i) (?h -` A \<inter> space P.P)"
@@ -1602,32 +1614,44 @@
qed
qed
+lemma (in product_sigma_finite) measure_preserving_merge:
+ assumes IJ: "I \<inter> J = {}" and "finite I" "finite J"
+ shows "(\<lambda>(x,y). merge I x J y) \<in> measure_preserving (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) (Pi\<^isub>M (I \<union> J) M)"
+ by (intro measure_preservingI measurable_merge[OF IJ] measure_fold[symmetric] assms)
+
lemma (in product_sigma_finite) product_positive_integral_fold:
- assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
+ assumes IJ[simp]: "I \<inter> J = {}" "finite I" "finite J"
and f: "f \<in> borel_measurable (Pi\<^isub>M (I \<union> J) M)"
shows "integral\<^isup>P (Pi\<^isub>M (I \<union> J) M) f =
(\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (merge I x J y) \<partial>(Pi\<^isub>M J M)) \<partial>(Pi\<^isub>M I M))"
proof -
interpret I: finite_product_sigma_finite M I by default fact
interpret J: finite_product_sigma_finite M J by default fact
- have "finite (I \<union> J)" using fin by auto
- interpret IJ: finite_product_sigma_finite M "I \<union> J" by default fact
- interpret P: pair_sigma_finite I.P J.P by default
+ interpret P: pair_sigma_finite "Pi\<^isub>M I M" "Pi\<^isub>M J M" by default
+ interpret IJ: finite_product_sigma_finite M "I \<union> J" by default simp
have P_borel: "(\<lambda>x. f (case x of (x, y) \<Rightarrow> merge I x J y)) \<in> borel_measurable P.P"
- using measurable_comp[OF measurable_merge[OF IJ] f] by (simp add: comp_def)
+ using measurable_comp[OF measurable_merge[OF IJ(1)] f] by (simp add: comp_def)
show ?thesis
unfolding P.positive_integral_fst_measurable[OF P_borel, simplified]
proof (rule P.positive_integral_vimage)
show "sigma_algebra IJ.P" by default
- show "(\<lambda>(x, y). merge I x J y) \<in> measurable P.P IJ.P" by (rule measurable_merge[OF IJ])
+ show "(\<lambda>(x, y). merge I x J y) \<in> measure_preserving P.P IJ.P"
+ using IJ by (rule measure_preserving_merge)
show "f \<in> borel_measurable IJ.P" using f by simp
- next
- fix A assume "A \<in> sets (Pi\<^isub>M (I \<union> J) M)"
- then show "IJ.\<mu> A = P.\<mu> ((\<lambda>(x,y). merge I x J y) -` A \<inter> space P.P)"
- using measure_fold[OF IJ fin] by simp
qed
qed
+lemma (in product_sigma_finite) measure_preserving_component_singelton:
+ "(\<lambda>x. x i) \<in> measure_preserving (Pi\<^isub>M {i} M) (M i)"
+proof (intro measure_preservingI measurable_component_singleton)
+ interpret I: finite_product_sigma_finite M "{i}" by default simp
+ fix A let ?P = "(\<lambda>x. x i) -` A \<inter> space I.P"
+ assume A: "A \<in> sets (M i)"
+ then have *: "?P = {i} \<rightarrow>\<^isub>E A" using sets_into_space by auto
+ show "I.\<mu> ?P = M.\<mu> i A" unfolding *
+ using A I.measure_times[of "\<lambda>_. A"] by auto
+qed auto
+
lemma (in product_sigma_finite) product_positive_integral_singleton:
assumes f: "f \<in> borel_measurable (M i)"
shows "integral\<^isup>P (Pi\<^isub>M {i} M) (\<lambda>x. f (x i)) = integral\<^isup>P (M i) f"
@@ -1636,14 +1660,9 @@
show ?thesis
proof (rule I.positive_integral_vimage[symmetric])
show "sigma_algebra (M i)" by (rule sigma_algebras)
- show "(\<lambda>x. x i) \<in> measurable (Pi\<^isub>M {i} M) (M i)" by (rule measurable_component_singleton) auto
+ show "(\<lambda>x. x i) \<in> measure_preserving (Pi\<^isub>M {i} M) (M i)"
+ by (rule measure_preserving_component_singelton)
show "f \<in> borel_measurable (M i)" by fact
- next
- fix A let ?P = "(\<lambda>x. x i) -` A \<inter> space I.P"
- assume A: "A \<in> sets (M i)"
- then have *: "?P = {i} \<rightarrow>\<^isub>E A" using sets_into_space by auto
- show "M.\<mu> i A = I.\<mu> ?P" unfolding *
- using A I.measure_times[of "\<lambda>_. A"] by auto
qed
qed
@@ -1723,14 +1742,14 @@
show ?thesis
proof (subst P.integrable_fst_measurable(2)[of ?f, simplified])
have 1: "sigma_algebra IJ.P" by default
- have 2: "?M \<in> measurable P.P IJ.P" using measurable_merge[OF IJ] .
- have 3: "\<And>A. A \<in> sets IJ.P \<Longrightarrow> IJ.\<mu> A = P.\<mu> (?M -` A \<inter> space P.P)"
- by (rule measure_fold[OF IJ fin])
- have 4: "integrable (Pi\<^isub>M (I \<union> J) M) f" by fact
+ have 2: "?M \<in> measure_preserving P.P IJ.P" using measure_preserving_merge[OF assms(1,2,3)] .
+ have 3: "integrable (Pi\<^isub>M (I \<union> J) M) f" by fact
+ then have 4: "f \<in> borel_measurable (Pi\<^isub>M (I \<union> J) M)"
+ by (simp add: integrable_def)
show "integrable P.P ?f"
- by (rule P.integral_vimage[where f=f, OF 1 2 3 4])
+ by (rule P.integrable_vimage[where f=f, OF 1 2 3])
show "integral\<^isup>L IJ.P f = integral\<^isup>L P.P ?f"
- by (rule P.integral_vimage[where f=f, OF 1 2 3 4])
+ by (rule P.integral_vimage[where f=f, OF 1 2 4])
qed
qed