author | blanchet |
Thu, 01 Apr 2010 10:27:06 +0200 | |
changeset 36066 | 1493b43204e9 |
parent 35977 | 30d42bfd0174 |
child 36624 | 25153c08655e |
permissions | -rw-r--r-- |
35582 | 1 |
theory Probability_Space |
2 |
imports Lebesgue |
|
3 |
begin |
|
4 |
||
5 |
locale prob_space = measure_space + |
|
6 |
assumes prob_space: "measure M (space M) = 1" |
|
7 |
begin |
|
8 |
||
9 |
abbreviation "events \<equiv> sets M" |
|
10 |
abbreviation "prob \<equiv> measure M" |
|
11 |
abbreviation "prob_preserving \<equiv> measure_preserving" |
|
12 |
abbreviation "random_variable \<equiv> \<lambda> s X. X \<in> measurable M s" |
|
13 |
abbreviation "expectation \<equiv> integral" |
|
14 |
||
15 |
definition |
|
16 |
"indep A B \<longleftrightarrow> A \<in> events \<and> B \<in> events \<and> prob (A \<inter> B) = prob A * prob B" |
|
17 |
||
18 |
definition |
|
19 |
"indep_families F G \<longleftrightarrow> (\<forall> A \<in> F. \<forall> B \<in> G. indep A B)" |
|
20 |
||
21 |
definition |
|
22 |
"distribution X = (\<lambda>s. prob ((X -` s) \<inter> (space M)))" |
|
23 |
||
24 |
definition |
|
25 |
"probably e \<longleftrightarrow> e \<in> events \<and> prob e = 1" |
|
26 |
||
27 |
definition |
|
28 |
"possibly e \<longleftrightarrow> e \<in> events \<and> prob e \<noteq> 0" |
|
29 |
||
30 |
definition |
|
31 |
"joint_distribution X Y \<equiv> (\<lambda>a. prob ((\<lambda>x. (X x, Y x)) -` a \<inter> space M))" |
|
32 |
||
33 |
definition |
|
34 |
"conditional_expectation X s \<equiv> THE f. random_variable borel_space f \<and> |
|
35 |
(\<forall> g \<in> s. integral (\<lambda>x. f x * indicator_fn g x) = |
|
36 |
integral (\<lambda>x. X x * indicator_fn g x))" |
|
37 |
||
38 |
definition |
|
39 |
"conditional_prob e1 e2 \<equiv> conditional_expectation (indicator_fn e1) e2" |
|
40 |
||
35929
90f38c8831e2
Unhide measure_space.positive defined in Caratheodory.
hoelzl
parents:
35582
diff
changeset
|
41 |
lemma positive': "positive M prob" |
35582 | 42 |
unfolding positive_def using positive empty_measure by blast |
43 |
||
44 |
lemma prob_compl: |
|
45 |
assumes "s \<in> events" |
|
46 |
shows "prob (space M - s) = 1 - prob s" |
|
47 |
using assms |
|
48 |
proof - |
|
49 |
have "prob ((space M - s) \<union> s) = prob (space M - s) + prob s" |
|
50 |
using assms additive[unfolded additive_def] by blast |
|
51 |
thus ?thesis by (simp add:Un_absorb2[OF sets_into_space[OF assms]] prob_space) |
|
52 |
qed |
|
53 |
||
54 |
lemma indep_space: |
|
55 |
assumes "s \<in> events" |
|
56 |
shows "indep (space M) s" |
|
57 |
using assms prob_space |
|
58 |
unfolding indep_def by auto |
|
59 |
||
60 |
||
61 |
lemma prob_space_increasing: |
|
62 |
"increasing M prob" |
|
35929
90f38c8831e2
Unhide measure_space.positive defined in Caratheodory.
hoelzl
parents:
35582
diff
changeset
|
63 |
by (rule additive_increasing[OF positive' additive]) |
35582 | 64 |
|
65 |
lemma prob_subadditive: |
|
66 |
assumes "s \<in> events" "t \<in> events" |
|
67 |
shows "prob (s \<union> t) \<le> prob s + prob t" |
|
68 |
using assms |
|
69 |
proof - |
|
70 |
have "prob (s \<union> t) = prob ((s - t) \<union> t)" by simp |
|
71 |
also have "\<dots> = prob (s - t) + prob t" |
|
72 |
using additive[unfolded additive_def, rule_format, of "s-t" "t"] |
|
73 |
assms by blast |
|
74 |
also have "\<dots> \<le> prob s + prob t" |
|
75 |
using prob_space_increasing[unfolded increasing_def, rule_format] assms |
|
76 |
by auto |
|
77 |
finally show ?thesis by simp |
|
78 |
qed |
|
79 |
||
80 |
lemma prob_zero_union: |
|
81 |
assumes "s \<in> events" "t \<in> events" "prob t = 0" |
|
82 |
shows "prob (s \<union> t) = prob s" |
|
83 |
using assms |
|
84 |
proof - |
|
85 |
have "prob (s \<union> t) \<le> prob s" |
|
86 |
using prob_subadditive[of s t] assms by auto |
|
87 |
moreover have "prob (s \<union> t) \<ge> prob s" |
|
88 |
using prob_space_increasing[unfolded increasing_def, rule_format] |
|
89 |
assms by auto |
|
90 |
ultimately show ?thesis by simp |
|
91 |
qed |
|
92 |
||
93 |
lemma prob_eq_compl: |
|
94 |
assumes "s \<in> events" "t \<in> events" |
|
95 |
assumes "prob (space M - s) = prob (space M - t)" |
|
96 |
shows "prob s = prob t" |
|
97 |
using assms prob_compl by auto |
|
98 |
||
99 |
lemma prob_one_inter: |
|
100 |
assumes events:"s \<in> events" "t \<in> events" |
|
101 |
assumes "prob t = 1" |
|
102 |
shows "prob (s \<inter> t) = prob s" |
|
103 |
using assms |
|
104 |
proof - |
|
105 |
have "prob ((space M - s) \<union> (space M - t)) = prob (space M - s)" |
|
106 |
using prob_compl[of "t"] prob_zero_union assms by auto |
|
107 |
then show "prob (s \<inter> t) = prob s" |
|
108 |
using prob_eq_compl[of "s \<inter> t"] events by (simp only: Diff_Int) auto |
|
109 |
qed |
|
110 |
||
111 |
lemma prob_eq_bigunion_image: |
|
112 |
assumes "range f \<subseteq> events" "range g \<subseteq> events" |
|
113 |
assumes "disjoint_family f" "disjoint_family g" |
|
114 |
assumes "\<And> n :: nat. prob (f n) = prob (g n)" |
|
115 |
shows "(prob (\<Union> i. f i) = prob (\<Union> i. g i))" |
|
116 |
using assms |
|
117 |
proof - |
|
118 |
have a: "(\<lambda> i. prob (f i)) sums (prob (\<Union> i. f i))" |
|
119 |
using ca[unfolded countably_additive_def] assms by blast |
|
120 |
have b: "(\<lambda> i. prob (g i)) sums (prob (\<Union> i. g i))" |
|
121 |
using ca[unfolded countably_additive_def] assms by blast |
|
122 |
show ?thesis using sums_unique[OF b] sums_unique[OF a] assms by simp |
|
123 |
qed |
|
124 |
||
125 |
lemma prob_countably_subadditive: |
|
126 |
assumes "range f \<subseteq> events" |
|
127 |
assumes "summable (prob \<circ> f)" |
|
128 |
shows "prob (\<Union>i. f i) \<le> (\<Sum> i. prob (f i))" |
|
129 |
using assms |
|
130 |
proof - |
|
131 |
def f' == "\<lambda> i. f i - (\<Union> j \<in> {0 ..< i}. f j)" |
|
132 |
have "(\<Union> i. f' i) \<subseteq> (\<Union> i. f i)" unfolding f'_def by auto |
|
133 |
moreover have "(\<Union> i. f' i) \<supseteq> (\<Union> i. f i)" |
|
134 |
proof (rule subsetI) |
|
135 |
fix x assume "x \<in> (\<Union> i. f i)" |
|
136 |
then obtain k where "x \<in> f k" by blast |
|
137 |
hence k: "k \<in> {m. x \<in> f m}" by simp |
|
138 |
have "\<exists> l. x \<in> f l \<and> (\<forall> l' < l. x \<notin> f l')" |
|
139 |
using wfE_min[of "{(x, y). x < y}" "k" "{m. x \<in> f m}", |
|
140 |
OF wf_less k] by auto |
|
141 |
thus "x \<in> (\<Union> i. f' i)" unfolding f'_def by auto |
|
142 |
qed |
|
143 |
ultimately have uf'f: "(\<Union> i. f' i) = (\<Union> i. f i)" by (rule equalityI) |
|
144 |
||
145 |
have df': "\<And> i j. i < j \<Longrightarrow> f' i \<inter> f' j = {}" |
|
146 |
unfolding f'_def by auto |
|
147 |
have "\<And> i j. i \<noteq> j \<Longrightarrow> f' i \<inter> f' j = {}" |
|
148 |
apply (drule iffD1[OF nat_neq_iff]) |
|
149 |
using df' by auto |
|
150 |
hence df: "disjoint_family f'" unfolding disjoint_family_on_def by simp |
|
151 |
||
152 |
have rf': "\<And> i. f' i \<in> events" |
|
153 |
proof - |
|
154 |
fix i :: nat |
|
155 |
have "(\<Union> {f j | j. j \<in> {0 ..< i}}) = (\<Union> j \<in> {0 ..< i}. f j)" by blast |
|
156 |
hence "(\<Union> {f j | j. j \<in> {0 ..< i}}) \<in> events |
|
157 |
\<Longrightarrow> (\<Union> j \<in> {0 ..< i}. f j) \<in> events" by auto |
|
158 |
thus "f' i \<in> events" |
|
159 |
unfolding f'_def |
|
160 |
using assms finite_union[of "{f j | j. j \<in> {0 ..< i}}"] |
|
161 |
Diff[of "f i" "\<Union> j \<in> {0 ..< i}. f j"] by auto |
|
162 |
qed |
|
163 |
hence uf': "(\<Union> range f') \<in> events" by auto |
|
164 |
||
165 |
have "\<And> i. prob (f' i) \<le> prob (f i)" |
|
166 |
using prob_space_increasing[unfolded increasing_def, rule_format, OF rf'] |
|
167 |
assms rf' unfolding f'_def by blast |
|
168 |
||
169 |
hence absinc: "\<And> i. \<bar> prob (f' i) \<bar> \<le> prob (f i)" |
|
35929
90f38c8831e2
Unhide measure_space.positive defined in Caratheodory.
hoelzl
parents:
35582
diff
changeset
|
170 |
using abs_of_nonneg positive'[unfolded positive_def] |
35582 | 171 |
assms rf' by auto |
172 |
||
173 |
have "prob (\<Union> i. f i) = prob (\<Union> i. f' i)" using uf'f by simp |
|
174 |
||
175 |
also have "\<dots> = (\<Sum> i. prob (f' i))" |
|
176 |
using ca[unfolded countably_additive_def, rule_format] |
|
177 |
sums_unique rf' uf' df |
|
178 |
by auto |
|
179 |
||
180 |
also have "\<dots> \<le> (\<Sum> i. prob (f i))" |
|
181 |
using summable_le2[of "\<lambda> i. prob (f' i)" "\<lambda> i. prob (f i)", |
|
182 |
rule_format, OF absinc] |
|
183 |
assms[unfolded o_def] by auto |
|
184 |
||
185 |
finally show ?thesis by auto |
|
186 |
qed |
|
187 |
||
188 |
lemma prob_countably_zero: |
|
189 |
assumes "range c \<subseteq> events" |
|
190 |
assumes "\<And> i. prob (c i) = 0" |
|
191 |
shows "(prob (\<Union> i :: nat. c i) = 0)" |
|
192 |
using assms |
|
193 |
proof - |
|
194 |
have leq0: "0 \<le> prob (\<Union> i. c i)" |
|
35929
90f38c8831e2
Unhide measure_space.positive defined in Caratheodory.
hoelzl
parents:
35582
diff
changeset
|
195 |
using assms positive'[unfolded positive_def, rule_format] |
35582 | 196 |
by auto |
197 |
||
198 |
have "prob (\<Union> i. c i) \<le> (\<Sum> i. prob (c i))" |
|
199 |
using prob_countably_subadditive[of c, unfolded o_def] |
|
200 |
assms sums_zero sums_summable by auto |
|
201 |
||
202 |
also have "\<dots> = 0" |
|
203 |
using assms sums_zero |
|
204 |
sums_unique[of "\<lambda> i. prob (c i)" "0"] by auto |
|
205 |
||
206 |
finally show "prob (\<Union> i. c i) = 0" |
|
207 |
using leq0 by auto |
|
208 |
qed |
|
209 |
||
210 |
lemma indep_sym: |
|
211 |
"indep a b \<Longrightarrow> indep b a" |
|
212 |
unfolding indep_def using Int_commute[of a b] by auto |
|
213 |
||
214 |
lemma indep_refl: |
|
215 |
assumes "a \<in> events" |
|
216 |
shows "indep a a = (prob a = 0) \<or> (prob a = 1)" |
|
217 |
using assms unfolding indep_def by auto |
|
218 |
||
219 |
lemma prob_equiprobable_finite_unions: |
|
220 |
assumes "s \<in> events" |
|
221 |
assumes "\<And>x. x \<in> s \<Longrightarrow> {x} \<in> events" |
|
222 |
assumes "finite s" |
|
223 |
assumes "\<And> x y. \<lbrakk>x \<in> s; y \<in> s\<rbrakk> \<Longrightarrow> (prob {x} = prob {y})" |
|
224 |
shows "prob s = of_nat (card s) * prob {SOME x. x \<in> s}" |
|
225 |
using assms |
|
226 |
proof (cases "s = {}") |
|
227 |
case True thus ?thesis by simp |
|
228 |
next |
|
229 |
case False hence " \<exists> x. x \<in> s" by blast |
|
230 |
from someI_ex[OF this] assms |
|
231 |
have prob_some: "\<And> x. x \<in> s \<Longrightarrow> prob {x} = prob {SOME y. y \<in> s}" by blast |
|
232 |
have "prob s = (\<Sum> x \<in> s. prob {x})" |
|
233 |
using assms measure_real_sum_image by blast |
|
234 |
also have "\<dots> = (\<Sum> x \<in> s. prob {SOME y. y \<in> s})" using prob_some by auto |
|
235 |
also have "\<dots> = of_nat (card s) * prob {(SOME x. x \<in> s)}" |
|
236 |
using setsum_constant assms by auto |
|
237 |
finally show ?thesis by simp |
|
238 |
qed |
|
239 |
||
240 |
lemma prob_real_sum_image_fn: |
|
241 |
assumes "e \<in> events" |
|
242 |
assumes "\<And> x. x \<in> s \<Longrightarrow> e \<inter> f x \<in> events" |
|
243 |
assumes "finite s" |
|
244 |
assumes "\<And> x y. \<lbrakk>x \<in> s ; y \<in> s ; x \<noteq> y\<rbrakk> \<Longrightarrow> f x \<inter> f y = {}" |
|
245 |
assumes "space M \<subseteq> (\<Union> i \<in> s. f i)" |
|
246 |
shows "prob e = (\<Sum> x \<in> s. prob (e \<inter> f x))" |
|
247 |
using assms |
|
248 |
proof - |
|
249 |
let ?S = "{0 ..< card s}" |
|
250 |
obtain g where "g ` ?S = s \<and> inj_on g ?S" |
|
251 |
using ex_bij_betw_nat_finite[unfolded bij_betw_def, of s] assms by auto |
|
252 |
moreover hence gs: "g ` ?S = s" by simp |
|
253 |
ultimately have ginj: "inj_on g ?S" by simp |
|
254 |
let ?f' = "\<lambda> i. e \<inter> f (g i)" |
|
255 |
have f': "?f' \<in> ?S \<rightarrow> events" |
|
256 |
using gs assms by blast |
|
257 |
hence "\<And> i j. \<lbrakk>i \<in> ?S ; j \<in> ?S ; i \<noteq> j\<rbrakk> |
|
258 |
\<Longrightarrow> ?f' i \<inter> ?f' j = {}" using assms ginj[unfolded inj_on_def] gs f' by blast |
|
259 |
hence df': "\<And> i j. \<lbrakk>i < card s ; j < card s ; i \<noteq> j\<rbrakk> |
|
260 |
\<Longrightarrow> ?f' i \<inter> ?f' j = {}" by simp |
|
261 |
||
262 |
have "e = e \<inter> space M" using assms sets_into_space by simp |
|
263 |
also hence "\<dots> = e \<inter> (\<Union> x \<in> s. f x)" using assms by blast |
|
264 |
also have "\<dots> = (\<Union> x \<in> g ` ?S. e \<inter> f x)" using gs by simp |
|
265 |
also have "\<dots> = (\<Union> i \<in> ?S. ?f' i)" by simp |
|
266 |
finally have "prob e = prob (\<Union> i \<in> ?S. ?f' i)" by simp |
|
267 |
also have "\<dots> = (\<Sum> i \<in> ?S. prob (?f' i))" |
|
268 |
apply (subst measure_finitely_additive'') |
|
269 |
using f' df' assms by (auto simp: disjoint_family_on_def) |
|
270 |
also have "\<dots> = (\<Sum> x \<in> g ` ?S. prob (e \<inter> f x))" |
|
271 |
using setsum_reindex[of g "?S" "\<lambda> x. prob (e \<inter> f x)"] |
|
272 |
ginj by simp |
|
273 |
also have "\<dots> = (\<Sum> x \<in> s. prob (e \<inter> f x))" using gs by simp |
|
274 |
finally show ?thesis by simp |
|
275 |
qed |
|
276 |
||
277 |
lemma distribution_prob_space: |
|
278 |
assumes "random_variable s X" |
|
279 |
shows "prob_space \<lparr>space = space s, sets = sets s, measure = distribution X\<rparr>" |
|
280 |
using assms |
|
281 |
proof - |
|
282 |
let ?N = "\<lparr>space = space s, sets = sets s, measure = distribution X\<rparr>" |
|
283 |
interpret s: sigma_algebra "s" using assms[unfolded measurable_def] by auto |
|
284 |
hence sigN: "sigma_algebra ?N" using s.sigma_algebra_extend by auto |
|
285 |
||
286 |
have pos: "\<And> e. e \<in> sets s \<Longrightarrow> distribution X e \<ge> 0" |
|
287 |
unfolding distribution_def |
|
35929
90f38c8831e2
Unhide measure_space.positive defined in Caratheodory.
hoelzl
parents:
35582
diff
changeset
|
288 |
using positive'[unfolded positive_def] |
35582 | 289 |
assms[unfolded measurable_def] by auto |
290 |
||
291 |
have cas: "countably_additive ?N (distribution X)" |
|
292 |
proof - |
|
293 |
{ |
|
294 |
fix f :: "nat \<Rightarrow> 'c \<Rightarrow> bool" |
|
295 |
let ?g = "\<lambda> n. X -` f n \<inter> space M" |
|
296 |
assume asm: "range f \<subseteq> sets s" "UNION UNIV f \<in> sets s" "disjoint_family f" |
|
297 |
hence "range ?g \<subseteq> events" |
|
298 |
using assms unfolding measurable_def by blast |
|
299 |
from ca[unfolded countably_additive_def, |
|
300 |
rule_format, of ?g, OF this] countable_UN[OF this] asm |
|
301 |
have "(\<lambda> n. prob (?g n)) sums prob (UNION UNIV ?g)" |
|
302 |
unfolding disjoint_family_on_def by blast |
|
303 |
moreover have "(X -` (\<Union> n. f n)) = (\<Union> n. X -` f n)" by blast |
|
304 |
ultimately have "(\<lambda> n. distribution X (f n)) sums distribution X (UNION UNIV f)" |
|
305 |
unfolding distribution_def by simp |
|
306 |
} thus ?thesis unfolding countably_additive_def by simp |
|
307 |
qed |
|
308 |
||
309 |
have ds0: "distribution X {} = 0" |
|
310 |
unfolding distribution_def by simp |
|
311 |
||
312 |
have "X -` space s \<inter> space M = space M" |
|
313 |
using assms[unfolded measurable_def] by auto |
|
314 |
hence ds1: "distribution X (space s) = 1" |
|
315 |
unfolding measurable_def distribution_def using prob_space by simp |
|
316 |
||
317 |
from ds0 ds1 cas pos sigN |
|
318 |
show "prob_space ?N" |
|
319 |
unfolding prob_space_def prob_space_axioms_def |
|
320 |
measure_space_def measure_space_axioms_def by simp |
|
321 |
qed |
|
322 |
||
323 |
lemma distribution_lebesgue_thm1: |
|
324 |
assumes "random_variable s X" |
|
325 |
assumes "A \<in> sets s" |
|
326 |
shows "distribution X A = expectation (indicator_fn (X -` A \<inter> space M))" |
|
327 |
unfolding distribution_def |
|
328 |
using assms unfolding measurable_def |
|
329 |
using integral_indicator_fn by auto |
|
330 |
||
331 |
lemma distribution_lebesgue_thm2: |
|
332 |
assumes "random_variable s X" "A \<in> sets s" |
|
333 |
shows "distribution X A = measure_space.integral \<lparr>space = space s, sets = sets s, measure = distribution X\<rparr> (indicator_fn A)" |
|
334 |
(is "_ = measure_space.integral ?M _") |
|
335 |
proof - |
|
336 |
interpret S: prob_space ?M using assms(1) by (rule distribution_prob_space) |
|
337 |
||
338 |
show ?thesis |
|
339 |
using S.integral_indicator_fn(1) |
|
340 |
using assms unfolding distribution_def by auto |
|
341 |
qed |
|
342 |
||
343 |
lemma finite_expectation1: |
|
344 |
assumes "finite (space M)" "random_variable borel_space X" |
|
345 |
shows "expectation X = (\<Sum> r \<in> X ` space M. r * prob (X -` {r} \<inter> space M))" |
|
346 |
using assms integral_finite measurable_def |
|
347 |
unfolding borel_measurable_def by auto |
|
348 |
||
349 |
lemma finite_expectation: |
|
350 |
assumes "finite (space M) \<and> random_variable borel_space X" |
|
351 |
shows "expectation X = (\<Sum> r \<in> X ` (space M). r * distribution X {r})" |
|
352 |
using assms unfolding distribution_def using finite_expectation1 by auto |
|
353 |
lemma prob_x_eq_1_imp_prob_y_eq_0: |
|
354 |
assumes "{x} \<in> events" |
|
355 |
assumes "(prob {x} = 1)" |
|
356 |
assumes "{y} \<in> events" |
|
357 |
assumes "y \<noteq> x" |
|
358 |
shows "prob {y} = 0" |
|
359 |
using prob_one_inter[of "{y}" "{x}"] assms by auto |
|
360 |
||
361 |
lemma distribution_x_eq_1_imp_distribution_y_eq_0: |
|
362 |
assumes X: "random_variable \<lparr>space = X ` (space M), sets = Pow (X ` (space M))\<rparr> X" |
|
363 |
assumes "(distribution X {x} = 1)" |
|
364 |
assumes "y \<noteq> x" |
|
365 |
shows "distribution X {y} = 0" |
|
366 |
proof - |
|
367 |
let ?S = "\<lparr>space = X ` (space M), sets = Pow (X ` (space M))\<rparr>" |
|
368 |
let ?M = "\<lparr>space = X ` (space M), sets = Pow (X ` (space M)), measure = distribution X\<rparr>" |
|
369 |
interpret S: prob_space ?M |
|
370 |
using distribution_prob_space[OF X] by auto |
|
371 |
{ assume "{x} \<notin> sets ?M" |
|
372 |
hence "x \<notin> X ` space M" by auto |
|
373 |
hence "X -` {x} \<inter> space M = {}" by auto |
|
374 |
hence "distribution X {x} = 0" unfolding distribution_def by auto |
|
375 |
hence "False" using assms by auto } |
|
376 |
hence x: "{x} \<in> sets ?M" by auto |
|
377 |
{ assume "{y} \<notin> sets ?M" |
|
378 |
hence "y \<notin> X ` space M" by auto |
|
379 |
hence "X -` {y} \<inter> space M = {}" by auto |
|
380 |
hence "distribution X {y} = 0" unfolding distribution_def by auto } |
|
381 |
moreover |
|
382 |
{ assume "{y} \<in> sets ?M" |
|
383 |
hence "distribution X {y} = 0" using assms S.prob_x_eq_1_imp_prob_y_eq_0[OF x] by auto } |
|
384 |
ultimately show ?thesis by auto |
|
385 |
qed |
|
386 |
||
35977 | 387 |
|
35582 | 388 |
end |
389 |
||
35977 | 390 |
locale finite_prob_space = prob_space + finite_measure_space |
391 |
||
392 |
lemma (in finite_prob_space) finite_marginal_product_space_POW2: |
|
393 |
assumes "finite s1" "finite s2" |
|
394 |
shows "finite_measure_space \<lparr> space = s1 \<times> s2, sets = Pow (s1 \<times> s2), measure = joint_distribution X Y\<rparr>" |
|
395 |
(is "finite_measure_space ?M") |
|
396 |
proof (rule finite_Pow_additivity_sufficient) |
|
397 |
show "positive ?M (measure ?M)" |
|
398 |
unfolding positive_def using positive'[unfolded positive_def] assms sets_eq_Pow |
|
399 |
by (simp add: joint_distribution_def) |
|
400 |
||
401 |
show "additive ?M (measure ?M)" unfolding additive_def |
|
402 |
proof safe |
|
403 |
fix x y |
|
404 |
have A: "((\<lambda>x. (X x, Y x)) -` x) \<inter> space M \<in> sets M" using assms sets_eq_Pow by auto |
|
405 |
have B: "((\<lambda>x. (X x, Y x)) -` y) \<inter> space M \<in> sets M" using assms sets_eq_Pow by auto |
|
406 |
assume "x \<inter> y = {}" |
|
407 |
from additive[unfolded additive_def, rule_format, OF A B] this |
|
408 |
show "measure ?M (x \<union> y) = measure ?M x + measure ?M y" |
|
409 |
apply (simp add: joint_distribution_def) |
|
410 |
apply (subst Int_Un_distrib2) |
|
411 |
by auto |
|
412 |
qed |
|
413 |
||
414 |
show "finite (space ?M)" |
|
415 |
using assms by auto |
|
416 |
||
417 |
show "sets ?M = Pow (space ?M)" |
|
418 |
by simp |
|
419 |
qed |
|
420 |
||
421 |
lemma (in finite_prob_space) finite_marginal_product_space_POW: |
|
422 |
shows "finite_measure_space \<lparr> space = X ` space M \<times> Y ` space M, |
|
423 |
sets = Pow (X ` space M \<times> Y ` space M), |
|
424 |
measure = joint_distribution X Y\<rparr>" |
|
425 |
(is "finite_measure_space ?M") |
|
426 |
using finite_space by (auto intro!: finite_marginal_product_space_POW2) |
|
427 |
||
35582 | 428 |
end |