diff -r 614ef6d7a6b6 -r 7582b39f51ed src/HOL/Probability/Probability_Mass_Function.thy --- a/src/HOL/Probability/Probability_Mass_Function.thy Wed Jan 06 13:04:31 2016 +0100 +++ b/src/HOL/Probability/Probability_Mass_Function.thy Wed Jan 06 12:18:53 2016 +0100 @@ -32,48 +32,6 @@ lemma ereal_divide': "b \ 0 \ ereal (a / b) = ereal a / ereal b" using ereal_divide[of a b] by simp -lemma (in finite_measure) countable_support: - "countable {x. measure M {x} \ 0}" -proof cases - assume "measure M (space M) = 0" - with bounded_measure measure_le_0_iff have "{x. measure M {x} \ 0} = {}" - by auto - then show ?thesis - by simp -next - let ?M = "measure M (space M)" and ?m = "\x. measure M {x}" - assume "?M \ 0" - then have *: "{x. ?m x \ 0} = (\n. {x. ?M / Suc n < ?m x})" - using reals_Archimedean[of "?m x / ?M" for x] - by (auto simp: field_simps not_le[symmetric] measure_nonneg divide_le_0_iff measure_le_0_iff) - have **: "\n. finite {x. ?M / Suc n < ?m x}" - proof (rule ccontr) - fix n assume "infinite {x. ?M / Suc n < ?m x}" (is "infinite ?X") - then obtain X where "finite X" "card X = Suc (Suc n)" "X \ ?X" - by (metis infinite_arbitrarily_large) - from this(3) have *: "\x. x \ X \ ?M / Suc n \ ?m x" - by auto - { fix x assume "x \ X" - from \?M \ 0\ *[OF this] have "?m x \ 0" by (auto simp: field_simps measure_le_0_iff) - then have "{x} \ sets M" by (auto dest: measure_notin_sets) } - note singleton_sets = this - have "?M < (\x\X. ?M / Suc n)" - using \?M \ 0\ - by (simp add: \card X = Suc (Suc n)\ of_nat_Suc field_simps less_le measure_nonneg) - also have "\ \ (\x\X. ?m x)" - by (rule setsum_mono) fact - also have "\ = measure M (\x\X. {x})" - using singleton_sets \finite X\ - by (intro finite_measure_finite_Union[symmetric]) (auto simp: disjoint_family_on_def) - finally have "?M < measure M (\x\X. {x})" . - moreover have "measure M (\x\X. {x}) \ ?M" - using singleton_sets[THEN sets.sets_into_space] by (intro finite_measure_mono) auto - ultimately show False by simp - qed - show ?thesis - unfolding * by (intro countable_UN countableI_type countable_finite[OF **]) -qed - lemma (in finite_measure) AE_support_countable: assumes [simp]: "sets M = UNIV" shows "(AE x in M. measure M {x} \ 0) \ (\S. countable S \ (AE x in M. x \ S))"