src/HOL/Probability/Probability_Mass_Function.thy
changeset 62083 7582b39f51ed
parent 62026 ea3b1b0413b4
child 62324 ae44f16dcea5
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Wed Jan 06 13:04:31 2016 +0100
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Wed Jan 06 12:18:53 2016 +0100
     1.3 @@ -32,48 +32,6 @@
     1.4  lemma ereal_divide': "b \<noteq> 0 \<Longrightarrow> ereal (a / b) = ereal a / ereal b"
     1.5    using ereal_divide[of a b] by simp
     1.6  
     1.7 -lemma (in finite_measure) countable_support:
     1.8 -  "countable {x. measure M {x} \<noteq> 0}"
     1.9 -proof cases
    1.10 -  assume "measure M (space M) = 0"
    1.11 -  with bounded_measure measure_le_0_iff have "{x. measure M {x} \<noteq> 0} = {}"
    1.12 -    by auto
    1.13 -  then show ?thesis
    1.14 -    by simp
    1.15 -next
    1.16 -  let ?M = "measure M (space M)" and ?m = "\<lambda>x. measure M {x}"
    1.17 -  assume "?M \<noteq> 0"
    1.18 -  then have *: "{x. ?m x \<noteq> 0} = (\<Union>n. {x. ?M / Suc n < ?m x})"
    1.19 -    using reals_Archimedean[of "?m x / ?M" for x]
    1.20 -    by (auto simp: field_simps not_le[symmetric] measure_nonneg divide_le_0_iff measure_le_0_iff)
    1.21 -  have **: "\<And>n. finite {x. ?M / Suc n < ?m x}"
    1.22 -  proof (rule ccontr)
    1.23 -    fix n assume "infinite {x. ?M / Suc n < ?m x}" (is "infinite ?X")
    1.24 -    then obtain X where "finite X" "card X = Suc (Suc n)" "X \<subseteq> ?X"
    1.25 -      by (metis infinite_arbitrarily_large)
    1.26 -    from this(3) have *: "\<And>x. x \<in> X \<Longrightarrow> ?M / Suc n \<le> ?m x"
    1.27 -      by auto
    1.28 -    { fix x assume "x \<in> X"
    1.29 -      from \<open>?M \<noteq> 0\<close> *[OF this] have "?m x \<noteq> 0" by (auto simp: field_simps measure_le_0_iff)
    1.30 -      then have "{x} \<in> sets M" by (auto dest: measure_notin_sets) }
    1.31 -    note singleton_sets = this
    1.32 -    have "?M < (\<Sum>x\<in>X. ?M / Suc n)"
    1.33 -      using \<open>?M \<noteq> 0\<close>
    1.34 -      by (simp add: \<open>card X = Suc (Suc n)\<close> of_nat_Suc field_simps less_le measure_nonneg)
    1.35 -    also have "\<dots> \<le> (\<Sum>x\<in>X. ?m x)"
    1.36 -      by (rule setsum_mono) fact
    1.37 -    also have "\<dots> = measure M (\<Union>x\<in>X. {x})"
    1.38 -      using singleton_sets \<open>finite X\<close>
    1.39 -      by (intro finite_measure_finite_Union[symmetric]) (auto simp: disjoint_family_on_def)
    1.40 -    finally have "?M < measure M (\<Union>x\<in>X. {x})" .
    1.41 -    moreover have "measure M (\<Union>x\<in>X. {x}) \<le> ?M"
    1.42 -      using singleton_sets[THEN sets.sets_into_space] by (intro finite_measure_mono) auto
    1.43 -    ultimately show False by simp
    1.44 -  qed
    1.45 -  show ?thesis
    1.46 -    unfolding * by (intro countable_UN countableI_type countable_finite[OF **])
    1.47 -qed
    1.48 -
    1.49  lemma (in finite_measure) AE_support_countable:
    1.50    assumes [simp]: "sets M = UNIV"
    1.51    shows "(AE x in M. measure M {x} \<noteq> 0) \<longleftrightarrow> (\<exists>S. countable S \<and> (AE x in M. x \<in> S))"