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

src/HOL/Probability/Probability_Mass_Function.thy

changeset 69313 | b021008c5397 |

parent 68386 | 98cf1c823c48 |

child 69529 | 4ab9657b3257 |

1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy Sun Nov 18 09:51:41 2018 +0100 1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy Sun Nov 18 18:07:51 2018 +0000 1.3 @@ -1851,15 +1851,15 @@ 1.4 uniformly at random. 1.5 \<close> 1.6 lemma pmf_of_set_UN: 1.7 - assumes "finite (UNION A f)" "A \<noteq> {}" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> {}" 1.8 + assumes "finite (\<Union>(f ` A))" "A \<noteq> {}" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> {}" 1.9 "\<And>x. x \<in> A \<Longrightarrow> card (f x) = n" "disjoint_family_on f A" 1.10 - shows "pmf_of_set (UNION A f) = do {x \<leftarrow> pmf_of_set A; pmf_of_set (f x)}" 1.11 + shows "pmf_of_set (\<Union>(f ` A)) = do {x \<leftarrow> pmf_of_set A; pmf_of_set (f x)}" 1.12 (is "?lhs = ?rhs") 1.13 proof (intro pmf_eqI) 1.14 fix x 1.15 from assms have [simp]: "finite A" 1.16 using infinite_disjoint_family_imp_infinite_UNION[of A f] by blast 1.17 - from assms have "ereal (pmf (pmf_of_set (UNION A f)) x) = 1.18 + from assms have "ereal (pmf (pmf_of_set (\<Union>(f ` A))) x) = 1.19 ereal (indicator (\<Union>x\<in>A. f x) x / real (card (\<Union>x\<in>A. f x)))" 1.20 by (subst pmf_of_set) auto 1.21 also from assms have "card (\<Union>x\<in>A. f x) = card A * n"