summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | hoelzl |

Tue, 12 Nov 2013 19:28:56 +0100 | |

changeset 54418 | 3b8e33d1a39a |

parent 54417 | dbb8ecfe1337 |

child 54419 | 0c50894fc0d9 |

measure of a countable union

--- 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"