author  hoelzl 
Wed, 17 Jun 2015 18:44:23 +0200  
changeset 60602  37588fbe39f9 
parent 60595  804dfdc82835 
child 61169  4de9ff3ea29a 
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 

25 
by (auto simp: emeasure_le_0_iff) } 

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 

59494  32 
lemma ereal_divide': "b \<noteq> 0 \<Longrightarrow> ereal (a / b) = ereal a / ereal b" 
33 
using ereal_divide[of a b] by simp 

34 

59052  35 
lemma (in finite_measure) countable_support: 
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

36 
"countable {x. measure M {x} \<noteq> 0}" 
59000  37 
proof cases 
38 
assume "measure M (space M) = 0" 

39 
with bounded_measure measure_le_0_iff have "{x. measure M {x} \<noteq> 0} = {}" 

40 
by auto 

41 
then show ?thesis 

42 
by simp 

43 
next 

44 
let ?M = "measure M (space M)" and ?m = "\<lambda>x. measure M {x}" 

45 
assume "?M \<noteq> 0" 

46 
then have *: "{x. ?m x \<noteq> 0} = (\<Union>n. {x. ?M / Suc n < ?m x})" 

47 
using reals_Archimedean[of "?m x / ?M" for x] 

48 
by (auto simp: field_simps not_le[symmetric] measure_nonneg divide_le_0_iff measure_le_0_iff) 

49 
have **: "\<And>n. finite {x. ?M / Suc n < ?m x}" 

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

50 
proof (rule ccontr) 
59000  51 
fix n assume "infinite {x. ?M / Suc n < ?m x}" (is "infinite ?X") 
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

52 
then obtain X where "finite X" "card X = Suc (Suc n)" "X \<subseteq> ?X" 
58606  53 
by (metis infinite_arbitrarily_large) 
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

54 
from this(3) have *: "\<And>x. x \<in> X \<Longrightarrow> ?M / Suc n \<le> ?m x" 
59000  55 
by auto 
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

56 
{ fix x assume "x \<in> X" 
59000  57 
from `?M \<noteq> 0` *[OF this] have "?m x \<noteq> 0" by (auto simp: field_simps measure_le_0_iff) 
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

58 
then have "{x} \<in> sets M" by (auto dest: measure_notin_sets) } 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

59 
note singleton_sets = this 
59000  60 
have "?M < (\<Sum>x\<in>X. ?M / Suc n)" 
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

61 
using `?M \<noteq> 0` 
59000  62 
by (simp add: `card X = Suc (Suc n)` real_eq_of_nat[symmetric] real_of_nat_Suc field_simps less_le measure_nonneg) 
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

63 
also have "\<dots> \<le> (\<Sum>x\<in>X. ?m x)" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

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

65 
also have "\<dots> = measure M (\<Union>x\<in>X. {x})" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

66 
using singleton_sets `finite X` 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

67 
by (intro finite_measure_finite_Union[symmetric]) (auto simp: disjoint_family_on_def) 
59000  68 
finally have "?M < measure M (\<Union>x\<in>X. {x})" . 
69 
moreover have "measure M (\<Union>x\<in>X. {x}) \<le> ?M" 

70 
using singleton_sets[THEN sets.sets_into_space] by (intro finite_measure_mono) auto 

71 
ultimately show False by simp 

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

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

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

74 
unfolding * by (intro countable_UN countableI_type countable_finite[OF **]) 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

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

76 

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

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

80 
proof 

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

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

83 
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

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

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

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

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

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

91 
by (subst emeasure_UN_countable) 

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

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

94 
using ae by (intro emeasure_eq_AE) auto 

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

96 
by (simp add: emeasure_single_in_space cong: rev_conj_cong) 

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

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

99 
by (intro AE_I[OF order_refl]) (auto simp: emeasure_eq_measure set_diff_eq cong: conj_cong) 

100 
then show "AE x in M. measure M {x} \<noteq> 0" 

101 
by (auto simp: emeasure_eq_measure) 

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

103 

59664  104 
subsection \<open> PMF as measure \<close> 
59000  105 

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

106 
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

107 
morphisms measure_pmf Abs_pmf 
58606  108 
by (intro exI[of _ "uniform_measure (count_space UNIV) {undefined}"]) 
109 
(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

110 

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

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

112 

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

113 
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

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

115 

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

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

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

118 

59000  119 
interpretation measure_pmf!: subprob_space "measure_pmf M" for M 
120 
by (rule prob_space_imp_subprob_space) unfold_locales 

121 

59048  122 
lemma subprob_space_measure_pmf: "subprob_space (measure_pmf x)" 
123 
by unfold_locales 

124 

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

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

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

127 

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

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

129 

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

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

131 

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

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

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

134 

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

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

136 

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

137 
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

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

139 

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

59000  142 
by simp 
143 

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

144 
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

145 
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

146 

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

149 

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

150 
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

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

152 

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

153 
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

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

155 

59664  156 
lemma measurable_pair_restrict_pmf2: 
157 
assumes "countable A" 

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

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

160 
proof  

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

162 
by (simp add: restrict_count_space) 

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

163 

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

166 
unfolded pair_collapse] assms) 

167 
measurable 

168 
qed 

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

169 

59664  170 
lemma measurable_pair_restrict_pmf1: 
171 
assumes "countable A" 

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

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

174 
proof  

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

176 
by (simp add: restrict_count_space) 

59000  177 

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

180 
unfolded pair_collapse] assms) 

181 
measurable 

182 
qed 

183 

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

185 

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

187 
declare [[coercion set_pmf]] 

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

188 

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

189 
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

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

191 

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

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

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

194 
shows "emeasure M {y} = 0 \<longleftrightarrow> y \<notin> M" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

195 
by transfer (simp add: finite_measure.emeasure_eq_measure[OF prob_space.finite_measure]) 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

196 

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

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

200 

201 
lemma countable_set_pmf [simp]: "countable (set_pmf p)" 

202 
by transfer (metis prob_space.finite_measure finite_measure.countable_support) 

203 

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

205 
by transfer (simp add: less_le measure_nonneg) 

206 

207 
lemma pmf_nonneg: "0 \<le> pmf p x" 

208 
by transfer (simp add: measure_nonneg) 

209 

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

211 
by (simp add: pmf.rep_eq) 

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

212 

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

213 
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

214 
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

215 

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

216 
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

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

218 

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

221 

222 
lemma emeasure_pmf_single: 

223 
fixes M :: "'a pmf" 

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

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

226 

60068  227 
lemma measure_pmf_single: "measure (measure_pmf M) {x} = pmf M x" 
228 
using emeasure_pmf_single[of M x] by(simp add: measure_pmf.emeasure_eq_measure) 

229 

59000  230 
lemma emeasure_measure_pmf_finite: "finite S \<Longrightarrow> emeasure (measure_pmf M) S = (\<Sum>s\<in>S. pmf M s)" 
231 
by (subst emeasure_eq_setsum_singleton) (auto simp: emeasure_pmf_single) 

232 

59023  233 
lemma measure_measure_pmf_finite: "finite S \<Longrightarrow> measure (measure_pmf M) S = setsum (pmf M) S" 
59425  234 
using emeasure_measure_pmf_finite[of S M] by(simp add: measure_pmf.emeasure_eq_measure) 
59023  235 

59000  236 
lemma nn_integral_measure_pmf_support: 
237 
fixes f :: "'a \<Rightarrow> ereal" 

238 
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" 

239 
shows "(\<integral>\<^sup>+x. f x \<partial>measure_pmf M) = (\<Sum>x\<in>A. f x * pmf M x)" 

240 
proof  

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

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

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

244 
using assms by (intro nn_integral_indicator_finite) auto 

245 
finally show ?thesis 

246 
by (simp add: emeasure_measure_pmf_finite) 

247 
qed 

248 

249 
lemma nn_integral_measure_pmf_finite: 

250 
fixes f :: "'a \<Rightarrow> ereal" 

251 
assumes f: "finite (set_pmf M)" and nn: "\<And>x. x \<in> set_pmf M \<Longrightarrow> 0 \<le> f x" 

252 
shows "(\<integral>\<^sup>+x. f x \<partial>measure_pmf M) = (\<Sum>x\<in>set_pmf M. f x * pmf M x)" 

253 
using assms by (intro nn_integral_measure_pmf_support) auto 

254 
lemma integrable_measure_pmf_finite: 

255 
fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" 

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

257 
by (auto intro!: integrableI_bounded simp: nn_integral_measure_pmf_finite) 

258 

259 
lemma integral_measure_pmf: 

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

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

262 
proof  

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

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

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

266 
by (subst integral_indicator_finite_real) (auto simp: measure_def emeasure_measure_pmf_finite) 

267 
finally show ?thesis . 

268 
qed 

269 

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

271 
proof  

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

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

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

275 
by (simp add: integrable_iff_bounded pmf_nonneg) 

276 
then show ?thesis 

59023  277 
by (simp add: pmf.rep_eq measure_pmf.integrable_measure disjoint_family_on_def) 
59000  278 
qed 
279 

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

281 
proof  

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

283 
by (simp add: pmf_nonneg integrable_pmf nn_integral_eq_integral) 

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

285 
by (auto intro!: nn_integral_cong_AE split: split_indicator 

286 
simp: pmf.rep_eq measure_pmf.emeasure_eq_measure nn_integral_count_space_indicator 

287 
AE_count_space set_pmf_iff) 

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

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

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

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

292 
finally show ?thesis 

293 
by (simp add: measure_pmf.emeasure_eq_measure) 

294 
qed 

295 

296 
lemma integral_pmf_restrict: 

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

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

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

300 

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

301 
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

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

303 
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

304 
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

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

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

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

308 

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

311 

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

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

315 
by(auto simp add: null_sets_def AE_measure_pmf_iff) 

316 

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

319 

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

321 

322 
lemma measurable_measure_pmf[measurable]: 

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

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

325 

326 
lemma bind_measure_pmf_cong: 

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

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

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

330 
proof (rule measure_eqI) 

331 
show "sets (measure_pmf x \<guillemotright>= A) = sets (measure_pmf x \<guillemotright>= B)" 

332 
using assms by (subst (1 2) sets_bind) (auto simp: space_subprob_algebra) 

333 
next 

334 
fix X assume "X \<in> sets (measure_pmf x \<guillemotright>= A)" 

335 
then have X: "X \<in> sets N" 

336 
using assms by (subst (asm) sets_bind) (auto simp: space_subprob_algebra) 

337 
show "emeasure (measure_pmf x \<guillemotright>= A) X = emeasure (measure_pmf x \<guillemotright>= B) X" 

338 
using assms 

339 
by (subst (1 2) emeasure_bind[where N=N, OF _ _ X]) 

340 
(auto intro!: nn_integral_cong_AE simp: AE_measure_pmf_iff) 

341 
qed 

342 

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

344 
proof (clarify, intro conjI) 

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

346 
assume "prob_space f" 

347 
then interpret f: prob_space f . 

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

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

350 
by simp 

351 
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)" 

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

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

354 
by auto 

355 

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

357 
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

358 

59664  359 
show "prob_space (f \<guillemotright>= g)" 
360 
using g by (intro f.prob_space_bind[where S="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

361 
then interpret fg: prob_space "f \<guillemotright>= g" . 
59664  362 
show [simp]: "sets (f \<guillemotright>= g) = UNIV" 
363 
using sets_eq_imp_space_eq[OF s_f] 

364 
by (subst sets_bind[where N="count_space UNIV"]) auto 

365 
show "AE x in f \<guillemotright>= g. measure (f \<guillemotright>= g) {x} \<noteq> 0" 

366 
apply (simp add: fg.prob_eq_0 AE_bind[where B="count_space UNIV"]) 

367 
using ae_f 

368 
apply eventually_elim 

369 
using ae_g 

370 
apply eventually_elim 

371 
apply (auto dest: AE_measure_singleton) 

372 
done 

373 
qed 

374 

375 
lemma ereal_pmf_bind: "pmf (bind_pmf N f) i = (\<integral>\<^sup>+x. pmf (f x) i \<partial>measure_pmf N)" 

376 
unfolding pmf.rep_eq bind_pmf.rep_eq 

377 
by (auto simp: measure_pmf.measure_bind[where N="count_space UNIV"] measure_subprob measure_nonneg 

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

379 

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

381 
using ereal_pmf_bind[of N f i] 

382 
by (subst (asm) nn_integral_eq_integral) 

383 
(auto simp: pmf_nonneg pmf_le_1 

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

385 

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

387 
by transfer (simp add: bind_const' prob_space_imp_subprob_space) 

388 

59665  389 
lemma set_bind_pmf[simp]: "set_pmf (bind_pmf M N) = (\<Union>M\<in>set_pmf M. set_pmf (N M))" 
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

390 
unfolding set_pmf_eq ereal_eq_0(1)[symmetric] ereal_pmf_bind 
59664  391 
by (auto simp add: nn_integral_0_iff_AE AE_measure_pmf_iff set_pmf_eq not_le less_le pmf_nonneg) 
392 

393 
lemma bind_pmf_cong: 

394 
assumes "p = q" 

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

396 
unfolding `p = q`[symmetric] measure_pmf_inject[symmetric] bind_pmf.rep_eq 

397 
by (auto simp: AE_measure_pmf_iff Pi_iff space_subprob_algebra subprob_space_measure_pmf 

398 
sets_bind[where N="count_space UNIV"] emeasure_bind[where N="count_space UNIV"] 

399 
intro!: nn_integral_cong_AE measure_eqI) 

400 

401 
lemma bind_pmf_cong_simp: 

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

403 
by (simp add: simp_implies_def cong: bind_pmf_cong) 

404 

405 
lemma measure_pmf_bind: "measure_pmf (bind_pmf M f) = (measure_pmf M \<guillemotright>= (\<lambda>x. measure_pmf (f x)))" 

406 
by transfer simp 

407 

408 
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)" 

409 
using measurable_measure_pmf[of N] 

410 
unfolding measure_pmf_bind 

411 
apply (subst (1 3) nn_integral_max_0[symmetric]) 

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

413 
apply auto 

414 
done 

415 

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

417 
using measurable_measure_pmf[of N] 

418 
unfolding measure_pmf_bind 

419 
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

420 

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

423 

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

425 
by transfer 

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

427 
simp: space_subprob_algebra) 

428 

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

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

433 
proof (transfer, clarify) 

434 
fix N :: "'a measure" assume "sets N = UNIV" then show "N \<guillemotright>= return (count_space UNIV) = N" 

435 
by (subst return_sets_cong[where N=N]) (simp_all add: bind_return') 

436 
qed 

437 

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

439 
by transfer 

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

441 
simp: measurable_def space_subprob_algebra prob_space_imp_subprob_space) 

442 

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

444 

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

446 
by (simp add: map_pmf_def bind_assoc_pmf) 

447 

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

449 
by (simp add: map_pmf_def bind_assoc_pmf bind_return_pmf) 

450 

451 
lemma map_pmf_transfer[transfer_rule]: 

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

453 
proof  

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

455 
(\<lambda>f M. M \<guillemotright>= (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

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

459 
qed 

460 

461 
lemma map_pmf_rep_eq: 

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

463 
unfolding map_pmf_def bind_pmf.rep_eq comp_def return_pmf.rep_eq 

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

465 

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

466 
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

467 
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

468 

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

471 

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

472 
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

473 
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

474 

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

477 

59664  478 
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" 
479 
unfolding map_pmf_def by (rule bind_pmf_cong) auto 

480 

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

59665  482 
by (auto simp add: comp_def fun_eq_iff map_pmf_def) 
59664  483 

59665  484 
lemma set_map_pmf[simp]: "set_pmf (map_pmf f M) = f`set_pmf M" 
59664  485 
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

486 

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

487 
lemma emeasure_map_pmf[simp]: "emeasure (map_pmf f M) X = emeasure M (f ` X)" 
59664  488 
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

489 

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

490 
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  491 
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

492 

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

497 
then interpret prob_space p . 

498 
presume "sets p = UNIV" 

499 
then show "ereal (measure (distr p (count_space UNIV) f) {x}) = integral\<^sup>N p (indicator (f ` {x}))" 

500 
by(simp add: measure_distr measurable_def emeasure_eq_measure) 

501 
qed simp_all 

502 

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

504 
proof  

505 
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))" 

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

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

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

509 
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})" 

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

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

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

513 
finally show ?thesis . 

514 
qed 

515 

60068  516 
lemma map_return_pmf [simp]: "map_pmf f (return_pmf x) = return_pmf (f x)" 
59664  517 
by transfer (simp add: distr_return) 
518 

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

520 
by transfer (auto simp: prob_space.distr_const) 

521 

60068  522 
lemma pmf_return [simp]: "pmf (return_pmf x) y = indicator {y} x" 
59664  523 
by transfer (simp add: measure_return) 
524 

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

526 
unfolding return_pmf.rep_eq by (intro nn_integral_return) auto 

527 

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

529 
unfolding return_pmf.rep_eq by (intro emeasure_return) auto 

530 

531 
lemma return_pmf_inj[simp]: "return_pmf x = return_pmf y \<longleftrightarrow> x = y" 

532 
by (metis insertI1 set_return_pmf singletonD) 

533 

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

536 
proof 

537 
assume "map_pmf f p = return_pmf x" 

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

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

540 
next 

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

542 
then show "map_pmf f p = return_pmf x" 

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

544 
qed 

545 

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

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

549 
unfolding pair_pmf_def pmf_bind pmf_return 

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

551 
apply (auto simp: indicator_eq_0_iff) 

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

553 
apply (auto simp: indicator_eq_0_iff setsum_nonneg_eq_0_iff pmf_nonneg) 

554 
done 

555 

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

559 
lemma measure_pmf_in_subprob_space[measurable (raw)]: 

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

561 
by (simp add: space_subprob_algebra) intro_locales 

562 

563 
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)" 

564 
proof  

565 
have "(\<integral>\<^sup>+x. f x \<partial>pair_pmf A B) = (\<integral>\<^sup>+x. max 0 (f x) * indicator (A \<times> B) x \<partial>pair_pmf A B)" 

566 
by (subst nn_integral_max_0[symmetric]) 

59665  567 
(auto simp: AE_measure_pmf_iff intro!: nn_integral_cong_AE) 
59664  568 
also have "\<dots> = (\<integral>\<^sup>+a. \<integral>\<^sup>+b. max 0 (f (a, b)) * indicator (A \<times> B) (a, b) \<partial>B \<partial>A)" 
569 
by (simp add: pair_pmf_def) 

570 
also have "\<dots> = (\<integral>\<^sup>+a. \<integral>\<^sup>+b. max 0 (f (a, b)) \<partial>B \<partial>A)" 

571 
by (auto intro!: nn_integral_cong_AE simp: AE_measure_pmf_iff) 

572 
finally show ?thesis 

573 
unfolding nn_integral_max_0 . 

574 
qed 

575 

576 
lemma bind_pair_pmf: 

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

578 
shows "measure_pmf (pair_pmf A B) \<guillemotright>= M = (measure_pmf A \<guillemotright>= (\<lambda>x. measure_pmf B \<guillemotright>= (\<lambda>y. M (x, y))))" 

579 
(is "?L = ?R") 

580 
proof (rule measure_eqI) 

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

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

583 

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

585 
note measure_pmf_in_subprob_space[simp] 

586 

587 
have sets_eq_N: "sets ?L = N" 

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

589 
show "sets ?L = sets ?R" 

590 
using measurable_space[OF M] 

591 
by (simp add: sets_eq_N space_pair_measure space_subprob_algebra) 

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

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

594 
unfolding sets_eq_N . 

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

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

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

60068  598 
nn_integral_measure_pmf_finite emeasure_nonneg one_ereal_def[symmetric]) 
59664  599 
apply (subst emeasure_bind[OF _ _ X]) 
600 
apply measurable 

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

602 
apply measurable 

603 
done 

604 
qed 

605 

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

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

608 

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

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

611 

612 
lemma nn_integral_pmf': 

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

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

615 
(auto simp: bij_betw_def nn_integral_pmf) 

616 

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

618 
using pmf_nonneg[of M p] by simp 

619 

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

621 
using pmf_nonneg[of M p] by simp_all 

622 

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

624 
unfolding set_pmf_iff by simp 

625 

626 
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" 

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

628 
intro!: measure_pmf.finite_measure_eq_AE) 

629 

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

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

633 
apply(simp add: pmf_eq_0_set_pmf[symmetric]) 

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

635 
done 

636 

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

638 
unfolding pmf_eq_0_set_pmf by simp 

639 

59664  640 
subsection \<open> PMFs as function \<close> 
59000  641 

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

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

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

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

645 
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

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

647 

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

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

649 
proof (intro conjI) 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

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

651 
by (simp split: split_indicator) 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

652 
show "AE x in density (count_space UNIV) (ereal \<circ> f). 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

653 
measure (density (count_space UNIV) (ereal \<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

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

655 
show "prob_space (density (count_space UNIV) (ereal \<circ> f))" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

656 
by default (simp add: emeasure_density prob) 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

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

658 

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

659 
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

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

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

662 
by (simp split: split_indicator) 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

663 
fix x show "measure (density (count_space UNIV) (ereal \<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

664 
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

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

666 

60068  667 
lemma set_embed_pmf: "set_pmf embed_pmf = {x. f x \<noteq> 0}" 
668 
by(auto simp add: set_pmf_eq assms pmf_embed_pmf) 

669 

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

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

671 

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

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

674 
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

675 

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

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

679 
assume "prob_space M" then interpret prob_space M . 

680 
show "M = density (count_space UNIV) (\<lambda>x. ereal (measure M {x}))" 

681 
proof (rule measure_eqI) 

682 
fix A :: "'a set" 

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

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

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

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

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

689 
by (intro emeasure_UN_countable[symmetric] countable_Int2 countable_support) 

690 
(auto simp: disjoint_family_on_def) 

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

692 
using ae by (intro emeasure_eq_AE) auto 

693 
finally show " emeasure M A = emeasure (density (count_space UNIV) (\<lambda>x. ereal (measure M {x}))) A" 

694 
using emeasure_space_1 by (simp add: emeasure_density) 

695 
qed simp 

696 
qed 

697 

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

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

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

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

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

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

703 
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

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

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

706 
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

707 

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

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

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

710 
(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

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

712 
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

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

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

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

716 

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

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

718 

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

721 

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

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

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

724 

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

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

726 

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

727 
lemma set_pmf_transfer[transfer_rule]: 
58730  728 
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

729 
shows "rel_fun (pcr_pmf A) (rel_set A) (\<lambda>f. {x. f x \<noteq> 0}) set_pmf" 
58730  730 
using `bi_total A` 
731 
by (auto simp: pcr_pmf_def cr_pmf_def rel_fun_def rel_set_def bi_total_def Bex_def set_pmf_iff) 

732 
metis+ 

733 

59000  734 
end 
735 

736 
context 

737 
begin 

738 

739 
interpretation pmf_as_function . 

740 

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

742 
by transfer auto 

743 

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

745 
by (auto intro: pmf_eqI) 

746 

59664  747 
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))" 
748 
unfolding pmf_eq_iff pmf_bind 

749 
proof 

750 
fix i 

751 
interpret B: prob_space "restrict_space B B" 

752 
by (intro prob_space_restrict_space measure_pmf.emeasure_eq_1_AE) 

753 
(auto simp: AE_measure_pmf_iff) 

754 
interpret A: prob_space "restrict_space A A" 

755 
by (intro prob_space_restrict_space measure_pmf.emeasure_eq_1_AE) 

756 
(auto simp: AE_measure_pmf_iff) 

757 

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

759 
by unfold_locales 

760 

761 
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)" 

762 
by (rule integral_cong) (auto intro!: integral_pmf_restrict) 

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

764 
by (intro integral_pmf_restrict B.borel_measurable_lebesgue_integral measurable_pair_restrict_pmf2 

765 
countable_set_pmf borel_measurable_count_space) 

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

767 
by (rule AB.Fubini_integral[symmetric]) 

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

769 
simp: pmf_nonneg pmf_le_1 measurable_restrict_space1) 

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

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

772 
countable_set_pmf borel_measurable_count_space) 

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

774 
by (rule integral_cong) (auto intro!: integral_pmf_restrict[symmetric]) 

775 
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)" . 

776 
qed 

777 

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

779 
proof (safe intro!: pmf_eqI) 

780 
fix a :: "'a" and b :: "'b" 

781 
have [simp]: "\<And>c d. indicator (apfst f ` {(a, b)}) (c, d) = indicator (f ` {a}) c * (indicator {b} d::ereal)" 

782 
by (auto split: split_indicator) 

783 

784 
have "ereal (pmf (pair_pmf (map_pmf f A) B) (a, b)) = 

785 
ereal (pmf (map_pmf (apfst f) (pair_pmf A B)) (a, b))" 

786 
unfolding pmf_pair ereal_pmf_map 

787 
by (simp add: nn_integral_pair_pmf' max_def emeasure_pmf_single nn_integral_multc pmf_nonneg 

788 
emeasure_map_pmf[symmetric] del: emeasure_map_pmf) 

789 
then show "pmf (pair_pmf (map_pmf f A) B) (a, b) = pmf (map_pmf (apfst f) (pair_pmf A B)) (a, b)" 

790 
by simp 

791 
qed 

792 

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

794 
proof (safe intro!: pmf_eqI) 

795 
fix a :: "'a" and b :: "'b" 

796 
have [simp]: "\<And>c d. indicator (apsnd f ` {(a, b)}) (c, d) = indicator {a} c * (indicator (f ` {b}) d::ereal)" 

797 
by (auto split: split_indicator) 

798 

799 
have "ereal (pmf (pair_pmf A (map_pmf f B)) (a, b)) = 

800 
ereal (pmf (map_pmf (apsnd f) (pair_pmf A B)) (a, b))" 

801 
unfolding pmf_pair ereal_pmf_map 

802 
by (simp add: nn_integral_pair_pmf' max_def emeasure_pmf_single nn_integral_cmult nn_integral_multc pmf_nonneg 

803 
emeasure_map_pmf[symmetric] del: emeasure_map_pmf) 

804 
then show "pmf (pair_pmf A (map_pmf f B)) (a, b) = pmf (map_pmf (apsnd f) (pair_pmf A B)) (a, b)" 

805 
by simp 

806 
qed 

807 

808 
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)" 

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

810 

59000  811 
end 
812 

59664  813 
subsection \<open> Conditional Probabilities \<close> 
814 

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

817 

59664  818 
context 
819 
fixes p :: "'a pmf" and s :: "'a set" 

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

821 
begin 

822 

823 
interpretation pmf_as_measure . 

824 

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

826 
proof 

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

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

829 
by (rule AE_I[rotated]) auto 

830 
with not_empty show False 

831 
by (auto simp: AE_measure_pmf_iff) 

832 
qed 

833 

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

835 
using emeasure_measure_pmf_not_zero unfolding measure_pmf.emeasure_eq_measure by simp 

836 

837 
lift_definition cond_pmf :: "'a pmf" is 

838 
"uniform_measure (measure_pmf p) s" 

839 
proof (intro conjI) 

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

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

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

843 
by (simp add: emeasure_measure_pmf_not_zero measure_measure_pmf_not_zero AE_uniform_measure 

844 
AE_measure_pmf_iff set_pmf.rep_eq) 

845 
qed simp 

846 

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

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

849 

59665  850 
lemma set_cond_pmf[simp]: "set_pmf cond_pmf = set_pmf p \<inter> s" 
59664  851 
by (auto simp add: set_pmf_iff pmf_cond measure_measure_pmf_not_zero split: split_if_asm) 
852 

853 
end 

854 

855 
lemma cond_map_pmf: 

856 
assumes "set_pmf p \<inter> f ` s \<noteq> {}" 

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

858 
proof  

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

59665  860 
using assms by auto 
59664  861 
{ fix x 
862 
have "ereal (pmf (map_pmf f (cond_pmf p (f ` s))) x) = 

863 
emeasure p (f ` s \<inter> f ` {x}) / emeasure p (f ` s)" 

864 
unfolding ereal_pmf_map cond_pmf.rep_eq[OF assms] by (simp add: nn_integral_uniform_measure) 

865 
also have "f ` s \<inter> f ` {x} = (if x \<in> s then f ` {x} else {})" 

866 
by auto 

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

868 
ereal (pmf (cond_pmf (map_pmf f p) s) x)" 

869 
using measure_measure_pmf_not_zero[OF *] 

870 
by (simp add: pmf_cond[OF *] ereal_divide' ereal_pmf_map measure_pmf.emeasure_eq_measure[symmetric] 

871 
del: ereal_divide) 

872 
finally have "ereal (pmf (cond_pmf (map_pmf f p) s) x) = ereal (pmf (map_pmf f (cond_pmf p (f ` s))) x)" 

873 
by simp } 

874 
then show ?thesis 

875 
by (intro pmf_eqI) simp 

876 
qed 

877 

878 
lemma bind_cond_pmf_cancel: 

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

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

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

59664  883 
proof (rule pmf_eqI) 
59670  884 
fix i 
885 
have "ereal (pmf (bind_pmf p (\<lambda>x. cond_pmf q {y. R x y})) i) = 

886 
(\<integral>\<^sup>+x. ereal (pmf q i / measure p {x. R x i}) * ereal (indicator {x. R x i} x) \<partial>p)" 

887 
by (auto simp add: ereal_pmf_bind AE_measure_pmf_iff pmf_cond pmf_eq_0_set_pmf intro!: nn_integral_cong_AE) 

888 
also have "\<dots> = (pmf q i * measure p {x. R x i}) / measure p {x. R x i}" 

889 
by (simp add: pmf_nonneg measure_nonneg zero_ereal_def[symmetric] ereal_indicator 

890 
nn_integral_cmult measure_pmf.emeasure_eq_measure) 

891 
also have "\<dots> = pmf q i" 

892 
by (cases "pmf q i = 0") (simp_all add: pmf_eq_0_set_pmf measure_measure_pmf_not_zero) 

893 
finally show "pmf (bind_pmf p (\<lambda>x. cond_pmf q {y. R x y})) i = pmf q i" 

894 
by simp 

59664  895 
qed 
896 

897 
subsection \<open> Relator \<close> 

898 

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

900 
for R p q 

901 
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

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

905 

59681  906 
lemma rel_pmfI: 
907 
assumes R: "rel_set R (set_pmf p) (set_pmf q)" 

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

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

910 
shows "rel_pmf R p q" 

911 
proof 

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

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

914 
using R by (auto simp: rel_set_def) 

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

916 
by auto 

917 
show "map_pmf fst ?pq = p" 

60068  918 
by (simp add: map_bind_pmf bind_return_pmf') 
59681  919 

920 
show "map_pmf snd ?pq = q" 

921 
using R eq 

60068  922 
apply (simp add: bind_cond_pmf_cancel map_bind_pmf bind_return_pmf') 
59681  923 
apply (rule bind_cond_pmf_cancel) 
924 
apply (auto simp: rel_set_def) 

925 
done 

926 
qed 

927 

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

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

930 

931 
lemma rel_pmfD_measure: 

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

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

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

935 
proof  

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

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

938 
by (auto elim: rel_pmf.cases) 

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

940 
by (simp add: eq map_pmf_rep_eq measure_distr) 

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

942 
by (intro measure_pmf.finite_measure_eq_AE) 

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

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

945 
by (simp add: eq map_pmf_rep_eq measure_distr) 

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

947 
qed 

948 

949 
lemma rel_pmf_iff_measure: 

950 
assumes "symp R" "transp R" 

951 
shows "rel_pmf R p q \<longleftrightarrow> 

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

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

954 
by (safe intro!: rel_pmf_imp_rel_set rel_pmfI) 

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

956 

957 
lemma quotient_rel_set_disjoint: 

958 
"equivp R \<Longrightarrow> C \<in> UNIV // {(x, y). R x y} \<Longrightarrow> rel_set R A B \<Longrightarrow> A \<inter> C = {} \<longleftrightarrow> B \<inter> C = {}" 

959 
using in_quotient_imp_closed[of UNIV "{(x, y). R x y}" C] 

960 
by (auto 0 0 simp: equivp_equiv rel_set_def set_eq_iff elim: equivpE) 

961 
(blast dest: equivp_symp)+ 

962 

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

964 
by (metis Image_singleton_iff equiv_class_eq_iff quotientE) 

965 

966 
lemma rel_pmf_iff_equivp: 

967 
assumes "equivp R" 

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

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

970 
proof (subst rel_pmf_iff_measure, safe) 

971 
show "symp R" "transp R" 

972 
using assms by (auto simp: equivp_reflp_symp_transp) 

973 
next 

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

975 
assume eq: "\<forall>x\<in>set_pmf p. \<forall>y\<in>set_pmf q. R x y \<longrightarrow> measure p {x. R x y} = measure q {y. R x y}" 

976 

977 
show "measure p C = measure q C" 

978 
proof cases 

979 
assume "p \<inter> C = {}" 

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

981 
using quotient_rel_set_disjoint[OF assms C R] by simp 

982 
ultimately show ?thesis 

983 
unfolding measure_pmf_zero_iff[symmetric] by simp 

984 
next 

985 
assume "p \<inter> C \<noteq> {}" 

986 
moreover then have "q \<inter> C \<noteq> {}" 

987 
using quotient_rel_set_disjoint[OF assms C R] by simp 

988 
ultimately obtain x y where in_set: "x \<in> set_pmf p" "y \<in> set_pmf q" and in_C: "x \<in> C" "y \<in> C" 

989 
by auto 

990 
then have "R x y" 

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

992 
by (simp add: equivp_equiv) 

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

994 
by auto 

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

996 
using assms `x \<in> C` C quotientD[of UNIV ?R C x] by (simp add: equivp_equiv) 

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

998 
using assms `y \<in> C` C quotientD[of UNIV "?R" C y] sympD[of R] 

999 
by (auto simp add: equivp_equiv elim: equivpE) 

1000 
ultimately show ?thesis 

1001 
by auto 

1002 
qed 

1003 
next 

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

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

1006 
unfolding rel_set_def 

1007 
proof safe 

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

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

1010 
by (auto simp: quotient_def) 

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

1012 
by auto 

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

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

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

1016 
unfolding measure_pmf_zero_iff by auto 

1017 
next 

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

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

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

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

1022 
by auto 

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

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

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

1026 
unfolding measure_pmf_zero_iff by auto 

1027 
qed 

1028 

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

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

1031 
using assms `R x y` by (auto simp: quotient_def dest: equivp_symp equivp_transp) 

1032 
with eq show "measure p {x. R x y} = measure q {y. R x y}" 

1033 
by auto 

1034 
qed 

1035 

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

1038 
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

1039 
show "\<And>f g. map_pmf (f \<circ> g) = map_pmf f \<circ> map_pmf g" by (rule map_pmf_compose) 
59664  1040 
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" 
1041 
by (intro map_pmf_cong refl) 

1042 

1043 
show "\<And>f::'a \<Rightarrow> 'b. set_pmf \<circ> map_pmf f = op ` f \<circ> set_pmf" 

1044 
by (rule pmf_set_map) 

1045 

60595  1046 
show "(card_of (set_pmf p), natLeq) \<in> ordLeq" for p :: "'s pmf" 
1047 
proof  

59664  1048 
have "(card_of (set_pmf p), card_of (UNIV :: nat set)) \<in> ordLeq" 
1049 
by (rule card_of_ordLeqI[where f="to_nat_on (set_pmf p)"]) 

1050 
(auto intro: countable_set_pmf) 

1051 
also have "(card_of (UNIV :: nat set), natLeq) \<in> ordLeq" 

1052 
by (metis Field_natLeq card_of_least natLeq_Well_order) 

60595  1053 
finally show ?thesis . 
1054 
qed 

59664  1055 

1056 
show "\<And>R. rel_pmf R = 

1057 
(BNF_Def.Grp {x. set_pmf x \<subseteq> {(x, y). R x y}} (map_pmf fst))\<inverse>\<inverse> OO 

1058 
BNF_Def.Grp {x. set_pmf x \<subseteq> {(x, y). R x y}} (map_pmf snd)" 

1059 
by (auto simp add: fun_eq_iff BNF_Def.Grp_def OO_def rel_pmf.simps) 

1060 

60595  1061 
show "rel_pmf R OO rel_pmf S \<le> rel_pmf (R OO S)" 
1062 
for R :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and S :: "'b \<Rightarrow> 'c \<Rightarrow> bool" 

1063 
proof  

1064 
{ fix p q r 

1065 
assume pq: "rel_pmf R p q" 

1066 
and qr:"rel_pmf S q r" 

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

1068 
and p: "p = map_pmf fst pq" and q: "q = map_pmf snd pq" by cases auto 

1069 
from qr obtain qr where qr: "\<And>y z. (y, z) \<in> set_pmf qr \<Longrightarrow> S y z" 

1070 
and q': "q = map_pmf fst qr" and r: "r = map_pmf snd qr" by cases auto 

1071 

1072 
def pr \<equiv> "bind_pmf pq (\<lambda>xy. bind_pmf (cond_pmf qr {yz. fst yz = snd xy}) (\<lambda>yz. return_pmf (fst xy, snd yz)))" 

1073 
have pr_welldefined: "\<And>y. y \<in> q \<Longrightarrow> qr \<inter> {yz. fst yz = y} \<noteq> {}" 

1074 
by (force simp: q') 

1075 

1076 
have "rel_pmf (R OO S) p r" 

1077 
proof (rule rel_pmf.intros) 

1078 
fix x z assume "(x, z) \<in> pr" 

1079 
then have "\<exists>y. (x, y) \<in> pq \<and> (y, z) \<in> qr" 

1080 
by (auto simp: q pr_welldefined pr_def split_beta) 

1081 
with pq qr show "(R OO S) x z" 

1082 
by blast 

1083 
next 

1084 
have "map_pmf snd pr = map_pmf snd (bind_pmf q (\<lambda>y. cond_pmf qr {yz. fst yz = y}))" 

1085 
by (simp add: pr_def q split_beta bind_map_pmf map_pmf_def[symmetric] map_bind_pmf map_pmf_comp) 

1086 
then show "map_pmf snd pr = r" 

1087 
unfolding r q' bind_map_pmf by (subst (asm) bind_cond_pmf_cancel) (auto simp: eq_commute) 

1088 
qed (simp add: pr_def map_bind_pmf split_beta map_pmf_def[symmetric] p map_pmf_comp) 

1089 
} 

1090 
then show ?thesis 

1091 
by(auto simp add: le_fun_def) 

1092 
qed 

59664  1093 
qed (fact natLeq_card_order natLeq_cinfinite)+ 
1094 

59665  1095 
lemma rel_pmf_conj[simp]: 
1096 
"rel_pmf (\<lambda>x y. P \<and> Q x y) x y \<longleftrightarrow> P \<and> rel_pmf Q x y" 

1097 
"rel_pmf (\<lambda>x y. Q x y \<and> P) x y \<longleftrightarrow> P \<and> rel_pmf Q x y" 

1098 
using set_pmf_not_empty by (fastforce simp: pmf.in_rel subset_eq)+ 

1099 

1100 
lemma rel_pmf_top[simp]: "rel_pmf top = top" 

1101 
by (auto simp: pmf.in_rel[abs_def] fun_eq_iff map_fst_pair_pmf map_snd_pair_pmf 

1102 
intro: exI[of _ "pair_pmf x y" for x y]) 

1103 

59664  1104 
lemma rel_pmf_return_pmf1: "rel_pmf R (return_pmf x) M \<longleftrightarrow> (\<forall>a\<in>M. R x a)" 
1105 
proof safe 

1106 
fix a assume "a \<in> M" "rel_pmf R (return_pmf x) M" 

1107 
then obtain pq where *: "\<And>a b. (a, b) \<in> set_pmf pq \<Longrightarrow> R a b" 

1108 
and eq: "return_pmf x = map_pmf fst pq" "M = map_pmf snd pq" 

1109 
by (force elim: rel_pmf.cases) 

1110 
moreover have "set_pmf (return_pmf x) = {x}" 

59665  1111 
by simp 
59664  1112 
with `a \<in> M` have "(x, a) \<in> pq" 
59665  1113 
by (force simp: eq) 
59664  1114 
with * show "R x a" 
1115 
by auto 

1116 
qed (auto intro!: rel_pmf.intros[where pq="pair_pmf (return_pmf x) M"] 

59665  1117 
simp: map_fst_pair_pmf map_snd_pair_pmf) 
59664  1118 

1119 
lemma rel_pmf_return_pmf2: "rel_pmf R M (return_pmf x) \<longleftrightarrow> (\<forall>a\<in>M. R a x)" 

1120 
by (subst pmf.rel_flip[symmetric]) (simp add: rel_pmf_return_pmf1) 

1121 

1122 
lemma rel_return_pmf[simp]: "rel_pmf R (return_pmf x1) (return_pmf x2) = R x1 x2" 

1123 
unfolding rel_pmf_return_pmf2 set_return_pmf by simp 

1124 

1125 
lemma rel_pmf_False[simp]: "rel_pmf (\<lambda>x y. False) x y = False" 

1126 
unfolding pmf.in_rel fun_eq_iff using set_pmf_not_empty by fastforce 

1127 

1128 
lemma rel_pmf_rel_prod: 

1129 
"rel_pmf (rel_prod R S) (pair_pmf A A') (pair_pmf B B') \<longleftrightarrow> rel_pmf R A B \<and> rel_pmf S A' B'" 

1130 
proof safe 

1131 
assume "rel_pmf (rel_prod R S) (pair_pmf A A') (pair_pmf B B')" 

1132 
then obtain pq where pq: "\<And>a b c d. ((a, c), (b, d)) \<in> set_pmf pq \<Longrightarrow> R a b \<and> S c d" 

1133 
and eq: "map_pmf fst pq = pair_pmf A A'" "map_pmf snd pq = pair_pmf B B'" 

1134 
by (force elim: rel_pmf.cases) 

1135 
show "rel_pmf R A B" 

1136 
proof (rule rel_pmf.intros) 

1137 
let ?f = "\<lambda>(a, b). (fst a, fst b)" 

1138 
have [simp]: "(\<lambda>x. fst (?f x)) = fst o fst" "(\<lambda>x. snd (?f x)) = fst o snd" 

1139 
by auto 

1140 

1141 
show "map_pmf fst (map_pmf ?f pq) = A" 

1142 
by (simp add: map_pmf_comp pmf.map_comp[symmetric] eq map_fst_pair_pmf) 

1143 
show "map_pmf snd (map_pmf ?f pq) = B" 

1144 
by (simp add: map_pmf_comp pmf.map_comp[symmetric] eq map_fst_pair_pmf) 

1145 

1146 
fix a b assume "(a, b) \<in> set_pmf (map_pmf ?f pq)" 

1147 
then obtain c d where "((a, c), (b, d)) \<in> set_pmf pq" 

59665  1148 
by auto 
59664  1149 
from pq[OF this] show "R a b" .. 
1150 
qed 

1151 
show "rel_pmf S A' B'" 

1152 
proof (rule rel_pmf.intros) 

1153 
let ?f = "\<lambda>(a, b). (snd a, snd b)" 

1154 
have [simp]: "(\<lambda>x. fst (?f x)) = snd o fst" "(\<lambda>x. snd (?f x)) = snd o snd" 

1155 
by auto 

1156 

1157 
show "map_pmf fst (map_pmf ?f pq) = A'" 

1158 
by (simp add: map_pmf_comp pmf.map_comp[symmetric] eq map_snd_pair_pmf) 

1159 
show "map_pmf snd (map_pmf ?f pq) = B'" 

1160 
by (simp add: map_pmf_comp pmf.map_comp[symmetric] eq map_snd_pair_pmf) 

1161 

1162 
fix c d assume "(c, d) \<in> set_pmf (map_pmf ?f pq)" 

1163 
then obtain a b where "((a, c), (b, d)) \<in> set_pmf pq" 

59665  1164 
by auto 
59664  1165 
from pq[OF this] show "S c d" .. 
1166 
qed 

1167 
next 

1168 
assume "rel_pmf R A B" "rel_pmf S A' B'" 

1169 
then obtain Rpq Spq 

1170 
where Rpq: "\<And>a b. (a, b) \<in> set_pmf Rpq \<Longrightarrow> R a b" 

1171 
"map_pmf fst Rpq = A" "map_pmf snd Rpq = B" 

1172 
and Spq: "\<And>a b. (a, b) \<in> set_pmf Spq \<Longrightarrow> S a b" 

1173 
"map_pmf fst Spq = A'" "map_pmf snd Spq = B'" 

1174 
by (force elim: rel_pmf.cases) 

1175 

1176 
let ?f = "(\<lambda>((a, c), (b, d)). ((a, b), (c, d)))" 

1177 
let ?pq = "map_pmf ?f (pair_pmf Rpq Spq)" 

1178 
have [simp]: "(\<lambda>x. fst (?f x)) = (\<lambda>(a, b). (fst a, fst b))" "(\<lambda>x. snd (?f x)) = (\<lambda>(a, b). (snd a, snd b))" 

1179 
by auto 

1180 

1181 
show "rel_pmf (rel_prod R S) (pair_pmf A A') (pair_pmf B B')" 

1182 
by (rule rel_pmf.intros[where pq="?pq"]) 

59665  1183 
(auto simp: map_snd_pair_pmf map_fst_pair_pmf map_pmf_comp Rpq Spq 
59664  1184 
map_pair) 
1185 
qed 

1186 

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

1187 
lemma rel_pmf_reflI: 
59664  1188 
assumes "\<And>x. x \<in> set_pmf p \<Longrightarrow> P x x" 
1189 
shows "rel_pmf P p p" 

59665  1190 
by (rule rel_pmf.intros[where pq="map_pmf (\<lambda>x. (x, x)) p"]) 
1191 
(auto simp add: pmf.map_comp o_def assms) 

59664  1192 

1193 
context 

1194 
begin 

1195 

1196 
interpretation pmf_as_measure . 

1197 

1198 
definition "join_pmf M = bind_pmf M (\<lambda>x. x)" 

1199 

1200 
lemma bind_eq_join_pmf: "bind_pmf M f = join_pmf (map_pmf f M)" 

1201 
unfolding join_pmf_def bind_map_pmf .. 

1202 

1203 
lemma join_eq_bind_pmf: "join_pmf M = bind_pmf M id" 

1204 
by (simp add: join_pmf_def id_def) 

224741ede5ae
build pmf's on bind
