author  hoelzl 
Fri, 16 Sep 2016 13:56:51 +0200  
changeset 63886  685fb01256af 
parent 63882  018998c00003 
child 63918  6bf55e6e0b75 
permissions  rwrr 
58606  1 
(* Title: HOL/Probability/Probability_Mass_Function.thy 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59665
diff
changeset

2 
Author: Johannes Hölzl, TU München 
59023  3 
Author: Andreas Lochbihler, ETH Zurich 
4 
*) 

58606  5 

59000  6 
section \<open> Probability mass function \<close> 
7 

58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

8 
theory Probability_Mass_Function 
59000  9 
imports 
10 
Giry_Monad 

11 
"~~/src/HOL/Library/Multiset" 

58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

12 
begin 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

13 

59664  14 
lemma AE_emeasure_singleton: 
15 
assumes x: "emeasure M {x} \<noteq> 0" and ae: "AE x in M. P x" shows "P x" 

16 
proof  

17 
from x have x_M: "{x} \<in> sets M" 

18 
by (auto intro: emeasure_notin_sets) 

19 
from ae obtain N where N: "{x\<in>space M. \<not> P x} \<subseteq> N" "emeasure M N = 0" "N \<in> sets M" 

20 
by (auto elim: AE_E) 

21 
{ assume "\<not> P x" 

22 
with x_M[THEN sets.sets_into_space] N have "emeasure M {x} \<le> emeasure M N" 

23 
by (intro emeasure_mono) auto 

24 
with x N have False 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

25 
by (auto simp:) } 
59664  26 
then show "P x" by auto 
27 
qed 

28 

29 
lemma AE_measure_singleton: "measure M {x} \<noteq> 0 \<Longrightarrow> AE x in M. P x \<Longrightarrow> P x" 

30 
by (metis AE_emeasure_singleton measure_def emeasure_empty measure_empty) 

31 

59000  32 
lemma (in finite_measure) AE_support_countable: 
33 
assumes [simp]: "sets M = UNIV" 

34 
shows "(AE x in M. measure M {x} \<noteq> 0) \<longleftrightarrow> (\<exists>S. countable S \<and> (AE x in M. x \<in> S))" 

35 
proof 

36 
assume "\<exists>S. countable S \<and> (AE x in M. x \<in> S)" 

37 
then obtain S where S[intro]: "countable S" and ae: "AE x in M. x \<in> S" 

38 
by auto 

59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59665
diff
changeset

39 
then have "emeasure M (\<Union>x\<in>{x\<in>S. emeasure M {x} \<noteq> 0}. {x}) = 
59000  40 
(\<integral>\<^sup>+ x. emeasure M {x} * indicator {x\<in>S. emeasure M {x} \<noteq> 0} x \<partial>count_space UNIV)" 
41 
by (subst emeasure_UN_countable) 

42 
(auto simp: disjoint_family_on_def nn_integral_restrict_space[symmetric] restrict_count_space) 

43 
also have "\<dots> = (\<integral>\<^sup>+ x. emeasure M {x} * indicator S x \<partial>count_space UNIV)" 

44 
by (auto intro!: nn_integral_cong split: split_indicator) 

45 
also have "\<dots> = emeasure M (\<Union>x\<in>S. {x})" 

46 
by (subst emeasure_UN_countable) 

47 
(auto simp: disjoint_family_on_def nn_integral_restrict_space[symmetric] restrict_count_space) 

48 
also have "\<dots> = emeasure M (space M)" 

49 
using ae by (intro emeasure_eq_AE) auto 

50 
finally have "emeasure M {x \<in> space M. x\<in>S \<and> emeasure M {x} \<noteq> 0} = emeasure M (space M)" 

51 
by (simp add: emeasure_single_in_space cong: rev_conj_cong) 

52 
with finite_measure_compl[of "{x \<in> space M. x\<in>S \<and> emeasure M {x} \<noteq> 0}"] 

53 
have "AE x in M. x \<in> S \<and> emeasure M {x} \<noteq> 0" 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

54 
by (intro AE_I[OF order_refl]) (auto simp: emeasure_eq_measure measure_nonneg set_diff_eq cong: conj_cong) 
59000  55 
then show "AE x in M. measure M {x} \<noteq> 0" 
56 
by (auto simp: emeasure_eq_measure) 

57 
qed (auto intro!: exI[of _ "{x. measure M {x} \<noteq> 0}"] countable_support) 

58 

59664  59 
subsection \<open> PMF as measure \<close> 
59000  60 

58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

61 
typedef 'a pmf = "{M :: 'a measure. prob_space M \<and> sets M = UNIV \<and> (AE x in M. measure M {x} \<noteq> 0)}" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

62 
morphisms measure_pmf Abs_pmf 
58606  63 
by (intro exI[of _ "uniform_measure (count_space UNIV) {undefined}"]) 
64 
(auto intro!: prob_space_uniform_measure AE_uniform_measureI) 

58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

65 

5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

66 
declare [[coercion measure_pmf]] 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

67 

5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

68 
lemma prob_space_measure_pmf: "prob_space (measure_pmf p)" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

69 
using pmf.measure_pmf[of p] by auto 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

70 

61605  71 
interpretation measure_pmf: prob_space "measure_pmf M" for M 
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

72 
by (rule prob_space_measure_pmf) 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

73 

61605  74 
interpretation measure_pmf: subprob_space "measure_pmf M" for M 
59000  75 
by (rule prob_space_imp_subprob_space) unfold_locales 
76 

59048  77 
lemma subprob_space_measure_pmf: "subprob_space (measure_pmf x)" 
78 
by unfold_locales 

79 

58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

80 
locale pmf_as_measure 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

81 
begin 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

82 

5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

83 
setup_lifting type_definition_pmf 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

84 

5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

85 
end 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

86 

5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

87 
context 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

88 
begin 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

89 

5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

90 
interpretation pmf_as_measure . 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

91 

5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

92 
lemma sets_measure_pmf[simp]: "sets (measure_pmf p) = UNIV" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59665
diff
changeset

93 
by transfer blast 
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

94 

59048  95 
lemma sets_measure_pmf_count_space[measurable_cong]: 
96 
"sets (measure_pmf M) = sets (count_space UNIV)" 

59000  97 
by simp 
98 

58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

99 
lemma space_measure_pmf[simp]: "space (measure_pmf p) = UNIV" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

100 
using sets_eq_imp_space_eq[of "measure_pmf p" "count_space UNIV"] by simp 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

101 

61634  102 
lemma measure_pmf_UNIV [simp]: "measure (measure_pmf p) UNIV = 1" 
103 
using measure_pmf.prob_space[of p] by simp 

104 

59048  105 
lemma measure_pmf_in_subprob_algebra[measurable (raw)]: "measure_pmf x \<in> space (subprob_algebra (count_space UNIV))" 
106 
by (simp add: space_subprob_algebra subprob_space_measure_pmf) 

107 

58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

108 
lemma measurable_pmf_measure1[simp]: "measurable (M :: 'a pmf) N = UNIV \<rightarrow> space N" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

109 
by (auto simp: measurable_def) 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

110 

5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

111 
lemma measurable_pmf_measure2[simp]: "measurable N (M :: 'a pmf) = measurable N (count_space UNIV)" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

112 
by (intro measurable_cong_sets) simp_all 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

113 

59664  114 
lemma measurable_pair_restrict_pmf2: 
115 
assumes "countable A" 

116 
assumes [measurable]: "\<And>y. y \<in> A \<Longrightarrow> (\<lambda>x. f (x, y)) \<in> measurable M L" 

117 
shows "f \<in> measurable (M \<Otimes>\<^sub>M restrict_space (measure_pmf N) A) L" (is "f \<in> measurable ?M _") 

118 
proof  

119 
have [measurable_cong]: "sets (restrict_space (count_space UNIV) A) = sets (count_space A)" 

120 
by (simp add: restrict_count_space) 

58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

121 

59664  122 
show ?thesis 
123 
by (intro measurable_compose_countable'[where f="\<lambda>a b. f (fst b, a)" and g=snd and I=A, 

61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61169
diff
changeset

124 
unfolded prod.collapse] assms) 
59664  125 
measurable 
126 
qed 

58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

127 

59664  128 
lemma measurable_pair_restrict_pmf1: 
129 
assumes "countable A" 

130 
assumes [measurable]: "\<And>x. x \<in> A \<Longrightarrow> (\<lambda>y. f (x, y)) \<in> measurable N L" 

131 
shows "f \<in> measurable (restrict_space (measure_pmf M) A \<Otimes>\<^sub>M N) L" 

132 
proof  

133 
have [measurable_cong]: "sets (restrict_space (count_space UNIV) A) = sets (count_space A)" 

134 
by (simp add: restrict_count_space) 

59000  135 

59664  136 
show ?thesis 
137 
by (intro measurable_compose_countable'[where f="\<lambda>a b. f (a, snd b)" and g=fst and I=A, 

61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61169
diff
changeset

138 
unfolded prod.collapse] assms) 
59664  139 
measurable 
140 
qed 

141 

142 
lift_definition pmf :: "'a pmf \<Rightarrow> 'a \<Rightarrow> real" is "\<lambda>M x. measure M {x}" . 

143 

144 
lift_definition set_pmf :: "'a pmf \<Rightarrow> 'a set" is "\<lambda>M. {x. measure M {x} \<noteq> 0}" . 

145 
declare [[coercion set_pmf]] 

58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

146 

5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

147 
lemma AE_measure_pmf: "AE x in (M::'a pmf). x \<in> M" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

148 
by transfer simp 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

149 

5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

150 
lemma emeasure_pmf_single_eq_zero_iff: 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

151 
fixes M :: "'a pmf" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

152 
shows "emeasure M {y} = 0 \<longleftrightarrow> y \<notin> M" 
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

153 
unfolding set_pmf.rep_eq by (simp add: measure_pmf.emeasure_eq_measure) 
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

154 

5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

155 
lemma AE_measure_pmf_iff: "(AE x in measure_pmf M. P x) \<longleftrightarrow> (\<forall>y\<in>M. P y)" 
59664  156 
using AE_measure_singleton[of M] AE_measure_pmf[of M] 
157 
by (auto simp: set_pmf.rep_eq) 

158 

61634  159 
lemma AE_pmfI: "(\<And>y. y \<in> set_pmf M \<Longrightarrow> P y) \<Longrightarrow> almost_everywhere (measure_pmf M) P" 
160 
by(simp add: AE_measure_pmf_iff) 

161 

59664  162 
lemma countable_set_pmf [simp]: "countable (set_pmf p)" 
163 
by transfer (metis prob_space.finite_measure finite_measure.countable_support) 

164 

165 
lemma pmf_positive: "x \<in> set_pmf p \<Longrightarrow> 0 < pmf p x" 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

166 
by transfer (simp add: less_le) 
59664  167 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

168 
lemma pmf_nonneg[simp]: "0 \<le> pmf p x" 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

169 
by transfer simp 
63886
685fb01256af
move HenstockKurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63882
diff
changeset

170 

63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

171 
lemma pmf_not_neg [simp]: "\<not>pmf p x < 0" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

172 
by (simp add: not_less pmf_nonneg) 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

173 

af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

174 
lemma pmf_pos [simp]: "pmf p x \<noteq> 0 \<Longrightarrow> pmf p x > 0" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

175 
using pmf_nonneg[of p x] by linarith 
59664  176 

177 
lemma pmf_le_1: "pmf p x \<le> 1" 

178 
by (simp add: pmf.rep_eq) 

58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

179 

5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

180 
lemma set_pmf_not_empty: "set_pmf M \<noteq> {}" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

181 
using AE_measure_pmf[of M] by (intro notI) simp 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

182 

5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

183 
lemma set_pmf_iff: "x \<in> set_pmf M \<longleftrightarrow> pmf M x \<noteq> 0" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

184 
by transfer simp 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

185 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

186 
lemma pmf_positive_iff: "0 < pmf p x \<longleftrightarrow> x \<in> set_pmf p" 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

187 
unfolding less_le by (simp add: set_pmf_iff) 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

188 

59664  189 
lemma set_pmf_eq: "set_pmf M = {x. pmf M x \<noteq> 0}" 
190 
by (auto simp: set_pmf_iff) 

191 

63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

192 
lemma set_pmf_eq': "set_pmf p = {x. pmf p x > 0}" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

193 
proof safe 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

194 
fix x assume "x \<in> set_pmf p" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

195 
hence "pmf p x \<noteq> 0" by (auto simp: set_pmf_eq) 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

196 
with pmf_nonneg[of p x] show "pmf p x > 0" by simp 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

197 
qed (auto simp: set_pmf_eq) 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

198 

59664  199 
lemma emeasure_pmf_single: 
200 
fixes M :: "'a pmf" 

201 
shows "emeasure M {x} = pmf M x" 

202 
by transfer (simp add: finite_measure.emeasure_eq_measure[OF prob_space.finite_measure]) 

203 

60068  204 
lemma measure_pmf_single: "measure (measure_pmf M) {x} = pmf M x" 
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

205 
using emeasure_pmf_single[of M x] by(simp add: measure_pmf.emeasure_eq_measure pmf_nonneg measure_nonneg) 
60068  206 

59000  207 
lemma emeasure_measure_pmf_finite: "finite S \<Longrightarrow> emeasure (measure_pmf M) S = (\<Sum>s\<in>S. pmf M s)" 
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

208 
by (subst emeasure_eq_setsum_singleton) (auto simp: emeasure_pmf_single pmf_nonneg) 
59000  209 

59023  210 
lemma measure_measure_pmf_finite: "finite S \<Longrightarrow> measure (measure_pmf M) S = setsum (pmf M) S" 
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

211 
using emeasure_measure_pmf_finite[of S M] 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

212 
by (simp add: measure_pmf.emeasure_eq_measure measure_nonneg setsum_nonneg pmf_nonneg) 
59023  213 

63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

214 
lemma setsum_pmf_eq_1: 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

215 
assumes "finite A" "set_pmf p \<subseteq> A" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

216 
shows "(\<Sum>x\<in>A. pmf p x) = 1" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

217 
proof  
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

218 
have "(\<Sum>x\<in>A. pmf p x) = measure_pmf.prob p A" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

219 
by (simp add: measure_measure_pmf_finite assms) 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

220 
also from assms have "\<dots> = 1" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

221 
by (subst measure_pmf.prob_eq_1) (auto simp: AE_measure_pmf_iff) 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

222 
finally show ?thesis . 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

223 
qed 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

224 

59000  225 
lemma nn_integral_measure_pmf_support: 
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

226 
fixes f :: "'a \<Rightarrow> ennreal" 
59000  227 
assumes f: "finite A" and nn: "\<And>x. x \<in> A \<Longrightarrow> 0 \<le> f x" "\<And>x. x \<in> set_pmf M \<Longrightarrow> x \<notin> A \<Longrightarrow> f x = 0" 
228 
shows "(\<integral>\<^sup>+x. f x \<partial>measure_pmf M) = (\<Sum>x\<in>A. f x * pmf M x)" 

229 
proof  

230 
have "(\<integral>\<^sup>+x. f x \<partial>M) = (\<integral>\<^sup>+x. f x * indicator A x \<partial>M)" 

231 
using nn by (intro nn_integral_cong_AE) (auto simp: AE_measure_pmf_iff split: split_indicator) 

232 
also have "\<dots> = (\<Sum>x\<in>A. f x * emeasure M {x})" 

233 
using assms by (intro nn_integral_indicator_finite) auto 

234 
finally show ?thesis 

235 
by (simp add: emeasure_measure_pmf_finite) 

236 
qed 

237 

238 
lemma nn_integral_measure_pmf_finite: 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

239 
fixes f :: "'a \<Rightarrow> ennreal" 
59000  240 
assumes f: "finite (set_pmf M)" and nn: "\<And>x. x \<in> set_pmf M \<Longrightarrow> 0 \<le> f x" 
241 
shows "(\<integral>\<^sup>+x. f x \<partial>measure_pmf M) = (\<Sum>x\<in>set_pmf M. f x * pmf M x)" 

242 
using assms by (intro nn_integral_measure_pmf_support) auto 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

243 

59000  244 
lemma integrable_measure_pmf_finite: 
245 
fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" 

246 
shows "finite (set_pmf M) \<Longrightarrow> integrable M f" 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

247 
by (auto intro!: integrableI_bounded simp: nn_integral_measure_pmf_finite ennreal_mult_less_top) 
59000  248 

249 
lemma integral_measure_pmf: 

250 
assumes [simp]: "finite A" and "\<And>a. a \<in> set_pmf M \<Longrightarrow> f a \<noteq> 0 \<Longrightarrow> a \<in> A" 

251 
shows "(\<integral>x. f x \<partial>measure_pmf M) = (\<Sum>a\<in>A. f a * pmf M a)" 

252 
proof  

253 
have "(\<integral>x. f x \<partial>measure_pmf M) = (\<integral>x. f x * indicator A x \<partial>measure_pmf M)" 

254 
using assms(2) by (intro integral_cong_AE) (auto split: split_indicator simp: AE_measure_pmf_iff) 

255 
also have "\<dots> = (\<Sum>a\<in>A. f a * pmf M a)" 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

256 
by (subst integral_indicator_finite_real) 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

257 
(auto simp: measure_def emeasure_measure_pmf_finite pmf_nonneg) 
59000  258 
finally show ?thesis . 
259 
qed 

260 

261 
lemma integrable_pmf: "integrable (count_space X) (pmf M)" 

262 
proof  

263 
have " (\<integral>\<^sup>+ x. pmf M x \<partial>count_space X) = (\<integral>\<^sup>+ x. pmf M x \<partial>count_space (M \<inter> X))" 

264 
by (auto simp add: nn_integral_count_space_indicator set_pmf_iff intro!: nn_integral_cong split: split_indicator) 

265 
then have "integrable (count_space X) (pmf M) = integrable (count_space (M \<inter> X)) (pmf M)" 

266 
by (simp add: integrable_iff_bounded pmf_nonneg) 

267 
then show ?thesis 

59023  268 
by (simp add: pmf.rep_eq measure_pmf.integrable_measure disjoint_family_on_def) 
59000  269 
qed 
270 

271 
lemma integral_pmf: "(\<integral>x. pmf M x \<partial>count_space X) = measure M X" 

272 
proof  

273 
have "(\<integral>x. pmf M x \<partial>count_space X) = (\<integral>\<^sup>+x. pmf M x \<partial>count_space X)" 

274 
by (simp add: pmf_nonneg integrable_pmf nn_integral_eq_integral) 

275 
also have "\<dots> = (\<integral>\<^sup>+x. emeasure M {x} \<partial>count_space (X \<inter> M))" 

276 
by (auto intro!: nn_integral_cong_AE split: split_indicator 

277 
simp: pmf.rep_eq measure_pmf.emeasure_eq_measure nn_integral_count_space_indicator 

278 
AE_count_space set_pmf_iff) 

279 
also have "\<dots> = emeasure M (X \<inter> M)" 

280 
by (rule emeasure_countable_singleton[symmetric]) (auto intro: countable_set_pmf) 

281 
also have "\<dots> = emeasure M X" 

282 
by (auto intro!: emeasure_eq_AE simp: AE_measure_pmf_iff) 

283 
finally show ?thesis 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

284 
by (simp add: measure_pmf.emeasure_eq_measure measure_nonneg integral_nonneg pmf_nonneg) 
59000  285 
qed 
286 

287 
lemma integral_pmf_restrict: 

288 
"(f::'a \<Rightarrow> 'b::{banach, second_countable_topology}) \<in> borel_measurable (count_space UNIV) \<Longrightarrow> 

289 
(\<integral>x. f x \<partial>measure_pmf M) = (\<integral>x. f x \<partial>restrict_space M M)" 

290 
by (auto intro!: integral_cong_AE simp add: integral_restrict_space AE_measure_pmf_iff) 

291 

58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

292 
lemma emeasure_pmf: "emeasure (M::'a pmf) M = 1" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

293 
proof  
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

294 
have "emeasure (M::'a pmf) M = emeasure (M::'a pmf) (space M)" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

295 
by (intro emeasure_eq_AE) (simp_all add: AE_measure_pmf) 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

296 
then show ?thesis 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

297 
using measure_pmf.emeasure_space_1 by simp 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

298 
qed 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

299 

59490  300 
lemma emeasure_pmf_UNIV [simp]: "emeasure (measure_pmf M) UNIV = 1" 
301 
using measure_pmf.emeasure_space_1[of M] by simp 

302 

59023  303 
lemma in_null_sets_measure_pmfI: 
304 
"A \<inter> set_pmf p = {} \<Longrightarrow> A \<in> null_sets (measure_pmf p)" 

305 
using emeasure_eq_0_AE[where ?P="\<lambda>x. x \<in> A" and M="measure_pmf p"] 

306 
by(auto simp add: null_sets_def AE_measure_pmf_iff) 

307 

59664  308 
lemma measure_subprob: "measure_pmf M \<in> space (subprob_algebra (count_space UNIV))" 
309 
by (simp add: space_subprob_algebra subprob_space_measure_pmf) 

310 

311 
subsection \<open> Monad Interpretation \<close> 

312 

313 
lemma measurable_measure_pmf[measurable]: 

314 
"(\<lambda>x. measure_pmf (M x)) \<in> measurable (count_space UNIV) (subprob_algebra (count_space UNIV))" 

315 
by (auto simp: space_subprob_algebra intro!: prob_space_imp_subprob_space) unfold_locales 

316 

317 
lemma bind_measure_pmf_cong: 

318 
assumes "\<And>x. A x \<in> space (subprob_algebra N)" "\<And>x. B x \<in> space (subprob_algebra N)" 

319 
assumes "\<And>i. i \<in> set_pmf x \<Longrightarrow> A i = B i" 

320 
shows "bind (measure_pmf x) A = bind (measure_pmf x) B" 

321 
proof (rule measure_eqI) 

62026  322 
show "sets (measure_pmf x \<bind> A) = sets (measure_pmf x \<bind> B)" 
59664  323 
using assms by (subst (1 2) sets_bind) (auto simp: space_subprob_algebra) 
324 
next 

62026  325 
fix X assume "X \<in> sets (measure_pmf x \<bind> A)" 
59664  326 
then have X: "X \<in> sets N" 
327 
using assms by (subst (asm) sets_bind) (auto simp: space_subprob_algebra) 

62026  328 
show "emeasure (measure_pmf x \<bind> A) X = emeasure (measure_pmf x \<bind> B) X" 
59664  329 
using assms 
330 
by (subst (1 2) emeasure_bind[where N=N, OF _ _ X]) 

331 
(auto intro!: nn_integral_cong_AE simp: AE_measure_pmf_iff) 

332 
qed 

333 

334 
lift_definition bind_pmf :: "'a pmf \<Rightarrow> ('a \<Rightarrow> 'b pmf ) \<Rightarrow> 'b pmf" is bind 

335 
proof (clarify, intro conjI) 

336 
fix f :: "'a measure" and g :: "'a \<Rightarrow> 'b measure" 

337 
assume "prob_space f" 

338 
then interpret f: prob_space f . 

339 
assume "sets f = UNIV" and ae_f: "AE x in f. measure f {x} \<noteq> 0" 

340 
then have s_f[simp]: "sets f = sets (count_space UNIV)" 

341 
by simp 

342 
assume g: "\<And>x. prob_space (g x) \<and> sets (g x) = UNIV \<and> (AE y in g x. measure (g x) {y} \<noteq> 0)" 

343 
then have g: "\<And>x. prob_space (g x)" and s_g[simp]: "\<And>x. sets (g x) = sets (count_space UNIV)" 

344 
and ae_g: "\<And>x. AE y in g x. measure (g x) {y} \<noteq> 0" 

345 
by auto 

346 

347 
have [measurable]: "g \<in> measurable f (subprob_algebra (count_space UNIV))" 

348 
by (auto simp: measurable_def space_subprob_algebra prob_space_imp_subprob_space g) 

59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59665
diff
changeset

349 

62026  350 
show "prob_space (f \<bind> g)" 
59664  351 
using g by (intro f.prob_space_bind[where S="count_space UNIV"]) auto 
62026  352 
then interpret fg: prob_space "f \<bind> g" . 
353 
show [simp]: "sets (f \<bind> g) = UNIV" 

59664  354 
using sets_eq_imp_space_eq[OF s_f] 
355 
by (subst sets_bind[where N="count_space UNIV"]) auto 

62026  356 
show "AE x in f \<bind> g. measure (f \<bind> g) {x} \<noteq> 0" 
59664  357 
apply (simp add: fg.prob_eq_0 AE_bind[where B="count_space UNIV"]) 
358 
using ae_f 

359 
apply eventually_elim 

360 
using ae_g 

361 
apply eventually_elim 

362 
apply (auto dest: AE_measure_singleton) 

363 
done 

364 
qed 

365 

63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

366 
adhoc_overloading Monad_Syntax.bind bind_pmf 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

367 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

368 
lemma ennreal_pmf_bind: "pmf (bind_pmf N f) i = (\<integral>\<^sup>+x. pmf (f x) i \<partial>measure_pmf N)" 
59664  369 
unfolding pmf.rep_eq bind_pmf.rep_eq 
370 
by (auto simp: measure_pmf.measure_bind[where N="count_space UNIV"] measure_subprob measure_nonneg 

371 
intro!: nn_integral_eq_integral[symmetric] measure_pmf.integrable_const_bound[where B=1]) 

372 

373 
lemma pmf_bind: "pmf (bind_pmf N f) i = (\<integral>x. pmf (f x) i \<partial>measure_pmf N)" 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

374 
using ennreal_pmf_bind[of N f i] 
59664  375 
by (subst (asm) nn_integral_eq_integral) 
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

376 
(auto simp: pmf_nonneg pmf_le_1 pmf_nonneg integral_nonneg 
59664  377 
intro!: nn_integral_eq_integral[symmetric] measure_pmf.integrable_const_bound[where B=1]) 
378 

379 
lemma bind_pmf_const[simp]: "bind_pmf M (\<lambda>x. c) = c" 

380 
by transfer (simp add: bind_const' prob_space_imp_subprob_space) 

381 

59665  382 
lemma set_bind_pmf[simp]: "set_pmf (bind_pmf M N) = (\<Union>M\<in>set_pmf M. set_pmf (N M))" 
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

383 
proof  
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

384 
have "set_pmf (bind_pmf M N) = {x. ennreal (pmf (bind_pmf M N) x) \<noteq> 0}" 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

385 
by (simp add: set_pmf_eq pmf_nonneg) 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

386 
also have "\<dots> = (\<Union>M\<in>set_pmf M. set_pmf (N M))" 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

387 
unfolding ennreal_pmf_bind 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

388 
by (subst nn_integral_0_iff_AE) (auto simp: AE_measure_pmf_iff pmf_nonneg set_pmf_eq) 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

389 
finally show ?thesis . 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

390 
qed 
59664  391 

63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

392 
lemma bind_pmf_cong [fundef_cong]: 
59664  393 
assumes "p = q" 
394 
shows "(\<And>x. x \<in> set_pmf q \<Longrightarrow> f x = g x) \<Longrightarrow> bind_pmf p f = bind_pmf q g" 

61808  395 
unfolding \<open>p = q\<close>[symmetric] measure_pmf_inject[symmetric] bind_pmf.rep_eq 
59664  396 
by (auto simp: AE_measure_pmf_iff Pi_iff space_subprob_algebra subprob_space_measure_pmf 
397 
sets_bind[where N="count_space UNIV"] emeasure_bind[where N="count_space UNIV"] 

398 
intro!: nn_integral_cong_AE measure_eqI) 

399 

400 
lemma bind_pmf_cong_simp: 

401 
"p = q \<Longrightarrow> (\<And>x. x \<in> set_pmf q =simp=> f x = g x) \<Longrightarrow> bind_pmf p f = bind_pmf q g" 

402 
by (simp add: simp_implies_def cong: bind_pmf_cong) 

403 

62026  404 
lemma measure_pmf_bind: "measure_pmf (bind_pmf M f) = (measure_pmf M \<bind> (\<lambda>x. measure_pmf (f x)))" 
59664  405 
by transfer simp 
406 

407 
lemma nn_integral_bind_pmf[simp]: "(\<integral>\<^sup>+x. f x \<partial>bind_pmf M N) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f y \<partial>N x \<partial>M)" 

408 
using measurable_measure_pmf[of N] 

409 
unfolding measure_pmf_bind 

410 
apply (intro nn_integral_bind[where B="count_space UNIV"]) 

411 
apply auto 

412 
done 

413 

414 
lemma emeasure_bind_pmf[simp]: "emeasure (bind_pmf M N) X = (\<integral>\<^sup>+x. emeasure (N x) X \<partial>M)" 

415 
using measurable_measure_pmf[of N] 

416 
unfolding measure_pmf_bind 

417 
by (subst emeasure_bind[where N="count_space UNIV"]) auto 

59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59665
diff
changeset

418 

59664  419 
lift_definition return_pmf :: "'a \<Rightarrow> 'a pmf" is "return (count_space UNIV)" 
420 
by (auto intro!: prob_space_return simp: AE_return measure_return) 

421 

422 
lemma bind_return_pmf: "bind_pmf (return_pmf x) f = f x" 

423 
by transfer 

424 
(auto intro!: prob_space_imp_subprob_space bind_return[where N="count_space UNIV"] 

425 
simp: space_subprob_algebra) 

426 

59665  427 
lemma set_return_pmf[simp]: "set_pmf (return_pmf x) = {x}" 
59664  428 
by transfer (auto simp add: measure_return split: split_indicator) 
429 

430 
lemma bind_return_pmf': "bind_pmf N return_pmf = N" 

431 
proof (transfer, clarify) 

62026  432 
fix N :: "'a measure" assume "sets N = UNIV" then show "N \<bind> return (count_space UNIV) = N" 
59664  433 
by (subst return_sets_cong[where N=N]) (simp_all add: bind_return') 
434 
qed 

435 

436 
lemma bind_assoc_pmf: "bind_pmf (bind_pmf A B) C = bind_pmf A (\<lambda>x. bind_pmf (B x) C)" 

437 
by transfer 

438 
(auto intro!: bind_assoc[where N="count_space UNIV" and R="count_space UNIV"] 

439 
simp: measurable_def space_subprob_algebra prob_space_imp_subprob_space) 

440 

441 
definition "map_pmf f M = bind_pmf M (\<lambda>x. return_pmf (f x))" 

442 

443 
lemma map_bind_pmf: "map_pmf f (bind_pmf M g) = bind_pmf M (\<lambda>x. map_pmf f (g x))" 

444 
by (simp add: map_pmf_def bind_assoc_pmf) 

445 

446 
lemma bind_map_pmf: "bind_pmf (map_pmf f M) g = bind_pmf M (\<lambda>x. g (f x))" 

447 
by (simp add: map_pmf_def bind_assoc_pmf bind_return_pmf) 

448 

449 
lemma map_pmf_transfer[transfer_rule]: 

450 
"rel_fun op = (rel_fun cr_pmf cr_pmf) (\<lambda>f M. distr M (count_space UNIV) f) map_pmf" 

451 
proof  

452 
have "rel_fun op = (rel_fun pmf_as_measure.cr_pmf pmf_as_measure.cr_pmf) 

62026  453 
(\<lambda>f M. M \<bind> (return (count_space UNIV) o f)) map_pmf" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59665
diff
changeset

454 
unfolding map_pmf_def[abs_def] comp_def by transfer_prover 
59664  455 
then show ?thesis 
456 
by (force simp: rel_fun_def cr_pmf_def bind_return_distr) 

457 
qed 

458 

459 
lemma map_pmf_rep_eq: 

460 
"measure_pmf (map_pmf f M) = distr (measure_pmf M) (count_space UNIV) f" 

461 
unfolding map_pmf_def bind_pmf.rep_eq comp_def return_pmf.rep_eq 

462 
using bind_return_distr[of M f "count_space UNIV"] by (simp add: comp_def) 

463 

58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

464 
lemma map_pmf_id[simp]: "map_pmf id = id" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

465 
by (rule, transfer) (auto simp: emeasure_distr measurable_def intro!: measure_eqI) 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

466 

59053  467 
lemma map_pmf_ident[simp]: "map_pmf (\<lambda>x. x) = (\<lambda>x. x)" 
468 
using map_pmf_id unfolding id_def . 

469 

58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

470 
lemma map_pmf_compose: "map_pmf (f \<circ> g) = map_pmf f \<circ> map_pmf g" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59665
diff
changeset

471 
by (rule, transfer) (simp add: distr_distr[symmetric, where N="count_space UNIV"] measurable_def) 
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

472 

59000  473 
lemma map_pmf_comp: "map_pmf f (map_pmf g M) = map_pmf (\<lambda>x. f (g x)) M" 
474 
using map_pmf_compose[of f g] by (simp add: comp_def) 

475 

59664  476 
lemma map_pmf_cong: "p = q \<Longrightarrow> (\<And>x. x \<in> set_pmf q \<Longrightarrow> f x = g x) \<Longrightarrow> map_pmf f p = map_pmf g q" 
477 
unfolding map_pmf_def by (rule bind_pmf_cong) auto 

478 

479 
lemma pmf_set_map: "set_pmf \<circ> map_pmf f = op ` f \<circ> set_pmf" 

59665  480 
by (auto simp add: comp_def fun_eq_iff map_pmf_def) 
59664  481 

59665  482 
lemma set_map_pmf[simp]: "set_pmf (map_pmf f M) = f`set_pmf M" 
59664  483 
using pmf_set_map[of f] by (auto simp: comp_def fun_eq_iff) 
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

484 

59002
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset

485 
lemma emeasure_map_pmf[simp]: "emeasure (map_pmf f M) X = emeasure M (f ` X)" 
59664  486 
unfolding map_pmf_rep_eq by (subst emeasure_distr) auto 
59002
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset

487 

61634  488 
lemma measure_map_pmf[simp]: "measure (map_pmf f M) X = measure M (f ` X)" 
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

489 
using emeasure_map_pmf[of f M X] by(simp add: measure_pmf.emeasure_eq_measure measure_nonneg) 
61634  490 

59002
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset

491 
lemma nn_integral_map_pmf[simp]: "(\<integral>\<^sup>+x. f x \<partial>map_pmf g M) = (\<integral>\<^sup>+x. f (g x) \<partial>M)" 
59664  492 
unfolding map_pmf_rep_eq by (intro nn_integral_distr) auto 
59002
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset

493 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

494 
lemma ennreal_pmf_map: "pmf (map_pmf f p) x = (\<integral>\<^sup>+ y. indicator (f ` {x}) y \<partial>measure_pmf p)" 
59664  495 
proof (transfer fixing: f x) 
59023  496 
fix p :: "'b measure" 
497 
presume "prob_space p" 

498 
then interpret prob_space p . 

499 
presume "sets p = UNIV" 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

500 
then show "ennreal (measure (distr p (count_space UNIV) f) {x}) = integral\<^sup>N p (indicator (f ` {x}))" 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

501 
by(simp add: measure_distr measurable_def emeasure_eq_measure) 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

502 
qed simp_all 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

503 

1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

504 
lemma pmf_map: "pmf (map_pmf f p) x = measure p (f ` {x})" 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

505 
proof (transfer fixing: f x) 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

506 
fix p :: "'b measure" 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

507 
presume "prob_space p" 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

508 
then interpret prob_space p . 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

509 
presume "sets p = UNIV" 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

510 
then show "measure (distr p (count_space UNIV) f) {x} = measure p (f ` {x})" 
59023  511 
by(simp add: measure_distr measurable_def emeasure_eq_measure) 
512 
qed simp_all 

513 

514 
lemma nn_integral_pmf: "(\<integral>\<^sup>+ x. pmf p x \<partial>count_space A) = emeasure (measure_pmf p) A" 

515 
proof  

516 
have "(\<integral>\<^sup>+ x. pmf p x \<partial>count_space A) = (\<integral>\<^sup>+ x. pmf p x \<partial>count_space (A \<inter> set_pmf p))" 

517 
by(auto simp add: nn_integral_count_space_indicator indicator_def set_pmf_iff intro: nn_integral_cong) 

518 
also have "\<dots> = emeasure (measure_pmf p) (\<Union>x\<in>A \<inter> set_pmf p. {x})" 

519 
by(subst emeasure_UN_countable)(auto simp add: emeasure_pmf_single disjoint_family_on_def) 

520 
also have "\<dots> = emeasure (measure_pmf p) ((\<Union>x\<in>A \<inter> set_pmf p. {x}) \<union> {x. x \<in> A \<and> x \<notin> set_pmf p})" 

521 
by(rule emeasure_Un_null_set[symmetric])(auto intro: in_null_sets_measure_pmfI) 

522 
also have "\<dots> = emeasure (measure_pmf p) A" 

523 
by(auto intro: arg_cong2[where f=emeasure]) 

524 
finally show ?thesis . 

525 
qed 

526 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

527 
lemma integral_map_pmf[simp]: 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

528 
fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

529 
shows "integral\<^sup>L (map_pmf g p) f = integral\<^sup>L p (\<lambda>x. f (g x))" 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

530 
by (simp add: integral_distr map_pmf_rep_eq) 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

531 

60068  532 
lemma map_return_pmf [simp]: "map_pmf f (return_pmf x) = return_pmf (f x)" 
59664  533 
by transfer (simp add: distr_return) 
534 

535 
lemma map_pmf_const[simp]: "map_pmf (\<lambda>_. c) M = return_pmf c" 

536 
by transfer (auto simp: prob_space.distr_const) 

537 

60068  538 
lemma pmf_return [simp]: "pmf (return_pmf x) y = indicator {y} x" 
59664  539 
by transfer (simp add: measure_return) 
540 

541 
lemma nn_integral_return_pmf[simp]: "0 \<le> f x \<Longrightarrow> (\<integral>\<^sup>+x. f x \<partial>return_pmf x) = f x" 

542 
unfolding return_pmf.rep_eq by (intro nn_integral_return) auto 

543 

544 
lemma emeasure_return_pmf[simp]: "emeasure (return_pmf x) X = indicator X x" 

545 
unfolding return_pmf.rep_eq by (intro emeasure_return) auto 

546 

63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

547 
lemma measure_return_pmf [simp]: "measure_pmf.prob (return_pmf x) A = indicator A x" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

548 
proof  
63886
685fb01256af
move HenstockKurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63882
diff
changeset

549 
have "ennreal (measure_pmf.prob (return_pmf x) A) = 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

550 
emeasure (measure_pmf (return_pmf x)) A" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

551 
by (simp add: measure_pmf.emeasure_eq_measure) 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

552 
also have "\<dots> = ennreal (indicator A x)" by (simp add: ennreal_indicator) 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

553 
finally show ?thesis by simp 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

554 
qed 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

555 

59664  556 
lemma return_pmf_inj[simp]: "return_pmf x = return_pmf y \<longleftrightarrow> x = y" 
557 
by (metis insertI1 set_return_pmf singletonD) 

558 

59665  559 
lemma map_pmf_eq_return_pmf_iff: 
560 
"map_pmf f p = return_pmf x \<longleftrightarrow> (\<forall>y \<in> set_pmf p. f y = x)" 

561 
proof 

562 
assume "map_pmf f p = return_pmf x" 

563 
then have "set_pmf (map_pmf f p) = set_pmf (return_pmf x)" by simp 

564 
then show "\<forall>y \<in> set_pmf p. f y = x" by auto 

565 
next 

566 
assume "\<forall>y \<in> set_pmf p. f y = x" 

567 
then show "map_pmf f p = return_pmf x" 

568 
unfolding map_pmf_const[symmetric, of _ p] by (intro map_pmf_cong) auto 

569 
qed 

570 

59664  571 
definition "pair_pmf A B = bind_pmf A (\<lambda>x. bind_pmf B (\<lambda>y. return_pmf (x, y)))" 
572 

573 
lemma pmf_pair: "pmf (pair_pmf M N) (a, b) = pmf M a * pmf N b" 

574 
unfolding pair_pmf_def pmf_bind pmf_return 

575 
apply (subst integral_measure_pmf[where A="{b}"]) 

576 
apply (auto simp: indicator_eq_0_iff) 

577 
apply (subst integral_measure_pmf[where A="{a}"]) 

578 
apply (auto simp: indicator_eq_0_iff setsum_nonneg_eq_0_iff pmf_nonneg) 

579 
done 

580 

59665  581 
lemma set_pair_pmf[simp]: "set_pmf (pair_pmf A B) = set_pmf A \<times> set_pmf B" 
59664  582 
unfolding pair_pmf_def set_bind_pmf set_return_pmf by auto 
583 

584 
lemma measure_pmf_in_subprob_space[measurable (raw)]: 

585 
"measure_pmf M \<in> space (subprob_algebra (count_space UNIV))" 

586 
by (simp add: space_subprob_algebra) intro_locales 

587 

588 
lemma nn_integral_pair_pmf': "(\<integral>\<^sup>+x. f x \<partial>pair_pmf A B) = (\<integral>\<^sup>+a. \<integral>\<^sup>+b. f (a, b) \<partial>B \<partial>A)" 

589 
proof  

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

590 
have "(\<integral>\<^sup>+x. f x \<partial>pair_pmf A B) = (\<integral>\<^sup>+x. f x * indicator (A \<times> B) x \<partial>pair_pmf A B)" 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

591 
by (auto simp: AE_measure_pmf_iff intro!: nn_integral_cong_AE) 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

592 
also have "\<dots> = (\<integral>\<^sup>+a. \<integral>\<^sup>+b. f (a, b) * indicator (A \<times> B) (a, b) \<partial>B \<partial>A)" 
59664  593 
by (simp add: pair_pmf_def) 
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

594 
also have "\<dots> = (\<integral>\<^sup>+a. \<integral>\<^sup>+b. f (a, b) \<partial>B \<partial>A)" 
59664  595 
by (auto intro!: nn_integral_cong_AE simp: AE_measure_pmf_iff) 
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

596 
finally show ?thesis . 
59664  597 
qed 
598 

599 
lemma bind_pair_pmf: 

600 
assumes M[measurable]: "M \<in> measurable (count_space UNIV \<Otimes>\<^sub>M count_space UNIV) (subprob_algebra N)" 

62026  601 
shows "measure_pmf (pair_pmf A B) \<bind> M = (measure_pmf A \<bind> (\<lambda>x. measure_pmf B \<bind> (\<lambda>y. M (x, y))))" 
59664  602 
(is "?L = ?R") 
603 
proof (rule measure_eqI) 

604 
have M'[measurable]: "M \<in> measurable (pair_pmf A B) (subprob_algebra N)" 

605 
using M[THEN measurable_space] by (simp_all add: space_pair_measure) 

606 

607 
note measurable_bind[where N="count_space UNIV", measurable] 

608 
note measure_pmf_in_subprob_space[simp] 

609 

610 
have sets_eq_N: "sets ?L = N" 

611 
by (subst sets_bind[OF sets_kernel[OF M']]) auto 

612 
show "sets ?L = sets ?R" 

613 
using measurable_space[OF M] 

614 
by (simp add: sets_eq_N space_pair_measure space_subprob_algebra) 

615 
fix X assume "X \<in> sets ?L" 

616 
then have X[measurable]: "X \<in> sets N" 

617 
unfolding sets_eq_N . 

618 
then show "emeasure ?L X = emeasure ?R X" 

619 
apply (simp add: emeasure_bind[OF _ M' X]) 

620 
apply (simp add: nn_integral_bind[where B="count_space UNIV"] pair_pmf_def measure_pmf_bind[of A] 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

621 
nn_integral_measure_pmf_finite) 
59664  622 
apply (subst emeasure_bind[OF _ _ X]) 
623 
apply measurable 

624 
apply (subst emeasure_bind[OF _ _ X]) 

625 
apply measurable 

626 
done 

627 
qed 

628 

629 
lemma map_fst_pair_pmf: "map_pmf fst (pair_pmf A B) = A" 

630 
by (simp add: pair_pmf_def map_pmf_def bind_assoc_pmf bind_return_pmf bind_return_pmf') 

631 

632 
lemma map_snd_pair_pmf: "map_pmf snd (pair_pmf A B) = B" 

633 
by (simp add: pair_pmf_def map_pmf_def bind_assoc_pmf bind_return_pmf bind_return_pmf') 

634 

635 
lemma nn_integral_pmf': 

636 
"inj_on f A \<Longrightarrow> (\<integral>\<^sup>+x. pmf p (f x) \<partial>count_space A) = emeasure p (f ` A)" 

637 
by (subst nn_integral_bij_count_space[where g=f and B="f`A"]) 

638 
(auto simp: bij_betw_def nn_integral_pmf) 

639 

640 
lemma pmf_le_0_iff[simp]: "pmf M p \<le> 0 \<longleftrightarrow> pmf M p = 0" 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

641 
using pmf_nonneg[of M p] by arith 
59664  642 

643 
lemma min_pmf_0[simp]: "min (pmf M p) 0 = 0" "min 0 (pmf M p) = 0" 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

644 
using pmf_nonneg[of M p] by arith+ 
59664  645 

646 
lemma pmf_eq_0_set_pmf: "pmf M p = 0 \<longleftrightarrow> p \<notin> set_pmf M" 

647 
unfolding set_pmf_iff by simp 

648 

649 
lemma pmf_map_inj: "inj_on f (set_pmf M) \<Longrightarrow> x \<in> set_pmf M \<Longrightarrow> pmf (map_pmf f M) (f x) = pmf M x" 

650 
by (auto simp: pmf.rep_eq map_pmf_rep_eq measure_distr AE_measure_pmf_iff inj_onD 

651 
intro!: measure_pmf.finite_measure_eq_AE) 

652 

60068  653 
lemma pmf_map_inj': "inj f \<Longrightarrow> pmf (map_pmf f M) (f x) = pmf M x" 
654 
apply(cases "x \<in> set_pmf M") 

655 
apply(simp add: pmf_map_inj[OF subset_inj_on]) 

656 
apply(simp add: pmf_eq_0_set_pmf[symmetric]) 

657 
apply(auto simp add: pmf_eq_0_set_pmf dest: injD) 

658 
done 

659 

660 
lemma pmf_map_outside: "x \<notin> f ` set_pmf M \<Longrightarrow> pmf (map_pmf f M) x = 0" 

661 
unfolding pmf_eq_0_set_pmf by simp 

662 

59664  663 
subsection \<open> PMFs as function \<close> 
59000  664 

58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

665 
context 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

666 
fixes f :: "'a \<Rightarrow> real" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

667 
assumes nonneg: "\<And>x. 0 \<le> f x" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

668 
assumes prob: "(\<integral>\<^sup>+x. f x \<partial>count_space UNIV) = 1" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

669 
begin 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

670 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

671 
lift_definition embed_pmf :: "'a pmf" is "density (count_space UNIV) (ennreal \<circ> f)" 
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

672 
proof (intro conjI) 
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

673 
have *[simp]: "\<And>x y. ennreal (f y) * indicator {x} y = ennreal (f x) * indicator {x} y" 
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

674 
by (simp split: split_indicator) 
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

675 
show "AE x in density (count_space UNIV) (ennreal \<circ> f). 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

676 
measure (density (count_space UNIV) (ennreal \<circ> f)) {x} \<noteq> 0" 
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59053
diff
changeset

677 
by (simp add: AE_density nonneg measure_def emeasure_density max_def) 
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

678 
show "prob_space (density (count_space UNIV) (ennreal \<circ> f))" 
61169  679 
by standard (simp add: emeasure_density prob) 
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

680 
qed simp 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

681 

5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

682 
lemma pmf_embed_pmf: "pmf embed_pmf x = f x" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

683 
proof transfer 
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

684 
have *[simp]: "\<And>x y. ennreal (f y) * indicator {x} y = ennreal (f x) * indicator {x} y" 
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

685 
by (simp split: split_indicator) 
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

686 
fix x show "measure (density (count_space UNIV) (ennreal \<circ> f)) {x} = f x" 
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59053
diff
changeset

687 
by transfer (simp add: measure_def emeasure_density nonneg max_def) 
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

688 
qed 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

689 

60068  690 
lemma set_embed_pmf: "set_pmf embed_pmf = {x. f x \<noteq> 0}" 
63092  691 
by(auto simp add: set_pmf_eq pmf_embed_pmf) 
60068  692 

58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

693 
end 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

694 

5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

695 
lemma embed_pmf_transfer: 
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

696 
"rel_fun (eq_onp (\<lambda>f. (\<forall>x. 0 \<le> f x) \<and> (\<integral>\<^sup>+x. ennreal (f x) \<partial>count_space UNIV) = 1)) pmf_as_measure.cr_pmf (\<lambda>f. density (count_space UNIV) (ennreal \<circ> f)) embed_pmf" 
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

697 
by (auto simp: rel_fun_def eq_onp_def embed_pmf.transfer) 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

698 

59000  699 
lemma measure_pmf_eq_density: "measure_pmf p = density (count_space UNIV) (pmf p)" 
700 
proof (transfer, elim conjE) 

701 
fix M :: "'a measure" assume [simp]: "sets M = UNIV" and ae: "AE x in M. measure M {x} \<noteq> 0" 

702 
assume "prob_space M" then interpret prob_space M . 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

703 
show "M = density (count_space UNIV) (\<lambda>x. ennreal (measure M {x}))" 
59000  704 
proof (rule measure_eqI) 
705 
fix A :: "'a set" 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

706 
have "(\<integral>\<^sup>+ x. ennreal (measure M {x}) * indicator A x \<partial>count_space UNIV) = 
59000  707 
(\<integral>\<^sup>+ x. emeasure M {x} * indicator (A \<inter> {x. measure M {x} \<noteq> 0}) x \<partial>count_space UNIV)" 
708 
by (auto intro!: nn_integral_cong simp: emeasure_eq_measure split: split_indicator) 

709 
also have "\<dots> = (\<integral>\<^sup>+ x. emeasure M {x} \<partial>count_space (A \<inter> {x. measure M {x} \<noteq> 0}))" 

710 
by (subst nn_integral_restrict_space[symmetric]) (auto simp: restrict_count_space) 

711 
also have "\<dots> = emeasure M (\<Union>x\<in>(A \<inter> {x. measure M {x} \<noteq> 0}). {x})" 

712 
by (intro emeasure_UN_countable[symmetric] countable_Int2 countable_support) 

713 
(auto simp: disjoint_family_on_def) 

714 
also have "\<dots> = emeasure M A" 

715 
using ae by (intro emeasure_eq_AE) auto 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

716 
finally show " emeasure M A = emeasure (density (count_space UNIV) (\<lambda>x. ennreal (measure M {x}))) A" 
59000  717 
using emeasure_space_1 by (simp add: emeasure_density) 
718 
qed simp 

719 
qed 

720 

58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

721 
lemma td_pmf_embed_pmf: 
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

722 
"type_definition pmf embed_pmf {f::'a \<Rightarrow> real. (\<forall>x. 0 \<le> f x) \<and> (\<integral>\<^sup>+x. ennreal (f x) \<partial>count_space UNIV) = 1}" 
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

723 
unfolding type_definition_def 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

724 
proof safe 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

725 
fix p :: "'a pmf" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

726 
have "(\<integral>\<^sup>+ x. 1 \<partial>measure_pmf p) = 1" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

727 
using measure_pmf.emeasure_space_1[of p] by simp 
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

728 
then show *: "(\<integral>\<^sup>+ x. ennreal (pmf p x) \<partial>count_space UNIV) = 1" 
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

729 
by (simp add: measure_pmf_eq_density nn_integral_density pmf_nonneg del: nn_integral_const) 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

730 

5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

731 
show "embed_pmf (pmf p) = p" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

732 
by (intro measure_pmf_inject[THEN iffD1]) 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

733 
(simp add: * embed_pmf.rep_eq pmf_nonneg measure_pmf_eq_density[of p] comp_def) 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

734 
next 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

735 
fix f :: "'a \<Rightarrow> real" assume "\<forall>x. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>count_space UNIV) = 1" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

736 
then show "pmf (embed_pmf f) = f" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

737 
by (auto intro!: pmf_embed_pmf) 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

738 
qed (rule pmf_nonneg) 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

739 

5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

740 
end 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

741 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

742 
lemma nn_integral_measure_pmf: "(\<integral>\<^sup>+ x. f x \<partial>measure_pmf p) = \<integral>\<^sup>+ x. ennreal (pmf p x) * f x \<partial>count_space UNIV" 
60068  743 
by(simp add: measure_pmf_eq_density nn_integral_density pmf_nonneg) 
744 

58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

745 
locale pmf_as_function 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

746 
begin 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

747 

5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

748 
setup_lifting td_pmf_embed_pmf 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

749 

59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59665
diff
changeset

750 
lemma set_pmf_transfer[transfer_rule]: 
58730  751 
assumes "bi_total A" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59665
diff
changeset

752 
shows "rel_fun (pcr_pmf A) (rel_set A) (\<lambda>f. {x. f x \<noteq> 0}) set_pmf" 
61808  753 
using \<open>bi_total A\<close> 
58730  754 
by (auto simp: pcr_pmf_def cr_pmf_def rel_fun_def rel_set_def bi_total_def Bex_def set_pmf_iff) 
755 
metis+ 

756 

59000  757 
end 
758 

759 
context 

760 
begin 

761 

762 
interpretation pmf_as_function . 

763 

764 
lemma pmf_eqI: "(\<And>i. pmf M i = pmf N i) \<Longrightarrow> M = N" 

765 
by transfer auto 

766 

767 
lemma pmf_eq_iff: "M = N \<longleftrightarrow> (\<forall>i. pmf M i = pmf N i)" 

768 
by (auto intro: pmf_eqI) 

769 

63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

770 
lemma pmf_neq_exists_less: 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

771 
assumes "M \<noteq> N" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

772 
shows "\<exists>x. pmf M x < pmf N x" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

773 
proof (rule ccontr) 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

774 
assume "\<not>(\<exists>x. pmf M x < pmf N x)" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

775 
hence ge: "pmf M x \<ge> pmf N x" for x by (auto simp: not_less) 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

776 
from assms obtain x where "pmf M x \<noteq> pmf N x" by (auto simp: pmf_eq_iff) 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

777 
with ge[of x] have gt: "pmf M x > pmf N x" by simp 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

778 
have "1 = measure (measure_pmf M) UNIV" by simp 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

779 
also have "\<dots> = measure (measure_pmf N) {x} + measure (measure_pmf N) (UNIV  {x})" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

780 
by (subst measure_pmf.finite_measure_Union [symmetric]) simp_all 
63886
685fb01256af
move HenstockKurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63882
diff
changeset

781 
also from gt have "measure (measure_pmf N) {x} < measure (measure_pmf M) {x}" 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

782 
by (simp add: measure_pmf_single) 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

783 
also have "measure (measure_pmf N) (UNIV  {x}) \<le> measure (measure_pmf M) (UNIV  {x})" 
63886
685fb01256af
move HenstockKurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63882
diff
changeset

784 
by (subst (1 2) integral_pmf [symmetric]) 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

785 
(intro integral_mono integrable_pmf, simp_all add: ge) 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

786 
also have "measure (measure_pmf M) {x} + \<dots> = 1" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

787 
by (subst measure_pmf.finite_measure_Union [symmetric]) simp_all 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

788 
finally show False by simp_all 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

789 
qed 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

790 

59664  791 
lemma bind_commute_pmf: "bind_pmf A (\<lambda>x. bind_pmf B (C x)) = bind_pmf B (\<lambda>y. bind_pmf A (\<lambda>x. C x y))" 
792 
unfolding pmf_eq_iff pmf_bind 

793 
proof 

794 
fix i 

795 
interpret B: prob_space "restrict_space B B" 

796 
by (intro prob_space_restrict_space measure_pmf.emeasure_eq_1_AE) 

797 
(auto simp: AE_measure_pmf_iff) 

798 
interpret A: prob_space "restrict_space A A" 

799 
by (intro prob_space_restrict_space measure_pmf.emeasure_eq_1_AE) 

800 
(auto simp: AE_measure_pmf_iff) 

801 

802 
interpret AB: pair_prob_space "restrict_space A A" "restrict_space B B" 

803 
by unfold_locales 

804 

805 
have "(\<integral> x. \<integral> y. pmf (C x y) i \<partial>B \<partial>A) = (\<integral> x. (\<integral> y. pmf (C x y) i \<partial>restrict_space B B) \<partial>A)" 

63886
685fb01256af
move HenstockKurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63882
diff
changeset

806 
by (rule Bochner_Integration.integral_cong) (auto intro!: integral_pmf_restrict) 
59664  807 
also have "\<dots> = (\<integral> x. (\<integral> y. pmf (C x y) i \<partial>restrict_space B B) \<partial>restrict_space A A)" 
808 
by (intro integral_pmf_restrict B.borel_measurable_lebesgue_integral measurable_pair_restrict_pmf2 

809 
countable_set_pmf borel_measurable_count_space) 

810 
also have "\<dots> = (\<integral> y. \<integral> x. pmf (C x y) i \<partial>restrict_space A A \<partial>restrict_space B B)" 

811 
by (rule AB.Fubini_integral[symmetric]) 

812 
(auto intro!: AB.integrable_const_bound[where B=1] measurable_pair_restrict_pmf2 

813 
simp: pmf_nonneg pmf_le_1 measurable_restrict_space1) 

814 
also have "\<dots> = (\<integral> y. \<integral> x. pmf (C x y) i \<partial>restrict_space A A \<partial>B)" 

815 
by (intro integral_pmf_restrict[symmetric] A.borel_measurable_lebesgue_integral measurable_pair_restrict_pmf2 

816 
countable_set_pmf borel_measurable_count_space) 

817 
also have "\<dots> = (\<integral> y. \<integral> x. pmf (C x y) i \<partial>A \<partial>B)" 

63886
685fb01256af
move HenstockKurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63882
diff
changeset

818 
by (rule Bochner_Integration.integral_cong) (auto intro!: integral_pmf_restrict[symmetric]) 
59664  819 
finally show "(\<integral> x. \<integral> y. pmf (C x y) i \<partial>B \<partial>A) = (\<integral> y. \<integral> x. pmf (C x y) i \<partial>A \<partial>B)" . 
820 
qed 

821 

822 
lemma pair_map_pmf1: "pair_pmf (map_pmf f A) B = map_pmf (apfst f) (pair_pmf A B)" 

823 
proof (safe intro!: pmf_eqI) 

824 
fix a :: "'a" and b :: "'b" 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

825 
have [simp]: "\<And>c d. indicator (apfst f ` {(a, b)}) (c, d) = indicator (f ` {a}) c * (indicator {b} d::ennreal)" 
59664  826 
by (auto split: split_indicator) 
827 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

828 
have "ennreal (pmf (pair_pmf (map_pmf f A) B) (a, b)) = 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

829 
ennreal (pmf (map_pmf (apfst f) (pair_pmf A B)) (a, b))" 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

830 
unfolding pmf_pair ennreal_pmf_map 
59664  831 
by (simp add: nn_integral_pair_pmf' max_def emeasure_pmf_single nn_integral_multc pmf_nonneg 
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

832 
emeasure_map_pmf[symmetric] ennreal_mult del: emeasure_map_pmf) 
59664  833 
then show "pmf (pair_pmf (map_pmf f A) B) (a, b) = pmf (map_pmf (apfst f) (pair_pmf A B)) (a, b)" 
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

834 
by (simp add: pmf_nonneg) 
59664  835 
qed 
836 

837 
lemma pair_map_pmf2: "pair_pmf A (map_pmf f B) = map_pmf (apsnd f) (pair_pmf A B)" 

838 
proof (safe intro!: pmf_eqI) 

839 
fix a :: "'a" and b :: "'b" 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

840 
have [simp]: "\<And>c d. indicator (apsnd f ` {(a, b)}) (c, d) = indicator {a} c * (indicator (f ` {b}) d::ennreal)" 
59664  841 
by (auto split: split_indicator) 
842 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

843 
have "ennreal (pmf (pair_pmf A (map_pmf f B)) (a, b)) = 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

844 
ennreal (pmf (map_pmf (apsnd f) (pair_pmf A B)) (a, b))" 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

845 
unfolding pmf_pair ennreal_pmf_map 
59664  846 
by (simp add: nn_integral_pair_pmf' max_def emeasure_pmf_single nn_integral_cmult nn_integral_multc pmf_nonneg 
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

847 
emeasure_map_pmf[symmetric] ennreal_mult del: emeasure_map_pmf) 
59664  848 
then show "pmf (pair_pmf A (map_pmf f B)) (a, b) = pmf (map_pmf (apsnd f) (pair_pmf A B)) (a, b)" 
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

849 
by (simp add: pmf_nonneg) 
59664  850 
qed 
851 

852 
lemma map_pair: "map_pmf (\<lambda>(a, b). (f a, g b)) (pair_pmf A B) = pair_pmf (map_pmf f A) (map_pmf g B)" 

853 
by (simp add: pair_map_pmf2 pair_map_pmf1 map_pmf_comp split_beta') 

854 

59000  855 
end 
856 

61634  857 
lemma pair_return_pmf1: "pair_pmf (return_pmf x) y = map_pmf (Pair x) y" 
858 
by(simp add: pair_pmf_def bind_return_pmf map_pmf_def) 

859 

860 
lemma pair_return_pmf2: "pair_pmf x (return_pmf y) = map_pmf (\<lambda>x. (x, y)) x" 

861 
by(simp add: pair_pmf_def bind_return_pmf map_pmf_def) 

862 

863 
lemma pair_pair_pmf: "pair_pmf (pair_pmf u v) w = map_pmf (\<lambda>(x, (y, z)). ((x, y), z)) (pair_pmf u (pair_pmf v w))" 

864 
by(simp add: pair_pmf_def bind_return_pmf map_pmf_def bind_assoc_pmf) 

865 

866 
lemma pair_commute_pmf: "pair_pmf x y = map_pmf (\<lambda>(x, y). (y, x)) (pair_pmf y x)" 

867 
unfolding pair_pmf_def by(subst bind_commute_pmf)(simp add: map_pmf_def bind_assoc_pmf bind_return_pmf) 

868 

869 
lemma set_pmf_subset_singleton: "set_pmf p \<subseteq> {x} \<longleftrightarrow> p = return_pmf x" 

870 
proof(intro iffI pmf_eqI) 

871 
fix i 

872 
assume x: "set_pmf p \<subseteq> {x}" 

873 
hence *: "set_pmf p = {x}" using set_pmf_not_empty[of p] by auto 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

874 
have "ennreal (pmf p x) = \<integral>\<^sup>+ i. indicator {x} i \<partial>p" by(simp add: emeasure_pmf_single) 
61634  875 
also have "\<dots> = \<integral>\<^sup>+ i. 1 \<partial>p" by(rule nn_integral_cong_AE)(simp add: AE_measure_pmf_iff * ) 
876 
also have "\<dots> = 1" by simp 

877 
finally show "pmf p i = pmf (return_pmf x) i" using x 

878 
by(auto split: split_indicator simp add: pmf_eq_0_set_pmf) 

879 
qed auto 

880 

881 
lemma bind_eq_return_pmf: 

882 
"bind_pmf p f = return_pmf x \<longleftrightarrow> (\<forall>y\<in>set_pmf p. f y = return_pmf x)" 

883 
(is "?lhs \<longleftrightarrow> ?rhs") 

884 
proof(intro iffI strip) 

885 
fix y 

886 
assume y: "y \<in> set_pmf p" 

887 
assume "?lhs" 

888 
hence "set_pmf (bind_pmf p f) = {x}" by simp 

889 
hence "(\<Union>y\<in>set_pmf p. set_pmf (f y)) = {x}" by simp 

890 
hence "set_pmf (f y) \<subseteq> {x}" using y by auto 

891 
thus "f y = return_pmf x" by(simp add: set_pmf_subset_singleton) 

892 
next 

893 
assume *: ?rhs 

894 
show ?lhs 

895 
proof(rule pmf_eqI) 

896 
fix i 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

897 
have "ennreal (pmf (bind_pmf p f) i) = \<integral>\<^sup>+ y. ennreal (pmf (f y) i) \<partial>p" 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

898 
by (simp add: ennreal_pmf_bind) 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

899 
also have "\<dots> = \<integral>\<^sup>+ y. ennreal (pmf (return_pmf x) i) \<partial>p" 
61634  900 
by(rule nn_integral_cong_AE)(simp add: AE_measure_pmf_iff * ) 
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

901 
also have "\<dots> = ennreal (pmf (return_pmf x) i)" 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

902 
by simp 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

903 
finally show "pmf (bind_pmf p f) i = pmf (return_pmf x) i" 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

904 
by (simp add: pmf_nonneg) 
61634  905 
qed 
906 
qed 

907 

908 
lemma pmf_False_conv_True: "pmf p False = 1  pmf p True" 

909 
proof  

910 
have "pmf p False + pmf p True = measure p {False} + measure p {True}" 

911 
by(simp add: measure_pmf_single) 

912 
also have "\<dots> = measure p ({False} \<union> {True})" 

913 
by(subst measure_pmf.finite_measure_Union) simp_all 

914 
also have "{False} \<union> {True} = space p" by auto 

915 
finally show ?thesis by simp 

916 
qed 

917 

918 
lemma pmf_True_conv_False: "pmf p True = 1  pmf p False" 

919 
by(simp add: pmf_False_conv_True) 

920 

59664  921 
subsection \<open> Conditional Probabilities \<close> 
922 

59670  923 
lemma measure_pmf_zero_iff: "measure (measure_pmf p) s = 0 \<longleftrightarrow> set_pmf p \<inter> s = {}" 
924 
by (subst measure_pmf.prob_eq_0) (auto simp: AE_measure_pmf_iff) 

925 

59664  926 
context 
927 
fixes p :: "'a pmf" and s :: "'a set" 

928 
assumes not_empty: "set_pmf p \<inter> s \<noteq> {}" 

929 
begin 

930 

931 
interpretation pmf_as_measure . 

932 

933 
lemma emeasure_measure_pmf_not_zero: "emeasure (measure_pmf p) s \<noteq> 0" 

934 
proof 

935 
assume "emeasure (measure_pmf p) s = 0" 

936 
then have "AE x in measure_pmf p. x \<notin> s" 

937 
by (rule AE_I[rotated]) auto 

938 
with not_empty show False 

939 
by (auto simp: AE_measure_pmf_iff) 

940 
qed 

941 

942 
lemma measure_measure_pmf_not_zero: "measure (measure_pmf p) s \<noteq> 0" 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

943 
using emeasure_measure_pmf_not_zero by (simp add: measure_pmf.emeasure_eq_measure measure_nonneg) 
59664  944 

945 
lift_definition cond_pmf :: "'a pmf" is 

946 
"uniform_measure (measure_pmf p) s" 

947 
proof (intro conjI) 

948 
show "prob_space (uniform_measure (measure_pmf p) s)" 

949 
by (intro prob_space_uniform_measure) (auto simp: emeasure_measure_pmf_not_zero) 

950 
show "AE x in uniform_measure (measure_pmf p) s. measure (uniform_measure (measure_pmf p) s) {x} \<noteq> 0" 

951 
by (simp add: emeasure_measure_pmf_not_zero measure_measure_pmf_not_zero AE_uniform_measure 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

952 
AE_measure_pmf_iff set_pmf.rep_eq less_top[symmetric]) 
59664  953 
qed simp 
954 

955 
lemma pmf_cond: "pmf cond_pmf x = (if x \<in> s then pmf p x / measure p s else 0)" 

956 
by transfer (simp add: emeasure_measure_pmf_not_zero pmf.rep_eq) 

957 

59665  958 
lemma set_cond_pmf[simp]: "set_pmf cond_pmf = set_pmf p \<inter> s" 
62390  959 
by (auto simp add: set_pmf_iff pmf_cond measure_measure_pmf_not_zero split: if_split_asm) 
59664  960 

961 
end 

962 

63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

963 
lemma measure_pmf_posI: "x \<in> set_pmf p \<Longrightarrow> x \<in> A \<Longrightarrow> measure_pmf.prob p A > 0" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

964 
using measure_measure_pmf_not_zero[of p A] by (subst zero_less_measure_iff) blast 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

965 

59664  966 
lemma cond_map_pmf: 
967 
assumes "set_pmf p \<inter> f ` s \<noteq> {}" 

968 
shows "cond_pmf (map_pmf f p) s = map_pmf f (cond_pmf p (f ` s))" 

969 
proof  

970 
have *: "set_pmf (map_pmf f p) \<inter> s \<noteq> {}" 

59665  971 
using assms by auto 
59664  972 
{ fix x 
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

973 
have "ennreal (pmf (map_pmf f (cond_pmf p (f ` s))) x) = 
59664  974 
emeasure p (f ` s \<inter> f ` {x}) / emeasure p (f ` s)" 
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

975 
unfolding ennreal_pmf_map cond_pmf.rep_eq[OF assms] by (simp add: nn_integral_uniform_measure) 
59664  976 
also have "f ` s \<inter> f ` {x} = (if x \<in> s then f ` {x} else {})" 
977 
by auto 

978 
also have "emeasure p (if x \<in> s then f ` {x} else {}) / emeasure p (f ` s) = 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

979 
ennreal (pmf (cond_pmf (map_pmf f p) s) x)" 
59664  980 
using measure_measure_pmf_not_zero[OF *] 
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

981 
by (simp add: pmf_cond[OF *] ennreal_pmf_map measure_pmf.emeasure_eq_measure 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

982 
divide_ennreal pmf_nonneg measure_nonneg zero_less_measure_iff pmf_map) 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

983 
finally have "ennreal (pmf (cond_pmf (map_pmf f p) s) x) = ennreal (pmf (map_pmf f (cond_pmf p (f ` s))) x)" 
59664  984 
by simp } 
985 
then show ?thesis 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

986 
by (intro pmf_eqI) (simp add: pmf_nonneg) 
59664  987 
qed 
988 

989 
lemma bind_cond_pmf_cancel: 

59670  990 
assumes [simp]: "\<And>x. x \<in> set_pmf p \<Longrightarrow> set_pmf q \<inter> {y. R x y} \<noteq> {}" 
991 
assumes [simp]: "\<And>y. y \<in> set_pmf q \<Longrightarrow> set_pmf p \<inter> {x. R x y} \<noteq> {}" 

992 
assumes [simp]: "\<And>x y. x \<in> set_pmf p \<Longrightarrow> y \<in> set_pmf q \<Longrightarrow> R x y \<Longrightarrow> measure q {y. R x y} = measure p {x. R x y}" 

993 
shows "bind_pmf p (\<lambda>x. cond_pmf q {y. R x y}) = q" 

59664  994 
proof (rule pmf_eqI) 
59670  995 
fix i 
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

996 
have "ennreal (pmf (bind_pmf p (\<lambda>x. cond_pmf q {y. R x y})) i) = 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

997 
(\<integral>\<^sup>+x. ennreal (pmf q i / measure p {x. R x i}) * ennreal (indicator {x. R x i} x) \<partial>p)" 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

998 
by (auto simp add: ennreal_pmf_bind AE_measure_pmf_iff pmf_cond pmf_eq_0_set_pmf pmf_nonneg measure_nonneg 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

999 
intro!: nn_integral_cong_AE) 
59670  1000 
also have "\<dots> = (pmf q i * measure p {x. R x i}) / measure p {x. R x i}" 
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

1001 
by (simp add: pmf_nonneg measure_nonneg zero_ennreal_def[symmetric] ennreal_indicator 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

1002 
nn_integral_cmult measure_pmf.emeasure_eq_measure ennreal_mult[symmetric]) 
59670  1003 
also have "\<dots> = pmf q i" 
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

1004 
by (cases "pmf q i = 0") 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

1005 
(simp_all add: pmf_eq_0_set_pmf measure_measure_pmf_not_zero pmf_nonneg) 
59670  1006 
finally show "pmf (bind_pmf p (\<lambda>x. cond_pmf q {y. R x y})) i = pmf q i" 
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset

1007 
by (simp add: pmf_nonneg) 
59664  1008 
qed 
1009 

1010 
subsection \<open> Relator \<close> 

1011 

1012 
inductive rel_pmf :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a pmf \<Rightarrow> 'b pmf \<Rightarrow> bool" 

1013 
for R p q 

1014 
where 

59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59665
diff
changeset

1015 
"\<lbrakk> \<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y; 
59664  1016 
map_pmf fst pq = p; map_pmf snd pq = q \<rbrakk> 
1017 
\<Longrightarrow> rel_pmf R p q" 

1018 

59681  1019 
lemma rel_pmfI: 
1020 
assumes R: "rel_set R (set_pmf p) (set_pmf q)" 

1021 
assumes eq: "\<And>x y. x \<in> set_pmf p \<Longrightarrow> y \<in> set_pmf q \<Longrightarrow> R x y \<Longrightarrow> 

1022 
measure p {x. R x y} = measure q {y. R x y}" 

1023 
shows "rel_pmf R p q" 

1024 
proof 

1025 
let ?pq = "bind_pmf p (\<lambda>x. bind_pmf (cond_pmf q {y. R x y}) (\<lambda>y. return_pmf (x, y)))" 

1026 
have "\<And>x. x \<in> set_pmf p \<Longrightarrow> set_pmf q \<inter> {y. R x y} \<noteq> {}" 

1027 
using R by (auto simp: rel_set_def) 

1028 
then show "\<And>x y. (x, y) \<in> set_pmf ?pq \<Longrightarrow> R x y" 

1029 
by auto 

1030 
show "map_pmf fst ?pq = p" 

60068  1031 
by (simp add: map_bind_pmf bind_return_pmf') 
59681  1032 

1033 
show "map_pmf snd ?pq = q" 

1034 
using R eq 

60068  1035 
apply (simp add: bind_cond_pmf_cancel map_bind_pmf bind_return_pmf') 
59681  1036 
apply (rule bind_cond_pmf_cancel) 
1037 
apply (auto simp: rel_set_def) 

1038 
done 

1039 
qed 

1040 

1041 
lemma rel_pmf_imp_rel_set: "rel_pmf R p q \<Longrightarrow> rel_set R (set_pmf p) (set_pmf q)" 

1042 
by (force simp add: rel_pmf.simps rel_set_def) 

1043 

1044 
lemma rel_pmfD_measure: 

1045 
assumes rel_R: "rel_pmf R p q" and R: "\<And>a b. R a b \<Longrightarrow> R a y \<longleftrightarrow> R x b" 

1046 
assumes "x \<in> set_pmf p" "y \<in> set_pmf q" 

1047 
shows "measure p {x. R x y} = measure q {y. R x y}" 

1048 
proof  

1049 
from rel_R obtain pq where pq: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y" 

1050 
and eq: "p = map_pmf fst pq" "q = map_pmf snd pq" 

1051 
by (auto elim: rel_pmf.cases) 

1052 
have "measure p {x. R x y} = measure pq {x. R (fst x) y}" 

1053 
by (simp add: eq map_pmf_rep_eq measure_distr) 

1054 
also have "\<dots> = measure pq {y. R x (snd y)}" 

1055 
by (intro measure_pmf.finite_measure_eq_AE) 

1056 
(auto simp: AE_measure_pmf_iff R dest!: pq) 

1057 
also have "\<dots> = measure q {y. R x y}" 

1058 
by (simp add: eq map_pmf_rep_eq measure_distr) 

1059 
finally show "measure p {x. R x y} = measure q {y. R x y}" . 

1060 
qed 

1061 

61634  1062 
lemma rel_pmf_measureD: 
1063 
assumes "rel_pmf R p q" 

1064 
shows "measure (measure_pmf p) A \<le> measure (measure_pmf q) {y. \<exists>x\<in>A. R x y}" (is "?lhs \<le> ?rhs") 

1065 
using assms 

1066 
proof cases 

1067 
fix pq 

1068 
assume R: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y" 

1069 
and p[symmetric]: "map_pmf fst pq = p" 

1070 
and q[symmetric]: "map_pmf snd pq = q" 

1071 
have "?lhs = measure (measure_pmf pq) (fst ` A)" by(simp add: p) 

1072 
also have "\<dots> \<le> measure (measure_pmf pq) {y. \<exists>x\<in>A. R x (snd y)}" 

1073 
by(rule measure_pmf.finite_measure_mono_AE)(auto 4 3 simp add: AE_measure_pmf_iff dest: R) 

1074 
also have "\<dots> = ?rhs" by(simp add: q) 

1075 
finally show ?thesis . 

1076 
qed 

1077 

59681  1078 
lemma rel_pmf_iff_measure: 
1079 
assumes "symp R" "transp R" 

1080 
shows "rel_pmf R p q \<longleftrightarrow> 

1081 
rel_set R (set_pmf p) (set_pmf q) \<and> 

1082 
(\<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})" 

1083 
by (safe intro!: rel_pmf_imp_rel_set rel_pmfI) 

1084 
(auto intro!: rel_pmfD_measure dest: sympD[OF \<open>symp R\<close>] transpD[OF \<open>transp R\<close>]) 

1085 

1086 
lemma quotient_rel_set_disjoint: 

1087 
"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 = {}" 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

1088 
using in_quotient_imp_closed[of UNIV "{(x, y). R x y}" C] 
59681  1089 
by (auto 0 0 simp: equivp_equiv rel_set_def set_eq_iff elim: equivpE) 
1090 
(blast dest: equivp_symp)+ 

1091 

1092 
lemma quotientD: "equiv X R \<Longrightarrow> A \<in> X // R \<Longrightarrow> x \<in> A \<Longrightarrow> A = R `` {x}" 

1093 
by (metis Image_singleton_iff equiv_class_eq_iff quotientE) 

1094 

1095 
lemma rel_pmf_iff_equivp: 

1096 
assumes "equivp R" 

1097 
shows "rel_pmf R p q \<longleftrightarrow> (\<forall>C\<in>UNIV // {(x, y). R x y}. measure p C = measure q C)" 

1098 
(is "_ \<longleftrightarrow> (\<forall>C\<in>_//?R. _)") 

1099 
proof (subst rel_pmf_iff_measure, safe) 

1100 
show "symp R" "transp R" 

1101 
using assms by (auto simp: equivp_reflp_symp_transp) 

1102 
next 

1103 
fix C assume C: "C \<in> UNIV // ?R" and R: "rel_set R (set_pmf p) (set_pmf q)" 

1104 
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}" 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

1105 

59681  1106 
show "measure p C = measure q C" 
63540  1107 
proof (cases "p \<inter> C = {}") 
1108 
case True 

1109 
then have "q \<inter> C = {}" 

59681  1110 
using quotient_rel_set_disjoint[OF assms C R] by simp 
63540  1111 
with True show ?thesis 
59681  1112 
unfolding measure_pmf_zero_iff[symmetric] by simp 
1113 
next 

63540  1114 
case False 
1115 
then have "q \<inter> C \<noteq> {}" 

59681  1116 
using quotient_rel_set_disjoint[OF assms C R] by simp 
63540  1117 
with False 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" 
59681  1118 
by auto 
1119 
then have "R x y" 

1120 
using in_quotient_imp_in_rel[of UNIV ?R C x y] C assms 

1121 
by (simp add: equivp_equiv) 

1122 
with in_set eq have "measure p {x. R x y} = measure q {y. R x y}" 

1123 
by auto 

1124 
moreover have "{y. R x y} = C" 

61808  1125 
using assms \<open>x \<in> C\<close> C quotientD[of UNIV ?R C x] by (simp add: equivp_equiv) 
59681  1126 
moreover have "{x. R x y} = C" 
61808  1127 
using assms \<open>y \<in> C\<close> C quotientD[of UNIV "?R" C y] sympD[of R] 
59681  1128 
by (auto simp add: equivp_equiv elim: equivpE) 
1129 
ultimately show ?thesis 

1130 
by auto 

1131 
qed 

1132 
next 

1133 
assume eq: "\<forall>C\<in>UNIV // ?R. measure p C = measure q C" 

1134 
show "rel_set R (set_pmf p) (set_pmf q)" 

1135 
unfolding rel_set_def 

1136 
proof safe 

1137 
fix x assume x: "x \<in> set_pmf p" 

1138 
have "{y. R x y} \<in> UNIV // ?R" 

1139 
by (auto simp: quotient_def) 

1140 
with eq have *: "measure q {y. R x y} = measure p {y. R x y}" 

1141 
by auto 

1142 
have "measure q {y. R x y} \<noteq> 0" 

1143 
using x assms unfolding * by (auto simp: measure_pmf_zero_iff set_eq_iff dest: equivp_reflp) 

1144 
then show "\<exists>y\<in>set_pmf q. R x y" 

1145 
unfolding measure_pmf_zero_iff by auto 

1146 
next 

1147 
fix y assume y: "y \<in> set_pmf q" 

1148 
have "{x. R x y} \<in> UNIV // ?R" 

1149 
using assms by (auto simp: quotient_def dest: equivp_symp) 

1150 
with eq have *: "measure p {x. R x y} = measure q {x. R x y}" 

1151 
by auto 

1152 
have "measure p {x. R x y} \<noteq> 0" 

1153 
using y assms unfolding * by (auto simp: measure_pmf_zero_iff set_eq_iff dest: equivp_reflp) 

1154 
then show "\<exists>x\<in>set_pmf p. R x y" 

1155 
unfolding measure_pmf_zero_iff by auto 

1156 
qed 

1157 

1158 
fix x y assume "x \<in> set_pmf p" "y \<in> set_pmf q" "R x y" 

1159 
have "{y. R x y} \<in> UNIV // ?R" "{x. R x y} = {y. R x y}" 

61808  1160 
using assms \<open>R x y\<close> by (auto simp: quotient_def dest: equivp_symp equivp_transp) 
59681  1161 
with eq show "measure p {x. R x y} = measure q {y. R x y}" 
1162 
by auto 

1163 
qed 

1164 

59664  1165 
bnf pmf: "'a pmf" map: map_pmf sets: set_pmf bd : "natLeq" rel: rel_pmf 
1166 
proof  

1167 
show "map_pmf id = id" by (rule map_pmf_id) 

59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59665
diff
changeset

1168 
show "\<And>f g. map_pmf (f \<circ> g) = map_pmf f \<circ> map_pmf g" by (rule map_pmf_compose) 
59664  1169 
show "\<And>f g::'a \<Rightarrow> 'b. \<And>p. (\<And>x. x \<in> set_pmf p \<Longrightarrow> f x = g x) \<Longrightarrow> map_pmf f p = map_pmf g p" 
1170 
by (intro map_pmf_cong refl) 

1171 

1172 
show "\<And>f::'a \<Rightarrow> 'b. set 