# HG changeset patch # User hoelzl # Date 1423573617 -3600 # Node ID 6faf024a189368f11882e05f5ffb9788dadcaadb # Parent 03944a830c4a0d5fe35d19bc6033b1bdbdc8d9e0# Parent ef195926dd981c95a0c97e528723cb32c325ad5d merged diff -r 03944a830c4a -r 6faf024a1893 src/HOL/Library/Infinite_Set.thy --- a/src/HOL/Library/Infinite_Set.thy Tue Feb 10 13:50:30 2015 +0100 +++ b/src/HOL/Library/Infinite_Set.thy Tue Feb 10 14:06:57 2015 +0100 @@ -143,23 +143,33 @@ contains some element that occurs infinitely often. *} +lemma inf_img_fin_dom': + assumes img: "finite (f ` A)" and dom: "infinite A" + shows "\y \ f ` A. infinite (f -` {y} \ A)" +proof (rule ccontr) + have "A \ (\y\f ` A. f -` {y} \ A)" by auto + moreover + assume "\ ?thesis" + with img have "finite (\y\f ` A. f -` {y} \ A)" by blast + ultimately have "finite A" by(rule finite_subset) + with dom show False by contradiction +qed + +lemma inf_img_fin_domE': + assumes "finite (f ` A)" and "infinite A" + obtains y where "y \ f`A" and "infinite (f -` {y} \ A)" + using assms by (blast dest: inf_img_fin_dom') + lemma inf_img_fin_dom: assumes img: "finite (f`A)" and dom: "infinite A" shows "\y \ f`A. infinite (f -` {y})" -proof (rule ccontr) - assume "\ ?thesis" - with img have "finite (UN y:f`A. f -` {y})" by blast - moreover have "A \ (UN y:f`A. f -` {y})" by auto - moreover note dom - ultimately show False by (simp add: infinite_super) -qed +using inf_img_fin_dom'[OF assms] by auto lemma inf_img_fin_domE: assumes "finite (f`A)" and "infinite A" obtains y where "y \ f`A" and "infinite (f -` {y})" using assms by (blast dest: inf_img_fin_dom) - subsection "Infinitely Many and Almost All" text {* diff -r 03944a830c4a -r 6faf024a1893 src/HOL/Probability/Binary_Product_Measure.thy --- a/src/HOL/Probability/Binary_Product_Measure.thy Tue Feb 10 13:50:30 2015 +0100 +++ b/src/HOL/Probability/Binary_Product_Measure.thy Tue Feb 10 14:06:57 2015 +0100 @@ -835,7 +835,6 @@ "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" @@ -957,6 +956,106 @@ by (subst (1 2 3) emeasure_count_space) (auto simp: finite_cartesian_product_iff) qed +lemma nn_integral_fst_count_space': + assumes nonneg: "\xy. 0 \ f xy" + shows "(\\<^sup>+ x. \\<^sup>+ y. f (x, y) \count_space UNIV \count_space UNIV) = integral\<^sup>N (count_space UNIV) f" + (is "?lhs = ?rhs") +proof(cases) + assume *: "countable {xy. f xy \ 0}" + let ?A = "fst ` {xy. f xy \ 0}" + let ?B = "snd ` {xy. f xy \ 0}" + from * have [simp]: "countable ?A" "countable ?B" by(rule countable_image)+ + from nonneg have f_neq_0: "\xy. f xy \ 0 \ f xy > 0" + by(auto simp add: order.order_iff_strict) + have "?lhs = (\\<^sup>+ x. \\<^sup>+ y. f (x, y) \count_space UNIV \count_space ?A)" + by(rule nn_integral_count_space_eq) + (auto simp add: f_neq_0 nn_integral_0_iff_AE AE_count_space not_le intro: rev_image_eqI) + also have "\ = (\\<^sup>+ x. \\<^sup>+ y. f (x, y) \count_space ?B \count_space ?A)" + by(intro nn_integral_count_space_eq nn_integral_cong)(auto intro: rev_image_eqI) + also have "\ = (\\<^sup>+ xy. f xy \count_space (?A \ ?B))" + by(subst sigma_finite_measure.nn_integral_fst) + (simp_all add: sigma_finite_measure_count_space_countable pair_measure_countable) + also have "\ = ?rhs" + by(rule nn_integral_count_space_eq)(auto intro: rev_image_eqI) + finally show ?thesis . +next + { fix xy assume "f xy \ 0" + with `0 \ f xy` have "(\r. 0 < r \ f xy = ereal r) \ f xy = \" + by (cases "f xy") (auto simp: less_le) + then have "\n. ereal (1 / real (Suc n)) \ f xy" + by (auto elim!: nat_approx_posE intro!: less_imp_le) } + note * = this + + assume cntbl: "uncountable {xy. f xy \ 0}" + also have "{xy. f xy \ 0} = (\n. {xy. 1/Suc n \ f xy})" + using * by auto + finally obtain n where "infinite {xy. 1/Suc n \ f xy}" + by (meson countableI_type countable_UN uncountable_infinite) + then obtain C where C: "C \ {xy. 1/Suc n \ f xy}" and "countable C" "infinite C" + by (metis infinite_countable_subset') + + have "\ = (\\<^sup>+ xy. ereal (1 / Suc n) * indicator C xy \count_space UNIV)" + using \infinite C\ by(simp add: nn_integral_cmult) + also have "\ \ ?rhs" using C + by(intro nn_integral_mono)(auto split: split_indicator simp add: nonneg) + finally have "?rhs = \" by simp + moreover have "?lhs = \" + proof(cases "finite (fst ` C)") + case True + then obtain x C' where x: "x \ fst ` C" + and C': "C' = fst -` {x} \ C" + and "infinite C'" + using \infinite C\ by(auto elim!: inf_img_fin_domE') + from x C C' have **: "C' \ {xy. 1 / Suc n \ f xy}" by auto + + from C' \infinite C'\ have "infinite (snd ` C')" + by(auto dest!: finite_imageD simp add: inj_on_def) + then have "\ = (\\<^sup>+ y. ereal (1 / Suc n) * indicator (snd ` C') y \count_space UNIV)" + by(simp add: nn_integral_cmult) + also have "\ = (\\<^sup>+ y. ereal (1 / Suc n) * indicator C' (x, y) \count_space UNIV)" + by(rule nn_integral_cong)(force split: split_indicator intro: rev_image_eqI simp add: C') + also have "\ = (\\<^sup>+ x'. (\\<^sup>+ y. ereal (1 / Suc n) * indicator C' (x, y) \count_space UNIV) * indicator {x} x' \count_space UNIV)" + by(simp add: one_ereal_def[symmetric] nn_integral_nonneg nn_integral_cmult_indicator) + also have "\ \ (\\<^sup>+ x. \\<^sup>+ y. ereal (1 / Suc n) * indicator C' (x, y) \count_space UNIV \count_space UNIV)" + by(rule nn_integral_mono)(simp split: split_indicator add: nn_integral_nonneg) + also have "\ \ ?lhs" using ** + by(intro nn_integral_mono)(auto split: split_indicator simp add: nonneg) + finally show ?thesis by simp + next + case False + def C' \ "fst ` C" + have "\ = \\<^sup>+ x. ereal (1 / Suc n) * indicator C' x \count_space UNIV" + using C'_def False by(simp add: nn_integral_cmult) + also have "\ = \\<^sup>+ x. \\<^sup>+ y. ereal (1 / Suc n) * indicator C' x * indicator {SOME y. (x, y) \ C} y \count_space UNIV \count_space UNIV" + by(auto simp add: one_ereal_def[symmetric] nn_integral_cmult_indicator intro: nn_integral_cong) + also have "\ \ \\<^sup>+ x. \\<^sup>+ y. ereal (1 / Suc n) * indicator C (x, y) \count_space UNIV \count_space UNIV" + by(intro nn_integral_mono)(auto simp add: C'_def split: split_indicator intro: someI) + also have "\ \ ?lhs" using C + by(intro nn_integral_mono)(auto split: split_indicator simp add: nonneg) + finally show ?thesis by simp + qed + ultimately show ?thesis by simp +qed + +lemma nn_integral_fst_count_space: + "(\\<^sup>+ x. \\<^sup>+ y. f (x, y) \count_space UNIV \count_space UNIV) = integral\<^sup>N (count_space UNIV) f" +by(subst (2 3) nn_integral_max_0[symmetric])(rule nn_integral_fst_count_space', simp) + +lemma nn_integral_snd_count_space: + "(\\<^sup>+ y. \\<^sup>+ x. f (x, y) \count_space UNIV \count_space UNIV) = integral\<^sup>N (count_space UNIV) f" + (is "?lhs = ?rhs") +proof - + have "?lhs = (\\<^sup>+ y. \\<^sup>+ x. (\(y, x). f (x, y)) (y, x) \count_space UNIV \count_space UNIV)" + by(simp) + also have "\ = \\<^sup>+ yx. (\(y, x). f (x, y)) yx \count_space UNIV" + by(rule nn_integral_fst_count_space) + also have "\ = \\<^sup>+ xy. f xy \count_space ((\(x, y). (y, x)) ` UNIV)" + by(subst nn_integral_bij_count_space[OF inj_on_imp_bij_betw, symmetric]) + (simp_all add: inj_on_def split_def) + also have "\ = ?rhs" by(rule nn_integral_count_space_eq) auto + finally show ?thesis . +qed + subsection {* Product of Borel spaces *} lemma borel_Times: diff -r 03944a830c4a -r 6faf024a1893 src/HOL/Probability/Probability_Mass_Function.thy --- a/src/HOL/Probability/Probability_Mass_Function.thy Tue Feb 10 13:50:30 2015 +0100 +++ b/src/HOL/Probability/Probability_Mass_Function.thy Tue Feb 10 14:06:57 2015 +0100 @@ -282,6 +282,9 @@ using measure_pmf.emeasure_space_1 by simp qed +lemma emeasure_pmf_UNIV [simp]: "emeasure (measure_pmf M) UNIV = 1" +using measure_pmf.emeasure_space_1[of M] by simp + lemma in_null_sets_measure_pmfI: "A \ set_pmf p = {} \ A \ null_sets (measure_pmf p)" using emeasure_eq_0_AE[where ?P="\x. x \ A" and M="measure_pmf p"]