--- a/src/HOL/Probability/Binary_Product_Measure.thy Fri Jan 23 12:37:23 2015 +0100
+++ b/src/HOL/Probability/Binary_Product_Measure.thy Fri Jan 23 12:37:57 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 Fri Jan 23 12:37:23 2015 +0100
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Fri Jan 23 12:37:57 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)"