author  eberlm <eberlm@in.tum.de> 
Tue, 04 Apr 2017 08:57:21 +0200  
changeset 65395  7504569a73c7 
parent 64634  5bd30359e46e 
child 66089  def95e0bc529 
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)" 
64267  208 
by (subst emeasure_eq_sum_singleton) (auto simp: emeasure_pmf_single pmf_nonneg) 
59000  209 

64267  210 
lemma measure_measure_pmf_finite: "finite S \<Longrightarrow> measure (measure_pmf M) S = sum (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] 
64267  212 
by (simp add: measure_pmf.emeasure_eq_measure measure_nonneg sum_nonneg pmf_nonneg) 
59023  213 

64267  214 
lemma sum_pmf_eq_1: 
63099
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 

64008
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

249 
lemma integral_measure_pmf_real: 
59000  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 

64008
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

575 
apply (subst integral_measure_pmf_real[where A="{b}"]) 
59664  576 
apply (auto simp: indicator_eq_0_iff) 
64008
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

577 
apply (subst integral_measure_pmf_real[where A="{a}"]) 
64267  578 
apply (auto simp: indicator_eq_0_iff sum_nonneg_eq_0_iff pmf_nonneg) 
59664  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" 

64008
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

661 
unfolding pmf_eq_0_set_pmf by simp 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

662 

17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

663 
lemma measurable_set_pmf[measurable]: "Measurable.pred (count_space UNIV) (\<lambda>x. x \<in> set_pmf M)" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

664 
by simp 
60068  665 

65395
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

666 

59664  667 
subsection \<open> PMFs as function \<close> 
59000  668 

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

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

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

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

672 
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

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

674 

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

675 
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

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

677 
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

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

679 
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

680 
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

681 
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

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

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

685 

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

686 
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

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

688 
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

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

690 
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

691 
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

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

693 

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

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

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

698 

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

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

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

701 
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

702 

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

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

706 
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

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

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

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

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

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

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

716 
by (intro emeasure_UN_countable[symmetric] countable_Int2 countable_support) 

717 
(auto simp: disjoint_family_on_def) 

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

719 
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

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

723 
qed 

724 

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

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

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

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

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

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

730 
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

731 
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

732 
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

733 
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

734 

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

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

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

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

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

739 
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

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

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

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

743 

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

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

745 

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

746 
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  747 
by(simp add: measure_pmf_eq_density nn_integral_density pmf_nonneg) 
748 

64008
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

749 
lemma integral_measure_pmf: 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

750 
fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

751 
assumes A: "finite A" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

752 
shows "(\<And>a. a \<in> set_pmf M \<Longrightarrow> f a \<noteq> 0 \<Longrightarrow> a \<in> A) \<Longrightarrow> (LINT xM. f x) = (\<Sum>a\<in>A. pmf M a *\<^sub>R f a)" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

753 
unfolding measure_pmf_eq_density 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

754 
apply (simp add: integral_density) 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

755 
apply (subst lebesgue_integral_count_space_finite_support) 
64267  756 
apply (auto intro!: finite_subset[OF _ \<open>finite A\<close>] sum.mono_neutral_left simp: pmf_eq_0_set_pmf) 
64008
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

757 
done 
65395
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

758 

7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

759 
lemma expectation_return_pmf [simp]: 
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

760 
fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" 
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

761 
shows "measure_pmf.expectation (return_pmf x) f = f x" 
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

762 
by (subst integral_measure_pmf[of "{x}"]) simp_all 
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

763 

7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

764 
lemma pmf_expectation_bind: 
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

765 
fixes p :: "'a pmf" and f :: "'a \<Rightarrow> 'b pmf" 
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

766 
and h :: "'b \<Rightarrow> 'c::{banach, second_countable_topology}" 
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

767 
assumes "finite A" "\<And>x. x \<in> A \<Longrightarrow> finite (set_pmf (f x))" "set_pmf p \<subseteq> A" 
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

768 
shows "measure_pmf.expectation (p \<bind> f) h = 
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

769 
(\<Sum>a\<in>A. pmf p a *\<^sub>R measure_pmf.expectation (f a) h)" 
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

770 
proof  
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

771 
have "measure_pmf.expectation (p \<bind> f) h = (\<Sum>a\<in>(\<Union>x\<in>A. set_pmf (f x)). pmf (p \<bind> f) a *\<^sub>R h a)" 
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

772 
using assms by (intro integral_measure_pmf) auto 
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

773 
also have "\<dots> = (\<Sum>x\<in>(\<Union>x\<in>A. set_pmf (f x)). (\<Sum>a\<in>A. (pmf p a * pmf (f a) x) *\<^sub>R h x))" 
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

774 
proof (intro sum.cong refl, goal_cases) 
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

775 
case (1 x) 
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

776 
thus ?case 
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

777 
by (subst pmf_bind, subst integral_measure_pmf[of A]) 
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

778 
(insert assms, auto simp: scaleR_sum_left) 
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

779 
qed 
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

780 
also have "\<dots> = (\<Sum>j\<in>A. pmf p j *\<^sub>R (\<Sum>i\<in>(\<Union>x\<in>A. set_pmf (f x)). pmf (f j) i *\<^sub>R h i))" 
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

781 
by (subst sum.commute) (simp add: scaleR_sum_right) 
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

782 
also have "\<dots> = (\<Sum>j\<in>A. pmf p j *\<^sub>R measure_pmf.expectation (f j) h)" 
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

783 
proof (intro sum.cong refl, goal_cases) 
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

784 
case (1 x) 
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

785 
thus ?case 
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

786 
by (subst integral_measure_pmf[of "(\<Union>x\<in>A. set_pmf (f x))"]) 
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

787 
(insert assms, auto simp: scaleR_sum_left) 
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

788 
qed 
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

789 
finally show ?thesis . 
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
64634
diff
changeset

790 
qed 
64008
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

791 

17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

792 
lemma continuous_on_LINT_pmf:  \<open>This is dominated convergence!?\<close> 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

793 
fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::{banach, second_countable_topology}" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

794 
assumes f: "\<And>i. i \<in> set_pmf M \<Longrightarrow> continuous_on A (f i)" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

795 
and bnd: "\<And>a i. a \<in> A \<Longrightarrow> i \<in> set_pmf M \<Longrightarrow> norm (f i a) \<le> B" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

796 
shows "continuous_on A (\<lambda>a. LINT iM. f i a)" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

797 
proof cases 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

798 
assume "finite M" with f show ?thesis 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

799 
using integral_measure_pmf[OF \<open>finite M\<close>] 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

800 
by (subst integral_measure_pmf[OF \<open>finite M\<close>]) 
64267  801 
(auto intro!: continuous_on_sum continuous_on_scaleR continuous_on_const) 
64008
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

802 
next 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

803 
assume "infinite M" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

804 
let ?f = "\<lambda>i x. pmf (map_pmf (to_nat_on M) M) i *\<^sub>R f (from_nat_into M i) x" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

805 

17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

806 
show ?thesis 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

807 
proof (rule uniform_limit_theorem) 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

808 
show "\<forall>\<^sub>F n in sequentially. continuous_on A (\<lambda>a. \<Sum>i<n. ?f i a)" 
64267  809 
by (intro always_eventually allI continuous_on_sum continuous_on_scaleR continuous_on_const f 
64008
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

810 
from_nat_into set_pmf_not_empty) 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

811 
show "uniform_limit A (\<lambda>n a. \<Sum>i<n. ?f i a) (\<lambda>a. LINT iM. f i a) sequentially" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

812 
proof (subst uniform_limit_cong[where g="\<lambda>n a. \<Sum>i<n. ?f i a"]) 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

813 
fix a assume "a \<in> A" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

814 
have 1: "(LINT iM. f i a) = (LINT imap_pmf (to_nat_on M) M. f (from_nat_into M i) a)" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

815 
by (auto intro!: integral_cong_AE AE_pmfI) 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

816 
have 2: "\<dots> = (LINT icount_space UNIV. pmf (map_pmf (to_nat_on M) M) i *\<^sub>R f (from_nat_into M i) a)" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

817 
by (simp add: measure_pmf_eq_density integral_density) 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

818 
have "(\<lambda>n. ?f n a) sums (LINT iM. f i a)" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

819 
unfolding 1 2 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

820 
proof (intro sums_integral_count_space_nat) 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

821 
have A: "integrable M (\<lambda>i. f i a)" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

822 
using \<open>a\<in>A\<close> by (auto intro!: measure_pmf.integrable_const_bound AE_pmfI bnd) 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

823 
have "integrable (map_pmf (to_nat_on M) M) (\<lambda>i. f (from_nat_into M i) a)" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

824 
by (auto simp add: map_pmf_rep_eq integrable_distr_eq intro!: AE_pmfI integrable_cong_AE_imp[OF A]) 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

825 
then show "integrable (count_space UNIV) (\<lambda>n. ?f n a)" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

826 
by (simp add: measure_pmf_eq_density integrable_density) 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

827 
qed 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

828 
then show "(LINT iM. f i a) = (\<Sum> n. ?f n a)" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

829 
by (simp add: sums_unique) 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

830 
next 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

831 
show "uniform_limit A (\<lambda>n a. \<Sum>i<n. ?f i a) (\<lambda>a. (\<Sum> n. ?f n a)) sequentially" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

832 
proof (rule weierstrass_m_test) 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

833 
fix n a assume "a\<in>A" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

834 
then show "norm (?f n a) \<le> pmf (map_pmf (to_nat_on M) M) n * B" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

835 
using bnd by (auto intro!: mult_mono simp: from_nat_into set_pmf_not_empty) 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

836 
next 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

837 
have "integrable (map_pmf (to_nat_on M) M) (\<lambda>n. B)" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

838 
by auto 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

839 
then show "summable (\<lambda>n. pmf (map_pmf (to_nat_on (set_pmf M)) M) n * B)" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

840 
by (simp add: measure_pmf_eq_density integrable_density integrable_count_space_nat_iff summable_rabs_cancel) 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

841 
qed 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

842 
qed simp 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

843 
qed simp 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

844 
qed 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

845 

17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

846 
lemma continuous_on_LBINT: 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

847 
fixes f :: "real \<Rightarrow> real" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

848 
assumes f: "\<And>b. a \<le> b \<Longrightarrow> set_integrable lborel {a..b} f" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

849 
shows "continuous_on UNIV (\<lambda>b. LBINT x:{a..b}. f x)" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

850 
proof (subst set_borel_integral_eq_integral) 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

851 
{ fix b :: real assume "a \<le> b" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

852 
from f[OF this] have "continuous_on {a..b} (\<lambda>b. integral {a..b} f)" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

853 
by (intro indefinite_integral_continuous set_borel_integral_eq_integral) } 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

854 
note * = this 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

855 

17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

856 
have "continuous_on (\<Union>b\<in>{a..}. {a <..< b}) (\<lambda>b. integral {a..b} f)" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

857 
proof (intro continuous_on_open_UN) 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

858 
show "b \<in> {a..} \<Longrightarrow> continuous_on {a<..<b} (\<lambda>b. integral {a..b} f)" for b 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

859 
using *[of b] by (rule continuous_on_subset) auto 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

860 
qed simp 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

861 
also have "(\<Union>b\<in>{a..}. {a <..< b}) = {a <..}" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

862 
by (auto simp: lt_ex gt_ex less_imp_le) (simp add: Bex_def less_imp_le gt_ex cong: rev_conj_cong) 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

863 
finally have "continuous_on {a+1 ..} (\<lambda>b. integral {a..b} f)" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

864 
by (rule continuous_on_subset) auto 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

865 
moreover have "continuous_on {a..a+1} (\<lambda>b. integral {a..b} f)" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

866 
by (rule *) simp 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

867 
moreover 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

868 
have "x \<le> a \<Longrightarrow> {a..x} = (if a = x then {a} else {})" for x 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

869 
by auto 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

870 
then have "continuous_on {..a} (\<lambda>b. integral {a..b} f)" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

871 
by (subst continuous_on_cong[OF refl, where g="\<lambda>x. 0"]) (auto intro!: continuous_on_const) 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

872 
ultimately have "continuous_on ({..a} \<union> {a..a+1} \<union> {a+1 ..}) (\<lambda>b. integral {a..b} f)" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

873 
by (intro continuous_on_closed_Un) auto 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

874 
also have "{..a} \<union> {a..a+1} \<union> {a+1 ..} = UNIV" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

875 
by auto 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

876 
finally show "continuous_on UNIV (\<lambda>b. integral {a..b} f)" 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

877 
by auto 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

878 
next 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

879 
show "set_integrable lborel {a..b} f" for b 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

880 
using f by (cases "a \<le> b") auto 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

881 
qed 
17a20ca86d62
HOLProbability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63973
diff
changeset

882 

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

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

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

885 

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

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

887 

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

888 
lemma set_pmf_transfer[transfer_rule]: 
58730  889 
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

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

894 

59000  895 
end 
896 

897 
context 

898 
begin 

899 

900 
interpretation pmf_as_function . 

901 

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

903 
by transfer auto 

904 

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

906 
by (auto intro: pmf_eqI) 

907 

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

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

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

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

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

912 
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

913 
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

914 
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

915 
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

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

917 
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

918 
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

919 
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

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

921 
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

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

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

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

925 
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

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

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

928 

59664  929 
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))" 
930 
unfolding pmf_eq_iff pmf_bind 

931 
proof 

932 
fix i 

933 
interpret B: prob_space "restrict_space B B" 

934 
by (intro prob_space_restrict_space measure_pmf.emeasure_eq_1_AE) 

935 
(auto simp: AE_measure_pmf_iff) 

936 
interpret A: prob_space "restrict_space A A" 

937 
by (intro prob_space_restrict_space measure_pmf.emeasure_eq_1_AE) 

938 
(auto simp: AE_measure_pmf_iff) 

939 

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

941 
by unfold_locales 

942 

943 
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

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

947 
countable_set_pmf borel_measurable_count_space) 

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

949 
by (rule AB.Fubini_integral[symmetric]) 

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

951 
simp: pmf_nonneg pmf_le_1 measurable_restrict_space1) 

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

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

954 
countable_set_pmf borel_measurable_count_space) 

955 
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

956 
by (rule Bochner_Integration.integral_cong) (auto intro!: integral_pmf_restrict[symmetric]) 
59664  957 
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)" . 
958 
qed 

959 

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

961 
proof (safe intro!: pmf_eqI) 

962 
fix a :: "'a" and b :: "'b" 

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

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

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

966 
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

967 
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

968 
unfolding pmf_pair ennreal_pmf_map 
59664  969 
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

970 
emeasure_map_pmf[symmetric] ennreal_mult del: emeasure_map_pmf) 
59664  971 
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

972 
by (simp add: pmf_nonneg) 
59664  973 
qed 
974 

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

976 
proof (safe intro!: pmf_eqI) 

977 
fix a :: "'a" and b :: "'b" 

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

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

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

981 
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

982 
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

983 
unfolding pmf_pair ennreal_pmf_map 
59664  984 
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

985 
emeasure_map_pmf[symmetric] ennreal_mult del: emeasure_map_pmf) 
59664  986 
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

987 
by (simp add: pmf_nonneg) 
59664  988 
qed 
989 

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

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

992 

59000  993 
end 
994 

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

997 

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

999 
by(simp add: pair_pmf_def bind_return_pmf map_pmf_def) 

1000 

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

1002 
by(simp add: pair_pmf_def bind_return_pmf map_pmf_def bind_assoc_pmf) 

1003 

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

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

1006 

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

1008 
proof(intro iffI pmf_eqI) 

1009 
fix i 

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

1011 
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

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

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

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

1017 
qed auto 

1018 

1019 
lemma bind_eq_return_pmf: 

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

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

1022 
proof(intro iffI strip) 

1023 
fix y 

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

1025 
assume "?lhs" 

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

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

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

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

1030 
next 

1031 
assume *: ?rhs 

1032 
show ?lhs 

1033 
proof(rule pmf_eqI) 

1034 
fix i 

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

1035 
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

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

1037 
also have "\<dots> = \<integral>\<^sup>+ y. ennreal (pmf (return_pmf x) i) \<partial>p" 
61634  1038 
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

1039 
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

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

1041 
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

1042 
by (simp add: pmf_nonneg) 
61634  1043 
qed 
1044 
qed 

1045 

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

1047 
proof  

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

1049 
by(simp add: measure_pmf_single) 

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

1051 
by(subst measure_pmf.finite_measure_Union) simp_all 

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

1053 
finally show ?thesis by simp 

1054 
qed 

1055 

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

1057 
by(simp add: pmf_False_conv_True) 

1058 

59664  1059 
subsection \<open> Conditional Probabilities \<close> 
1060 

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

1063 

59664  1064 
context 
1065 
fixes p :: "'a pmf" and s :: "'a set" 

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

1067 
begin 

1068 

1069 
interpretation pmf_as_measure . 

1070 

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

1072 
proof 

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

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

1075 
by (rule AE_I[rotated]) auto 

1076 
with not_empty show False 

1077 
by (auto simp: AE_measure_pmf_iff) 

1078 
qed 

1079 

1080 
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

1081 
using emeasure_measure_pmf_not_zero by (simp add: measure_pmf.emeasure_eq_measure measure_nonneg) 
59664  1082 

1083 
lift_definition cond_pmf :: "'a pmf" is 

1084 
"uniform_measure (measure_pmf p) s" 

1085 
proof (intro conjI) 

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

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

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

1089 
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

1090 
AE_measure_pmf_iff set_pmf.rep_eq less_top[symmetric]) 
59664  1091 
qed simp 
1092 

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

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

1095 

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

1099 
end 

1100 

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

1101 
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

1102 
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

1103 

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

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

1107 
proof  

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

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

1111 
have "ennreal (pmf (map_pmf f (cond_pmf p (f ` s))) x) = 
59664  1112 
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

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

1116 
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

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

1119 
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

1120 
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

1121 
finally have "ennreal (pmf (cond_pmf (map_pmf f p) s) x) = ennreal (pmf (map_pmf f (cond_pmf p (f ` s))) x)" 
59664  1122 
by simp } 
1123 
then show ?thesis 

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

1124 
by (intro pmf_eqI) (simp add: pmf_nonneg) 
59664  1125 
qed 
1126 

1127 
lemma bind_cond_pmf_cancel: 

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

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

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

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

1134 
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

1135 
(\<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

1136 
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

1137 
intro!: nn_integral_cong_AE) 
59670  1138 
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

1139 
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

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

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

1143 
(simp_all add: pmf_eq_0_set_pmf measure_measure_pmf_not_zero pmf_nonneg) 
59670  1144 
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

1145 
by (simp add: pmf_nonneg) 
59664  1146 
qed 
1147 

1148 
subsection \<open> Relator \<close> 

1149 

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

1151 
for R p q 

1152 
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

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

1156 

59681  1157 
lemma rel_pmfI: 
1158 
assumes R: "rel_set R (set_pmf p) (set_pmf q)" 

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

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

1161 
shows "rel_pmf R p q" 

1162 
proof 

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