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: