author | haftmann |
Fri, 11 Jun 2010 17:14:02 +0200 | |
changeset 37407 | 61dd8c145da7 |
parent 36624 | 25153c08655e |
child 38656 | d5d342611edb |
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 |
||
36624 | 24 |
abbreviation |
25 |
"joint_distribution X Y \<equiv> distribution (\<lambda>x. (X x, Y x))" |
|
35582 | 26 |
|
36624 | 27 |
(* |
28 |
definition probably :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "\<forall>\<^sup>*" 10) where |
|
29 |
"probably P \<longleftrightarrow> { x. P x } \<in> events \<and> prob { x. P x } = 1" |
|
30 |
definition possibly :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "\<exists>\<^sup>*" 10) where |
|
31 |
"possibly P \<longleftrightarrow> { x. P x } \<in> events \<and> prob { x. P x } \<noteq> 0" |
|
32 |
*) |
|
35582 | 33 |
|
34 |
definition |
|
36624 | 35 |
"conditional_expectation X M' \<equiv> SOME f. f \<in> measurable M' borel_space \<and> |
36 |
(\<forall> g \<in> sets M'. measure_space.integral M' (\<lambda>x. f x * indicator_fn g x) = |
|
37 |
measure_space.integral M' (\<lambda>x. X x * indicator_fn g x))" |
|
35582 | 38 |
|
39 |
definition |
|
36624 | 40 |
"conditional_prob E M' \<equiv> conditional_expectation (indicator_fn E) M'" |
35582 | 41 |
|
35929
90f38c8831e2
Unhide measure_space.positive defined in Caratheodory.
hoelzl
parents:
35582
diff
changeset
|
42 |
lemma positive': "positive M prob" |
35582 | 43 |
unfolding positive_def using positive empty_measure by blast |
44 |
||
45 |
lemma prob_compl: |
|
46 |
assumes "s \<in> events" |
|
47 |
shows "prob (space M - s) = 1 - prob s" |
|
48 |
using assms |
|
49 |
proof - |
|
50 |
have "prob ((space M - s) \<union> s) = prob (space M - s) + prob s" |
|
51 |
using assms additive[unfolded additive_def] by blast |
|
52 |
thus ?thesis by (simp add:Un_absorb2[OF sets_into_space[OF assms]] prob_space) |
|
53 |
qed |
|
54 |
||
55 |
lemma indep_space: |
|
56 |
assumes "s \<in> events" |
|
57 |
shows "indep (space M) s" |
|
58 |
using assms prob_space |
|
59 |
unfolding indep_def by auto |
|
60 |
||
61 |
||
62 |
lemma prob_space_increasing: |
|
63 |
"increasing M prob" |
|
35929
90f38c8831e2
Unhide measure_space.positive defined in Caratheodory.
hoelzl
parents:
35582
diff
changeset
|
64 |
by (rule additive_increasing[OF positive' additive]) |
35582 | 65 |
|
66 |
lemma prob_subadditive: |
|
67 |
assumes "s \<in> events" "t \<in> events" |
|
68 |
shows "prob (s \<union> t) \<le> prob s + prob t" |
|
69 |
using assms |
|
70 |
proof - |
|
71 |
have "prob (s \<union> t) = prob ((s - t) \<union> t)" by simp |
|
72 |
also have "\<dots> = prob (s - t) + prob t" |
|
73 |
using additive[unfolded additive_def, rule_format, of "s-t" "t"] |
|
74 |
assms by blast |
|
75 |
also have "\<dots> \<le> prob s + prob t" |
|
76 |
using prob_space_increasing[unfolded increasing_def, rule_format] assms |
|
77 |
by auto |
|
78 |
finally show ?thesis by simp |
|
79 |
qed |
|
80 |
||
81 |
lemma prob_zero_union: |
|
82 |
assumes "s \<in> events" "t \<in> events" "prob t = 0" |
|
83 |
shows "prob (s \<union> t) = prob s" |
|
84 |
using assms |
|
85 |
proof - |
|
86 |
have "prob (s \<union> t) \<le> prob s" |
|
87 |
using prob_subadditive[of s t] assms by auto |
|
88 |
moreover have "prob (s \<union> t) \<ge> prob s" |
|
89 |
using prob_space_increasing[unfolded increasing_def, rule_format] |
|
90 |
assms by auto |
|
91 |
ultimately show ?thesis by simp |
|
92 |
qed |
|
93 |
||
94 |
lemma prob_eq_compl: |
|
95 |
assumes "s \<in> events" "t \<in> events" |
|
96 |
assumes "prob (space M - s) = prob (space M - t)" |
|
97 |
shows "prob s = prob t" |
|
98 |
using assms prob_compl by auto |
|
99 |
||
100 |
lemma prob_one_inter: |
|
101 |
assumes events:"s \<in> events" "t \<in> events" |
|
102 |
assumes "prob t = 1" |
|
103 |
shows "prob (s \<inter> t) = prob s" |
|
104 |
using assms |
|
105 |
proof - |
|
106 |
have "prob ((space M - s) \<union> (space M - t)) = prob (space M - s)" |
|
107 |
using prob_compl[of "t"] prob_zero_union assms by auto |
|
108 |
then show "prob (s \<inter> t) = prob s" |
|
109 |
using prob_eq_compl[of "s \<inter> t"] events by (simp only: Diff_Int) auto |
|
110 |
qed |
|
111 |
||
112 |
lemma prob_eq_bigunion_image: |
|
113 |
assumes "range f \<subseteq> events" "range g \<subseteq> events" |
|
114 |
assumes "disjoint_family f" "disjoint_family g" |
|
115 |
assumes "\<And> n :: nat. prob (f n) = prob (g n)" |
|
116 |
shows "(prob (\<Union> i. f i) = prob (\<Union> i. g i))" |
|
117 |
using assms |
|
118 |
proof - |
|
119 |
have a: "(\<lambda> i. prob (f i)) sums (prob (\<Union> i. f i))" |
|
120 |
using ca[unfolded countably_additive_def] assms by blast |
|
121 |
have b: "(\<lambda> i. prob (g i)) sums (prob (\<Union> i. g i))" |
|
122 |
using ca[unfolded countably_additive_def] assms by blast |
|
123 |
show ?thesis using sums_unique[OF b] sums_unique[OF a] assms by simp |
|
124 |
qed |
|
125 |
||
126 |
lemma prob_countably_subadditive: |
|
127 |
assumes "range f \<subseteq> events" |
|
128 |
assumes "summable (prob \<circ> f)" |
|
129 |
shows "prob (\<Union>i. f i) \<le> (\<Sum> i. prob (f i))" |
|
130 |
using assms |
|
131 |
proof - |
|
132 |
def f' == "\<lambda> i. f i - (\<Union> j \<in> {0 ..< i}. f j)" |
|
133 |
have "(\<Union> i. f' i) \<subseteq> (\<Union> i. f i)" unfolding f'_def by auto |
|
134 |
moreover have "(\<Union> i. f' i) \<supseteq> (\<Union> i. f i)" |
|
135 |
proof (rule subsetI) |
|
136 |
fix x assume "x \<in> (\<Union> i. f i)" |
|
137 |
then obtain k where "x \<in> f k" by blast |
|
138 |
hence k: "k \<in> {m. x \<in> f m}" by simp |
|
139 |
have "\<exists> l. x \<in> f l \<and> (\<forall> l' < l. x \<notin> f l')" |
|
140 |
using wfE_min[of "{(x, y). x < y}" "k" "{m. x \<in> f m}", |
|
141 |
OF wf_less k] by auto |
|
142 |
thus "x \<in> (\<Union> i. f' i)" unfolding f'_def by auto |
|
143 |
qed |
|
144 |
ultimately have uf'f: "(\<Union> i. f' i) = (\<Union> i. f i)" by (rule equalityI) |
|
145 |
||
146 |
have df': "\<And> i j. i < j \<Longrightarrow> f' i \<inter> f' j = {}" |
|
147 |
unfolding f'_def by auto |
|
148 |
have "\<And> i j. i \<noteq> j \<Longrightarrow> f' i \<inter> f' j = {}" |
|
149 |
apply (drule iffD1[OF nat_neq_iff]) |
|
150 |
using df' by auto |
|
151 |
hence df: "disjoint_family f'" unfolding disjoint_family_on_def by simp |
|
152 |
||
153 |
have rf': "\<And> i. f' i \<in> events" |
|
154 |
proof - |
|
155 |
fix i :: nat |
|
156 |
have "(\<Union> {f j | j. j \<in> {0 ..< i}}) = (\<Union> j \<in> {0 ..< i}. f j)" by blast |
|
157 |
hence "(\<Union> {f j | j. j \<in> {0 ..< i}}) \<in> events |
|
158 |
\<Longrightarrow> (\<Union> j \<in> {0 ..< i}. f j) \<in> events" by auto |
|
159 |
thus "f' i \<in> events" |
|
160 |
unfolding f'_def |
|
161 |
using assms finite_union[of "{f j | j. j \<in> {0 ..< i}}"] |
|
162 |
Diff[of "f i" "\<Union> j \<in> {0 ..< i}. f j"] by auto |
|
163 |
qed |
|
164 |
hence uf': "(\<Union> range f') \<in> events" by auto |
|
165 |
||
166 |
have "\<And> i. prob (f' i) \<le> prob (f i)" |
|
167 |
using prob_space_increasing[unfolded increasing_def, rule_format, OF rf'] |
|
168 |
assms rf' unfolding f'_def by blast |
|
169 |
||
170 |
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
|
171 |
using abs_of_nonneg positive'[unfolded positive_def] |
35582 | 172 |
assms rf' by auto |
173 |
||
174 |
have "prob (\<Union> i. f i) = prob (\<Union> i. f' i)" using uf'f by simp |
|
175 |
||
176 |
also have "\<dots> = (\<Sum> i. prob (f' i))" |
|
177 |
using ca[unfolded countably_additive_def, rule_format] |
|
178 |
sums_unique rf' uf' df |
|
179 |
by auto |
|
180 |
||
181 |
also have "\<dots> \<le> (\<Sum> i. prob (f i))" |
|
182 |
using summable_le2[of "\<lambda> i. prob (f' i)" "\<lambda> i. prob (f i)", |
|
183 |
rule_format, OF absinc] |
|
184 |
assms[unfolded o_def] by auto |
|
185 |
||
186 |
finally show ?thesis by auto |
|
187 |
qed |
|
188 |
||
189 |
lemma prob_countably_zero: |
|
190 |
assumes "range c \<subseteq> events" |
|
191 |
assumes "\<And> i. prob (c i) = 0" |
|
192 |
shows "(prob (\<Union> i :: nat. c i) = 0)" |
|
193 |
using assms |
|
194 |
proof - |
|
195 |
have leq0: "0 \<le> prob (\<Union> i. c i)" |
|
35929
90f38c8831e2
Unhide measure_space.positive defined in Caratheodory.
hoelzl
parents:
35582
diff
changeset
|
196 |
using assms positive'[unfolded positive_def, rule_format] |
35582 | 197 |
by auto |
198 |
||
199 |
have "prob (\<Union> i. c i) \<le> (\<Sum> i. prob (c i))" |
|
200 |
using prob_countably_subadditive[of c, unfolded o_def] |
|
201 |
assms sums_zero sums_summable by auto |
|
202 |
||
203 |
also have "\<dots> = 0" |
|
204 |
using assms sums_zero |
|
205 |
sums_unique[of "\<lambda> i. prob (c i)" "0"] by auto |
|
206 |
||
207 |
finally show "prob (\<Union> i. c i) = 0" |
|
208 |
using leq0 by auto |
|
209 |
qed |
|
210 |
||
211 |
lemma indep_sym: |
|
212 |
"indep a b \<Longrightarrow> indep b a" |
|
213 |
unfolding indep_def using Int_commute[of a b] by auto |
|
214 |
||
215 |
lemma indep_refl: |
|
216 |
assumes "a \<in> events" |
|
217 |
shows "indep a a = (prob a = 0) \<or> (prob a = 1)" |
|
218 |
using assms unfolding indep_def by auto |
|
219 |
||
220 |
lemma prob_equiprobable_finite_unions: |
|
221 |
assumes "s \<in> events" |
|
222 |
assumes "\<And>x. x \<in> s \<Longrightarrow> {x} \<in> events" |
|
223 |
assumes "finite s" |
|
224 |
assumes "\<And> x y. \<lbrakk>x \<in> s; y \<in> s\<rbrakk> \<Longrightarrow> (prob {x} = prob {y})" |
|
225 |
shows "prob s = of_nat (card s) * prob {SOME x. x \<in> s}" |
|
226 |
using assms |
|
227 |
proof (cases "s = {}") |
|
228 |
case True thus ?thesis by simp |
|
229 |
next |
|
230 |
case False hence " \<exists> x. x \<in> s" by blast |
|
231 |
from someI_ex[OF this] assms |
|
232 |
have prob_some: "\<And> x. x \<in> s \<Longrightarrow> prob {x} = prob {SOME y. y \<in> s}" by blast |
|
233 |
have "prob s = (\<Sum> x \<in> s. prob {x})" |
|
234 |
using assms measure_real_sum_image by blast |
|
235 |
also have "\<dots> = (\<Sum> x \<in> s. prob {SOME y. y \<in> s})" using prob_some by auto |
|
236 |
also have "\<dots> = of_nat (card s) * prob {(SOME x. x \<in> s)}" |
|
237 |
using setsum_constant assms by auto |
|
238 |
finally show ?thesis by simp |
|
239 |
qed |
|
240 |
||
241 |
lemma prob_real_sum_image_fn: |
|
242 |
assumes "e \<in> events" |
|
243 |
assumes "\<And> x. x \<in> s \<Longrightarrow> e \<inter> f x \<in> events" |
|
244 |
assumes "finite s" |
|
245 |
assumes "\<And> x y. \<lbrakk>x \<in> s ; y \<in> s ; x \<noteq> y\<rbrakk> \<Longrightarrow> f x \<inter> f y = {}" |
|
246 |
assumes "space M \<subseteq> (\<Union> i \<in> s. f i)" |
|
247 |
shows "prob e = (\<Sum> x \<in> s. prob (e \<inter> f x))" |
|
248 |
using assms |
|
249 |
proof - |
|
250 |
let ?S = "{0 ..< card s}" |
|
251 |
obtain g where "g ` ?S = s \<and> inj_on g ?S" |
|
252 |
using ex_bij_betw_nat_finite[unfolded bij_betw_def, of s] assms by auto |
|
253 |
moreover hence gs: "g ` ?S = s" by simp |
|
254 |
ultimately have ginj: "inj_on g ?S" by simp |
|
255 |
let ?f' = "\<lambda> i. e \<inter> f (g i)" |
|
256 |
have f': "?f' \<in> ?S \<rightarrow> events" |
|
257 |
using gs assms by blast |
|
258 |
hence "\<And> i j. \<lbrakk>i \<in> ?S ; j \<in> ?S ; i \<noteq> j\<rbrakk> |
|
259 |
\<Longrightarrow> ?f' i \<inter> ?f' j = {}" using assms ginj[unfolded inj_on_def] gs f' by blast |
|
260 |
hence df': "\<And> i j. \<lbrakk>i < card s ; j < card s ; i \<noteq> j\<rbrakk> |
|
261 |
\<Longrightarrow> ?f' i \<inter> ?f' j = {}" by simp |
|
262 |
||
263 |
have "e = e \<inter> space M" using assms sets_into_space by simp |
|
264 |
also hence "\<dots> = e \<inter> (\<Union> x \<in> s. f x)" using assms by blast |
|
265 |
also have "\<dots> = (\<Union> x \<in> g ` ?S. e \<inter> f x)" using gs by simp |
|
266 |
also have "\<dots> = (\<Union> i \<in> ?S. ?f' i)" by simp |
|
267 |
finally have "prob e = prob (\<Union> i \<in> ?S. ?f' i)" by simp |
|
268 |
also have "\<dots> = (\<Sum> i \<in> ?S. prob (?f' i))" |
|
269 |
apply (subst measure_finitely_additive'') |
|
270 |
using f' df' assms by (auto simp: disjoint_family_on_def) |
|
271 |
also have "\<dots> = (\<Sum> x \<in> g ` ?S. prob (e \<inter> f x))" |
|
272 |
using setsum_reindex[of g "?S" "\<lambda> x. prob (e \<inter> f x)"] |
|
273 |
ginj by simp |
|
274 |
also have "\<dots> = (\<Sum> x \<in> s. prob (e \<inter> f x))" using gs by simp |
|
275 |
finally show ?thesis by simp |
|
276 |
qed |
|
277 |
||
278 |
lemma distribution_prob_space: |
|
279 |
assumes "random_variable s X" |
|
280 |
shows "prob_space \<lparr>space = space s, sets = sets s, measure = distribution X\<rparr>" |
|
281 |
using assms |
|
282 |
proof - |
|
283 |
let ?N = "\<lparr>space = space s, sets = sets s, measure = distribution X\<rparr>" |
|
284 |
interpret s: sigma_algebra "s" using assms[unfolded measurable_def] by auto |
|
285 |
hence sigN: "sigma_algebra ?N" using s.sigma_algebra_extend by auto |
|
286 |
||
287 |
have pos: "\<And> e. e \<in> sets s \<Longrightarrow> distribution X e \<ge> 0" |
|
288 |
unfolding distribution_def |
|
35929
90f38c8831e2
Unhide measure_space.positive defined in Caratheodory.
hoelzl
parents:
35582
diff
changeset
|
289 |
using positive'[unfolded positive_def] |
35582 | 290 |
assms[unfolded measurable_def] by auto |
291 |
||
292 |
have cas: "countably_additive ?N (distribution X)" |
|
293 |
proof - |
|
294 |
{ |
|
295 |
fix f :: "nat \<Rightarrow> 'c \<Rightarrow> bool" |
|
296 |
let ?g = "\<lambda> n. X -` f n \<inter> space M" |
|
297 |
assume asm: "range f \<subseteq> sets s" "UNION UNIV f \<in> sets s" "disjoint_family f" |
|
298 |
hence "range ?g \<subseteq> events" |
|
299 |
using assms unfolding measurable_def by blast |
|
300 |
from ca[unfolded countably_additive_def, |
|
301 |
rule_format, of ?g, OF this] countable_UN[OF this] asm |
|
302 |
have "(\<lambda> n. prob (?g n)) sums prob (UNION UNIV ?g)" |
|
303 |
unfolding disjoint_family_on_def by blast |
|
304 |
moreover have "(X -` (\<Union> n. f n)) = (\<Union> n. X -` f n)" by blast |
|
305 |
ultimately have "(\<lambda> n. distribution X (f n)) sums distribution X (UNION UNIV f)" |
|
306 |
unfolding distribution_def by simp |
|
307 |
} thus ?thesis unfolding countably_additive_def by simp |
|
308 |
qed |
|
309 |
||
310 |
have ds0: "distribution X {} = 0" |
|
311 |
unfolding distribution_def by simp |
|
312 |
||
313 |
have "X -` space s \<inter> space M = space M" |
|
314 |
using assms[unfolded measurable_def] by auto |
|
315 |
hence ds1: "distribution X (space s) = 1" |
|
316 |
unfolding measurable_def distribution_def using prob_space by simp |
|
317 |
||
318 |
from ds0 ds1 cas pos sigN |
|
319 |
show "prob_space ?N" |
|
320 |
unfolding prob_space_def prob_space_axioms_def |
|
321 |
measure_space_def measure_space_axioms_def by simp |
|
322 |
qed |
|
323 |
||
324 |
lemma distribution_lebesgue_thm1: |
|
325 |
assumes "random_variable s X" |
|
326 |
assumes "A \<in> sets s" |
|
327 |
shows "distribution X A = expectation (indicator_fn (X -` A \<inter> space M))" |
|
328 |
unfolding distribution_def |
|
329 |
using assms unfolding measurable_def |
|
330 |
using integral_indicator_fn by auto |
|
331 |
||
332 |
lemma distribution_lebesgue_thm2: |
|
333 |
assumes "random_variable s X" "A \<in> sets s" |
|
334 |
shows "distribution X A = measure_space.integral \<lparr>space = space s, sets = sets s, measure = distribution X\<rparr> (indicator_fn A)" |
|
335 |
(is "_ = measure_space.integral ?M _") |
|
336 |
proof - |
|
337 |
interpret S: prob_space ?M using assms(1) by (rule distribution_prob_space) |
|
338 |
||
339 |
show ?thesis |
|
340 |
using S.integral_indicator_fn(1) |
|
341 |
using assms unfolding distribution_def by auto |
|
342 |
qed |
|
343 |
||
344 |
lemma finite_expectation1: |
|
345 |
assumes "finite (space M)" "random_variable borel_space X" |
|
346 |
shows "expectation X = (\<Sum> r \<in> X ` space M. r * prob (X -` {r} \<inter> space M))" |
|
347 |
using assms integral_finite measurable_def |
|
348 |
unfolding borel_measurable_def by auto |
|
349 |
||
350 |
lemma finite_expectation: |
|
351 |
assumes "finite (space M) \<and> random_variable borel_space X" |
|
352 |
shows "expectation X = (\<Sum> r \<in> X ` (space M). r * distribution X {r})" |
|
353 |
using assms unfolding distribution_def using finite_expectation1 by auto |
|
354 |
lemma prob_x_eq_1_imp_prob_y_eq_0: |
|
355 |
assumes "{x} \<in> events" |
|
356 |
assumes "(prob {x} = 1)" |
|
357 |
assumes "{y} \<in> events" |
|
358 |
assumes "y \<noteq> x" |
|
359 |
shows "prob {y} = 0" |
|
360 |
using prob_one_inter[of "{y}" "{x}"] assms by auto |
|
361 |
||
362 |
lemma distribution_x_eq_1_imp_distribution_y_eq_0: |
|
363 |
assumes X: "random_variable \<lparr>space = X ` (space M), sets = Pow (X ` (space M))\<rparr> X" |
|
364 |
assumes "(distribution X {x} = 1)" |
|
365 |
assumes "y \<noteq> x" |
|
366 |
shows "distribution X {y} = 0" |
|
367 |
proof - |
|
368 |
let ?S = "\<lparr>space = X ` (space M), sets = Pow (X ` (space M))\<rparr>" |
|
369 |
let ?M = "\<lparr>space = X ` (space M), sets = Pow (X ` (space M)), measure = distribution X\<rparr>" |
|
370 |
interpret S: prob_space ?M |
|
371 |
using distribution_prob_space[OF X] by auto |
|
372 |
{ assume "{x} \<notin> sets ?M" |
|
373 |
hence "x \<notin> X ` space M" by auto |
|
374 |
hence "X -` {x} \<inter> space M = {}" by auto |
|
375 |
hence "distribution X {x} = 0" unfolding distribution_def by auto |
|
376 |
hence "False" using assms by auto } |
|
377 |
hence x: "{x} \<in> sets ?M" by auto |
|
378 |
{ assume "{y} \<notin> sets ?M" |
|
379 |
hence "y \<notin> X ` space M" by auto |
|
380 |
hence "X -` {y} \<inter> space M = {}" by auto |
|
381 |
hence "distribution X {y} = 0" unfolding distribution_def by auto } |
|
382 |
moreover |
|
383 |
{ assume "{y} \<in> sets ?M" |
|
384 |
hence "distribution X {y} = 0" using assms S.prob_x_eq_1_imp_prob_y_eq_0[OF x] by auto } |
|
385 |
ultimately show ?thesis by auto |
|
386 |
qed |
|
387 |
||
35977 | 388 |
|
35582 | 389 |
end |
390 |
||
35977 | 391 |
locale finite_prob_space = prob_space + finite_measure_space |
392 |
||
36624 | 393 |
lemma finite_prob_space_eq: |
394 |
"finite_prob_space M \<longleftrightarrow> finite_measure_space M \<and> measure M (space M) = 1" |
|
395 |
unfolding finite_prob_space_def finite_measure_space_def prob_space_def prob_space_axioms_def |
|
396 |
by auto |
|
397 |
||
398 |
lemma (in prob_space) not_empty: "space M \<noteq> {}" |
|
399 |
using prob_space empty_measure by auto |
|
400 |
||
401 |
lemma (in finite_prob_space) sum_over_space_eq_1: "(\<Sum>x\<in>space M. measure M {x}) = 1" |
|
402 |
using prob_space sum_over_space by simp |
|
403 |
||
404 |
lemma (in finite_prob_space) positive_distribution: "0 \<le> distribution X x" |
|
405 |
unfolding distribution_def using positive sets_eq_Pow by simp |
|
406 |
||
407 |
lemma (in finite_prob_space) joint_distribution_restriction_fst: |
|
408 |
"joint_distribution X Y A \<le> distribution X (fst ` A)" |
|
409 |
unfolding distribution_def |
|
410 |
proof (safe intro!: measure_mono) |
|
411 |
fix x assume "x \<in> space M" and *: "(X x, Y x) \<in> A" |
|
412 |
show "x \<in> X -` fst ` A" |
|
413 |
by (auto intro!: image_eqI[OF _ *]) |
|
414 |
qed (simp_all add: sets_eq_Pow) |
|
415 |
||
416 |
lemma (in finite_prob_space) joint_distribution_restriction_snd: |
|
417 |
"joint_distribution X Y A \<le> distribution Y (snd ` A)" |
|
418 |
unfolding distribution_def |
|
419 |
proof (safe intro!: measure_mono) |
|
420 |
fix x assume "x \<in> space M" and *: "(X x, Y x) \<in> A" |
|
421 |
show "x \<in> Y -` snd ` A" |
|
422 |
by (auto intro!: image_eqI[OF _ *]) |
|
423 |
qed (simp_all add: sets_eq_Pow) |
|
424 |
||
425 |
lemma (in finite_prob_space) distribution_order: |
|
426 |
shows "0 \<le> distribution X x'" |
|
427 |
and "(distribution X x' \<noteq> 0) \<longleftrightarrow> (0 < distribution X x')" |
|
428 |
and "r \<le> joint_distribution X Y {(x, y)} \<Longrightarrow> r \<le> distribution X {x}" |
|
429 |
and "r \<le> joint_distribution X Y {(x, y)} \<Longrightarrow> r \<le> distribution Y {y}" |
|
430 |
and "r < joint_distribution X Y {(x, y)} \<Longrightarrow> r < distribution X {x}" |
|
431 |
and "r < joint_distribution X Y {(x, y)} \<Longrightarrow> r < distribution Y {y}" |
|
432 |
and "distribution X {x} = 0 \<Longrightarrow> joint_distribution X Y {(x, y)} = 0" |
|
433 |
and "distribution Y {y} = 0 \<Longrightarrow> joint_distribution X Y {(x, y)} = 0" |
|
434 |
using positive_distribution[of X x'] |
|
435 |
positive_distribution[of "\<lambda>x. (X x, Y x)" "{(x, y)}"] |
|
436 |
joint_distribution_restriction_fst[of X Y "{(x, y)}"] |
|
437 |
joint_distribution_restriction_snd[of X Y "{(x, y)}"] |
|
438 |
by auto |
|
439 |
||
440 |
lemma (in finite_prob_space) finite_product_measure_space: |
|
35977 | 441 |
assumes "finite s1" "finite s2" |
442 |
shows "finite_measure_space \<lparr> space = s1 \<times> s2, sets = Pow (s1 \<times> s2), measure = joint_distribution X Y\<rparr>" |
|
443 |
(is "finite_measure_space ?M") |
|
444 |
proof (rule finite_Pow_additivity_sufficient) |
|
445 |
show "positive ?M (measure ?M)" |
|
446 |
unfolding positive_def using positive'[unfolded positive_def] assms sets_eq_Pow |
|
36624 | 447 |
by (simp add: distribution_def) |
35977 | 448 |
|
449 |
show "additive ?M (measure ?M)" unfolding additive_def |
|
450 |
proof safe |
|
451 |
fix x y |
|
452 |
have A: "((\<lambda>x. (X x, Y x)) -` x) \<inter> space M \<in> sets M" using assms sets_eq_Pow by auto |
|
453 |
have B: "((\<lambda>x. (X x, Y x)) -` y) \<inter> space M \<in> sets M" using assms sets_eq_Pow by auto |
|
454 |
assume "x \<inter> y = {}" |
|
455 |
from additive[unfolded additive_def, rule_format, OF A B] this |
|
456 |
show "measure ?M (x \<union> y) = measure ?M x + measure ?M y" |
|
36624 | 457 |
apply (simp add: distribution_def) |
35977 | 458 |
apply (subst Int_Un_distrib2) |
459 |
by auto |
|
460 |
qed |
|
461 |
||
462 |
show "finite (space ?M)" |
|
463 |
using assms by auto |
|
464 |
||
465 |
show "sets ?M = Pow (space ?M)" |
|
466 |
by simp |
|
467 |
qed |
|
468 |
||
36624 | 469 |
lemma (in finite_prob_space) finite_product_measure_space_of_images: |
35977 | 470 |
shows "finite_measure_space \<lparr> space = X ` space M \<times> Y ` space M, |
471 |
sets = Pow (X ` space M \<times> Y ` space M), |
|
472 |
measure = joint_distribution X Y\<rparr>" |
|
473 |
(is "finite_measure_space ?M") |
|
36624 | 474 |
using finite_space by (auto intro!: finite_product_measure_space) |
475 |
||
476 |
lemma (in finite_prob_space) finite_measure_space: |
|
477 |
shows "finite_measure_space \<lparr> space = X ` space M, sets = Pow (X ` space M), measure = distribution X\<rparr>" |
|
478 |
(is "finite_measure_space ?S") |
|
479 |
proof (rule finite_Pow_additivity_sufficient, simp_all) |
|
480 |
show "finite (X ` space M)" using finite_space by simp |
|
481 |
||
482 |
show "positive ?S (distribution X)" unfolding distribution_def |
|
483 |
unfolding positive_def using positive'[unfolded positive_def] sets_eq_Pow by auto |
|
484 |
||
485 |
show "additive ?S (distribution X)" unfolding additive_def distribution_def |
|
486 |
proof (simp, safe) |
|
487 |
fix x y |
|
488 |
have x: "(X -` x) \<inter> space M \<in> sets M" |
|
489 |
and y: "(X -` y) \<inter> space M \<in> sets M" using sets_eq_Pow by auto |
|
490 |
assume "x \<inter> y = {}" |
|
491 |
from additive[unfolded additive_def, rule_format, OF x y] this |
|
492 |
have "prob (((X -` x) \<union> (X -` y)) \<inter> space M) = |
|
493 |
prob ((X -` x) \<inter> space M) + prob ((X -` y) \<inter> space M)" |
|
494 |
apply (subst Int_Un_distrib2) |
|
495 |
by auto |
|
496 |
thus "prob ((X -` x \<union> X -` y) \<inter> space M) = prob (X -` x \<inter> space M) + prob (X -` y \<inter> space M)" |
|
497 |
by auto |
|
498 |
qed |
|
499 |
qed |
|
500 |
||
501 |
lemma (in finite_prob_space) finite_prob_space_of_images: |
|
502 |
"finite_prob_space \<lparr> space = X ` space M, sets = Pow (X ` space M), measure = distribution X\<rparr>" |
|
503 |
(is "finite_prob_space ?S") |
|
504 |
proof (simp add: finite_prob_space_eq, safe) |
|
505 |
show "finite_measure_space ?S" by (rule finite_measure_space) |
|
506 |
have "X -` X ` space M \<inter> space M = space M" by auto |
|
507 |
thus "distribution X (X`space M) = 1" |
|
508 |
by (simp add: distribution_def prob_space) |
|
509 |
qed |
|
510 |
||
511 |
lemma (in finite_prob_space) finite_product_prob_space_of_images: |
|
512 |
"finite_prob_space \<lparr> space = X ` space M \<times> Y ` space M, sets = Pow (X ` space M \<times> Y ` space M), |
|
513 |
measure = joint_distribution X Y\<rparr>" |
|
514 |
(is "finite_prob_space ?S") |
|
515 |
proof (simp add: finite_prob_space_eq, safe) |
|
516 |
show "finite_measure_space ?S" by (rule finite_product_measure_space_of_images) |
|
517 |
||
518 |
have "X -` X ` space M \<inter> Y -` Y ` space M \<inter> space M = space M" by auto |
|
519 |
thus "joint_distribution X Y (X ` space M \<times> Y ` space M) = 1" |
|
520 |
by (simp add: distribution_def prob_space vimage_Times comp_def) |
|
521 |
qed |
|
35977 | 522 |
|
35582 | 523 |
end |