author  hoelzl 
Thu, 13 Nov 2014 17:19:52 +0100  
changeset 59000  6eb0725503fc 
parent 58730  b3fd0628f849 
child 59002  2c8b2fb54b88 
permissions  rwrr 
58606  1 
(* Title: HOL/Probability/Probability_Mass_Function.thy 
2 
Author: Johannes Hölzl, TU München *) 

3 

59000  4 
section \<open> Probability mass function \<close> 
5 

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

6 
theory Probability_Mass_Function 
59000  7 
imports 
8 
Giry_Monad 

9 
"~~/src/HOL/Library/Multiset" 

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

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

11 

59000  12 
lemma (in finite_measure) countable_support: (* replace version in pmf *) 
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

13 
"countable {x. measure M {x} \<noteq> 0}" 
59000  14 
proof cases 
15 
assume "measure M (space M) = 0" 

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

17 
by auto 

18 
then show ?thesis 

19 
by simp 

20 
next 

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

22 
assume "?M \<noteq> 0" 

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

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

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

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

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

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

29 
then obtain X where "finite X" "card X = Suc (Suc n)" "X \<subseteq> ?X" 
58606  30 
by (metis infinite_arbitrarily_large) 
59000  31 
from this(3) have *: "\<And>x. x \<in> X \<Longrightarrow> ?M / Suc n \<le> ?m x" 
32 
by auto 

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

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

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

36 
note singleton_sets = this 
59000  37 
have "?M < (\<Sum>x\<in>X. ?M / Suc n)" 
38 
using `?M \<noteq> 0` 

39 
by (simp add: `card X = Suc (Suc n)` real_eq_of_nat[symmetric] real_of_nat_Suc field_simps less_le measure_nonneg) 

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

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

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

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

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

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

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

48 
ultimately show False by simp 

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

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

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

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

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

53 

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

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

57 
proof 

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

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

60 
by auto 

61 
then have "emeasure M (\<Union>x\<in>{x\<in>S. emeasure M {x} \<noteq> 0}. {x}) = 

62 
(\<integral>\<^sup>+ x. emeasure M {x} * indicator {x\<in>S. emeasure M {x} \<noteq> 0} x \<partial>count_space UNIV)" 

63 
by (subst emeasure_UN_countable) 

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

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

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

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

68 
by (subst emeasure_UN_countable) 

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

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

71 
using ae by (intro emeasure_eq_AE) auto 

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

73 
by (simp add: emeasure_single_in_space cong: rev_conj_cong) 

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

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

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

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

78 
by (auto simp: emeasure_eq_measure) 

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

80 

81 
subsection {* PMF as measure *} 

82 

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

83 
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

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

87 

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

88 
declare [[coercion measure_pmf]] 
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 
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

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

92 

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

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

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

95 

59000  96 
interpretation measure_pmf!: subprob_space "measure_pmf M" for M 
97 
by (rule prob_space_imp_subprob_space) unfold_locales 

98 

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

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

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

101 

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

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

103 

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

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

105 

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

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

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

108 

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

109 
interpretation pmf_as_measure . 
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 
lift_definition pmf :: "'a pmf \<Rightarrow> 'a \<Rightarrow> real" is "\<lambda>M x. measure M {x}" . 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

112 

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

113 
lift_definition set_pmf :: "'a pmf \<Rightarrow> 'a set" is "\<lambda>M. {x. measure M {x} \<noteq> 0}" . 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

114 

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

115 
lift_definition map_pmf :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a pmf \<Rightarrow> 'b pmf" is 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

116 
"\<lambda>f M. distr M (count_space UNIV) f" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

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

118 
fix M and f :: "'a \<Rightarrow> 'b" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

119 
let ?D = "distr M (count_space UNIV) f" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

120 
assume "prob_space M" and [simp]: "sets M = UNIV" and ae: "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

121 
interpret prob_space M by fact 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

122 
from ae have "AE x in M. measure M (f ` {f x}) \<noteq> 0" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

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

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

125 
have "measure M {x} \<le> measure M (f ` {f x})" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

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

127 
then show "measure M {x} \<noteq> 0 \<Longrightarrow> measure M (f ` {f x}) \<noteq> 0" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

128 
using measure_nonneg[of M "{x}"] by auto 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

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

130 
then show "AE x in ?D. measure ?D {x} \<noteq> 0" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

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

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

133 

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

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

135 

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

136 
lemma countable_set_pmf: "countable (set_pmf p)" 
59000  137 
by transfer (metis prob_space.finite_measure finite_measure.countable_support) 
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

138 

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

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

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

141 

59000  142 
lemma sets_measure_pmf_count_space: "sets (measure_pmf M) = sets (count_space UNIV)" 
143 
by simp 

144 

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

145 
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

146 
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

147 

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

148 
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

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

150 

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

151 
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

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

153 

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

154 
lemma pmf_positive: "x \<in> set_pmf p \<Longrightarrow> 0 < pmf p x" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

155 
by transfer (simp add: less_le measure_nonneg) 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

156 

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

157 
lemma pmf_nonneg: "0 \<le> pmf p x" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

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

159 

59000  160 
lemma pmf_le_1: "pmf p x \<le> 1" 
161 
by (simp add: pmf.rep_eq) 

162 

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

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

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

165 
shows "emeasure M {x} = pmf M x" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

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

167 

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

168 
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

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

170 

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

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

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

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

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

175 

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

176 
lemma AE_measure_pmf_iff: "(AE x in measure_pmf M. P x) \<longleftrightarrow> (\<forall>y\<in>M. P y)" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

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

178 
{ fix y assume y: "y \<in> M" and P: "AE x in M. P x" "\<not> P y" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

179 
with P have "AE x in M. x \<noteq> y" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

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

181 
with y have False 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

182 
by (simp add: emeasure_pmf_single_eq_zero_iff AE_iff_measurable[OF _ refl]) } 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

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

184 
using AE_measure_pmf[of M] by auto 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

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

186 

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

187 
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

188 
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

189 

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

190 
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

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

192 

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

195 

196 
lemma nn_integral_measure_pmf_support: 

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

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

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

200 
proof  

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

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

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

204 
using assms by (intro nn_integral_indicator_finite) auto 

205 
finally show ?thesis 

206 
by (simp add: emeasure_measure_pmf_finite) 

207 
qed 

208 

209 
lemma nn_integral_measure_pmf_finite: 

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

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

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

213 
using assms by (intro nn_integral_measure_pmf_support) auto 

214 
lemma integrable_measure_pmf_finite: 

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

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

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

218 

219 
lemma integral_measure_pmf: 

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

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

222 
proof  

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

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

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

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

227 
finally show ?thesis . 

228 
qed 

229 

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

231 
proof  

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

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

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

235 
by (simp add: integrable_iff_bounded pmf_nonneg) 

236 
then show ?thesis 

237 
by (simp add: pmf.rep_eq measure_pmf.integrable_measure countable_set_pmf disjoint_family_on_def) 

238 
qed 

239 

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

241 
proof  

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

243 
by (simp add: pmf_nonneg integrable_pmf nn_integral_eq_integral) 

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

245 
by (auto intro!: nn_integral_cong_AE split: split_indicator 

246 
simp: pmf.rep_eq measure_pmf.emeasure_eq_measure nn_integral_count_space_indicator 

247 
AE_count_space set_pmf_iff) 

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

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

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

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

252 
finally show ?thesis 

253 
by (simp add: measure_pmf.emeasure_eq_measure) 

254 
qed 

255 

256 
lemma integral_pmf_restrict: 

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

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

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

260 

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

261 
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

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

263 
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

264 
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

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

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

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

268 

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

269 
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

270 
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

271 

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

272 
lemma map_pmf_compose: "map_pmf (f \<circ> g) = map_pmf f \<circ> map_pmf g" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

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

274 

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

277 

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

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

279 
assumes "p = q" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

280 
shows "(\<And>x. x \<in> set_pmf q \<Longrightarrow> f x = g x) \<Longrightarrow> map_pmf f p = map_pmf g q" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

281 
unfolding `p = q`[symmetric] measure_pmf_inject[symmetric] map_pmf.rep_eq 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

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

283 

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

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

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

286 
shows "set_pmf \<circ> map_pmf f = op ` f \<circ> set_pmf" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

287 
proof (rule, transfer, clarsimp simp add: measure_distr measurable_def) 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

288 
fix f :: "'a \<Rightarrow> 'b" and M :: "'a measure" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

289 
assume "prob_space M" and ae: "AE x in M. measure M {x} \<noteq> 0" and [simp]: "sets M = UNIV" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

290 
interpret prob_space M by fact 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

291 
show "{x. measure M (f ` {x}) \<noteq> 0} = f ` {x. measure M {x} \<noteq> 0}" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

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

293 
fix x assume "measure M (f ` {x}) \<noteq> 0" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

294 
moreover have "measure M (f ` {x}) = measure M {y. f y = x \<and> measure M {y} \<noteq> 0}" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

295 
using ae by (intro finite_measure_eq_AE) auto 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

296 
ultimately have "{y. f y = x \<and> measure M {y} \<noteq> 0} \<noteq> {}" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

297 
by (metis measure_empty) 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

298 
then show "x \<in> f ` {x. measure M {x} \<noteq> 0}" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

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

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

301 
fix x assume "measure M {x} \<noteq> 0" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

302 
then have "0 < measure M {x}" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

303 
using measure_nonneg[of M "{x}"] by auto 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

304 
also have "measure M {x} \<le> measure M (f ` {f x})" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

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

306 
finally show "measure M (f ` {f x}) = 0 \<Longrightarrow> False" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

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

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

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

310 

59000  311 
lemma set_map_pmf: "set_pmf (map_pmf f M) = f`set_pmf M" 
312 
using pmf_set_map[of f] by (auto simp: comp_def fun_eq_iff) 

313 

314 
subsection {* PMFs as function *} 

315 

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

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

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

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

319 
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

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

321 

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

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

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

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

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

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

327 
measure (density (count_space UNIV) (ereal \<circ> f)) {x} \<noteq> 0" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

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

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

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

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

332 

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

333 
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

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

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

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

337 
fix x show "measure (density (count_space UNIV) (ereal \<circ> f)) {x} = f x" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

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

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

340 

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

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

342 

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

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

345 
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

346 

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

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

350 
assume "prob_space M" then interpret prob_space M . 

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

352 
proof (rule measure_eqI) 

353 
fix A :: "'a set" 

354 
have "(\<integral>\<^sup>+ x. ereal (measure M {x}) * indicator A x \<partial>count_space UNIV) = 

355 
(\<integral>\<^sup>+ x. emeasure M {x} * indicator (A \<inter> {x. measure M {x} \<noteq> 0}) x \<partial>count_space UNIV)" 

356 
by (auto intro!: nn_integral_cong simp: emeasure_eq_measure split: split_indicator) 

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

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

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

360 
by (intro emeasure_UN_countable[symmetric] countable_Int2 countable_support) 

361 
(auto simp: disjoint_family_on_def) 

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

363 
using ae by (intro emeasure_eq_AE) auto 

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

365 
using emeasure_space_1 by (simp add: emeasure_density) 

366 
qed simp 

367 
qed 

368 

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

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

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

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

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

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

374 
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

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

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

377 
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

378 

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

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

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

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

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

383 
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

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

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

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

387 

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

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

389 

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

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

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

392 

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

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

394 

58730  395 
lemma set_pmf_transfer[transfer_rule]: 
396 
assumes "bi_total A" 

397 
shows "rel_fun (pcr_pmf A) (rel_set A) (\<lambda>f. {x. f x \<noteq> 0}) set_pmf" 

398 
using `bi_total A` 

399 
by (auto simp: pcr_pmf_def cr_pmf_def rel_fun_def rel_set_def bi_total_def Bex_def set_pmf_iff) 

400 
metis+ 

401 

59000  402 
end 
403 

404 
context 

405 
begin 

406 

407 
interpretation pmf_as_function . 

408 

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

410 
by transfer auto 

411 

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

413 
by (auto intro: pmf_eqI) 

414 

415 
end 

416 

417 
context 

418 
begin 

419 

420 
interpretation pmf_as_function . 

421 

422 
lift_definition bernoulli_pmf :: "real \<Rightarrow> bool pmf" is 

423 
"\<lambda>p b. ((\<lambda>p. if b then p else 1  p) \<circ> min 1 \<circ> max 0) p" 

424 
by (auto simp: nn_integral_count_space_finite[where A="{False, True}"] UNIV_bool 

425 
split: split_max split_min) 

426 

427 
lemma pmf_bernoulli_True[simp]: "0 \<le> p \<Longrightarrow> p \<le> 1 \<Longrightarrow> pmf (bernoulli_pmf p) True = p" 

428 
by transfer simp 

429 

430 
lemma pmf_bernoulli_False[simp]: "0 \<le> p \<Longrightarrow> p \<le> 1 \<Longrightarrow> pmf (bernoulli_pmf p) False = 1  p" 

431 
by transfer simp 

432 

433 
lemma set_pmf_bernoulli: "0 < p \<Longrightarrow> p < 1 \<Longrightarrow> set_pmf (bernoulli_pmf p) = UNIV" 

434 
by (auto simp add: set_pmf_iff UNIV_bool) 

435 

436 
lift_definition geometric_pmf :: "nat pmf" is "\<lambda>n. 1 / 2^Suc n" 

437 
proof 

438 
note geometric_sums[of "1 / 2"] 

439 
note sums_mult[OF this, of "1 / 2"] 

440 
from sums_suminf_ereal[OF this] 

441 
show "(\<integral>\<^sup>+ x. ereal (1 / 2 ^ Suc x) \<partial>count_space UNIV) = 1" 

442 
by (simp add: nn_integral_count_space_nat field_simps) 

443 
qed simp 

444 

445 
lemma pmf_geometric[simp]: "pmf geometric_pmf n = 1 / 2^Suc n" 

446 
by transfer rule 

447 

448 
lemma set_pmf_geometric: "set_pmf geometric_pmf = UNIV" 

449 
by (auto simp: set_pmf_iff) 

450 

451 
context 

452 
fixes M :: "'a multiset" assumes M_not_empty: "M \<noteq> {#}" 

453 
begin 

454 

455 
lift_definition pmf_of_multiset :: "'a pmf" is "\<lambda>x. count M x / size M" 

456 
proof 

457 
show "(\<integral>\<^sup>+ x. ereal (real (count M x) / real (size M)) \<partial>count_space UNIV) = 1" 

458 
using M_not_empty 

459 
by (simp add: zero_less_divide_iff nn_integral_count_space nonempty_has_size 

460 
setsum_divide_distrib[symmetric]) 

461 
(auto simp: size_multiset_overloaded_eq intro!: setsum.cong) 

462 
qed simp 

463 

464 
lemma pmf_of_multiset[simp]: "pmf pmf_of_multiset x = count M x / size M" 

465 
by transfer rule 

466 

467 
lemma set_pmf_of_multiset[simp]: "set_pmf pmf_of_multiset = set_of M" 

468 
by (auto simp: set_pmf_iff) 

469 

470 
end 

471 

472 
context 

473 
fixes S :: "'a set" assumes S_not_empty: "S \<noteq> {}" and S_finite: "finite S" 

474 
begin 

475 

476 
lift_definition pmf_of_set :: "'a pmf" is "\<lambda>x. indicator S x / card S" 

477 
proof 

478 
show "(\<integral>\<^sup>+ x. ereal (indicator S x / real (card S)) \<partial>count_space UNIV) = 1" 

479 
using S_not_empty S_finite by (subst nn_integral_count_space'[of S]) auto 

480 
qed simp 

481 

482 
lemma pmf_of_set[simp]: "pmf pmf_of_set x = indicator S x / card S" 

483 
by transfer rule 

484 

485 
lemma set_pmf_of_set[simp]: "set_pmf pmf_of_set = S" 

486 
using S_finite S_not_empty by (auto simp: set_pmf_iff) 

487 

488 
end 

489 

490 
end 

491 

492 
subsection {* Monad interpretation *} 

493 

494 
lemma measurable_measure_pmf[measurable]: 

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

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

497 

498 
lemma bind_pmf_cong: 

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

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

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

502 
proof (rule measure_eqI) 

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

504 
using assms by (subst (1 2) sets_bind) auto 

505 
next 

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

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

508 
using assms by (subst (asm) sets_bind) auto 

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

510 
using assms 

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

512 
(auto intro!: nn_integral_cong_AE simp: AE_measure_pmf_iff) 

513 
qed 

514 

515 
context 

516 
begin 

517 

518 
interpretation pmf_as_measure . 

519 

520 
lift_definition join_pmf :: "'a pmf pmf \<Rightarrow> 'a pmf" is "\<lambda>M. measure_pmf M \<guillemotright>= measure_pmf" 

521 
proof (intro conjI) 

522 
fix M :: "'a pmf pmf" 

523 

524 
have *: "measure_pmf \<in> measurable (measure_pmf M) (subprob_algebra (count_space UNIV))" 

525 
using measurable_measure_pmf[of "\<lambda>x. x"] by simp 

526 

527 
interpret bind: prob_space "measure_pmf M \<guillemotright>= measure_pmf" 

528 
apply (rule measure_pmf.prob_space_bind[OF _ *]) 

529 
apply (auto intro!: AE_I2) 

530 
apply unfold_locales 

531 
done 

532 
show "prob_space (measure_pmf M \<guillemotright>= measure_pmf)" 

533 
by intro_locales 

534 
show "sets (measure_pmf M \<guillemotright>= measure_pmf) = UNIV" 

535 
by (subst sets_bind[OF *]) auto 

536 
have "AE x in measure_pmf M \<guillemotright>= measure_pmf. emeasure (measure_pmf M \<guillemotright>= measure_pmf) {x} \<noteq> 0" 

537 
by (auto simp add: AE_bind[OF _ *] AE_measure_pmf_iff emeasure_bind[OF _ *] 

538 
nn_integral_0_iff_AE measure_pmf.emeasure_eq_measure measure_le_0_iff set_pmf_iff pmf.rep_eq) 

539 
then show "AE x in measure_pmf M \<guillemotright>= measure_pmf. measure (measure_pmf M \<guillemotright>= measure_pmf) {x} \<noteq> 0" 

540 
unfolding bind.emeasure_eq_measure by simp 

541 
qed 

542 

543 
lemma pmf_join: "pmf (join_pmf N) i = (\<integral>M. pmf M i \<partial>measure_pmf N)" 

544 
proof (transfer fixing: N i) 

545 
have N: "subprob_space (measure_pmf N)" 

546 
by (rule prob_space_imp_subprob_space) intro_locales 

547 
show "measure (measure_pmf N \<guillemotright>= measure_pmf) {i} = integral\<^sup>L (measure_pmf N) (\<lambda>M. measure M {i})" 

548 
using measurable_measure_pmf[of "\<lambda>x. x"] 

549 
by (intro subprob_space.measure_bind[where N="count_space UNIV", OF N]) auto 

550 
qed (auto simp: Transfer.Rel_def rel_fun_def cr_pmf_def) 

551 

552 
lift_definition return_pmf :: "'a \<Rightarrow> 'a pmf" is "return (count_space UNIV)" 

553 
by (auto intro!: prob_space_return simp: AE_return measure_return) 

554 

555 
lemma join_return_pmf: "join_pmf (return_pmf M) = M" 

556 
by (simp add: integral_return pmf_eq_iff pmf_join return_pmf.rep_eq) 

557 

558 
lemma map_return_pmf: "map_pmf f (return_pmf x) = return_pmf (f x)" 

559 
by transfer (simp add: distr_return) 

560 

561 
lemma set_pmf_return: "set_pmf (return_pmf x) = {x}" 

562 
by transfer (auto simp add: measure_return split: split_indicator) 

563 

564 
lemma pmf_return: "pmf (return_pmf x) y = indicator {y} x" 

565 
by transfer (simp add: measure_return) 

566 

567 
end 

568 

569 
definition "bind_pmf M f = join_pmf (map_pmf f M)" 

570 

571 
lemma (in pmf_as_measure) bind_transfer[transfer_rule]: 

572 
"rel_fun pmf_as_measure.cr_pmf (rel_fun (rel_fun op = pmf_as_measure.cr_pmf) pmf_as_measure.cr_pmf) op \<guillemotright>= bind_pmf" 

573 
proof (auto simp: pmf_as_measure.cr_pmf_def rel_fun_def bind_pmf_def join_pmf.rep_eq map_pmf.rep_eq) 

574 
fix M f and g :: "'a \<Rightarrow> 'b pmf" assume "\<forall>x. f x = measure_pmf (g x)" 

575 
then have f: "f = (\<lambda>x. measure_pmf (g x))" 

576 
by auto 

577 
show "measure_pmf M \<guillemotright>= f = distr (measure_pmf M) (count_space UNIV) g \<guillemotright>= measure_pmf" 

578 
unfolding f by (subst bind_distr[OF _ measurable_measure_pmf]) auto 

579 
qed 

580 

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

582 
by (auto intro!: integral_distr simp: bind_pmf_def pmf_join map_pmf.rep_eq) 

583 

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

585 
unfolding bind_pmf_def map_return_pmf join_return_pmf .. 

586 

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

588 
unfolding pmf_eq_iff pmf_bind 

589 
proof 

590 
fix i 

591 
interpret B: prob_space "restrict_space B B" 

592 
by (intro prob_space_restrict_space measure_pmf.emeasure_eq_1_AE) 

593 
(auto simp: AE_measure_pmf_iff) 

594 
interpret A: prob_space "restrict_space A A" 

595 
by (intro prob_space_restrict_space measure_pmf.emeasure_eq_1_AE) 

596 
(auto simp: AE_measure_pmf_iff) 

597 

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

599 
by unfold_locales 

600 

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

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

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

604 
apply (intro integral_pmf_restrict B.borel_measurable_lebesgue_integral) 

605 
apply (auto simp: measurable_split_conv) 

606 
apply (subst measurable_cong_sets) 

607 
apply (rule sets_pair_measure_cong sets_restrict_space_cong sets_measure_pmf_count_space refl)+ 

608 
apply (simp add: restrict_count_space) 

609 
apply (rule measurable_compose_countable'[OF _ measurable_snd]) 

610 
apply (rule measurable_compose[OF measurable_fst]) 

611 
apply (auto intro: countable_set_pmf) 

612 
done 

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

614 
apply (rule AB.Fubini_integral[symmetric]) 

615 
apply (auto intro!: AB.integrable_const_bound[where B=1] simp: pmf_nonneg pmf_le_1) 

616 
apply (auto simp: measurable_split_conv) 

617 
apply (subst measurable_cong_sets) 

618 
apply (rule sets_pair_measure_cong sets_restrict_space_cong sets_measure_pmf_count_space refl)+ 

619 
apply (simp add: restrict_count_space) 

620 
apply (rule measurable_compose_countable'[OF _ measurable_snd]) 

621 
apply (rule measurable_compose[OF measurable_fst]) 

622 
apply (auto intro: countable_set_pmf) 

623 
done 

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

625 
apply (intro integral_pmf_restrict[symmetric] A.borel_measurable_lebesgue_integral) 

626 
apply (auto simp: measurable_split_conv) 

627 
apply (subst measurable_cong_sets) 

628 
apply (rule sets_pair_measure_cong sets_restrict_space_cong sets_measure_pmf_count_space refl)+ 

629 
apply (simp add: restrict_count_space) 

630 
apply (rule measurable_compose_countable'[OF _ measurable_snd]) 

631 
apply (rule measurable_compose[OF measurable_fst]) 

632 
apply (auto intro: countable_set_pmf) 

633 
done 

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

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

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

637 
qed 

638 

639 

640 
context 

641 
begin 

642 

643 
interpretation pmf_as_measure . 

644 

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

646 
proof (transfer, clarify) 

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

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

649 
qed 

650 

651 
lemma bind_return_pmf'': "bind_pmf N (\<lambda>x. return_pmf (f x)) = map_pmf f N" 

652 
proof (transfer, clarify) 

653 
fix N :: "'b measure" and f :: "'b \<Rightarrow> 'a" assume "prob_space N" "sets N = UNIV" 

654 
then show "N \<guillemotright>= (\<lambda>x. return (count_space UNIV) (f x)) = distr N (count_space UNIV) f" 

655 
by (subst bind_return_distr[symmetric]) 

656 
(auto simp: prob_space.not_empty measurable_def comp_def) 

657 
qed 

658 

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

660 
by transfer 

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

662 
simp: measurable_def space_subprob_algebra prob_space_imp_subprob_space) 

663 

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

665 
by transfer simp 

666 

667 
end 

668 

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

670 

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

672 
unfolding pair_pmf_def pmf_bind pmf_return 

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

674 
apply (auto simp: indicator_eq_0_iff) 

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

676 
apply (auto simp: indicator_eq_0_iff setsum_nonneg_eq_0_iff pmf_nonneg) 

677 
done 

678 

679 
lemma bind_pair_pmf: 

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

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

682 
(is "?L = ?R") 

683 
proof (rule measure_eqI) 

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

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

686 

687 
have sets_eq_N: "sets ?L = N" 

688 
by (simp add: sets_bind[OF M']) 

689 
show "sets ?L = sets ?R" 

690 
unfolding sets_eq_N 

691 
apply (subst sets_bind[where N=N]) 

692 
apply (rule measurable_bind) 

693 
apply (rule measurable_compose[OF _ measurable_measure_pmf]) 

694 
apply measurable 

695 
apply (auto intro!: sets_pair_measure_cong sets_measure_pmf_count_space) 

696 
done 

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

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

699 
unfolding sets_eq_N . 

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

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

702 
unfolding pair_pmf_def measure_pmf_bind[of A] 

703 
apply (subst nn_integral_bind[OF _ emeasure_nonneg]) 

704 
apply (rule measurable_compose[OF M' measurable_emeasure_subprob_algebra, OF X]) 

705 
apply (subst measurable_cong_sets[OF sets_measure_pmf_count_space refl]) 

706 
apply (subst subprob_algebra_cong[OF sets_measure_pmf_count_space]) 

707 
apply measurable 

708 
unfolding measure_pmf_bind 

709 
apply (subst nn_integral_bind[OF _ emeasure_nonneg]) 

710 
apply (rule measurable_compose[OF M' measurable_emeasure_subprob_algebra, OF X]) 

711 
apply (subst measurable_cong_sets[OF sets_measure_pmf_count_space refl]) 

712 
apply (subst subprob_algebra_cong[OF sets_measure_pmf_count_space]) 

713 
apply measurable 

714 
apply (simp add: nn_integral_measure_pmf_finite set_pmf_return emeasure_nonneg pmf_return one_ereal_def[symmetric]) 

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

716 
apply simp 

717 
apply (rule measurable_bind[where N="count_space UNIV"]) 

718 
apply (rule measurable_compose[OF _ measurable_measure_pmf]) 

719 
apply measurable 

720 
apply (rule sets_pair_measure_cong sets_measure_pmf_count_space refl)+ 

721 
apply (subst measurable_cong_sets[OF sets_pair_measure_cong[OF sets_measure_pmf_count_space refl] refl]) 

722 
apply simp 

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

724 
apply simp 

725 
apply (rule measurable_compose[OF _ M]) 

726 
apply (auto simp: space_pair_measure) 

727 
done 

728 
qed 

729 

730 
lemma set_pmf_bind: "set_pmf (bind_pmf M N) = (\<Union>M\<in>set_pmf M. set_pmf (N M))" 

731 
apply (simp add: set_eq_iff set_pmf_iff pmf_bind) 

732 
apply (subst integral_nonneg_eq_0_iff_AE) 

733 
apply (auto simp: pmf_nonneg pmf_le_1 AE_measure_pmf_iff 

734 
intro!: measure_pmf.integrable_const_bound[where B=1]) 

735 
done 

736 

737 
lemma set_pmf_pair_pmf: "set_pmf (pair_pmf A B) = set_pmf A \<times> set_pmf B" 

738 
unfolding pair_pmf_def set_pmf_bind set_pmf_return by auto 

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

739 

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

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

741 

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

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

743 
"rel_pmf P d1 d2 \<longleftrightarrow> (\<exists>p3. (\<forall>(x, y) \<in> set_pmf p3. P x y) \<and> map_pmf fst p3 = d1 \<and> map_pmf snd p3 = d2)" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

744 

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

745 
bnf pmf: "'a pmf" map: map_pmf sets: set_pmf bd : "natLeq" rel: pmf_rel 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

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

747 
show "map_pmf id = id" by (rule map_pmf_id) 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

748 
show "\<And>f g. map_pmf (f \<circ> g) = map_pmf f \<circ> map_pmf g" by (rule map_pmf_compose) 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

749 
show "\<And>f g::'a \<Rightarrow> 'b. \<And>p. (\<And>x. x \<in> set_pmf p \<Longrightarrow> f x = g x) \<Longrightarrow> map_pmf f p = map_pmf g p" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

750 
by (intro map_pmg_cong refl) 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

751 

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

752 
show "\<And>f::'a \<Rightarrow> 'b. set_pmf \<circ> map_pmf f = op ` f \<circ> set_pmf" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

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

754 

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

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

756 
have "(card_of (set_pmf p), card_of (UNIV :: nat set)) \<in> ordLeq" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

757 
by (rule card_of_ordLeqI[where f="to_nat_on (set_pmf p)"]) 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

758 
(auto intro: countable_set_pmf inj_on_to_nat_on) 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

759 
also have "(card_of (UNIV :: nat set), natLeq) \<in> ordLeq" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

760 
by (metis Field_natLeq card_of_least natLeq_Well_order) 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

761 
finally show "(card_of (set_pmf p), natLeq) \<in> ordLeq" . } 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

762 

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

763 
show "\<And>R. pmf_rel R = 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

764 
(BNF_Util.Grp {x. set_pmf x \<subseteq> {(x, y). R x y}} (map_pmf fst))\<inverse>\<inverse> OO 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

765 
BNF_Util.Grp {x. set_pmf x \<subseteq> {(x, y). R x y}} (map_pmf snd)" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

766 
by (auto simp add: fun_eq_iff pmf_rel_def BNF_Util.Grp_def OO_def) 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

767 

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

768 
{ let ?f = "map_pmf fst" and ?s = "map_pmf snd" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

769 
fix R :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and A assume "\<And>x y. (x, y) \<in> set_pmf A \<Longrightarrow> R x y" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

770 
fix S :: "'b \<Rightarrow> 'c \<Rightarrow> bool" and B assume "\<And>y z. (y, z) \<in> set_pmf B \<Longrightarrow> S y z" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

771 
assume "?f B = ?s A" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

772 
have "\<exists>C. (\<forall>(x, z)\<in>set_pmf C. \<exists>y. R x y \<and> S y z) \<and> ?f C = ?f A \<and> ?s C = ?s B" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

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

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

775 
then show "\<And>R::'a \<Rightarrow> 'b \<Rightarrow> bool. \<And>S::'b \<Rightarrow> 'c \<Rightarrow> bool. pmf_rel R OO pmf_rel S \<le> pmf_rel (R OO S)" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

776 
by (auto simp add: subset_eq pmf_rel_def fun_eq_iff OO_def Ball_def) 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

777 
qed (fact natLeq_card_order natLeq_cinfinite)+ 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

778 

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

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

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

781 
fix x y :: "nat \<Rightarrow> real" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

782 
def IJz \<equiv> "rec_nat ((0, 0), \<lambda>_. 0) (\<lambda>n ((I, J), z). 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

783 
let a = x I  (\<Sum>j<J. z (I, j)) ; b = y J  (\<Sum>i<I. z (i, J)) in 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

784 
((if a \<le> b then I + 1 else I, if b \<le> a then J + 1 else J), z((I, J) := min a b)))" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

785 
def I == "fst \<circ> fst \<circ> IJz" def J == "snd \<circ> fst \<circ> IJz" def z == "snd \<circ> IJz" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

786 
let ?a = "\<lambda>n. x (I n)  (\<Sum>j<J n. z n (I n, j))" and ?b = "\<lambda>n. y (J n)  (\<Sum>i<I n. z n (i, J n))" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

787 
have IJz_0[simp]: "\<And>p. z 0 p = 0" "I 0 = 0" "J 0 = 0" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

788 
by (simp_all add: I_def J_def z_def IJz_def) 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

789 
have z_Suc[simp]: "\<And>n. z (Suc n) = (z n)((I n, J n) := min (?a n) (?b n))" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

790 
by (simp add: z_def I_def J_def IJz_def Let_def split_beta) 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

791 
have I_Suc[simp]: "\<And>n. I (Suc n) = (if ?a n \<le> ?b n then I n + 1 else I n)" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

792 
by (simp add: z_def I_def J_def IJz_def Let_def split_beta) 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

793 
have J_Suc[simp]: "\<And>n. J (Suc n) = (if ?b n \<le> ?a n then J n + 1 else J n)" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

794 
by (simp add: z_def I_def J_def IJz_def Let_def split_beta) 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

795 

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

796 
{ fix N have "\<And>p. z N p \<noteq> 0 \<Longrightarrow> \<exists>n<N. p = (I n, J n)" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

797 
by (induct N) (auto simp add: less_Suc_eq split: split_if_asm) } 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

798 

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

799 
{ fix i n assume "i < I n" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

800 
then have "(\<Sum>j. z n (i, j)) = x i" 
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset

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

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

803 

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

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

805 