summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | hoelzl |

Wed, 23 Feb 2011 11:40:12 +0100 | |

changeset 41831 | 91a2b435dd7a |

parent 41830 | 719b0a517c33 |

child 41832 | 27cb9113b1a0 |

use measure_preserving in ..._vimage lemmas

--- 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