1849 of finite non-empty sets with the same size is the same as first choosing a set |
1849 of finite non-empty sets with the same size is the same as first choosing a set |
1850 from the family uniformly at random and then choosing an element from the chosen set |
1850 from the family uniformly at random and then choosing an element from the chosen set |
1851 uniformly at random. |
1851 uniformly at random. |
1852 \<close> |
1852 \<close> |
1853 lemma pmf_of_set_UN: |
1853 lemma pmf_of_set_UN: |
1854 assumes "finite (UNION A f)" "A \<noteq> {}" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> {}" |
1854 assumes "finite (\<Union>(f ` A))" "A \<noteq> {}" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> {}" |
1855 "\<And>x. x \<in> A \<Longrightarrow> card (f x) = n" "disjoint_family_on f A" |
1855 "\<And>x. x \<in> A \<Longrightarrow> card (f x) = n" "disjoint_family_on f A" |
1856 shows "pmf_of_set (UNION A f) = do {x \<leftarrow> pmf_of_set A; pmf_of_set (f x)}" |
1856 shows "pmf_of_set (\<Union>(f ` A)) = do {x \<leftarrow> pmf_of_set A; pmf_of_set (f x)}" |
1857 (is "?lhs = ?rhs") |
1857 (is "?lhs = ?rhs") |
1858 proof (intro pmf_eqI) |
1858 proof (intro pmf_eqI) |
1859 fix x |
1859 fix x |
1860 from assms have [simp]: "finite A" |
1860 from assms have [simp]: "finite A" |
1861 using infinite_disjoint_family_imp_infinite_UNION[of A f] by blast |
1861 using infinite_disjoint_family_imp_infinite_UNION[of A f] by blast |
1862 from assms have "ereal (pmf (pmf_of_set (UNION A f)) x) = |
1862 from assms have "ereal (pmf (pmf_of_set (\<Union>(f ` A))) x) = |
1863 ereal (indicator (\<Union>x\<in>A. f x) x / real (card (\<Union>x\<in>A. f x)))" |
1863 ereal (indicator (\<Union>x\<in>A. f x) x / real (card (\<Union>x\<in>A. f x)))" |
1864 by (subst pmf_of_set) auto |
1864 by (subst pmf_of_set) auto |
1865 also from assms have "card (\<Union>x\<in>A. f x) = card A * n" |
1865 also from assms have "card (\<Union>x\<in>A. f x) = card A * n" |
1866 by (subst card_UN_disjoint) (auto simp: disjoint_family_on_def) |
1866 by (subst card_UN_disjoint) (auto simp: disjoint_family_on_def) |
1867 also from assms |
1867 also from assms |