38 |
38 |
39 definition (in prob_space) |
39 definition (in prob_space) |
40 "indep_families F G \<longleftrightarrow> (\<forall> A \<in> F. \<forall> B \<in> G. indep A B)" |
40 "indep_families F G \<longleftrightarrow> (\<forall> A \<in> F. \<forall> B \<in> G. indep A B)" |
41 |
41 |
42 definition (in prob_space) |
42 definition (in prob_space) |
43 "distribution X = (\<lambda>s. \<mu> ((X -` s) \<inter> (space M)))" |
43 "distribution X A = \<mu>' (X -` A \<inter> space M)" |
44 |
44 |
45 abbreviation (in prob_space) |
45 abbreviation (in prob_space) |
46 "joint_distribution X Y \<equiv> distribution (\<lambda>x. (X x, Y x))" |
46 "joint_distribution X Y \<equiv> distribution (\<lambda>x. (X x, Y x))" |
|
47 |
|
48 declare (in finite_measure) positive_measure'[intro, simp] |
47 |
49 |
48 lemma (in prob_space) distribution_cong: |
50 lemma (in prob_space) distribution_cong: |
49 assumes "\<And>x. x \<in> space M \<Longrightarrow> X x = Y x" |
51 assumes "\<And>x. x \<in> space M \<Longrightarrow> X x = Y x" |
50 shows "distribution X = distribution Y" |
52 shows "distribution X = distribution Y" |
51 unfolding distribution_def fun_eq_iff |
53 unfolding distribution_def fun_eq_iff |
52 using assms by (auto intro!: arg_cong[where f="\<mu>"]) |
54 using assms by (auto intro!: arg_cong[where f="\<mu>'"]) |
53 |
55 |
54 lemma (in prob_space) joint_distribution_cong: |
56 lemma (in prob_space) joint_distribution_cong: |
55 assumes "\<And>x. x \<in> space M \<Longrightarrow> X x = X' x" |
57 assumes "\<And>x. x \<in> space M \<Longrightarrow> X x = X' x" |
56 assumes "\<And>x. x \<in> space M \<Longrightarrow> Y x = Y' x" |
58 assumes "\<And>x. x \<in> space M \<Longrightarrow> Y x = Y' x" |
57 shows "joint_distribution X Y = joint_distribution X' Y'" |
59 shows "joint_distribution X Y = joint_distribution X' Y'" |
58 unfolding distribution_def fun_eq_iff |
60 unfolding distribution_def fun_eq_iff |
59 using assms by (auto intro!: arg_cong[where f="\<mu>"]) |
61 using assms by (auto intro!: arg_cong[where f="\<mu>'"]) |
60 |
62 |
61 lemma (in prob_space) distribution_id[simp]: |
63 lemma (in prob_space) distribution_id[simp]: |
62 assumes "N \<in> sets M" shows "distribution (\<lambda>x. x) N = \<mu> N" |
64 "N \<in> events \<Longrightarrow> distribution (\<lambda>x. x) N = prob N" |
63 using assms by (auto simp: distribution_def intro!: arg_cong[where f=\<mu>]) |
65 by (auto simp: distribution_def intro!: arg_cong[where f=prob]) |
64 |
66 |
65 lemma (in prob_space) prob_space: "prob (space M) = 1" |
67 lemma (in prob_space) prob_space: "prob (space M) = 1" |
66 unfolding measure_space_1 by simp |
68 using measure_space_1 unfolding \<mu>'_def by (simp add: one_extreal_def) |
67 |
69 |
68 lemma (in prob_space) measure_le_1[simp, intro]: |
70 lemma (in prob_space) prob_le_1[simp, intro]: "prob A \<le> 1" |
69 assumes "A \<in> events" shows "\<mu> A \<le> 1" |
71 using bounded_measure[of A] by (simp add: prob_space) |
70 proof - |
72 |
71 have "\<mu> A \<le> \<mu> (space M)" |
73 lemma (in prob_space) distribution_positive[simp, intro]: |
72 using assms sets_into_space by(auto intro!: measure_mono) |
74 "0 \<le> distribution X A" unfolding distribution_def by auto |
73 also note measure_space_1 |
75 |
74 finally show ?thesis . |
76 lemma (in prob_space) joint_distribution_remove[simp]: |
75 qed |
77 "joint_distribution X X {(x, x)} = distribution X {x}" |
|
78 unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>']) |
|
79 |
|
80 lemma (in prob_space) distribution_1: |
|
81 "distribution X A \<le> 1" |
|
82 unfolding distribution_def by simp |
76 |
83 |
77 lemma (in prob_space) prob_compl: |
84 lemma (in prob_space) prob_compl: |
78 assumes "A \<in> events" |
85 assumes A: "A \<in> events" |
79 shows "prob (space M - A) = 1 - prob A" |
86 shows "prob (space M - A) = 1 - prob A" |
80 using `A \<in> events`[THEN sets_into_space] `A \<in> events` measure_space_1 |
87 using finite_measure_compl[OF A] by (simp add: prob_space) |
81 by (subst real_finite_measure_Diff) auto |
88 |
82 |
89 lemma (in prob_space) indep_space: "s \<in> events \<Longrightarrow> indep (space M) s" |
83 lemma (in prob_space) indep_space: |
90 by (simp add: indep_def prob_space) |
84 assumes "s \<in> events" |
|
85 shows "indep (space M) s" |
|
86 using assms prob_space by (simp add: indep_def) |
|
87 |
91 |
88 lemma (in prob_space) prob_space_increasing: "increasing M prob" |
92 lemma (in prob_space) prob_space_increasing: "increasing M prob" |
89 by (auto intro!: real_measure_mono simp: increasing_def) |
93 by (auto intro!: finite_measure_mono simp: increasing_def) |
90 |
94 |
91 lemma (in prob_space) prob_zero_union: |
95 lemma (in prob_space) prob_zero_union: |
92 assumes "s \<in> events" "t \<in> events" "prob t = 0" |
96 assumes "s \<in> events" "t \<in> events" "prob t = 0" |
93 shows "prob (s \<union> t) = prob s" |
97 shows "prob (s \<union> t) = prob s" |
94 using assms |
98 using assms |
95 proof - |
99 proof - |
96 have "prob (s \<union> t) \<le> prob s" |
100 have "prob (s \<union> t) \<le> prob s" |
97 using real_finite_measure_subadditive[of s t] assms by auto |
101 using finite_measure_subadditive[of s t] assms by auto |
98 moreover have "prob (s \<union> t) \<ge> prob s" |
102 moreover have "prob (s \<union> t) \<ge> prob s" |
99 using assms by (blast intro: real_measure_mono) |
103 using assms by (blast intro: finite_measure_mono) |
100 ultimately show ?thesis by simp |
104 ultimately show ?thesis by simp |
101 qed |
105 qed |
102 |
106 |
103 lemma (in prob_space) prob_eq_compl: |
107 lemma (in prob_space) prob_eq_compl: |
104 assumes "s \<in> events" "t \<in> events" |
108 assumes "s \<in> events" "t \<in> events" |
180 proof - |
183 proof - |
181 have e: "e = (\<Union> i \<in> s. e \<inter> f i)" |
184 have e: "e = (\<Union> i \<in> s. e \<inter> f i)" |
182 using `e \<in> events` sets_into_space upper by blast |
185 using `e \<in> events` sets_into_space upper by blast |
183 hence "prob e = prob (\<Union> i \<in> s. e \<inter> f i)" by simp |
186 hence "prob e = prob (\<Union> i \<in> s. e \<inter> f i)" by simp |
184 also have "\<dots> = (\<Sum> x \<in> s. prob (e \<inter> f x))" |
187 also have "\<dots> = (\<Sum> x \<in> s. prob (e \<inter> f x))" |
185 proof (rule real_finite_measure_finite_Union) |
188 proof (rule finite_measure_finite_Union) |
186 show "finite s" by fact |
189 show "finite s" by fact |
187 show "\<And>i. i \<in> s \<Longrightarrow> e \<inter> f i \<in> events" by fact |
190 show "\<And>i. i \<in> s \<Longrightarrow> e \<inter> f i \<in> events" by fact |
188 show "disjoint_family_on (\<lambda>i. e \<inter> f i) s" |
191 show "disjoint_family_on (\<lambda>i. e \<inter> f i) s" |
189 using disjoint by (auto simp: disjoint_family_on_def) |
192 using disjoint by (auto simp: disjoint_family_on_def) |
190 qed |
193 qed |
191 finally show ?thesis . |
194 finally show ?thesis . |
192 qed |
195 qed |
193 |
196 |
194 lemma (in prob_space) distribution_prob_space: |
197 lemma (in prob_space) distribution_prob_space: |
195 assumes "random_variable S X" |
198 assumes "random_variable S X" |
196 shows "prob_space (S\<lparr>measure := distribution X\<rparr>)" |
199 shows "prob_space (S\<lparr>measure := extreal \<circ> distribution X\<rparr>)" |
197 proof - |
200 proof - |
198 interpret S: measure_space "S\<lparr>measure := distribution X\<rparr>" |
201 interpret S: measure_space "S\<lparr>measure := extreal \<circ> distribution X\<rparr>" |
199 unfolding distribution_def using assms |
202 proof (rule measure_space.measure_space_cong) |
200 by (intro measure_space_vimage) |
203 show "measure_space (S\<lparr> measure := \<lambda>A. \<mu> (X -` A \<inter> space M) \<rparr>)" |
201 (auto intro!: sigma_algebra.sigma_algebra_cong[of S] simp: measure_preserving_def) |
204 using assms by (auto intro!: measure_space_vimage simp: measure_preserving_def) |
|
205 qed (insert assms, auto simp add: finite_measure_eq distribution_def measurable_sets) |
202 show ?thesis |
206 show ?thesis |
203 proof (default, simp) |
207 proof (default, simp) |
204 have "X -` space S \<inter> space M = space M" |
208 have "X -` space S \<inter> space M = space M" |
205 using `random_variable S X` by (auto simp: measurable_def) |
209 using `random_variable S X` by (auto simp: measurable_def) |
206 then show "distribution X (space S) = 1" |
210 then show "extreal (distribution X (space S)) = 1" |
207 using measure_space_1 by (simp add: distribution_def) |
211 by (simp add: distribution_def one_extreal_def prob_space) |
208 qed |
212 qed |
209 qed |
213 qed |
210 |
214 |
211 lemma (in prob_space) AE_distribution: |
215 lemma (in prob_space) AE_distribution: |
212 assumes X: "random_variable MX X" and "measure_space.almost_everywhere (MX\<lparr>measure := distribution X\<rparr>) (\<lambda>x. Q x)" |
216 assumes X: "random_variable MX X" and "AE x in MX\<lparr>measure := extreal \<circ> distribution X\<rparr>. Q x" |
213 shows "AE x. Q (X x)" |
217 shows "AE x. Q (X x)" |
214 proof - |
218 proof - |
215 interpret X: prob_space "MX\<lparr>measure := distribution X\<rparr>" using X by (rule distribution_prob_space) |
219 interpret X: prob_space "MX\<lparr>measure := extreal \<circ> distribution X\<rparr>" using X by (rule distribution_prob_space) |
216 obtain N where N: "N \<in> sets MX" "distribution X N = 0" "{x\<in>space MX. \<not> Q x} \<subseteq> N" |
220 obtain N where N: "N \<in> sets MX" "distribution X N = 0" "{x\<in>space MX. \<not> Q x} \<subseteq> N" |
217 using assms unfolding X.almost_everywhere_def by auto |
221 using assms unfolding X.almost_everywhere_def by auto |
218 show "AE x. Q (X x)" |
222 from X[unfolded measurable_def] N show "AE x. Q (X x)" |
219 using X[unfolded measurable_def] N unfolding distribution_def |
223 by (intro AE_I'[where N="X -` N \<inter> space M"]) |
220 by (intro AE_I'[where N="X -` N \<inter> space M"]) auto |
224 (auto simp: finite_measure_eq distribution_def measurable_sets) |
221 qed |
225 qed |
222 |
226 |
223 lemma (in prob_space) distribution_lebesgue_thm1: |
227 lemma (in prob_space) distribution_eq_integral: |
224 assumes "random_variable s X" |
228 "random_variable S X \<Longrightarrow> A \<in> sets S \<Longrightarrow> distribution X A = expectation (indicator (X -` A \<inter> space M))" |
225 assumes "A \<in> sets s" |
229 using finite_measure_eq[of "X -` A \<inter> space M"] |
226 shows "real (distribution X A) = expectation (indicator (X -` A \<inter> space M))" |
230 by (auto simp: measurable_sets distribution_def) |
227 unfolding distribution_def |
231 |
228 using assms unfolding measurable_def |
232 lemma (in prob_space) distribution_eq_translated_integral: |
229 using integral_indicator by auto |
233 assumes "random_variable S X" "A \<in> sets S" |
230 |
234 shows "distribution X A = integral\<^isup>P (S\<lparr>measure := extreal \<circ> distribution X\<rparr>) (indicator A)" |
231 lemma (in prob_space) distribution_lebesgue_thm2: |
235 proof - |
232 assumes "random_variable S X" and "A \<in> sets S" |
236 interpret S: prob_space "S\<lparr>measure := extreal \<circ> distribution X\<rparr>" |
233 shows "distribution X A = integral\<^isup>P (S\<lparr>measure := distribution X\<rparr>) (indicator A)" |
|
234 proof - |
|
235 interpret S: prob_space "S\<lparr>measure := distribution X\<rparr>" |
|
236 using assms(1) by (rule distribution_prob_space) |
237 using assms(1) by (rule distribution_prob_space) |
237 show ?thesis |
238 show ?thesis |
238 using S.positive_integral_indicator(1) |
239 using S.positive_integral_indicator(1)[of A] assms by simp |
239 using assms unfolding distribution_def by auto |
|
240 qed |
240 qed |
241 |
241 |
242 lemma (in prob_space) finite_expectation1: |
242 lemma (in prob_space) finite_expectation1: |
243 assumes f: "finite (X`space M)" and rv: "random_variable borel X" |
243 assumes f: "finite (X`space M)" and rv: "random_variable borel X" |
244 shows "expectation X = (\<Sum> r \<in> X ` space M. r * prob (X -` {r} \<inter> space M))" |
244 shows "expectation X = (\<Sum>r \<in> X ` space M. r * prob (X -` {r} \<inter> space M))" (is "_ = ?r") |
245 proof (rule integral_on_finite(2)[OF rv[THEN conjunct2] f]) |
245 proof (subst integral_on_finite) |
246 fix x have "X -` {x} \<inter> space M \<in> sets M" |
246 show "X \<in> borel_measurable M" "finite (X`space M)" using assms by auto |
247 using rv unfolding measurable_def by auto |
247 show "(\<Sum> r \<in> X ` space M. r * real (\<mu> (X -` {r} \<inter> space M))) = ?r" |
248 thus "\<mu> (X -` {x} \<inter> space M) \<noteq> \<omega>" using finite_measure by simp |
248 "\<And>x. \<mu> (X -` {x} \<inter> space M) \<noteq> \<infinity>" |
|
249 using finite_measure_eq[OF borel_measurable_vimage, of X] rv by auto |
249 qed |
250 qed |
250 |
251 |
251 lemma (in prob_space) finite_expectation: |
252 lemma (in prob_space) finite_expectation: |
252 assumes "finite (X`space M)" "random_variable borel X" |
253 assumes "finite (X`space M)" "random_variable borel X" |
253 shows "expectation X = (\<Sum> r \<in> X ` (space M). r * real (distribution X {r}))" |
254 shows "expectation X = (\<Sum> r \<in> X ` (space M). r * distribution X {r})" |
254 using assms unfolding distribution_def using finite_expectation1 by auto |
255 using assms unfolding distribution_def using finite_expectation1 by auto |
255 |
256 |
256 lemma (in prob_space) prob_x_eq_1_imp_prob_y_eq_0: |
257 lemma (in prob_space) prob_x_eq_1_imp_prob_y_eq_0: |
257 assumes "{x} \<in> events" |
258 assumes "{x} \<in> events" |
258 assumes "prob {x} = 1" |
259 assumes "prob {x} = 1" |
313 lemma (in prob_space) joint_distribution_Times_le_fst: |
309 lemma (in prob_space) joint_distribution_Times_le_fst: |
314 assumes X: "random_variable MX X" and Y: "random_variable MY Y" |
310 assumes X: "random_variable MX X" and Y: "random_variable MY Y" |
315 and A: "A \<in> sets MX" and B: "B \<in> sets MY" |
311 and A: "A \<in> sets MX" and B: "B \<in> sets MY" |
316 shows "joint_distribution X Y (A \<times> B) \<le> distribution X A" |
312 shows "joint_distribution X Y (A \<times> B) \<le> distribution X A" |
317 unfolding distribution_def |
313 unfolding distribution_def |
318 proof (intro measure_mono) |
314 proof (intro finite_measure_mono) |
319 show "(\<lambda>x. (X x, Y x)) -` (A \<times> B) \<inter> space M \<subseteq> X -` A \<inter> space M" by force |
315 show "(\<lambda>x. (X x, Y x)) -` (A \<times> B) \<inter> space M \<subseteq> X -` A \<inter> space M" by force |
320 show "X -` A \<inter> space M \<in> events" |
316 show "X -` A \<inter> space M \<in> events" |
321 using X A unfolding measurable_def by simp |
317 using X A unfolding measurable_def by simp |
322 have *: "(\<lambda>x. (X x, Y x)) -` (A \<times> B) \<inter> space M = |
318 have *: "(\<lambda>x. (X x, Y x)) -` (A \<times> B) \<inter> space M = |
323 (X -` A \<inter> space M) \<inter> (Y -` B \<inter> space M)" by auto |
319 (X -` A \<inter> space M) \<inter> (Y -` B \<inter> space M)" by auto |
324 show "(\<lambda>x. (X x, Y x)) -` (A \<times> B) \<inter> space M \<in> events" |
|
325 unfolding * apply (rule Int) |
|
326 using assms unfolding measurable_def by auto |
|
327 qed |
320 qed |
328 |
321 |
329 lemma (in prob_space) joint_distribution_commute: |
322 lemma (in prob_space) joint_distribution_commute: |
330 "joint_distribution X Y x = joint_distribution Y X ((\<lambda>(x,y). (y,x))`x)" |
323 "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>]) |
324 unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>']) |
332 |
325 |
333 lemma (in prob_space) joint_distribution_Times_le_snd: |
326 lemma (in prob_space) joint_distribution_Times_le_snd: |
334 assumes X: "random_variable MX X" and Y: "random_variable MY Y" |
327 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" |
328 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" |
329 shows "joint_distribution X Y (A \<times> B) \<le> distribution Y B" |
350 have sa: "sigma_algebra M" by default |
343 have sa: "sigma_algebra M" by default |
351 show "(\<lambda>x. (X x, Y x)) \<in> measurable M (MX \<Otimes>\<^isub>M MY)" |
344 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) |
345 unfolding P.measurable_pair_iff[OF sa] using assms by (simp add: comp_def) |
353 qed |
346 qed |
354 |
347 |
355 lemma (in prob_space) distribution_order: |
|
356 assumes "random_variable MX X" "random_variable MY Y" |
|
357 assumes "{x} \<in> sets MX" "{y} \<in> sets MY" |
|
358 shows "r \<le> joint_distribution X Y {(x, y)} \<Longrightarrow> r \<le> distribution X {x}" |
|
359 and "r \<le> joint_distribution X Y {(x, y)} \<Longrightarrow> r \<le> distribution Y {y}" |
|
360 and "r < joint_distribution X Y {(x, y)} \<Longrightarrow> r < distribution X {x}" |
|
361 and "r < joint_distribution X Y {(x, y)} \<Longrightarrow> r < distribution Y {y}" |
|
362 and "distribution X {x} = 0 \<Longrightarrow> joint_distribution X Y {(x, y)} = 0" |
|
363 and "distribution Y {y} = 0 \<Longrightarrow> joint_distribution X Y {(x, y)} = 0" |
|
364 using joint_distribution_Times_le_snd[OF assms] |
|
365 using joint_distribution_Times_le_fst[OF assms] |
|
366 by auto |
|
367 |
|
368 lemma (in prob_space) joint_distribution_commute_singleton: |
348 lemma (in prob_space) joint_distribution_commute_singleton: |
369 "joint_distribution X Y {(x, y)} = joint_distribution Y X {(y, x)}" |
349 "joint_distribution X Y {(x, y)} = joint_distribution Y X {(y, x)}" |
370 unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>]) |
350 unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>']) |
371 |
351 |
372 lemma (in prob_space) joint_distribution_assoc_singleton: |
352 lemma (in prob_space) joint_distribution_assoc_singleton: |
373 "joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)} = |
353 "joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)} = |
374 joint_distribution (\<lambda>x. (X x, Y x)) Z {((x, y), z)}" |
354 joint_distribution (\<lambda>x. (X x, Y x)) Z {((x, y), z)}" |
375 unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>]) |
355 unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>']) |
376 |
356 |
377 locale pair_prob_space = M1: prob_space M1 + M2: prob_space M2 for M1 M2 |
357 locale pair_prob_space = M1: prob_space M1 + M2: prob_space M2 for M1 M2 |
378 |
358 |
379 sublocale pair_prob_space \<subseteq> pair_sigma_finite M1 M2 by default |
359 sublocale pair_prob_space \<subseteq> pair_sigma_finite M1 M2 by default |
380 |
360 |
381 sublocale pair_prob_space \<subseteq> P: prob_space P |
361 sublocale pair_prob_space \<subseteq> P: prob_space P |
382 by default (simp add: pair_measure_times M1.measure_space_1 M2.measure_space_1 space_pair_measure) |
362 by default (simp add: pair_measure_times M1.measure_space_1 M2.measure_space_1 space_pair_measure) |
383 |
363 |
384 lemma countably_additiveI[case_names countably]: |
364 lemma countably_additiveI[case_names countably]: |
385 assumes "\<And>A. \<lbrakk> range A \<subseteq> sets M ; disjoint_family A ; (\<Union>i. A i) \<in> sets M\<rbrakk> \<Longrightarrow> |
365 assumes "\<And>A. \<lbrakk> range A \<subseteq> sets M ; disjoint_family A ; (\<Union>i. A i) \<in> sets M\<rbrakk> \<Longrightarrow> |
386 (\<Sum>\<^isub>\<infinity>n. \<mu> (A n)) = \<mu> (\<Union>i. A i)" |
366 (\<Sum>n. \<mu> (A n)) = \<mu> (\<Union>i. A i)" |
387 shows "countably_additive M \<mu>" |
367 shows "countably_additive M \<mu>" |
388 using assms unfolding countably_additive_def by auto |
368 using assms unfolding countably_additive_def by auto |
389 |
369 |
390 lemma (in prob_space) joint_distribution_prob_space: |
370 lemma (in prob_space) joint_distribution_prob_space: |
391 assumes "random_variable MX X" "random_variable MY Y" |
371 assumes "random_variable MX X" "random_variable MY Y" |
392 shows "prob_space ((MX \<Otimes>\<^isub>M MY) \<lparr> measure := joint_distribution X Y\<rparr>)" |
372 shows "prob_space ((MX \<Otimes>\<^isub>M MY) \<lparr> measure := extreal \<circ> joint_distribution X Y\<rparr>)" |
393 using random_variable_pairI[OF assms] by (rule distribution_prob_space) |
373 using random_variable_pairI[OF assms] by (rule distribution_prob_space) |
394 |
374 |
395 section "Probability spaces on finite sets" |
375 section "Probability spaces on finite sets" |
396 |
376 |
397 locale finite_prob_space = prob_space + finite_measure_space |
377 locale finite_prob_space = prob_space + finite_measure_space |
490 |
463 |
491 lemma (in prob_space) joint_distribution_finite_Times_le_fst: |
464 lemma (in prob_space) joint_distribution_finite_Times_le_fst: |
492 assumes X: "finite_random_variable MX X" and Y: "finite_random_variable MY Y" |
465 assumes X: "finite_random_variable MX X" and Y: "finite_random_variable MY Y" |
493 shows "joint_distribution X Y (A \<times> B) \<le> distribution X A" |
466 shows "joint_distribution X Y (A \<times> B) \<le> distribution X A" |
494 unfolding distribution_def |
467 unfolding distribution_def |
495 proof (intro measure_mono) |
468 proof (intro finite_measure_mono) |
496 show "(\<lambda>x. (X x, Y x)) -` (A \<times> B) \<inter> space M \<subseteq> X -` A \<inter> space M" by force |
469 show "(\<lambda>x. (X x, Y x)) -` (A \<times> B) \<inter> space M \<subseteq> X -` A \<inter> space M" by force |
497 show "X -` A \<inter> space M \<in> events" |
470 show "X -` A \<inter> space M \<in> events" |
498 using finite_random_variable_vimage[OF X] . |
471 using finite_random_variable_measurable[OF X] . |
499 have *: "(\<lambda>x. (X x, Y x)) -` (A \<times> B) \<inter> space M = |
472 have *: "(\<lambda>x. (X x, Y x)) -` (A \<times> B) \<inter> space M = |
500 (X -` A \<inter> space M) \<inter> (Y -` B \<inter> space M)" by auto |
473 (X -` A \<inter> space M) \<inter> (Y -` B \<inter> space M)" by auto |
501 show "(\<lambda>x. (X x, Y x)) -` (A \<times> B) \<inter> space M \<in> events" |
|
502 unfolding * apply (rule Int) |
|
503 using assms[THEN finite_random_variable_vimage] by auto |
|
504 qed |
474 qed |
505 |
475 |
506 lemma (in prob_space) joint_distribution_finite_Times_le_snd: |
476 lemma (in prob_space) joint_distribution_finite_Times_le_snd: |
507 assumes X: "finite_random_variable MX X" and Y: "finite_random_variable MY Y" |
477 assumes X: "finite_random_variable MX X" and Y: "finite_random_variable MY Y" |
508 shows "joint_distribution X Y (A \<times> B) \<le> distribution Y B" |
478 shows "joint_distribution X Y (A \<times> B) \<le> distribution Y B" |
509 using assms |
479 using assms |
510 by (subst joint_distribution_commute) |
480 by (subst joint_distribution_commute) |
511 (simp add: swap_product joint_distribution_finite_Times_le_fst) |
481 (simp add: swap_product joint_distribution_finite_Times_le_fst) |
512 |
482 |
513 lemma (in prob_space) finite_distribution_order: |
483 lemma (in prob_space) finite_distribution_order: |
|
484 fixes MX :: "('c, 'd) measure_space_scheme" and MY :: "('e, 'f) measure_space_scheme" |
514 assumes "finite_random_variable MX X" "finite_random_variable MY Y" |
485 assumes "finite_random_variable MX X" "finite_random_variable MY Y" |
515 shows "r \<le> joint_distribution X Y {(x, y)} \<Longrightarrow> r \<le> distribution X {x}" |
486 shows "r \<le> joint_distribution X Y {(x, y)} \<Longrightarrow> r \<le> distribution X {x}" |
516 and "r \<le> joint_distribution X Y {(x, y)} \<Longrightarrow> r \<le> distribution Y {y}" |
487 and "r \<le> joint_distribution X Y {(x, y)} \<Longrightarrow> r \<le> distribution Y {y}" |
517 and "r < joint_distribution X Y {(x, y)} \<Longrightarrow> r < distribution X {x}" |
488 and "r < joint_distribution X Y {(x, y)} \<Longrightarrow> r < distribution X {x}" |
518 and "r < joint_distribution X Y {(x, y)} \<Longrightarrow> r < distribution Y {y}" |
489 and "r < joint_distribution X Y {(x, y)} \<Longrightarrow> r < distribution Y {y}" |
519 and "distribution X {x} = 0 \<Longrightarrow> joint_distribution X Y {(x, y)} = 0" |
490 and "distribution X {x} = 0 \<Longrightarrow> joint_distribution X Y {(x, y)} = 0" |
520 and "distribution Y {y} = 0 \<Longrightarrow> joint_distribution X Y {(x, y)} = 0" |
491 and "distribution Y {y} = 0 \<Longrightarrow> joint_distribution X Y {(x, y)} = 0" |
521 using joint_distribution_finite_Times_le_snd[OF assms, of "{x}" "{y}"] |
492 using joint_distribution_finite_Times_le_snd[OF assms, of "{x}" "{y}"] |
522 using joint_distribution_finite_Times_le_fst[OF assms, of "{x}" "{y}"] |
493 using joint_distribution_finite_Times_le_fst[OF assms, of "{x}" "{y}"] |
523 by auto |
494 by (auto intro: antisym) |
524 |
|
525 lemma (in prob_space) finite_distribution_finite: |
|
526 assumes "finite_random_variable M' X" |
|
527 shows "distribution X {x} \<noteq> \<omega>" |
|
528 proof - |
|
529 have "distribution X {x} \<le> \<mu> (space M)" |
|
530 unfolding distribution_def |
|
531 using finite_random_variable_vimage[OF assms] |
|
532 by (intro measure_mono) auto |
|
533 then show ?thesis |
|
534 by auto |
|
535 qed |
|
536 |
495 |
537 lemma (in prob_space) setsum_joint_distribution: |
496 lemma (in prob_space) setsum_joint_distribution: |
538 assumes X: "finite_random_variable MX X" |
497 assumes X: "finite_random_variable MX X" |
539 assumes Y: "random_variable MY Y" "B \<in> sets MY" |
498 assumes Y: "random_variable MY Y" "B \<in> sets MY" |
540 shows "(\<Sum>a\<in>space MX. joint_distribution X Y ({a} \<times> B)) = distribution Y B" |
499 shows "(\<Sum>a\<in>space MX. joint_distribution X Y ({a} \<times> B)) = distribution Y B" |
541 unfolding distribution_def |
500 unfolding distribution_def |
542 proof (subst measure_finitely_additive'') |
501 proof (subst finite_measure_finite_Union[symmetric]) |
543 interpret MX: finite_sigma_algebra MX using X by auto |
502 interpret MX: finite_sigma_algebra MX using X by auto |
544 show "finite (space MX)" using MX.finite_space . |
503 show "finite (space MX)" using MX.finite_space . |
545 let "?d i" = "(\<lambda>x. (X x, Y x)) -` ({i} \<times> B) \<inter> space M" |
504 let "?d i" = "(\<lambda>x. (X x, Y x)) -` ({i} \<times> B) \<inter> space M" |
546 { fix i assume "i \<in> space MX" |
505 { fix i assume "i \<in> space MX" |
547 moreover have "?d i = (X -` {i} \<inter> space M) \<inter> (Y -` B \<inter> space M)" by auto |
506 moreover have "?d i = (X -` {i} \<inter> space M) \<inter> (Y -` B \<inter> space M)" by auto |
548 ultimately show "?d i \<in> events" |
507 ultimately show "?d i \<in> events" |
549 using measurable_sets[of X M MX] measurable_sets[of Y M MY B] X Y |
508 using measurable_sets[of X M MX] measurable_sets[of Y M MY B] X Y |
550 using MX.sets_eq_Pow by auto } |
509 using MX.sets_eq_Pow by auto } |
551 show "disjoint_family_on ?d (space MX)" by (auto simp: disjoint_family_on_def) |
510 show "disjoint_family_on ?d (space MX)" by (auto simp: disjoint_family_on_def) |
552 show "\<mu> (\<Union>i\<in>space MX. ?d i) = \<mu> (Y -` B \<inter> space M)" |
511 show "\<mu>' (\<Union>i\<in>space MX. ?d i) = \<mu>' (Y -` B \<inter> space M)" |
553 using X[unfolded measurable_def] |
512 using X[unfolded measurable_def] by (auto intro!: arg_cong[where f=\<mu>']) |
554 by (auto intro!: arg_cong[where f=\<mu>]) |
|
555 qed |
513 qed |
556 |
514 |
557 lemma (in prob_space) setsum_joint_distribution_singleton: |
515 lemma (in prob_space) setsum_joint_distribution_singleton: |
558 assumes X: "finite_random_variable MX X" |
516 assumes X: "finite_random_variable MX X" |
559 assumes Y: "finite_random_variable MY Y" "b \<in> space MY" |
517 assumes Y: "finite_random_variable MY Y" "b \<in> space MY" |
560 shows "(\<Sum>a\<in>space MX. joint_distribution X Y {(a, b)}) = distribution Y {b}" |
518 shows "(\<Sum>a\<in>space MX. joint_distribution X Y {(a, b)}) = distribution Y {b}" |
561 using setsum_joint_distribution[OF X |
519 using setsum_joint_distribution[OF X |
562 finite_random_variableD[OF Y(1)] |
520 finite_random_variableD[OF Y(1)] |
563 finite_random_variable_imp_sets[OF Y]] by simp |
521 finite_random_variable_imp_sets[OF Y]] by simp |
564 |
522 |
565 lemma (in prob_space) setsum_real_joint_distribution: |
|
566 fixes MX :: "('c, 'x) measure_space_scheme" and MY :: "('d, 'y) measure_space_scheme" |
|
567 assumes X: "finite_random_variable MX X" |
|
568 assumes Y: "random_variable MY Y" "B \<in> sets MY" |
|
569 shows "(\<Sum>a\<in>space MX. real (joint_distribution X Y ({a} \<times> B))) = real (distribution Y B)" |
|
570 proof - |
|
571 interpret MX: finite_sigma_algebra MX using X by auto |
|
572 show ?thesis |
|
573 unfolding setsum_joint_distribution[OF assms, symmetric] |
|
574 using distribution_finite[OF random_variable_pairI[OF finite_random_variableD[OF X] Y(1)]] Y(2) |
|
575 by (simp add: space_pair_measure real_of_pextreal_setsum) |
|
576 qed |
|
577 |
|
578 lemma (in prob_space) setsum_real_joint_distribution_singleton: |
|
579 fixes MX :: "('c, 'x) measure_space_scheme" and MY :: "('d, 'y) measure_space_scheme" |
|
580 assumes X: "finite_random_variable MX X" |
|
581 assumes Y: "finite_random_variable MY Y" "b \<in> space MY" |
|
582 shows "(\<Sum>a\<in>space MX. real (joint_distribution X Y {(a,b)})) = real (distribution Y {b})" |
|
583 using setsum_real_joint_distribution[OF X |
|
584 finite_random_variableD[OF Y(1)] |
|
585 finite_random_variable_imp_sets[OF Y]] by simp |
|
586 |
|
587 locale pair_finite_prob_space = M1: finite_prob_space M1 + M2: finite_prob_space M2 for M1 M2 |
523 locale pair_finite_prob_space = M1: finite_prob_space M1 + M2: finite_prob_space M2 for M1 M2 |
588 |
524 |
589 sublocale pair_finite_prob_space \<subseteq> pair_prob_space M1 M2 by default |
525 sublocale pair_finite_prob_space \<subseteq> pair_prob_space M1 M2 by default |
590 sublocale pair_finite_prob_space \<subseteq> pair_finite_space M1 M2 by default |
526 sublocale pair_finite_prob_space \<subseteq> pair_finite_space M1 M2 by default |
591 sublocale pair_finite_prob_space \<subseteq> finite_prob_space P by default |
527 sublocale pair_finite_prob_space \<subseteq> finite_prob_space P by default |
592 |
528 |
593 lemma (in prob_space) joint_distribution_finite_prob_space: |
529 lemma (in prob_space) joint_distribution_finite_prob_space: |
594 assumes X: "finite_random_variable MX X" |
530 assumes X: "finite_random_variable MX X" |
595 assumes Y: "finite_random_variable MY Y" |
531 assumes Y: "finite_random_variable MY Y" |
596 shows "finite_prob_space ((MX \<Otimes>\<^isub>M MY)\<lparr> measure := joint_distribution X Y\<rparr>)" |
532 shows "finite_prob_space ((MX \<Otimes>\<^isub>M MY)\<lparr> measure := extreal \<circ> joint_distribution X Y\<rparr>)" |
597 by (intro distribution_finite_prob_space finite_random_variable_pairI X Y) |
533 by (intro distribution_finite_prob_space finite_random_variable_pairI X Y) |
598 |
534 |
599 lemma finite_prob_space_eq: |
535 lemma finite_prob_space_eq: |
600 "finite_prob_space M \<longleftrightarrow> finite_measure_space M \<and> measure M (space M) = 1" |
536 "finite_prob_space M \<longleftrightarrow> finite_measure_space M \<and> measure M (space M) = 1" |
601 unfolding finite_prob_space_def finite_measure_space_def prob_space_def prob_space_axioms_def |
537 unfolding finite_prob_space_def finite_measure_space_def prob_space_def prob_space_axioms_def |
602 by auto |
538 by auto |
603 |
539 |
604 lemma (in prob_space) not_empty: "space M \<noteq> {}" |
540 lemma (in prob_space) not_empty: "space M \<noteq> {}" |
605 using prob_space empty_measure by auto |
541 using prob_space empty_measure' by auto |
606 |
542 |
607 lemma (in finite_prob_space) sum_over_space_eq_1: "(\<Sum>x\<in>space M. \<mu> {x}) = 1" |
543 lemma (in finite_prob_space) sum_over_space_eq_1: "(\<Sum>x\<in>space M. \<mu> {x}) = 1" |
608 using measure_space_1 sum_over_space by simp |
544 using measure_space_1 sum_over_space by simp |
609 |
|
610 lemma (in finite_prob_space) positive_distribution: "0 \<le> distribution X x" |
|
611 unfolding distribution_def by simp |
|
612 |
545 |
613 lemma (in finite_prob_space) joint_distribution_restriction_fst: |
546 lemma (in finite_prob_space) joint_distribution_restriction_fst: |
614 "joint_distribution X Y A \<le> distribution X (fst ` A)" |
547 "joint_distribution X Y A \<le> distribution X (fst ` A)" |
615 unfolding distribution_def |
548 unfolding distribution_def |
616 proof (safe intro!: measure_mono) |
549 proof (safe intro!: finite_measure_mono) |
617 fix x assume "x \<in> space M" and *: "(X x, Y x) \<in> A" |
550 fix x assume "x \<in> space M" and *: "(X x, Y x) \<in> A" |
618 show "x \<in> X -` fst ` A" |
551 show "x \<in> X -` fst ` A" |
619 by (auto intro!: image_eqI[OF _ *]) |
552 by (auto intro!: image_eqI[OF _ *]) |
620 qed (simp_all add: sets_eq_Pow) |
553 qed (simp_all add: sets_eq_Pow) |
621 |
554 |
622 lemma (in finite_prob_space) joint_distribution_restriction_snd: |
555 lemma (in finite_prob_space) joint_distribution_restriction_snd: |
623 "joint_distribution X Y A \<le> distribution Y (snd ` A)" |
556 "joint_distribution X Y A \<le> distribution Y (snd ` A)" |
624 unfolding distribution_def |
557 unfolding distribution_def |
625 proof (safe intro!: measure_mono) |
558 proof (safe intro!: finite_measure_mono) |
626 fix x assume "x \<in> space M" and *: "(X x, Y x) \<in> A" |
559 fix x assume "x \<in> space M" and *: "(X x, Y x) \<in> A" |
627 show "x \<in> Y -` snd ` A" |
560 show "x \<in> Y -` snd ` A" |
628 by (auto intro!: image_eqI[OF _ *]) |
561 by (auto intro!: image_eqI[OF _ *]) |
629 qed (simp_all add: sets_eq_Pow) |
562 qed (simp_all add: sets_eq_Pow) |
630 |
563 |
635 and "r \<le> joint_distribution X Y {(x, y)} \<Longrightarrow> r \<le> distribution Y {y}" |
568 and "r \<le> joint_distribution X Y {(x, y)} \<Longrightarrow> r \<le> distribution Y {y}" |
636 and "r < joint_distribution X Y {(x, y)} \<Longrightarrow> r < distribution X {x}" |
569 and "r < joint_distribution X Y {(x, y)} \<Longrightarrow> r < distribution X {x}" |
637 and "r < joint_distribution X Y {(x, y)} \<Longrightarrow> r < distribution Y {y}" |
570 and "r < joint_distribution X Y {(x, y)} \<Longrightarrow> r < distribution Y {y}" |
638 and "distribution X {x} = 0 \<Longrightarrow> joint_distribution X Y {(x, y)} = 0" |
571 and "distribution X {x} = 0 \<Longrightarrow> joint_distribution X Y {(x, y)} = 0" |
639 and "distribution Y {y} = 0 \<Longrightarrow> joint_distribution X Y {(x, y)} = 0" |
572 and "distribution Y {y} = 0 \<Longrightarrow> joint_distribution X Y {(x, y)} = 0" |
640 using positive_distribution[of X x'] |
573 using |
641 positive_distribution[of "\<lambda>x. (X x, Y x)" "{(x, y)}"] |
|
642 joint_distribution_restriction_fst[of X Y "{(x, y)}"] |
574 joint_distribution_restriction_fst[of X Y "{(x, y)}"] |
643 joint_distribution_restriction_snd[of X Y "{(x, y)}"] |
575 joint_distribution_restriction_snd[of X Y "{(x, y)}"] |
644 by auto |
576 by (auto intro: antisym) |
645 |
577 |
646 lemma (in finite_prob_space) distribution_mono: |
578 lemma (in finite_prob_space) distribution_mono: |
647 assumes "\<And>t. \<lbrakk> t \<in> space M ; X t \<in> x \<rbrakk> \<Longrightarrow> Y t \<in> y" |
579 assumes "\<And>t. \<lbrakk> t \<in> space M ; X t \<in> x \<rbrakk> \<Longrightarrow> Y t \<in> y" |
648 shows "distribution X x \<le> distribution Y y" |
580 shows "distribution X x \<le> distribution Y y" |
649 unfolding distribution_def |
581 unfolding distribution_def |
650 using assms by (auto simp: sets_eq_Pow intro!: measure_mono) |
582 using assms by (auto simp: sets_eq_Pow intro!: finite_measure_mono) |
651 |
583 |
652 lemma (in finite_prob_space) distribution_mono_gt_0: |
584 lemma (in finite_prob_space) distribution_mono_gt_0: |
653 assumes gt_0: "0 < distribution X x" |
585 assumes gt_0: "0 < distribution X x" |
654 assumes *: "\<And>t. \<lbrakk> t \<in> space M ; X t \<in> x \<rbrakk> \<Longrightarrow> Y t \<in> y" |
586 assumes *: "\<And>t. \<lbrakk> t \<in> space M ; X t \<in> x \<rbrakk> \<Longrightarrow> Y t \<in> y" |
655 shows "0 < distribution Y y" |
587 shows "0 < distribution Y y" |
656 by (rule less_le_trans[OF gt_0 distribution_mono]) (rule *) |
588 by (rule less_le_trans[OF gt_0 distribution_mono]) (rule *) |
657 |
589 |
658 lemma (in finite_prob_space) sum_over_space_distrib: |
590 lemma (in finite_prob_space) sum_over_space_distrib: |
659 "(\<Sum>x\<in>X`space M. distribution X {x}) = 1" |
591 "(\<Sum>x\<in>X`space M. distribution X {x}) = 1" |
660 unfolding distribution_def measure_space_1[symmetric] using finite_space |
592 unfolding distribution_def prob_space[symmetric] using finite_space |
661 by (subst measure_finitely_additive'') |
593 by (subst finite_measure_finite_Union[symmetric]) |
662 (auto simp add: disjoint_family_on_def sets_eq_Pow intro!: arg_cong[where f=\<mu>]) |
594 (auto simp add: disjoint_family_on_def sets_eq_Pow |
|
595 intro!: arg_cong[where f=\<mu>']) |
663 |
596 |
664 lemma (in finite_prob_space) sum_over_space_real_distribution: |
597 lemma (in finite_prob_space) sum_over_space_real_distribution: |
665 "(\<Sum>x\<in>X`space M. real (distribution X {x})) = 1" |
598 "(\<Sum>x\<in>X`space M. distribution X {x}) = 1" |
666 unfolding distribution_def prob_space[symmetric] using finite_space |
599 unfolding distribution_def prob_space[symmetric] using finite_space |
667 by (subst real_finite_measure_finite_Union[symmetric]) |
600 by (subst finite_measure_finite_Union[symmetric]) |
668 (auto simp add: disjoint_family_on_def sets_eq_Pow intro!: arg_cong[where f=prob]) |
601 (auto simp add: disjoint_family_on_def sets_eq_Pow intro!: arg_cong[where f=prob]) |
669 |
602 |
670 lemma (in finite_prob_space) finite_sum_over_space_eq_1: |
603 lemma (in finite_prob_space) finite_sum_over_space_eq_1: |
671 "(\<Sum>x\<in>space M. real (\<mu> {x})) = 1" |
604 "(\<Sum>x\<in>space M. prob {x}) = 1" |
672 using sum_over_space_eq_1 finite_measure by (simp add: real_of_pextreal_setsum sets_eq_Pow) |
605 using prob_space finite_space |
673 |
606 by (subst (asm) finite_measure_finite_singleton) auto |
674 lemma (in finite_prob_space) distribution_finite: |
|
675 "distribution X A \<noteq> \<omega>" |
|
676 using finite_measure[of "X -` A \<inter> space M"] |
|
677 unfolding distribution_def sets_eq_Pow by auto |
|
678 |
|
679 lemma (in finite_prob_space) real_distribution_gt_0[simp]: |
|
680 "0 < real (distribution Y y) \<longleftrightarrow> 0 < distribution Y y" |
|
681 using assms by (auto intro!: real_pextreal_pos distribution_finite) |
|
682 |
|
683 lemma (in finite_prob_space) real_distribution_mult_pos_pos: |
|
684 assumes "0 < distribution Y y" |
|
685 and "0 < distribution X x" |
|
686 shows "0 < real (distribution Y y * distribution X x)" |
|
687 unfolding real_of_pextreal_mult[symmetric] |
|
688 using assms by (auto intro!: mult_pos_pos) |
|
689 |
|
690 lemma (in finite_prob_space) real_distribution_divide_pos_pos: |
|
691 assumes "0 < distribution Y y" |
|
692 and "0 < distribution X x" |
|
693 shows "0 < real (distribution Y y / distribution X x)" |
|
694 unfolding divide_pextreal_def real_of_pextreal_mult[symmetric] |
|
695 using assms distribution_finite[of X x] by (cases "distribution X x") (auto intro!: mult_pos_pos) |
|
696 |
|
697 lemma (in finite_prob_space) real_distribution_mult_inverse_pos_pos: |
|
698 assumes "0 < distribution Y y" |
|
699 and "0 < distribution X x" |
|
700 shows "0 < real (distribution Y y * inverse (distribution X x))" |
|
701 unfolding divide_pextreal_def real_of_pextreal_mult[symmetric] |
|
702 using assms distribution_finite[of X x] by (cases "distribution X x") (auto intro!: mult_pos_pos) |
|
703 |
607 |
704 lemma (in prob_space) distribution_remove_const: |
608 lemma (in prob_space) distribution_remove_const: |
705 shows "joint_distribution X (\<lambda>x. ()) {(x, ())} = distribution X {x}" |
609 shows "joint_distribution X (\<lambda>x. ()) {(x, ())} = distribution X {x}" |
706 and "joint_distribution (\<lambda>x. ()) X {((), x)} = distribution X {x}" |
610 and "joint_distribution (\<lambda>x. ()) X {((), x)} = distribution X {x}" |
707 and "joint_distribution X (\<lambda>x. (Y x, ())) {(x, y, ())} = joint_distribution X Y {(x, y)}" |
611 and "joint_distribution X (\<lambda>x. (Y x, ())) {(x, y, ())} = joint_distribution X Y {(x, y)}" |
708 and "joint_distribution X (\<lambda>x. ((), Y x)) {(x, (), y)} = joint_distribution X Y {(x, y)}" |
612 and "joint_distribution X (\<lambda>x. ((), Y x)) {(x, (), y)} = joint_distribution X Y {(x, y)}" |
709 and "distribution (\<lambda>x. ()) {()} = 1" |
613 and "distribution (\<lambda>x. ()) {()} = 1" |
710 unfolding measure_space_1[symmetric] |
614 by (auto intro!: arg_cong[where f=\<mu>'] simp: distribution_def prob_space[symmetric]) |
711 by (auto intro!: arg_cong[where f="\<mu>"] simp: distribution_def) |
|
712 |
615 |
713 lemma (in finite_prob_space) setsum_distribution_gen: |
616 lemma (in finite_prob_space) setsum_distribution_gen: |
714 assumes "Z -` {c} \<inter> space M = (\<Union>x \<in> X`space M. Y -` {f x}) \<inter> space M" |
617 assumes "Z -` {c} \<inter> space M = (\<Union>x \<in> X`space M. Y -` {f x}) \<inter> space M" |
715 and "inj_on f (X`space M)" |
618 and "inj_on f (X`space M)" |
716 shows "(\<Sum>x \<in> X`space M. distribution Y {f x}) = distribution Z {c}" |
619 shows "(\<Sum>x \<in> X`space M. distribution Y {f x}) = distribution Z {c}" |
717 unfolding distribution_def assms |
620 unfolding distribution_def assms |
718 using finite_space assms |
621 using finite_space assms |
719 by (subst measure_finitely_additive'') |
622 by (subst finite_measure_finite_Union[symmetric]) |
720 (auto simp add: disjoint_family_on_def sets_eq_Pow inj_on_def |
623 (auto simp add: disjoint_family_on_def sets_eq_Pow inj_on_def |
721 intro!: arg_cong[where f=prob]) |
624 intro!: arg_cong[where f=prob]) |
722 |
625 |
723 lemma (in finite_prob_space) setsum_distribution: |
626 lemma (in finite_prob_space) setsum_distribution: |
724 "(\<Sum>x \<in> X`space M. joint_distribution X Y {(x, y)}) = distribution Y {y}" |
627 "(\<Sum>x \<in> X`space M. joint_distribution X Y {(x, y)}) = distribution Y {y}" |
726 "(\<Sum>x \<in> X`space M. joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)}) = joint_distribution Y Z {(y, z)}" |
629 "(\<Sum>x \<in> X`space M. joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)}) = joint_distribution Y Z {(y, z)}" |
727 "(\<Sum>y \<in> Y`space M. joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)}) = joint_distribution X Z {(x, z)}" |
630 "(\<Sum>y \<in> Y`space M. joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)}) = joint_distribution X Z {(x, z)}" |
728 "(\<Sum>z \<in> Z`space M. joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)}) = joint_distribution X Y {(x, y)}" |
631 "(\<Sum>z \<in> Z`space M. joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)}) = joint_distribution X Y {(x, y)}" |
729 by (auto intro!: inj_onI setsum_distribution_gen) |
632 by (auto intro!: inj_onI setsum_distribution_gen) |
730 |
633 |
731 lemma (in finite_prob_space) setsum_real_distribution_gen: |
|
732 assumes "Z -` {c} \<inter> space M = (\<Union>x \<in> X`space M. Y -` {f x}) \<inter> space M" |
|
733 and "inj_on f (X`space M)" |
|
734 shows "(\<Sum>x \<in> X`space M. real (distribution Y {f x})) = real (distribution Z {c})" |
|
735 unfolding distribution_def assms |
|
736 using finite_space assms |
|
737 by (subst real_finite_measure_finite_Union[symmetric]) |
|
738 (auto simp add: disjoint_family_on_def sets_eq_Pow inj_on_def |
|
739 intro!: arg_cong[where f=prob]) |
|
740 |
|
741 lemma (in finite_prob_space) setsum_real_distribution: |
|
742 "(\<Sum>x \<in> X`space M. real (joint_distribution X Y {(x, y)})) = real (distribution Y {y})" |
|
743 "(\<Sum>y \<in> Y`space M. real (joint_distribution X Y {(x, y)})) = real (distribution X {x})" |
|
744 "(\<Sum>x \<in> X`space M. real (joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)})) = real (joint_distribution Y Z {(y, z)})" |
|
745 "(\<Sum>y \<in> Y`space M. real (joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)})) = real (joint_distribution X Z {(x, z)})" |
|
746 "(\<Sum>z \<in> Z`space M. real (joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)})) = real (joint_distribution X Y {(x, y)})" |
|
747 by (auto intro!: inj_onI setsum_real_distribution_gen) |
|
748 |
|
749 lemma (in finite_prob_space) real_distribution_order: |
|
750 shows "r \<le> real (joint_distribution X Y {(x, y)}) \<Longrightarrow> r \<le> real (distribution X {x})" |
|
751 and "r \<le> real (joint_distribution X Y {(x, y)}) \<Longrightarrow> r \<le> real (distribution Y {y})" |
|
752 and "r < real (joint_distribution X Y {(x, y)}) \<Longrightarrow> r < real (distribution X {x})" |
|
753 and "r < real (joint_distribution X Y {(x, y)}) \<Longrightarrow> r < real (distribution Y {y})" |
|
754 and "distribution X {x} = 0 \<Longrightarrow> real (joint_distribution X Y {(x, y)}) = 0" |
|
755 and "distribution Y {y} = 0 \<Longrightarrow> real (joint_distribution X Y {(x, y)}) = 0" |
|
756 using real_of_pextreal_mono[OF distribution_finite joint_distribution_restriction_fst, of X Y "{(x, y)}"] |
|
757 using real_of_pextreal_mono[OF distribution_finite joint_distribution_restriction_snd, of X Y "{(x, y)}"] |
|
758 using real_pextreal_nonneg[of "joint_distribution X Y {(x, y)}"] |
|
759 by auto |
|
760 |
|
761 lemma (in prob_space) joint_distribution_remove[simp]: |
|
762 "joint_distribution X X {(x, x)} = distribution X {x}" |
|
763 unfolding distribution_def by (auto intro!: arg_cong[where f="\<mu>"]) |
|
764 |
|
765 lemma (in finite_prob_space) distribution_1: |
|
766 "distribution X A \<le> 1" |
|
767 unfolding distribution_def measure_space_1[symmetric] |
|
768 by (auto intro!: measure_mono simp: sets_eq_Pow) |
|
769 |
|
770 lemma (in finite_prob_space) real_distribution_1: |
|
771 "real (distribution X A) \<le> 1" |
|
772 unfolding real_pextreal_1[symmetric] |
|
773 by (rule real_of_pextreal_mono[OF _ distribution_1]) simp |
|
774 |
|
775 lemma (in finite_prob_space) uniform_prob: |
634 lemma (in finite_prob_space) uniform_prob: |
776 assumes "x \<in> space M" |
635 assumes "x \<in> space M" |
777 assumes "\<And> x y. \<lbrakk>x \<in> space M ; y \<in> space M\<rbrakk> \<Longrightarrow> prob {x} = prob {y}" |
636 assumes "\<And> x y. \<lbrakk>x \<in> space M ; y \<in> space M\<rbrakk> \<Longrightarrow> prob {x} = prob {y}" |
778 shows "prob {x} = 1 / real (card (space M))" |
637 shows "prob {x} = 1 / card (space M)" |
779 proof - |
638 proof - |
780 have prob_x: "\<And> y. y \<in> space M \<Longrightarrow> prob {y} = prob {x}" |
639 have prob_x: "\<And> y. y \<in> space M \<Longrightarrow> prob {y} = prob {x}" |
781 using assms(2)[OF _ `x \<in> space M`] by blast |
640 using assms(2)[OF _ `x \<in> space M`] by blast |
782 have "1 = prob (space M)" |
641 have "1 = prob (space M)" |
783 using prob_space by auto |
642 using prob_space by auto |
784 also have "\<dots> = (\<Sum> x \<in> space M. prob {x})" |
643 also have "\<dots> = (\<Sum> x \<in> space M. prob {x})" |
785 using real_finite_measure_finite_Union[of "space M" "\<lambda> x. {x}", simplified] |
644 using finite_measure_finite_Union[of "space M" "\<lambda> x. {x}", simplified] |
786 sets_eq_Pow inj_singleton[unfolded inj_on_def, rule_format] |
645 sets_eq_Pow inj_singleton[unfolded inj_on_def, rule_format] |
787 finite_space unfolding disjoint_family_on_def prob_space[symmetric] |
646 finite_space unfolding disjoint_family_on_def prob_space[symmetric] |
788 by (auto simp add:setsum_restrict_set) |
647 by (auto simp add:setsum_restrict_set) |
789 also have "\<dots> = (\<Sum> y \<in> space M. prob {x})" |
648 also have "\<dots> = (\<Sum> y \<in> space M. prob {x})" |
790 using prob_x by auto |
649 using prob_x by auto |
807 show ?thesis |
666 show ?thesis |
808 proof qed (insert assms(4)[OF N.top], simp add: assms measure_space_1) |
667 proof qed (insert assms(4)[OF N.top], simp add: assms measure_space_1) |
809 qed |
668 qed |
810 |
669 |
811 lemma (in prob_space) prob_space_of_restricted_space: |
670 lemma (in prob_space) prob_space_of_restricted_space: |
812 assumes "\<mu> A \<noteq> 0" "\<mu> A \<noteq> \<omega>" "A \<in> sets M" |
671 assumes "\<mu> A \<noteq> 0" "A \<in> sets M" |
813 shows "prob_space (restricted_space A \<lparr>measure := \<lambda>S. \<mu> S / \<mu> A\<rparr>)" |
672 shows "prob_space (restricted_space A \<lparr>measure := \<lambda>S. \<mu> S / \<mu> A\<rparr>)" |
814 (is "prob_space ?P") |
673 (is "prob_space ?P") |
815 proof - |
674 proof - |
816 interpret A: measure_space "restricted_space A" |
675 interpret A: measure_space "restricted_space A" |
817 using `A \<in> sets M` by (rule restricted_measure_space) |
676 using `A \<in> sets M` by (rule restricted_measure_space) |
818 interpret A': sigma_algebra ?P |
677 interpret A': sigma_algebra ?P |
819 by (rule A.sigma_algebra_cong) auto |
678 by (rule A.sigma_algebra_cong) auto |
820 show "prob_space ?P" |
679 show "prob_space ?P" |
821 proof |
680 proof |
822 show "measure ?P (space ?P) = 1" |
681 show "measure ?P (space ?P) = 1" |
823 using `\<mu> A \<noteq> 0` `\<mu> A \<noteq> \<omega>` by (auto simp: pextreal_noteq_omega_Ex) |
682 using real_measure[OF `A \<in> events`] `\<mu> A \<noteq> 0` by auto |
824 show "measure ?P {} = 0" by auto |
683 show "positive ?P (measure ?P)" |
825 have "\<And>S. \<mu> S / \<mu> A = inverse (\<mu> A) * \<mu> S" by (simp add: mult_commute) |
684 proof (simp add: positive_def, safe) |
826 then show "countably_additive ?P (measure ?P)" |
685 show "0 / \<mu> A = 0" using `\<mu> A \<noteq> 0` by (cases "\<mu> A") (auto simp: zero_extreal_def) |
827 unfolding countably_additive_def psuminf_cmult_right |
686 fix B assume "B \<in> events" |
828 using A.measure_countably_additive by auto |
687 with real_measure[of "A \<inter> B"] real_measure[OF `A \<in> events`] `A \<in> sets M` |
|
688 show "0 \<le> \<mu> (A \<inter> B) / \<mu> A" by (auto simp: Int) |
|
689 qed |
|
690 show "countably_additive ?P (measure ?P)" |
|
691 proof (simp add: countably_additive_def, safe) |
|
692 fix B and F :: "nat \<Rightarrow> 'a set" |
|
693 assume F: "range F \<subseteq> op \<inter> A ` events" "disjoint_family F" |
|
694 { fix i |
|
695 from F have "F i \<in> op \<inter> A ` events" by auto |
|
696 with `A \<in> events` have "F i \<in> events" by auto } |
|
697 moreover then have "range F \<subseteq> events" by auto |
|
698 moreover have "\<And>S. \<mu> S / \<mu> A = inverse (\<mu> A) * \<mu> S" |
|
699 by (simp add: mult_commute divide_extreal_def) |
|
700 moreover have "0 \<le> inverse (\<mu> A)" |
|
701 using real_measure[OF `A \<in> events`] by auto |
|
702 ultimately show "(\<Sum>i. \<mu> (F i) / \<mu> A) = \<mu> (\<Union>i. F i) / \<mu> A" |
|
703 using measure_countably_additive[of F] F |
|
704 by (auto simp: suminf_cmult_extreal) |
|
705 qed |
829 qed |
706 qed |
830 qed |
707 qed |
831 |
708 |
832 lemma finite_prob_spaceI: |
709 lemma finite_prob_spaceI: |
833 assumes "finite (space M)" "sets M = Pow(space M)" "measure M (space M) = 1" "measure M {} = 0" |
710 assumes "finite (space M)" "sets M = Pow(space M)" |
|
711 and "measure M (space M) = 1" "measure M {} = 0" "\<And>A. A \<subseteq> space M \<Longrightarrow> 0 \<le> measure M A" |
834 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" |
712 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" |
835 shows "finite_prob_space M" |
713 shows "finite_prob_space M" |
836 unfolding finite_prob_space_eq |
714 unfolding finite_prob_space_eq |
837 proof |
715 proof |
838 show "finite_measure_space M" using assms |
716 show "finite_measure_space M" using assms |
839 by (auto intro!: finite_measure_spaceI) |
717 by (auto intro!: finite_measure_spaceI) |
840 show "measure M (space M) = 1" by fact |
718 show "measure M (space M) = 1" by fact |
841 qed |
719 qed |
842 |
720 |
843 lemma (in finite_prob_space) finite_measure_space: |
721 lemma (in finite_prob_space) finite_measure_space: |
844 fixes X :: "'a \<Rightarrow> 'x" |
722 fixes X :: "'a \<Rightarrow> 'x" |
845 shows "finite_measure_space \<lparr>space = X ` space M, sets = Pow (X ` space M), measure = distribution X\<rparr>" |
723 shows "finite_measure_space \<lparr>space = X ` space M, sets = Pow (X ` space M), measure = extreal \<circ> distribution X\<rparr>" |
846 (is "finite_measure_space ?S") |
724 (is "finite_measure_space ?S") |
847 proof (rule finite_measure_spaceI, simp_all) |
725 proof (rule finite_measure_spaceI, simp_all) |
848 show "finite (X ` space M)" using finite_space by simp |
726 show "finite (X ` space M)" using finite_space by simp |
849 next |
727 next |
850 fix A B :: "'x set" assume "A \<inter> B = {}" |
728 fix A B :: "'x set" assume "A \<inter> B = {}" |
851 then show "distribution X (A \<union> B) = distribution X A + distribution X B" |
729 then show "distribution X (A \<union> B) = distribution X A + distribution X B" |
852 unfolding distribution_def |
730 unfolding distribution_def |
853 by (subst measure_additive) |
731 by (subst finite_measure_Union[symmetric]) |
854 (auto intro!: arg_cong[where f=\<mu>] simp: sets_eq_Pow) |
732 (auto intro!: arg_cong[where f=\<mu>'] simp: sets_eq_Pow) |
855 qed |
733 qed |
856 |
734 |
857 lemma (in finite_prob_space) finite_prob_space_of_images: |
735 lemma (in finite_prob_space) finite_prob_space_of_images: |
858 "finite_prob_space \<lparr> space = X ` space M, sets = Pow (X ` space M), measure = distribution X \<rparr>" |
736 "finite_prob_space \<lparr> space = X ` space M, sets = Pow (X ` space M), measure = extreal \<circ> distribution X \<rparr>" |
859 by (simp add: finite_prob_space_eq finite_measure_space) |
737 by (simp add: finite_prob_space_eq finite_measure_space measure_space_1 one_extreal_def) |
860 |
|
861 lemma (in finite_prob_space) real_distribution_order': |
|
862 shows "real (distribution X {x}) = 0 \<Longrightarrow> real (joint_distribution X Y {(x, y)}) = 0" |
|
863 and "real (distribution Y {y}) = 0 \<Longrightarrow> real (joint_distribution X Y {(x, y)}) = 0" |
|
864 using real_of_pextreal_mono[OF distribution_finite joint_distribution_restriction_fst, of X Y "{(x, y)}"] |
|
865 using real_of_pextreal_mono[OF distribution_finite joint_distribution_restriction_snd, of X Y "{(x, y)}"] |
|
866 using real_pextreal_nonneg[of "joint_distribution X Y {(x, y)}"] |
|
867 by auto |
|
868 |
738 |
869 lemma (in finite_prob_space) finite_product_measure_space: |
739 lemma (in finite_prob_space) finite_product_measure_space: |
870 fixes X :: "'a \<Rightarrow> 'x" and Y :: "'a \<Rightarrow> 'y" |
740 fixes X :: "'a \<Rightarrow> 'x" and Y :: "'a \<Rightarrow> 'y" |
871 assumes "finite s1" "finite s2" |
741 assumes "finite s1" "finite s2" |
872 shows "finite_measure_space \<lparr> space = s1 \<times> s2, sets = Pow (s1 \<times> s2), measure = joint_distribution X Y\<rparr>" |
742 shows "finite_measure_space \<lparr> space = s1 \<times> s2, sets = Pow (s1 \<times> s2), measure = extreal \<circ> joint_distribution X Y\<rparr>" |
873 (is "finite_measure_space ?M") |
743 (is "finite_measure_space ?M") |
874 proof (rule finite_measure_spaceI, simp_all) |
744 proof (rule finite_measure_spaceI, simp_all) |
875 show "finite (s1 \<times> s2)" |
745 show "finite (s1 \<times> s2)" |
876 using assms by auto |
746 using assms by auto |
877 show "joint_distribution X Y (s1\<times>s2) \<noteq> \<omega>" |
|
878 using distribution_finite . |
|
879 next |
747 next |
880 fix A B :: "('x*'y) set" assume "A \<inter> B = {}" |
748 fix A B :: "('x*'y) set" assume "A \<inter> B = {}" |
881 then show "joint_distribution X Y (A \<union> B) = joint_distribution X Y A + joint_distribution X Y B" |
749 then show "joint_distribution X Y (A \<union> B) = joint_distribution X Y A + joint_distribution X Y B" |
882 unfolding distribution_def |
750 unfolding distribution_def |
883 by (subst measure_additive) |
751 by (subst finite_measure_Union[symmetric]) |
884 (auto intro!: arg_cong[where f=\<mu>] simp: sets_eq_Pow) |
752 (auto intro!: arg_cong[where f=\<mu>'] simp: sets_eq_Pow) |
885 qed |
753 qed |
886 |
754 |
887 lemma (in finite_prob_space) finite_product_measure_space_of_images: |
755 lemma (in finite_prob_space) finite_product_measure_space_of_images: |
888 shows "finite_measure_space \<lparr> space = X ` space M \<times> Y ` space M, |
756 shows "finite_measure_space \<lparr> space = X ` space M \<times> Y ` space M, |
889 sets = Pow (X ` space M \<times> Y ` space M), |
757 sets = Pow (X ` space M \<times> Y ` space M), |
890 measure = joint_distribution X Y \<rparr>" |
758 measure = extreal \<circ> joint_distribution X Y \<rparr>" |
891 using finite_space by (auto intro!: finite_product_measure_space) |
759 using finite_space by (auto intro!: finite_product_measure_space) |
892 |
760 |
893 lemma (in finite_prob_space) finite_product_prob_space_of_images: |
761 lemma (in finite_prob_space) finite_product_prob_space_of_images: |
894 "finite_prob_space \<lparr> space = X ` space M \<times> Y ` space M, sets = Pow (X ` space M \<times> Y ` space M), |
762 "finite_prob_space \<lparr> space = X ` space M \<times> Y ` space M, sets = Pow (X ` space M \<times> Y ` space M), |
895 measure = joint_distribution X Y \<rparr>" |
763 measure = extreal \<circ> joint_distribution X Y \<rparr>" |
896 (is "finite_prob_space ?S") |
764 (is "finite_prob_space ?S") |
897 proof (simp add: finite_prob_space_eq finite_product_measure_space_of_images) |
765 proof (simp add: finite_prob_space_eq finite_product_measure_space_of_images one_extreal_def) |
898 have "X -` X ` space M \<inter> Y -` Y ` space M \<inter> space M = space M" by auto |
766 have "X -` X ` space M \<inter> Y -` Y ` space M \<inter> space M = space M" by auto |
899 thus "joint_distribution X Y (X ` space M \<times> Y ` space M) = 1" |
767 thus "joint_distribution X Y (X ` space M \<times> Y ` space M) = 1" |
900 by (simp add: distribution_def prob_space vimage_Times comp_def measure_space_1) |
768 by (simp add: distribution_def prob_space vimage_Times comp_def measure_space_1) |
901 qed |
769 qed |
902 |
770 |
903 section "Conditional Expectation and Probability" |
771 section "Conditional Expectation and Probability" |
904 |
772 |
905 lemma (in prob_space) conditional_expectation_exists: |
773 lemma (in prob_space) conditional_expectation_exists: |
906 fixes X :: "'a \<Rightarrow> pextreal" and N :: "('a, 'b) measure_space_scheme" |
774 fixes X :: "'a \<Rightarrow> extreal" and N :: "('a, 'b) measure_space_scheme" |
907 assumes borel: "X \<in> borel_measurable M" |
775 assumes borel: "X \<in> borel_measurable M" "AE x. 0 \<le> X x" |
908 and N: "sigma_algebra N" "sets N \<subseteq> sets M" "space N = space M" "\<And>A. measure N A = \<mu> A" |
776 and N: "sigma_algebra N" "sets N \<subseteq> sets M" "space N = space M" "\<And>A. measure N A = \<mu> A" |
909 shows "\<exists>Y\<in>borel_measurable N. \<forall>C\<in>sets N. |
777 shows "\<exists>Y\<in>borel_measurable N. (\<forall>x. 0 \<le> Y x) \<and> (\<forall>C\<in>sets N. |
910 (\<integral>\<^isup>+x. Y x * indicator C x \<partial>M) = (\<integral>\<^isup>+x. X x * indicator C x \<partial>M)" |
778 (\<integral>\<^isup>+x. Y x * indicator C x \<partial>M) = (\<integral>\<^isup>+x. X x * indicator C x \<partial>M))" |
911 proof - |
779 proof - |
912 note N(4)[simp] |
780 note N(4)[simp] |
913 interpret P: prob_space N |
781 interpret P: prob_space N |
914 using prob_space_subalgebra[OF N] . |
782 using prob_space_subalgebra[OF N] . |
915 |
783 |
924 |
792 |
925 have "P.absolutely_continuous ?Q" |
793 have "P.absolutely_continuous ?Q" |
926 unfolding P.absolutely_continuous_def |
794 unfolding P.absolutely_continuous_def |
927 proof safe |
795 proof safe |
928 fix A assume "A \<in> sets N" "P.\<mu> A = 0" |
796 fix A assume "A \<in> sets N" "P.\<mu> A = 0" |
929 moreover then have f_borel: "?f A \<in> borel_measurable M" |
797 then have f_borel: "?f A \<in> borel_measurable M" "AE x. x \<notin> A" |
930 using borel N by (auto intro: borel_measurable_indicator) |
798 using borel N by (auto intro!: borel_measurable_indicator AE_not_in) |
931 moreover have "{x\<in>space M. ?f A x \<noteq> 0} = (?f A -` {0<..} \<inter> space M) \<inter> A" |
799 then show "?Q A = 0" |
932 by (auto simp: indicator_def) |
800 by (auto simp add: positive_integral_0_iff_AE) |
933 moreover have "\<mu> \<dots> \<le> \<mu> A" |
|
934 using `A \<in> sets N` N f_borel |
|
935 by (auto intro!: measure_mono Int[of _ A] measurable_sets) |
|
936 ultimately show "?Q A = 0" |
|
937 by (simp add: positive_integral_0_iff) |
|
938 qed |
801 qed |
939 from P.Radon_Nikodym[OF Q this] |
802 from P.Radon_Nikodym[OF Q this] |
940 obtain Y where Y: "Y \<in> borel_measurable N" |
803 obtain Y where Y: "Y \<in> borel_measurable N" "\<And>x. 0 \<le> Y x" |
941 "\<And>A. A \<in> sets N \<Longrightarrow> ?Q A =(\<integral>\<^isup>+x. Y x * indicator A x \<partial>N)" |
804 "\<And>A. A \<in> sets N \<Longrightarrow> ?Q A =(\<integral>\<^isup>+x. Y x * indicator A x \<partial>N)" |
942 by blast |
805 by blast |
943 with N(2) show ?thesis |
806 with N(2) show ?thesis |
944 by (auto intro!: bexI[OF _ Y(1)] simp: positive_integral_subalgebra[OF _ N(2,3,4,1)]) |
807 by (auto intro!: bexI[OF _ Y(1)] simp: positive_integral_subalgebra[OF _ _ N(2,3,4,1)]) |
945 qed |
808 qed |
946 |
809 |
947 definition (in prob_space) |
810 definition (in prob_space) |
948 "conditional_expectation N X = (SOME Y. Y\<in>borel_measurable N |
811 "conditional_expectation N X = (SOME Y. Y\<in>borel_measurable N \<and> (\<forall>x. 0 \<le> Y x) |
949 \<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)))" |
812 \<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)))" |
950 |
813 |
951 abbreviation (in prob_space) |
814 abbreviation (in prob_space) |
952 "conditional_prob N A \<equiv> conditional_expectation N (indicator A)" |
815 "conditional_prob N A \<equiv> conditional_expectation N (indicator A)" |
953 |
816 |
954 lemma (in prob_space) |
817 lemma (in prob_space) |
955 fixes X :: "'a \<Rightarrow> pextreal" and N :: "('a, 'b) measure_space_scheme" |
818 fixes X :: "'a \<Rightarrow> extreal" and N :: "('a, 'b) measure_space_scheme" |
956 assumes borel: "X \<in> borel_measurable M" |
819 assumes borel: "X \<in> borel_measurable M" "AE x. 0 \<le> X x" |
957 and N: "sigma_algebra N" "sets N \<subseteq> sets M" "space N = space M" "\<And>A. measure N A = \<mu> A" |
820 and N: "sigma_algebra N" "sets N \<subseteq> sets M" "space N = space M" "\<And>A. measure N A = \<mu> A" |
958 shows borel_measurable_conditional_expectation: |
821 shows borel_measurable_conditional_expectation: |
959 "conditional_expectation N X \<in> borel_measurable N" |
822 "conditional_expectation N X \<in> borel_measurable N" |
960 and conditional_expectation: "\<And>C. C \<in> sets N \<Longrightarrow> |
823 and conditional_expectation: "\<And>C. C \<in> sets N \<Longrightarrow> |
961 (\<integral>\<^isup>+x. conditional_expectation N X x * indicator C x \<partial>M) = |
824 (\<integral>\<^isup>+x. conditional_expectation N X x * indicator C x \<partial>M) = |
968 |
831 |
969 from CE show "\<And>C. C \<in> sets N \<Longrightarrow> ?eq C" |
832 from CE show "\<And>C. C \<in> sets N \<Longrightarrow> ?eq C" |
970 unfolding conditional_expectation_def by (rule someI2_ex) blast |
833 unfolding conditional_expectation_def by (rule someI2_ex) blast |
971 qed |
834 qed |
972 |
835 |
|
836 lemma (in sigma_algebra) factorize_measurable_function_pos: |
|
837 fixes Z :: "'a \<Rightarrow> extreal" and Y :: "'a \<Rightarrow> 'c" |
|
838 assumes "sigma_algebra M'" and "Y \<in> measurable M M'" "Z \<in> borel_measurable M" |
|
839 assumes Z: "Z \<in> borel_measurable (sigma_algebra.vimage_algebra M' (space M) Y)" |
|
840 shows "\<exists>g\<in>borel_measurable M'. \<forall>x\<in>space M. max 0 (Z x) = g (Y x)" |
|
841 proof - |
|
842 interpret M': sigma_algebra M' by fact |
|
843 have Y: "Y \<in> space M \<rightarrow> space M'" using assms unfolding measurable_def by auto |
|
844 from M'.sigma_algebra_vimage[OF this] |
|
845 interpret va: sigma_algebra "M'.vimage_algebra (space M) Y" . |
|
846 |
|
847 from va.borel_measurable_implies_simple_function_sequence'[OF Z] guess f . note f = this |
|
848 |
|
849 have "\<forall>i. \<exists>g. simple_function M' g \<and> (\<forall>x\<in>space M. f i x = g (Y x))" |
|
850 proof |
|
851 fix i |
|
852 from f(1)[of i] have "finite (f i`space M)" and B_ex: |
|
853 "\<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" |
|
854 unfolding simple_function_def by auto |
|
855 from B_ex[THEN bchoice] guess B .. note B = this |
|
856 |
|
857 let ?g = "\<lambda>x. \<Sum>z\<in>f i`space M. z * indicator (B z) x" |
|
858 |
|
859 show "\<exists>g. simple_function M' g \<and> (\<forall>x\<in>space M. f i x = g (Y x))" |
|
860 proof (intro exI[of _ ?g] conjI ballI) |
|
861 show "simple_function M' ?g" using B by auto |
|
862 |
|
863 fix x assume "x \<in> space M" |
|
864 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)" |
|
865 unfolding indicator_def using B by auto |
|
866 then show "f i x = ?g (Y x)" using `x \<in> space M` f(1)[of i] |
|
867 by (subst va.simple_function_indicator_representation) auto |
|
868 qed |
|
869 qed |
|
870 from choice[OF this] guess g .. note g = this |
|
871 |
|
872 show ?thesis |
|
873 proof (intro ballI bexI) |
|
874 show "(\<lambda>x. SUP i. g i x) \<in> borel_measurable M'" |
|
875 using g by (auto intro: M'.borel_measurable_simple_function) |
|
876 fix x assume "x \<in> space M" |
|
877 have "max 0 (Z x) = (SUP i. f i x)" using f by simp |
|
878 also have "\<dots> = (SUP i. g i (Y x))" |
|
879 using g `x \<in> space M` by simp |
|
880 finally show "max 0 (Z x) = (SUP i. g i (Y x))" . |
|
881 qed |
|
882 qed |
|
883 |
|
884 lemma extreal_0_le_iff_le_0[simp]: |
|
885 fixes a :: extreal shows "0 \<le> -a \<longleftrightarrow> a \<le> 0" |
|
886 by (cases rule: extreal2_cases[of a]) auto |
|
887 |
973 lemma (in sigma_algebra) factorize_measurable_function: |
888 lemma (in sigma_algebra) factorize_measurable_function: |
974 fixes Z :: "'a \<Rightarrow> pextreal" and Y :: "'a \<Rightarrow> 'c" |
889 fixes Z :: "'a \<Rightarrow> extreal" and Y :: "'a \<Rightarrow> 'c" |
975 assumes "sigma_algebra M'" and "Y \<in> measurable M M'" "Z \<in> borel_measurable M" |
890 assumes "sigma_algebra M'" and "Y \<in> measurable M M'" "Z \<in> borel_measurable M" |
976 shows "Z \<in> borel_measurable (sigma_algebra.vimage_algebra M' (space M) Y) |
891 shows "Z \<in> borel_measurable (sigma_algebra.vimage_algebra M' (space M) Y) |
977 \<longleftrightarrow> (\<exists>g\<in>borel_measurable M'. \<forall>x\<in>space M. Z x = g (Y x))" |
892 \<longleftrightarrow> (\<exists>g\<in>borel_measurable M'. \<forall>x\<in>space M. Z x = g (Y x))" |
978 proof safe |
893 proof safe |
979 interpret M': sigma_algebra M' by fact |
894 interpret M': sigma_algebra M' by fact |
980 have Y: "Y \<in> space M \<rightarrow> space M'" using assms unfolding measurable_def by auto |
895 have Y: "Y \<in> space M \<rightarrow> space M'" using assms unfolding measurable_def by auto |
981 from M'.sigma_algebra_vimage[OF this] |
896 from M'.sigma_algebra_vimage[OF this] |
982 interpret va: sigma_algebra "M'.vimage_algebra (space M) Y" . |
897 interpret va: sigma_algebra "M'.vimage_algebra (space M) Y" . |
983 |
898 |
984 { fix g :: "'c \<Rightarrow> pextreal" assume "g \<in> borel_measurable M'" |
899 { fix g :: "'c \<Rightarrow> extreal" assume "g \<in> borel_measurable M'" |
985 with M'.measurable_vimage_algebra[OF Y] |
900 with M'.measurable_vimage_algebra[OF Y] |
986 have "g \<circ> Y \<in> borel_measurable (M'.vimage_algebra (space M) Y)" |
901 have "g \<circ> Y \<in> borel_measurable (M'.vimage_algebra (space M) Y)" |
987 by (rule measurable_comp) |
902 by (rule measurable_comp) |
988 moreover assume "\<forall>x\<in>space M. Z x = g (Y x)" |
903 moreover assume "\<forall>x\<in>space M. Z x = g (Y x)" |
989 then have "Z \<in> borel_measurable (M'.vimage_algebra (space M) Y) \<longleftrightarrow> |
904 then have "Z \<in> borel_measurable (M'.vimage_algebra (space M) Y) \<longleftrightarrow> |
990 g \<circ> Y \<in> borel_measurable (M'.vimage_algebra (space M) Y)" |
905 g \<circ> Y \<in> borel_measurable (M'.vimage_algebra (space M) Y)" |
991 by (auto intro!: measurable_cong) |
906 by (auto intro!: measurable_cong) |
992 ultimately show "Z \<in> borel_measurable (M'.vimage_algebra (space M) Y)" |
907 ultimately show "Z \<in> borel_measurable (M'.vimage_algebra (space M) Y)" |
993 by simp } |
908 by simp } |
994 |
909 |
995 assume "Z \<in> borel_measurable (M'.vimage_algebra (space M) Y)" |
910 assume Z: "Z \<in> borel_measurable (M'.vimage_algebra (space M) Y)" |
996 from va.borel_measurable_implies_simple_function_sequence[OF this] |
911 with assms have "(\<lambda>x. - Z x) \<in> borel_measurable M" |
997 obtain f where f: "\<And>i. simple_function (M'.vimage_algebra (space M) Y) (f i)" and "f \<up> Z" by blast |
912 "(\<lambda>x. - Z x) \<in> borel_measurable (M'.vimage_algebra (space M) Y)" |
998 |
913 by auto |
999 have "\<forall>i. \<exists>g. simple_function M' g \<and> (\<forall>x\<in>space M. f i x = g (Y x))" |
914 from factorize_measurable_function_pos[OF assms(1,2) this] guess n .. note n = this |
1000 proof |
915 from factorize_measurable_function_pos[OF assms Z] guess p .. note p = this |
1001 fix i |
916 let "?g x" = "p x - n x" |
1002 from f[of i] have "finite (f i`space M)" and B_ex: |
917 show "\<exists>g\<in>borel_measurable M'. \<forall>x\<in>space M. Z x = g (Y x)" |
1003 "\<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" |
918 proof (intro bexI ballI) |
1004 unfolding simple_function_def by auto |
919 show "?g \<in> borel_measurable M'" using p n by auto |
1005 from B_ex[THEN bchoice] guess B .. note B = this |
920 fix x assume "x \<in> space M" |
1006 |
921 then have "p (Y x) = max 0 (Z x)" "n (Y x) = max 0 (- Z x)" |
1007 let ?g = "\<lambda>x. \<Sum>z\<in>f i`space M. z * indicator (B z) x" |
922 using p n by auto |
1008 |
923 then show "Z x = ?g (Y x)" |
1009 show "\<exists>g. simple_function M' g \<and> (\<forall>x\<in>space M. f i x = g (Y x))" |
924 by (auto split: split_max) |
1010 proof (intro exI[of _ ?g] conjI ballI) |
|
1011 show "simple_function M' ?g" using B by auto |
|
1012 |
|
1013 fix x assume "x \<in> space M" |
|
1014 then have "\<And>z. z \<in> f i`space M \<Longrightarrow> indicator (B z) (Y x) = (indicator (f i -` {z} \<inter> space M) x::pextreal)" |
|
1015 unfolding indicator_def using B by auto |
|
1016 then show "f i x = ?g (Y x)" using `x \<in> space M` f[of i] |
|
1017 by (subst va.simple_function_indicator_representation) auto |
|
1018 qed |
|
1019 qed |
925 qed |
1020 from choice[OF this] guess g .. note g = this |
|
1021 |
|
1022 show "\<exists>g\<in>borel_measurable M'. \<forall>x\<in>space M. Z x = g (Y x)" |
|
1023 proof (intro ballI bexI) |
|
1024 show "(\<lambda>x. SUP i. g i x) \<in> borel_measurable M'" |
|
1025 using g by (auto intro: M'.borel_measurable_simple_function) |
|
1026 fix x assume "x \<in> space M" |
|
1027 have "Z x = (SUP i. f i) x" using `f \<up> Z` unfolding isoton_def by simp |
|
1028 also have "\<dots> = (SUP i. g i (Y x))" unfolding SUPR_apply |
|
1029 using g `x \<in> space M` by simp |
|
1030 finally show "Z x = (SUP i. g i (Y x))" . |
|
1031 qed |
|
1032 qed |
926 qed |
1033 |
927 |
1034 end |
928 end |