# HG changeset patch
# User hoelzl
# Date 1384280936 -3600
# Node ID 3b8e33d1a39a45744a362571b50516734b01b6ec
# Parent  dbb8ecfe13377168064d76390d6083022c30993e
measure of a countable union

diff -r dbb8ecfe1337 -r 3b8e33d1a39a src/HOL/Probability/Lebesgue_Integration.thy
--- 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:
diff -r dbb8ecfe1337 -r 3b8e33d1a39a src/HOL/Probability/Probability_Measure.thy
--- 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"
diff -r dbb8ecfe1337 -r 3b8e33d1a39a src/HOL/Probability/Sigma_Algebra.thy
--- 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"