summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Probability/Measurable.thy

changeset 57025 | e7fd64f82876 |

parent 56993 | e5366291d6aa |

child 58965 | a62cdcc5344b |

1.1 --- a/src/HOL/Probability/Measurable.thy Tue May 20 16:52:59 2014 +0200 1.2 +++ b/src/HOL/Probability/Measurable.thy Tue May 20 19:24:39 2014 +0200 1.3 @@ -330,6 +330,31 @@ 1.4 "s \<in> S \<Longrightarrow> A \<in> sets (count_space S) \<Longrightarrow> insert s A \<in> sets (count_space S)" 1.5 by simp 1.6 1.7 +lemma measurable_card[measurable]: 1.8 + fixes S :: "'a \<Rightarrow> nat set" 1.9 + assumes [measurable]: "\<And>i. {x\<in>space M. i \<in> S x} \<in> sets M" 1.10 + shows "(\<lambda>x. card (S x)) \<in> measurable M (count_space UNIV)" 1.11 + unfolding measurable_count_space_eq2_countable 1.12 +proof safe 1.13 + fix n show "(\<lambda>x. card (S x)) -` {n} \<inter> space M \<in> sets M" 1.14 + proof (cases n) 1.15 + case 0 1.16 + then have "(\<lambda>x. card (S x)) -` {n} \<inter> space M = {x\<in>space M. infinite (S x) \<or> (\<forall>i. i \<notin> S x)}" 1.17 + by auto 1.18 + also have "\<dots> \<in> sets M" 1.19 + by measurable 1.20 + finally show ?thesis . 1.21 + next 1.22 + case (Suc i) 1.23 + then have "(\<lambda>x. card (S x)) -` {n} \<inter> space M = 1.24 + (\<Union>F\<in>{A\<in>{A. finite A}. card A = n}. {x\<in>space M. (\<forall>i. i \<in> S x \<longleftrightarrow> i \<in> F)})" 1.25 + unfolding set_eq_iff[symmetric] Collect_bex_eq[symmetric] by (auto intro: card_ge_0_finite) 1.26 + also have "\<dots> \<in> sets M" 1.27 + by (intro sets.countable_UN' countable_Collect countable_Collect_finite) auto 1.28 + finally show ?thesis . 1.29 + qed 1.30 +qed rule 1.31 + 1.32 subsection {* Measurability for (co)inductive predicates *} 1.33 1.34 lemma measurable_lfp: