author | hoelzl |
Tue, 25 Nov 2014 17:29:39 +0100 | |
changeset 59052 | a05c8305781e |
parent 59048 | 7dc8ac6f0895 |
child 59053 | 43e07797269b |
permissions | -rw-r--r-- |
58606 | 1 |
(* Title: HOL/Probability/Probability_Mass_Function.thy |
59023 | 2 |
Author: Johannes Hölzl, TU München |
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 |
|
59052 | 14 |
lemma bind_return'': "sets M = sets N \<Longrightarrow> M \<guillemotright>= return N = M" |
15 |
by (cases "space M = {}") |
|
16 |
(simp_all add: bind_empty space_empty[symmetric] bind_nonempty join_return' |
|
17 |
cong: subprob_algebra_cong) |
|
18 |
||
19 |
||
20 |
lemma (in prob_space) distr_const[simp]: |
|
21 |
"c \<in> space N \<Longrightarrow> distr M N (\<lambda>x. c) = return N c" |
|
22 |
by (rule measure_eqI) (auto simp: emeasure_distr emeasure_space_1) |
|
23 |
||
24 |
lemma (in finite_measure) countable_support: |
|
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
25 |
"countable {x. measure M {x} \<noteq> 0}" |
59000 | 26 |
proof cases |
27 |
assume "measure M (space M) = 0" |
|
28 |
with bounded_measure measure_le_0_iff have "{x. measure M {x} \<noteq> 0} = {}" |
|
29 |
by auto |
|
30 |
then show ?thesis |
|
31 |
by simp |
|
32 |
next |
|
33 |
let ?M = "measure M (space M)" and ?m = "\<lambda>x. measure M {x}" |
|
34 |
assume "?M \<noteq> 0" |
|
35 |
then have *: "{x. ?m x \<noteq> 0} = (\<Union>n. {x. ?M / Suc n < ?m x})" |
|
36 |
using reals_Archimedean[of "?m x / ?M" for x] |
|
37 |
by (auto simp: field_simps not_le[symmetric] measure_nonneg divide_le_0_iff measure_le_0_iff) |
|
38 |
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
|
39 |
proof (rule ccontr) |
59000 | 40 |
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
|
41 |
then obtain X where "finite X" "card X = Suc (Suc n)" "X \<subseteq> ?X" |
58606 | 42 |
by (metis infinite_arbitrarily_large) |
59000 | 43 |
from this(3) have *: "\<And>x. x \<in> X \<Longrightarrow> ?M / Suc n \<le> ?m x" |
44 |
by auto |
|
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
45 |
{ fix x assume "x \<in> X" |
59000 | 46 |
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
|
47 |
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
|
48 |
note singleton_sets = this |
59000 | 49 |
have "?M < (\<Sum>x\<in>X. ?M / Suc n)" |
50 |
using `?M \<noteq> 0` |
|
51 |
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
|
52 |
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
|
53 |
by (rule setsum_mono) fact |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
54 |
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
|
55 |
using singleton_sets `finite X` |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
56 |
by (intro finite_measure_finite_Union[symmetric]) (auto simp: disjoint_family_on_def) |
59000 | 57 |
finally have "?M < measure M (\<Union>x\<in>X. {x})" . |
58 |
moreover have "measure M (\<Union>x\<in>X. {x}) \<le> ?M" |
|
59 |
using singleton_sets[THEN sets.sets_into_space] by (intro finite_measure_mono) auto |
|
60 |
ultimately show False by simp |
|
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
61 |
qed |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
62 |
show ?thesis |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
63 |
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
|
64 |
qed |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
65 |
|
59000 | 66 |
lemma (in finite_measure) AE_support_countable: |
67 |
assumes [simp]: "sets M = UNIV" |
|
68 |
shows "(AE x in M. measure M {x} \<noteq> 0) \<longleftrightarrow> (\<exists>S. countable S \<and> (AE x in M. x \<in> S))" |
|
69 |
proof |
|
70 |
assume "\<exists>S. countable S \<and> (AE x in M. x \<in> S)" |
|
71 |
then obtain S where S[intro]: "countable S" and ae: "AE x in M. x \<in> S" |
|
72 |
by auto |
|
73 |
then have "emeasure M (\<Union>x\<in>{x\<in>S. emeasure M {x} \<noteq> 0}. {x}) = |
|
74 |
(\<integral>\<^sup>+ x. emeasure M {x} * indicator {x\<in>S. emeasure M {x} \<noteq> 0} x \<partial>count_space UNIV)" |
|
75 |
by (subst emeasure_UN_countable) |
|
76 |
(auto simp: disjoint_family_on_def nn_integral_restrict_space[symmetric] restrict_count_space) |
|
77 |
also have "\<dots> = (\<integral>\<^sup>+ x. emeasure M {x} * indicator S x \<partial>count_space UNIV)" |
|
78 |
by (auto intro!: nn_integral_cong split: split_indicator) |
|
79 |
also have "\<dots> = emeasure M (\<Union>x\<in>S. {x})" |
|
80 |
by (subst emeasure_UN_countable) |
|
81 |
(auto simp: disjoint_family_on_def nn_integral_restrict_space[symmetric] restrict_count_space) |
|
82 |
also have "\<dots> = emeasure M (space M)" |
|
83 |
using ae by (intro emeasure_eq_AE) auto |
|
84 |
finally have "emeasure M {x \<in> space M. x\<in>S \<and> emeasure M {x} \<noteq> 0} = emeasure M (space M)" |
|
85 |
by (simp add: emeasure_single_in_space cong: rev_conj_cong) |
|
86 |
with finite_measure_compl[of "{x \<in> space M. x\<in>S \<and> emeasure M {x} \<noteq> 0}"] |
|
87 |
have "AE x in M. x \<in> S \<and> emeasure M {x} \<noteq> 0" |
|
88 |
by (intro AE_I[OF order_refl]) (auto simp: emeasure_eq_measure set_diff_eq cong: conj_cong) |
|
89 |
then show "AE x in M. measure M {x} \<noteq> 0" |
|
90 |
by (auto simp: emeasure_eq_measure) |
|
91 |
qed (auto intro!: exI[of _ "{x. measure M {x} \<noteq> 0}"] countable_support) |
|
92 |
||
93 |
subsection {* PMF as measure *} |
|
94 |
||
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
95 |
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
|
96 |
morphisms measure_pmf Abs_pmf |
58606 | 97 |
by (intro exI[of _ "uniform_measure (count_space UNIV) {undefined}"]) |
98 |
(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
|
99 |
|
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
100 |
declare [[coercion measure_pmf]] |
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 |
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
|
103 |
using pmf.measure_pmf[of p] by auto |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
104 |
|
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
105 |
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
|
106 |
by (rule prob_space_measure_pmf) |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
107 |
|
59000 | 108 |
interpretation measure_pmf!: subprob_space "measure_pmf M" for M |
109 |
by (rule prob_space_imp_subprob_space) unfold_locales |
|
110 |
||
59048 | 111 |
lemma subprob_space_measure_pmf: "subprob_space (measure_pmf x)" |
112 |
by unfold_locales |
|
113 |
||
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
114 |
locale pmf_as_measure |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
115 |
begin |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
116 |
|
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
117 |
setup_lifting type_definition_pmf |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
118 |
|
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
119 |
end |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
120 |
|
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
121 |
context |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
122 |
begin |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
123 |
|
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
124 |
interpretation pmf_as_measure . |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
125 |
|
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
126 |
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
|
127 |
|
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
128 |
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
|
129 |
|
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
130 |
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
|
131 |
"\<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
|
132 |
proof safe |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
133 |
fix M and f :: "'a \<Rightarrow> 'b" |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
134 |
let ?D = "distr M (count_space UNIV) f" |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
135 |
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
|
136 |
interpret prob_space M by fact |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
137 |
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
|
138 |
proof eventually_elim |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
139 |
fix x |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
140 |
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
|
141 |
by (intro finite_measure_mono) auto |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
142 |
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
|
143 |
using measure_nonneg[of M "{x}"] by auto |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
144 |
qed |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
145 |
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
|
146 |
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
|
147 |
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
|
148 |
|
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
149 |
declare [[coercion set_pmf]] |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
150 |
|
59023 | 151 |
lemma countable_set_pmf [simp]: "countable (set_pmf p)" |
59000 | 152 |
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
|
153 |
|
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
154 |
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
|
155 |
by transfer metis |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
156 |
|
59048 | 157 |
lemma sets_measure_pmf_count_space[measurable_cong]: |
158 |
"sets (measure_pmf M) = sets (count_space UNIV)" |
|
59000 | 159 |
by simp |
160 |
||
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
161 |
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
|
162 |
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
|
163 |
|
59048 | 164 |
lemma measure_pmf_in_subprob_algebra[measurable (raw)]: "measure_pmf x \<in> space (subprob_algebra (count_space UNIV))" |
165 |
by (simp add: space_subprob_algebra subprob_space_measure_pmf) |
|
166 |
||
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
167 |
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
|
168 |
by (auto simp: measurable_def) |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
169 |
|
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
170 |
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
|
171 |
by (intro measurable_cong_sets) simp_all |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
172 |
|
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
173 |
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
|
174 |
by transfer (simp add: less_le measure_nonneg) |
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 pmf_nonneg: "0 \<le> pmf p x" |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
177 |
by transfer (simp add: measure_nonneg) |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
178 |
|
59000 | 179 |
lemma pmf_le_1: "pmf p x \<le> 1" |
180 |
by (simp add: pmf.rep_eq) |
|
181 |
||
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
182 |
lemma emeasure_pmf_single: |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
183 |
fixes M :: "'a pmf" |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
184 |
shows "emeasure M {x} = pmf M x" |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
185 |
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
|
186 |
|
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
187 |
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
|
188 |
by transfer 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 emeasure_pmf_single_eq_zero_iff: |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
191 |
fixes M :: "'a pmf" |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
192 |
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
|
193 |
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
|
194 |
|
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
195 |
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
|
196 |
proof - |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
197 |
{ 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
|
198 |
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
|
199 |
by auto |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
200 |
with y have False |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
201 |
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
|
202 |
then show ?thesis |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
203 |
using AE_measure_pmf[of M] by auto |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
204 |
qed |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
205 |
|
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
206 |
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
|
207 |
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
|
208 |
|
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
209 |
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
|
210 |
by transfer simp |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
211 |
|
59000 | 212 |
lemma emeasure_measure_pmf_finite: "finite S \<Longrightarrow> emeasure (measure_pmf M) S = (\<Sum>s\<in>S. pmf M s)" |
213 |
by (subst emeasure_eq_setsum_singleton) (auto simp: emeasure_pmf_single) |
|
214 |
||
59023 | 215 |
lemma measure_measure_pmf_finite: "finite S \<Longrightarrow> measure (measure_pmf M) S = setsum (pmf M) S" |
216 |
using emeasure_measure_pmf_finite[of S M] |
|
217 |
by(simp add: measure_pmf.emeasure_eq_measure) |
|
218 |
||
59000 | 219 |
lemma nn_integral_measure_pmf_support: |
220 |
fixes f :: "'a \<Rightarrow> ereal" |
|
221 |
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" |
|
222 |
shows "(\<integral>\<^sup>+x. f x \<partial>measure_pmf M) = (\<Sum>x\<in>A. f x * pmf M x)" |
|
223 |
proof - |
|
224 |
have "(\<integral>\<^sup>+x. f x \<partial>M) = (\<integral>\<^sup>+x. f x * indicator A x \<partial>M)" |
|
225 |
using nn by (intro nn_integral_cong_AE) (auto simp: AE_measure_pmf_iff split: split_indicator) |
|
226 |
also have "\<dots> = (\<Sum>x\<in>A. f x * emeasure M {x})" |
|
227 |
using assms by (intro nn_integral_indicator_finite) auto |
|
228 |
finally show ?thesis |
|
229 |
by (simp add: emeasure_measure_pmf_finite) |
|
230 |
qed |
|
231 |
||
232 |
lemma nn_integral_measure_pmf_finite: |
|
233 |
fixes f :: "'a \<Rightarrow> ereal" |
|
234 |
assumes f: "finite (set_pmf M)" and nn: "\<And>x. x \<in> set_pmf M \<Longrightarrow> 0 \<le> f x" |
|
235 |
shows "(\<integral>\<^sup>+x. f x \<partial>measure_pmf M) = (\<Sum>x\<in>set_pmf M. f x * pmf M x)" |
|
236 |
using assms by (intro nn_integral_measure_pmf_support) auto |
|
237 |
lemma integrable_measure_pmf_finite: |
|
238 |
fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" |
|
239 |
shows "finite (set_pmf M) \<Longrightarrow> integrable M f" |
|
240 |
by (auto intro!: integrableI_bounded simp: nn_integral_measure_pmf_finite) |
|
241 |
||
242 |
lemma integral_measure_pmf: |
|
243 |
assumes [simp]: "finite A" and "\<And>a. a \<in> set_pmf M \<Longrightarrow> f a \<noteq> 0 \<Longrightarrow> a \<in> A" |
|
244 |
shows "(\<integral>x. f x \<partial>measure_pmf M) = (\<Sum>a\<in>A. f a * pmf M a)" |
|
245 |
proof - |
|
246 |
have "(\<integral>x. f x \<partial>measure_pmf M) = (\<integral>x. f x * indicator A x \<partial>measure_pmf M)" |
|
247 |
using assms(2) by (intro integral_cong_AE) (auto split: split_indicator simp: AE_measure_pmf_iff) |
|
248 |
also have "\<dots> = (\<Sum>a\<in>A. f a * pmf M a)" |
|
249 |
by (subst integral_indicator_finite_real) (auto simp: measure_def emeasure_measure_pmf_finite) |
|
250 |
finally show ?thesis . |
|
251 |
qed |
|
252 |
||
253 |
lemma integrable_pmf: "integrable (count_space X) (pmf M)" |
|
254 |
proof - |
|
255 |
have " (\<integral>\<^sup>+ x. pmf M x \<partial>count_space X) = (\<integral>\<^sup>+ x. pmf M x \<partial>count_space (M \<inter> X))" |
|
256 |
by (auto simp add: nn_integral_count_space_indicator set_pmf_iff intro!: nn_integral_cong split: split_indicator) |
|
257 |
then have "integrable (count_space X) (pmf M) = integrable (count_space (M \<inter> X)) (pmf M)" |
|
258 |
by (simp add: integrable_iff_bounded pmf_nonneg) |
|
259 |
then show ?thesis |
|
59023 | 260 |
by (simp add: pmf.rep_eq measure_pmf.integrable_measure disjoint_family_on_def) |
59000 | 261 |
qed |
262 |
||
263 |
lemma integral_pmf: "(\<integral>x. pmf M x \<partial>count_space X) = measure M X" |
|
264 |
proof - |
|
265 |
have "(\<integral>x. pmf M x \<partial>count_space X) = (\<integral>\<^sup>+x. pmf M x \<partial>count_space X)" |
|
266 |
by (simp add: pmf_nonneg integrable_pmf nn_integral_eq_integral) |
|
267 |
also have "\<dots> = (\<integral>\<^sup>+x. emeasure M {x} \<partial>count_space (X \<inter> M))" |
|
268 |
by (auto intro!: nn_integral_cong_AE split: split_indicator |
|
269 |
simp: pmf.rep_eq measure_pmf.emeasure_eq_measure nn_integral_count_space_indicator |
|
270 |
AE_count_space set_pmf_iff) |
|
271 |
also have "\<dots> = emeasure M (X \<inter> M)" |
|
272 |
by (rule emeasure_countable_singleton[symmetric]) (auto intro: countable_set_pmf) |
|
273 |
also have "\<dots> = emeasure M X" |
|
274 |
by (auto intro!: emeasure_eq_AE simp: AE_measure_pmf_iff) |
|
275 |
finally show ?thesis |
|
276 |
by (simp add: measure_pmf.emeasure_eq_measure) |
|
277 |
qed |
|
278 |
||
279 |
lemma integral_pmf_restrict: |
|
280 |
"(f::'a \<Rightarrow> 'b::{banach, second_countable_topology}) \<in> borel_measurable (count_space UNIV) \<Longrightarrow> |
|
281 |
(\<integral>x. f x \<partial>measure_pmf M) = (\<integral>x. f x \<partial>restrict_space M M)" |
|
282 |
by (auto intro!: integral_cong_AE simp add: integral_restrict_space AE_measure_pmf_iff) |
|
283 |
||
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
284 |
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
|
285 |
proof - |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
286 |
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
|
287 |
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
|
288 |
then show ?thesis |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
289 |
using measure_pmf.emeasure_space_1 by simp |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
290 |
qed |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
291 |
|
59023 | 292 |
lemma in_null_sets_measure_pmfI: |
293 |
"A \<inter> set_pmf p = {} \<Longrightarrow> A \<in> null_sets (measure_pmf p)" |
|
294 |
using emeasure_eq_0_AE[where ?P="\<lambda>x. x \<in> A" and M="measure_pmf p"] |
|
295 |
by(auto simp add: null_sets_def AE_measure_pmf_iff) |
|
296 |
||
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
297 |
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
|
298 |
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
|
299 |
|
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
300 |
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
|
301 |
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
|
302 |
|
59000 | 303 |
lemma map_pmf_comp: "map_pmf f (map_pmf g M) = map_pmf (\<lambda>x. f (g x)) M" |
304 |
using map_pmf_compose[of f g] by (simp add: comp_def) |
|
305 |
||
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
306 |
lemma map_pmf_cong: |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
307 |
assumes "p = q" |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
308 |
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
|
309 |
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
|
310 |
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
|
311 |
|
59002
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
312 |
lemma emeasure_map_pmf[simp]: "emeasure (map_pmf f M) X = emeasure M (f -` X)" |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
313 |
unfolding map_pmf.rep_eq by (subst emeasure_distr) auto |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
314 |
|
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
315 |
lemma nn_integral_map_pmf[simp]: "(\<integral>\<^sup>+x. f x \<partial>map_pmf g M) = (\<integral>\<^sup>+x. f (g x) \<partial>M)" |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
316 |
unfolding map_pmf.rep_eq by (intro nn_integral_distr) auto |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
317 |
|
59023 | 318 |
lemma ereal_pmf_map: "pmf (map_pmf f p) x = (\<integral>\<^sup>+ y. indicator (f -` {x}) y \<partial>measure_pmf p)" |
319 |
proof(transfer fixing: f x) |
|
320 |
fix p :: "'b measure" |
|
321 |
presume "prob_space p" |
|
322 |
then interpret prob_space p . |
|
323 |
presume "sets p = UNIV" |
|
324 |
then show "ereal (measure (distr p (count_space UNIV) f) {x}) = integral\<^sup>N p (indicator (f -` {x}))" |
|
325 |
by(simp add: measure_distr measurable_def emeasure_eq_measure) |
|
326 |
qed simp_all |
|
327 |
||
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
328 |
lemma pmf_set_map: |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
329 |
fixes f :: "'a \<Rightarrow> 'b" |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
330 |
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
|
331 |
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
|
332 |
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
|
333 |
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
|
334 |
interpret prob_space M by fact |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
335 |
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
|
336 |
proof safe |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
337 |
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
|
338 |
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
|
339 |
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
|
340 |
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
|
341 |
by (metis measure_empty) |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
342 |
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
|
343 |
by auto |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
344 |
next |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
345 |
fix x assume "measure M {x} \<noteq> 0" |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
346 |
then have "0 < measure M {x}" |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
347 |
using measure_nonneg[of M "{x}"] by auto |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
348 |
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
|
349 |
by (intro finite_measure_mono) auto |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
350 |
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
|
351 |
by simp |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
352 |
qed |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
353 |
qed |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
354 |
|
59000 | 355 |
lemma set_map_pmf: "set_pmf (map_pmf f M) = f`set_pmf M" |
356 |
using pmf_set_map[of f] by (auto simp: comp_def fun_eq_iff) |
|
357 |
||
59023 | 358 |
lemma nn_integral_pmf: "(\<integral>\<^sup>+ x. pmf p x \<partial>count_space A) = emeasure (measure_pmf p) A" |
359 |
proof - |
|
360 |
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))" |
|
361 |
by(auto simp add: nn_integral_count_space_indicator indicator_def set_pmf_iff intro: nn_integral_cong) |
|
362 |
also have "\<dots> = emeasure (measure_pmf p) (\<Union>x\<in>A \<inter> set_pmf p. {x})" |
|
363 |
by(subst emeasure_UN_countable)(auto simp add: emeasure_pmf_single disjoint_family_on_def) |
|
364 |
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})" |
|
365 |
by(rule emeasure_Un_null_set[symmetric])(auto intro: in_null_sets_measure_pmfI) |
|
366 |
also have "\<dots> = emeasure (measure_pmf p) A" |
|
367 |
by(auto intro: arg_cong2[where f=emeasure]) |
|
368 |
finally show ?thesis . |
|
369 |
qed |
|
370 |
||
59000 | 371 |
subsection {* PMFs as function *} |
372 |
||
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
373 |
context |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
374 |
fixes f :: "'a \<Rightarrow> real" |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
375 |
assumes nonneg: "\<And>x. 0 \<le> f x" |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
376 |
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
|
377 |
begin |
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 |
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
|
380 |
proof (intro conjI) |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
381 |
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
|
382 |
by (simp split: split_indicator) |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
383 |
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
|
384 |
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
|
385 |
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
|
386 |
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
|
387 |
by default (simp add: emeasure_density prob) |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
388 |
qed simp |
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 |
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
|
391 |
proof transfer |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
392 |
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
|
393 |
by (simp split: split_indicator) |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
394 |
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
|
395 |
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
|
396 |
qed |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
397 |
|
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
398 |
end |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
399 |
|
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
400 |
lemma embed_pmf_transfer: |
58730 | 401 |
"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
|
402 |
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
|
403 |
|
59000 | 404 |
lemma measure_pmf_eq_density: "measure_pmf p = density (count_space UNIV) (pmf p)" |
405 |
proof (transfer, elim conjE) |
|
406 |
fix M :: "'a measure" assume [simp]: "sets M = UNIV" and ae: "AE x in M. measure M {x} \<noteq> 0" |
|
407 |
assume "prob_space M" then interpret prob_space M . |
|
408 |
show "M = density (count_space UNIV) (\<lambda>x. ereal (measure M {x}))" |
|
409 |
proof (rule measure_eqI) |
|
410 |
fix A :: "'a set" |
|
411 |
have "(\<integral>\<^sup>+ x. ereal (measure M {x}) * indicator A x \<partial>count_space UNIV) = |
|
412 |
(\<integral>\<^sup>+ x. emeasure M {x} * indicator (A \<inter> {x. measure M {x} \<noteq> 0}) x \<partial>count_space UNIV)" |
|
413 |
by (auto intro!: nn_integral_cong simp: emeasure_eq_measure split: split_indicator) |
|
414 |
also have "\<dots> = (\<integral>\<^sup>+ x. emeasure M {x} \<partial>count_space (A \<inter> {x. measure M {x} \<noteq> 0}))" |
|
415 |
by (subst nn_integral_restrict_space[symmetric]) (auto simp: restrict_count_space) |
|
416 |
also have "\<dots> = emeasure M (\<Union>x\<in>(A \<inter> {x. measure M {x} \<noteq> 0}). {x})" |
|
417 |
by (intro emeasure_UN_countable[symmetric] countable_Int2 countable_support) |
|
418 |
(auto simp: disjoint_family_on_def) |
|
419 |
also have "\<dots> = emeasure M A" |
|
420 |
using ae by (intro emeasure_eq_AE) auto |
|
421 |
finally show " emeasure M A = emeasure (density (count_space UNIV) (\<lambda>x. ereal (measure M {x}))) A" |
|
422 |
using emeasure_space_1 by (simp add: emeasure_density) |
|
423 |
qed simp |
|
424 |
qed |
|
425 |
||
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
426 |
lemma td_pmf_embed_pmf: |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
427 |
"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
|
428 |
unfolding type_definition_def |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
429 |
proof safe |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
430 |
fix p :: "'a pmf" |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
431 |
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
|
432 |
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
|
433 |
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
|
434 |
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
|
435 |
|
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
436 |
show "embed_pmf (pmf p) = p" |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
437 |
by (intro measure_pmf_inject[THEN iffD1]) |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
438 |
(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
|
439 |
next |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
440 |
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
|
441 |
then show "pmf (embed_pmf f) = f" |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
442 |
by (auto intro!: pmf_embed_pmf) |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
443 |
qed (rule pmf_nonneg) |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
444 |
|
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
445 |
end |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
446 |
|
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
447 |
locale pmf_as_function |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
448 |
begin |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
449 |
|
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
450 |
setup_lifting td_pmf_embed_pmf |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
451 |
|
58730 | 452 |
lemma set_pmf_transfer[transfer_rule]: |
453 |
assumes "bi_total A" |
|
454 |
shows "rel_fun (pcr_pmf A) (rel_set A) (\<lambda>f. {x. f x \<noteq> 0}) set_pmf" |
|
455 |
using `bi_total A` |
|
456 |
by (auto simp: pcr_pmf_def cr_pmf_def rel_fun_def rel_set_def bi_total_def Bex_def set_pmf_iff) |
|
457 |
metis+ |
|
458 |
||
59000 | 459 |
end |
460 |
||
461 |
context |
|
462 |
begin |
|
463 |
||
464 |
interpretation pmf_as_function . |
|
465 |
||
466 |
lemma pmf_eqI: "(\<And>i. pmf M i = pmf N i) \<Longrightarrow> M = N" |
|
467 |
by transfer auto |
|
468 |
||
469 |
lemma pmf_eq_iff: "M = N \<longleftrightarrow> (\<forall>i. pmf M i = pmf N i)" |
|
470 |
by (auto intro: pmf_eqI) |
|
471 |
||
472 |
end |
|
473 |
||
474 |
context |
|
475 |
begin |
|
476 |
||
477 |
interpretation pmf_as_function . |
|
478 |
||
479 |
lift_definition bernoulli_pmf :: "real \<Rightarrow> bool pmf" is |
|
480 |
"\<lambda>p b. ((\<lambda>p. if b then p else 1 - p) \<circ> min 1 \<circ> max 0) p" |
|
481 |
by (auto simp: nn_integral_count_space_finite[where A="{False, True}"] UNIV_bool |
|
482 |
split: split_max split_min) |
|
483 |
||
484 |
lemma pmf_bernoulli_True[simp]: "0 \<le> p \<Longrightarrow> p \<le> 1 \<Longrightarrow> pmf (bernoulli_pmf p) True = p" |
|
485 |
by transfer simp |
|
486 |
||
487 |
lemma pmf_bernoulli_False[simp]: "0 \<le> p \<Longrightarrow> p \<le> 1 \<Longrightarrow> pmf (bernoulli_pmf p) False = 1 - p" |
|
488 |
by transfer simp |
|
489 |
||
490 |
lemma set_pmf_bernoulli: "0 < p \<Longrightarrow> p < 1 \<Longrightarrow> set_pmf (bernoulli_pmf p) = UNIV" |
|
491 |
by (auto simp add: set_pmf_iff UNIV_bool) |
|
492 |
||
59002
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
493 |
lemma nn_integral_bernoulli_pmf[simp]: |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
494 |
assumes [simp]: "0 \<le> p" "p \<le> 1" "\<And>x. 0 \<le> f x" |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
495 |
shows "(\<integral>\<^sup>+x. f x \<partial>bernoulli_pmf p) = f True * p + f False * (1 - p)" |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
496 |
by (subst nn_integral_measure_pmf_support[of UNIV]) |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
497 |
(auto simp: UNIV_bool field_simps) |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
498 |
|
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
499 |
lemma integral_bernoulli_pmf[simp]: |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
500 |
assumes [simp]: "0 \<le> p" "p \<le> 1" |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
501 |
shows "(\<integral>x. f x \<partial>bernoulli_pmf p) = f True * p + f False * (1 - p)" |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
502 |
by (subst integral_measure_pmf[of UNIV]) (auto simp: UNIV_bool) |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
503 |
|
59000 | 504 |
lift_definition geometric_pmf :: "nat pmf" is "\<lambda>n. 1 / 2^Suc n" |
505 |
proof |
|
506 |
note geometric_sums[of "1 / 2"] |
|
507 |
note sums_mult[OF this, of "1 / 2"] |
|
508 |
from sums_suminf_ereal[OF this] |
|
509 |
show "(\<integral>\<^sup>+ x. ereal (1 / 2 ^ Suc x) \<partial>count_space UNIV) = 1" |
|
510 |
by (simp add: nn_integral_count_space_nat field_simps) |
|
511 |
qed simp |
|
512 |
||
513 |
lemma pmf_geometric[simp]: "pmf geometric_pmf n = 1 / 2^Suc n" |
|
514 |
by transfer rule |
|
515 |
||
59002
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
516 |
lemma set_pmf_geometric[simp]: "set_pmf geometric_pmf = UNIV" |
59000 | 517 |
by (auto simp: set_pmf_iff) |
518 |
||
519 |
context |
|
520 |
fixes M :: "'a multiset" assumes M_not_empty: "M \<noteq> {#}" |
|
521 |
begin |
|
522 |
||
523 |
lift_definition pmf_of_multiset :: "'a pmf" is "\<lambda>x. count M x / size M" |
|
524 |
proof |
|
525 |
show "(\<integral>\<^sup>+ x. ereal (real (count M x) / real (size M)) \<partial>count_space UNIV) = 1" |
|
526 |
using M_not_empty |
|
527 |
by (simp add: zero_less_divide_iff nn_integral_count_space nonempty_has_size |
|
528 |
setsum_divide_distrib[symmetric]) |
|
529 |
(auto simp: size_multiset_overloaded_eq intro!: setsum.cong) |
|
530 |
qed simp |
|
531 |
||
532 |
lemma pmf_of_multiset[simp]: "pmf pmf_of_multiset x = count M x / size M" |
|
533 |
by transfer rule |
|
534 |
||
535 |
lemma set_pmf_of_multiset[simp]: "set_pmf pmf_of_multiset = set_of M" |
|
536 |
by (auto simp: set_pmf_iff) |
|
537 |
||
538 |
end |
|
539 |
||
540 |
context |
|
541 |
fixes S :: "'a set" assumes S_not_empty: "S \<noteq> {}" and S_finite: "finite S" |
|
542 |
begin |
|
543 |
||
544 |
lift_definition pmf_of_set :: "'a pmf" is "\<lambda>x. indicator S x / card S" |
|
545 |
proof |
|
546 |
show "(\<integral>\<^sup>+ x. ereal (indicator S x / real (card S)) \<partial>count_space UNIV) = 1" |
|
547 |
using S_not_empty S_finite by (subst nn_integral_count_space'[of S]) auto |
|
548 |
qed simp |
|
549 |
||
550 |
lemma pmf_of_set[simp]: "pmf pmf_of_set x = indicator S x / card S" |
|
551 |
by transfer rule |
|
552 |
||
553 |
lemma set_pmf_of_set[simp]: "set_pmf pmf_of_set = S" |
|
554 |
using S_finite S_not_empty by (auto simp: set_pmf_iff) |
|
555 |
||
59002
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
556 |
lemma emeasure_pmf_of_set[simp]: "emeasure pmf_of_set S = 1" |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
557 |
by (rule measure_pmf.emeasure_eq_1_AE) (auto simp: AE_measure_pmf_iff) |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
558 |
|
59000 | 559 |
end |
560 |
||
561 |
end |
|
562 |
||
563 |
subsection {* Monad interpretation *} |
|
564 |
||
565 |
lemma measurable_measure_pmf[measurable]: |
|
566 |
"(\<lambda>x. measure_pmf (M x)) \<in> measurable (count_space UNIV) (subprob_algebra (count_space UNIV))" |
|
567 |
by (auto simp: space_subprob_algebra intro!: prob_space_imp_subprob_space) unfold_locales |
|
568 |
||
569 |
lemma bind_pmf_cong: |
|
570 |
assumes "\<And>x. A x \<in> space (subprob_algebra N)" "\<And>x. B x \<in> space (subprob_algebra N)" |
|
571 |
assumes "\<And>i. i \<in> set_pmf x \<Longrightarrow> A i = B i" |
|
572 |
shows "bind (measure_pmf x) A = bind (measure_pmf x) B" |
|
573 |
proof (rule measure_eqI) |
|
574 |
show "sets (measure_pmf x \<guillemotright>= A) = sets (measure_pmf x \<guillemotright>= B)" |
|
59048 | 575 |
using assms by (subst (1 2) sets_bind) (auto simp: space_subprob_algebra) |
59000 | 576 |
next |
577 |
fix X assume "X \<in> sets (measure_pmf x \<guillemotright>= A)" |
|
578 |
then have X: "X \<in> sets N" |
|
59048 | 579 |
using assms by (subst (asm) sets_bind) (auto simp: space_subprob_algebra) |
59000 | 580 |
show "emeasure (measure_pmf x \<guillemotright>= A) X = emeasure (measure_pmf x \<guillemotright>= B) X" |
581 |
using assms |
|
582 |
by (subst (1 2) emeasure_bind[where N=N, OF _ _ X]) |
|
583 |
(auto intro!: nn_integral_cong_AE simp: AE_measure_pmf_iff) |
|
584 |
qed |
|
585 |
||
586 |
context |
|
587 |
begin |
|
588 |
||
589 |
interpretation pmf_as_measure . |
|
590 |
||
591 |
lift_definition join_pmf :: "'a pmf pmf \<Rightarrow> 'a pmf" is "\<lambda>M. measure_pmf M \<guillemotright>= measure_pmf" |
|
592 |
proof (intro conjI) |
|
593 |
fix M :: "'a pmf pmf" |
|
594 |
||
595 |
interpret bind: prob_space "measure_pmf M \<guillemotright>= measure_pmf" |
|
59048 | 596 |
apply (intro measure_pmf.prob_space_bind[where S="count_space UNIV"] AE_I2) |
597 |
apply (auto intro!: subprob_space_measure_pmf simp: space_subprob_algebra) |
|
59000 | 598 |
apply unfold_locales |
599 |
done |
|
600 |
show "prob_space (measure_pmf M \<guillemotright>= measure_pmf)" |
|
601 |
by intro_locales |
|
602 |
show "sets (measure_pmf M \<guillemotright>= measure_pmf) = UNIV" |
|
59048 | 603 |
by (subst sets_bind) auto |
59000 | 604 |
have "AE x in measure_pmf M \<guillemotright>= measure_pmf. emeasure (measure_pmf M \<guillemotright>= measure_pmf) {x} \<noteq> 0" |
59048 | 605 |
by (auto simp: AE_bind[where B="count_space UNIV"] measure_pmf_in_subprob_algebra |
606 |
emeasure_bind[where N="count_space UNIV"] AE_measure_pmf_iff nn_integral_0_iff_AE |
|
607 |
measure_pmf.emeasure_eq_measure measure_le_0_iff set_pmf_iff pmf.rep_eq) |
|
59000 | 608 |
then show "AE x in measure_pmf M \<guillemotright>= measure_pmf. measure (measure_pmf M \<guillemotright>= measure_pmf) {x} \<noteq> 0" |
609 |
unfolding bind.emeasure_eq_measure by simp |
|
610 |
qed |
|
611 |
||
612 |
lemma pmf_join: "pmf (join_pmf N) i = (\<integral>M. pmf M i \<partial>measure_pmf N)" |
|
613 |
proof (transfer fixing: N i) |
|
614 |
have N: "subprob_space (measure_pmf N)" |
|
615 |
by (rule prob_space_imp_subprob_space) intro_locales |
|
616 |
show "measure (measure_pmf N \<guillemotright>= measure_pmf) {i} = integral\<^sup>L (measure_pmf N) (\<lambda>M. measure M {i})" |
|
617 |
using measurable_measure_pmf[of "\<lambda>x. x"] |
|
618 |
by (intro subprob_space.measure_bind[where N="count_space UNIV", OF N]) auto |
|
619 |
qed (auto simp: Transfer.Rel_def rel_fun_def cr_pmf_def) |
|
620 |
||
59024 | 621 |
lemma set_pmf_join_pmf: "set_pmf (join_pmf f) = (\<Union>p\<in>set_pmf f. set_pmf p)" |
622 |
apply(simp add: set_eq_iff set_pmf_iff pmf_join) |
|
623 |
apply(subst integral_nonneg_eq_0_iff_AE) |
|
624 |
apply(auto simp add: pmf_le_1 pmf_nonneg AE_measure_pmf_iff intro!: measure_pmf.integrable_const_bound[where B=1]) |
|
625 |
done |
|
626 |
||
59000 | 627 |
lift_definition return_pmf :: "'a \<Rightarrow> 'a pmf" is "return (count_space UNIV)" |
628 |
by (auto intro!: prob_space_return simp: AE_return measure_return) |
|
629 |
||
630 |
lemma join_return_pmf: "join_pmf (return_pmf M) = M" |
|
631 |
by (simp add: integral_return pmf_eq_iff pmf_join return_pmf.rep_eq) |
|
632 |
||
633 |
lemma map_return_pmf: "map_pmf f (return_pmf x) = return_pmf (f x)" |
|
634 |
by transfer (simp add: distr_return) |
|
635 |
||
59052 | 636 |
lemma map_pmf_const[simp]: "map_pmf (\<lambda>_. c) M = return_pmf c" |
637 |
by transfer (auto simp: prob_space.distr_const) |
|
638 |
||
59002
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
639 |
lemma set_return_pmf: "set_pmf (return_pmf x) = {x}" |
59000 | 640 |
by transfer (auto simp add: measure_return split: split_indicator) |
641 |
||
642 |
lemma pmf_return: "pmf (return_pmf x) y = indicator {y} x" |
|
643 |
by transfer (simp add: measure_return) |
|
644 |
||
59002
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
645 |
lemma nn_integral_return_pmf[simp]: "0 \<le> f x \<Longrightarrow> (\<integral>\<^sup>+x. f x \<partial>return_pmf x) = f x" |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
646 |
unfolding return_pmf.rep_eq by (intro nn_integral_return) auto |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
647 |
|
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
648 |
lemma emeasure_return_pmf[simp]: "emeasure (return_pmf x) X = indicator X x" |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
649 |
unfolding return_pmf.rep_eq by (intro emeasure_return) auto |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
650 |
|
59000 | 651 |
end |
652 |
||
653 |
definition "bind_pmf M f = join_pmf (map_pmf f M)" |
|
654 |
||
655 |
lemma (in pmf_as_measure) bind_transfer[transfer_rule]: |
|
656 |
"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" |
|
657 |
proof (auto simp: pmf_as_measure.cr_pmf_def rel_fun_def bind_pmf_def join_pmf.rep_eq map_pmf.rep_eq) |
|
658 |
fix M f and g :: "'a \<Rightarrow> 'b pmf" assume "\<forall>x. f x = measure_pmf (g x)" |
|
659 |
then have f: "f = (\<lambda>x. measure_pmf (g x))" |
|
660 |
by auto |
|
661 |
show "measure_pmf M \<guillemotright>= f = distr (measure_pmf M) (count_space UNIV) g \<guillemotright>= measure_pmf" |
|
662 |
unfolding f by (subst bind_distr[OF _ measurable_measure_pmf]) auto |
|
663 |
qed |
|
664 |
||
665 |
lemma pmf_bind: "pmf (bind_pmf N f) i = (\<integral>x. pmf (f x) i \<partial>measure_pmf N)" |
|
666 |
by (auto intro!: integral_distr simp: bind_pmf_def pmf_join map_pmf.rep_eq) |
|
667 |
||
668 |
lemma bind_return_pmf: "bind_pmf (return_pmf x) f = f x" |
|
669 |
unfolding bind_pmf_def map_return_pmf join_return_pmf .. |
|
670 |
||
59052 | 671 |
lemma join_eq_bind_pmf: "join_pmf M = bind_pmf M id" |
672 |
by (simp add: bind_pmf_def) |
|
673 |
||
674 |
lemma bind_pmf_const[simp]: "bind_pmf M (\<lambda>x. c) = c" |
|
675 |
unfolding bind_pmf_def map_pmf_const join_return_pmf .. |
|
676 |
||
59002
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
677 |
lemma set_bind_pmf: "set_pmf (bind_pmf M N) = (\<Union>M\<in>set_pmf M. set_pmf (N M))" |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
678 |
apply (simp add: set_eq_iff set_pmf_iff pmf_bind) |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
679 |
apply (subst integral_nonneg_eq_0_iff_AE) |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
680 |
apply (auto simp: pmf_nonneg pmf_le_1 AE_measure_pmf_iff |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
681 |
intro!: measure_pmf.integrable_const_bound[where B=1]) |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
682 |
done |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
683 |
|
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
684 |
lemma measurable_pair_restrict_pmf2: |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
685 |
assumes "countable A" |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
686 |
assumes "\<And>y. y \<in> A \<Longrightarrow> (\<lambda>x. f (x, y)) \<in> measurable M L" |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
687 |
shows "f \<in> measurable (M \<Otimes>\<^sub>M restrict_space (measure_pmf N) A) L" |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
688 |
apply (subst measurable_cong_sets) |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
689 |
apply (rule sets_pair_measure_cong sets_restrict_space_cong sets_measure_pmf_count_space refl)+ |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
690 |
apply (simp_all add: restrict_count_space) |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
691 |
apply (subst split_eta[symmetric]) |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
692 |
unfolding measurable_split_conv |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
693 |
apply (rule measurable_compose_countable'[OF _ measurable_snd `countable A`]) |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
694 |
apply (rule measurable_compose[OF measurable_fst]) |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
695 |
apply fact |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
696 |
done |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
697 |
|
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
698 |
lemma measurable_pair_restrict_pmf1: |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
699 |
assumes "countable A" |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
700 |
assumes "\<And>x. x \<in> A \<Longrightarrow> (\<lambda>y. f (x, y)) \<in> measurable N L" |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
701 |
shows "f \<in> measurable (restrict_space (measure_pmf M) A \<Otimes>\<^sub>M N) L" |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
702 |
apply (subst measurable_cong_sets) |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
703 |
apply (rule sets_pair_measure_cong sets_restrict_space_cong sets_measure_pmf_count_space refl)+ |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
704 |
apply (simp_all add: restrict_count_space) |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
705 |
apply (subst split_eta[symmetric]) |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
706 |
unfolding measurable_split_conv |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
707 |
apply (rule measurable_compose_countable'[OF _ measurable_fst `countable A`]) |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
708 |
apply (rule measurable_compose[OF measurable_snd]) |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
709 |
apply fact |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
710 |
done |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
711 |
|
59000 | 712 |
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))" |
713 |
unfolding pmf_eq_iff pmf_bind |
|
714 |
proof |
|
715 |
fix i |
|
716 |
interpret B: prob_space "restrict_space B B" |
|
717 |
by (intro prob_space_restrict_space measure_pmf.emeasure_eq_1_AE) |
|
718 |
(auto simp: AE_measure_pmf_iff) |
|
719 |
interpret A: prob_space "restrict_space A A" |
|
720 |
by (intro prob_space_restrict_space measure_pmf.emeasure_eq_1_AE) |
|
721 |
(auto simp: AE_measure_pmf_iff) |
|
722 |
||
723 |
interpret AB: pair_prob_space "restrict_space A A" "restrict_space B B" |
|
724 |
by unfold_locales |
|
725 |
||
726 |
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)" |
|
727 |
by (rule integral_cong) (auto intro!: integral_pmf_restrict) |
|
728 |
also have "\<dots> = (\<integral> x. (\<integral> y. pmf (C x y) i \<partial>restrict_space B B) \<partial>restrict_space A A)" |
|
59002
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
729 |
by (intro integral_pmf_restrict B.borel_measurable_lebesgue_integral measurable_pair_restrict_pmf2 |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
730 |
countable_set_pmf borel_measurable_count_space) |
59000 | 731 |
also have "\<dots> = (\<integral> y. \<integral> x. pmf (C x y) i \<partial>restrict_space A A \<partial>restrict_space B B)" |
59002
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
732 |
by (rule AB.Fubini_integral[symmetric]) |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
733 |
(auto intro!: AB.integrable_const_bound[where B=1] measurable_pair_restrict_pmf2 |
59023 | 734 |
simp: pmf_nonneg pmf_le_1 measurable_restrict_space1) |
59000 | 735 |
also have "\<dots> = (\<integral> y. \<integral> x. pmf (C x y) i \<partial>restrict_space A A \<partial>B)" |
59002
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
736 |
by (intro integral_pmf_restrict[symmetric] A.borel_measurable_lebesgue_integral measurable_pair_restrict_pmf2 |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
737 |
countable_set_pmf borel_measurable_count_space) |
59000 | 738 |
also have "\<dots> = (\<integral> y. \<integral> x. pmf (C x y) i \<partial>A \<partial>B)" |
739 |
by (rule integral_cong) (auto intro!: integral_pmf_restrict[symmetric]) |
|
740 |
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)" . |
|
741 |
qed |
|
742 |
||
743 |
||
744 |
context |
|
745 |
begin |
|
746 |
||
747 |
interpretation pmf_as_measure . |
|
748 |
||
59002
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
749 |
lemma measure_pmf_bind: "measure_pmf (bind_pmf M f) = (measure_pmf M \<guillemotright>= (\<lambda>x. measure_pmf (f x)))" |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
750 |
by transfer simp |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
751 |
|
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
752 |
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)" |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
753 |
using measurable_measure_pmf[of N] |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
754 |
unfolding measure_pmf_bind |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
755 |
apply (subst (1 3) nn_integral_max_0[symmetric]) |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
756 |
apply (intro nn_integral_bind[where B="count_space UNIV"]) |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
757 |
apply auto |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
758 |
done |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
759 |
|
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
760 |
lemma emeasure_bind_pmf[simp]: "emeasure (bind_pmf M N) X = (\<integral>\<^sup>+x. emeasure (N x) X \<partial>M)" |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
761 |
using measurable_measure_pmf[of N] |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
762 |
unfolding measure_pmf_bind |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
763 |
by (subst emeasure_bind[where N="count_space UNIV"]) auto |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
764 |
|
59000 | 765 |
lemma bind_return_pmf': "bind_pmf N return_pmf = N" |
766 |
proof (transfer, clarify) |
|
767 |
fix N :: "'a measure" assume "sets N = UNIV" then show "N \<guillemotright>= return (count_space UNIV) = N" |
|
768 |
by (subst return_sets_cong[where N=N]) (simp_all add: bind_return') |
|
769 |
qed |
|
770 |
||
771 |
lemma bind_return_pmf'': "bind_pmf N (\<lambda>x. return_pmf (f x)) = map_pmf f N" |
|
772 |
proof (transfer, clarify) |
|
773 |
fix N :: "'b measure" and f :: "'b \<Rightarrow> 'a" assume "prob_space N" "sets N = UNIV" |
|
774 |
then show "N \<guillemotright>= (\<lambda>x. return (count_space UNIV) (f x)) = distr N (count_space UNIV) f" |
|
775 |
by (subst bind_return_distr[symmetric]) |
|
776 |
(auto simp: prob_space.not_empty measurable_def comp_def) |
|
777 |
qed |
|
778 |
||
779 |
lemma bind_assoc_pmf: "bind_pmf (bind_pmf A B) C = bind_pmf A (\<lambda>x. bind_pmf (B x) C)" |
|
780 |
by transfer |
|
781 |
(auto intro!: bind_assoc[where N="count_space UNIV" and R="count_space UNIV"] |
|
782 |
simp: measurable_def space_subprob_algebra prob_space_imp_subprob_space) |
|
783 |
||
784 |
end |
|
785 |
||
59052 | 786 |
lemma map_join_pmf: "map_pmf f (join_pmf AA) = join_pmf (map_pmf (map_pmf f) AA)" |
787 |
unfolding bind_pmf_def[symmetric] |
|
788 |
unfolding bind_return_pmf''[symmetric] join_eq_bind_pmf bind_assoc_pmf |
|
789 |
by (simp add: bind_return_pmf'') |
|
790 |
||
59000 | 791 |
definition "pair_pmf A B = bind_pmf A (\<lambda>x. bind_pmf B (\<lambda>y. return_pmf (x, y)))" |
792 |
||
793 |
lemma pmf_pair: "pmf (pair_pmf M N) (a, b) = pmf M a * pmf N b" |
|
794 |
unfolding pair_pmf_def pmf_bind pmf_return |
|
795 |
apply (subst integral_measure_pmf[where A="{b}"]) |
|
796 |
apply (auto simp: indicator_eq_0_iff) |
|
797 |
apply (subst integral_measure_pmf[where A="{a}"]) |
|
798 |
apply (auto simp: indicator_eq_0_iff setsum_nonneg_eq_0_iff pmf_nonneg) |
|
799 |
done |
|
800 |
||
59002
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
801 |
lemma set_pair_pmf: "set_pmf (pair_pmf A B) = set_pmf A \<times> set_pmf B" |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
802 |
unfolding pair_pmf_def set_bind_pmf set_return_pmf by auto |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset
|
803 |
|
59048 | 804 |
lemma measure_pmf_in_subprob_space[measurable (raw)]: |
805 |
"measure_pmf M \<in> space (subprob_algebra (count_space UNIV))" |
|
806 |
by (simp add: space_subprob_algebra) intro_locales |
|
807 |
||
59000 | 808 |
lemma bind_pair_pmf: |
809 |
assumes M[measurable]: "M \<in> measurable (count_space UNIV \<Otimes>\<^sub>M count_space UNIV) (subprob_algebra N)" |
|
810 |
shows "measure_pmf (pair_pmf A B) \<guillemotright>= M = (measure_pmf A \<guillemotright>= (\<lambda>x. measure_pmf B \<guillemotright>= (\<lambda>y. M (x, y))))" |
|
811 |
(is "?L = ?R") |
|
812 |
proof (rule measure_eqI) |
|
813 |
have M'[measurable]: "M \<in> measurable (pair_pmf A B) (subprob_algebra N)" |
|
814 |
using M[THEN measurable_space] by (simp_all add: space_pair_measure) |
|
815 |
||
59048 | 816 |
note measurable_bind[where N="count_space UNIV", measurable] |
817 |
note measure_pmf_in_subprob_space[simp] |
|
818 |
||
59000 | 819 |
have sets_eq_N: "sets ?L = N" |
59048 | 820 |
by (subst sets_bind[OF sets_kernel[OF M']]) auto |
59000 | 821 |
show "sets ?L = sets ?R" |
59048 | 822 |
using measurable_space[OF M] |
823 |
by (simp add: sets_eq_N space_pair_measure space_subprob_algebra) |
|
59000 | 824 |
fix X assume "X \<in> sets ?L" |
825 |
then have X[measurable]: "X \<in> sets N" |
|
826 |
unfolding sets_eq_N . |
|
827 |
then show "emeasure ?L X = emeasure ?R X" |
|
828 |
apply (simp add: emeasure_bind[OF _ M' X]) |
|
59048 | 829 |
apply (simp add: nn_integral_bind[where B="count_space UNIV"] pair_pmf_def measure_pmf_bind[of A] |
830 |
nn_integral_measure_pmf_finite set_return_pmf emeasure_nonneg pmf_return one_ereal_def[symmetric]) |
|
831 |
apply (subst emeasure_bind[OF _ _ X]) |
|
59000 | 832 |
apply measurable |
833 |
apply (subst emeasure_bind[OF _ _ X]) |
|
834 |
apply measurable |
|
835 |
done |
|
836 |
qed |
|
837 |
||
59052 | 838 |
lemma join_map_return_pmf: "join_pmf (map_pmf return_pmf A) = A" |
839 |
unfolding bind_pmf_def[symmetric] bind_return_pmf' .. |
|
840 |
||
841 |
lemma map_fst_pair_pmf: "map_pmf fst (pair_pmf A B) = A" |
|
842 |
by (simp add: pair_pmf_def bind_return_pmf''[symmetric] bind_assoc_pmf bind_return_pmf bind_return_pmf') |
|
843 |
||
844 |
lemma map_snd_pair_pmf: "map_pmf snd (pair_pmf A B) = B" |
|
845 |
by (simp add: pair_pmf_def bind_return_pmf''[symmetric] bind_assoc_pmf bind_return_pmf bind_return_pmf') |
|
846 |
||
59023 | 847 |
inductive rel_pmf :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a pmf \<Rightarrow> 'b pmf \<Rightarrow> bool" |
848 |
for R p q |
|
849 |
where |
|
850 |
"\<lbrakk> \<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y; |
|
851 |
map_pmf fst pq = p; map_pmf snd pq = q \<rbrakk> |
|
852 |
\<Longrightarrow> rel_pmf R p q" |
|
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
853 |
|
59023 | 854 |
bnf pmf: "'a pmf" map: map_pmf sets: set_pmf bd : "natLeq" rel: rel_pmf |
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
855 |
proof - |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
856 |
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
|
857 |
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
|
858 |
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" |
59023 | 859 |
by (intro map_pmf_cong refl) |
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
860 |
|
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
861 |
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
|
862 |
by (rule pmf_set_map) |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
863 |
|
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
864 |
{ fix p :: "'s pmf" |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
865 |
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
|
866 |
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
|
867 |
(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
|
868 |
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
|
869 |
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
|
870 |
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
|
871 |
|
59023 | 872 |
show "\<And>R. rel_pmf R = |
873 |
(BNF_Def.Grp {x. set_pmf x \<subseteq> {(x, y). R x y}} (map_pmf fst))\<inverse>\<inverse> OO |
|
874 |
BNF_Def.Grp {x. set_pmf x \<subseteq> {(x, y). R x y}} (map_pmf snd)" |
|
875 |
by (auto simp add: fun_eq_iff BNF_Def.Grp_def OO_def rel_pmf.simps) |
|
876 |
||
877 |
{ fix p :: "'a pmf" and f :: "'a \<Rightarrow> 'b" and g x |
|
878 |
assume p: "\<And>z. z \<in> set_pmf p \<Longrightarrow> f z = g z" |
|
879 |
and x: "x \<in> set_pmf p" |
|
880 |
thus "f x = g x" by simp } |
|
881 |
||
882 |
fix R :: "'a => 'b \<Rightarrow> bool" and S :: "'b \<Rightarrow> 'c \<Rightarrow> bool" |
|
883 |
{ fix p q r |
|
884 |
assume pq: "rel_pmf R p q" |
|
885 |
and qr:"rel_pmf S q r" |
|
886 |
from pq obtain pq where pq: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y" |
|
887 |
and p: "p = map_pmf fst pq" and q: "q = map_pmf snd pq" by cases auto |
|
888 |
from qr obtain qr where qr: "\<And>y z. (y, z) \<in> set_pmf qr \<Longrightarrow> S y z" |
|
889 |
and q': "q = map_pmf fst qr" and r: "r = map_pmf snd qr" by cases auto |
|
890 |
||
891 |
have support_subset: "set_pmf pq O set_pmf qr \<subseteq> set_pmf p \<times> set_pmf r" |
|
892 |
by(auto simp add: p r set_map_pmf intro: rev_image_eqI) |
|
893 |
||
894 |
let ?A = "\<lambda>y. {x. (x, y) \<in> set_pmf pq}" |
|
895 |
and ?B = "\<lambda>y. {z. (y, z) \<in> set_pmf qr}" |
|
896 |
||
897 |
||
898 |
def ppp \<equiv> "\<lambda>A. \<lambda>f :: 'a \<Rightarrow> real. \<lambda>n. if n \<in> to_nat_on A ` A then f (from_nat_into A n) else 0" |
|
899 |
have [simp]: "\<And>A f n. (\<And>x. x \<in> A \<Longrightarrow> 0 \<le> f x) \<Longrightarrow> 0 \<le> ppp A f n" |
|
900 |
"\<And>A f n x. \<lbrakk> x \<in> A; countable A \<rbrakk> \<Longrightarrow> ppp A f (to_nat_on A x) = f x" |
|
901 |
"\<And>A f n. n \<notin> to_nat_on A ` A \<Longrightarrow> ppp A f n = 0" |
|
902 |
by(auto simp add: ppp_def intro: from_nat_into) |
|
903 |
def rrr \<equiv> "\<lambda>A. \<lambda>f :: 'c \<Rightarrow> real. \<lambda>n. if n \<in> to_nat_on A ` A then f (from_nat_into A n) else 0" |
|
904 |
have [simp]: "\<And>A f n. (\<And>x. x \<in> A \<Longrightarrow> 0 \<le> f x) \<Longrightarrow> 0 \<le> rrr A f n" |
|
905 |
"\<And>A f n x. \<lbrakk> x \<in> A; countable A \<rbrakk> \<Longrightarrow> rrr A f (to_nat_on A x) = f x" |
|
906 |
"\<And>A f n. n \<notin> to_nat_on A ` A \<Longrightarrow> rrr A f n = 0" |
|
907 |
by(auto simp add: rrr_def intro: from_nat_into) |
|
908 |
||
909 |
def pp \<equiv> "\<lambda>y. ppp (?A y) (\<lambda>x. pmf pq (x, y))" |
|
910 |
and rr \<equiv> "\<lambda>y. rrr (?B y) (\<lambda>z. pmf qr (y, z))" |
|
911 |
||
912 |
have pos_p [simp]: "\<And>y n. 0 \<le> pp y n" |
|
913 |
and pos_r [simp]: "\<And>y n. 0 \<le> rr y n" |
|
914 |
by(simp_all add: pmf_nonneg pp_def rr_def) |
|
915 |
{ fix y n |
|
916 |
have "pp y n \<le> 0 \<longleftrightarrow> pp y n = 0" "\<not> 0 < pp y n \<longleftrightarrow> pp y n = 0" |
|
917 |
and "min (pp y n) 0 = 0" "min 0 (pp y n) = 0" |
|
918 |
using pos_p[of y n] by(auto simp del: pos_p) } |
|
919 |
note pp_convs [simp] = this |
|
920 |
{ fix y n |
|
921 |
have "rr y n \<le> 0 \<longleftrightarrow> rr y n = 0" "\<not> 0 < rr y n \<longleftrightarrow> rr y n = 0" |
|
922 |
and "min (rr y n) 0 = 0" "min 0 (rr y n) = 0" |
|
923 |
using pos_r[of y n] by(auto simp del: pos_r) } |
|
924 |
note r_convs [simp] = this |
|
925 |
||
926 |
have "\<And>y. ?A y \<subseteq> set_pmf p" by(auto simp add: p set_map_pmf intro: rev_image_eqI) |
|
927 |
then have [simp]: "\<And>y. countable (?A y)" by(rule countable_subset) simp |
|
928 |
||
929 |
have "\<And>y. ?B y \<subseteq> set_pmf r" by(auto simp add: r set_map_pmf intro: rev_image_eqI) |
|
930 |
then have [simp]: "\<And>y. countable (?B y)" by(rule countable_subset) simp |
|
931 |
||
932 |
let ?P = "\<lambda>y. to_nat_on (?A y)" |
|
933 |
and ?R = "\<lambda>y. to_nat_on (?B y)" |
|
934 |
||
935 |
have eq: "\<And>y. (\<integral>\<^sup>+ x. pp y x \<partial>count_space UNIV) = \<integral>\<^sup>+ z. rr y z \<partial>count_space UNIV" |
|
936 |
proof - |
|
937 |
fix y |
|
938 |
have "(\<integral>\<^sup>+ x. pp y x \<partial>count_space UNIV) = (\<integral>\<^sup>+ x. pp y x \<partial>count_space (?P y ` ?A y))" |
|
939 |
by(auto simp add: pp_def nn_integral_count_space_indicator indicator_def intro!: nn_integral_cong) |
|
940 |
also have "\<dots> = (\<integral>\<^sup>+ x. pp y (?P y x) \<partial>count_space (?A y))" |
|
941 |
by(intro nn_integral_bij_count_space[symmetric] inj_on_imp_bij_betw inj_on_to_nat_on) simp |
|
942 |
also have "\<dots> = (\<integral>\<^sup>+ x. pmf pq (x, y) \<partial>count_space (?A y))" |
|
943 |
by(rule nn_integral_cong)(simp add: pp_def) |
|
944 |
also have "\<dots> = \<integral>\<^sup>+ x. emeasure (measure_pmf pq) {(x, y)} \<partial>count_space (?A y)" |
|
945 |
by(simp add: emeasure_pmf_single) |
|
946 |
also have "\<dots> = emeasure (measure_pmf pq) (\<Union>x\<in>?A y. {(x, y)})" |
|
947 |
by(subst emeasure_UN_countable)(simp_all add: disjoint_family_on_def) |
|
948 |
also have "\<dots> = emeasure (measure_pmf pq) ((\<Union>x\<in>?A y. {(x, y)}) \<union> {(x, y'). x \<notin> ?A y \<and> y' = y})" |
|
949 |
by(rule emeasure_Un_null_set[symmetric])+ |
|
950 |
(auto simp add: q set_map_pmf split_beta intro!: in_null_sets_measure_pmfI intro: rev_image_eqI) |
|
951 |
also have "\<dots> = emeasure (measure_pmf pq) (snd -` {y})" |
|
952 |
by(rule arg_cong2[where f=emeasure])+auto |
|
953 |
also have "\<dots> = pmf q y" by(simp add: q ereal_pmf_map) |
|
954 |
also have "\<dots> = emeasure (measure_pmf qr) (fst -` {y})" |
|
955 |
by(simp add: q' ereal_pmf_map) |
|
956 |
also have "\<dots> = emeasure (measure_pmf qr) ((\<Union>z\<in>?B y. {(y, z)}) \<union> {(y', z). z \<notin> ?B y \<and> y' = y})" |
|
957 |
by(rule arg_cong2[where f=emeasure])+auto |
|
958 |
also have "\<dots> = emeasure (measure_pmf qr) (\<Union>z\<in>?B y. {(y, z)})" |
|
959 |
by(rule emeasure_Un_null_set) |
|
960 |
(auto simp add: q' set_map_pmf split_beta intro!: in_null_sets_measure_pmfI intro: rev_image_eqI) |
|
961 |
also have "\<dots> = \<integral>\<^sup>+ z. emeasure (measure_pmf qr) {(y, z)} \<partial>count_space (?B y)" |
|
962 |
by(subst emeasure_UN_countable)(simp_all add: disjoint_family_on_def) |
|
963 |
also have "\<dots> = (\<integral>\<^sup>+ z. pmf qr (y, z) \<partial>count_space (?B y))" |
|
964 |
by(simp add: emeasure_pmf_single) |
|
965 |
also have "\<dots> = (\<integral>\<^sup>+ z. rr y (?R y z) \<partial>count_space (?B y))" |
|
966 |
by(rule nn_integral_cong)(simp add: rr_def) |
|
967 |
also have "\<dots> = (\<integral>\<^sup>+ z. rr y z \<partial>count_space (?R y ` ?B y))" |
|
968 |
by(intro nn_integral_bij_count_space inj_on_imp_bij_betw inj_on_to_nat_on) simp |
|
969 |
also have "\<dots> = \<integral>\<^sup>+ z. rr y z \<partial>count_space UNIV" |
|
970 |
by(auto simp add: rr_def nn_integral_count_space_indicator indicator_def intro!: nn_integral_cong) |
|
971 |
finally show "?thesis y" . |
|
972 |
qed |
|
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
973 |
|
59023 | 974 |
def assign_aux \<equiv> "\<lambda>y remainder start weight z. |
975 |
if z < start then 0 |
|
976 |
else if z = start then min weight remainder |
|
977 |
else if remainder + setsum (rr y) {Suc start ..<z} < weight then min (weight - remainder - setsum (rr y) {Suc start..<z}) (rr y z) else 0" |
|
978 |
hence assign_aux_alt_def: "\<And>y remainder start weight z. assign_aux y remainder start weight z = |
|
979 |
(if z < start then 0 |
|
980 |
else if z = start then min weight remainder |
|
981 |
else if remainder + setsum (rr y) {Suc start ..<z} < weight then min (weight - remainder - setsum (rr y) {Suc start..<z}) (rr y z) else 0)" |
|
982 |
by simp |
|
983 |
{ fix y and remainder :: real and start and weight :: real |
|
984 |
assume weight_nonneg: "0 \<le> weight" |
|
985 |
let ?assign_aux = "assign_aux y remainder start weight" |
|
986 |
{ fix z |
|
987 |
have "setsum ?assign_aux {..<z} = |
|
988 |
(if z \<le> start then 0 else if remainder + setsum (rr y) {Suc start..<z} < weight then remainder + setsum (rr y) {Suc start..<z} else weight)" |
|
989 |
proof(induction z) |
|
990 |
case (Suc z) show ?case |
|
991 |
by(auto simp add: Suc.IH assign_aux_alt_def[where z=z] not_less)(metis add.commute add.left_commute add_increasing pos_r) |
|
992 |
qed(auto simp add: assign_aux_def) } |
|
993 |
note setsum_start_assign_aux = this |
|
994 |
moreover { |
|
995 |
assume remainder_nonneg: "0 \<le> remainder" |
|
996 |
have [simp]: "\<And>z. 0 \<le> ?assign_aux z" |
|
997 |
by(simp add: assign_aux_def weight_nonneg remainder_nonneg) |
|
998 |
moreover have "\<And>z. \<lbrakk> rr y z = 0; remainder \<le> rr y start \<rbrakk> \<Longrightarrow> ?assign_aux z = 0" |
|
999 |
using remainder_nonneg weight_nonneg |
|
1000 |
by(auto simp add: assign_aux_def min_def) |
|
1001 |
moreover have "(\<integral>\<^sup>+ z. ?assign_aux z \<partial>count_space UNIV) = |
|
1002 |
min weight (\<integral>\<^sup>+ z. (if z < start then 0 else if z = start then remainder else rr y z) \<partial>count_space UNIV)" |
|
1003 |
(is "?lhs = ?rhs" is "_ = min _ (\<integral>\<^sup>+ y. ?f y \<partial>_)") |
|
1004 |
proof - |
|
1005 |
have "?lhs = (SUP n. \<Sum>z<n. ereal (?assign_aux z))" |
|
1006 |
by(simp add: nn_integral_count_space_nat suminf_ereal_eq_SUP) |
|
1007 |
also have "\<dots> = (SUP n. min weight (\<Sum>z<n. ?f z))" |
|
1008 |
proof(rule arg_cong2[where f=SUPREMUM] ext refl)+ |
|
1009 |
fix n |
|
1010 |
have "(\<Sum>z<n. ereal (?assign_aux z)) = min weight ((if n > start then remainder else 0) + setsum ?f {Suc start..<n})" |
|
1011 |
using weight_nonneg remainder_nonneg by(simp add: setsum_start_assign_aux min_def) |
|
1012 |
also have "\<dots> = min weight (setsum ?f {start..<n})" |
|
1013 |
by(simp add: setsum_head_upt_Suc) |
|
1014 |
also have "\<dots> = min weight (setsum ?f {..<n})" |
|
1015 |
by(intro arg_cong2[where f=min] setsum.mono_neutral_left) auto |
|
1016 |
finally show "(\<Sum>z<n. ereal (?assign_aux z)) = \<dots>" . |
|
1017 |
qed |
|
1018 |
also have "\<dots> = min weight (SUP n. setsum ?f {..<n})" |
|
1019 |
unfolding inf_min[symmetric] by(subst inf_SUP) simp |
|
1020 |
also have "\<dots> = ?rhs" |
|
1021 |
by(simp add: nn_integral_count_space_nat suminf_ereal_eq_SUP remainder_nonneg) |
|
1022 |
finally show ?thesis . |
|
1023 |
qed |
|
1024 |
moreover note calculation } |
|
1025 |
moreover note calculation } |
|
1026 |
note setsum_start_assign_aux = this(1) |
|
1027 |
and assign_aux_nonneg [simp] = this(2) |
|
1028 |
and assign_aux_eq_0_outside = this(3) |
|
1029 |
and nn_integral_assign_aux = this(4) |
|
1030 |
{ fix y and remainder :: real and start target |
|
1031 |
have "setsum (rr y) {Suc start..<target} \<ge> 0" by(simp add: setsum_nonneg) |
|
1032 |
moreover assume "0 \<le> remainder" |
|
1033 |
ultimately have "assign_aux y remainder start 0 target = 0" |
|
1034 |
by(auto simp add: assign_aux_def min_def) } |
|
1035 |
note assign_aux_weight_0 [simp] = this |
|
1036 |
||
1037 |
def find_start \<equiv> "\<lambda>y weight. if \<exists>n. weight \<le> setsum (rr y) {..n} then Some (LEAST n. weight \<le> setsum (rr y) {..n}) else None" |
|
1038 |
have find_start_eq_Some_above: |
|
1039 |
"\<And>y weight n. find_start y weight = Some n \<Longrightarrow> weight \<le> setsum (rr y) {..n}" |
|
1040 |
by(drule sym)(auto simp add: find_start_def split: split_if_asm intro: LeastI) |
|
1041 |
{ fix y weight n |
|
1042 |
assume find_start: "find_start y weight = Some n" |
|
1043 |
and weight: "0 \<le> weight" |
|
1044 |
have "setsum (rr y) {..n} \<le> rr y n + weight" |
|
1045 |
proof(rule ccontr) |
|
1046 |
assume "\<not> ?thesis" |
|
1047 |
hence "rr y n + weight < setsum (rr y) {..n}" by simp |
|
1048 |
moreover with weight obtain n' where "n = Suc n'" by(cases n) auto |
|
1049 |
ultimately have "weight \<le> setsum (rr y) {..n'}" by simp |
|
1050 |
hence "(LEAST n. weight \<le> setsum (rr y) {..n}) \<le> n'" by(rule Least_le) |
|
1051 |
moreover from find_start have "n = (LEAST n. weight \<le> setsum (rr y) {..n})" |
|
1052 |
by(auto simp add: find_start_def split: split_if_asm) |
|
1053 |
ultimately show False using \<open>n = Suc n'\<close> by auto |
|
1054 |
qed } |
|
1055 |
note find_start_eq_Some_least = this |
|
1056 |
have find_start_0 [simp]: "\<And>y. find_start y 0 = Some 0" |
|
1057 |
by(auto simp add: find_start_def intro!: exI[where x=0]) |
|
1058 |
{ fix y and weight :: real |
|
1059 |
assume "weight < \<integral>\<^sup>+ z. rr y z \<partial>count_space UNIV" |
|
1060 |
also have "(\<integral>\<^sup>+ z. rr y z \<partial>count_space UNIV) = (SUP n. \<Sum>z<n. ereal (rr y z))" |
|
1061 |
by(simp add: nn_integral_count_space_nat suminf_ereal_eq_SUP) |
|
1062 |
finally obtain n where "weight < (\<Sum>z<n. rr y z)" by(auto simp add: less_SUP_iff) |
|
1063 |
hence "weight \<in> dom (find_start y)" |
|
1064 |
by(auto simp add: find_start_def)(meson atMost_iff finite_atMost lessThan_iff less_imp_le order_trans pos_r setsum_mono3 subsetI) } |
|
1065 |
note in_dom_find_startI = this |
|
1066 |
{ fix y and w w' :: real and m |
|
1067 |
let ?m' = "LEAST m. w' \<le> setsum (rr y) {..m}" |
|
1068 |
assume "w' \<le> w" |
|
1069 |
also assume "find_start y w = Some m" |
|
1070 |
hence "w \<le> setsum (rr y) {..m}" by(rule find_start_eq_Some_above) |
|
1071 |
finally have "find_start y w' = Some ?m'" by(auto simp add: find_start_def) |
|
1072 |
moreover from \<open>w' \<le> setsum (rr y) {..m}\<close> have "?m' \<le> m" by(rule Least_le) |
|
1073 |
ultimately have "\<exists>m'. find_start y w' = Some m' \<and> m' \<le> m" by blast } |
|
1074 |
note find_start_mono = this[rotated] |
|
1075 |
||
1076 |
def assign \<equiv> "\<lambda>y x z. let used = setsum (pp y) {..<x} |
|
1077 |
in case find_start y used of None \<Rightarrow> 0 |
|
1078 |
| Some start \<Rightarrow> assign_aux y (setsum (rr y) {..start} - used) start (pp y x) z" |
|
1079 |
hence assign_alt_def: "\<And>y x z. assign y x z = |
|
1080 |
(let used = setsum (pp y) {..<x} |
|
1081 |
in case find_start y used of None \<Rightarrow> 0 |
|
1082 |
| Some start \<Rightarrow> assign_aux y (setsum (rr y) {..start} - used) start (pp y x) z)" |
|
1083 |
by simp |
|
1084 |
have assign_nonneg [simp]: "\<And>y x z. 0 \<le> assign y x z" |
|
1085 |
by(simp add: assign_def diff_le_iff find_start_eq_Some_above split: option.split) |
|
1086 |
have assign_eq_0_outside: "\<And>y x z. \<lbrakk> pp y x = 0 \<or> rr y z = 0 \<rbrakk> \<Longrightarrow> assign y x z = 0" |
|
1087 |
by(auto simp add: assign_def assign_aux_eq_0_outside diff_le_iff find_start_eq_Some_above find_start_eq_Some_least setsum_nonneg split: option.split) |
|
1088 |
||
1089 |
{ fix y x z |
|
1090 |
have "(\<Sum>n<Suc x. assign y n z) = |
|
1091 |
(case find_start y (setsum (pp y) {..<x}) of None \<Rightarrow> rr y z |
|
1092 |
| Some m \<Rightarrow> if z < m then rr y z |
|
1093 |
else min (rr y z) (max 0 (setsum (pp y) {..<x} + pp y x - setsum (rr y) {..<z})))" |
|
1094 |
(is "?lhs x = ?rhs x") |
|
1095 |
proof(induction x) |
|
1096 |
case 0 thus ?case |
|
1097 |
by(auto simp add: assign_def assign_aux_def setsum_head_upt_Suc atLeast0LessThan[symmetric] not_less field_simps max_def) |
|
1098 |
next |
|
1099 |
case (Suc x) |
|
1100 |
have "?lhs (Suc x) = ?lhs x + assign y (Suc x) z" by simp |
|
1101 |
also have "?lhs x = ?rhs x" by(rule Suc.IH) |
|
1102 |
also have "?rhs x + assign y (Suc x) z = ?rhs (Suc x)" |
|
1103 |
proof(cases "find_start y (setsum (pp y) {..<Suc x})") |
|
1104 |
case None |
|
1105 |
thus ?thesis |
|
1106 |
by(auto split: option.split simp add: assign_def min_def max_def diff_le_iff setsum_nonneg not_le field_simps) |
|
1107 |
(metis add.commute add_increasing find_start_def lessThan_Suc_atMost less_imp_le option.distinct(1) setsum_lessThan_Suc)+ |
|
1108 |
next |
|
1109 |
case (Some m) |
|
1110 |
have [simp]: "setsum (rr y) {..m} = rr y m + setsum (rr y) {..<m}" |
|
1111 |
by(simp add: ivl_disj_un(2)[symmetric]) |
|
1112 |
from Some obtain m' where m': "find_start y (setsum (pp y) {..<x}) = Some m'" "m' \<le> m" |
|
1113 |
by(auto dest: find_start_mono[where w'2="setsum (pp y) {..<x}"]) |
|
1114 |
moreover { |
|
1115 |
assume "z < m" |
|
1116 |
then have "setsum (rr y) {..z} \<le> setsum (rr y) {..<m}" |
|
1117 |
by(auto intro: setsum_mono3) |
|
1118 |
also have "\<dots> \<le> setsum (pp y) {..<Suc x}" using find_start_eq_Some_least[OF Some] |
|
1119 |
by(simp add: ivl_disj_un(2)[symmetric] setsum_nonneg) |
|
1120 |
finally have "rr y z \<le> max 0 (setsum (pp y) {..<x} + pp y x - setsum (rr y) {..<z})" |
|
1121 |
by(auto simp add: ivl_disj_un(2)[symmetric] max_def diff_le_iff simp del: r_convs) |
|
1122 |
} moreover { |
|
1123 |
assume "m \<le> z" |
|
1124 |
have "setsum (pp y) {..<Suc x} \<le> setsum (rr y) {..m}" |
|
1125 |
using Some by(rule find_start_eq_Some_above) |
|
1126 |
also have "\<dots> \<le> setsum (rr y) {..<Suc z}" using \<open>m \<le> z\<close> by(intro setsum_mono3) auto |
|
1127 |
finally have "max 0 (setsum (pp y) {..<x} + pp y x - setsum (rr y) {..<z}) \<le> rr y z" by simp |
|
1128 |
moreover have "z \<noteq> m \<Longrightarrow> setsum (rr y) {..m} + setsum (rr y) {Suc m..<z} = setsum (rr y) {..<z}" |
|
1129 |
using \<open>m \<le> z\<close> |
|
1130 |
by(subst ivl_disj_un(8)[where l="Suc m", symmetric]) |
|
1131 |
(simp_all add: setsum_Un ivl_disj_un(2)[symmetric] setsum.neutral) |
|
1132 |
moreover note calculation |
|
1133 |
} moreover { |
|
1134 |
assume "m < z" |
|
1135 |
have "setsum (pp y) {..<Suc x} \<le> setsum (rr y) {..m}" |
|
1136 |
using Some by(rule find_start_eq_Some_above) |
|
1137 |
also have "\<dots> \<le> setsum (rr y) {..<z}" using \<open>m < z\<close> by(intro setsum_mono3) auto |
|
1138 |
finally have "max 0 (setsum (pp y) {..<Suc x} - setsum (rr y) {..<z}) = 0" by simp } |
|
1139 |
moreover have "setsum (pp y) {..<Suc x} \<ge> setsum (rr y) {..<m}" |
|
1140 |
using find_start_eq_Some_least[OF Some] |
|
1141 |
by(simp add: setsum_nonneg ivl_disj_un(2)[symmetric]) |
|
1142 |
moreover hence "setsum (pp y) {..<Suc (Suc x)} \<ge> setsum (rr y) {..<m}" |
|
1143 |
by(fastforce intro: order_trans) |
|
1144 |
ultimately show ?thesis using Some |
|
1145 |
by(auto simp add: assign_def assign_aux_def Let_def field_simps max_def) |
|
1146 |
qed |
|
1147 |
finally show ?case . |
|
1148 |
qed } |
|
1149 |
note setsum_assign = this |
|
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
1150 |
|
59023 | 1151 |
have nn_integral_assign1: "\<And>y z. (\<integral>\<^sup>+ x. assign y x z \<partial>count_space UNIV) = rr y z" |
1152 |
proof - |
|
1153 |
fix y z |
|
1154 |
have "(\<integral>\<^sup>+ x. assign y x z \<partial>count_space UNIV) = (SUP n. ereal (\<Sum>x<n. assign y x z))" |
|
1155 |
by(simp add: nn_integral_count_space_nat suminf_ereal_eq_SUP) |
|
1156 |
also have "\<dots> = rr y z" |
|
1157 |
proof(rule antisym) |
|
1158 |
show "(SUP n. ereal (\<Sum>x<n. assign y x z)) \<le> rr y z" |
|
1159 |
proof(rule SUP_least) |
|
1160 |
fix n |
|
1161 |
show "ereal (\<Sum>x<n. (assign y x z)) \<le> rr y z" |
|
1162 |
using setsum_assign[of y z "n - 1"] |
|
1163 |
by(cases n)(simp_all split: option.split) |
|
1164 |
qed |
|
1165 |
show "rr y z \<le> (SUP n. ereal (\<Sum>x<n. assign y x z))" |
|
1166 |
proof(cases "setsum (rr y) {..z} < \<integral>\<^sup>+ x. pp y x \<partial>count_space UNIV") |
|
1167 |
case True |
|
1168 |
then obtain n where "setsum (rr y) {..z} < setsum (pp y) {..<n}" |
|
1169 |
by(auto simp add: nn_integral_count_space_nat suminf_ereal_eq_SUP less_SUP_iff) |
|
1170 |
moreover have "\<And>k. k < z \<Longrightarrow> setsum (rr y) {..k} \<le> setsum (rr y) {..<z}" |
|
1171 |
by(auto intro: setsum_mono3) |
|
1172 |
ultimately have "rr y z \<le> (\<Sum>x<Suc n. assign y x z)" |
|
1173 |
by(subst setsum_assign)(auto split: option.split dest!: find_start_eq_Some_above simp add: ivl_disj_un(2)[symmetric] add.commute add_increasing le_diff_eq le_max_iff_disj) |
|
1174 |
also have "\<dots> \<le> (SUP n. ereal (\<Sum>x<n. assign y x z))" |
|
1175 |
by(rule SUP_upper) simp |
|
1176 |
finally show ?thesis by simp |
|
1177 |
next |
|
1178 |
case False |
|
1179 |
have "setsum (rr y) {..z} = \<integral>\<^sup>+ z. rr y z \<partial>count_space {..z}" |
|
1180 |
by(simp add: nn_integral_count_space_finite max_def) |
|
1181 |
also have "\<dots> \<le> \<integral>\<^sup>+ z. rr y z \<partial>count_space UNIV" |
|
1182 |
by(auto simp add: nn_integral_count_space_indicator indicator_def intro: nn_integral_mono) |
|
1183 |
also have "\<dots> = \<integral>\<^sup>+ x. pp y x \<partial>count_space UNIV" by(simp add: eq) |
|
1184 |
finally have *: "setsum (rr y) {..z} = \<dots>" using False by simp |
|
1185 |
also have "\<dots> = (SUP n. ereal (\<Sum>x<n. pp y x))" |
|
1186 |
by(simp add: nn_integral_count_space_nat suminf_ereal_eq_SUP) |
|
1187 |
also have "\<dots> \<le> (SUP n. ereal (\<Sum>x<n. assign y x z)) + setsum (rr y) {..<z}" |
|
1188 |
proof(rule SUP_least) |
|
1189 |
fix n |
|
1190 |
have "setsum (pp y) {..<n} = \<integral>\<^sup>+ x. pp y x \<partial>count_space {..<n}" |
|
1191 |
by(simp add: nn_integral_count_space_finite max_def) |
|
1192 |
also have "\<dots> \<le> \<integral>\<^sup>+ x. pp y x \<partial>count_space UNIV" |
|
1193 |
by(auto simp add: nn_integral_count_space_indicator indicator_def intro: nn_integral_mono) |
|
1194 |
also have "\<dots> = setsum (rr y) {..z}" using * by simp |
|
1195 |
finally obtain k where k: "find_start y (setsum (pp y) {..<n}) = Some k" |
|
1196 |
by(fastforce simp add: find_start_def) |
|
1197 |
with \<open>ereal (setsum (pp y) {..<n}) \<le> setsum (rr y) {..z}\<close> |
|
1198 |
have "k \<le> z" by(auto simp add: find_start_def split: split_if_asm intro: Least_le) |
|
1199 |
then have "setsum (pp y) {..<n} - setsum (rr y) {..<z} \<le> ereal (\<Sum>x<Suc n. assign y x z)" |
|
1200 |
using \<open>ereal (setsum (pp y) {..<n}) \<le> setsum (rr y) {..z}\<close> |
|
1201 |
by(subst setsum_assign)(auto simp add: field_simps max_def k ivl_disj_un(2)[symmetric], metis le_add_same_cancel2 max.bounded_iff max_def pos_p) |
|
1202 |
also have "\<dots> \<le> (SUP n. ereal (\<Sum>x<n. assign y x z))" |
|
1203 |
by(rule SUP_upper) simp |
|
1204 |
finally show "ereal (\<Sum>x<n. pp y x) \<le> \<dots> + setsum (rr y) {..<z}" |
|
1205 |
by(simp add: ereal_minus(1)[symmetric] ereal_minus_le del: ereal_minus(1)) |
|
1206 |
qed |
|
1207 |
finally show ?thesis |
|
1208 |
by(simp add: ivl_disj_un(2)[symmetric] plus_ereal.simps(1)[symmetric] ereal_add_le_add_iff2 del: plus_ereal.simps(1)) |
|
1209 |
qed |
|
1210 |
qed |
|
1211 |
finally show "?thesis y z" . |
|
1212 |
qed |
|
1213 |
||
1214 |
{ fix y x |
|
1215 |
have "(\<integral>\<^sup>+ z. assign y x z \<partial>count_space UNIV) = pp y x" |
|
1216 |
proof(cases "setsum (pp y) {..<x} = \<integral>\<^sup>+ x. pp y x \<partial>count_space UNIV") |
|
1217 |
case False |
|
1218 |
let ?used = "setsum (pp y) {..<x}" |
|
1219 |
have "?used = \<integral>\<^sup>+ x. pp y x \<partial>count_space {..<x}" |
|
1220 |
by(simp add: nn_integral_count_space_finite max_def) |
|
1221 |
also have "\<dots> \<le> \<integral>\<^sup>+ x. pp y x \<partial>count_space UNIV" |
|
1222 |
by(auto simp add: nn_integral_count_space_indicator indicator_def intro!: nn_integral_mono) |
|
1223 |
finally have "?used < \<dots>" using False by auto |
|
1224 |
also note eq finally have "?used \<in> dom (find_start y)" by(rule in_dom_find_startI) |
|
1225 |
then obtain k where k: "find_start y ?used = Some k" by auto |
|
1226 |
let ?f = "\<lambda>z. if z < k then 0 else if z = k then setsum (rr y) {..k} - ?used else rr y z" |
|
1227 |
let ?g = "\<lambda>x'. if x' < x then 0 else pp y x'" |
|
1228 |
have "pp y x = ?g x" by simp |
|
1229 |
also have "?g x \<le> \<integral>\<^sup>+ x'. ?g x' \<partial>count_space UNIV" by(rule nn_integral_ge_point) simp |
|
1230 |
also { |
|
1231 |
have "?used = \<integral>\<^sup>+ x. pp y x \<partial>count_space {..<x}" |
|
1232 |
by(simp add: nn_integral_count_space_finite max_def) |
|
1233 |
also have "\<dots> = \<integral>\<^sup>+ x'. (if x' < x then pp y x' else 0) \<partial>count_space UNIV" |
|
1234 |
by(simp add: nn_integral_count_space_indicator indicator_def if_distrib zero_ereal_def cong: if_cong) |
|
1235 |
also have "(\<integral>\<^sup>+ x'. ?g x' \<partial>count_space UNIV) + \<dots> = \<integral>\<^sup>+ x. pp y x \<partial>count_space UNIV" |
|
1236 |
by(subst nn_integral_add[symmetric])(auto intro: nn_integral_cong) |
|
1237 |
also note calculation } |
|
1238 |
ultimately have "ereal (pp y x) + ?used \<le> \<integral>\<^sup>+ x. pp y x \<partial>count_space UNIV" |
|
1239 |
by (metis (no_types, lifting) ereal_add_mono order_refl) |
|
1240 |
also note eq |
|
1241 |
also have "(\<integral>\<^sup>+ z. rr y z \<partial>count_space UNIV) = (\<integral>\<^sup>+ z. ?f z \<partial>count_space UNIV) + (\<integral>\<^sup>+ z. (if z < k then rr y z else if z = k then ?used - setsum (rr y) {..<k} else 0) \<partial>count_space UNIV)" |
|
1242 |
using k by(subst nn_integral_add[symmetric])(auto intro!: nn_integral_cong simp add: ivl_disj_un(2)[symmetric] setsum_nonneg dest: find_start_eq_Some_least find_start_eq_Some_above) |
|
1243 |
also have "(\<integral>\<^sup>+ z. (if z < k then rr y z else if z = k then ?used - setsum (rr y) {..<k} else 0) \<partial>count_space UNIV) = |
|
1244 |
(\<integral>\<^sup>+ z. (if z < k then rr y z else if z = k then ?used - setsum (rr y) {..<k} else 0) \<partial>count_space {..k})" |
|
1245 |
by(auto simp add: nn_integral_count_space_indicator indicator_def intro: nn_integral_cong) |
|
1246 |
also have "\<dots> = ?used" |
|
1247 |
using k by(auto simp add: nn_integral_count_space_finite max_def ivl_disj_un(2)[symmetric] diff_le_iff setsum_nonneg dest: find_start_eq_Some_least) |
|
1248 |
finally have "pp y x \<le> (\<integral>\<^sup>+ z. ?f z \<partial>count_space UNIV)" |
|
1249 |
by(cases "\<integral>\<^sup>+ z. ?f z \<partial>count_space UNIV") simp_all |
|
1250 |
then show ?thesis using k |
|
1251 |
by(simp add: assign_def nn_integral_assign_aux diff_le_iff find_start_eq_Some_above min_def) |
|
1252 |
next |
|
1253 |
case True |
|
1254 |
have "setsum (pp y) {..x} = \<integral>\<^sup>+ x. pp y x \<partial>count_space {..x}" |
|
1255 |
by(simp add: nn_integral_count_space_finite max_def) |
|
1256 |
also have "\<dots> \<le> \<integral>\<^sup>+ x. pp y x \<partial>count_space UNIV" |
|
1257 |
by(auto simp add: nn_integral_count_space_indicator indicator_def intro: nn_integral_mono) |
|
1258 |
also have "\<dots> = setsum (pp y) {..<x}" by(simp add: True) |
|
1259 |
finally have "pp y x = 0" by(simp add: ivl_disj_un(2)[symmetric] eq_iff del: pp_convs) |
|
1260 |
thus ?thesis |
|
1261 |
by(cases "find_start y (setsum (pp y) {..<x})")(simp_all add: assign_def diff_le_iff find_start_eq_Some_above) |
|
1262 |
qed } |
|
1263 |
note nn_integral_assign2 = this |
|
1264 |
||
1265 |
let ?f = "\<lambda>y x z. if x \<in> ?A y \<and> z \<in> ?B y then assign y (?P y x) (?R y z) else 0" |
|
1266 |
def f \<equiv> "\<lambda>y x z. ereal (?f y x z)" |
|
1267 |
||
1268 |
have pos: "\<And>y x z. 0 \<le> f y x z" by(simp add: f_def) |
|
1269 |
{ fix y x z |
|
1270 |
have "f y x z \<le> 0 \<longleftrightarrow> f y x z = 0" using pos[of y x z] by simp } |
|
1271 |
note f [simp] = this |
|
1272 |
have support: |
|
1273 |
"\<And>x y z. (x, y) \<notin> set_pmf pq \<Longrightarrow> f y x z = 0" |
|
1274 |
"\<And>x y z. (y, z) \<notin> set_pmf qr \<Longrightarrow> f y x z = 0" |
|
1275 |
by(auto simp add: f_def) |
|
1276 |
||
1277 |
from pos support have support': |
|
1278 |
"\<And>x z. x \<notin> set_pmf p \<Longrightarrow> (\<integral>\<^sup>+ y. f y x z \<partial>count_space UNIV) = 0" |
|
1279 |
"\<And>x z. z \<notin> set_pmf r \<Longrightarrow> (\<integral>\<^sup>+ y. f y x z \<partial>count_space UNIV) = 0" |
|
1280 |
and support'': |
|
1281 |
"\<And>x y z. x \<notin> set_pmf p \<Longrightarrow> f y x z = 0" |
|
1282 |
"\<And>x y z. y \<notin> set_pmf q \<Longrightarrow> f y x z = 0" |
|
1283 |
"\<And>x y z. z \<notin> set_pmf r \<Longrightarrow> f y x z = 0" |
|
1284 |
by(auto simp add: nn_integral_0_iff_AE AE_count_space p q r set_map_pmf image_iff)(metis fst_conv snd_conv)+ |
|
1285 |
||
1286 |
have f_x: "\<And>y z. (\<integral>\<^sup>+ x. f y x z \<partial>count_space (set_pmf p)) = pmf qr (y, z)" |
|
1287 |
proof(case_tac "z \<in> ?B y") |
|
1288 |
fix y z |
|
1289 |
assume z: "z \<in> ?B y" |
|
1290 |
have "(\<integral>\<^sup>+ x. f y x z \<partial>count_space (set_pmf p)) = (\<integral>\<^sup>+ x. ?f y x z \<partial>count_space (?A y))" |
|
1291 |
using support''(1)[of _ y z] |
|
1292 |
by(fastforce simp add: f_def nn_integral_count_space_indicator indicator_def intro!: nn_integral_cong) |
|
1293 |
also have "\<dots> = \<integral>\<^sup>+ x. assign y (?P y x) (?R y z) \<partial>count_space (?A y)" |
|
1294 |
using z by(intro nn_integral_cong) simp |
|
1295 |
also have "\<dots> = \<integral>\<^sup>+ x. assign y x (?R y z) \<partial>count_space (?P y ` ?A y)" |
|
1296 |
by(intro nn_integral_bij_count_space inj_on_imp_bij_betw inj_on_to_nat_on) simp |
|
1297 |
also have "\<dots> = \<integral>\<^sup>+ x. assign y x (?R y z) \<partial>count_space UNIV" |
|
1298 |
by(auto simp add: nn_integral_count_space_indicator indicator_def assign_eq_0_outside pp_def intro!: nn_integral_cong) |
|
1299 |
also have "\<dots> = rr y (?R y z)" by(rule nn_integral_assign1) |
|
1300 |
also have "\<dots> = pmf qr (y, z)" using z by(simp add: rr_def) |
|
1301 |
finally show "?thesis y z" . |
|
1302 |
qed(auto simp add: f_def zero_ereal_def[symmetric] set_pmf_iff) |
|
1303 |
||
1304 |
have f_z: "\<And>x y. (\<integral>\<^sup>+ z. f y x z \<partial>count_space (set_pmf r)) = pmf pq (x, y)" |
|
1305 |
proof(case_tac "x \<in> ?A y") |
|
1306 |
fix x y |
|
1307 |
assume x: "x \<in> ?A y" |
|
1308 |
have "(\<integral>\<^sup>+ z. f y x z \<partial>count_space (set_pmf r)) = (\<integral>\<^sup>+ z. ?f y x z \<partial>count_space (?B y))" |
|
1309 |
using support''(3)[of _ y x] |
|
1310 |
by(fastforce simp add: f_def nn_integral_count_space_indicator indicator_def intro!: nn_integral_cong) |
|
1311 |
also have "\<dots> = \<integral>\<^sup>+ z. assign y (?P y x) (?R y z) \<partial>count_space (?B y)" |
|
1312 |
using x by(intro nn_integral_cong) simp |
|
1313 |
also have "\<dots> = \<integral>\<^sup>+ z. assign y (?P y x) z \<partial>count_space (?R y ` ?B y)" |
|
1314 |
by(intro nn_integral_bij_count_space inj_on_imp_bij_betw inj_on_to_nat_on) simp |
|
1315 |
also have "\<dots> = \<integral>\<^sup>+ z. assign y (?P y x) z \<partial>count_space UNIV" |
|
1316 |
by(auto simp add: nn_integral_count_space_indicator indicator_def assign_eq_0_outside rr_def intro!: nn_integral_cong) |
|
1317 |
also have "\<dots> = pp y (?P y x)" by(rule nn_integral_assign2) |
|
1318 |
also have "\<dots> = pmf pq (x, y)" using x by(simp add: pp_def) |
|
1319 |
finally show "?thesis x y" . |
|
1320 |
qed(auto simp add: f_def zero_ereal_def[symmetric] set_pmf_iff) |
|
1321 |
||
1322 |
let ?pr = "\<lambda>(x, z). \<integral>\<^sup>+ y. f y x z \<partial>count_space UNIV" |
|
1323 |
||
1324 |
have pr_pos: "\<And>xz. 0 \<le> ?pr xz" |
|
1325 |
by(auto simp add: nn_integral_nonneg) |
|
1326 |
||
1327 |
have pr': "?pr = (\<lambda>(x, z). \<integral>\<^sup>+ y. f y x z \<partial>count_space (set_pmf q))" |
|
1328 |
by(auto simp add: fun_eq_iff nn_integral_count_space_indicator indicator_def support'' intro: nn_integral_cong) |
|
1329 |
||
1330 |
have "(\<integral>\<^sup>+ xz. ?pr xz \<partial>count_space UNIV) = (\<integral>\<^sup>+ xz. ?pr xz * indicator (set_pmf p \<times> set_pmf r) xz \<partial>count_space UNIV)" |
|
1331 |
by(rule nn_integral_cong)(auto simp add: indicator_def support' intro: ccontr) |
|
1332 |
also have "\<dots> = (\<integral>\<^sup>+ xz. ?pr xz \<partial>count_space (set_pmf p \<times> set_pmf r))" |
|
1333 |
by(simp add: nn_integral_count_space_indicator) |
|
1334 |
also have "\<dots> = (\<integral>\<^sup>+ xz. ?pr xz \<partial>(count_space (set_pmf p) \<Otimes>\<^sub>M count_space (set_pmf r)))" |
|
1335 |
by(simp add: pair_measure_countable) |
|
1336 |
also have "\<dots> = (\<integral>\<^sup>+ (x, z). \<integral>\<^sup>+ y. f y x z \<partial>count_space (set_pmf q) \<partial>(count_space (set_pmf p) \<Otimes>\<^sub>M count_space (set_pmf r)))" |
|
1337 |
by(simp add: pr') |
|
1338 |
also have "\<dots> = (\<integral>\<^sup>+ x. \<integral>\<^sup>+ z. \<integral>\<^sup>+ y. f y x z \<partial>count_space (set_pmf q) \<partial>count_space (set_pmf r) \<partial>count_space (set_pmf p))" |
|
1339 |
by(subst sigma_finite_measure.nn_integral_fst[symmetric, OF sigma_finite_measure_count_space_countable])(simp_all add: pair_measure_countable) |
|
1340 |
also have "\<dots> = (\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. \<integral>\<^sup>+ z. f y x z \<partial>count_space (set_pmf r) \<partial>count_space (set_pmf q) \<partial>count_space (set_pmf p))" |
|
1341 |
by(subst (2) pair_sigma_finite.Fubini')(simp_all add: pair_sigma_finite.intro sigma_finite_measure_count_space_countable pair_measure_countable) |
|
1342 |
also have "\<dots> = (\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. pmf pq (x, y) \<partial>count_space (set_pmf q) \<partial>count_space (set_pmf p))" |
|
1343 |
by(simp add: f_z) |
|
1344 |
also have "\<dots> = (\<integral>\<^sup>+ y. \<integral>\<^sup>+ x. pmf pq (x, y) \<partial>count_space (set_pmf p) \<partial>count_space (set_pmf q))" |
|
1345 |
by(subst pair_sigma_finite.Fubini')(simp_all add: pair_sigma_finite.intro sigma_finite_measure_count_space_countable pair_measure_countable) |
|
1346 |
also have "\<dots> = (\<integral>\<^sup>+ y. \<integral>\<^sup>+ x. emeasure (measure_pmf pq) {(x, y)} \<partial>count_space (set_pmf p) \<partial>count_space (set_pmf q))" |
|
1347 |
by(simp add: emeasure_pmf_single) |
|
1348 |
also have "\<dots> = (\<integral>\<^sup>+ y. emeasure (measure_pmf pq) (\<Union>x\<in>set_pmf p. {(x, y)}) \<partial>count_space (set_pmf q))" |
|
1349 |
by(subst emeasure_UN_countable)(simp_all add: disjoint_family_on_def) |
|
1350 |
also have "\<dots> = (\<integral>\<^sup>+ y. emeasure (measure_pmf pq) ((\<Union>x\<in>set_pmf p. {(x, y)}) \<union> {(x, y'). x \<notin> set_pmf p \<and> y' = y}) \<partial>count_space (set_pmf q))" |
|
1351 |
by(rule nn_integral_cong emeasure_Un_null_set[symmetric])+ |
|
1352 |
(auto simp add: p set_map_pmf split_beta intro!: in_null_sets_measure_pmfI intro: rev_image_eqI) |
|
1353 |
also have "\<dots> = (\<integral>\<^sup>+ y. emeasure (measure_pmf pq) (snd -` {y}) \<partial>count_space (set_pmf q))" |
|
1354 |
by(rule nn_integral_cong arg_cong2[where f=emeasure])+auto |
|
1355 |
also have "\<dots> = (\<integral>\<^sup>+ y. pmf q y \<partial>count_space (set_pmf q))" |
|
1356 |
by(simp add: ereal_pmf_map q) |
|
1357 |
also have "\<dots> = (\<integral>\<^sup>+ y. pmf q y \<partial>count_space UNIV)" |
|
1358 |
by(auto simp add: nn_integral_count_space_indicator indicator_def set_pmf_iff intro: nn_integral_cong) |
|
1359 |
also have "\<dots> = 1" |
|
1360 |
by(subst nn_integral_pmf)(simp add: measure_pmf.emeasure_eq_1_AE) |
|
1361 |
finally have pr_prob: "(\<integral>\<^sup>+ xz. ?pr xz \<partial>count_space UNIV) = 1" . |
|
1362 |
||
1363 |
have pr_bounded: "\<And>xz. ?pr xz \<noteq> \<infinity>" |
|
1364 |
proof - |
|
1365 |
fix xz |
|
1366 |
have "?pr xz \<le> \<integral>\<^sup>+ xz. ?pr xz \<partial>count_space UNIV" |
|
1367 |
by(rule nn_integral_ge_point) simp |
|
1368 |
also have "\<dots> = 1" by(fact pr_prob) |
|
1369 |
finally show "?thesis xz" by auto |
|
1370 |
qed |
|
1371 |
||
1372 |
def pr \<equiv> "embed_pmf (real \<circ> ?pr)" |
|
1373 |
have pmf_pr: "\<And>xz. pmf pr xz = real (?pr xz)" using pr_pos pr_prob |
|
1374 |
unfolding pr_def by(subst pmf_embed_pmf)(auto simp add: real_of_ereal_pos ereal_real pr_bounded) |
|
1375 |
||
1376 |
have set_pmf_pr_subset: "set_pmf pr \<subseteq> set_pmf pq O set_pmf qr" |
|
1377 |
proof |
|
1378 |
fix xz :: "'a \<times> 'c" |
|
1379 |
obtain x z where xz: "xz = (x, z)" by(cases xz) |
|
1380 |
assume "xz \<in> set_pmf pr" |
|
1381 |
with xz have "pmf pr (x, z) \<noteq> 0" by(simp add: set_pmf_iff) |
|
1382 |
hence "\<exists>y. f y x z \<noteq> 0" by(rule contrapos_np)(simp add: pmf_pr) |
|
1383 |
then obtain y where y: "f y x z \<noteq> 0" .. |
|
1384 |
then have "(x, y) \<in> set_pmf pq" "(y, z) \<in> set_pmf qr" |
|
1385 |
using support by fastforce+ |
|
1386 |
then show "xz \<in> set_pmf pq O set_pmf qr" using xz by auto |
|
1387 |
qed |
|
1388 |
hence "\<And>x z. (x, z) \<in> set_pmf pr \<Longrightarrow> (R OO S) x z" using pq qr by blast |
|
1389 |
moreover |
|
1390 |
have "map_pmf fst pr = p" |
|
1391 |
proof(rule pmf_eqI) |
|
1392 |
fix x |
|
1393 |
have "pmf (map_pmf fst pr) x = emeasure (measure_pmf pr) (fst -` {x})" |
|
1394 |
by(simp add: ereal_pmf_map) |
|
1395 |
also have "\<dots> = \<integral>\<^sup>+ xz. pmf pr xz \<partial>count_space (fst -` {x})" |
|
1396 |
by(simp add: nn_integral_pmf) |
|
1397 |
also have "\<dots> = \<integral>\<^sup>+ xz. ?pr xz \<partial>count_space (fst -` {x})" |
|
1398 |
by(simp add: pmf_pr ereal_real pr_bounded pr_pos) |
|
1399 |
also have "\<dots> = \<integral>\<^sup>+ xz. ?pr xz \<partial>count_space {x} \<Otimes>\<^sub>M count_space (set_pmf r)" |
|
1400 |
by(auto simp add: nn_integral_count_space_indicator indicator_def support' pair_measure_countable intro!: nn_integral_cong) |
|
1401 |
also have "\<dots> = \<integral>\<^sup>+ z. \<integral>\<^sup>+ x. ?pr (x, z) \<partial>count_space {x} \<partial>count_space (set_pmf r)" |
|
1402 |
by(subst pair_sigma_finite.nn_integral_snd[symmetric])(simp_all add: pair_measure_countable pair_sigma_finite.intro sigma_finite_measure_count_space_countable) |
|
1403 |
also have "\<dots> = \<integral>\<^sup>+ z. ?pr (x, z) \<partial>count_space (set_pmf r)" |
|
1404 |
using pr_pos by(clarsimp simp add: nn_integral_count_space_finite max_def) |
|
1405 |
also have "\<dots> = \<integral>\<^sup>+ z. \<integral>\<^sup>+ y. f y x z \<partial>count_space (set_pmf q) \<partial>count_space (set_pmf r)" |
|
1406 |
by(simp add: pr') |
|
1407 |
also have "\<dots> = \<integral>\<^sup>+ y. \<integral>\<^sup>+ z. f y x z \<partial>count_space (set_pmf r) \<partial>count_space (set_pmf q)" |
|
1408 |
by(subst pair_sigma_finite.Fubini')(simp_all add: pair_sigma_finite.intro sigma_finite_measure_count_space_countable pair_measure_countable) |
|
1409 |
also have "\<dots> = \<integral>\<^sup>+ y. pmf pq (x, y) \<partial>count_space (set_pmf q)" |
|
1410 |
by(simp add: f_z) |
|
1411 |
also have "\<dots> = \<integral>\<^sup>+ y. emeasure (measure_pmf pq) {(x, y)} \<partial>count_space (set_pmf q)" |
|
1412 |
by(simp add: emeasure_pmf_single) |
|
1413 |
also have "\<dots> = emeasure (measure_pmf pq) (\<Union>y\<in>set_pmf q. {(x, y)})" |
|
1414 |
by(subst emeasure_UN_countable)(simp_all add: disjoint_family_on_def) |
|
1415 |
also have "\<dots> = emeasure (measure_pmf pq) ((\<Union>y\<in>set_pmf q. {(x, y)}) \<union> {(x', y). y \<notin> set_pmf q \<and> x' = x})" |
|
1416 |
by(rule emeasure_Un_null_set[symmetric])+ |
|
1417 |
(auto simp add: q set_map_pmf split_beta intro!: in_null_sets_measure_pmfI intro: rev_image_eqI) |
|
1418 |
also have "\<dots> = emeasure (measure_pmf pq) (fst -` {x})" |
|
1419 |
by(rule arg_cong2[where f=emeasure])+auto |
|
1420 |
also have "\<dots> = pmf p x" by(simp add: ereal_pmf_map p) |
|
1421 |
finally show "pmf (map_pmf fst pr) x = pmf p x" by simp |
|
1422 |
qed |
|
1423 |
moreover |
|
1424 |
have "map_pmf snd pr = r" |
|
1425 |
proof(rule pmf_eqI) |
|
1426 |
fix z |
|
1427 |
have "pmf (map_pmf snd pr) z = emeasure (measure_pmf pr) (snd -` {z})" |
|
1428 |
by(simp add: ereal_pmf_map) |
|
1429 |
also have "\<dots> = \<integral>\<^sup>+ xz. pmf pr xz \<partial>count_space (snd -` {z})" |
|
1430 |
by(simp add: nn_integral_pmf) |
|
1431 |
also have "\<dots> = \<integral>\<^sup>+ xz. ?pr xz \<partial>count_space (snd -` {z})" |
|
1432 |
by(simp add: pmf_pr ereal_real pr_bounded pr_pos) |
|
1433 |
also have "\<dots> = \<integral>\<^sup>+ xz. ?pr xz \<partial>count_space (set_pmf p) \<Otimes>\<^sub>M count_space {z}" |
|
1434 |
by(auto simp add: nn_integral_count_space_indicator indicator_def support' pair_measure_countable intro!: nn_integral_cong) |
|
1435 |
also have "\<dots> = \<integral>\<^sup>+ x. \<integral>\<^sup>+ z. ?pr (x, z) \<partial>count_space {z} \<partial>count_space (set_pmf p)" |
|
1436 |
by(subst sigma_finite_measure.nn_integral_fst[symmetric])(simp_all add: pair_measure_countable sigma_finite_measure_count_space_countable) |
|
1437 |
also have "\<dots> = \<integral>\<^sup>+ x. ?pr (x, z) \<partial>count_space (set_pmf p)" |
|
1438 |
using pr_pos by(clarsimp simp add: nn_integral_count_space_finite max_def) |
|
1439 |
also have "\<dots> = \<integral>\<^sup>+ x. \<integral>\<^sup>+ y. f y x z \<partial>count_space (set_pmf q) \<partial>count_space (set_pmf p)" |
|
1440 |
by(simp add: pr') |
|
1441 |
also have "\<dots> = \<integral>\<^sup>+ y. \<integral>\<^sup>+ x. f y x z \<partial>count_space (set_pmf p) \<partial>count_space (set_pmf q)" |
|
1442 |
by(subst pair_sigma_finite.Fubini')(simp_all add: pair_sigma_finite.intro sigma_finite_measure_count_space_countable pair_measure_countable) |
|
1443 |
also have "\<dots> = \<integral>\<^sup>+ y. pmf qr (y, z) \<partial>count_space (set_pmf q)" |
|
1444 |
by(simp add: f_x) |
|
1445 |
also have "\<dots> = \<integral>\<^sup>+ y. emeasure (measure_pmf qr) {(y, z)} \<partial>count_space (set_pmf q)" |
|
1446 |
by(simp add: emeasure_pmf_single) |
|
1447 |
also have "\<dots> = emeasure (measure_pmf qr) (\<Union>y\<in>set_pmf q. {(y, z)})" |
|
1448 |
by(subst emeasure_UN_countable)(simp_all add: disjoint_family_on_def) |
|
1449 |
also have "\<dots> = emeasure (measure_pmf qr) ((\<Union>y\<in>set_pmf q. {(y, z)}) \<union> {(y, z'). y \<notin> set_pmf q \<and> z' = z})" |
|
1450 |
by(rule emeasure_Un_null_set[symmetric])+ |
|
1451 |
(auto simp add: q' set_map_pmf split_beta intro!: in_null_sets_measure_pmfI intro: rev_image_eqI) |
|
1452 |
also have "\<dots> = emeasure (measure_pmf qr) (snd -` {z})" |
|
1453 |
by(rule arg_cong2[where f=emeasure])+auto |
|
1454 |
also have "\<dots> = pmf r z" by(simp add: ereal_pmf_map r) |
|
1455 |
finally show "pmf (map_pmf snd pr) z = pmf r z" by simp |
|
1456 |
qed |
|
1457 |
ultimately have "rel_pmf (R OO S) p r" .. } |
|
1458 |
then show "rel_pmf R OO rel_pmf S \<le> rel_pmf (R OO S)" |
|
1459 |
by(auto simp add: le_fun_def) |
|
1460 |
qed (fact natLeq_card_order natLeq_cinfinite)+ |
|
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
1461 |
|
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
1462 |
end |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
diff
changeset
|
1463 |