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