# 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 "\<exists>y \<in> f ` A. infinite (f -` {y} \<inter> A)"
+proof (rule ccontr)
+  have "A \<subseteq> (\<Union>y\<in>f ` A. f -` {y} \<inter> A)" by auto
+  moreover
+  assume "\<not> ?thesis"
+  with img have "finite (\<Union>y\<in>f ` A. f -` {y} \<inter> 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 \<in> f`A" and "infinite (f -` {y} \<inter> 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 "\<exists>y \<in> f`A. infinite (f -` {y})"
-proof (rule ccontr)
-  assume "\<not> ?thesis"
-  with img have "finite (UN y:f`A. f -` {y})" by blast
-  moreover have "A \<subseteq> (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 \<in> 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 \<Otimes>\<^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 \<in> borel_measurable M1" "AE x in M1. 0 \<le> f x"
   assumes g: "g \<in> borel_measurable M2" "AE x in M2. 0 \<le> 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: "\<And>xy. 0 \<le> f xy"
+  shows "(\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. f (x, y) \<partial>count_space UNIV \<partial>count_space UNIV) = integral\<^sup>N (count_space UNIV) f"
+  (is "?lhs = ?rhs")
+proof(cases)
+  assume *: "countable {xy. f xy \<noteq> 0}"
+  let ?A = "fst ` {xy. f xy \<noteq> 0}"
+  let ?B = "snd ` {xy. f xy \<noteq> 0}"
+  from * have [simp]: "countable ?A" "countable ?B" by(rule countable_image)+
+  from nonneg have f_neq_0: "\<And>xy. f xy \<noteq> 0 \<longleftrightarrow> f xy > 0"
+    by(auto simp add: order.order_iff_strict)
+  have "?lhs = (\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. f (x, y) \<partial>count_space UNIV \<partial>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 "\<dots> = (\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. f (x, y) \<partial>count_space ?B \<partial>count_space ?A)"
+    by(intro nn_integral_count_space_eq nn_integral_cong)(auto intro: rev_image_eqI)
+  also have "\<dots> = (\<integral>\<^sup>+ xy. f xy \<partial>count_space (?A \<times> ?B))"
+    by(subst sigma_finite_measure.nn_integral_fst)
+      (simp_all add: sigma_finite_measure_count_space_countable pair_measure_countable)
+  also have "\<dots> = ?rhs"
+    by(rule nn_integral_count_space_eq)(auto intro: rev_image_eqI)
+  finally show ?thesis .
+next
+  { fix xy assume "f xy \<noteq> 0"
+    with `0 \<le> f xy` have "(\<exists>r. 0 < r \<and> f xy = ereal r) \<or> f xy = \<infinity>"
+      by (cases "f xy") (auto simp: less_le)
+    then have "\<exists>n. ereal (1 / real (Suc n)) \<le> f xy"
+      by (auto elim!: nat_approx_posE intro!: less_imp_le) }
+  note * = this
+
+  assume cntbl: "uncountable {xy. f xy \<noteq> 0}"
+  also have "{xy. f xy \<noteq> 0} = (\<Union>n. {xy. 1/Suc n \<le> f xy})"
+    using * by auto
+  finally obtain n where "infinite {xy. 1/Suc n \<le> f xy}"
+    by (meson countableI_type countable_UN uncountable_infinite)
+  then obtain C where C: "C \<subseteq> {xy. 1/Suc n \<le> f xy}" and "countable C" "infinite C"
+    by (metis infinite_countable_subset')
+
+  have "\<infinity> = (\<integral>\<^sup>+ xy. ereal (1 / Suc n) * indicator C xy \<partial>count_space UNIV)"
+    using \<open>infinite C\<close> by(simp add: nn_integral_cmult)
+  also have "\<dots> \<le> ?rhs" using C
+    by(intro nn_integral_mono)(auto split: split_indicator simp add: nonneg)
+  finally have "?rhs = \<infinity>" by simp
+  moreover have "?lhs = \<infinity>"
+  proof(cases "finite (fst ` C)")
+    case True
+    then obtain x C' where x: "x \<in> fst ` C" 
+      and C': "C' = fst -` {x} \<inter> C"
+      and "infinite C'"
+      using \<open>infinite C\<close> by(auto elim!: inf_img_fin_domE')
+    from x C C' have **: "C' \<subseteq> {xy. 1 / Suc n \<le> f xy}" by auto
+
+    from C' \<open>infinite C'\<close> have "infinite (snd ` C')"
+      by(auto dest!: finite_imageD simp add: inj_on_def)
+    then have "\<infinity> = (\<integral>\<^sup>+ y. ereal (1 / Suc n) * indicator (snd ` C') y \<partial>count_space UNIV)"
+      by(simp add: nn_integral_cmult)
+    also have "\<dots> = (\<integral>\<^sup>+ y. ereal (1 / Suc n) * indicator C' (x, y) \<partial>count_space UNIV)"
+      by(rule nn_integral_cong)(force split: split_indicator intro: rev_image_eqI simp add: C')
+    also have "\<dots> = (\<integral>\<^sup>+ x'. (\<integral>\<^sup>+ y. ereal (1 / Suc n) * indicator C' (x, y) \<partial>count_space UNIV) * indicator {x} x' \<partial>count_space UNIV)"
+      by(simp add: one_ereal_def[symmetric] nn_integral_nonneg nn_integral_cmult_indicator)
+    also have "\<dots> \<le> (\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. ereal (1 / Suc n) * indicator C' (x, y) \<partial>count_space UNIV \<partial>count_space UNIV)"
+      by(rule nn_integral_mono)(simp split: split_indicator add: nn_integral_nonneg)
+    also have "\<dots> \<le> ?lhs" using **
+      by(intro nn_integral_mono)(auto split: split_indicator simp add: nonneg)
+    finally show ?thesis by simp
+  next
+    case False
+    def C' \<equiv> "fst ` C"
+    have "\<infinity> = \<integral>\<^sup>+ x. ereal (1 / Suc n) * indicator C' x \<partial>count_space UNIV"
+      using C'_def False by(simp add: nn_integral_cmult)
+    also have "\<dots> = \<integral>\<^sup>+ x. \<integral>\<^sup>+ y. ereal (1 / Suc n) * indicator C' x * indicator {SOME y. (x, y) \<in> C} y \<partial>count_space UNIV \<partial>count_space UNIV"
+      by(auto simp add: one_ereal_def[symmetric] nn_integral_cmult_indicator intro: nn_integral_cong)
+    also have "\<dots> \<le> \<integral>\<^sup>+ x. \<integral>\<^sup>+ y. ereal (1 / Suc n) * indicator C (x, y) \<partial>count_space UNIV \<partial>count_space UNIV"
+      by(intro nn_integral_mono)(auto simp add: C'_def split: split_indicator intro: someI)
+    also have "\<dots> \<le> ?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:
+  "(\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. f (x, y) \<partial>count_space UNIV \<partial>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:
+  "(\<integral>\<^sup>+ y. \<integral>\<^sup>+ x. f (x, y) \<partial>count_space UNIV \<partial>count_space UNIV) = integral\<^sup>N (count_space UNIV) f"
+  (is "?lhs = ?rhs")
+proof -
+  have "?lhs = (\<integral>\<^sup>+ y. \<integral>\<^sup>+ x. (\<lambda>(y, x). f (x, y)) (y, x) \<partial>count_space UNIV \<partial>count_space UNIV)"
+    by(simp)
+  also have "\<dots> = \<integral>\<^sup>+ yx. (\<lambda>(y, x). f (x, y)) yx \<partial>count_space UNIV"
+    by(rule nn_integral_fst_count_space)
+  also have "\<dots> = \<integral>\<^sup>+ xy. f xy \<partial>count_space ((\<lambda>(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 "\<dots> = ?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 \<inter> set_pmf p = {} \<Longrightarrow> A \<in> null_sets (measure_pmf p)"
 using emeasure_eq_0_AE[where ?P="\<lambda>x. x \<in> A" and M="measure_pmf p"]