integral of the product of count spaces equals the integral of the count space of the product type

--- 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 \<in> sets (count_space UNIV \<Otimes>\<^sub>M M)" (is "A \<in> sets (?A \<Otimes>\<^sub>M ?B)")
+  shows "emeasure (?A \<Otimes>\<^sub>M ?B) A = (\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. indicator A (x, y) \<partial>?B \<partial>?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 \<Otimes>\<^sub>M count_space UNIV) {x} = 1"
+proof -
+  have [simp]: "\<And>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 \<times> 'b) set"
+  assumes A: "A \<in> sets (count_space UNIV \<Otimes>\<^sub>M count_space UNIV)" (is "A \<in> sets (?A \<Otimes>\<^sub>M ?B)")
+  shows "emeasure (?A \<Otimes>\<^sub>M ?B) A = emeasure (count_space UNIV) A"
+proof -
+  { fix A :: "('a \<times> 'b) set" assume "countable A"
+    then have "emeasure (?A \<Otimes>\<^sub>M ?B) (\<Union>a\<in>A. {a}) = (\<integral>\<^sup>+a. emeasure (?A \<Otimes>\<^sub>M ?B) {a} \<partial>count_space A)"
+      by (intro emeasure_UN_countable) (auto simp: sets_Pair disjoint_family_on_def)
+    also have "\<dots> = (\<integral>\<^sup>+a. indicator A a \<partial>count_space UNIV)"
+      by (subst nn_integral_count_space_indicator) auto
+    finally have "emeasure (?A \<Otimes>\<^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 \<subseteq> A"
+      by (auto dest: infinite_countable_subset')
+    with A have "emeasure (?A \<Otimes>\<^sub>M ?B) C \<le> emeasure (?A \<Otimes>\<^sub>M ?B) A"
+      by (intro emeasure_mono) auto
+    also have "emeasure (?A \<Otimes>\<^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]: "\<And>x. 0 \<le> f x"
+  shows "nn_integral (count_space UNIV \<Otimes>\<^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 \<noteq> 0}"
+  have [simp]: "\<And>x. ereal (real (card ({x} \<inter> {x. f x \<noteq> 0}))) = indicator {x. f x \<noteq> 0} x"
+    by (auto split: split_indicator)
+  have [measurable]: "\<And>y. (\<lambda>x. indicator {y} x) \<in> borel_measurable ?P"
+    by (rule measurable_discrete_difference[of "\<lambda>x. 0" _ borel "{y}" "\<lambda>x. indicator {y} x" for y])
+       (auto intro: sets_Pair)
+
+  have "(\<integral>\<^sup>+x. f x \<partial>?P) = (\<integral>\<^sup>+x. \<integral>\<^sup>+x'. f x * indicator {x} x' \<partial>count_space {x. f x \<noteq> 0} \<partial>?P)"
+    by (auto simp add: nn_integral_cmult nn_integral_indicator' intro!: nn_integral_cong split: split_indicator)
+  also have "\<dots> = (\<integral>\<^sup>+x. \<integral>\<^sup>+x'. f x' * indicator {x'} x \<partial>count_space {x. f x \<noteq> 0} \<partial>?P)"
+    by (auto intro!: nn_integral_cong split: split_indicator)
+  also have "\<dots> = (\<integral>\<^sup>+x'. \<integral>\<^sup>+x. f x' * indicator {x'} x \<partial>?P \<partial>count_space {x. f x \<noteq> 0})"
+    by (intro nn_integral_count_space_nn_integral cntbl) auto
+  also have "\<dots> = (\<integral>\<^sup>+x'. f x' \<partial>count_space {x. f x \<noteq> 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 \<noteq> 0"
+    with `0 \<le> f x` have "(\<exists>r. 0 < r \<and> f x = ereal r) \<or> f x = \<infinity>"
+      by (cases "f x") (auto simp: less_le)
+    then have "\<exists>n. ereal (1 / real (Suc n)) \<le> f x"
+      by (auto elim!: nat_approx_posE intro!: less_imp_le) }
+  note * = this
+
+  assume cntbl: "uncountable {x. f x \<noteq> 0}"
+  also have "{x. f x \<noteq> 0} = (\<Union>n. {x. 1/Suc n \<le> f x})"
+    using * by auto
+  finally obtain n where "infinite {x. 1/Suc n \<le> f x}"
+    by (meson countableI_type countable_UN uncountable_infinite)
+  then obtain C where C: "C \<subseteq> {x. 1/Suc n \<le> f x}" and "countable C" "infinite C"
+    by (metis infinite_countable_subset')
+
+  have [measurable]: "C \<in> sets ?P"
+    using sets.countable[OF _ `countable C`, of ?P] by (auto simp: sets_Pair)
+
+  have "(\<integral>\<^sup>+x. ereal (1/Suc n) * indicator C x \<partial>?P) \<le> nn_integral ?P f"
+    using C by (intro nn_integral_mono) (auto split: split_indicator simp: zero_ereal_def[symmetric])
+  moreover have "(\<integral>\<^sup>+x. ereal (1/Suc n) * indicator C x \<partial>?P) = \<infinity>"
+    using `infinite C` by (simp add: nn_integral_cmult emeasure_count_space_prod_eq)
+  moreover have "(\<integral>\<^sup>+x. ereal (1/Suc n) * indicator C x \<partial>count_space UNIV) \<le> nn_integral (count_space UNIV) f"
+    using C by (intro nn_integral_mono) (auto split: split_indicator simp: zero_ereal_def[symmetric])
+  moreover have "(\<integral>\<^sup>+x. ereal (1/Suc n) * indicator C x \<partial>count_space UNIV) = \<infinity>"
+    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 \<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"

--- 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 "\<exists>C\<subseteq>X. countable C \<and> 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 \<le> (indicator B x::ereal) \<longleftrightarrow> (x \<in> A \<longrightarrow> x \<in> B)"
   by (simp add: indicator_def not_le)
@@ -836,6 +844,10 @@
   "(\<And>x. x \<in> space M \<Longrightarrow> u x = v x) \<Longrightarrow> integral\<^sup>N M u = integral\<^sup>N M v"
   by (auto intro: nn_integral_cong_AE)
 
+lemma nn_integral_cong_simp:
+  "(\<And>x. x \<in> space M =simp=> u x = v x) \<Longrightarrow> 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 \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> u x = v x) \<Longrightarrow> 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: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> sets M" and I: "countable I" 
-  assumes disj: "disjoint_family_on X I"
-  shows "emeasure M (UNION I X) = (\<integral>\<^sup>+i. emeasure M (X i) \<partial>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: "\<not> finite I"
-  then have [intro]: "I \<noteq> {}" by auto
-  from from_nat_into_inj_infinite[OF I f] from_nat_into[OF this] disj
-  have disj2: "disjoint_family (\<lambda>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 "(\<Union>i\<in>I. X i) = (\<Union>i. (X \<circ> 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 (\<Union>i. X (from_nat_into I i))"
-    by simp
-  also have "\<dots> = (\<Sum>i. emeasure M (X (from_nat_into I i)))"
-    by (intro suminf_emeasure[symmetric] disj disj2) (auto intro!: sets from_nat_into[OF `I \<noteq> {}`])
-  also have "\<dots> = (\<Sum>n. \<integral>\<^sup>+i. emeasure M (X i) * indicator {from_nat_into I n} i \<partial>count_space I)"
-  proof (intro arg_cong[where f=suminf] ext)
-    fix i
-    have eq: "{a \<in> 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 \<noteq> {}` simp del: ereal_0_less_1)
-    have "(\<integral>\<^sup>+ ia. emeasure M (X ia) * indicator {from_nat_into I i} ia \<partial>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 "\<dots> = 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)) =
-         \<integral>\<^sup>+ ia. emeasure M (X ia) * indicator {from_nat_into I i} ia \<partial>count_space I" ..
-  qed
-  also have "\<dots> = (\<integral>\<^sup>+i. emeasure M (X i) \<partial>count_space I)"
-    apply (subst nn_integral_suminf[symmetric])
-    apply (auto simp: emeasure_nonneg intro!: nn_integral_cong)
-  proof -
-    fix x assume "x \<in> I"
-    then have "(\<Sum>i. emeasure M (X x) * indicator {from_nat_into I i} x) = (\<Sum>i\<in>{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 "\<dots> = emeasure M (X x)"
-      by (simp add: I f `x\<in>I`)
-    finally show "(\<Sum>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 \<Rightarrow> ereal"
   assumes nonneg: "\<And>i. 0 \<le> f i"
@@ -1798,6 +1758,53 @@
   finally show ?thesis .
 qed
 
+lemma nn_integral_count_space_nn_integral:
+  fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> ereal"
+  assumes "countable I" and [measurable]: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable M"
+  shows "(\<integral>\<^sup>+x. \<integral>\<^sup>+i. f i x \<partial>count_space I \<partial>M) = (\<integral>\<^sup>+i. \<integral>\<^sup>+x. f i x \<partial>M \<partial>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 \<noteq> {}"
+    by auto
+  note * = bij_betw_from_nat_into[OF `countable I` `infinite I`]
+  have **: "\<And>f. (\<And>i. 0 \<le> f i) \<Longrightarrow> (\<integral>\<^sup>+i. f i \<partial>count_space I) = (\<Sum>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]: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> sets M" and I[simp]: "countable I" 
+  assumes disj: "disjoint_family_on X I"
+  shows "emeasure M (UNION I X) = (\<integral>\<^sup>+i. emeasure M (X i) \<partial>count_space I)"
+proof -
+  have eq: "\<And>x. indicator (UNION I X) x = \<integral>\<^sup>+ i. indicator (X i) x \<partial>count_space I"
+  proof cases 
+    fix x assume x: "x \<in> UNION I X"
+    then obtain j where j: "x \<in> X j" "j \<in> I"
+      by auto
+    with disj have "\<And>i. i \<in> I \<Longrightarrow> 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) = (\<integral>\<^sup>+x. indicator (UNION I X) x \<partial>M)"
+    by simp
+  also have "\<dots> = (\<integral>\<^sup>+i. \<integral>\<^sup>+x. indicator (X i) x \<partial>M \<partial>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: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M" and X: "countable X"
   shows "emeasure M X = (\<integral>\<^sup>+x. emeasure M {x} \<partial>count_space X)"