--- a/src/HOL/Probability/Lebesgue_Integration.thy Tue Nov 12 19:28:56 2013 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Tue Nov 12 19:28:56 2013 +0100
@@ -2521,6 +2521,61 @@
"f \<in> borel_measurable (count_space A)"
by simp
+lemma lessThan_eq_empty_iff: "{..< n::nat} = {} \<longleftrightarrow> n = 0"
+ by auto
+
+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 positive_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_compose 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 positive_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 positive_integral_suminf[symmetric])
+ apply (auto simp: emeasure_nonneg intro!: positive_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
+
section {* Measures with Restricted Space *}
lemma positive_integral_restrict_space:
--- a/src/HOL/Probability/Probability_Measure.thy Tue Nov 12 19:28:56 2013 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy Tue Nov 12 19:28:56 2013 +0100
@@ -268,6 +268,31 @@
by (intro finite_measure_UNION) auto
qed
+lemma (in prob_space) prob_EX_countable:
+ assumes sets: "\<And>i. i \<in> I \<Longrightarrow> {x\<in>space M. P i x} \<in> sets M" and I: "countable I"
+ assumes disj: "AE x in M. \<forall>i\<in>I. \<forall>j\<in>I. P i x \<longrightarrow> P j x \<longrightarrow> i = j"
+ shows "\<P>(x in M. \<exists>i\<in>I. P i x) = (\<integral>\<^sup>+i. \<P>(x in M. P i x) \<partial>count_space I)"
+proof -
+ let ?N= "\<lambda>x. \<exists>!i\<in>I. P i x"
+ have "ereal (\<P>(x in M. \<exists>i\<in>I. P i x)) = \<P>(x in M. (\<exists>i\<in>I. P i x \<and> ?N x))"
+ unfolding ereal.inject
+ proof (rule prob_eq_AE)
+ show "AE x in M. (\<exists>i\<in>I. P i x) = (\<exists>i\<in>I. P i x \<and> ?N x)"
+ using disj by eventually_elim blast
+ qed (auto intro!: sets.sets_Collect_countable_Ex' sets.sets_Collect_conj sets.sets_Collect_countable_Ex1' I sets)+
+ also have "\<P>(x in M. (\<exists>i\<in>I. P i x \<and> ?N x)) = emeasure M (\<Union>i\<in>I. {x\<in>space M. P i x \<and> ?N x})"
+ unfolding emeasure_eq_measure by (auto intro!: arg_cong[where f=prob])
+ also have "\<dots> = (\<integral>\<^sup>+i. emeasure M {x\<in>space M. P i x \<and> ?N x} \<partial>count_space I)"
+ by (rule emeasure_UN_countable)
+ (auto intro!: sets.sets_Collect_countable_Ex' sets.sets_Collect_conj sets.sets_Collect_countable_Ex1' I sets
+ simp: disjoint_family_on_def)
+ also have "\<dots> = (\<integral>\<^sup>+i. \<P>(x in M. P i x) \<partial>count_space I)"
+ unfolding emeasure_eq_measure using disj
+ by (intro positive_integral_cong ereal.inject[THEN iffD2] prob_eq_AE)
+ (auto intro!: sets.sets_Collect_countable_Ex' sets.sets_Collect_conj sets.sets_Collect_countable_Ex1' I sets)+
+ finally show ?thesis .
+qed
+
lemma (in prob_space) cond_prob_eq_AE:
assumes P: "AE x in M. Q x \<longrightarrow> P x \<longleftrightarrow> P' x" "{x\<in>space M. P x} \<in> events" "{x\<in>space M. P' x} \<in> events"
assumes Q: "AE x in M. Q x \<longleftrightarrow> Q' x" "{x\<in>space M. Q x} \<in> events" "{x\<in>space M. Q' x} \<in> events"
--- a/src/HOL/Probability/Sigma_Algebra.thy Tue Nov 12 19:28:56 2013 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy Tue Nov 12 19:28:56 2013 +0100
@@ -397,7 +397,7 @@
qed
lemma (in sigma_algebra) sets_Collect_countable_Ex':
- assumes "\<And>i. {x\<in>\<Omega>. P i x} \<in> M"
+ assumes "\<And>i. i \<in> I \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M"
assumes "countable I"
shows "{x\<in>\<Omega>. \<exists>i\<in>I. P i x} \<in> M"
proof -
@@ -406,6 +406,27 @@
by (auto intro!: countable_UN')
qed
+lemma (in sigma_algebra) sets_Collect_countable_All':
+ assumes "\<And>i. i \<in> I \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M"
+ assumes "countable I"
+ shows "{x\<in>\<Omega>. \<forall>i\<in>I. P i x} \<in> M"
+proof -
+ have "{x\<in>\<Omega>. \<forall>i\<in>I. P i x} = (\<Inter>i\<in>I. {x\<in>\<Omega>. P i x}) \<inter> \<Omega>" by auto
+ with assms show ?thesis
+ by (cases "I = {}") (auto intro!: countable_INT')
+qed
+
+lemma (in sigma_algebra) sets_Collect_countable_Ex1':
+ assumes "\<And>i. i \<in> I \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M"
+ assumes "countable I"
+ shows "{x\<in>\<Omega>. \<exists>!i\<in>I. P i x} \<in> M"
+proof -
+ have "{x\<in>\<Omega>. \<exists>!i\<in>I. P i x} = {x\<in>\<Omega>. \<exists>i\<in>I. P i x \<and> (\<forall>j\<in>I. P j x \<longrightarrow> i = j)}"
+ by auto
+ with assms show ?thesis
+ by (auto intro!: sets_Collect_countable_All' sets_Collect_countable_Ex' sets_Collect_conj sets_Collect_imp sets_Collect_const)
+qed
+
lemmas (in sigma_algebra) sets_Collect =
sets_Collect_imp sets_Collect_disj sets_Collect_conj sets_Collect_neg sets_Collect_const
sets_Collect_countable_All sets_Collect_countable_Ex sets_Collect_countable_All
@@ -1544,6 +1565,19 @@
shows "(\<lambda>x. f (g x)) \<in> measurable M N"
using measurable_compose[OF g f] .
+lemma measurable_count_space_eq_countable:
+ assumes "countable A"
+ shows "f \<in> measurable M (count_space A) \<longleftrightarrow> (f \<in> space M \<rightarrow> A \<and> (\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M))"
+proof -
+ { fix X assume "X \<subseteq> A" "f \<in> space M \<rightarrow> A"
+ with `countable A` have "f -` X \<inter> space M = (\<Union>a\<in>X. f -` {a} \<inter> space M)" "countable X"
+ by (auto dest: countable_subset)
+ moreover assume "\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M"
+ ultimately have "f -` X \<inter> space M \<in> sets M"
+ using `X \<subseteq> A` by (auto intro!: sets.countable_UN' simp del: UN_simps) }
+ then show ?thesis
+ unfolding measurable_def by auto
+qed
subsection {* Extend measure *}
@@ -1608,7 +1642,7 @@
subsection {* Sigma algebra generated by function preimages *}
definition
- "vimage_algebra M S f = sigma S ((\<lambda>A. f -` A \<inter> S) ` sets M)"
+ "vimage_algebra M S X = sigma S ((\<lambda>A. X -` A \<inter> S) ` sets M)"
lemma sigma_algebra_preimages:
fixes f :: "'x \<Rightarrow> 'a"