57 from `?M \<noteq> 0` *[OF this] have "?m x \<noteq> 0" by (auto simp: field_simps measure_le_0_iff) |
57 from `?M \<noteq> 0` *[OF this] have "?m x \<noteq> 0" by (auto simp: field_simps measure_le_0_iff) |
58 then have "{x} \<in> sets M" by (auto dest: measure_notin_sets) } |
58 then have "{x} \<in> sets M" by (auto dest: measure_notin_sets) } |
59 note singleton_sets = this |
59 note singleton_sets = this |
60 have "?M < (\<Sum>x\<in>X. ?M / Suc n)" |
60 have "?M < (\<Sum>x\<in>X. ?M / Suc n)" |
61 using `?M \<noteq> 0` |
61 using `?M \<noteq> 0` |
62 by (simp add: `card X = Suc (Suc n)` real_eq_of_nat[symmetric] real_of_nat_Suc field_simps less_le measure_nonneg) |
62 by (simp add: `card X = Suc (Suc n)` of_nat_Suc field_simps less_le measure_nonneg) |
63 also have "\<dots> \<le> (\<Sum>x\<in>X. ?m x)" |
63 also have "\<dots> \<le> (\<Sum>x\<in>X. ?m x)" |
64 by (rule setsum_mono) fact |
64 by (rule setsum_mono) fact |
65 also have "\<dots> = measure M (\<Union>x\<in>X. {x})" |
65 also have "\<dots> = measure M (\<Union>x\<in>X. {x})" |
66 using singleton_sets `finite X` |
66 using singleton_sets `finite X` |
67 by (intro finite_measure_finite_Union[symmetric]) (auto simp: disjoint_family_on_def) |
67 by (intro finite_measure_finite_Union[symmetric]) (auto simp: disjoint_family_on_def) |
954 by (safe intro!: rel_pmf_imp_rel_set rel_pmfI) |
954 by (safe intro!: rel_pmf_imp_rel_set rel_pmfI) |
955 (auto intro!: rel_pmfD_measure dest: sympD[OF \<open>symp R\<close>] transpD[OF \<open>transp R\<close>]) |
955 (auto intro!: rel_pmfD_measure dest: sympD[OF \<open>symp R\<close>] transpD[OF \<open>transp R\<close>]) |
956 |
956 |
957 lemma quotient_rel_set_disjoint: |
957 lemma quotient_rel_set_disjoint: |
958 "equivp R \<Longrightarrow> C \<in> UNIV // {(x, y). R x y} \<Longrightarrow> rel_set R A B \<Longrightarrow> A \<inter> C = {} \<longleftrightarrow> B \<inter> C = {}" |
958 "equivp R \<Longrightarrow> C \<in> UNIV // {(x, y). R x y} \<Longrightarrow> rel_set R A B \<Longrightarrow> A \<inter> C = {} \<longleftrightarrow> B \<inter> C = {}" |
959 using in_quotient_imp_closed[of UNIV "{(x, y). R x y}" C] |
959 using in_quotient_imp_closed[of UNIV "{(x, y). R x y}" C] |
960 by (auto 0 0 simp: equivp_equiv rel_set_def set_eq_iff elim: equivpE) |
960 by (auto 0 0 simp: equivp_equiv rel_set_def set_eq_iff elim: equivpE) |
961 (blast dest: equivp_symp)+ |
961 (blast dest: equivp_symp)+ |
962 |
962 |
963 lemma quotientD: "equiv X R \<Longrightarrow> A \<in> X // R \<Longrightarrow> x \<in> A \<Longrightarrow> A = R `` {x}" |
963 lemma quotientD: "equiv X R \<Longrightarrow> A \<in> X // R \<Longrightarrow> x \<in> A \<Longrightarrow> A = R `` {x}" |
964 by (metis Image_singleton_iff equiv_class_eq_iff quotientE) |
964 by (metis Image_singleton_iff equiv_class_eq_iff quotientE) |
971 show "symp R" "transp R" |
971 show "symp R" "transp R" |
972 using assms by (auto simp: equivp_reflp_symp_transp) |
972 using assms by (auto simp: equivp_reflp_symp_transp) |
973 next |
973 next |
974 fix C assume C: "C \<in> UNIV // ?R" and R: "rel_set R (set_pmf p) (set_pmf q)" |
974 fix C assume C: "C \<in> UNIV // ?R" and R: "rel_set R (set_pmf p) (set_pmf q)" |
975 assume eq: "\<forall>x\<in>set_pmf p. \<forall>y\<in>set_pmf q. R x y \<longrightarrow> measure p {x. R x y} = measure q {y. R x y}" |
975 assume eq: "\<forall>x\<in>set_pmf p. \<forall>y\<in>set_pmf q. R x y \<longrightarrow> measure p {x. R x y} = measure q {y. R x y}" |
976 |
976 |
977 show "measure p C = measure q C" |
977 show "measure p C = measure q C" |
978 proof cases |
978 proof cases |
979 assume "p \<inter> C = {}" |
979 assume "p \<inter> C = {}" |
980 moreover then have "q \<inter> C = {}" |
980 moreover then have "q \<inter> C = {}" |
981 using quotient_rel_set_disjoint[OF assms C R] by simp |
981 using quotient_rel_set_disjoint[OF assms C R] by simp |
982 ultimately show ?thesis |
982 ultimately show ?thesis |
983 unfolding measure_pmf_zero_iff[symmetric] by simp |
983 unfolding measure_pmf_zero_iff[symmetric] by simp |
984 next |
984 next |
985 assume "p \<inter> C \<noteq> {}" |
985 assume "p \<inter> C \<noteq> {}" |
986 moreover then have "q \<inter> C \<noteq> {}" |
986 moreover then have "q \<inter> C \<noteq> {}" |
987 using quotient_rel_set_disjoint[OF assms C R] by simp |
987 using quotient_rel_set_disjoint[OF assms C R] by simp |
988 ultimately obtain x y where in_set: "x \<in> set_pmf p" "y \<in> set_pmf q" and in_C: "x \<in> C" "y \<in> C" |
988 ultimately obtain x y where in_set: "x \<in> set_pmf p" "y \<in> set_pmf q" and in_C: "x \<in> C" "y \<in> C" |
989 by auto |
989 by auto |
990 then have "R x y" |
990 then have "R x y" |
991 using in_quotient_imp_in_rel[of UNIV ?R C x y] C assms |
991 using in_quotient_imp_in_rel[of UNIV ?R C x y] C assms |
1066 and qr:"rel_pmf S q r" |
1066 and qr:"rel_pmf S q r" |
1067 from pq obtain pq where pq: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y" |
1067 from pq obtain pq where pq: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y" |
1068 and p: "p = map_pmf fst pq" and q: "q = map_pmf snd pq" by cases auto |
1068 and p: "p = map_pmf fst pq" and q: "q = map_pmf snd pq" by cases auto |
1069 from qr obtain qr where qr: "\<And>y z. (y, z) \<in> set_pmf qr \<Longrightarrow> S y z" |
1069 from qr obtain qr where qr: "\<And>y z. (y, z) \<in> set_pmf qr \<Longrightarrow> S y z" |
1070 and q': "q = map_pmf fst qr" and r: "r = map_pmf snd qr" by cases auto |
1070 and q': "q = map_pmf fst qr" and r: "r = map_pmf snd qr" by cases auto |
1071 |
1071 |
1072 def pr \<equiv> "bind_pmf pq (\<lambda>xy. bind_pmf (cond_pmf qr {yz. fst yz = snd xy}) (\<lambda>yz. return_pmf (fst xy, snd yz)))" |
1072 def pr \<equiv> "bind_pmf pq (\<lambda>xy. bind_pmf (cond_pmf qr {yz. fst yz = snd xy}) (\<lambda>yz. return_pmf (fst xy, snd yz)))" |
1073 have pr_welldefined: "\<And>y. y \<in> q \<Longrightarrow> qr \<inter> {yz. fst yz = y} \<noteq> {}" |
1073 have pr_welldefined: "\<And>y. y \<in> q \<Longrightarrow> qr \<inter> {yz. fst yz = y} \<noteq> {}" |
1074 by (force simp: q') |
1074 by (force simp: q') |
1075 |
1075 |
1076 have "rel_pmf (R OO S) p r" |
1076 have "rel_pmf (R OO S) p r" |
1077 proof (rule rel_pmf.intros) |
1077 proof (rule rel_pmf.intros) |
1078 fix x z assume "(x, z) \<in> pr" |
1078 fix x z assume "(x, z) \<in> pr" |
1079 then have "\<exists>y. (x, y) \<in> pq \<and> (y, z) \<in> qr" |
1079 then have "\<exists>y. (x, y) \<in> pq \<and> (y, z) \<in> qr" |
1080 by (auto simp: q pr_welldefined pr_def split_beta) |
1080 by (auto simp: q pr_welldefined pr_def split_beta) |
1281 and refl: "reflp R" and trans: "transp R" |
1281 and refl: "reflp R" and trans: "transp R" |
1282 shows "rel_pmf (inf R R\<inverse>\<inverse>) p q" |
1282 shows "rel_pmf (inf R R\<inverse>\<inverse>) p q" |
1283 proof (subst rel_pmf_iff_equivp, safe) |
1283 proof (subst rel_pmf_iff_equivp, safe) |
1284 show "equivp (inf R R\<inverse>\<inverse>)" |
1284 show "equivp (inf R R\<inverse>\<inverse>)" |
1285 using trans refl by (auto simp: equivp_reflp_symp_transp intro: sympI transpI reflpI dest: transpD reflpD) |
1285 using trans refl by (auto simp: equivp_reflp_symp_transp intro: sympI transpI reflpI dest: transpD reflpD) |
1286 |
1286 |
1287 fix C assume "C \<in> UNIV // {(x, y). inf R R\<inverse>\<inverse> x y}" |
1287 fix C assume "C \<in> UNIV // {(x, y). inf R R\<inverse>\<inverse> x y}" |
1288 then obtain x where C: "C = {y. R x y \<and> R y x}" |
1288 then obtain x where C: "C = {y. R x y \<and> R y x}" |
1289 by (auto elim: quotientE) |
1289 by (auto elim: quotientE) |
1290 |
1290 |
1291 let ?R = "\<lambda>x y. R x y \<and> R y x" |
1291 let ?R = "\<lambda>x y. R x y \<and> R y x" |
1443 using S_finite S_not_empty by (auto simp: set_pmf_iff) |
1443 using S_finite S_not_empty by (auto simp: set_pmf_iff) |
1444 |
1444 |
1445 lemma emeasure_pmf_of_set[simp]: "emeasure pmf_of_set S = 1" |
1445 lemma emeasure_pmf_of_set[simp]: "emeasure pmf_of_set S = 1" |
1446 by (rule measure_pmf.emeasure_eq_1_AE) (auto simp: AE_measure_pmf_iff) |
1446 by (rule measure_pmf.emeasure_eq_1_AE) (auto simp: AE_measure_pmf_iff) |
1447 |
1447 |
1448 lemma nn_integral_pmf_of_set': |
1448 lemma nn_integral_pmf_of_set': |
1449 "(\<And>x. x \<in> S \<Longrightarrow> f x \<ge> 0) \<Longrightarrow> nn_integral (measure_pmf pmf_of_set) f = setsum f S / card S" |
1449 "(\<And>x. x \<in> S \<Longrightarrow> f x \<ge> 0) \<Longrightarrow> nn_integral (measure_pmf pmf_of_set) f = setsum f S / card S" |
1450 apply(subst nn_integral_measure_pmf_finite, simp_all add: S_finite) |
1450 apply(subst nn_integral_measure_pmf_finite, simp_all add: S_finite) |
1451 apply(simp add: setsum_ereal_left_distrib[symmetric]) |
1451 apply(simp add: setsum_ereal_left_distrib[symmetric]) |
1452 apply(subst ereal_divide', simp add: S_not_empty S_finite) |
1452 apply(subst ereal_divide', simp add: S_not_empty S_finite) |
1453 apply(simp add: ereal_times_divide_eq one_ereal_def[symmetric]) |
1453 apply(simp add: ereal_times_divide_eq one_ereal_def[symmetric]) |
1454 done |
1454 done |
1455 |
1455 |
1456 lemma nn_integral_pmf_of_set: |
1456 lemma nn_integral_pmf_of_set: |
1457 "nn_integral (measure_pmf pmf_of_set) f = setsum (max 0 \<circ> f) S / card S" |
1457 "nn_integral (measure_pmf pmf_of_set) f = setsum (max 0 \<circ> f) S / card S" |
1458 apply(subst nn_integral_max_0[symmetric]) |
1458 apply(subst nn_integral_max_0[symmetric]) |
1459 apply(subst nn_integral_pmf_of_set') |
1459 apply(subst nn_integral_pmf_of_set') |
1460 apply simp_all |
1460 apply simp_all |
1461 done |
1461 done |
1474 end |
1474 end |
1475 |
1475 |
1476 lemma pmf_of_set_singleton: "pmf_of_set {x} = return_pmf x" |
1476 lemma pmf_of_set_singleton: "pmf_of_set {x} = return_pmf x" |
1477 by(rule pmf_eqI)(simp add: indicator_def) |
1477 by(rule pmf_eqI)(simp add: indicator_def) |
1478 |
1478 |
1479 lemma map_pmf_of_set_inj: |
1479 lemma map_pmf_of_set_inj: |
1480 assumes f: "inj_on f A" |
1480 assumes f: "inj_on f A" |
1481 and [simp]: "A \<noteq> {}" "finite A" |
1481 and [simp]: "A \<noteq> {}" "finite A" |
1482 shows "map_pmf f (pmf_of_set A) = pmf_of_set (f ` A)" (is "?lhs = ?rhs") |
1482 shows "map_pmf f (pmf_of_set A) = pmf_of_set (f ` A)" (is "?lhs = ?rhs") |
1483 proof(rule pmf_eqI) |
1483 proof(rule pmf_eqI) |
1484 fix i |
1484 fix i |
1538 proof |
1538 proof |
1539 have "(\<integral>\<^sup>+k. ereal (real (n choose k) * p ^ k * (1 - p) ^ (n - k)) \<partial>count_space UNIV) = |
1539 have "(\<integral>\<^sup>+k. ereal (real (n choose k) * p ^ k * (1 - p) ^ (n - k)) \<partial>count_space UNIV) = |
1540 ereal (\<Sum>k\<le>n. real (n choose k) * p ^ k * (1 - p) ^ (n - k))" |
1540 ereal (\<Sum>k\<le>n. real (n choose k) * p ^ k * (1 - p) ^ (n - k))" |
1541 using p_le_1 p_nonneg by (subst nn_integral_count_space') auto |
1541 using p_le_1 p_nonneg by (subst nn_integral_count_space') auto |
1542 also have "(\<Sum>k\<le>n. real (n choose k) * p ^ k * (1 - p) ^ (n - k)) = (p + (1 - p)) ^ n" |
1542 also have "(\<Sum>k\<le>n. real (n choose k) * p ^ k * (1 - p) ^ (n - k)) = (p + (1 - p)) ^ n" |
1543 by (subst binomial_ring) (simp add: atLeast0AtMost real_of_nat_def) |
1543 by (subst binomial_ring) (simp add: atLeast0AtMost) |
1544 finally show "(\<integral>\<^sup>+ x. ereal (real (n choose x) * p ^ x * (1 - p) ^ (n - x)) \<partial>count_space UNIV) = 1" |
1544 finally show "(\<integral>\<^sup>+ x. ereal (real (n choose x) * p ^ x * (1 - p) ^ (n - x)) \<partial>count_space UNIV) = 1" |
1545 by simp |
1545 by simp |
1546 qed (insert p_nonneg p_le_1, simp) |
1546 qed (insert p_nonneg p_le_1, simp) |
1547 |
1547 |
1548 lemma pmf_binomial[simp]: "pmf binomial_pmf k = (n choose k) * p^k * (1 - p)^(n - k)" |
1548 lemma pmf_binomial[simp]: "pmf binomial_pmf k = (n choose k) * p^k * (1 - p)^(n - k)" |