# HG changeset patch # User hoelzl # Date 1298457612 -3600 # Node ID 91a2b435dd7a82299eb4cb09a7803e1a5e0f1924 # Parent 719b0a517c3382f0b6e0953a6f8f9eff8f9d2273 use measure_preserving in ..._vimage lemmas diff -r 719b0a517c33 -r 91a2b435dd7a src/HOL/Probability/Lebesgue_Integration.thy --- 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 \ measure_preserving A B \ X \ sets B \ measure A (T -` X \ space A) = measure B X" + unfolding measure_preserving_def by auto + lemma (in measure_space) simple_integral_vimage: - assumes T: "sigma_algebra M'" "T \ measurable M M'" + assumes T: "sigma_algebra M'" "T \ measure_preserving M M'" and f: "simple_function M' f" - and \: "\A. A \ sets M' \ measure M' A = \ (T -` A \ space M)" shows "integral\<^isup>S M' f = (\\<^isup>S x. f (T x) \M)" proof - - interpret T: measure_space M' using \ 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 = (\\<^isup>S x. f (T x) \M)" unfolding simple_integral_def proof (intro setsum_mono_zero_cong_right ballI) show "(\x. f (T x)) ` space M \ 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 \ f ` space M' - (\x. f (T x)) ` space M" then have "T -` (f -` {i} \ space M') \ space M = {}" by (auto simp: image_iff) - with f[THEN T.simple_functionD(2), THEN \] + with f[THEN T.simple_functionD(2), THEN measure_preservingD[OF T(2)], of "{i}"] show "i * T.\ (f -` {i} \ space M') = 0" by simp next fix i assume "i \ (\x. f (T x)) ` space M" then have "T -` (f -` {i} \ space M') \ space M = (\x. f (T x)) -` {i} \ space M" - using T unfolding measurable_def by auto - with f[THEN T.simple_functionD(2), THEN \] + 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.\ (f -` {i} \ space M') = i * \ ((\x. f (T x)) -` {i} \ space M)" by auto qed @@ -1195,20 +1198,23 @@ using positive_integral_isoton[OF `f \ u` e(1)[THEN borel_measurable_simple_function]] unfolding positive_integral_eq_simple_integral[OF e] . +lemma measure_preservingD2: + "f \ measure_preserving A B \ f \ measurable A B" + unfolding measure_preserving_def by auto + lemma (in measure_space) positive_integral_vimage: - assumes T: "sigma_algebra M'" "T \ measurable M M'" and f: "f \ borel_measurable M'" - and \: "\A. A \ sets M' \ measure M' A = \ (T -` A \ space M)" + assumes T: "sigma_algebra M'" "T \ measure_preserving M M'" and f: "f \ borel_measurable M'" shows "integral\<^isup>P M' f = (\\<^isup>+ x. f (T x) \M)" proof - - interpret T: measure_space M' using \ by (rule measure_space_vimage[OF T]) + interpret T: measure_space M' by (rule measure_space_vimage[OF T]) obtain f' where f': "f' \ f" "\i. simple_function M' (f' i)" using T.borel_measurable_implies_simple_function_sequence[OF f] by blast then have f: "(\i x. f' i (T x)) \ (\x. f (T x))" "\i. simple_function M (\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 = (\\<^isup>+ x. f (T x) \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) \] 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 \ measurable M M'" - and \: "\A. A \ sets M' \ measure M' A = \ (T -` A \ space M)" - assumes f: "integrable M' f" - shows "integrable M (\x. f (T x))" (is ?P) - and "integral\<^isup>L M' f = (\x. f (T x) \M)" (is ?I) + assumes T: "sigma_algebra M'" "T \ measure_preserving M M'" + assumes f: "f \ borel_measurable M'" + shows "integral\<^isup>L M' f = (\x. f (T x) \M)" proof - - interpret T: measure_space M' using \ 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: "(\x. Real (f x)) \ borel_measurable M'" "(\x. Real (- f x)) \ borel_measurable M'" and "(\x. f (T x)) \ 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 \]) + by (auto simp: borel[THEN positive_integral_vimage[OF T]]) +qed + +lemma (in measure_space) integrable_vimage: + assumes T: "sigma_algebra M'" "T \ measure_preserving M M'" + assumes f: "integrable M' f" + shows "integrable M (\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: "(\x. Real (f x)) \ borel_measurable M'" "(\x. Real (- f x)) \ borel_measurable M'" + and "(\x. f (T x)) \ 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]: diff -r 719b0a517c33 -r 91a2b435dd7a src/HOL/Probability/Lebesgue_Measure.thy --- 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 \ 'b::ordered_euclidean_space" - assumes "continuous_on UNIV f" - shows "f \ 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 \ (nat \ real)" where @@ -759,13 +752,13 @@ interpretation lborel_product: product_sigma_finite "\x. lborel::real measure_space" by default -interpretation lborel_space: finite_product_sigma_finite "\x. lborel::real measure_space" "{..x. lborel::real measure_space" "{.." and "measurable lborel = measurable borel" proof - - show "finite_product_sigma_finite (\x. lborel::real measure_space) {..x. lborel::real measure_space) {.. sets borel" - shows "lborel.\ A = lborel_space.\ TYPE('a) (p2e -` A \ (space (lborel_space.P TYPE('a))))" + shows "lborel.\ A = lborel_space.\ DIM('a) (p2e -` A \ (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 \ measure_preserving (\\<^isub>M i\{.. measure_preserving ?P ?E") +proof + show "p2e \ measurable ?P ?E" + using measurable_p2e by (simp add: measurable_def) + fix A :: "'a set" assume "A \ sets lborel" + then show "lborel_space.\ DIM('a) (p2e -` A \ (space (lborel_space.P DIM('a)))) = lborel.\ 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 \ sets borel" - shows "lebesgue.\ A = lborel_space.\ TYPE('a) (p2e -` A \ (space (lborel_space.P TYPE('a))))" + shows "lebesgue.\ A = lborel_space.\ DIM('a) (p2e -` A \ (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 \ pextreal" assumes f: "f \ borel_measurable borel" - shows "integral\<^isup>P lborel f = \\<^isup>+x. f (p2e x) \(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 \ measurable (lborel_space.P TYPE('a)) (lborel :: 'a measure_space)" - "f \ borel_measurable lborel" - using measurable_p2e f by (simp_all add: measurable_def) -qed simp + shows "integral\<^isup>P lborel f = \\<^isup>+x. f (p2e x) \(lborel_space.P DIM('a))" +proof (rule lborel_space.positive_integral_vimage[OF _ measure_preserving_p2e _]) + show "f \ borel_measurable lborel" + using f by (simp_all add: measurable_def) +qed default lemma borel_fubini_integrable: fixes f :: "'a::ordered_euclidean_space \ real" shows "integrable lborel f \ - integrable (lborel_space.P TYPE('a)) (\x. f (p2e x))" + integrable (lborel_space.P DIM('a)) (\x. f (p2e x))" (is "_ \ integrable ?B ?f") proof assume "integrable lborel f" @@ -916,7 +918,7 @@ lemma borel_fubini: fixes f :: "'a::ordered_euclidean_space \ real" assumes f: "f \ borel_measurable borel" - shows "integral\<^isup>L lborel f = \x. f (p2e x) \(lborel_space.P TYPE('a))" + shows "integral\<^isup>L lborel f = \x. f (p2e x) \(lborel_space.P DIM('a))" using f by (simp add: borel_fubini_positiv_integral lebesgue_integral_def) end diff -r 719b0a517c33 -r 91a2b435dd7a src/HOL/Probability/Measure.thy --- 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'\measure := m\) \ algebra M'" + unfolding algebra_def by simp + +lemma sigma_algebra_measure_update[simp]: + "sigma_algebra (M'\measure := m\) \ sigma_algebra M'" + unfolding sigma_algebra_def sigma_algebra_axioms_def by simp + +lemma finite_sigma_algebra_measure_update[simp]: + "finite_sigma_algebra (M'\measure := m\) \ finite_sigma_algebra M'" + unfolding finite_sigma_algebra_def finite_sigma_algebra_axioms_def by simp + +lemma measurable_cancel_measure[simp]: + "measurable M1 (M2\measure := m2\) = measurable M1 M2" + "measurable (M2\measure := m1\) M1 = measurable M2 M1" + unfolding measurable_def by auto + lemma inj_on_image_eq_iff: assumes "inj_on f S" assumes "A \ S" "B \ 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 \ measurable M M'" - and \: "\A. A \ sets M' \ measure M' A = \ (T -` A \ space M)" - shows "measure_space M'" -proof - - interpret M': sigma_algebra M' by fact - show ?thesis - proof - show "measure M' {} = 0" using \[of "{}"] by simp - - show "countably_additive M' (measure M')" - proof (intro countably_additiveI) - fix A :: "nat \ 'c set" assume "range A \ sets M'" "disjoint_family A" - then have A: "\i. A i \ sets M'" "(\i. A i) \ sets M'" by auto - then have *: "range (\i. T -` (A i) \ space M) \ sets M" - using `T \ measurable M M'` by (auto simp: measurable_def) - moreover have "(\i. T -` A i \ space M) \ sets M" - using * by blast - moreover have **: "disjoint_family (\i. T -` A i \ space M)" - using `disjoint_family A` by (auto simp: disjoint_family_on_def) - ultimately show "(\\<^isub>\ i. measure M' (A i)) = measure M' (\i. A i)" - using measure_countably_additive[OF _ **] A - by (auto simp: comp_def vimage_UN \) - qed - qed -qed - -lemma measure_unique_Int_stable_vimage: - fixes A :: "nat \ 'a set" - assumes E: "Int_stable E" - and A: "range A \ sets E" "A \ space E" "\i. measure M (A i) \ \" - and N: "measure_space N" "T \ measurable N M" - and M: "measure_space M" "sets (sigma E) = sets M" "space E = space M" - and eq: "\X. X \ sets E \ measure M X = measure N (T -` X \ space N)" - assumes X: "X \ sets (sigma E)" - shows "measure M X = measure N (T -` X \ 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 \ space N" - show "measure_space \space = space E, sets = sets (sigma E), measure = measure M\" - by (rule M.measure_space_cong) (auto simp: M) - show "measure_space \space = space E, sets = sets (sigma E), measure = \X. measure N (?T X)\" (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 \ measurable N ?E" - using `T \ measurable N M` by (auto simp: M measurable_def) - qed simp - show "\i. M.\ (A i) \ \" by fact -qed - section "@{text \}-null sets" abbreviation (in measure_space) "null_sets \ {N\sets M. \ N = 0}" @@ -991,6 +955,105 @@ qed force+ qed +section {* Measure preserving *} + +definition "measure_preserving A B = + {f \ measurable A B. (\y \ sets B. measure A (f -` y \ space A) = measure B y)}" + +lemma measure_preservingI[intro?]: + assumes "f \ measurable A B" + and "\y. y \ sets B \ measure A (f -` y \ space A) = measure B y" + shows "f \ 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 \ 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 \ 'c set" assume "range A \ sets M'" "disjoint_family A" + then have A: "\i. A i \ sets M'" "(\i. A i) \ sets M'" by auto + then have *: "range (\i. T -` (A i) \ space M) \ sets M" + using T by (auto simp: measurable_def measure_preserving_def) + moreover have "(\i. T -` A i \ space M) \ sets M" + using * by blast + moreover have **: "disjoint_family (\i. T -` A i \ space M)" + using `disjoint_family A` by (auto simp: disjoint_family_on_def) + ultimately show "(\\<^isub>\ i. measure M' (A i)) = measure M' (\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 \ 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 \ space M"]) auto +qed + +lemma measure_unique_Int_stable_vimage: + fixes A :: "nat \ 'a set" + assumes E: "Int_stable E" + and A: "range A \ sets E" "A \ space E" "\i. measure M (A i) \ \" + and N: "measure_space N" "T \ measurable N M" + and M: "measure_space M" "sets (sigma E) = sets M" "space E = space M" + and eq: "\X. X \ sets E \ measure M X = measure N (T -` X \ space N)" + assumes X: "X \ sets (sigma E)" + shows "measure M X = measure N (T -` X \ 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 \ space N" + show "measure_space \space = space E, sets = sets (sigma E), measure = measure M\" + by (rule M.measure_space_cong) (auto simp: M) + show "measure_space \space = space E, sets = sets (sigma E), measure = \X. measure N (?T X)\" (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 \ measure_preserving N ?E" + using `T \ measurable N M` by (auto simp: M measurable_def measure_preserving_def) + qed + show "\i. M.\ (A i) \ \" by fact +qed + +lemma (in measure_space) measure_preserving_Int_stable: + fixes A :: "nat \ 'a set" + assumes E: "Int_stable E" "range A \ sets E" "A \ space E" "\i. measure E (A i) \ \" + and N: "measure_space (sigma E)" + and T: "T \ measure_preserving M E" + shows "T \ measure_preserving M (sigma E)" +proof + interpret E: measure_space "sigma E" by fact + show "T \ 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 \ sets (sigma E)" + show "\ (T -` X \ space M) = E.\ X" + proof (rule measure_unique_Int_stable_vimage[symmetric]) + show "sets (sigma E) = sets (sigma E)" "space E = space (sigma E)" + "\i. E.\ (A i) \ \" using E by auto + show "measure_space M" by default + next + fix X assume "X \ sets E" then show "E.\ X = \ (T -` X \ 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 \ measurable A B. (\y \ sets B. measure A (f -` y \ space A) = measure B y)}" - lemma (in finite_measure) measure_preserving_lift: fixes f :: "'a \ 'c" and A :: "('c, 'd) measure_space_scheme" assumes "algebra A" "finite_measure (sigma A)" (is "finite_measure ?sA") diff -r 719b0a517c33 -r 91a2b435dd7a src/HOL/Probability/Probability_Space.thy --- 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\measure := distribution X\" 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 \ space M = space M" diff -r 719b0a517c33 -r 91a2b435dd7a src/HOL/Probability/Product_Measure.thy --- 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\measure := m\) = measurable M1 M2" - unfolding measurable_def by auto - -lemma measurable_cancel_measure1[simp]: - "measurable (M1\measure := m\) M2 = measurable M1 M2" - unfolding measurable_def by auto - lemma sigma_sets_subseteq: assumes "A \ B" shows "sigma_sets X A \ sigma_sets X B" proof fix x assume "x \ sigma_sets X A" then show "x \ sigma_sets X B" @@ -926,20 +918,27 @@ unfolding F_SUPR by simp qed +lemma (in pair_sigma_finite) measure_preserving_swap: + "(\(x,y). (y, x)) \ measure_preserving (M1 \\<^isub>M M2) (M2 \\<^isub>M M1)" +proof + interpret Q: pair_sigma_finite M2 M1 by default + show *: "(\(x,y). (y, x)) \ measurable (M1 \\<^isub>M M2) (M2 \\<^isub>M M1)" + using pair_sigma_algebra_swap_measurable . + fix X assume "X \ sets (M2 \\<^isub>M M1)" + from measurable_sets[OF * this] this Q.sets_into_space[OF this] + show "measure (M1 \\<^isub>M M2) ((\(x, y). (y, x)) -` X \ space P) = measure (M2 \\<^isub>M M1) X" + by (auto intro!: M1.positive_integral_cong arg_cong[where f="M2.\"] + simp: pair_measure_alt Q.pair_measure_alt2 space_pair_measure) +qed + lemma (in pair_sigma_finite) positive_integral_product_swap: assumes f: "f \ borel_measurable P" shows "(\\<^isup>+x. f (case x of (x,y)\(y,x)) \(M2 \\<^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 \ sets P" - from Q.pair_sigma_algebra_swap_measurable[THEN measurable_sets, OF this] this sets_into_space[OF this] - show "\ A = Q.\ ((\(x, y). (y, x)) -` A \ space (M2 \\<^isub>M M1))" - by (auto intro!: M1.positive_integral_cong arg_cong[where f="M2.\"] - 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 "\ i (F i k) \ \" by fact next fix A assume "A \ (\i. ?F i)" then show "A \ space G" - using `\i. range (F i) \ sets (M i)` M.sets_into_space by auto blast + using `\i. range (F i) \ sets (M i)` M.sets_into_space + by (force simp: image_subset_iff) next fix f assume "f \ space G" with Pi_UN[OF finite_index, of "\k i. F i k"] @@ -1418,6 +1418,19 @@ qed qed +lemma sets_pair_cancel_measure[simp]: + "sets (M1\measure := m1\ \\<^isub>M M2) = sets (M1 \\<^isub>M M2)" + "sets (M1 \\<^isub>M M2\measure := m2\) = sets (M1 \\<^isub>M M2)" + unfolding pair_measure_def pair_measure_generator_def sets_sigma + by simp_all + +lemma measurable_pair_cancel_measure[simp]: + "measurable (M1\measure := m1\ \\<^isub>M M2) M = measurable (M1 \\<^isub>M M2) M" + "measurable (M1 \\<^isub>M M2\measure := m2\) M = measurable (M1 \\<^isub>M M2) M" + "measurable M (M1\measure := m3\ \\<^isub>M M2) = measurable M (M1 \\<^isub>M M2)" + "measurable M (M1 \\<^isub>M M2\measure := m4\) = measurable M (M1 \\<^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 "\\. sigma_finite_measure (sigma (product_algebra_generator I M) \ measure := \ \) \ @@ -1455,8 +1468,7 @@ by (rule I'.sigma_algebra_cong) simp_all interpret I'': measure_space "I'.P\ measure := ?\ \" using measurable_add_dim[OF `i \ 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 _ ?\] conjI ballI) let "?m A" = "measure (Pi\<^isub>M I M\measure := \\ \\<^isub>M M i) (?h -` A \ space P.P)" @@ -1602,32 +1614,44 @@ qed qed +lemma (in product_sigma_finite) measure_preserving_merge: + assumes IJ: "I \ J = {}" and "finite I" "finite J" + shows "(\(x,y). merge I x J y) \ measure_preserving (Pi\<^isub>M I M \\<^isub>M Pi\<^isub>M J M) (Pi\<^isub>M (I \ 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 \ J = {}" and fin: "finite I" "finite J" + assumes IJ[simp]: "I \ J = {}" "finite I" "finite J" and f: "f \ borel_measurable (Pi\<^isub>M (I \ J) M)" shows "integral\<^isup>P (Pi\<^isub>M (I \