# HG changeset patch # User hoelzl # Date 1422011067 -3600 # Node ID 6fca83e88417587b325ece8765405873f1f3b2e9 # Parent c5e79df8cc21363647eb020efad99aa34bbe7874 integral of the product of count spaces equals the integral of the count space of the product type diff -r c5e79df8cc21 -r 6fca83e88417 src/HOL/Probability/Binary_Product_Measure.thy --- a/src/HOL/Probability/Binary_Product_Measure.thy Thu Jan 22 14:51:08 2015 +0100 +++ b/src/HOL/Probability/Binary_Product_Measure.thy Fri Jan 23 12:04:27 2015 +0100 @@ -730,6 +730,112 @@ done qed + +lemma emeasure_prod_count_space: + assumes A: "A \ sets (count_space UNIV \\<^sub>M M)" (is "A \ sets (?A \\<^sub>M ?B)") + shows "emeasure (?A \\<^sub>M ?B) A = (\\<^sup>+ x. \\<^sup>+ y. indicator A (x, y) \?B \?A)" + by (rule emeasure_measure_of[OF pair_measure_def]) + (auto simp: countably_additive_def positive_def suminf_indicator nn_integral_nonneg A + nn_integral_suminf[symmetric] dest: sets.sets_into_space) + +lemma emeasure_prod_count_space_single[simp]: "emeasure (count_space UNIV \\<^sub>M count_space UNIV) {x} = 1" +proof - + have [simp]: "\a b x y. indicator {(a, b)} (x, y) = (indicator {a} x * indicator {b} y::ereal)" + by (auto split: split_indicator) + show ?thesis + by (cases x) + (auto simp: emeasure_prod_count_space nn_integral_cmult sets_Pair nn_integral_max_0 one_ereal_def[symmetric]) +qed + +lemma emeasure_count_space_prod_eq: + fixes A :: "('a \ 'b) set" + assumes A: "A \ sets (count_space UNIV \\<^sub>M count_space UNIV)" (is "A \ sets (?A \\<^sub>M ?B)") + shows "emeasure (?A \\<^sub>M ?B) A = emeasure (count_space UNIV) A" +proof - + { fix A :: "('a \ 'b) set" assume "countable A" + then have "emeasure (?A \\<^sub>M ?B) (\a\A. {a}) = (\\<^sup>+a. emeasure (?A \\<^sub>M ?B) {a} \count_space A)" + by (intro emeasure_UN_countable) (auto simp: sets_Pair disjoint_family_on_def) + also have "\ = (\\<^sup>+a. indicator A a \count_space UNIV)" + by (subst nn_integral_count_space_indicator) auto + finally have "emeasure (?A \\<^sub>M ?B) A = emeasure (count_space UNIV) A" + by simp } + note * = this + + show ?thesis + proof cases + assume "finite A" then show ?thesis + by (intro * countable_finite) + next + assume "infinite A" + then obtain C where "countable C" and "infinite C" and "C \ A" + by (auto dest: infinite_countable_subset') + with A have "emeasure (?A \\<^sub>M ?B) C \ emeasure (?A \\<^sub>M ?B) A" + by (intro emeasure_mono) auto + also have "emeasure (?A \\<^sub>M ?B) C = emeasure (count_space UNIV) C" + using `countable C` by (rule *) + finally show ?thesis + using `infinite C` `infinite A` by simp + qed +qed + +lemma nn_intergal_count_space_prod_eq': + assumes [simp]: "\x. 0 \ f x" + shows "nn_integral (count_space UNIV \\<^sub>M count_space UNIV) f = nn_integral (count_space UNIV) f" + (is "nn_integral ?P f = _") +proof cases + assume cntbl: "countable {x. f x \ 0}" + have [simp]: "\x. ereal (real (card ({x} \ {x. f x \ 0}))) = indicator {x. f x \ 0} x" + by (auto split: split_indicator) + have [measurable]: "\y. (\x. indicator {y} x) \ borel_measurable ?P" + by (rule measurable_discrete_difference[of "\x. 0" _ borel "{y}" "\x. indicator {y} x" for y]) + (auto intro: sets_Pair) + + have "(\\<^sup>+x. f x \?P) = (\\<^sup>+x. \\<^sup>+x'. f x * indicator {x} x' \count_space {x. f x \ 0} \?P)" + by (auto simp add: nn_integral_cmult nn_integral_indicator' intro!: nn_integral_cong split: split_indicator) + also have "\ = (\\<^sup>+x. \\<^sup>+x'. f x' * indicator {x'} x \count_space {x. f x \ 0} \?P)" + by (auto intro!: nn_integral_cong split: split_indicator) + also have "\ = (\\<^sup>+x'. \\<^sup>+x. f x' * indicator {x'} x \?P \count_space {x. f x \ 0})" + by (intro nn_integral_count_space_nn_integral cntbl) auto + also have "\ = (\\<^sup>+x'. f x' \count_space {x. f x \ 0})" + by (intro nn_integral_cong) (auto simp: nn_integral_cmult sets_Pair) + finally show ?thesis + by (auto simp add: nn_integral_count_space_indicator intro!: nn_integral_cong split: split_indicator) +next + { fix x assume "f x \ 0" + with `0 \ f x` have "(\r. 0 < r \ f x = ereal r) \ f x = \" + by (cases "f x") (auto simp: less_le) + then have "\n. ereal (1 / real (Suc n)) \ f x" + by (auto elim!: nat_approx_posE intro!: less_imp_le) } + note * = this + + assume cntbl: "uncountable {x. f x \ 0}" + also have "{x. f x \ 0} = (\n. {x. 1/Suc n \ f x})" + using * by auto + finally obtain n where "infinite {x. 1/Suc n \ f x}" + by (meson countableI_type countable_UN uncountable_infinite) + then obtain C where C: "C \ {x. 1/Suc n \ f x}" and "countable C" "infinite C" + by (metis infinite_countable_subset') + + have [measurable]: "C \ sets ?P" + using sets.countable[OF _ `countable C`, of ?P] by (auto simp: sets_Pair) + + have "(\\<^sup>+x. ereal (1/Suc n) * indicator C x \?P) \ nn_integral ?P f" + using C by (intro nn_integral_mono) (auto split: split_indicator simp: zero_ereal_def[symmetric]) + moreover have "(\\<^sup>+x. ereal (1/Suc n) * indicator C x \?P) = \" + using `infinite C` by (simp add: nn_integral_cmult emeasure_count_space_prod_eq) + moreover have "(\\<^sup>+x. ereal (1/Suc n) * indicator C x \count_space UNIV) \ nn_integral (count_space UNIV) f" + using C by (intro nn_integral_mono) (auto split: split_indicator simp: zero_ereal_def[symmetric]) + moreover have "(\\<^sup>+x. ereal (1/Suc n) * indicator C x \count_space UNIV) = \" + using `infinite C` by (simp add: nn_integral_cmult) + ultimately show ?thesis + by simp +qed + +lemma nn_intergal_count_space_prod_eq: + "nn_integral (count_space UNIV \\<^sub>M count_space UNIV) f = nn_integral (count_space UNIV) f" + by (subst (1 2) nn_integral_max_0[symmetric]) (auto intro!: nn_intergal_count_space_prod_eq') + + lemma pair_measure_density: assumes f: "f \ borel_measurable M1" "AE x in M1. 0 \ f x" assumes g: "g \ borel_measurable M2" "AE x in M2. 0 \ g x" diff -r c5e79df8cc21 -r 6fca83e88417 src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy --- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Thu Jan 22 14:51:08 2015 +0100 +++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Fri Jan 23 12:04:27 2015 +0100 @@ -9,6 +9,14 @@ imports Measure_Space Borel_Space begin +lemma infinite_countable_subset': + assumes X: "infinite X" shows "\C\X. countable C \ infinite C" +proof - + from infinite_countable_subset[OF X] guess f .. + then show ?thesis + by (intro exI[of _ "range f"]) (auto simp: range_inj_infinite) +qed + lemma indicator_less_ereal[simp]: "indicator A x \ (indicator B x::ereal) \ (x \ A \ x \ B)" by (simp add: indicator_def not_le) @@ -836,6 +844,10 @@ "(\x. x \ space M \ u x = v x) \ integral\<^sup>N M u = integral\<^sup>N M v" by (auto intro: nn_integral_cong_AE) +lemma nn_integral_cong_simp: + "(\x. x \ space M =simp=> u x = v x) \ integral\<^sup>N M u = integral\<^sup>N M v" + by (auto intro: nn_integral_cong simp: simp_implies_def) + lemma nn_integral_cong_strong: "M = N \ (\x. x \ space M \ u x = v x) \ integral\<^sup>N M u = integral\<^sup>N N v" by (auto intro: nn_integral_cong) @@ -1724,58 +1736,6 @@ finally show ?thesis . qed -lemma emeasure_UN_countable: - assumes sets: "\i. i \ I \ X i \ sets M" and I: "countable I" - assumes disj: "disjoint_family_on X I" - shows "emeasure M (UNION I X) = (\\<^sup>+i. emeasure M (X i) \count_space I)" -proof cases - assume "finite I" with sets disj show ?thesis - by (subst setsum_emeasure[symmetric]) - (auto intro!: setsum.cong simp add: max_def subset_eq nn_integral_count_space_finite emeasure_nonneg) -next - assume f: "\ finite I" - then have [intro]: "I \ {}" by auto - from from_nat_into_inj_infinite[OF I f] from_nat_into[OF this] disj - have disj2: "disjoint_family (\i. X (from_nat_into I i))" - unfolding disjoint_family_on_def by metis - - from f have "bij_betw (from_nat_into I) UNIV I" - using bij_betw_from_nat_into[OF I] by simp - then have "(\i\I. X i) = (\i. (X \ from_nat_into I) i)" - unfolding SUP_def image_comp [symmetric] by (simp add: bij_betw_def) - then have "emeasure M (UNION I X) = emeasure M (\i. X (from_nat_into I i))" - by simp - also have "\ = (\i. emeasure M (X (from_nat_into I i)))" - by (intro suminf_emeasure[symmetric] disj disj2) (auto intro!: sets from_nat_into[OF `I \ {}`]) - also have "\ = (\n. \\<^sup>+i. emeasure M (X i) * indicator {from_nat_into I n} i \count_space I)" - proof (intro arg_cong[where f=suminf] ext) - fix i - have eq: "{a \ I. 0 < emeasure M (X a) * indicator {from_nat_into I i} a} - = (if 0 < emeasure M (X (from_nat_into I i)) then {from_nat_into I i} else {})" - using ereal_0_less_1 - by (auto simp: ereal_zero_less_0_iff indicator_def from_nat_into `I \ {}` simp del: ereal_0_less_1) - have "(\\<^sup>+ ia. emeasure M (X ia) * indicator {from_nat_into I i} ia \count_space I) = - (if 0 < emeasure M (X (from_nat_into I i)) then emeasure M (X (from_nat_into I i)) else 0)" - by (subst nn_integral_count_space) (simp_all add: eq) - also have "\ = emeasure M (X (from_nat_into I i))" - by (simp add: less_le emeasure_nonneg) - finally show "emeasure M (X (from_nat_into I i)) = - \\<^sup>+ ia. emeasure M (X ia) * indicator {from_nat_into I i} ia \count_space I" .. - qed - also have "\ = (\\<^sup>+i. emeasure M (X i) \count_space I)" - apply (subst nn_integral_suminf[symmetric]) - apply (auto simp: emeasure_nonneg intro!: nn_integral_cong) - proof - - fix x assume "x \ I" - then have "(\i. emeasure M (X x) * indicator {from_nat_into I i} x) = (\i\{to_nat_on I x}. emeasure M (X x) * indicator {from_nat_into I i} x)" - by (intro suminf_finite) (auto simp: indicator_def I f) - also have "\ = emeasure M (X x)" - by (simp add: I f `x\I`) - finally show "(\i. emeasure M (X x) * indicator {from_nat_into I i} x) = emeasure M (X x)" . - qed - finally show ?thesis . -qed - lemma nn_integral_count_space_nat: fixes f :: "nat \ ereal" assumes nonneg: "\i. 0 \ f i" @@ -1798,6 +1758,53 @@ finally show ?thesis . qed +lemma nn_integral_count_space_nn_integral: + fixes f :: "'i \ 'a \ ereal" + assumes "countable I" and [measurable]: "\i. i \ I \ f i \ borel_measurable M" + shows "(\\<^sup>+x. \\<^sup>+i. f i x \count_space I \M) = (\\<^sup>+i. \\<^sup>+x. f i x \M \count_space I)" +proof cases + assume "finite I" then show ?thesis + by (simp add: nn_integral_count_space_finite nn_integral_nonneg max.absorb2 nn_integral_setsum + nn_integral_max_0) +next + assume "infinite I" + then have [simp]: "I \ {}" + by auto + note * = bij_betw_from_nat_into[OF `countable I` `infinite I`] + have **: "\f. (\i. 0 \ f i) \ (\\<^sup>+i. f i \count_space I) = (\n. f (from_nat_into I n))" + by (simp add: nn_integral_bij_count_space[symmetric, OF *] nn_integral_count_space_nat) + show ?thesis + apply (subst (2) nn_integral_max_0[symmetric]) + apply (simp add: ** nn_integral_nonneg nn_integral_suminf from_nat_into) + apply (simp add: nn_integral_max_0) + done +qed + +lemma emeasure_UN_countable: + assumes sets[measurable]: "\i. i \ I \ X i \ sets M" and I[simp]: "countable I" + assumes disj: "disjoint_family_on X I" + shows "emeasure M (UNION I X) = (\\<^sup>+i. emeasure M (X i) \count_space I)" +proof - + have eq: "\x. indicator (UNION I X) x = \\<^sup>+ i. indicator (X i) x \count_space I" + proof cases + fix x assume x: "x \ UNION I X" + then obtain j where j: "x \ X j" "j \ I" + by auto + with disj have "\i. i \ I \ indicator (X i) x = (indicator {j} i::ereal)" + by (auto simp: disjoint_family_on_def split: split_indicator) + with x j show "?thesis x" + by (simp cong: nn_integral_cong_simp) + qed (auto simp: nn_integral_0_iff_AE) + + note sets.countable_UN'[unfolded subset_eq, measurable] + have "emeasure M (UNION I X) = (\\<^sup>+x. indicator (UNION I X) x \M)" + by simp + also have "\ = (\\<^sup>+i. \\<^sup>+x. indicator (X i) x \M \count_space I)" + by (simp add: eq nn_integral_count_space_nn_integral) + finally show ?thesis + by (simp cong: nn_integral_cong_simp) +qed + lemma emeasure_countable_singleton: assumes sets: "\x. x \ X \ {x} \ sets M" and X: "countable X" shows "emeasure M X = (\\<^sup>+x. emeasure M {x} \count_space X)"