1 (* Title: HOL/Probability/Probability_Space.thy |
|
2 Author: Johannes Hölzl, TU München |
|
3 Author: Armin Heller, TU München |
|
4 *) |
|
5 |
|
6 header {*Probability spaces*} |
|
7 |
|
8 theory Probability_Space |
|
9 imports Lebesgue_Integration Radon_Nikodym Finite_Product_Measure |
|
10 begin |
|
11 |
|
12 lemma real_of_extreal_inverse[simp]: |
|
13 fixes X :: extreal |
|
14 shows "real (inverse X) = 1 / real X" |
|
15 by (cases X) (auto simp: inverse_eq_divide) |
|
16 |
|
17 lemma real_of_extreal_le_0[simp]: "real (X :: extreal) \<le> 0 \<longleftrightarrow> (X \<le> 0 \<or> X = \<infinity>)" |
|
18 by (cases X) auto |
|
19 |
|
20 lemma abs_real_of_extreal[simp]: "\<bar>real (X :: extreal)\<bar> = real \<bar>X\<bar>" |
|
21 by (cases X) auto |
|
22 |
|
23 lemma zero_less_real_of_extreal: "0 < real X \<longleftrightarrow> (0 < X \<and> X \<noteq> \<infinity>)" |
|
24 by (cases X) auto |
|
25 |
|
26 lemma real_of_extreal_le_1: fixes X :: extreal shows "X \<le> 1 \<Longrightarrow> real X \<le> 1" |
|
27 by (cases X) (auto simp: one_extreal_def) |
|
28 |
|
29 locale prob_space = measure_space + |
|
30 assumes measure_space_1: "measure M (space M) = 1" |
|
31 |
|
32 sublocale prob_space < finite_measure |
|
33 proof |
|
34 from measure_space_1 show "\<mu> (space M) \<noteq> \<infinity>" by simp |
|
35 qed |
|
36 |
|
37 abbreviation (in prob_space) "events \<equiv> sets M" |
|
38 abbreviation (in prob_space) "prob \<equiv> \<mu>'" |
|
39 abbreviation (in prob_space) "prob_preserving \<equiv> measure_preserving" |
|
40 abbreviation (in prob_space) "random_variable M' X \<equiv> sigma_algebra M' \<and> X \<in> measurable M M'" |
|
41 abbreviation (in prob_space) "expectation \<equiv> integral\<^isup>L M" |
|
42 |
|
43 definition (in prob_space) |
|
44 "indep A B \<longleftrightarrow> A \<in> events \<and> B \<in> events \<and> prob (A \<inter> B) = prob A * prob B" |
|
45 |
|
46 definition (in prob_space) |
|
47 "indep_families F G \<longleftrightarrow> (\<forall> A \<in> F. \<forall> B \<in> G. indep A B)" |
|
48 |
|
49 definition (in prob_space) |
|
50 "distribution X A = \<mu>' (X -` A \<inter> space M)" |
|
51 |
|
52 abbreviation (in prob_space) |
|
53 "joint_distribution X Y \<equiv> distribution (\<lambda>x. (X x, Y x))" |
|
54 |
|
55 declare (in finite_measure) positive_measure'[intro, simp] |
|
56 |
|
57 lemma (in prob_space) distribution_cong: |
|
58 assumes "\<And>x. x \<in> space M \<Longrightarrow> X x = Y x" |
|
59 shows "distribution X = distribution Y" |
|
60 unfolding distribution_def fun_eq_iff |
|
61 using assms by (auto intro!: arg_cong[where f="\<mu>'"]) |
|
62 |
|
63 lemma (in prob_space) joint_distribution_cong: |
|
64 assumes "\<And>x. x \<in> space M \<Longrightarrow> X x = X' x" |
|
65 assumes "\<And>x. x \<in> space M \<Longrightarrow> Y x = Y' x" |
|
66 shows "joint_distribution X Y = joint_distribution X' Y'" |
|
67 unfolding distribution_def fun_eq_iff |
|
68 using assms by (auto intro!: arg_cong[where f="\<mu>'"]) |
|
69 |
|
70 lemma (in prob_space) distribution_id[simp]: |
|
71 "N \<in> events \<Longrightarrow> distribution (\<lambda>x. x) N = prob N" |
|
72 by (auto simp: distribution_def intro!: arg_cong[where f=prob]) |
|
73 |
|
74 lemma (in prob_space) prob_space: "prob (space M) = 1" |
|
75 using measure_space_1 unfolding \<mu>'_def by (simp add: one_extreal_def) |
|
76 |
|
77 lemma (in prob_space) prob_le_1[simp, intro]: "prob A \<le> 1" |
|
78 using bounded_measure[of A] by (simp add: prob_space) |
|
79 |
|
80 lemma (in prob_space) distribution_positive[simp, intro]: |
|
81 "0 \<le> distribution X A" unfolding distribution_def by auto |
|
82 |
|
83 lemma (in prob_space) joint_distribution_remove[simp]: |
|
84 "joint_distribution X X {(x, x)} = distribution X {x}" |
|
85 unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>']) |
|
86 |
|
87 lemma (in prob_space) distribution_1: |
|
88 "distribution X A \<le> 1" |
|
89 unfolding distribution_def by simp |
|
90 |
|
91 lemma (in prob_space) prob_compl: |
|
92 assumes A: "A \<in> events" |
|
93 shows "prob (space M - A) = 1 - prob A" |
|
94 using finite_measure_compl[OF A] by (simp add: prob_space) |
|
95 |
|
96 lemma (in prob_space) indep_space: "s \<in> events \<Longrightarrow> indep (space M) s" |
|
97 by (simp add: indep_def prob_space) |
|
98 |
|
99 lemma (in prob_space) prob_space_increasing: "increasing M prob" |
|
100 by (auto intro!: finite_measure_mono simp: increasing_def) |
|
101 |
|
102 lemma (in prob_space) prob_zero_union: |
|
103 assumes "s \<in> events" "t \<in> events" "prob t = 0" |
|
104 shows "prob (s \<union> t) = prob s" |
|
105 using assms |
|
106 proof - |
|
107 have "prob (s \<union> t) \<le> prob s" |
|
108 using finite_measure_subadditive[of s t] assms by auto |
|
109 moreover have "prob (s \<union> t) \<ge> prob s" |
|
110 using assms by (blast intro: finite_measure_mono) |
|
111 ultimately show ?thesis by simp |
|
112 qed |
|
113 |
|
114 lemma (in prob_space) prob_eq_compl: |
|
115 assumes "s \<in> events" "t \<in> events" |
|
116 assumes "prob (space M - s) = prob (space M - t)" |
|
117 shows "prob s = prob t" |
|
118 using assms prob_compl by auto |
|
119 |
|
120 lemma (in prob_space) prob_one_inter: |
|
121 assumes events:"s \<in> events" "t \<in> events" |
|
122 assumes "prob t = 1" |
|
123 shows "prob (s \<inter> t) = prob s" |
|
124 proof - |
|
125 have "prob ((space M - s) \<union> (space M - t)) = prob (space M - s)" |
|
126 using events assms prob_compl[of "t"] by (auto intro!: prob_zero_union) |
|
127 also have "(space M - s) \<union> (space M - t) = space M - (s \<inter> t)" |
|
128 by blast |
|
129 finally show "prob (s \<inter> t) = prob s" |
|
130 using events by (auto intro!: prob_eq_compl[of "s \<inter> t" s]) |
|
131 qed |
|
132 |
|
133 lemma (in prob_space) prob_eq_bigunion_image: |
|
134 assumes "range f \<subseteq> events" "range g \<subseteq> events" |
|
135 assumes "disjoint_family f" "disjoint_family g" |
|
136 assumes "\<And> n :: nat. prob (f n) = prob (g n)" |
|
137 shows "(prob (\<Union> i. f i) = prob (\<Union> i. g i))" |
|
138 using assms |
|
139 proof - |
|
140 have a: "(\<lambda> i. prob (f i)) sums (prob (\<Union> i. f i))" |
|
141 by (rule finite_measure_UNION[OF assms(1,3)]) |
|
142 have b: "(\<lambda> i. prob (g i)) sums (prob (\<Union> i. g i))" |
|
143 by (rule finite_measure_UNION[OF assms(2,4)]) |
|
144 show ?thesis using sums_unique[OF b] sums_unique[OF a] assms by simp |
|
145 qed |
|
146 |
|
147 lemma (in prob_space) prob_countably_zero: |
|
148 assumes "range c \<subseteq> events" |
|
149 assumes "\<And> i. prob (c i) = 0" |
|
150 shows "prob (\<Union> i :: nat. c i) = 0" |
|
151 proof (rule antisym) |
|
152 show "prob (\<Union> i :: nat. c i) \<le> 0" |
|
153 using finite_measure_countably_subadditive[OF assms(1)] |
|
154 by (simp add: assms(2) suminf_zero summable_zero) |
|
155 qed simp |
|
156 |
|
157 lemma (in prob_space) indep_sym: |
|
158 "indep a b \<Longrightarrow> indep b a" |
|
159 unfolding indep_def using Int_commute[of a b] by auto |
|
160 |
|
161 lemma (in prob_space) indep_refl: |
|
162 assumes "a \<in> events" |
|
163 shows "indep a a = (prob a = 0) \<or> (prob a = 1)" |
|
164 using assms unfolding indep_def by auto |
|
165 |
|
166 lemma (in prob_space) prob_equiprobable_finite_unions: |
|
167 assumes "s \<in> events" |
|
168 assumes s_finite: "finite s" "\<And>x. x \<in> s \<Longrightarrow> {x} \<in> events" |
|
169 assumes "\<And> x y. \<lbrakk>x \<in> s; y \<in> s\<rbrakk> \<Longrightarrow> (prob {x} = prob {y})" |
|
170 shows "prob s = real (card s) * prob {SOME x. x \<in> s}" |
|
171 proof (cases "s = {}") |
|
172 case False hence "\<exists> x. x \<in> s" by blast |
|
173 from someI_ex[OF this] assms |
|
174 have prob_some: "\<And> x. x \<in> s \<Longrightarrow> prob {x} = prob {SOME y. y \<in> s}" by blast |
|
175 have "prob s = (\<Sum> x \<in> s. prob {x})" |
|
176 using finite_measure_finite_singleton[OF s_finite] by simp |
|
177 also have "\<dots> = (\<Sum> x \<in> s. prob {SOME y. y \<in> s})" using prob_some by auto |
|
178 also have "\<dots> = real (card s) * prob {(SOME x. x \<in> s)}" |
|
179 using setsum_constant assms by (simp add: real_eq_of_nat) |
|
180 finally show ?thesis by simp |
|
181 qed simp |
|
182 |
|
183 lemma (in prob_space) prob_real_sum_image_fn: |
|
184 assumes "e \<in> events" |
|
185 assumes "\<And> x. x \<in> s \<Longrightarrow> e \<inter> f x \<in> events" |
|
186 assumes "finite s" |
|
187 assumes disjoint: "\<And> x y. \<lbrakk>x \<in> s ; y \<in> s ; x \<noteq> y\<rbrakk> \<Longrightarrow> f x \<inter> f y = {}" |
|
188 assumes upper: "space M \<subseteq> (\<Union> i \<in> s. f i)" |
|
189 shows "prob e = (\<Sum> x \<in> s. prob (e \<inter> f x))" |
|
190 proof - |
|
191 have e: "e = (\<Union> i \<in> s. e \<inter> f i)" |
|
192 using `e \<in> events` sets_into_space upper by blast |
|
193 hence "prob e = prob (\<Union> i \<in> s. e \<inter> f i)" by simp |
|
194 also have "\<dots> = (\<Sum> x \<in> s. prob (e \<inter> f x))" |
|
195 proof (rule finite_measure_finite_Union) |
|
196 show "finite s" by fact |
|
197 show "\<And>i. i \<in> s \<Longrightarrow> e \<inter> f i \<in> events" by fact |
|
198 show "disjoint_family_on (\<lambda>i. e \<inter> f i) s" |
|
199 using disjoint by (auto simp: disjoint_family_on_def) |
|
200 qed |
|
201 finally show ?thesis . |
|
202 qed |
|
203 |
|
204 lemma (in prob_space) distribution_prob_space: |
|
205 assumes "random_variable S X" |
|
206 shows "prob_space (S\<lparr>measure := extreal \<circ> distribution X\<rparr>)" |
|
207 proof - |
|
208 interpret S: measure_space "S\<lparr>measure := extreal \<circ> distribution X\<rparr>" |
|
209 proof (rule measure_space.measure_space_cong) |
|
210 show "measure_space (S\<lparr> measure := \<lambda>A. \<mu> (X -` A \<inter> space M) \<rparr>)" |
|
211 using assms by (auto intro!: measure_space_vimage simp: measure_preserving_def) |
|
212 qed (insert assms, auto simp add: finite_measure_eq distribution_def measurable_sets) |
|
213 show ?thesis |
|
214 proof (default, simp) |
|
215 have "X -` space S \<inter> space M = space M" |
|
216 using `random_variable S X` by (auto simp: measurable_def) |
|
217 then show "extreal (distribution X (space S)) = 1" |
|
218 by (simp add: distribution_def one_extreal_def prob_space) |
|
219 qed |
|
220 qed |
|
221 |
|
222 lemma (in prob_space) AE_distribution: |
|
223 assumes X: "random_variable MX X" and "AE x in MX\<lparr>measure := extreal \<circ> distribution X\<rparr>. Q x" |
|
224 shows "AE x. Q (X x)" |
|
225 proof - |
|
226 interpret X: prob_space "MX\<lparr>measure := extreal \<circ> distribution X\<rparr>" using X by (rule distribution_prob_space) |
|
227 obtain N where N: "N \<in> sets MX" "distribution X N = 0" "{x\<in>space MX. \<not> Q x} \<subseteq> N" |
|
228 using assms unfolding X.almost_everywhere_def by auto |
|
229 from X[unfolded measurable_def] N show "AE x. Q (X x)" |
|
230 by (intro AE_I'[where N="X -` N \<inter> space M"]) |
|
231 (auto simp: finite_measure_eq distribution_def measurable_sets) |
|
232 qed |
|
233 |
|
234 lemma (in prob_space) distribution_eq_integral: |
|
235 "random_variable S X \<Longrightarrow> A \<in> sets S \<Longrightarrow> distribution X A = expectation (indicator (X -` A \<inter> space M))" |
|
236 using finite_measure_eq[of "X -` A \<inter> space M"] |
|
237 by (auto simp: measurable_sets distribution_def) |
|
238 |
|
239 lemma (in prob_space) distribution_eq_translated_integral: |
|
240 assumes "random_variable S X" "A \<in> sets S" |
|
241 shows "distribution X A = integral\<^isup>P (S\<lparr>measure := extreal \<circ> distribution X\<rparr>) (indicator A)" |
|
242 proof - |
|
243 interpret S: prob_space "S\<lparr>measure := extreal \<circ> distribution X\<rparr>" |
|
244 using assms(1) by (rule distribution_prob_space) |
|
245 show ?thesis |
|
246 using S.positive_integral_indicator(1)[of A] assms by simp |
|
247 qed |
|
248 |
|
249 lemma (in prob_space) finite_expectation1: |
|
250 assumes f: "finite (X`space M)" and rv: "random_variable borel X" |
|
251 shows "expectation X = (\<Sum>r \<in> X ` space M. r * prob (X -` {r} \<inter> space M))" (is "_ = ?r") |
|
252 proof (subst integral_on_finite) |
|
253 show "X \<in> borel_measurable M" "finite (X`space M)" using assms by auto |
|
254 show "(\<Sum> r \<in> X ` space M. r * real (\<mu> (X -` {r} \<inter> space M))) = ?r" |
|
255 "\<And>x. \<mu> (X -` {x} \<inter> space M) \<noteq> \<infinity>" |
|
256 using finite_measure_eq[OF borel_measurable_vimage, of X] rv by auto |
|
257 qed |
|
258 |
|
259 lemma (in prob_space) finite_expectation: |
|
260 assumes "finite (X`space M)" "random_variable borel X" |
|
261 shows "expectation X = (\<Sum> r \<in> X ` (space M). r * distribution X {r})" |
|
262 using assms unfolding distribution_def using finite_expectation1 by auto |
|
263 |
|
264 lemma (in prob_space) prob_x_eq_1_imp_prob_y_eq_0: |
|
265 assumes "{x} \<in> events" |
|
266 assumes "prob {x} = 1" |
|
267 assumes "{y} \<in> events" |
|
268 assumes "y \<noteq> x" |
|
269 shows "prob {y} = 0" |
|
270 using prob_one_inter[of "{y}" "{x}"] assms by auto |
|
271 |
|
272 lemma (in prob_space) distribution_empty[simp]: "distribution X {} = 0" |
|
273 unfolding distribution_def by simp |
|
274 |
|
275 lemma (in prob_space) distribution_space[simp]: "distribution X (X ` space M) = 1" |
|
276 proof - |
|
277 have "X -` X ` space M \<inter> space M = space M" by auto |
|
278 thus ?thesis unfolding distribution_def by (simp add: prob_space) |
|
279 qed |
|
280 |
|
281 lemma (in prob_space) distribution_one: |
|
282 assumes "random_variable M' X" and "A \<in> sets M'" |
|
283 shows "distribution X A \<le> 1" |
|
284 proof - |
|
285 have "distribution X A \<le> \<mu>' (space M)" unfolding distribution_def |
|
286 using assms[unfolded measurable_def] by (auto intro!: finite_measure_mono) |
|
287 thus ?thesis by (simp add: prob_space) |
|
288 qed |
|
289 |
|
290 lemma (in prob_space) distribution_x_eq_1_imp_distribution_y_eq_0: |
|
291 assumes X: "random_variable \<lparr>space = X ` (space M), sets = Pow (X ` (space M))\<rparr> X" |
|
292 (is "random_variable ?S X") |
|
293 assumes "distribution X {x} = 1" |
|
294 assumes "y \<noteq> x" |
|
295 shows "distribution X {y} = 0" |
|
296 proof cases |
|
297 { fix x have "X -` {x} \<inter> space M \<in> sets M" |
|
298 proof cases |
|
299 assume "x \<in> X`space M" with X show ?thesis |
|
300 by (auto simp: measurable_def image_iff) |
|
301 next |
|
302 assume "x \<notin> X`space M" then have "X -` {x} \<inter> space M = {}" by auto |
|
303 then show ?thesis by auto |
|
304 qed } note single = this |
|
305 have "X -` {x} \<inter> space M - X -` {y} \<inter> space M = X -` {x} \<inter> space M" |
|
306 "X -` {y} \<inter> space M \<inter> (X -` {x} \<inter> space M) = {}" |
|
307 using `y \<noteq> x` by auto |
|
308 with finite_measure_inter_full_set[OF single single, of x y] assms(2) |
|
309 show ?thesis by (auto simp: distribution_def prob_space) |
|
310 next |
|
311 assume "{y} \<notin> sets ?S" |
|
312 then have "X -` {y} \<inter> space M = {}" by auto |
|
313 thus "distribution X {y} = 0" unfolding distribution_def by auto |
|
314 qed |
|
315 |
|
316 lemma (in prob_space) joint_distribution_Times_le_fst: |
|
317 assumes X: "random_variable MX X" and Y: "random_variable MY Y" |
|
318 and A: "A \<in> sets MX" and B: "B \<in> sets MY" |
|
319 shows "joint_distribution X Y (A \<times> B) \<le> distribution X A" |
|
320 unfolding distribution_def |
|
321 proof (intro finite_measure_mono) |
|
322 show "(\<lambda>x. (X x, Y x)) -` (A \<times> B) \<inter> space M \<subseteq> X -` A \<inter> space M" by force |
|
323 show "X -` A \<inter> space M \<in> events" |
|
324 using X A unfolding measurable_def by simp |
|
325 have *: "(\<lambda>x. (X x, Y x)) -` (A \<times> B) \<inter> space M = |
|
326 (X -` A \<inter> space M) \<inter> (Y -` B \<inter> space M)" by auto |
|
327 qed |
|
328 |
|
329 lemma (in prob_space) joint_distribution_commute: |
|
330 "joint_distribution X Y x = joint_distribution Y X ((\<lambda>(x,y). (y,x))`x)" |
|
331 unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>']) |
|
332 |
|
333 lemma (in prob_space) joint_distribution_Times_le_snd: |
|
334 assumes X: "random_variable MX X" and Y: "random_variable MY Y" |
|
335 and A: "A \<in> sets MX" and B: "B \<in> sets MY" |
|
336 shows "joint_distribution X Y (A \<times> B) \<le> distribution Y B" |
|
337 using assms |
|
338 by (subst joint_distribution_commute) |
|
339 (simp add: swap_product joint_distribution_Times_le_fst) |
|
340 |
|
341 lemma (in prob_space) random_variable_pairI: |
|
342 assumes "random_variable MX X" |
|
343 assumes "random_variable MY Y" |
|
344 shows "random_variable (MX \<Otimes>\<^isub>M MY) (\<lambda>x. (X x, Y x))" |
|
345 proof |
|
346 interpret MX: sigma_algebra MX using assms by simp |
|
347 interpret MY: sigma_algebra MY using assms by simp |
|
348 interpret P: pair_sigma_algebra MX MY by default |
|
349 show "sigma_algebra (MX \<Otimes>\<^isub>M MY)" by default |
|
350 have sa: "sigma_algebra M" by default |
|
351 show "(\<lambda>x. (X x, Y x)) \<in> measurable M (MX \<Otimes>\<^isub>M MY)" |
|
352 unfolding P.measurable_pair_iff[OF sa] using assms by (simp add: comp_def) |
|
353 qed |
|
354 |
|
355 lemma (in prob_space) joint_distribution_commute_singleton: |
|
356 "joint_distribution X Y {(x, y)} = joint_distribution Y X {(y, x)}" |
|
357 unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>']) |
|
358 |
|
359 lemma (in prob_space) joint_distribution_assoc_singleton: |
|
360 "joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)} = |
|
361 joint_distribution (\<lambda>x. (X x, Y x)) Z {((x, y), z)}" |
|
362 unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>']) |
|
363 |
|
364 locale pair_prob_space = M1: prob_space M1 + M2: prob_space M2 for M1 M2 |
|
365 |
|
366 sublocale pair_prob_space \<subseteq> pair_sigma_finite M1 M2 by default |
|
367 |
|
368 sublocale pair_prob_space \<subseteq> P: prob_space P |
|
369 by default (simp add: pair_measure_times M1.measure_space_1 M2.measure_space_1 space_pair_measure) |
|
370 |
|
371 lemma countably_additiveI[case_names countably]: |
|
372 assumes "\<And>A. \<lbrakk> range A \<subseteq> sets M ; disjoint_family A ; (\<Union>i. A i) \<in> sets M\<rbrakk> \<Longrightarrow> |
|
373 (\<Sum>n. \<mu> (A n)) = \<mu> (\<Union>i. A i)" |
|
374 shows "countably_additive M \<mu>" |
|
375 using assms unfolding countably_additive_def by auto |
|
376 |
|
377 lemma (in prob_space) joint_distribution_prob_space: |
|
378 assumes "random_variable MX X" "random_variable MY Y" |
|
379 shows "prob_space ((MX \<Otimes>\<^isub>M MY) \<lparr> measure := extreal \<circ> joint_distribution X Y\<rparr>)" |
|
380 using random_variable_pairI[OF assms] by (rule distribution_prob_space) |
|
381 |
|
382 section "Probability spaces on finite sets" |
|
383 |
|
384 locale finite_prob_space = prob_space + finite_measure_space |
|
385 |
|
386 abbreviation (in prob_space) "finite_random_variable M' X \<equiv> finite_sigma_algebra M' \<and> X \<in> measurable M M'" |
|
387 |
|
388 lemma (in prob_space) finite_random_variableD: |
|
389 assumes "finite_random_variable M' X" shows "random_variable M' X" |
|
390 proof - |
|
391 interpret M': finite_sigma_algebra M' using assms by simp |
|
392 then show "random_variable M' X" using assms by simp default |
|
393 qed |
|
394 |
|
395 lemma (in prob_space) distribution_finite_prob_space: |
|
396 assumes "finite_random_variable MX X" |
|
397 shows "finite_prob_space (MX\<lparr>measure := extreal \<circ> distribution X\<rparr>)" |
|
398 proof - |
|
399 interpret X: prob_space "MX\<lparr>measure := extreal \<circ> distribution X\<rparr>" |
|
400 using assms[THEN finite_random_variableD] by (rule distribution_prob_space) |
|
401 interpret MX: finite_sigma_algebra MX |
|
402 using assms by auto |
|
403 show ?thesis by default (simp_all add: MX.finite_space) |
|
404 qed |
|
405 |
|
406 lemma (in prob_space) simple_function_imp_finite_random_variable[simp, intro]: |
|
407 assumes "simple_function M X" |
|
408 shows "finite_random_variable \<lparr> space = X`space M, sets = Pow (X`space M), \<dots> = x \<rparr> X" |
|
409 (is "finite_random_variable ?X _") |
|
410 proof (intro conjI) |
|
411 have [simp]: "finite (X ` space M)" using assms unfolding simple_function_def by simp |
|
412 interpret X: sigma_algebra ?X by (rule sigma_algebra_Pow) |
|
413 show "finite_sigma_algebra ?X" |
|
414 by default auto |
|
415 show "X \<in> measurable M ?X" |
|
416 proof (unfold measurable_def, clarsimp) |
|
417 fix A assume A: "A \<subseteq> X`space M" |
|
418 then have "finite A" by (rule finite_subset) simp |
|
419 then have "X -` (\<Union>a\<in>A. {a}) \<inter> space M \<in> events" |
|
420 unfolding vimage_UN UN_extend_simps |
|
421 apply (rule finite_UN) |
|
422 using A assms unfolding simple_function_def by auto |
|
423 then show "X -` A \<inter> space M \<in> events" by simp |
|
424 qed |
|
425 qed |
|
426 |
|
427 lemma (in prob_space) simple_function_imp_random_variable[simp, intro]: |
|
428 assumes "simple_function M X" |
|
429 shows "random_variable \<lparr> space = X`space M, sets = Pow (X`space M), \<dots> = ext \<rparr> X" |
|
430 using simple_function_imp_finite_random_variable[OF assms, of ext] |
|
431 by (auto dest!: finite_random_variableD) |
|
432 |
|
433 lemma (in prob_space) sum_over_space_real_distribution: |
|
434 "simple_function M X \<Longrightarrow> (\<Sum>x\<in>X`space M. distribution X {x}) = 1" |
|
435 unfolding distribution_def prob_space[symmetric] |
|
436 by (subst finite_measure_finite_Union[symmetric]) |
|
437 (auto simp add: disjoint_family_on_def simple_function_def |
|
438 intro!: arg_cong[where f=prob]) |
|
439 |
|
440 lemma (in prob_space) finite_random_variable_pairI: |
|
441 assumes "finite_random_variable MX X" |
|
442 assumes "finite_random_variable MY Y" |
|
443 shows "finite_random_variable (MX \<Otimes>\<^isub>M MY) (\<lambda>x. (X x, Y x))" |
|
444 proof |
|
445 interpret MX: finite_sigma_algebra MX using assms by simp |
|
446 interpret MY: finite_sigma_algebra MY using assms by simp |
|
447 interpret P: pair_finite_sigma_algebra MX MY by default |
|
448 show "finite_sigma_algebra (MX \<Otimes>\<^isub>M MY)" by default |
|
449 have sa: "sigma_algebra M" by default |
|
450 show "(\<lambda>x. (X x, Y x)) \<in> measurable M (MX \<Otimes>\<^isub>M MY)" |
|
451 unfolding P.measurable_pair_iff[OF sa] using assms by (simp add: comp_def) |
|
452 qed |
|
453 |
|
454 lemma (in prob_space) finite_random_variable_imp_sets: |
|
455 "finite_random_variable MX X \<Longrightarrow> x \<in> space MX \<Longrightarrow> {x} \<in> sets MX" |
|
456 unfolding finite_sigma_algebra_def finite_sigma_algebra_axioms_def by simp |
|
457 |
|
458 lemma (in prob_space) finite_random_variable_measurable: |
|
459 assumes X: "finite_random_variable MX X" shows "X -` A \<inter> space M \<in> events" |
|
460 proof - |
|
461 interpret X: finite_sigma_algebra MX using X by simp |
|
462 from X have vimage: "\<And>A. A \<subseteq> space MX \<Longrightarrow> X -` A \<inter> space M \<in> events" and |
|
463 "X \<in> space M \<rightarrow> space MX" |
|
464 by (auto simp: measurable_def) |
|
465 then have *: "X -` A \<inter> space M = X -` (A \<inter> space MX) \<inter> space M" |
|
466 by auto |
|
467 show "X -` A \<inter> space M \<in> events" |
|
468 unfolding * by (intro vimage) auto |
|
469 qed |
|
470 |
|
471 lemma (in prob_space) joint_distribution_finite_Times_le_fst: |
|
472 assumes X: "finite_random_variable MX X" and Y: "finite_random_variable MY Y" |
|
473 shows "joint_distribution X Y (A \<times> B) \<le> distribution X A" |
|
474 unfolding distribution_def |
|
475 proof (intro finite_measure_mono) |
|
476 show "(\<lambda>x. (X x, Y x)) -` (A \<times> B) \<inter> space M \<subseteq> X -` A \<inter> space M" by force |
|
477 show "X -` A \<inter> space M \<in> events" |
|
478 using finite_random_variable_measurable[OF X] . |
|
479 have *: "(\<lambda>x. (X x, Y x)) -` (A \<times> B) \<inter> space M = |
|
480 (X -` A \<inter> space M) \<inter> (Y -` B \<inter> space M)" by auto |
|
481 qed |
|
482 |
|
483 lemma (in prob_space) joint_distribution_finite_Times_le_snd: |
|
484 assumes X: "finite_random_variable MX X" and Y: "finite_random_variable MY Y" |
|
485 shows "joint_distribution X Y (A \<times> B) \<le> distribution Y B" |
|
486 using assms |
|
487 by (subst joint_distribution_commute) |
|
488 (simp add: swap_product joint_distribution_finite_Times_le_fst) |
|
489 |
|
490 lemma (in prob_space) finite_distribution_order: |
|
491 fixes MX :: "('c, 'd) measure_space_scheme" and MY :: "('e, 'f) measure_space_scheme" |
|
492 assumes "finite_random_variable MX X" "finite_random_variable MY Y" |
|
493 shows "r \<le> joint_distribution X Y {(x, y)} \<Longrightarrow> r \<le> distribution X {x}" |
|
494 and "r \<le> joint_distribution X Y {(x, y)} \<Longrightarrow> r \<le> distribution Y {y}" |
|
495 and "r < joint_distribution X Y {(x, y)} \<Longrightarrow> r < distribution X {x}" |
|
496 and "r < joint_distribution X Y {(x, y)} \<Longrightarrow> r < distribution Y {y}" |
|
497 and "distribution X {x} = 0 \<Longrightarrow> joint_distribution X Y {(x, y)} = 0" |
|
498 and "distribution Y {y} = 0 \<Longrightarrow> joint_distribution X Y {(x, y)} = 0" |
|
499 using joint_distribution_finite_Times_le_snd[OF assms, of "{x}" "{y}"] |
|
500 using joint_distribution_finite_Times_le_fst[OF assms, of "{x}" "{y}"] |
|
501 by (auto intro: antisym) |
|
502 |
|
503 lemma (in prob_space) setsum_joint_distribution: |
|
504 assumes X: "finite_random_variable MX X" |
|
505 assumes Y: "random_variable MY Y" "B \<in> sets MY" |
|
506 shows "(\<Sum>a\<in>space MX. joint_distribution X Y ({a} \<times> B)) = distribution Y B" |
|
507 unfolding distribution_def |
|
508 proof (subst finite_measure_finite_Union[symmetric]) |
|
509 interpret MX: finite_sigma_algebra MX using X by auto |
|
510 show "finite (space MX)" using MX.finite_space . |
|
511 let "?d i" = "(\<lambda>x. (X x, Y x)) -` ({i} \<times> B) \<inter> space M" |
|
512 { fix i assume "i \<in> space MX" |
|
513 moreover have "?d i = (X -` {i} \<inter> space M) \<inter> (Y -` B \<inter> space M)" by auto |
|
514 ultimately show "?d i \<in> events" |
|
515 using measurable_sets[of X M MX] measurable_sets[of Y M MY B] X Y |
|
516 using MX.sets_eq_Pow by auto } |
|
517 show "disjoint_family_on ?d (space MX)" by (auto simp: disjoint_family_on_def) |
|
518 show "\<mu>' (\<Union>i\<in>space MX. ?d i) = \<mu>' (Y -` B \<inter> space M)" |
|
519 using X[unfolded measurable_def] by (auto intro!: arg_cong[where f=\<mu>']) |
|
520 qed |
|
521 |
|
522 lemma (in prob_space) setsum_joint_distribution_singleton: |
|
523 assumes X: "finite_random_variable MX X" |
|
524 assumes Y: "finite_random_variable MY Y" "b \<in> space MY" |
|
525 shows "(\<Sum>a\<in>space MX. joint_distribution X Y {(a, b)}) = distribution Y {b}" |
|
526 using setsum_joint_distribution[OF X |
|
527 finite_random_variableD[OF Y(1)] |
|
528 finite_random_variable_imp_sets[OF Y]] by simp |
|
529 |
|
530 locale pair_finite_prob_space = M1: finite_prob_space M1 + M2: finite_prob_space M2 for M1 M2 |
|
531 |
|
532 sublocale pair_finite_prob_space \<subseteq> pair_prob_space M1 M2 by default |
|
533 sublocale pair_finite_prob_space \<subseteq> pair_finite_space M1 M2 by default |
|
534 sublocale pair_finite_prob_space \<subseteq> finite_prob_space P by default |
|
535 |
|
536 lemma (in prob_space) joint_distribution_finite_prob_space: |
|
537 assumes X: "finite_random_variable MX X" |
|
538 assumes Y: "finite_random_variable MY Y" |
|
539 shows "finite_prob_space ((MX \<Otimes>\<^isub>M MY)\<lparr> measure := extreal \<circ> joint_distribution X Y\<rparr>)" |
|
540 by (intro distribution_finite_prob_space finite_random_variable_pairI X Y) |
|
541 |
|
542 lemma finite_prob_space_eq: |
|
543 "finite_prob_space M \<longleftrightarrow> finite_measure_space M \<and> measure M (space M) = 1" |
|
544 unfolding finite_prob_space_def finite_measure_space_def prob_space_def prob_space_axioms_def |
|
545 by auto |
|
546 |
|
547 lemma (in prob_space) not_empty: "space M \<noteq> {}" |
|
548 using prob_space empty_measure' by auto |
|
549 |
|
550 lemma (in finite_prob_space) sum_over_space_eq_1: "(\<Sum>x\<in>space M. \<mu> {x}) = 1" |
|
551 using measure_space_1 sum_over_space by simp |
|
552 |
|
553 lemma (in finite_prob_space) joint_distribution_restriction_fst: |
|
554 "joint_distribution X Y A \<le> distribution X (fst ` A)" |
|
555 unfolding distribution_def |
|
556 proof (safe intro!: finite_measure_mono) |
|
557 fix x assume "x \<in> space M" and *: "(X x, Y x) \<in> A" |
|
558 show "x \<in> X -` fst ` A" |
|
559 by (auto intro!: image_eqI[OF _ *]) |
|
560 qed (simp_all add: sets_eq_Pow) |
|
561 |
|
562 lemma (in finite_prob_space) joint_distribution_restriction_snd: |
|
563 "joint_distribution X Y A \<le> distribution Y (snd ` A)" |
|
564 unfolding distribution_def |
|
565 proof (safe intro!: finite_measure_mono) |
|
566 fix x assume "x \<in> space M" and *: "(X x, Y x) \<in> A" |
|
567 show "x \<in> Y -` snd ` A" |
|
568 by (auto intro!: image_eqI[OF _ *]) |
|
569 qed (simp_all add: sets_eq_Pow) |
|
570 |
|
571 lemma (in finite_prob_space) distribution_order: |
|
572 shows "0 \<le> distribution X x'" |
|
573 and "(distribution X x' \<noteq> 0) \<longleftrightarrow> (0 < distribution X x')" |
|
574 and "r \<le> joint_distribution X Y {(x, y)} \<Longrightarrow> r \<le> distribution X {x}" |
|
575 and "r \<le> joint_distribution X Y {(x, y)} \<Longrightarrow> r \<le> distribution Y {y}" |
|
576 and "r < joint_distribution X Y {(x, y)} \<Longrightarrow> r < distribution X {x}" |
|
577 and "r < joint_distribution X Y {(x, y)} \<Longrightarrow> r < distribution Y {y}" |
|
578 and "distribution X {x} = 0 \<Longrightarrow> joint_distribution X Y {(x, y)} = 0" |
|
579 and "distribution Y {y} = 0 \<Longrightarrow> joint_distribution X Y {(x, y)} = 0" |
|
580 using |
|
581 joint_distribution_restriction_fst[of X Y "{(x, y)}"] |
|
582 joint_distribution_restriction_snd[of X Y "{(x, y)}"] |
|
583 by (auto intro: antisym) |
|
584 |
|
585 lemma (in finite_prob_space) distribution_mono: |
|
586 assumes "\<And>t. \<lbrakk> t \<in> space M ; X t \<in> x \<rbrakk> \<Longrightarrow> Y t \<in> y" |
|
587 shows "distribution X x \<le> distribution Y y" |
|
588 unfolding distribution_def |
|
589 using assms by (auto simp: sets_eq_Pow intro!: finite_measure_mono) |
|
590 |
|
591 lemma (in finite_prob_space) distribution_mono_gt_0: |
|
592 assumes gt_0: "0 < distribution X x" |
|
593 assumes *: "\<And>t. \<lbrakk> t \<in> space M ; X t \<in> x \<rbrakk> \<Longrightarrow> Y t \<in> y" |
|
594 shows "0 < distribution Y y" |
|
595 by (rule less_le_trans[OF gt_0 distribution_mono]) (rule *) |
|
596 |
|
597 lemma (in finite_prob_space) sum_over_space_distrib: |
|
598 "(\<Sum>x\<in>X`space M. distribution X {x}) = 1" |
|
599 unfolding distribution_def prob_space[symmetric] using finite_space |
|
600 by (subst finite_measure_finite_Union[symmetric]) |
|
601 (auto simp add: disjoint_family_on_def sets_eq_Pow |
|
602 intro!: arg_cong[where f=\<mu>']) |
|
603 |
|
604 lemma (in finite_prob_space) sum_over_space_real_distribution: |
|
605 "(\<Sum>x\<in>X`space M. distribution X {x}) = 1" |
|
606 unfolding distribution_def prob_space[symmetric] using finite_space |
|
607 by (subst finite_measure_finite_Union[symmetric]) |
|
608 (auto simp add: disjoint_family_on_def sets_eq_Pow intro!: arg_cong[where f=prob]) |
|
609 |
|
610 lemma (in finite_prob_space) finite_sum_over_space_eq_1: |
|
611 "(\<Sum>x\<in>space M. prob {x}) = 1" |
|
612 using prob_space finite_space |
|
613 by (subst (asm) finite_measure_finite_singleton) auto |
|
614 |
|
615 lemma (in prob_space) distribution_remove_const: |
|
616 shows "joint_distribution X (\<lambda>x. ()) {(x, ())} = distribution X {x}" |
|
617 and "joint_distribution (\<lambda>x. ()) X {((), x)} = distribution X {x}" |
|
618 and "joint_distribution X (\<lambda>x. (Y x, ())) {(x, y, ())} = joint_distribution X Y {(x, y)}" |
|
619 and "joint_distribution X (\<lambda>x. ((), Y x)) {(x, (), y)} = joint_distribution X Y {(x, y)}" |
|
620 and "distribution (\<lambda>x. ()) {()} = 1" |
|
621 by (auto intro!: arg_cong[where f=\<mu>'] simp: distribution_def prob_space[symmetric]) |
|
622 |
|
623 lemma (in finite_prob_space) setsum_distribution_gen: |
|
624 assumes "Z -` {c} \<inter> space M = (\<Union>x \<in> X`space M. Y -` {f x}) \<inter> space M" |
|
625 and "inj_on f (X`space M)" |
|
626 shows "(\<Sum>x \<in> X`space M. distribution Y {f x}) = distribution Z {c}" |
|
627 unfolding distribution_def assms |
|
628 using finite_space assms |
|
629 by (subst finite_measure_finite_Union[symmetric]) |
|
630 (auto simp add: disjoint_family_on_def sets_eq_Pow inj_on_def |
|
631 intro!: arg_cong[where f=prob]) |
|
632 |
|
633 lemma (in finite_prob_space) setsum_distribution: |
|
634 "(\<Sum>x \<in> X`space M. joint_distribution X Y {(x, y)}) = distribution Y {y}" |
|
635 "(\<Sum>y \<in> Y`space M. joint_distribution X Y {(x, y)}) = distribution X {x}" |
|
636 "(\<Sum>x \<in> X`space M. joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)}) = joint_distribution Y Z {(y, z)}" |
|
637 "(\<Sum>y \<in> Y`space M. joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)}) = joint_distribution X Z {(x, z)}" |
|
638 "(\<Sum>z \<in> Z`space M. joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)}) = joint_distribution X Y {(x, y)}" |
|
639 by (auto intro!: inj_onI setsum_distribution_gen) |
|
640 |
|
641 lemma (in finite_prob_space) uniform_prob: |
|
642 assumes "x \<in> space M" |
|
643 assumes "\<And> x y. \<lbrakk>x \<in> space M ; y \<in> space M\<rbrakk> \<Longrightarrow> prob {x} = prob {y}" |
|
644 shows "prob {x} = 1 / card (space M)" |
|
645 proof - |
|
646 have prob_x: "\<And> y. y \<in> space M \<Longrightarrow> prob {y} = prob {x}" |
|
647 using assms(2)[OF _ `x \<in> space M`] by blast |
|
648 have "1 = prob (space M)" |
|
649 using prob_space by auto |
|
650 also have "\<dots> = (\<Sum> x \<in> space M. prob {x})" |
|
651 using finite_measure_finite_Union[of "space M" "\<lambda> x. {x}", simplified] |
|
652 sets_eq_Pow inj_singleton[unfolded inj_on_def, rule_format] |
|
653 finite_space unfolding disjoint_family_on_def prob_space[symmetric] |
|
654 by (auto simp add:setsum_restrict_set) |
|
655 also have "\<dots> = (\<Sum> y \<in> space M. prob {x})" |
|
656 using prob_x by auto |
|
657 also have "\<dots> = real_of_nat (card (space M)) * prob {x}" by simp |
|
658 finally have one: "1 = real (card (space M)) * prob {x}" |
|
659 using real_eq_of_nat by auto |
|
660 hence two: "real (card (space M)) \<noteq> 0" by fastsimp |
|
661 from one have three: "prob {x} \<noteq> 0" by fastsimp |
|
662 thus ?thesis using one two three divide_cancel_right |
|
663 by (auto simp:field_simps) |
|
664 qed |
|
665 |
|
666 lemma (in prob_space) prob_space_subalgebra: |
|
667 assumes "sigma_algebra N" "sets N \<subseteq> sets M" "space N = space M" |
|
668 and "\<And>A. A \<in> sets N \<Longrightarrow> measure N A = \<mu> A" |
|
669 shows "prob_space N" |
|
670 proof - |
|
671 interpret N: measure_space N |
|
672 by (rule measure_space_subalgebra[OF assms]) |
|
673 show ?thesis |
|
674 proof qed (insert assms(4)[OF N.top], simp add: assms measure_space_1) |
|
675 qed |
|
676 |
|
677 lemma (in prob_space) prob_space_of_restricted_space: |
|
678 assumes "\<mu> A \<noteq> 0" "A \<in> sets M" |
|
679 shows "prob_space (restricted_space A \<lparr>measure := \<lambda>S. \<mu> S / \<mu> A\<rparr>)" |
|
680 (is "prob_space ?P") |
|
681 proof - |
|
682 interpret A: measure_space "restricted_space A" |
|
683 using `A \<in> sets M` by (rule restricted_measure_space) |
|
684 interpret A': sigma_algebra ?P |
|
685 by (rule A.sigma_algebra_cong) auto |
|
686 show "prob_space ?P" |
|
687 proof |
|
688 show "measure ?P (space ?P) = 1" |
|
689 using real_measure[OF `A \<in> events`] `\<mu> A \<noteq> 0` by auto |
|
690 show "positive ?P (measure ?P)" |
|
691 proof (simp add: positive_def, safe) |
|
692 show "0 / \<mu> A = 0" using `\<mu> A \<noteq> 0` by (cases "\<mu> A") (auto simp: zero_extreal_def) |
|
693 fix B assume "B \<in> events" |
|
694 with real_measure[of "A \<inter> B"] real_measure[OF `A \<in> events`] `A \<in> sets M` |
|
695 show "0 \<le> \<mu> (A \<inter> B) / \<mu> A" by (auto simp: Int) |
|
696 qed |
|
697 show "countably_additive ?P (measure ?P)" |
|
698 proof (simp add: countably_additive_def, safe) |
|
699 fix B and F :: "nat \<Rightarrow> 'a set" |
|
700 assume F: "range F \<subseteq> op \<inter> A ` events" "disjoint_family F" |
|
701 { fix i |
|
702 from F have "F i \<in> op \<inter> A ` events" by auto |
|
703 with `A \<in> events` have "F i \<in> events" by auto } |
|
704 moreover then have "range F \<subseteq> events" by auto |
|
705 moreover have "\<And>S. \<mu> S / \<mu> A = inverse (\<mu> A) * \<mu> S" |
|
706 by (simp add: mult_commute divide_extreal_def) |
|
707 moreover have "0 \<le> inverse (\<mu> A)" |
|
708 using real_measure[OF `A \<in> events`] by auto |
|
709 ultimately show "(\<Sum>i. \<mu> (F i) / \<mu> A) = \<mu> (\<Union>i. F i) / \<mu> A" |
|
710 using measure_countably_additive[of F] F |
|
711 by (auto simp: suminf_cmult_extreal) |
|
712 qed |
|
713 qed |
|
714 qed |
|
715 |
|
716 lemma finite_prob_spaceI: |
|
717 assumes "finite (space M)" "sets M = Pow(space M)" |
|
718 and "measure M (space M) = 1" "measure M {} = 0" "\<And>A. A \<subseteq> space M \<Longrightarrow> 0 \<le> measure M A" |
|
719 and "\<And>A B. A\<subseteq>space M \<Longrightarrow> B\<subseteq>space M \<Longrightarrow> A \<inter> B = {} \<Longrightarrow> measure M (A \<union> B) = measure M A + measure M B" |
|
720 shows "finite_prob_space M" |
|
721 unfolding finite_prob_space_eq |
|
722 proof |
|
723 show "finite_measure_space M" using assms |
|
724 by (auto intro!: finite_measure_spaceI) |
|
725 show "measure M (space M) = 1" by fact |
|
726 qed |
|
727 |
|
728 lemma (in finite_prob_space) finite_measure_space: |
|
729 fixes X :: "'a \<Rightarrow> 'x" |
|
730 shows "finite_measure_space \<lparr>space = X ` space M, sets = Pow (X ` space M), measure = extreal \<circ> distribution X\<rparr>" |
|
731 (is "finite_measure_space ?S") |
|
732 proof (rule finite_measure_spaceI, simp_all) |
|
733 show "finite (X ` space M)" using finite_space by simp |
|
734 next |
|
735 fix A B :: "'x set" assume "A \<inter> B = {}" |
|
736 then show "distribution X (A \<union> B) = distribution X A + distribution X B" |
|
737 unfolding distribution_def |
|
738 by (subst finite_measure_Union[symmetric]) |
|
739 (auto intro!: arg_cong[where f=\<mu>'] simp: sets_eq_Pow) |
|
740 qed |
|
741 |
|
742 lemma (in finite_prob_space) finite_prob_space_of_images: |
|
743 "finite_prob_space \<lparr> space = X ` space M, sets = Pow (X ` space M), measure = extreal \<circ> distribution X \<rparr>" |
|
744 by (simp add: finite_prob_space_eq finite_measure_space measure_space_1 one_extreal_def) |
|
745 |
|
746 lemma (in finite_prob_space) finite_product_measure_space: |
|
747 fixes X :: "'a \<Rightarrow> 'x" and Y :: "'a \<Rightarrow> 'y" |
|
748 assumes "finite s1" "finite s2" |
|
749 shows "finite_measure_space \<lparr> space = s1 \<times> s2, sets = Pow (s1 \<times> s2), measure = extreal \<circ> joint_distribution X Y\<rparr>" |
|
750 (is "finite_measure_space ?M") |
|
751 proof (rule finite_measure_spaceI, simp_all) |
|
752 show "finite (s1 \<times> s2)" |
|
753 using assms by auto |
|
754 next |
|
755 fix A B :: "('x*'y) set" assume "A \<inter> B = {}" |
|
756 then show "joint_distribution X Y (A \<union> B) = joint_distribution X Y A + joint_distribution X Y B" |
|
757 unfolding distribution_def |
|
758 by (subst finite_measure_Union[symmetric]) |
|
759 (auto intro!: arg_cong[where f=\<mu>'] simp: sets_eq_Pow) |
|
760 qed |
|
761 |
|
762 lemma (in finite_prob_space) finite_product_measure_space_of_images: |
|
763 shows "finite_measure_space \<lparr> space = X ` space M \<times> Y ` space M, |
|
764 sets = Pow (X ` space M \<times> Y ` space M), |
|
765 measure = extreal \<circ> joint_distribution X Y \<rparr>" |
|
766 using finite_space by (auto intro!: finite_product_measure_space) |
|
767 |
|
768 lemma (in finite_prob_space) finite_product_prob_space_of_images: |
|
769 "finite_prob_space \<lparr> space = X ` space M \<times> Y ` space M, sets = Pow (X ` space M \<times> Y ` space M), |
|
770 measure = extreal \<circ> joint_distribution X Y \<rparr>" |
|
771 (is "finite_prob_space ?S") |
|
772 proof (simp add: finite_prob_space_eq finite_product_measure_space_of_images one_extreal_def) |
|
773 have "X -` X ` space M \<inter> Y -` Y ` space M \<inter> space M = space M" by auto |
|
774 thus "joint_distribution X Y (X ` space M \<times> Y ` space M) = 1" |
|
775 by (simp add: distribution_def prob_space vimage_Times comp_def measure_space_1) |
|
776 qed |
|
777 |
|
778 section "Conditional Expectation and Probability" |
|
779 |
|
780 lemma (in prob_space) conditional_expectation_exists: |
|
781 fixes X :: "'a \<Rightarrow> extreal" and N :: "('a, 'b) measure_space_scheme" |
|
782 assumes borel: "X \<in> borel_measurable M" "AE x. 0 \<le> X x" |
|
783 and N: "sigma_algebra N" "sets N \<subseteq> sets M" "space N = space M" "\<And>A. measure N A = \<mu> A" |
|
784 shows "\<exists>Y\<in>borel_measurable N. (\<forall>x. 0 \<le> Y x) \<and> (\<forall>C\<in>sets N. |
|
785 (\<integral>\<^isup>+x. Y x * indicator C x \<partial>M) = (\<integral>\<^isup>+x. X x * indicator C x \<partial>M))" |
|
786 proof - |
|
787 note N(4)[simp] |
|
788 interpret P: prob_space N |
|
789 using prob_space_subalgebra[OF N] . |
|
790 |
|
791 let "?f A" = "\<lambda>x. X x * indicator A x" |
|
792 let "?Q A" = "integral\<^isup>P M (?f A)" |
|
793 |
|
794 from measure_space_density[OF borel] |
|
795 have Q: "measure_space (N\<lparr> measure := ?Q \<rparr>)" |
|
796 apply (rule measure_space.measure_space_subalgebra[of "M\<lparr> measure := ?Q \<rparr>"]) |
|
797 using N by (auto intro!: P.sigma_algebra_cong) |
|
798 then interpret Q: measure_space "N\<lparr> measure := ?Q \<rparr>" . |
|
799 |
|
800 have "P.absolutely_continuous ?Q" |
|
801 unfolding P.absolutely_continuous_def |
|
802 proof safe |
|
803 fix A assume "A \<in> sets N" "P.\<mu> A = 0" |
|
804 then have f_borel: "?f A \<in> borel_measurable M" "AE x. x \<notin> A" |
|
805 using borel N by (auto intro!: borel_measurable_indicator AE_not_in) |
|
806 then show "?Q A = 0" |
|
807 by (auto simp add: positive_integral_0_iff_AE) |
|
808 qed |
|
809 from P.Radon_Nikodym[OF Q this] |
|
810 obtain Y where Y: "Y \<in> borel_measurable N" "\<And>x. 0 \<le> Y x" |
|
811 "\<And>A. A \<in> sets N \<Longrightarrow> ?Q A =(\<integral>\<^isup>+x. Y x * indicator A x \<partial>N)" |
|
812 by blast |
|
813 with N(2) show ?thesis |
|
814 by (auto intro!: bexI[OF _ Y(1)] simp: positive_integral_subalgebra[OF _ _ N(2,3,4,1)]) |
|
815 qed |
|
816 |
|
817 definition (in prob_space) |
|
818 "conditional_expectation N X = (SOME Y. Y\<in>borel_measurable N \<and> (\<forall>x. 0 \<le> Y x) |
|
819 \<and> (\<forall>C\<in>sets N. (\<integral>\<^isup>+x. Y x * indicator C x\<partial>M) = (\<integral>\<^isup>+x. X x * indicator C x\<partial>M)))" |
|
820 |
|
821 abbreviation (in prob_space) |
|
822 "conditional_prob N A \<equiv> conditional_expectation N (indicator A)" |
|
823 |
|
824 lemma (in prob_space) |
|
825 fixes X :: "'a \<Rightarrow> extreal" and N :: "('a, 'b) measure_space_scheme" |
|
826 assumes borel: "X \<in> borel_measurable M" "AE x. 0 \<le> X x" |
|
827 and N: "sigma_algebra N" "sets N \<subseteq> sets M" "space N = space M" "\<And>A. measure N A = \<mu> A" |
|
828 shows borel_measurable_conditional_expectation: |
|
829 "conditional_expectation N X \<in> borel_measurable N" |
|
830 and conditional_expectation: "\<And>C. C \<in> sets N \<Longrightarrow> |
|
831 (\<integral>\<^isup>+x. conditional_expectation N X x * indicator C x \<partial>M) = |
|
832 (\<integral>\<^isup>+x. X x * indicator C x \<partial>M)" |
|
833 (is "\<And>C. C \<in> sets N \<Longrightarrow> ?eq C") |
|
834 proof - |
|
835 note CE = conditional_expectation_exists[OF assms, unfolded Bex_def] |
|
836 then show "conditional_expectation N X \<in> borel_measurable N" |
|
837 unfolding conditional_expectation_def by (rule someI2_ex) blast |
|
838 |
|
839 from CE show "\<And>C. C \<in> sets N \<Longrightarrow> ?eq C" |
|
840 unfolding conditional_expectation_def by (rule someI2_ex) blast |
|
841 qed |
|
842 |
|
843 lemma (in sigma_algebra) factorize_measurable_function_pos: |
|
844 fixes Z :: "'a \<Rightarrow> extreal" and Y :: "'a \<Rightarrow> 'c" |
|
845 assumes "sigma_algebra M'" and "Y \<in> measurable M M'" "Z \<in> borel_measurable M" |
|
846 assumes Z: "Z \<in> borel_measurable (sigma_algebra.vimage_algebra M' (space M) Y)" |
|
847 shows "\<exists>g\<in>borel_measurable M'. \<forall>x\<in>space M. max 0 (Z x) = g (Y x)" |
|
848 proof - |
|
849 interpret M': sigma_algebra M' by fact |
|
850 have Y: "Y \<in> space M \<rightarrow> space M'" using assms unfolding measurable_def by auto |
|
851 from M'.sigma_algebra_vimage[OF this] |
|
852 interpret va: sigma_algebra "M'.vimage_algebra (space M) Y" . |
|
853 |
|
854 from va.borel_measurable_implies_simple_function_sequence'[OF Z] guess f . note f = this |
|
855 |
|
856 have "\<forall>i. \<exists>g. simple_function M' g \<and> (\<forall>x\<in>space M. f i x = g (Y x))" |
|
857 proof |
|
858 fix i |
|
859 from f(1)[of i] have "finite (f i`space M)" and B_ex: |
|
860 "\<forall>z\<in>(f i)`space M. \<exists>B. B \<in> sets M' \<and> (f i) -` {z} \<inter> space M = Y -` B \<inter> space M" |
|
861 unfolding simple_function_def by auto |
|
862 from B_ex[THEN bchoice] guess B .. note B = this |
|
863 |
|
864 let ?g = "\<lambda>x. \<Sum>z\<in>f i`space M. z * indicator (B z) x" |
|
865 |
|
866 show "\<exists>g. simple_function M' g \<and> (\<forall>x\<in>space M. f i x = g (Y x))" |
|
867 proof (intro exI[of _ ?g] conjI ballI) |
|
868 show "simple_function M' ?g" using B by auto |
|
869 |
|
870 fix x assume "x \<in> space M" |
|
871 then have "\<And>z. z \<in> f i`space M \<Longrightarrow> indicator (B z) (Y x) = (indicator (f i -` {z} \<inter> space M) x::extreal)" |
|
872 unfolding indicator_def using B by auto |
|
873 then show "f i x = ?g (Y x)" using `x \<in> space M` f(1)[of i] |
|
874 by (subst va.simple_function_indicator_representation) auto |
|
875 qed |
|
876 qed |
|
877 from choice[OF this] guess g .. note g = this |
|
878 |
|
879 show ?thesis |
|
880 proof (intro ballI bexI) |
|
881 show "(\<lambda>x. SUP i. g i x) \<in> borel_measurable M'" |
|
882 using g by (auto intro: M'.borel_measurable_simple_function) |
|
883 fix x assume "x \<in> space M" |
|
884 have "max 0 (Z x) = (SUP i. f i x)" using f by simp |
|
885 also have "\<dots> = (SUP i. g i (Y x))" |
|
886 using g `x \<in> space M` by simp |
|
887 finally show "max 0 (Z x) = (SUP i. g i (Y x))" . |
|
888 qed |
|
889 qed |
|
890 |
|
891 lemma extreal_0_le_iff_le_0[simp]: |
|
892 fixes a :: extreal shows "0 \<le> -a \<longleftrightarrow> a \<le> 0" |
|
893 by (cases rule: extreal2_cases[of a]) auto |
|
894 |
|
895 lemma (in sigma_algebra) factorize_measurable_function: |
|
896 fixes Z :: "'a \<Rightarrow> extreal" and Y :: "'a \<Rightarrow> 'c" |
|
897 assumes "sigma_algebra M'" and "Y \<in> measurable M M'" "Z \<in> borel_measurable M" |
|
898 shows "Z \<in> borel_measurable (sigma_algebra.vimage_algebra M' (space M) Y) |
|
899 \<longleftrightarrow> (\<exists>g\<in>borel_measurable M'. \<forall>x\<in>space M. Z x = g (Y x))" |
|
900 proof safe |
|
901 interpret M': sigma_algebra M' by fact |
|
902 have Y: "Y \<in> space M \<rightarrow> space M'" using assms unfolding measurable_def by auto |
|
903 from M'.sigma_algebra_vimage[OF this] |
|
904 interpret va: sigma_algebra "M'.vimage_algebra (space M) Y" . |
|
905 |
|
906 { fix g :: "'c \<Rightarrow> extreal" assume "g \<in> borel_measurable M'" |
|
907 with M'.measurable_vimage_algebra[OF Y] |
|
908 have "g \<circ> Y \<in> borel_measurable (M'.vimage_algebra (space M) Y)" |
|
909 by (rule measurable_comp) |
|
910 moreover assume "\<forall>x\<in>space M. Z x = g (Y x)" |
|
911 then have "Z \<in> borel_measurable (M'.vimage_algebra (space M) Y) \<longleftrightarrow> |
|
912 g \<circ> Y \<in> borel_measurable (M'.vimage_algebra (space M) Y)" |
|
913 by (auto intro!: measurable_cong) |
|
914 ultimately show "Z \<in> borel_measurable (M'.vimage_algebra (space M) Y)" |
|
915 by simp } |
|
916 |
|
917 assume Z: "Z \<in> borel_measurable (M'.vimage_algebra (space M) Y)" |
|
918 with assms have "(\<lambda>x. - Z x) \<in> borel_measurable M" |
|
919 "(\<lambda>x. - Z x) \<in> borel_measurable (M'.vimage_algebra (space M) Y)" |
|
920 by auto |
|
921 from factorize_measurable_function_pos[OF assms(1,2) this] guess n .. note n = this |
|
922 from factorize_measurable_function_pos[OF assms Z] guess p .. note p = this |
|
923 let "?g x" = "p x - n x" |
|
924 show "\<exists>g\<in>borel_measurable M'. \<forall>x\<in>space M. Z x = g (Y x)" |
|
925 proof (intro bexI ballI) |
|
926 show "?g \<in> borel_measurable M'" using p n by auto |
|
927 fix x assume "x \<in> space M" |
|
928 then have "p (Y x) = max 0 (Z x)" "n (Y x) = max 0 (- Z x)" |
|
929 using p n by auto |
|
930 then show "Z x = ?g (Y x)" |
|
931 by (auto split: split_max) |
|
932 qed |
|
933 qed |
|
934 |
|
935 end |
|