author | hoelzl |
Wed, 10 Oct 2012 12:12:25 +0200 | |
changeset 49786 | f33d5f009627 |
parent 49783 | 38b84d1802ed |
child 49788 | 3c10763f5cb4 |
permissions | -rw-r--r-- |
42148 | 1 |
(* Title: HOL/Probability/Probability_Measure.thy |
42067 | 2 |
Author: Johannes Hölzl, TU München |
3 |
Author: Armin Heller, TU München |
|
4 |
*) |
|
5 |
||
42148 | 6 |
header {*Probability measure*} |
42067 | 7 |
|
42148 | 8 |
theory Probability_Measure |
47694 | 9 |
imports Lebesgue_Measure Radon_Nikodym |
35582 | 10 |
begin |
11 |
||
47694 | 12 |
lemma funset_eq_UN_fun_upd_I: |
13 |
assumes *: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f(a := d) \<in> F A" |
|
14 |
and **: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f a \<in> G (f(a:=d))" |
|
15 |
and ***: "\<And>f x. \<lbrakk> f \<in> F A ; x \<in> G f \<rbrakk> \<Longrightarrow> f(a:=x) \<in> F (insert a A)" |
|
16 |
shows "F (insert a A) = (\<Union>f\<in>F A. fun_upd f a ` (G f))" |
|
17 |
proof safe |
|
18 |
fix f assume f: "f \<in> F (insert a A)" |
|
19 |
show "f \<in> (\<Union>f\<in>F A. fun_upd f a ` G f)" |
|
20 |
proof (rule UN_I[of "f(a := d)"]) |
|
21 |
show "f(a := d) \<in> F A" using *[OF f] . |
|
22 |
show "f \<in> fun_upd (f(a:=d)) a ` G (f(a:=d))" |
|
23 |
proof (rule image_eqI[of _ _ "f a"]) |
|
24 |
show "f a \<in> G (f(a := d))" using **[OF f] . |
|
25 |
qed simp |
|
26 |
qed |
|
27 |
next |
|
28 |
fix f x assume "f \<in> F A" "x \<in> G f" |
|
29 |
from ***[OF this] show "f(a := x) \<in> F (insert a A)" . |
|
30 |
qed |
|
31 |
||
32 |
lemma extensional_funcset_insert_eq[simp]: |
|
33 |
assumes "a \<notin> A" |
|
34 |
shows "extensional (insert a A) \<inter> (insert a A \<rightarrow> B) = (\<Union>f \<in> extensional A \<inter> (A \<rightarrow> B). (\<lambda>b. f(a := b)) ` B)" |
|
35 |
apply (rule funset_eq_UN_fun_upd_I) |
|
36 |
using assms |
|
37 |
by (auto intro!: inj_onI dest: inj_onD split: split_if_asm simp: extensional_def) |
|
38 |
||
39 |
lemma finite_extensional_funcset[simp, intro]: |
|
40 |
assumes "finite A" "finite B" |
|
41 |
shows "finite (extensional A \<inter> (A \<rightarrow> B))" |
|
42 |
using assms by induct auto |
|
43 |
||
44 |
lemma finite_PiE[simp, intro]: |
|
45 |
assumes fin: "finite A" "\<And>i. i \<in> A \<Longrightarrow> finite (B i)" |
|
46 |
shows "finite (Pi\<^isub>E A B)" |
|
47 |
proof - |
|
48 |
have *: "(Pi\<^isub>E A B) \<subseteq> extensional A \<inter> (A \<rightarrow> (\<Union>i\<in>A. B i))" by auto |
|
49 |
show ?thesis |
|
50 |
using fin by (intro finite_subset[OF *] finite_extensional_funcset) auto |
|
51 |
qed |
|
52 |
||
53 |
||
54 |
lemma countably_additiveI[case_names countably]: |
|
55 |
assumes "\<And>A. \<lbrakk> range A \<subseteq> M ; disjoint_family A ; (\<Union>i. A i) \<in> M\<rbrakk> \<Longrightarrow> (\<Sum>n. \<mu> (A n)) = \<mu> (\<Union>i. A i)" |
|
56 |
shows "countably_additive M \<mu>" |
|
57 |
using assms unfolding countably_additive_def by auto |
|
58 |
||
59 |
lemma convex_le_Inf_differential: |
|
60 |
fixes f :: "real \<Rightarrow> real" |
|
61 |
assumes "convex_on I f" |
|
62 |
assumes "x \<in> interior I" "y \<in> I" |
|
63 |
shows "f y \<ge> f x + Inf ((\<lambda>t. (f x - f t) / (x - t)) ` ({x<..} \<inter> I)) * (y - x)" |
|
64 |
(is "_ \<ge> _ + Inf (?F x) * (y - x)") |
|
65 |
proof - |
|
66 |
show ?thesis |
|
67 |
proof (cases rule: linorder_cases) |
|
68 |
assume "x < y" |
|
69 |
moreover |
|
70 |
have "open (interior I)" by auto |
|
71 |
from openE[OF this `x \<in> interior I`] guess e . note e = this |
|
72 |
moreover def t \<equiv> "min (x + e / 2) ((x + y) / 2)" |
|
73 |
ultimately have "x < t" "t < y" "t \<in> ball x e" |
|
74 |
by (auto simp: dist_real_def field_simps split: split_min) |
|
75 |
with `x \<in> interior I` e interior_subset[of I] have "t \<in> I" "x \<in> I" by auto |
|
76 |
||
77 |
have "open (interior I)" by auto |
|
78 |
from openE[OF this `x \<in> interior I`] guess e . |
|
79 |
moreover def K \<equiv> "x - e / 2" |
|
80 |
with `0 < e` have "K \<in> ball x e" "K < x" by (auto simp: dist_real_def) |
|
81 |
ultimately have "K \<in> I" "K < x" "x \<in> I" |
|
82 |
using interior_subset[of I] `x \<in> interior I` by auto |
|
83 |
||
84 |
have "Inf (?F x) \<le> (f x - f y) / (x - y)" |
|
85 |
proof (rule Inf_lower2) |
|
86 |
show "(f x - f t) / (x - t) \<in> ?F x" |
|
87 |
using `t \<in> I` `x < t` by auto |
|
88 |
show "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)" |
|
89 |
using `convex_on I f` `x \<in> I` `y \<in> I` `x < t` `t < y` by (rule convex_on_diff) |
|
90 |
next |
|
91 |
fix y assume "y \<in> ?F x" |
|
92 |
with order_trans[OF convex_on_diff[OF `convex_on I f` `K \<in> I` _ `K < x` _]] |
|
93 |
show "(f K - f x) / (K - x) \<le> y" by auto |
|
94 |
qed |
|
95 |
then show ?thesis |
|
96 |
using `x < y` by (simp add: field_simps) |
|
97 |
next |
|
98 |
assume "y < x" |
|
99 |
moreover |
|
100 |
have "open (interior I)" by auto |
|
101 |
from openE[OF this `x \<in> interior I`] guess e . note e = this |
|
102 |
moreover def t \<equiv> "x + e / 2" |
|
103 |
ultimately have "x < t" "t \<in> ball x e" |
|
104 |
by (auto simp: dist_real_def field_simps) |
|
105 |
with `x \<in> interior I` e interior_subset[of I] have "t \<in> I" "x \<in> I" by auto |
|
106 |
||
107 |
have "(f x - f y) / (x - y) \<le> Inf (?F x)" |
|
108 |
proof (rule Inf_greatest) |
|
109 |
have "(f x - f y) / (x - y) = (f y - f x) / (y - x)" |
|
110 |
using `y < x` by (auto simp: field_simps) |
|
111 |
also |
|
112 |
fix z assume "z \<in> ?F x" |
|
113 |
with order_trans[OF convex_on_diff[OF `convex_on I f` `y \<in> I` _ `y < x`]] |
|
114 |
have "(f y - f x) / (y - x) \<le> z" by auto |
|
115 |
finally show "(f x - f y) / (x - y) \<le> z" . |
|
116 |
next |
|
117 |
have "open (interior I)" by auto |
|
118 |
from openE[OF this `x \<in> interior I`] guess e . note e = this |
|
119 |
then have "x + e / 2 \<in> ball x e" by (auto simp: dist_real_def) |
|
120 |
with e interior_subset[of I] have "x + e / 2 \<in> {x<..} \<inter> I" by auto |
|
121 |
then show "?F x \<noteq> {}" by blast |
|
122 |
qed |
|
123 |
then show ?thesis |
|
124 |
using `y < x` by (simp add: field_simps) |
|
125 |
qed simp |
|
126 |
qed |
|
127 |
||
128 |
lemma distr_id[simp]: "distr N N (\<lambda>x. x) = N" |
|
129 |
by (rule measure_eqI) (auto simp: emeasure_distr) |
|
130 |
||
45777
c36637603821
remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset
|
131 |
locale prob_space = finite_measure + |
47694 | 132 |
assumes emeasure_space_1: "emeasure M (space M) = 1" |
38656 | 133 |
|
45777
c36637603821
remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset
|
134 |
lemma prob_spaceI[Pure.intro!]: |
47694 | 135 |
assumes *: "emeasure M (space M) = 1" |
45777
c36637603821
remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset
|
136 |
shows "prob_space M" |
c36637603821
remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset
|
137 |
proof - |
c36637603821
remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset
|
138 |
interpret finite_measure M |
c36637603821
remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset
|
139 |
proof |
47694 | 140 |
show "emeasure M (space M) \<noteq> \<infinity>" using * by simp |
45777
c36637603821
remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset
|
141 |
qed |
c36637603821
remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset
|
142 |
show "prob_space M" by default fact |
38656 | 143 |
qed |
144 |
||
40859 | 145 |
abbreviation (in prob_space) "events \<equiv> sets M" |
47694 | 146 |
abbreviation (in prob_space) "prob \<equiv> measure M" |
147 |
abbreviation (in prob_space) "random_variable M' X \<equiv> X \<in> measurable M M'" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
148 |
abbreviation (in prob_space) "expectation \<equiv> integral\<^isup>L M" |
35582 | 149 |
|
47694 | 150 |
lemma (in prob_space) prob_space_distr: |
151 |
assumes f: "f \<in> measurable M M'" shows "prob_space (distr M M' f)" |
|
152 |
proof (rule prob_spaceI) |
|
153 |
have "f -` space M' \<inter> space M = space M" using f by (auto dest: measurable_space) |
|
154 |
with f show "emeasure (distr M M' f) (space (distr M M' f)) = 1" |
|
155 |
by (auto simp: emeasure_distr emeasure_space_1) |
|
43339 | 156 |
qed |
157 |
||
40859 | 158 |
lemma (in prob_space) prob_space: "prob (space M) = 1" |
47694 | 159 |
using emeasure_space_1 unfolding measure_def by (simp add: one_ereal_def) |
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset
|
160 |
|
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset
|
161 |
lemma (in prob_space) prob_le_1[simp, intro]: "prob A \<le> 1" |
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset
|
162 |
using bounded_measure[of A] by (simp add: prob_space) |
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset
|
163 |
|
47694 | 164 |
lemma (in prob_space) not_empty: "space M \<noteq> {}" |
165 |
using prob_space by auto |
|
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset
|
166 |
|
47694 | 167 |
lemma (in prob_space) measure_le_1: "emeasure M X \<le> 1" |
168 |
using emeasure_space[of M X] by (simp add: emeasure_space_1) |
|
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42902
diff
changeset
|
169 |
|
43339 | 170 |
lemma (in prob_space) AE_I_eq_1: |
47694 | 171 |
assumes "emeasure M {x\<in>space M. P x} = 1" "{x\<in>space M. P x} \<in> sets M" |
172 |
shows "AE x in M. P x" |
|
43339 | 173 |
proof (rule AE_I) |
47694 | 174 |
show "emeasure M (space M - {x \<in> space M. P x}) = 0" |
175 |
using assms emeasure_space_1 by (simp add: emeasure_compl) |
|
43339 | 176 |
qed (insert assms, auto) |
177 |
||
40859 | 178 |
lemma (in prob_space) prob_compl: |
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset
|
179 |
assumes A: "A \<in> events" |
38656 | 180 |
shows "prob (space M - A) = 1 - prob A" |
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset
|
181 |
using finite_measure_compl[OF A] by (simp add: prob_space) |
35582 | 182 |
|
47694 | 183 |
lemma (in prob_space) AE_in_set_eq_1: |
184 |
assumes "A \<in> events" shows "(AE x in M. x \<in> A) \<longleftrightarrow> prob A = 1" |
|
185 |
proof |
|
186 |
assume ae: "AE x in M. x \<in> A" |
|
187 |
have "{x \<in> space M. x \<in> A} = A" "{x \<in> space M. x \<notin> A} = space M - A" |
|
188 |
using `A \<in> events`[THEN sets_into_space] by auto |
|
189 |
with AE_E2[OF ae] `A \<in> events` have "1 - emeasure M A = 0" |
|
190 |
by (simp add: emeasure_compl emeasure_space_1) |
|
191 |
then show "prob A = 1" |
|
192 |
using `A \<in> events` by (simp add: emeasure_eq_measure one_ereal_def) |
|
193 |
next |
|
194 |
assume prob: "prob A = 1" |
|
195 |
show "AE x in M. x \<in> A" |
|
196 |
proof (rule AE_I) |
|
197 |
show "{x \<in> space M. x \<notin> A} \<subseteq> space M - A" by auto |
|
198 |
show "emeasure M (space M - A) = 0" |
|
199 |
using `A \<in> events` prob |
|
200 |
by (simp add: prob_compl emeasure_space_1 emeasure_eq_measure one_ereal_def) |
|
201 |
show "space M - A \<in> events" |
|
202 |
using `A \<in> events` by auto |
|
203 |
qed |
|
204 |
qed |
|
205 |
||
206 |
lemma (in prob_space) AE_False: "(AE x in M. False) \<longleftrightarrow> False" |
|
207 |
proof |
|
208 |
assume "AE x in M. False" |
|
209 |
then have "AE x in M. x \<in> {}" by simp |
|
210 |
then show False |
|
211 |
by (subst (asm) AE_in_set_eq_1) auto |
|
212 |
qed simp |
|
213 |
||
214 |
lemma (in prob_space) AE_prob_1: |
|
215 |
assumes "prob A = 1" shows "AE x in M. x \<in> A" |
|
216 |
proof - |
|
217 |
from `prob A = 1` have "A \<in> events" |
|
218 |
by (metis measure_notin_sets zero_neq_one) |
|
219 |
with AE_in_set_eq_1 assms show ?thesis by simp |
|
220 |
qed |
|
221 |
||
49783 | 222 |
lemma (in finite_measure) prob_space_increasing: "increasing M (measure M)" |
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset
|
223 |
by (auto intro!: finite_measure_mono simp: increasing_def) |
35582 | 224 |
|
49783 | 225 |
lemma (in finite_measure) prob_zero_union: |
226 |
assumes "s \<in> sets M" "t \<in> sets M" "measure M t = 0" |
|
227 |
shows "measure M (s \<union> t) = measure M s" |
|
38656 | 228 |
using assms |
35582 | 229 |
proof - |
49783 | 230 |
have "measure M (s \<union> t) \<le> measure M s" |
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset
|
231 |
using finite_measure_subadditive[of s t] assms by auto |
49783 | 232 |
moreover have "measure M (s \<union> t) \<ge> measure M s" |
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset
|
233 |
using assms by (blast intro: finite_measure_mono) |
35582 | 234 |
ultimately show ?thesis by simp |
235 |
qed |
|
236 |
||
49783 | 237 |
lemma (in finite_measure) prob_eq_compl: |
238 |
assumes "s \<in> sets M" "t \<in> sets M" |
|
239 |
assumes "measure M (space M - s) = measure M (space M - t)" |
|
240 |
shows "measure M s = measure M t" |
|
241 |
using assms finite_measure_compl by auto |
|
35582 | 242 |
|
40859 | 243 |
lemma (in prob_space) prob_one_inter: |
35582 | 244 |
assumes events:"s \<in> events" "t \<in> events" |
245 |
assumes "prob t = 1" |
|
246 |
shows "prob (s \<inter> t) = prob s" |
|
247 |
proof - |
|
38656 | 248 |
have "prob ((space M - s) \<union> (space M - t)) = prob (space M - s)" |
249 |
using events assms prob_compl[of "t"] by (auto intro!: prob_zero_union) |
|
250 |
also have "(space M - s) \<union> (space M - t) = space M - (s \<inter> t)" |
|
251 |
by blast |
|
252 |
finally show "prob (s \<inter> t) = prob s" |
|
253 |
using events by (auto intro!: prob_eq_compl[of "s \<inter> t" s]) |
|
35582 | 254 |
qed |
255 |
||
49783 | 256 |
lemma (in finite_measure) prob_eq_bigunion_image: |
257 |
assumes "range f \<subseteq> sets M" "range g \<subseteq> sets M" |
|
35582 | 258 |
assumes "disjoint_family f" "disjoint_family g" |
49783 | 259 |
assumes "\<And> n :: nat. measure M (f n) = measure M (g n)" |
260 |
shows "measure M (\<Union> i. f i) = measure M (\<Union> i. g i)" |
|
35582 | 261 |
using assms |
262 |
proof - |
|
49783 | 263 |
have a: "(\<lambda> i. measure M (f i)) sums (measure M (\<Union> i. f i))" |
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset
|
264 |
by (rule finite_measure_UNION[OF assms(1,3)]) |
49783 | 265 |
have b: "(\<lambda> i. measure M (g i)) sums (measure M (\<Union> i. g i))" |
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset
|
266 |
by (rule finite_measure_UNION[OF assms(2,4)]) |
38656 | 267 |
show ?thesis using sums_unique[OF b] sums_unique[OF a] assms by simp |
35582 | 268 |
qed |
269 |
||
49783 | 270 |
lemma (in finite_measure) prob_countably_zero: |
271 |
assumes "range c \<subseteq> sets M" |
|
272 |
assumes "\<And> i. measure M (c i) = 0" |
|
273 |
shows "measure M (\<Union> i :: nat. c i) = 0" |
|
38656 | 274 |
proof (rule antisym) |
49783 | 275 |
show "measure M (\<Union> i :: nat. c i) \<le> 0" |
47694 | 276 |
using finite_measure_subadditive_countably[OF assms(1)] by (simp add: assms(2)) |
277 |
qed (simp add: measure_nonneg) |
|
35582 | 278 |
|
40859 | 279 |
lemma (in prob_space) prob_equiprobable_finite_unions: |
38656 | 280 |
assumes "s \<in> events" |
281 |
assumes s_finite: "finite s" "\<And>x. x \<in> s \<Longrightarrow> {x} \<in> events" |
|
35582 | 282 |
assumes "\<And> x y. \<lbrakk>x \<in> s; y \<in> s\<rbrakk> \<Longrightarrow> (prob {x} = prob {y})" |
38656 | 283 |
shows "prob s = real (card s) * prob {SOME x. x \<in> s}" |
35582 | 284 |
proof (cases "s = {}") |
38656 | 285 |
case False hence "\<exists> x. x \<in> s" by blast |
35582 | 286 |
from someI_ex[OF this] assms |
287 |
have prob_some: "\<And> x. x \<in> s \<Longrightarrow> prob {x} = prob {SOME y. y \<in> s}" by blast |
|
288 |
have "prob s = (\<Sum> x \<in> s. prob {x})" |
|
47694 | 289 |
using finite_measure_eq_setsum_singleton[OF s_finite] by simp |
35582 | 290 |
also have "\<dots> = (\<Sum> x \<in> s. prob {SOME y. y \<in> s})" using prob_some by auto |
38656 | 291 |
also have "\<dots> = real (card s) * prob {(SOME x. x \<in> s)}" |
292 |
using setsum_constant assms by (simp add: real_eq_of_nat) |
|
35582 | 293 |
finally show ?thesis by simp |
38656 | 294 |
qed simp |
35582 | 295 |
|
40859 | 296 |
lemma (in prob_space) prob_real_sum_image_fn: |
35582 | 297 |
assumes "e \<in> events" |
298 |
assumes "\<And> x. x \<in> s \<Longrightarrow> e \<inter> f x \<in> events" |
|
299 |
assumes "finite s" |
|
38656 | 300 |
assumes disjoint: "\<And> x y. \<lbrakk>x \<in> s ; y \<in> s ; x \<noteq> y\<rbrakk> \<Longrightarrow> f x \<inter> f y = {}" |
301 |
assumes upper: "space M \<subseteq> (\<Union> i \<in> s. f i)" |
|
35582 | 302 |
shows "prob e = (\<Sum> x \<in> s. prob (e \<inter> f x))" |
303 |
proof - |
|
38656 | 304 |
have e: "e = (\<Union> i \<in> s. e \<inter> f i)" |
305 |
using `e \<in> events` sets_into_space upper by blast |
|
306 |
hence "prob e = prob (\<Union> i \<in> s. e \<inter> f i)" by simp |
|
307 |
also have "\<dots> = (\<Sum> x \<in> s. prob (e \<inter> f x))" |
|
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset
|
308 |
proof (rule finite_measure_finite_Union) |
38656 | 309 |
show "finite s" by fact |
47694 | 310 |
show "(\<lambda>i. e \<inter> f i)`s \<subseteq> events" using assms(2) by auto |
38656 | 311 |
show "disjoint_family_on (\<lambda>i. e \<inter> f i) s" |
312 |
using disjoint by (auto simp: disjoint_family_on_def) |
|
313 |
qed |
|
314 |
finally show ?thesis . |
|
35582 | 315 |
qed |
316 |
||
43339 | 317 |
lemma (in prob_space) expectation_less: |
318 |
assumes [simp]: "integrable M X" |
|
49786 | 319 |
assumes gt: "AE x in M. X x < b" |
43339 | 320 |
shows "expectation X < b" |
321 |
proof - |
|
322 |
have "expectation X < expectation (\<lambda>x. b)" |
|
47694 | 323 |
using gt emeasure_space_1 |
43340
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
43339
diff
changeset
|
324 |
by (intro integral_less_AE_space) auto |
43339 | 325 |
then show ?thesis using prob_space by simp |
326 |
qed |
|
327 |
||
328 |
lemma (in prob_space) expectation_greater: |
|
329 |
assumes [simp]: "integrable M X" |
|
49786 | 330 |
assumes gt: "AE x in M. a < X x" |
43339 | 331 |
shows "a < expectation X" |
332 |
proof - |
|
333 |
have "expectation (\<lambda>x. a) < expectation X" |
|
47694 | 334 |
using gt emeasure_space_1 |
43340
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
43339
diff
changeset
|
335 |
by (intro integral_less_AE_space) auto |
43339 | 336 |
then show ?thesis using prob_space by simp |
337 |
qed |
|
338 |
||
339 |
lemma (in prob_space) jensens_inequality: |
|
340 |
fixes a b :: real |
|
49786 | 341 |
assumes X: "integrable M X" "AE x in M. X x \<in> I" |
43339 | 342 |
assumes I: "I = {a <..< b} \<or> I = {a <..} \<or> I = {..< b} \<or> I = UNIV" |
343 |
assumes q: "integrable M (\<lambda>x. q (X x))" "convex_on I q" |
|
344 |
shows "q (expectation X) \<le> expectation (\<lambda>x. q (X x))" |
|
345 |
proof - |
|
46731 | 346 |
let ?F = "\<lambda>x. Inf ((\<lambda>t. (q x - q t) / (x - t)) ` ({x<..} \<inter> I))" |
49786 | 347 |
from X(2) AE_False have "I \<noteq> {}" by auto |
43339 | 348 |
|
349 |
from I have "open I" by auto |
|
350 |
||
351 |
note I |
|
352 |
moreover |
|
353 |
{ assume "I \<subseteq> {a <..}" |
|
354 |
with X have "a < expectation X" |
|
355 |
by (intro expectation_greater) auto } |
|
356 |
moreover |
|
357 |
{ assume "I \<subseteq> {..< b}" |
|
358 |
with X have "expectation X < b" |
|
359 |
by (intro expectation_less) auto } |
|
360 |
ultimately have "expectation X \<in> I" |
|
361 |
by (elim disjE) (auto simp: subset_eq) |
|
362 |
moreover |
|
363 |
{ fix y assume y: "y \<in> I" |
|
364 |
with q(2) `open I` have "Sup ((\<lambda>x. q x + ?F x * (y - x)) ` I) = q y" |
|
365 |
by (auto intro!: Sup_eq_maximum convex_le_Inf_differential image_eqI[OF _ y] simp: interior_open) } |
|
366 |
ultimately have "q (expectation X) = Sup ((\<lambda>x. q x + ?F x * (expectation X - x)) ` I)" |
|
367 |
by simp |
|
368 |
also have "\<dots> \<le> expectation (\<lambda>w. q (X w))" |
|
369 |
proof (rule Sup_least) |
|
370 |
show "(\<lambda>x. q x + ?F x * (expectation X - x)) ` I \<noteq> {}" |
|
371 |
using `I \<noteq> {}` by auto |
|
372 |
next |
|
373 |
fix k assume "k \<in> (\<lambda>x. q x + ?F x * (expectation X - x)) ` I" |
|
374 |
then guess x .. note x = this |
|
375 |
have "q x + ?F x * (expectation X - x) = expectation (\<lambda>w. q x + ?F x * (X w - x))" |
|
47694 | 376 |
using prob_space by (simp add: X) |
43339 | 377 |
also have "\<dots> \<le> expectation (\<lambda>w. q (X w))" |
378 |
using `x \<in> I` `open I` X(2) |
|
49786 | 379 |
apply (intro integral_mono_AE integral_add integral_cmult integral_diff |
380 |
lebesgue_integral_const X q) |
|
381 |
apply (elim eventually_elim1) |
|
382 |
apply (intro convex_le_Inf_differential) |
|
383 |
apply (auto simp: interior_open q) |
|
384 |
done |
|
43339 | 385 |
finally show "k \<le> expectation (\<lambda>w. q (X w))" using x by auto |
386 |
qed |
|
387 |
finally show "q (expectation X) \<le> expectation (\<lambda>x. q (X x))" . |
|
388 |
qed |
|
389 |
||
40859 | 390 |
lemma (in prob_space) prob_x_eq_1_imp_prob_y_eq_0: |
35582 | 391 |
assumes "{x} \<in> events" |
38656 | 392 |
assumes "prob {x} = 1" |
35582 | 393 |
assumes "{y} \<in> events" |
394 |
assumes "y \<noteq> x" |
|
395 |
shows "prob {y} = 0" |
|
396 |
using prob_one_inter[of "{y}" "{x}"] assms by auto |
|
397 |
||
40859 | 398 |
lemma (in prob_space) joint_distribution_Times_le_fst: |
47694 | 399 |
"random_variable MX X \<Longrightarrow> random_variable MY Y \<Longrightarrow> A \<in> sets MX \<Longrightarrow> B \<in> sets MY |
400 |
\<Longrightarrow> emeasure (distr M (MX \<Otimes>\<^isub>M MY) (\<lambda>x. (X x, Y x))) (A \<times> B) \<le> emeasure (distr M MX X) A" |
|
401 |
by (auto simp: emeasure_distr measurable_pair_iff comp_def intro!: emeasure_mono measurable_sets) |
|
40859 | 402 |
|
403 |
lemma (in prob_space) joint_distribution_Times_le_snd: |
|
47694 | 404 |
"random_variable MX X \<Longrightarrow> random_variable MY Y \<Longrightarrow> A \<in> sets MX \<Longrightarrow> B \<in> sets MY |
405 |
\<Longrightarrow> emeasure (distr M (MX \<Otimes>\<^isub>M MY) (\<lambda>x. (X x, Y x))) (A \<times> B) \<le> emeasure (distr M MY Y) B" |
|
406 |
by (auto simp: emeasure_distr measurable_pair_iff comp_def intro!: emeasure_mono measurable_sets) |
|
40859 | 407 |
|
45777
c36637603821
remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset
|
408 |
locale pair_prob_space = pair_sigma_finite M1 M2 + M1: prob_space M1 + M2: prob_space M2 for M1 M2 |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
409 |
|
47694 | 410 |
sublocale pair_prob_space \<subseteq> P: prob_space "M1 \<Otimes>\<^isub>M M2" |
45777
c36637603821
remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset
|
411 |
proof |
47694 | 412 |
show "emeasure (M1 \<Otimes>\<^isub>M M2) (space (M1 \<Otimes>\<^isub>M M2)) = 1" |
49776 | 413 |
by (simp add: M2.emeasure_pair_measure_Times M1.emeasure_space_1 M2.emeasure_space_1 space_pair_measure) |
45777
c36637603821
remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset
|
414 |
qed |
40859 | 415 |
|
47694 | 416 |
locale product_prob_space = product_sigma_finite M for M :: "'i \<Rightarrow> 'a measure" + |
45777
c36637603821
remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset
|
417 |
fixes I :: "'i set" |
c36637603821
remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset
|
418 |
assumes prob_space: "\<And>i. prob_space (M i)" |
42988 | 419 |
|
45777
c36637603821
remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset
|
420 |
sublocale product_prob_space \<subseteq> M: prob_space "M i" for i |
42988 | 421 |
by (rule prob_space) |
422 |
||
45777
c36637603821
remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset
|
423 |
locale finite_product_prob_space = finite_product_sigma_finite M I + product_prob_space M I for M I |
42988 | 424 |
|
425 |
sublocale finite_product_prob_space \<subseteq> prob_space "\<Pi>\<^isub>M i\<in>I. M i" |
|
45777
c36637603821
remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset
|
426 |
proof |
47694 | 427 |
show "emeasure (\<Pi>\<^isub>M i\<in>I. M i) (space (\<Pi>\<^isub>M i\<in>I. M i)) = 1" |
428 |
by (simp add: measure_times M.emeasure_space_1 setprod_1 space_PiM) |
|
45777
c36637603821
remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset
|
429 |
qed |
42988 | 430 |
|
431 |
lemma (in finite_product_prob_space) prob_times: |
|
432 |
assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> sets (M i)" |
|
433 |
shows "prob (\<Pi>\<^isub>E i\<in>I. X i) = (\<Prod>i\<in>I. M.prob i (X i))" |
|
434 |
proof - |
|
47694 | 435 |
have "ereal (measure (\<Pi>\<^isub>M i\<in>I. M i) (\<Pi>\<^isub>E i\<in>I. X i)) = emeasure (\<Pi>\<^isub>M i\<in>I. M i) (\<Pi>\<^isub>E i\<in>I. X i)" |
436 |
using X by (simp add: emeasure_eq_measure) |
|
437 |
also have "\<dots> = (\<Prod>i\<in>I. emeasure (M i) (X i))" |
|
42988 | 438 |
using measure_times X by simp |
47694 | 439 |
also have "\<dots> = ereal (\<Prod>i\<in>I. measure (M i) (X i))" |
440 |
using X by (simp add: M.emeasure_eq_measure setprod_ereal) |
|
42859
d9dfc733f25c
add product of probability spaces with finite cardinality
hoelzl
parents:
42858
diff
changeset
|
441 |
finally show ?thesis by simp |
d9dfc733f25c
add product of probability spaces with finite cardinality
hoelzl
parents:
42858
diff
changeset
|
442 |
qed |
d9dfc733f25c
add product of probability spaces with finite cardinality
hoelzl
parents:
42858
diff
changeset
|
443 |
|
47694 | 444 |
section {* Distributions *} |
42892 | 445 |
|
47694 | 446 |
definition "distributed M N X f \<longleftrightarrow> distr M N X = density N f \<and> |
447 |
f \<in> borel_measurable N \<and> (AE x in N. 0 \<le> f x) \<and> X \<in> measurable M N" |
|
36624 | 448 |
|
47694 | 449 |
lemma |
450 |
shows distributed_distr_eq_density: "distributed M N X f \<Longrightarrow> distr M N X = density N f" |
|
451 |
and distributed_measurable: "distributed M N X f \<Longrightarrow> X \<in> measurable M N" |
|
452 |
and distributed_borel_measurable: "distributed M N X f \<Longrightarrow> f \<in> borel_measurable N" |
|
453 |
and distributed_AE: "distributed M N X f \<Longrightarrow> (AE x in N. 0 \<le> f x)" |
|
454 |
by (simp_all add: distributed_def) |
|
39097 | 455 |
|
47694 | 456 |
lemma |
457 |
shows distributed_real_measurable: "distributed M N X (\<lambda>x. ereal (f x)) \<Longrightarrow> f \<in> borel_measurable N" |
|
458 |
and distributed_real_AE: "distributed M N X (\<lambda>x. ereal (f x)) \<Longrightarrow> (AE x in N. 0 \<le> f x)" |
|
459 |
by (simp_all add: distributed_def borel_measurable_ereal_iff) |
|
35977 | 460 |
|
47694 | 461 |
lemma distributed_count_space: |
462 |
assumes X: "distributed M (count_space A) X P" and a: "a \<in> A" and A: "finite A" |
|
463 |
shows "P a = emeasure M (X -` {a} \<inter> space M)" |
|
39097 | 464 |
proof - |
47694 | 465 |
have "emeasure M (X -` {a} \<inter> space M) = emeasure (distr M (count_space A) X) {a}" |
466 |
using X a A by (simp add: distributed_measurable emeasure_distr) |
|
467 |
also have "\<dots> = emeasure (density (count_space A) P) {a}" |
|
468 |
using X by (simp add: distributed_distr_eq_density) |
|
469 |
also have "\<dots> = (\<integral>\<^isup>+x. P a * indicator {a} x \<partial>count_space A)" |
|
470 |
using X a by (auto simp add: emeasure_density distributed_def indicator_def intro!: positive_integral_cong) |
|
471 |
also have "\<dots> = P a" |
|
472 |
using X a by (subst positive_integral_cmult_indicator) (auto simp: distributed_def one_ereal_def[symmetric] AE_count_space) |
|
473 |
finally show ?thesis .. |
|
39092 | 474 |
qed |
35977 | 475 |
|
47694 | 476 |
lemma distributed_cong_density: |
477 |
"(AE x in N. f x = g x) \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> f \<in> borel_measurable N \<Longrightarrow> |
|
478 |
distributed M N X f \<longleftrightarrow> distributed M N X g" |
|
479 |
by (auto simp: distributed_def intro!: density_cong) |
|
480 |
||
481 |
lemma subdensity: |
|
482 |
assumes T: "T \<in> measurable P Q" |
|
483 |
assumes f: "distributed M P X f" |
|
484 |
assumes g: "distributed M Q Y g" |
|
485 |
assumes Y: "Y = T \<circ> X" |
|
486 |
shows "AE x in P. g (T x) = 0 \<longrightarrow> f x = 0" |
|
487 |
proof - |
|
488 |
have "{x\<in>space Q. g x = 0} \<in> null_sets (distr M Q (T \<circ> X))" |
|
489 |
using g Y by (auto simp: null_sets_density_iff distributed_def) |
|
490 |
also have "distr M Q (T \<circ> X) = distr (distr M P X) Q T" |
|
491 |
using T f[THEN distributed_measurable] by (rule distr_distr[symmetric]) |
|
492 |
finally have "T -` {x\<in>space Q. g x = 0} \<inter> space P \<in> null_sets (distr M P X)" |
|
493 |
using T by (subst (asm) null_sets_distr_iff) auto |
|
494 |
also have "T -` {x\<in>space Q. g x = 0} \<inter> space P = {x\<in>space P. g (T x) = 0}" |
|
495 |
using T by (auto dest: measurable_space) |
|
496 |
finally show ?thesis |
|
497 |
using f g by (auto simp add: null_sets_density_iff distributed_def) |
|
35977 | 498 |
qed |
499 |
||
47694 | 500 |
lemma subdensity_real: |
501 |
fixes g :: "'a \<Rightarrow> real" and f :: "'b \<Rightarrow> real" |
|
502 |
assumes T: "T \<in> measurable P Q" |
|
503 |
assumes f: "distributed M P X f" |
|
504 |
assumes g: "distributed M Q Y g" |
|
505 |
assumes Y: "Y = T \<circ> X" |
|
506 |
shows "AE x in P. g (T x) = 0 \<longrightarrow> f x = 0" |
|
507 |
using subdensity[OF T, of M X "\<lambda>x. ereal (f x)" Y "\<lambda>x. ereal (g x)"] assms by auto |
|
508 |
||
509 |
lemma distributed_integral: |
|
510 |
"distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> (\<integral>x. f x * g x \<partial>N) = (\<integral>x. g (X x) \<partial>M)" |
|
511 |
by (auto simp: distributed_real_measurable distributed_real_AE distributed_measurable |
|
512 |
distributed_distr_eq_density[symmetric] integral_density[symmetric] integral_distr) |
|
513 |
||
514 |
lemma distributed_transform_integral: |
|
515 |
assumes Px: "distributed M N X Px" |
|
516 |
assumes "distributed M P Y Py" |
|
517 |
assumes Y: "Y = T \<circ> X" and T: "T \<in> measurable N P" and f: "f \<in> borel_measurable P" |
|
518 |
shows "(\<integral>x. Py x * f x \<partial>P) = (\<integral>x. Px x * f (T x) \<partial>N)" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
519 |
proof - |
47694 | 520 |
have "(\<integral>x. Py x * f x \<partial>P) = (\<integral>x. f (Y x) \<partial>M)" |
521 |
by (rule distributed_integral) fact+ |
|
522 |
also have "\<dots> = (\<integral>x. f (T (X x)) \<partial>M)" |
|
523 |
using Y by simp |
|
524 |
also have "\<dots> = (\<integral>x. Px x * f (T x) \<partial>N)" |
|
525 |
using measurable_comp[OF T f] Px by (intro distributed_integral[symmetric]) (auto simp: comp_def) |
|
45777
c36637603821
remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset
|
526 |
finally show ?thesis . |
39092 | 527 |
qed |
36624 | 528 |
|
47694 | 529 |
lemma distributed_marginal_eq_joint: |
530 |
assumes T: "sigma_finite_measure T" |
|
531 |
assumes S: "sigma_finite_measure S" |
|
532 |
assumes Px: "distributed M S X Px" |
|
533 |
assumes Py: "distributed M T Y Py" |
|
534 |
assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy" |
|
535 |
shows "AE y in T. Py y = (\<integral>\<^isup>+x. Pxy (x, y) \<partial>S)" |
|
536 |
proof (rule sigma_finite_measure.density_unique[OF T]) |
|
537 |
interpret ST: pair_sigma_finite S T using S T unfolding pair_sigma_finite_def by simp |
|
538 |
show "Py \<in> borel_measurable T" "AE y in T. 0 \<le> Py y" |
|
539 |
"(\<lambda>x. \<integral>\<^isup>+ xa. Pxy (xa, x) \<partial>S) \<in> borel_measurable T" "AE y in T. 0 \<le> \<integral>\<^isup>+ x. Pxy (x, y) \<partial>S" |
|
540 |
using Pxy[THEN distributed_borel_measurable] |
|
541 |
by (auto intro!: Py[THEN distributed_borel_measurable] Py[THEN distributed_AE] |
|
542 |
ST.positive_integral_snd_measurable' positive_integral_positive) |
|
543 |
||
544 |
show "density T Py = density T (\<lambda>x. \<integral>\<^isup>+ xa. Pxy (xa, x) \<partial>S)" |
|
545 |
proof (rule measure_eqI) |
|
546 |
fix A assume A: "A \<in> sets (density T Py)" |
|
547 |
have *: "\<And>x y. x \<in> space S \<Longrightarrow> indicator (space S \<times> A) (x, y) = indicator A y" |
|
548 |
by (auto simp: indicator_def) |
|
549 |
have "emeasure (density T Py) A = emeasure (distr M T Y) A" |
|
550 |
unfolding Py[THEN distributed_distr_eq_density] .. |
|
551 |
also have "\<dots> = emeasure (distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))) (space S \<times> A)" |
|
552 |
using A Px Py Pxy |
|
553 |
by (subst (1 2) emeasure_distr) |
|
554 |
(auto dest: measurable_space distributed_measurable intro!: arg_cong[where f="emeasure M"]) |
|
555 |
also have "\<dots> = emeasure (density (S \<Otimes>\<^isub>M T) Pxy) (space S \<times> A)" |
|
556 |
unfolding Pxy[THEN distributed_distr_eq_density] .. |
|
557 |
also have "\<dots> = (\<integral>\<^isup>+ x. Pxy x * indicator (space S \<times> A) x \<partial>(S \<Otimes>\<^isub>M T))" |
|
558 |
using A Pxy by (simp add: emeasure_density distributed_borel_measurable) |
|
559 |
also have "\<dots> = (\<integral>\<^isup>+y. \<integral>\<^isup>+x. Pxy (x, y) * indicator (space S \<times> A) (x, y) \<partial>S \<partial>T)" |
|
560 |
using A Pxy |
|
561 |
by (subst ST.positive_integral_snd_measurable) (simp_all add: emeasure_density distributed_borel_measurable) |
|
562 |
also have "\<dots> = (\<integral>\<^isup>+y. (\<integral>\<^isup>+x. Pxy (x, y) \<partial>S) * indicator A y \<partial>T)" |
|
49783 | 563 |
using measurable_comp[OF measurable_Pair1[OF measurable_ident] distributed_borel_measurable[OF Pxy]] |
47694 | 564 |
using distributed_borel_measurable[OF Pxy] distributed_AE[OF Pxy, THEN ST.AE_pair] |
565 |
by (subst (asm) ST.AE_commute) (auto intro!: positive_integral_cong_AE positive_integral_multc cong: positive_integral_cong simp: * comp_def) |
|
566 |
also have "\<dots> = emeasure (density T (\<lambda>x. \<integral>\<^isup>+ xa. Pxy (xa, x) \<partial>S)) A" |
|
567 |
using A by (intro emeasure_density[symmetric]) (auto intro!: ST.positive_integral_snd_measurable' Pxy[THEN distributed_borel_measurable]) |
|
568 |
finally show "emeasure (density T Py) A = emeasure (density T (\<lambda>x. \<integral>\<^isup>+ xa. Pxy (xa, x) \<partial>S)) A" . |
|
569 |
qed simp |
|
36624 | 570 |
qed |
571 |
||
47694 | 572 |
lemma (in prob_space) distr_marginal1: |
573 |
fixes Pxy :: "('b \<times> 'c) \<Rightarrow> real" |
|
574 |
assumes "sigma_finite_measure S" "sigma_finite_measure T" |
|
575 |
assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy" |
|
576 |
defines "Px \<equiv> \<lambda>x. real (\<integral>\<^isup>+z. Pxy (x, z) \<partial>T)" |
|
577 |
shows "distributed M S X Px" |
|
578 |
unfolding distributed_def |
|
579 |
proof safe |
|
580 |
interpret S: sigma_finite_measure S by fact |
|
581 |
interpret T: sigma_finite_measure T by fact |
|
582 |
interpret ST: pair_sigma_finite S T by default |
|
583 |
||
584 |
have XY: "(\<lambda>x. (X x, Y x)) \<in> measurable M (S \<Otimes>\<^isub>M T)" |
|
585 |
using Pxy by (rule distributed_measurable) |
|
586 |
then show X: "X \<in> measurable M S" |
|
587 |
unfolding measurable_pair_iff by (simp add: comp_def) |
|
588 |
from XY have Y: "Y \<in> measurable M T" |
|
589 |
unfolding measurable_pair_iff by (simp add: comp_def) |
|
590 |
||
591 |
from Pxy show borel: "(\<lambda>x. ereal (Px x)) \<in> borel_measurable S" |
|
592 |
by (auto intro!: ST.positive_integral_fst_measurable borel_measurable_real_of_ereal dest!: distributed_real_measurable simp: Px_def) |
|
39097 | 593 |
|
47694 | 594 |
interpret Pxy: prob_space "distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))" |
595 |
using XY by (rule prob_space_distr) |
|
596 |
have "(\<integral>\<^isup>+ x. max 0 (ereal (- Pxy x)) \<partial>(S \<Otimes>\<^isub>M T)) = (\<integral>\<^isup>+ x. 0 \<partial>(S \<Otimes>\<^isub>M T))" |
|
597 |
using Pxy |
|
598 |
by (intro positive_integral_cong_AE) (auto simp: max_def dest: distributed_real_measurable distributed_real_AE) |
|
599 |
then have Pxy_integrable: "integrable (S \<Otimes>\<^isub>M T) Pxy" |
|
600 |
using Pxy Pxy.emeasure_space_1 |
|
601 |
by (simp add: integrable_def emeasure_density positive_integral_max_0 distributed_def borel_measurable_ereal_iff cong: positive_integral_cong) |
|
602 |
||
603 |
show "distr M S X = density S Px" |
|
604 |
proof (rule measure_eqI) |
|
605 |
fix A assume A: "A \<in> sets (distr M S X)" |
|
606 |
with X Y XY have "emeasure (distr M S X) A = emeasure (distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))) (A \<times> space T)" |
|
607 |
by (auto simp add: emeasure_distr |
|
608 |
intro!: arg_cong[where f="emeasure M"] dest: measurable_space) |
|
609 |
also have "\<dots> = emeasure (density (S \<Otimes>\<^isub>M T) Pxy) (A \<times> space T)" |
|
610 |
using Pxy by (simp add: distributed_def) |
|
611 |
also have "\<dots> = \<integral>\<^isup>+ x. \<integral>\<^isup>+ y. ereal (Pxy (x, y)) * indicator (A \<times> space T) (x, y) \<partial>T \<partial>S" |
|
612 |
using A borel Pxy |
|
613 |
by (simp add: emeasure_density ST.positive_integral_fst_measurable(2)[symmetric] distributed_def) |
|
614 |
also have "\<dots> = \<integral>\<^isup>+ x. ereal (Px x) * indicator A x \<partial>S" |
|
615 |
apply (rule positive_integral_cong_AE) |
|
616 |
using Pxy[THEN distributed_real_AE, THEN ST.AE_pair] ST.integrable_fst_measurable(1)[OF Pxy_integrable] AE_space |
|
617 |
proof eventually_elim |
|
618 |
fix x assume "x \<in> space S" "AE y in T. 0 \<le> Pxy (x, y)" and i: "integrable T (\<lambda>y. Pxy (x, y))" |
|
619 |
moreover have eq: "\<And>y. y \<in> space T \<Longrightarrow> indicator (A \<times> space T) (x, y) = indicator A x" |
|
620 |
by (auto simp: indicator_def) |
|
621 |
ultimately have "(\<integral>\<^isup>+ y. ereal (Pxy (x, y)) * indicator (A \<times> space T) (x, y) \<partial>T) = |
|
622 |
(\<integral>\<^isup>+ y. ereal (Pxy (x, y)) \<partial>T) * indicator A x" |
|
623 |
using Pxy[THEN distributed_real_measurable] by (simp add: eq positive_integral_multc measurable_Pair2 cong: positive_integral_cong) |
|
624 |
also have "(\<integral>\<^isup>+ y. ereal (Pxy (x, y)) \<partial>T) = Px x" |
|
625 |
using i by (simp add: Px_def ereal_real integrable_def positive_integral_positive) |
|
626 |
finally show "(\<integral>\<^isup>+ y. ereal (Pxy (x, y)) * indicator (A \<times> space T) (x, y) \<partial>T) = ereal (Px x) * indicator A x" . |
|
627 |
qed |
|
628 |
finally show "emeasure (distr M S X) A = emeasure (density S Px) A" |
|
629 |
using A borel Pxy by (simp add: emeasure_density) |
|
630 |
qed simp |
|
631 |
||
632 |
show "AE x in S. 0 \<le> ereal (Px x)" |
|
633 |
by (simp add: Px_def positive_integral_positive real_of_ereal_pos) |
|
40859 | 634 |
qed |
635 |
||
47694 | 636 |
definition |
637 |
"simple_distributed M X f \<longleftrightarrow> distributed M (count_space (X`space M)) X (\<lambda>x. ereal (f x)) \<and> |
|
638 |
finite (X`space M)" |
|
42902 | 639 |
|
47694 | 640 |
lemma simple_distributed: |
641 |
"simple_distributed M X Px \<Longrightarrow> distributed M (count_space (X`space M)) X Px" |
|
642 |
unfolding simple_distributed_def by auto |
|
42902 | 643 |
|
47694 | 644 |
lemma simple_distributed_finite[dest]: "simple_distributed M X P \<Longrightarrow> finite (X`space M)" |
645 |
by (simp add: simple_distributed_def) |
|
42902 | 646 |
|
47694 | 647 |
lemma (in prob_space) distributed_simple_function_superset: |
648 |
assumes X: "simple_function M X" "\<And>x. x \<in> X ` space M \<Longrightarrow> P x = measure M (X -` {x} \<inter> space M)" |
|
649 |
assumes A: "X`space M \<subseteq> A" "finite A" |
|
650 |
defines "S \<equiv> count_space A" and "P' \<equiv> (\<lambda>x. if x \<in> X`space M then P x else 0)" |
|
651 |
shows "distributed M S X P'" |
|
652 |
unfolding distributed_def |
|
653 |
proof safe |
|
654 |
show "(\<lambda>x. ereal (P' x)) \<in> borel_measurable S" unfolding S_def by simp |
|
655 |
show "AE x in S. 0 \<le> ereal (P' x)" |
|
656 |
using X by (auto simp: S_def P'_def simple_distributed_def intro!: measure_nonneg) |
|
657 |
show "distr M S X = density S P'" |
|
658 |
proof (rule measure_eqI_finite) |
|
659 |
show "sets (distr M S X) = Pow A" "sets (density S P') = Pow A" |
|
660 |
using A unfolding S_def by auto |
|
661 |
show "finite A" by fact |
|
662 |
fix a assume a: "a \<in> A" |
|
663 |
then have "a \<notin> X`space M \<Longrightarrow> X -` {a} \<inter> space M = {}" by auto |
|
664 |
with A a X have "emeasure (distr M S X) {a} = P' a" |
|
665 |
by (subst emeasure_distr) |
|
666 |
(auto simp add: S_def P'_def simple_functionD emeasure_eq_measure |
|
667 |
intro!: arg_cong[where f=prob]) |
|
668 |
also have "\<dots> = (\<integral>\<^isup>+x. ereal (P' a) * indicator {a} x \<partial>S)" |
|
669 |
using A X a |
|
670 |
by (subst positive_integral_cmult_indicator) |
|
671 |
(auto simp: S_def P'_def simple_distributed_def simple_functionD measure_nonneg) |
|
672 |
also have "\<dots> = (\<integral>\<^isup>+x. ereal (P' x) * indicator {a} x \<partial>S)" |
|
673 |
by (auto simp: indicator_def intro!: positive_integral_cong) |
|
674 |
also have "\<dots> = emeasure (density S P') {a}" |
|
675 |
using a A by (intro emeasure_density[symmetric]) (auto simp: S_def) |
|
676 |
finally show "emeasure (distr M S X) {a} = emeasure (density S P') {a}" . |
|
677 |
qed |
|
678 |
show "random_variable S X" |
|
679 |
using X(1) A by (auto simp: measurable_def simple_functionD S_def) |
|
680 |
qed |
|
42902 | 681 |
|
47694 | 682 |
lemma (in prob_space) simple_distributedI: |
683 |
assumes X: "simple_function M X" "\<And>x. x \<in> X ` space M \<Longrightarrow> P x = measure M (X -` {x} \<inter> space M)" |
|
684 |
shows "simple_distributed M X P" |
|
685 |
unfolding simple_distributed_def |
|
686 |
proof |
|
687 |
have "distributed M (count_space (X ` space M)) X (\<lambda>x. ereal (if x \<in> X`space M then P x else 0))" |
|
688 |
(is "?A") |
|
689 |
using simple_functionD[OF X(1)] by (intro distributed_simple_function_superset[OF X]) auto |
|
690 |
also have "?A \<longleftrightarrow> distributed M (count_space (X ` space M)) X (\<lambda>x. ereal (P x))" |
|
691 |
by (rule distributed_cong_density) auto |
|
692 |
finally show "\<dots>" . |
|
693 |
qed (rule simple_functionD[OF X(1)]) |
|
694 |
||
695 |
lemma simple_distributed_joint_finite: |
|
696 |
assumes X: "simple_distributed M (\<lambda>x. (X x, Y x)) Px" |
|
697 |
shows "finite (X ` space M)" "finite (Y ` space M)" |
|
42902 | 698 |
proof - |
47694 | 699 |
have "finite ((\<lambda>x. (X x, Y x)) ` space M)" |
700 |
using X by (auto simp: simple_distributed_def simple_functionD) |
|
701 |
then have "finite (fst ` (\<lambda>x. (X x, Y x)) ` space M)" "finite (snd ` (\<lambda>x. (X x, Y x)) ` space M)" |
|
702 |
by auto |
|
703 |
then show fin: "finite (X ` space M)" "finite (Y ` space M)" |
|
704 |
by (auto simp: image_image) |
|
705 |
qed |
|
706 |
||
707 |
lemma simple_distributed_joint2_finite: |
|
708 |
assumes X: "simple_distributed M (\<lambda>x. (X x, Y x, Z x)) Px" |
|
709 |
shows "finite (X ` space M)" "finite (Y ` space M)" "finite (Z ` space M)" |
|
710 |
proof - |
|
711 |
have "finite ((\<lambda>x. (X x, Y x, Z x)) ` space M)" |
|
712 |
using X by (auto simp: simple_distributed_def simple_functionD) |
|
713 |
then have "finite (fst ` (\<lambda>x. (X x, Y x, Z x)) ` space M)" |
|
714 |
"finite ((fst \<circ> snd) ` (\<lambda>x. (X x, Y x, Z x)) ` space M)" |
|
715 |
"finite ((snd \<circ> snd) ` (\<lambda>x. (X x, Y x, Z x)) ` space M)" |
|
716 |
by auto |
|
717 |
then show fin: "finite (X ` space M)" "finite (Y ` space M)" "finite (Z ` space M)" |
|
718 |
by (auto simp: image_image) |
|
42902 | 719 |
qed |
720 |
||
47694 | 721 |
lemma simple_distributed_simple_function: |
722 |
"simple_distributed M X Px \<Longrightarrow> simple_function M X" |
|
723 |
unfolding simple_distributed_def distributed_def |
|
724 |
by (auto simp: simple_function_def) |
|
725 |
||
726 |
lemma simple_distributed_measure: |
|
727 |
"simple_distributed M X P \<Longrightarrow> a \<in> X`space M \<Longrightarrow> P a = measure M (X -` {a} \<inter> space M)" |
|
728 |
using distributed_count_space[of M "X`space M" X P a, symmetric] |
|
729 |
by (auto simp: simple_distributed_def measure_def) |
|
730 |
||
731 |
lemma simple_distributed_nonneg: "simple_distributed M X f \<Longrightarrow> x \<in> space M \<Longrightarrow> 0 \<le> f (X x)" |
|
732 |
by (auto simp: simple_distributed_measure measure_nonneg) |
|
42860 | 733 |
|
47694 | 734 |
lemma (in prob_space) simple_distributed_joint: |
735 |
assumes X: "simple_distributed M (\<lambda>x. (X x, Y x)) Px" |
|
736 |
defines "S \<equiv> count_space (X`space M) \<Otimes>\<^isub>M count_space (Y`space M)" |
|
737 |
defines "P \<equiv> (\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x))`space M then Px x else 0)" |
|
738 |
shows "distributed M S (\<lambda>x. (X x, Y x)) P" |
|
739 |
proof - |
|
740 |
from simple_distributed_joint_finite[OF X, simp] |
|
741 |
have S_eq: "S = count_space (X`space M \<times> Y`space M)" |
|
742 |
by (simp add: S_def pair_measure_count_space) |
|
743 |
show ?thesis |
|
744 |
unfolding S_eq P_def |
|
745 |
proof (rule distributed_simple_function_superset) |
|
746 |
show "simple_function M (\<lambda>x. (X x, Y x))" |
|
747 |
using X by (rule simple_distributed_simple_function) |
|
748 |
fix x assume "x \<in> (\<lambda>x. (X x, Y x)) ` space M" |
|
749 |
from simple_distributed_measure[OF X this] |
|
750 |
show "Px x = prob ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M)" . |
|
751 |
qed auto |
|
752 |
qed |
|
42860 | 753 |
|
47694 | 754 |
lemma (in prob_space) simple_distributed_joint2: |
755 |
assumes X: "simple_distributed M (\<lambda>x. (X x, Y x, Z x)) Px" |
|
756 |
defines "S \<equiv> count_space (X`space M) \<Otimes>\<^isub>M count_space (Y`space M) \<Otimes>\<^isub>M count_space (Z`space M)" |
|
757 |
defines "P \<equiv> (\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x, Z x))`space M then Px x else 0)" |
|
758 |
shows "distributed M S (\<lambda>x. (X x, Y x, Z x)) P" |
|
759 |
proof - |
|
760 |
from simple_distributed_joint2_finite[OF X, simp] |
|
761 |
have S_eq: "S = count_space (X`space M \<times> Y`space M \<times> Z`space M)" |
|
762 |
by (simp add: S_def pair_measure_count_space) |
|
763 |
show ?thesis |
|
764 |
unfolding S_eq P_def |
|
765 |
proof (rule distributed_simple_function_superset) |
|
766 |
show "simple_function M (\<lambda>x. (X x, Y x, Z x))" |
|
767 |
using X by (rule simple_distributed_simple_function) |
|
768 |
fix x assume "x \<in> (\<lambda>x. (X x, Y x, Z x)) ` space M" |
|
769 |
from simple_distributed_measure[OF X this] |
|
770 |
show "Px x = prob ((\<lambda>x. (X x, Y x, Z x)) -` {x} \<inter> space M)" . |
|
771 |
qed auto |
|
772 |
qed |
|
773 |
||
774 |
lemma (in prob_space) simple_distributed_setsum_space: |
|
775 |
assumes X: "simple_distributed M X f" |
|
776 |
shows "setsum f (X`space M) = 1" |
|
777 |
proof - |
|
778 |
from X have "setsum f (X`space M) = prob (\<Union>i\<in>X`space M. X -` {i} \<inter> space M)" |
|
779 |
by (subst finite_measure_finite_Union) |
|
780 |
(auto simp add: disjoint_family_on_def simple_distributed_measure simple_distributed_simple_function simple_functionD |
|
781 |
intro!: setsum_cong arg_cong[where f="prob"]) |
|
782 |
also have "\<dots> = prob (space M)" |
|
783 |
by (auto intro!: arg_cong[where f=prob]) |
|
784 |
finally show ?thesis |
|
785 |
using emeasure_space_1 by (simp add: emeasure_eq_measure one_ereal_def) |
|
786 |
qed |
|
42860 | 787 |
|
47694 | 788 |
lemma (in prob_space) distributed_marginal_eq_joint_simple: |
789 |
assumes Px: "simple_function M X" |
|
790 |
assumes Py: "simple_distributed M Y Py" |
|
791 |
assumes Pxy: "simple_distributed M (\<lambda>x. (X x, Y x)) Pxy" |
|
792 |
assumes y: "y \<in> Y`space M" |
|
793 |
shows "Py y = (\<Sum>x\<in>X`space M. if (x, y) \<in> (\<lambda>x. (X x, Y x)) ` space M then Pxy (x, y) else 0)" |
|
794 |
proof - |
|
795 |
note Px = simple_distributedI[OF Px refl] |
|
796 |
have *: "\<And>f A. setsum (\<lambda>x. max 0 (ereal (f x))) A = ereal (setsum (\<lambda>x. max 0 (f x)) A)" |
|
797 |
by (simp add: setsum_ereal[symmetric] zero_ereal_def) |
|
798 |
from distributed_marginal_eq_joint[OF sigma_finite_measure_count_space_finite sigma_finite_measure_count_space_finite |
|
799 |
simple_distributed[OF Px] simple_distributed[OF Py] simple_distributed_joint[OF Pxy], |
|
800 |
OF Py[THEN simple_distributed_finite] Px[THEN simple_distributed_finite]] |
|
801 |
y Px[THEN simple_distributed_finite] Py[THEN simple_distributed_finite] |
|
802 |
Pxy[THEN simple_distributed, THEN distributed_real_AE] |
|
803 |
show ?thesis |
|
804 |
unfolding AE_count_space |
|
805 |
apply (elim ballE[where x=y]) |
|
806 |
apply (auto simp add: positive_integral_count_space_finite * intro!: setsum_cong split: split_max) |
|
807 |
done |
|
808 |
qed |
|
42860 | 809 |
|
47694 | 810 |
|
811 |
lemma prob_space_uniform_measure: |
|
812 |
assumes A: "emeasure M A \<noteq> 0" "emeasure M A \<noteq> \<infinity>" |
|
813 |
shows "prob_space (uniform_measure M A)" |
|
814 |
proof |
|
815 |
show "emeasure (uniform_measure M A) (space (uniform_measure M A)) = 1" |
|
816 |
using emeasure_uniform_measure[OF emeasure_neq_0_sets[OF A(1)], of "space M"] |
|
817 |
using sets_into_space[OF emeasure_neq_0_sets[OF A(1)]] A |
|
818 |
by (simp add: Int_absorb2 emeasure_nonneg) |
|
819 |
qed |
|
820 |
||
821 |
lemma prob_space_uniform_count_measure: "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> prob_space (uniform_count_measure A)" |
|
822 |
by default (auto simp: emeasure_uniform_count_measure space_uniform_count_measure one_ereal_def) |
|
42860 | 823 |
|
35582 | 824 |
end |