author | hoelzl |
Thu, 13 Nov 2014 17:19:52 +0100 | |
changeset 59000 | 6eb0725503fc |
parent 58876 | 1888e3cb8048 |
child 59353 | f0707dc3d9aa |
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 |
||
58876 | 6 |
section {*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'" |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
29 |
abbreviation (in prob_space) "expectation \<equiv> integral\<^sup>L M" |
57235
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
30 |
abbreviation (in prob_space) "variance X \<equiv> integral\<^sup>L M (\<lambda>x. (X x - expectation X)\<^sup>2)" |
35582 | 31 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
32 |
lemma (in prob_space) finite_measure [simp]: "finite_measure M" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
33 |
by unfold_locales |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
34 |
|
47694 | 35 |
lemma (in prob_space) prob_space_distr: |
36 |
assumes f: "f \<in> measurable M M'" shows "prob_space (distr M M' f)" |
|
37 |
proof (rule prob_spaceI) |
|
38 |
have "f -` space M' \<inter> space M = space M" using f by (auto dest: measurable_space) |
|
39 |
with f show "emeasure (distr M M' f) (space (distr M M' f)) = 1" |
|
40 |
by (auto simp: emeasure_distr emeasure_space_1) |
|
43339 | 41 |
qed |
42 |
||
40859 | 43 |
lemma (in prob_space) prob_space: "prob (space M) = 1" |
47694 | 44 |
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
|
45 |
|
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset
|
46 |
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
|
47 |
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
|
48 |
|
47694 | 49 |
lemma (in prob_space) not_empty: "space M \<noteq> {}" |
50 |
using prob_space by auto |
|
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset
|
51 |
|
47694 | 52 |
lemma (in prob_space) measure_le_1: "emeasure M X \<le> 1" |
53 |
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
|
54 |
|
43339 | 55 |
lemma (in prob_space) AE_I_eq_1: |
47694 | 56 |
assumes "emeasure M {x\<in>space M. P x} = 1" "{x\<in>space M. P x} \<in> sets M" |
57 |
shows "AE x in M. P x" |
|
43339 | 58 |
proof (rule AE_I) |
47694 | 59 |
show "emeasure M (space M - {x \<in> space M. P x}) = 0" |
60 |
using assms emeasure_space_1 by (simp add: emeasure_compl) |
|
43339 | 61 |
qed (insert assms, auto) |
62 |
||
59000 | 63 |
lemma prob_space_restrict_space: |
64 |
"S \<in> sets M \<Longrightarrow> emeasure M S = 1 \<Longrightarrow> prob_space (restrict_space M S)" |
|
65 |
by (intro prob_spaceI) |
|
66 |
(simp add: emeasure_restrict_space space_restrict_space) |
|
67 |
||
40859 | 68 |
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
|
69 |
assumes A: "A \<in> events" |
38656 | 70 |
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
|
71 |
using finite_measure_compl[OF A] by (simp add: prob_space) |
35582 | 72 |
|
47694 | 73 |
lemma (in prob_space) AE_in_set_eq_1: |
74 |
assumes "A \<in> events" shows "(AE x in M. x \<in> A) \<longleftrightarrow> prob A = 1" |
|
75 |
proof |
|
76 |
assume ae: "AE x in M. x \<in> A" |
|
77 |
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
|
78 |
using `A \<in> events`[THEN sets.sets_into_space] by auto |
47694 | 79 |
with AE_E2[OF ae] `A \<in> events` have "1 - emeasure M A = 0" |
80 |
by (simp add: emeasure_compl emeasure_space_1) |
|
81 |
then show "prob A = 1" |
|
82 |
using `A \<in> events` by (simp add: emeasure_eq_measure one_ereal_def) |
|
83 |
next |
|
84 |
assume prob: "prob A = 1" |
|
85 |
show "AE x in M. x \<in> A" |
|
86 |
proof (rule AE_I) |
|
87 |
show "{x \<in> space M. x \<notin> A} \<subseteq> space M - A" by auto |
|
88 |
show "emeasure M (space M - A) = 0" |
|
89 |
using `A \<in> events` prob |
|
90 |
by (simp add: prob_compl emeasure_space_1 emeasure_eq_measure one_ereal_def) |
|
91 |
show "space M - A \<in> events" |
|
92 |
using `A \<in> events` by auto |
|
93 |
qed |
|
94 |
qed |
|
95 |
||
96 |
lemma (in prob_space) AE_False: "(AE x in M. False) \<longleftrightarrow> False" |
|
97 |
proof |
|
98 |
assume "AE x in M. False" |
|
99 |
then have "AE x in M. x \<in> {}" by simp |
|
100 |
then show False |
|
101 |
by (subst (asm) AE_in_set_eq_1) auto |
|
102 |
qed simp |
|
103 |
||
104 |
lemma (in prob_space) AE_prob_1: |
|
105 |
assumes "prob A = 1" shows "AE x in M. x \<in> A" |
|
106 |
proof - |
|
107 |
from `prob A = 1` have "A \<in> events" |
|
108 |
by (metis measure_notin_sets zero_neq_one) |
|
109 |
with AE_in_set_eq_1 assms show ?thesis by simp |
|
110 |
qed |
|
111 |
||
50098 | 112 |
lemma (in prob_space) AE_const[simp]: "(AE x in M. P) \<longleftrightarrow> P" |
113 |
by (cases P) (auto simp: AE_False) |
|
114 |
||
59000 | 115 |
lemma (in prob_space) ae_filter_bot: "ae_filter M \<noteq> bot" |
116 |
by (simp add: trivial_limit_def) |
|
117 |
||
50098 | 118 |
lemma (in prob_space) AE_contr: |
119 |
assumes ae: "AE \<omega> in M. P \<omega>" "AE \<omega> in M. \<not> P \<omega>" |
|
120 |
shows False |
|
121 |
proof - |
|
122 |
from ae have "AE \<omega> in M. False" by eventually_elim auto |
|
123 |
then show False by auto |
|
124 |
qed |
|
125 |
||
59000 | 126 |
lemma (in prob_space) emeasure_eq_1_AE: |
127 |
"S \<in> sets M \<Longrightarrow> AE x in M. x \<in> S \<Longrightarrow> emeasure M S = 1" |
|
128 |
by (subst emeasure_eq_AE[where B="space M"]) (auto simp: emeasure_space_1) |
|
129 |
||
57025 | 130 |
lemma (in prob_space) integral_ge_const: |
131 |
fixes c :: real |
|
132 |
shows "integrable M f \<Longrightarrow> (AE x in M. c \<le> f x) \<Longrightarrow> c \<le> (\<integral>x. f x \<partial>M)" |
|
133 |
using integral_mono_AE[of M "\<lambda>x. c" f] prob_space by simp |
|
134 |
||
135 |
lemma (in prob_space) integral_le_const: |
|
136 |
fixes c :: real |
|
137 |
shows "integrable M f \<Longrightarrow> (AE x in M. f x \<le> c) \<Longrightarrow> (\<integral>x. f x \<partial>M) \<le> c" |
|
138 |
using integral_mono_AE[of M f "\<lambda>x. c"] prob_space by simp |
|
139 |
||
140 |
lemma (in prob_space) nn_integral_ge_const: |
|
141 |
"(AE x in M. c \<le> f x) \<Longrightarrow> c \<le> (\<integral>\<^sup>+x. f x \<partial>M)" |
|
142 |
using nn_integral_mono_AE[of "\<lambda>x. c" f M] emeasure_space_1 |
|
143 |
by (simp add: nn_integral_const_If split: split_if_asm) |
|
144 |
||
145 |
lemma (in prob_space) nn_integral_le_const: |
|
146 |
"0 \<le> c \<Longrightarrow> (AE x in M. f x \<le> c) \<Longrightarrow> (\<integral>\<^sup>+x. f x \<partial>M) \<le> c" |
|
147 |
using nn_integral_mono_AE[of f "\<lambda>x. c" M] emeasure_space_1 |
|
148 |
by (simp add: nn_integral_const_If split: split_if_asm) |
|
149 |
||
43339 | 150 |
lemma (in prob_space) expectation_less: |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56166
diff
changeset
|
151 |
fixes X :: "_ \<Rightarrow> real" |
43339 | 152 |
assumes [simp]: "integrable M X" |
49786 | 153 |
assumes gt: "AE x in M. X x < b" |
43339 | 154 |
shows "expectation X < b" |
155 |
proof - |
|
156 |
have "expectation X < expectation (\<lambda>x. b)" |
|
47694 | 157 |
using gt emeasure_space_1 |
43340
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
43339
diff
changeset
|
158 |
by (intro integral_less_AE_space) auto |
43339 | 159 |
then show ?thesis using prob_space by simp |
160 |
qed |
|
161 |
||
162 |
lemma (in prob_space) expectation_greater: |
|
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56166
diff
changeset
|
163 |
fixes X :: "_ \<Rightarrow> real" |
43339 | 164 |
assumes [simp]: "integrable M X" |
49786 | 165 |
assumes gt: "AE x in M. a < X x" |
43339 | 166 |
shows "a < expectation X" |
167 |
proof - |
|
168 |
have "expectation (\<lambda>x. a) < expectation X" |
|
47694 | 169 |
using gt emeasure_space_1 |
43340
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
43339
diff
changeset
|
170 |
by (intro integral_less_AE_space) auto |
43339 | 171 |
then show ?thesis using prob_space by simp |
172 |
qed |
|
173 |
||
174 |
lemma (in prob_space) jensens_inequality: |
|
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56166
diff
changeset
|
175 |
fixes q :: "real \<Rightarrow> real" |
49786 | 176 |
assumes X: "integrable M X" "AE x in M. X x \<in> I" |
43339 | 177 |
assumes I: "I = {a <..< b} \<or> I = {a <..} \<or> I = {..< b} \<or> I = UNIV" |
178 |
assumes q: "integrable M (\<lambda>x. q (X x))" "convex_on I q" |
|
179 |
shows "q (expectation X) \<le> expectation (\<lambda>x. q (X x))" |
|
180 |
proof - |
|
46731 | 181 |
let ?F = "\<lambda>x. Inf ((\<lambda>t. (q x - q t) / (x - t)) ` ({x<..} \<inter> I))" |
49786 | 182 |
from X(2) AE_False have "I \<noteq> {}" by auto |
43339 | 183 |
|
184 |
from I have "open I" by auto |
|
185 |
||
186 |
note I |
|
187 |
moreover |
|
188 |
{ assume "I \<subseteq> {a <..}" |
|
189 |
with X have "a < expectation X" |
|
190 |
by (intro expectation_greater) auto } |
|
191 |
moreover |
|
192 |
{ assume "I \<subseteq> {..< b}" |
|
193 |
with X have "expectation X < b" |
|
194 |
by (intro expectation_less) auto } |
|
195 |
ultimately have "expectation X \<in> I" |
|
196 |
by (elim disjE) (auto simp: subset_eq) |
|
197 |
moreover |
|
198 |
{ fix y assume y: "y \<in> I" |
|
199 |
with q(2) `open I` have "Sup ((\<lambda>x. q x + ?F x * (y - x)) ` I) = q y" |
|
56166 | 200 |
by (auto intro!: cSup_eq_maximum convex_le_Inf_differential image_eqI [OF _ y] simp: interior_open simp del: Sup_image_eq Inf_image_eq) } |
43339 | 201 |
ultimately have "q (expectation X) = Sup ((\<lambda>x. q x + ?F x * (expectation X - x)) ` I)" |
202 |
by simp |
|
203 |
also have "\<dots> \<le> expectation (\<lambda>w. q (X w))" |
|
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
50419
diff
changeset
|
204 |
proof (rule cSup_least) |
43339 | 205 |
show "(\<lambda>x. q x + ?F x * (expectation X - x)) ` I \<noteq> {}" |
206 |
using `I \<noteq> {}` by auto |
|
207 |
next |
|
208 |
fix k assume "k \<in> (\<lambda>x. q x + ?F x * (expectation X - x)) ` I" |
|
209 |
then guess x .. note x = this |
|
210 |
have "q x + ?F x * (expectation X - x) = expectation (\<lambda>w. q x + ?F x * (X w - x))" |
|
47694 | 211 |
using prob_space by (simp add: X) |
43339 | 212 |
also have "\<dots> \<le> expectation (\<lambda>w. q (X w))" |
213 |
using `x \<in> I` `open I` X(2) |
|
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56166
diff
changeset
|
214 |
apply (intro integral_mono_AE integrable_add integrable_mult_right integrable_diff |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56166
diff
changeset
|
215 |
integrable_const X q) |
49786 | 216 |
apply (elim eventually_elim1) |
217 |
apply (intro convex_le_Inf_differential) |
|
218 |
apply (auto simp: interior_open q) |
|
219 |
done |
|
43339 | 220 |
finally show "k \<le> expectation (\<lambda>w. q (X w))" using x by auto |
221 |
qed |
|
222 |
finally show "q (expectation X) \<le> expectation (\<lambda>x. q (X x))" . |
|
223 |
qed |
|
224 |
||
50001
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
225 |
subsection {* Introduce binder for probability *} |
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
226 |
|
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
227 |
syntax |
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
228 |
"_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
|
229 |
|
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
230 |
translations |
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
231 |
"\<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
|
232 |
|
58764
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
233 |
print_translation {* |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
234 |
let |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
235 |
fun to_pattern (Const (@{const_syntax Pair}, _) $ l $ r) = |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
236 |
Syntax.const @{const_syntax Pair} :: to_pattern l @ to_pattern r |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
237 |
| to_pattern (t as (Const (@{syntax_const "_bound"}, _)) $ _) = [t] |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
238 |
|
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
239 |
fun mk_pattern ((t, n) :: xs) = mk_patterns n xs |>> curry list_comb t |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
240 |
and mk_patterns 0 xs = ([], xs) |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
241 |
| mk_patterns n xs = |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
242 |
let |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
243 |
val (t, xs') = mk_pattern xs |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
244 |
val (ts, xs'') = mk_patterns (n - 1) xs' |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
245 |
in |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
246 |
(t :: ts, xs'') |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
247 |
end |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
248 |
|
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
249 |
fun unnest_tuples |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
250 |
(Const (@{syntax_const "_pattern"}, _) $ |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
251 |
t1 $ |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
252 |
(t as (Const (@{syntax_const "_pattern"}, _) $ _ $ _))) |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
253 |
= let |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
254 |
val (_ $ t2 $ t3) = unnest_tuples t |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
255 |
in |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
256 |
Syntax.const @{syntax_const "_pattern"} $ |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
257 |
unnest_tuples t1 $ |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
258 |
(Syntax.const @{syntax_const "_patterns"} $ t2 $ t3) |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
259 |
end |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
260 |
| unnest_tuples pat = pat |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
261 |
|
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
262 |
fun tr' [sig_alg, Const (@{const_syntax Collect}, _) $ t] = |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
263 |
let |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
264 |
val bound_dummyT = Const (@{syntax_const "_bound"}, dummyT) |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
265 |
|
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
266 |
fun go pattern elem |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
267 |
(Const (@{const_syntax "conj"}, _) $ |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
268 |
(Const (@{const_syntax Set.member}, _) $ elem' $ (Const (@{const_syntax space}, _) $ sig_alg')) $ |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
269 |
u) |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
270 |
= let |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
271 |
val _ = if sig_alg aconv sig_alg' andalso to_pattern elem' = rev elem then () else raise Match; |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
272 |
val (pat, rest) = mk_pattern (rev pattern); |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
273 |
val _ = case rest of [] => () | _ => raise Match |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
274 |
in |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
275 |
Syntax.const @{syntax_const "_prob"} $ unnest_tuples pat $ sig_alg $ u |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
276 |
end |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
277 |
| go pattern elem (Abs abs) = |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
278 |
let |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
279 |
val (x as (_ $ tx), t) = Syntax_Trans.atomic_abs_tr' abs |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
280 |
in |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
281 |
go ((x, 0) :: pattern) (bound_dummyT $ tx :: elem) t |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
282 |
end |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
283 |
| go pattern elem (Const (@{const_syntax case_prod}, _) $ t) = |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
284 |
go |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
285 |
((Syntax.const @{syntax_const "_pattern"}, 2) :: pattern) |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
286 |
(Syntax.const @{const_syntax Pair} :: elem) |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
287 |
t |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
288 |
in |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
289 |
go [] [] t |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
290 |
end |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
291 |
in |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
292 |
[(@{const_syntax Sigma_Algebra.measure}, K tr')] |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
293 |
end |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
294 |
*} |
ca2f59aef665
add print translation for probability notation \<P>
Andreas Lochbihler
parents:
57447
diff
changeset
|
295 |
|
50001
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
296 |
definition |
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
297 |
"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
|
298 |
|
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
299 |
syntax |
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
300 |
"_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
|
301 |
|
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
302 |
translations |
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
303 |
"\<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
|
304 |
|
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
305 |
lemma (in prob_space) AE_E_prob: |
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
306 |
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
|
307 |
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
|
308 |
proof - |
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
309 |
from ae[THEN AE_E] guess N . |
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
310 |
then show thesis |
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
311 |
by (intro that[of "space M - N"]) |
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
312 |
(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
|
313 |
qed |
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
314 |
|
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
315 |
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
|
316 |
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
|
317 |
|
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
318 |
lemma (in prob_space) prob_eq_AE: |
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
319 |
"(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
|
320 |
by (rule finite_measure_eq_AE) auto |
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
321 |
|
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
322 |
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
|
323 |
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
|
324 |
proof cases |
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
325 |
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
|
326 |
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
|
327 |
by (intro prob_eq_AE) auto |
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
328 |
then show ?thesis by simp |
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
329 |
qed (simp add: measure_notin_sets) |
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
330 |
|
50098 | 331 |
lemma (in prob_space) prob_Collect_eq_0: |
332 |
"{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)" |
|
333 |
using AE_iff_measurable[OF _ refl, of M "\<lambda>x. \<not> P x"] by (simp add: emeasure_eq_measure) |
|
334 |
||
335 |
lemma (in prob_space) prob_Collect_eq_1: |
|
336 |
"{x \<in> space M. P x} \<in> sets M \<Longrightarrow> \<P>(x in M. P x) = 1 \<longleftrightarrow> (AE x in M. P x)" |
|
337 |
using AE_in_set_eq_1[of "{x\<in>space M. P x}"] by simp |
|
338 |
||
339 |
lemma (in prob_space) prob_eq_0: |
|
340 |
"A \<in> sets M \<Longrightarrow> prob A = 0 \<longleftrightarrow> (AE x in M. x \<notin> A)" |
|
341 |
using AE_iff_measurable[OF _ refl, of M "\<lambda>x. x \<notin> A"] |
|
342 |
by (auto simp add: emeasure_eq_measure Int_def[symmetric]) |
|
343 |
||
344 |
lemma (in prob_space) prob_eq_1: |
|
345 |
"A \<in> sets M \<Longrightarrow> prob A = 1 \<longleftrightarrow> (AE x in M. x \<in> A)" |
|
346 |
using AE_in_set_eq_1[of A] by simp |
|
347 |
||
50001
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
348 |
lemma (in prob_space) prob_sums: |
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
349 |
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
|
350 |
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
|
351 |
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
|
352 |
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
|
353 |
proof - |
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
354 |
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
|
355 |
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
|
356 |
by (auto simp: disjoint_family_on_def) |
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
357 |
from S have ae_S: |
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
358 |
"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
|
359 |
"\<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
|
360 |
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
|
361 |
from ae_S have *: |
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
362 |
"\<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
|
363 |
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
|
364 |
from ae_S have **: |
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
365 |
"\<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
|
366 |
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
|
367 |
show ?thesis |
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
368 |
unfolding * ** using S P disj |
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
369 |
by (intro finite_measure_UNION) auto |
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
370 |
qed |
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
371 |
|
59000 | 372 |
lemma (in prob_space) prob_setsum: |
373 |
assumes [simp, intro]: "finite I" |
|
374 |
assumes P: "\<And>n. n \<in> I \<Longrightarrow> {x\<in>space M. P n x} \<in> events" |
|
375 |
assumes Q: "{x\<in>space M. Q x} \<in> events" |
|
376 |
assumes ae: "AE x in M. (\<forall>n\<in>I. P n x \<longrightarrow> Q x) \<and> (Q x \<longrightarrow> (\<exists>!n\<in>I. P n x))" |
|
377 |
shows "\<P>(x in M. Q x) = (\<Sum>n\<in>I. \<P>(x in M. P n x))" |
|
378 |
proof - |
|
379 |
from ae[THEN AE_E_prob] guess S . note S = this |
|
380 |
then have disj: "disjoint_family_on (\<lambda>n. {x\<in>space M. P n x} \<inter> S) I" |
|
381 |
by (auto simp: disjoint_family_on_def) |
|
382 |
from S have ae_S: |
|
383 |
"AE x in M. x \<in> {x\<in>space M. Q x} \<longleftrightarrow> x \<in> (\<Union>n\<in>I. {x\<in>space M. P n x} \<inter> S)" |
|
384 |
"\<And>n. n \<in> I \<Longrightarrow> 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" |
|
385 |
using ae by (auto dest!: AE_prob_1) |
|
386 |
from ae_S have *: |
|
387 |
"\<P>(x in M. Q x) = prob (\<Union>n\<in>I. {x\<in>space M. P n x} \<inter> S)" |
|
388 |
using P Q S by (intro finite_measure_eq_AE) (auto intro!: sets.Int) |
|
389 |
from ae_S have **: |
|
390 |
"\<And>n. n \<in> I \<Longrightarrow> \<P>(x in M. P n x) = prob ({x\<in>space M. P n x} \<inter> S)" |
|
391 |
using P Q S by (intro finite_measure_eq_AE) auto |
|
392 |
show ?thesis |
|
393 |
using S P disj |
|
394 |
by (auto simp add: * ** simp del: UN_simps intro!: finite_measure_finite_Union) |
|
395 |
qed |
|
396 |
||
54418 | 397 |
lemma (in prob_space) prob_EX_countable: |
398 |
assumes sets: "\<And>i. i \<in> I \<Longrightarrow> {x\<in>space M. P i x} \<in> sets M" and I: "countable I" |
|
399 |
assumes disj: "AE x in M. \<forall>i\<in>I. \<forall>j\<in>I. P i x \<longrightarrow> P j x \<longrightarrow> i = j" |
|
400 |
shows "\<P>(x in M. \<exists>i\<in>I. P i x) = (\<integral>\<^sup>+i. \<P>(x in M. P i x) \<partial>count_space I)" |
|
401 |
proof - |
|
402 |
let ?N= "\<lambda>x. \<exists>!i\<in>I. P i x" |
|
403 |
have "ereal (\<P>(x in M. \<exists>i\<in>I. P i x)) = \<P>(x in M. (\<exists>i\<in>I. P i x \<and> ?N x))" |
|
404 |
unfolding ereal.inject |
|
405 |
proof (rule prob_eq_AE) |
|
406 |
show "AE x in M. (\<exists>i\<in>I. P i x) = (\<exists>i\<in>I. P i x \<and> ?N x)" |
|
407 |
using disj by eventually_elim blast |
|
408 |
qed (auto intro!: sets.sets_Collect_countable_Ex' sets.sets_Collect_conj sets.sets_Collect_countable_Ex1' I sets)+ |
|
409 |
also have "\<P>(x in M. (\<exists>i\<in>I. P i x \<and> ?N x)) = emeasure M (\<Union>i\<in>I. {x\<in>space M. P i x \<and> ?N x})" |
|
410 |
unfolding emeasure_eq_measure by (auto intro!: arg_cong[where f=prob]) |
|
411 |
also have "\<dots> = (\<integral>\<^sup>+i. emeasure M {x\<in>space M. P i x \<and> ?N x} \<partial>count_space I)" |
|
412 |
by (rule emeasure_UN_countable) |
|
413 |
(auto intro!: sets.sets_Collect_countable_Ex' sets.sets_Collect_conj sets.sets_Collect_countable_Ex1' I sets |
|
414 |
simp: disjoint_family_on_def) |
|
415 |
also have "\<dots> = (\<integral>\<^sup>+i. \<P>(x in M. P i x) \<partial>count_space I)" |
|
416 |
unfolding emeasure_eq_measure using disj |
|
56996 | 417 |
by (intro nn_integral_cong ereal.inject[THEN iffD2] prob_eq_AE) |
54418 | 418 |
(auto intro!: sets.sets_Collect_countable_Ex' sets.sets_Collect_conj sets.sets_Collect_countable_Ex1' I sets)+ |
419 |
finally show ?thesis . |
|
420 |
qed |
|
421 |
||
50001
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
422 |
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
|
423 |
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
|
424 |
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
|
425 |
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
|
426 |
using P Q |
50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50104
diff
changeset
|
427 |
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
|
428 |
|
382bd3173584
add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset
|
429 |
|
40859 | 430 |
lemma (in prob_space) joint_distribution_Times_le_fst: |
47694 | 431 |
"random_variable MX X \<Longrightarrow> random_variable MY Y \<Longrightarrow> A \<in> sets MX \<Longrightarrow> B \<in> sets MY |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
432 |
\<Longrightarrow> emeasure (distr M (MX \<Otimes>\<^sub>M MY) (\<lambda>x. (X x, Y x))) (A \<times> B) \<le> emeasure (distr M MX X) A" |
47694 | 433 |
by (auto simp: emeasure_distr measurable_pair_iff comp_def intro!: emeasure_mono measurable_sets) |
40859 | 434 |
|
435 |
lemma (in prob_space) joint_distribution_Times_le_snd: |
|
47694 | 436 |
"random_variable MX X \<Longrightarrow> random_variable MY Y \<Longrightarrow> A \<in> sets MX \<Longrightarrow> B \<in> sets MY |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
437 |
\<Longrightarrow> emeasure (distr M (MX \<Otimes>\<^sub>M MY) (\<lambda>x. (X x, Y x))) (A \<times> B) \<le> emeasure (distr M MY Y) B" |
47694 | 438 |
by (auto simp: emeasure_distr measurable_pair_iff comp_def intro!: emeasure_mono measurable_sets) |
40859 | 439 |
|
57235
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
440 |
lemma (in prob_space) variance_eq: |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
441 |
fixes X :: "'a \<Rightarrow> real" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
442 |
assumes [simp]: "integrable M X" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
443 |
assumes [simp]: "integrable M (\<lambda>x. (X x)\<^sup>2)" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
444 |
shows "variance X = expectation (\<lambda>x. (X x)\<^sup>2) - (expectation X)\<^sup>2" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
445 |
by (simp add: field_simps prob_space power2_diff power2_eq_square[symmetric]) |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
446 |
|
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
447 |
lemma (in prob_space) variance_positive: "0 \<le> variance (X::'a \<Rightarrow> real)" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
448 |
by (intro integral_nonneg_AE) (auto intro!: integral_nonneg_AE) |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
449 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
450 |
lemma (in prob_space) variance_mean_zero: |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
451 |
"expectation X = 0 \<Longrightarrow> variance X = expectation (\<lambda>x. (X x)^2)" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
452 |
by simp |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
453 |
|
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
|
454 |
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
|
455 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
456 |
sublocale pair_prob_space \<subseteq> P: prob_space "M1 \<Otimes>\<^sub>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
|
457 |
proof |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
458 |
show "emeasure (M1 \<Otimes>\<^sub>M M2) (space (M1 \<Otimes>\<^sub>M M2)) = 1" |
49776 | 459 |
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
|
460 |
qed |
40859 | 461 |
|
47694 | 462 |
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
|
463 |
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
|
464 |
assumes prob_space: "\<And>i. prob_space (M i)" |
42988 | 465 |
|
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
|
466 |
sublocale product_prob_space \<subseteq> M: prob_space "M i" for i |
42988 | 467 |
by (rule prob_space) |
468 |
||
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
|
469 |
locale finite_product_prob_space = finite_product_sigma_finite M I + product_prob_space M I for M I |
42988 | 470 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
471 |
sublocale finite_product_prob_space \<subseteq> prob_space "\<Pi>\<^sub>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
|
472 |
proof |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
473 |
show "emeasure (\<Pi>\<^sub>M i\<in>I. M i) (space (\<Pi>\<^sub>M i\<in>I. M i)) = 1" |
57418 | 474 |
by (simp add: measure_times M.emeasure_space_1 setprod.neutral_const 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
|
475 |
qed |
42988 | 476 |
|
477 |
lemma (in finite_product_prob_space) prob_times: |
|
478 |
assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> sets (M i)" |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
479 |
shows "prob (\<Pi>\<^sub>E i\<in>I. X i) = (\<Prod>i\<in>I. M.prob i (X i))" |
42988 | 480 |
proof - |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
481 |
have "ereal (measure (\<Pi>\<^sub>M i\<in>I. M i) (\<Pi>\<^sub>E i\<in>I. X i)) = emeasure (\<Pi>\<^sub>M i\<in>I. M i) (\<Pi>\<^sub>E i\<in>I. X i)" |
47694 | 482 |
using X by (simp add: emeasure_eq_measure) |
483 |
also have "\<dots> = (\<Prod>i\<in>I. emeasure (M i) (X i))" |
|
42988 | 484 |
using measure_times X by simp |
47694 | 485 |
also have "\<dots> = ereal (\<Prod>i\<in>I. measure (M i) (X i))" |
486 |
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
|
487 |
finally show ?thesis by simp |
d9dfc733f25c
add product of probability spaces with finite cardinality
hoelzl
parents:
42858
diff
changeset
|
488 |
qed |
d9dfc733f25c
add product of probability spaces with finite cardinality
hoelzl
parents:
42858
diff
changeset
|
489 |
|
56994 | 490 |
subsection {* Distributions *} |
42892 | 491 |
|
47694 | 492 |
definition "distributed M N X f \<longleftrightarrow> distr M N X = density N f \<and> |
493 |
f \<in> borel_measurable N \<and> (AE x in N. 0 \<le> f x) \<and> X \<in> measurable M N" |
|
36624 | 494 |
|
47694 | 495 |
lemma |
50003 | 496 |
assumes "distributed M N X f" |
497 |
shows distributed_distr_eq_density: "distr M N X = density N f" |
|
498 |
and distributed_measurable: "X \<in> measurable M N" |
|
499 |
and distributed_borel_measurable: "f \<in> borel_measurable N" |
|
500 |
and distributed_AE: "(AE x in N. 0 \<le> f x)" |
|
501 |
using assms by (simp_all add: distributed_def) |
|
502 |
||
503 |
lemma |
|
504 |
assumes D: "distributed M N X f" |
|
505 |
shows distributed_measurable'[measurable_dest]: |
|
506 |
"g \<in> measurable L M \<Longrightarrow> (\<lambda>x. X (g x)) \<in> measurable L N" |
|
507 |
and distributed_borel_measurable'[measurable_dest]: |
|
508 |
"h \<in> measurable L N \<Longrightarrow> (\<lambda>x. f (h x)) \<in> borel_measurable L" |
|
509 |
using distributed_measurable[OF D] distributed_borel_measurable[OF D] |
|
510 |
by simp_all |
|
39097 | 511 |
|
47694 | 512 |
lemma |
513 |
shows distributed_real_measurable: "distributed M N X (\<lambda>x. ereal (f x)) \<Longrightarrow> f \<in> borel_measurable N" |
|
514 |
and distributed_real_AE: "distributed M N X (\<lambda>x. ereal (f x)) \<Longrightarrow> (AE x in N. 0 \<le> f x)" |
|
515 |
by (simp_all add: distributed_def borel_measurable_ereal_iff) |
|
35977 | 516 |
|
50003 | 517 |
lemma |
518 |
assumes D: "distributed M N X (\<lambda>x. ereal (f x))" |
|
519 |
shows distributed_real_measurable'[measurable_dest]: |
|
520 |
"h \<in> measurable L N \<Longrightarrow> (\<lambda>x. f (h x)) \<in> borel_measurable L" |
|
521 |
using distributed_real_measurable[OF D] |
|
522 |
by simp_all |
|
523 |
||
524 |
lemma |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
525 |
assumes D: "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) f" |
50003 | 526 |
shows joint_distributed_measurable1[measurable_dest]: |
527 |
"h1 \<in> measurable N M \<Longrightarrow> (\<lambda>x. X (h1 x)) \<in> measurable N S" |
|
528 |
and joint_distributed_measurable2[measurable_dest]: |
|
529 |
"h2 \<in> measurable N M \<Longrightarrow> (\<lambda>x. Y (h2 x)) \<in> measurable N T" |
|
530 |
using measurable_compose[OF distributed_measurable[OF D] measurable_fst] |
|
531 |
using measurable_compose[OF distributed_measurable[OF D] measurable_snd] |
|
532 |
by auto |
|
533 |
||
47694 | 534 |
lemma distributed_count_space: |
535 |
assumes X: "distributed M (count_space A) X P" and a: "a \<in> A" and A: "finite A" |
|
536 |
shows "P a = emeasure M (X -` {a} \<inter> space M)" |
|
39097 | 537 |
proof - |
47694 | 538 |
have "emeasure M (X -` {a} \<inter> space M) = emeasure (distr M (count_space A) X) {a}" |
50003 | 539 |
using X a A by (simp add: emeasure_distr) |
47694 | 540 |
also have "\<dots> = emeasure (density (count_space A) P) {a}" |
541 |
using X by (simp add: distributed_distr_eq_density) |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
542 |
also have "\<dots> = (\<integral>\<^sup>+x. P a * indicator {a} x \<partial>count_space A)" |
56996 | 543 |
using X a by (auto simp add: emeasure_density distributed_def indicator_def intro!: nn_integral_cong) |
47694 | 544 |
also have "\<dots> = P a" |
56996 | 545 |
using X a by (subst nn_integral_cmult_indicator) (auto simp: distributed_def one_ereal_def[symmetric] AE_count_space) |
47694 | 546 |
finally show ?thesis .. |
39092 | 547 |
qed |
35977 | 548 |
|
47694 | 549 |
lemma distributed_cong_density: |
550 |
"(AE x in N. f x = g x) \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> f \<in> borel_measurable N \<Longrightarrow> |
|
551 |
distributed M N X f \<longleftrightarrow> distributed M N X g" |
|
552 |
by (auto simp: distributed_def intro!: density_cong) |
|
553 |
||
554 |
lemma subdensity: |
|
555 |
assumes T: "T \<in> measurable P Q" |
|
556 |
assumes f: "distributed M P X f" |
|
557 |
assumes g: "distributed M Q Y g" |
|
558 |
assumes Y: "Y = T \<circ> X" |
|
559 |
shows "AE x in P. g (T x) = 0 \<longrightarrow> f x = 0" |
|
560 |
proof - |
|
561 |
have "{x\<in>space Q. g x = 0} \<in> null_sets (distr M Q (T \<circ> X))" |
|
562 |
using g Y by (auto simp: null_sets_density_iff distributed_def) |
|
563 |
also have "distr M Q (T \<circ> X) = distr (distr M P X) Q T" |
|
564 |
using T f[THEN distributed_measurable] by (rule distr_distr[symmetric]) |
|
565 |
finally have "T -` {x\<in>space Q. g x = 0} \<inter> space P \<in> null_sets (distr M P X)" |
|
566 |
using T by (subst (asm) null_sets_distr_iff) auto |
|
567 |
also have "T -` {x\<in>space Q. g x = 0} \<inter> space P = {x\<in>space P. g (T x) = 0}" |
|
568 |
using T by (auto dest: measurable_space) |
|
569 |
finally show ?thesis |
|
570 |
using f g by (auto simp add: null_sets_density_iff distributed_def) |
|
35977 | 571 |
qed |
572 |
||
47694 | 573 |
lemma subdensity_real: |
574 |
fixes g :: "'a \<Rightarrow> real" and f :: "'b \<Rightarrow> real" |
|
575 |
assumes T: "T \<in> measurable P Q" |
|
576 |
assumes f: "distributed M P X f" |
|
577 |
assumes g: "distributed M Q Y g" |
|
578 |
assumes Y: "Y = T \<circ> X" |
|
579 |
shows "AE x in P. g (T x) = 0 \<longrightarrow> f x = 0" |
|
580 |
using subdensity[OF T, of M X "\<lambda>x. ereal (f x)" Y "\<lambda>x. ereal (g x)"] assms by auto |
|
581 |
||
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
582 |
lemma distributed_emeasure: |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
583 |
"distributed M N X f \<Longrightarrow> A \<in> sets N \<Longrightarrow> emeasure M (X -` A \<inter> space M) = (\<integral>\<^sup>+x. f x * indicator A x \<partial>N)" |
50003 | 584 |
by (auto simp: distributed_AE |
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
585 |
distributed_distr_eq_density[symmetric] emeasure_density[symmetric] emeasure_distr) |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
586 |
|
56996 | 587 |
lemma distributed_nn_integral: |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
588 |
"distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> (\<integral>\<^sup>+x. f x * g x \<partial>N) = (\<integral>\<^sup>+x. g (X x) \<partial>M)" |
50003 | 589 |
by (auto simp: distributed_AE |
56996 | 590 |
distributed_distr_eq_density[symmetric] nn_integral_density[symmetric] nn_integral_distr) |
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
591 |
|
47694 | 592 |
lemma distributed_integral: |
593 |
"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 | 594 |
by (auto simp: distributed_real_AE |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56166
diff
changeset
|
595 |
distributed_distr_eq_density[symmetric] integral_real_density[symmetric] integral_distr) |
47694 | 596 |
|
597 |
lemma distributed_transform_integral: |
|
598 |
assumes Px: "distributed M N X Px" |
|
599 |
assumes "distributed M P Y Py" |
|
600 |
assumes Y: "Y = T \<circ> X" and T: "T \<in> measurable N P" and f: "f \<in> borel_measurable P" |
|
601 |
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
|
602 |
proof - |
47694 | 603 |
have "(\<integral>x. Py x * f x \<partial>P) = (\<integral>x. f (Y x) \<partial>M)" |
604 |
by (rule distributed_integral) fact+ |
|
605 |
also have "\<dots> = (\<integral>x. f (T (X x)) \<partial>M)" |
|
606 |
using Y by simp |
|
607 |
also have "\<dots> = (\<integral>x. Px x * f (T x) \<partial>N)" |
|
608 |
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
|
609 |
finally show ?thesis . |
39092 | 610 |
qed |
36624 | 611 |
|
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
612 |
lemma (in prob_space) distributed_unique: |
47694 | 613 |
assumes Px: "distributed M S X Px" |
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
614 |
assumes Py: "distributed M S X Py" |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
615 |
shows "AE x in S. Px x = Py x" |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
616 |
proof - |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
617 |
interpret X: prob_space "distr M S X" |
50003 | 618 |
using Px by (intro prob_space_distr) simp |
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
619 |
have "sigma_finite_measure (distr M S X)" .. |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
620 |
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
|
621 |
show ?thesis |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
622 |
by (auto simp: distributed_def) |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
623 |
qed |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
624 |
|
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
625 |
lemma (in prob_space) distributed_jointI: |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
626 |
assumes "sigma_finite_measure S" "sigma_finite_measure T" |
50003 | 627 |
assumes X[measurable]: "X \<in> measurable M S" and Y[measurable]: "Y \<in> measurable M T" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
628 |
assumes [measurable]: "f \<in> borel_measurable (S \<Otimes>\<^sub>M T)" and f: "AE x in S \<Otimes>\<^sub>M T. 0 \<le> f x" |
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
629 |
assumes eq: "\<And>A B. A \<in> sets S \<Longrightarrow> B \<in> sets T \<Longrightarrow> |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
630 |
emeasure M {x \<in> space M. X x \<in> A \<and> Y x \<in> B} = (\<integral>\<^sup>+x. (\<integral>\<^sup>+y. f (x, y) * indicator B y \<partial>T) * indicator A x \<partial>S)" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
631 |
shows "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) f" |
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
632 |
unfolding distributed_def |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
633 |
proof safe |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
634 |
interpret S: sigma_finite_measure S by fact |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
635 |
interpret T: sigma_finite_measure T by fact |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
636 |
interpret ST: pair_sigma_finite S T by default |
47694 | 637 |
|
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
638 |
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
|
639 |
let ?E = "{a \<times> b |a b. a \<in> sets S \<and> b \<in> sets T}" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
640 |
let ?P = "S \<Otimes>\<^sub>M T" |
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
641 |
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
|
642 |
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
|
643 |
show "?E \<subseteq> Pow (space ?P)" |
50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50104
diff
changeset
|
644 |
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
|
645 |
show "sets ?L = sigma_sets (space ?P) ?E" |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
646 |
by (simp add: sets_pair_measure space_pair_measure) |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
647 |
then show "sets ?R = sigma_sets (space ?P) ?E" |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
648 |
by simp |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
649 |
next |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
650 |
interpret L: prob_space ?L |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
651 |
by (rule prob_space_distr) (auto intro!: measurable_Pair) |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
652 |
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
|
653 |
using F by (auto simp: space_pair_measure) |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
654 |
next |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
655 |
fix E assume "E \<in> ?E" |
50003 | 656 |
then obtain A B where E[simp]: "E = A \<times> B" |
657 |
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
|
658 |
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
|
659 |
by (auto intro!: arg_cong[where f="emeasure M"] simp add: emeasure_distr measurable_Pair) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
660 |
also have "\<dots> = (\<integral>\<^sup>+x. (\<integral>\<^sup>+y. (f (x, y) * indicator B y) * indicator A x \<partial>T) \<partial>S)" |
56996 | 661 |
using f by (auto simp add: eq nn_integral_multc intro!: nn_integral_cong) |
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
662 |
also have "\<dots> = emeasure ?R E" |
56996 | 663 |
by (auto simp add: emeasure_density T.nn_integral_fst[symmetric] |
664 |
intro!: nn_integral_cong split: split_indicator) |
|
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
665 |
finally show "emeasure ?L E = emeasure ?R E" . |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
666 |
qed |
50003 | 667 |
qed (auto simp: f) |
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
668 |
|
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
669 |
lemma (in prob_space) distributed_swap: |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
670 |
assumes "sigma_finite_measure S" "sigma_finite_measure T" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
671 |
assumes Pxy: "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) Pxy" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
672 |
shows "distributed M (T \<Otimes>\<^sub>M S) (\<lambda>x. (Y x, X x)) (\<lambda>(x, y). Pxy (y, x))" |
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
673 |
proof - |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
674 |
interpret S: sigma_finite_measure S by fact |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
675 |
interpret T: sigma_finite_measure T by fact |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
676 |
interpret ST: pair_sigma_finite S T by default |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
677 |
interpret TS: pair_sigma_finite T S by default |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
678 |
|
50003 | 679 |
note Pxy[measurable] |
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
680 |
show ?thesis |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
681 |
apply (subst TS.distr_pair_swap) |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
682 |
unfolding distributed_def |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
683 |
proof safe |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
684 |
let ?D = "distr (S \<Otimes>\<^sub>M T) (T \<Otimes>\<^sub>M S) (\<lambda>(x, y). (y, x))" |
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
685 |
show 1: "(\<lambda>(x, y). Pxy (y, x)) \<in> borel_measurable ?D" |
50003 | 686 |
by auto |
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
687 |
with Pxy |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
688 |
show "AE x in distr (S \<Otimes>\<^sub>M T) (T \<Otimes>\<^sub>M S) (\<lambda>(x, y). (y, x)). 0 \<le> (case x of (x, y) \<Rightarrow> Pxy (y, x))" |
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
689 |
by (subst AE_distr_iff) |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
690 |
(auto dest!: distributed_AE |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
691 |
simp: measurable_split_conv split_beta |
51683
baefa3b461c2
generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51475
diff
changeset
|
692 |
intro!: measurable_Pair) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
693 |
show 2: "random_variable (distr (S \<Otimes>\<^sub>M T) (T \<Otimes>\<^sub>M S) (\<lambda>(x, y). (y, x))) (\<lambda>x. (Y x, X x))" |
50003 | 694 |
using Pxy by auto |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
695 |
{ fix A assume A: "A \<in> sets (T \<Otimes>\<^sub>M S)" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
696 |
let ?B = "(\<lambda>(x, y). (y, x)) -` A \<inter> space (S \<Otimes>\<^sub>M T)" |
50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50104
diff
changeset
|
697 |
from sets.sets_into_space[OF A] |
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
698 |
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
|
699 |
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
|
700 |
by (auto intro!: arg_cong2[where f=emeasure] simp: space_pair_measure) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
701 |
also have "\<dots> = (\<integral>\<^sup>+ x. Pxy x * indicator ?B x \<partial>(S \<Otimes>\<^sub>M T))" |
50003 | 702 |
using Pxy A by (intro distributed_emeasure) auto |
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
703 |
finally have "emeasure M ((\<lambda>x. (Y x, X x)) -` A \<inter> space M) = |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
704 |
(\<integral>\<^sup>+ x. Pxy x * indicator A (snd x, fst x) \<partial>(S \<Otimes>\<^sub>M T))" |
56996 | 705 |
by (auto intro!: nn_integral_cong split: split_indicator) } |
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
706 |
note * = this |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
707 |
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
|
708 |
apply (intro measure_eqI) |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
709 |
apply (simp_all add: emeasure_distr[OF 2] emeasure_density[OF 1]) |
56996 | 710 |
apply (subst nn_integral_distr) |
50003 | 711 |
apply (auto intro!: * simp: comp_def split_beta) |
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
712 |
done |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
713 |
qed |
36624 | 714 |
qed |
715 |
||
47694 | 716 |
lemma (in prob_space) distr_marginal1: |
717 |
assumes "sigma_finite_measure S" "sigma_finite_measure T" |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
718 |
assumes Pxy: "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) Pxy" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
719 |
defines "Px \<equiv> \<lambda>x. (\<integral>\<^sup>+z. Pxy (x, z) \<partial>T)" |
47694 | 720 |
shows "distributed M S X Px" |
721 |
unfolding distributed_def |
|
722 |
proof safe |
|
723 |
interpret S: sigma_finite_measure S by fact |
|
724 |
interpret T: sigma_finite_measure T by fact |
|
725 |
interpret ST: pair_sigma_finite S T by default |
|
726 |
||
50003 | 727 |
note Pxy[measurable] |
728 |
show X: "X \<in> measurable M S" by simp |
|
47694 | 729 |
|
50003 | 730 |
show borel: "Px \<in> borel_measurable S" |
56996 | 731 |
by (auto intro!: T.nn_integral_fst simp: Px_def) |
39097 | 732 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
733 |
interpret Pxy: prob_space "distr M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x))" |
50003 | 734 |
by (intro prob_space_distr) simp |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
735 |
have "(\<integral>\<^sup>+ x. max 0 (- Pxy x) \<partial>(S \<Otimes>\<^sub>M T)) = (\<integral>\<^sup>+ x. 0 \<partial>(S \<Otimes>\<^sub>M T))" |
47694 | 736 |
using Pxy |
56996 | 737 |
by (intro nn_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
|
738 |
|
47694 | 739 |
show "distr M S X = density S Px" |
740 |
proof (rule measure_eqI) |
|
741 |
fix A assume A: "A \<in> sets (distr M S X)" |
|
50003 | 742 |
with X measurable_space[of Y M T] |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
743 |
have "emeasure (distr M S X) A = emeasure (distr M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x))) (A \<times> space T)" |
50003 | 744 |
by (auto simp add: emeasure_distr intro!: arg_cong[where f="emeasure M"]) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
745 |
also have "\<dots> = emeasure (density (S \<Otimes>\<^sub>M T) Pxy) (A \<times> space T)" |
47694 | 746 |
using Pxy by (simp add: distributed_def) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
747 |
also have "\<dots> = \<integral>\<^sup>+ x. \<integral>\<^sup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T \<partial>S" |
47694 | 748 |
using A borel Pxy |
56996 | 749 |
by (simp add: emeasure_density T.nn_integral_fst[symmetric]) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
750 |
also have "\<dots> = \<integral>\<^sup>+ x. Px x * indicator A x \<partial>S" |
56996 | 751 |
apply (rule nn_integral_cong_AE) |
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
752 |
using Pxy[THEN distributed_AE, THEN ST.AE_pair] AE_space |
47694 | 753 |
proof eventually_elim |
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
754 |
fix x assume "x \<in> space S" "AE y in T. 0 \<le> Pxy (x, y)" |
47694 | 755 |
moreover have eq: "\<And>y. y \<in> space T \<Longrightarrow> indicator (A \<times> space T) (x, y) = indicator A x" |
756 |
by (auto simp: indicator_def) |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
757 |
ultimately have "(\<integral>\<^sup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T) = (\<integral>\<^sup>+ y. Pxy (x, y) \<partial>T) * indicator A x" |
56996 | 758 |
by (simp add: eq nn_integral_multc cong: nn_integral_cong) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
759 |
also have "(\<integral>\<^sup>+ y. Pxy (x, y) \<partial>T) = Px x" |
56996 | 760 |
by (simp add: Px_def ereal_real nn_integral_nonneg) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
761 |
finally show "(\<integral>\<^sup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T) = Px x * indicator A x" . |
47694 | 762 |
qed |
763 |
finally show "emeasure (distr M S X) A = emeasure (density S Px) A" |
|
764 |
using A borel Pxy by (simp add: emeasure_density) |
|
765 |
qed simp |
|
766 |
||
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
767 |
show "AE x in S. 0 \<le> Px x" |
56996 | 768 |
by (simp add: Px_def nn_integral_nonneg real_of_ereal_pos) |
40859 | 769 |
qed |
770 |
||
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
771 |
lemma (in prob_space) distr_marginal2: |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
772 |
assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
773 |
assumes Pxy: "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) Pxy" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
774 |
shows "distributed M T Y (\<lambda>y. (\<integral>\<^sup>+x. Pxy (x, y) \<partial>S))" |
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
775 |
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
|
776 |
|
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
777 |
lemma (in prob_space) distributed_marginal_eq_joint1: |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
778 |
assumes T: "sigma_finite_measure T" |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
779 |
assumes S: "sigma_finite_measure S" |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
780 |
assumes Px: "distributed M S X Px" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
781 |
assumes Pxy: "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) Pxy" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
782 |
shows "AE x in S. Px x = (\<integral>\<^sup>+y. Pxy (x, y) \<partial>T)" |
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
783 |
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
|
784 |
|
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
785 |
lemma (in prob_space) distributed_marginal_eq_joint2: |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
786 |
assumes T: "sigma_finite_measure T" |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
787 |
assumes S: "sigma_finite_measure S" |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
788 |
assumes Py: "distributed M T Y Py" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
789 |
assumes Pxy: "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) Pxy" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
790 |
shows "AE y in T. Py y = (\<integral>\<^sup>+x. Pxy (x, y) \<partial>S)" |
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
791 |
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
|
792 |
|
49795 | 793 |
lemma (in prob_space) distributed_joint_indep': |
794 |
assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T" |
|
50003 | 795 |
assumes X[measurable]: "distributed M S X Px" and Y[measurable]: "distributed M T Y Py" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
796 |
assumes indep: "distr M S X \<Otimes>\<^sub>M distr M T Y = distr M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x))" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
797 |
shows "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) (\<lambda>(x, y). Px x * Py y)" |
49795 | 798 |
unfolding distributed_def |
799 |
proof safe |
|
800 |
interpret S: sigma_finite_measure S by fact |
|
801 |
interpret T: sigma_finite_measure T by fact |
|
802 |
interpret ST: pair_sigma_finite S T by default |
|
803 |
||
804 |
interpret X: prob_space "density S Px" |
|
805 |
unfolding distributed_distr_eq_density[OF X, symmetric] |
|
50003 | 806 |
by (rule prob_space_distr) simp |
49795 | 807 |
have sf_X: "sigma_finite_measure (density S Px)" .. |
808 |
||
809 |
interpret Y: prob_space "density T Py" |
|
810 |
unfolding distributed_distr_eq_density[OF Y, symmetric] |
|
50003 | 811 |
by (rule prob_space_distr) simp |
49795 | 812 |
have sf_Y: "sigma_finite_measure (density T Py)" .. |
813 |
||
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
814 |
show "distr M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) = density (S \<Otimes>\<^sub>M T) (\<lambda>(x, y). Px x * Py y)" |
49795 | 815 |
unfolding indep[symmetric] distributed_distr_eq_density[OF X] distributed_distr_eq_density[OF Y] |
816 |
using distributed_borel_measurable[OF X] distributed_AE[OF X] |
|
817 |
using distributed_borel_measurable[OF Y] distributed_AE[OF Y] |
|
50003 | 818 |
by (rule pair_measure_density[OF _ _ _ _ T sf_Y]) |
49795 | 819 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
820 |
show "random_variable (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x))" by auto |
49795 | 821 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
822 |
show Pxy: "(\<lambda>(x, y). Px x * Py y) \<in> borel_measurable (S \<Otimes>\<^sub>M T)" by auto |
49795 | 823 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
824 |
show "AE x in S \<Otimes>\<^sub>M T. 0 \<le> (case x of (x, y) \<Rightarrow> Px x * Py y)" |
51683
baefa3b461c2
generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51475
diff
changeset
|
825 |
apply (intro ST.AE_pair_measure borel_measurable_le Pxy borel_measurable_const) |
49795 | 826 |
using distributed_AE[OF X] |
827 |
apply eventually_elim |
|
828 |
using distributed_AE[OF Y] |
|
829 |
apply eventually_elim |
|
830 |
apply auto |
|
831 |
done |
|
832 |
qed |
|
833 |
||
57235
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
834 |
lemma distributed_integrable: |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
835 |
"distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
836 |
integrable N (\<lambda>x. f x * g x) \<longleftrightarrow> integrable M (\<lambda>x. g (X x))" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
837 |
by (auto simp: distributed_real_AE |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
838 |
distributed_distr_eq_density[symmetric] integrable_real_density[symmetric] integrable_distr_eq) |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
839 |
|
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
840 |
lemma distributed_transform_integrable: |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
841 |
assumes Px: "distributed M N X Px" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
842 |
assumes "distributed M P Y Py" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
843 |
assumes Y: "Y = (\<lambda>x. T (X x))" and T: "T \<in> measurable N P" and f: "f \<in> borel_measurable P" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
844 |
shows "integrable P (\<lambda>x. Py x * f x) \<longleftrightarrow> integrable N (\<lambda>x. Px x * f (T x))" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
845 |
proof - |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
846 |
have "integrable P (\<lambda>x. Py x * f x) \<longleftrightarrow> integrable M (\<lambda>x. f (Y x))" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
847 |
by (rule distributed_integrable) fact+ |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
848 |
also have "\<dots> \<longleftrightarrow> integrable M (\<lambda>x. f (T (X x)))" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
849 |
using Y by simp |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
850 |
also have "\<dots> \<longleftrightarrow> integrable N (\<lambda>x. Px x * f (T x))" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
851 |
using measurable_comp[OF T f] Px by (intro distributed_integrable[symmetric]) (auto simp: comp_def) |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
852 |
finally show ?thesis . |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
853 |
qed |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
854 |
|
57275
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
855 |
lemma distributed_integrable_var: |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
856 |
fixes X :: "'a \<Rightarrow> real" |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
857 |
shows "distributed M lborel X (\<lambda>x. ereal (f x)) \<Longrightarrow> integrable lborel (\<lambda>x. f x * x) \<Longrightarrow> integrable M X" |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
858 |
using distributed_integrable[of M lborel X f "\<lambda>x. x"] by simp |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
859 |
|
57235
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
860 |
lemma (in prob_space) distributed_variance: |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
861 |
fixes f::"real \<Rightarrow> real" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
862 |
assumes D: "distributed M lborel X f" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
863 |
shows "variance X = (\<integral>x. x\<^sup>2 * f (x + expectation X) \<partial>lborel)" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
864 |
proof (subst distributed_integral[OF D, symmetric]) |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
865 |
show "(\<integral> x. f x * (x - expectation X)\<^sup>2 \<partial>lborel) = (\<integral> x. x\<^sup>2 * f (x + expectation X) \<partial>lborel)" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
866 |
by (subst lborel_integral_real_affine[where c=1 and t="expectation X"]) (auto simp: ac_simps) |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
867 |
qed simp |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
868 |
|
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
869 |
lemma (in prob_space) variance_affine: |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
870 |
fixes f::"real \<Rightarrow> real" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
871 |
assumes [arith]: "b \<noteq> 0" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
872 |
assumes D[intro]: "distributed M lborel X f" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
873 |
assumes [simp]: "prob_space (density lborel f)" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
874 |
assumes I[simp]: "integrable M X" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
875 |
assumes I2[simp]: "integrable M (\<lambda>x. (X x)\<^sup>2)" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
876 |
shows "variance (\<lambda>x. a + b * X x) = b\<^sup>2 * variance X" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
877 |
by (subst variance_eq) |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
878 |
(auto simp: power2_sum power_mult_distrib prob_space variance_eq right_diff_distrib) |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57025
diff
changeset
|
879 |
|
47694 | 880 |
definition |
881 |
"simple_distributed M X f \<longleftrightarrow> distributed M (count_space (X`space M)) X (\<lambda>x. ereal (f x)) \<and> |
|
882 |
finite (X`space M)" |
|
42902 | 883 |
|
47694 | 884 |
lemma simple_distributed: |
885 |
"simple_distributed M X Px \<Longrightarrow> distributed M (count_space (X`space M)) X Px" |
|
886 |
unfolding simple_distributed_def by auto |
|
42902 | 887 |
|
47694 | 888 |
lemma simple_distributed_finite[dest]: "simple_distributed M X P \<Longrightarrow> finite (X`space M)" |
889 |
by (simp add: simple_distributed_def) |
|
42902 | 890 |
|
47694 | 891 |
lemma (in prob_space) distributed_simple_function_superset: |
892 |
assumes X: "simple_function M X" "\<And>x. x \<in> X ` space M \<Longrightarrow> P x = measure M (X -` {x} \<inter> space M)" |
|
893 |
assumes A: "X`space M \<subseteq> A" "finite A" |
|
894 |
defines "S \<equiv> count_space A" and "P' \<equiv> (\<lambda>x. if x \<in> X`space M then P x else 0)" |
|
895 |
shows "distributed M S X P'" |
|
896 |
unfolding distributed_def |
|
897 |
proof safe |
|
898 |
show "(\<lambda>x. ereal (P' x)) \<in> borel_measurable S" unfolding S_def by simp |
|
899 |
show "AE x in S. 0 \<le> ereal (P' x)" |
|
900 |
using X by (auto simp: S_def P'_def simple_distributed_def intro!: measure_nonneg) |
|
901 |
show "distr M S X = density S P'" |
|
902 |
proof (rule measure_eqI_finite) |
|
903 |
show "sets (distr M S X) = Pow A" "sets (density S P') = Pow A" |
|
904 |
using A unfolding S_def by auto |
|
905 |
show "finite A" by fact |
|
906 |
fix a assume a: "a \<in> A" |
|
907 |
then have "a \<notin> X`space M \<Longrightarrow> X -` {a} \<inter> space M = {}" by auto |
|
908 |
with A a X have "emeasure (distr M S X) {a} = P' a" |
|
909 |
by (subst emeasure_distr) |
|
50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset
|
910 |
(auto simp add: S_def P'_def simple_functionD emeasure_eq_measure measurable_count_space_eq2 |
47694 | 911 |
intro!: arg_cong[where f=prob]) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
912 |
also have "\<dots> = (\<integral>\<^sup>+x. ereal (P' a) * indicator {a} x \<partial>S)" |
47694 | 913 |
using A X a |
56996 | 914 |
by (subst nn_integral_cmult_indicator) |
47694 | 915 |
(auto simp: S_def P'_def simple_distributed_def simple_functionD measure_nonneg) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
916 |
also have "\<dots> = (\<integral>\<^sup>+x. ereal (P' x) * indicator {a} x \<partial>S)" |
56996 | 917 |
by (auto simp: indicator_def intro!: nn_integral_cong) |
47694 | 918 |
also have "\<dots> = emeasure (density S P') {a}" |
919 |
using a A by (intro emeasure_density[symmetric]) (auto simp: S_def) |
|
920 |
finally show "emeasure (distr M S X) {a} = emeasure (density S P') {a}" . |
|
921 |
qed |
|
922 |
show "random_variable S X" |
|
923 |
using X(1) A by (auto simp: measurable_def simple_functionD S_def) |
|
924 |
qed |
|
42902 | 925 |
|
47694 | 926 |
lemma (in prob_space) simple_distributedI: |
927 |
assumes X: "simple_function M X" "\<And>x. x \<in> X ` space M \<Longrightarrow> P x = measure M (X -` {x} \<inter> space M)" |
|
928 |
shows "simple_distributed M X P" |
|
929 |
unfolding simple_distributed_def |
|
930 |
proof |
|
931 |
have "distributed M (count_space (X ` space M)) X (\<lambda>x. ereal (if x \<in> X`space M then P x else 0))" |
|
932 |
(is "?A") |
|
933 |
using simple_functionD[OF X(1)] by (intro distributed_simple_function_superset[OF X]) auto |
|
934 |
also have "?A \<longleftrightarrow> distributed M (count_space (X ` space M)) X (\<lambda>x. ereal (P x))" |
|
935 |
by (rule distributed_cong_density) auto |
|
936 |
finally show "\<dots>" . |
|
937 |
qed (rule simple_functionD[OF X(1)]) |
|
938 |
||
939 |
lemma simple_distributed_joint_finite: |
|
940 |
assumes X: "simple_distributed M (\<lambda>x. (X x, Y x)) Px" |
|
941 |
shows "finite (X ` space M)" "finite (Y ` space M)" |
|
42902 | 942 |
proof - |
47694 | 943 |
have "finite ((\<lambda>x. (X x, Y x)) ` space M)" |
944 |
using X by (auto simp: simple_distributed_def simple_functionD) |
|
945 |
then have "finite (fst ` (\<lambda>x. (X x, Y x)) ` space M)" "finite (snd ` (\<lambda>x. (X x, Y x)) ` space M)" |
|
946 |
by auto |
|
947 |
then show fin: "finite (X ` space M)" "finite (Y ` space M)" |
|
948 |
by (auto simp: image_image) |
|
949 |
qed |
|
950 |
||
951 |
lemma simple_distributed_joint2_finite: |
|
952 |
assumes X: "simple_distributed M (\<lambda>x. (X x, Y x, Z x)) Px" |
|
953 |
shows "finite (X ` space M)" "finite (Y ` space M)" "finite (Z ` space M)" |
|
954 |
proof - |
|
955 |
have "finite ((\<lambda>x. (X x, Y x, Z x)) ` space M)" |
|
956 |
using X by (auto simp: simple_distributed_def simple_functionD) |
|
957 |
then have "finite (fst ` (\<lambda>x. (X x, Y x, Z x)) ` space M)" |
|
958 |
"finite ((fst \<circ> snd) ` (\<lambda>x. (X x, Y x, Z x)) ` space M)" |
|
959 |
"finite ((snd \<circ> snd) ` (\<lambda>x. (X x, Y x, Z x)) ` space M)" |
|
960 |
by auto |
|
961 |
then show fin: "finite (X ` space M)" "finite (Y ` space M)" "finite (Z ` space M)" |
|
962 |
by (auto simp: image_image) |
|
42902 | 963 |
qed |
964 |
||
47694 | 965 |
lemma simple_distributed_simple_function: |
966 |
"simple_distributed M X Px \<Longrightarrow> simple_function M X" |
|
967 |
unfolding simple_distributed_def distributed_def |
|
50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset
|
968 |
by (auto simp: simple_function_def measurable_count_space_eq2) |
47694 | 969 |
|
970 |
lemma simple_distributed_measure: |
|
971 |
"simple_distributed M X P \<Longrightarrow> a \<in> X`space M \<Longrightarrow> P a = measure M (X -` {a} \<inter> space M)" |
|
972 |
using distributed_count_space[of M "X`space M" X P a, symmetric] |
|
973 |
by (auto simp: simple_distributed_def measure_def) |
|
974 |
||
975 |
lemma simple_distributed_nonneg: "simple_distributed M X f \<Longrightarrow> x \<in> space M \<Longrightarrow> 0 \<le> f (X x)" |
|
976 |
by (auto simp: simple_distributed_measure measure_nonneg) |
|
42860 | 977 |
|
47694 | 978 |
lemma (in prob_space) simple_distributed_joint: |
979 |
assumes X: "simple_distributed M (\<lambda>x. (X x, Y x)) Px" |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
980 |
defines "S \<equiv> count_space (X`space M) \<Otimes>\<^sub>M count_space (Y`space M)" |
47694 | 981 |
defines "P \<equiv> (\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x))`space M then Px x else 0)" |
982 |
shows "distributed M S (\<lambda>x. (X x, Y x)) P" |
|
983 |
proof - |
|
984 |
from simple_distributed_joint_finite[OF X, simp] |
|
985 |
have S_eq: "S = count_space (X`space M \<times> Y`space M)" |
|
986 |
by (simp add: S_def pair_measure_count_space) |
|
987 |
show ?thesis |
|
988 |
unfolding S_eq P_def |
|
989 |
proof (rule distributed_simple_function_superset) |
|
990 |
show "simple_function M (\<lambda>x. (X x, Y x))" |
|
991 |
using X by (rule simple_distributed_simple_function) |
|
992 |
fix x assume "x \<in> (\<lambda>x. (X x, Y x)) ` space M" |
|
993 |
from simple_distributed_measure[OF X this] |
|
994 |
show "Px x = prob ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M)" . |
|
995 |
qed auto |
|
996 |
qed |
|
42860 | 997 |
|
47694 | 998 |
lemma (in prob_space) simple_distributed_joint2: |
999 |
assumes X: "simple_distributed M (\<lambda>x. (X x, Y x, Z x)) Px" |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
1000 |
defines "S \<equiv> count_space (X`space M) \<Otimes>\<^sub>M count_space (Y`space M) \<Otimes>\<^sub>M count_space (Z`space M)" |
47694 | 1001 |
defines "P \<equiv> (\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x, Z x))`space M then Px x else 0)" |
1002 |
shows "distributed M S (\<lambda>x. (X x, Y x, Z x)) P" |
|
1003 |
proof - |
|
1004 |
from simple_distributed_joint2_finite[OF X, simp] |
|
1005 |
have S_eq: "S = count_space (X`space M \<times> Y`space M \<times> Z`space M)" |
|
1006 |
by (simp add: S_def pair_measure_count_space) |
|
1007 |
show ?thesis |
|
1008 |
unfolding S_eq P_def |
|
1009 |
proof (rule distributed_simple_function_superset) |
|
1010 |
show "simple_function M (\<lambda>x. (X x, Y x, Z x))" |
|
1011 |
using X by (rule simple_distributed_simple_function) |
|
1012 |
fix x assume "x \<in> (\<lambda>x. (X x, Y x, Z x)) ` space M" |
|
1013 |
from simple_distributed_measure[OF X this] |
|
1014 |
show "Px x = prob ((\<lambda>x. (X x, Y x, Z x)) -` {x} \<inter> space M)" . |
|
1015 |
qed auto |
|
1016 |
qed |
|
1017 |
||
1018 |
lemma (in prob_space) simple_distributed_setsum_space: |
|
1019 |
assumes X: "simple_distributed M X f" |
|
1020 |
shows "setsum f (X`space M) = 1" |
|
1021 |
proof - |
|
1022 |
from X have "setsum f (X`space M) = prob (\<Union>i\<in>X`space M. X -` {i} \<inter> space M)" |
|
1023 |
by (subst finite_measure_finite_Union) |
|
1024 |
(auto simp add: disjoint_family_on_def simple_distributed_measure simple_distributed_simple_function simple_functionD |
|
57418 | 1025 |
intro!: setsum.cong arg_cong[where f="prob"]) |
47694 | 1026 |
also have "\<dots> = prob (space M)" |
1027 |
by (auto intro!: arg_cong[where f=prob]) |
|
1028 |
finally show ?thesis |
|
1029 |
using emeasure_space_1 by (simp add: emeasure_eq_measure one_ereal_def) |
|
1030 |
qed |
|
42860 | 1031 |
|
47694 | 1032 |
lemma (in prob_space) distributed_marginal_eq_joint_simple: |
1033 |
assumes Px: "simple_function M X" |
|
1034 |
assumes Py: "simple_distributed M Y Py" |
|
1035 |
assumes Pxy: "simple_distributed M (\<lambda>x. (X x, Y x)) Pxy" |
|
1036 |
assumes y: "y \<in> Y`space M" |
|
1037 |
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)" |
|
1038 |
proof - |
|
1039 |
note Px = simple_distributedI[OF Px refl] |
|
1040 |
have *: "\<And>f A. setsum (\<lambda>x. max 0 (ereal (f x))) A = ereal (setsum (\<lambda>x. max 0 (f x)) A)" |
|
1041 |
by (simp add: setsum_ereal[symmetric] zero_ereal_def) |
|
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
1042 |
from distributed_marginal_eq_joint2[OF |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
1043 |
sigma_finite_measure_count_space_finite |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
1044 |
sigma_finite_measure_count_space_finite |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
1045 |
simple_distributed[OF Py] simple_distributed_joint[OF Pxy], |
47694 | 1046 |
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
|
1047 |
y |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
1048 |
Px[THEN simple_distributed_finite] |
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset
|
1049 |
Py[THEN simple_distributed_finite] |
47694 | 1050 |
Pxy[THEN simple_distributed, THEN distributed_real_AE] |
1051 |
show ?thesis |
|
1052 |
unfolding AE_count_space |
|
57418 | 1053 |
apply (auto simp add: nn_integral_count_space_finite * intro!: setsum.cong split: split_max) |
47694 | 1054 |
done |
1055 |
qed |
|
42860 | 1056 |
|
50419 | 1057 |
lemma distributedI_real: |
1058 |
fixes f :: "'a \<Rightarrow> real" |
|
1059 |
assumes gen: "sets M1 = sigma_sets (space M1) E" and "Int_stable E" |
|
1060 |
and A: "range A \<subseteq> E" "(\<Union>i::nat. A i) = space M1" "\<And>i. emeasure (distr M M1 X) (A i) \<noteq> \<infinity>" |
|
1061 |
and X: "X \<in> measurable M M1" |
|
1062 |
and f: "f \<in> borel_measurable M1" "AE x in M1. 0 \<le> f x" |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
1063 |
and eq: "\<And>A. A \<in> E \<Longrightarrow> emeasure M (X -` A \<inter> space M) = (\<integral>\<^sup>+ x. f x * indicator A x \<partial>M1)" |
50419 | 1064 |
shows "distributed M M1 X f" |
1065 |
unfolding distributed_def |
|
1066 |
proof (intro conjI) |
|
1067 |
show "distr M M1 X = density M1 f" |
|
1068 |
proof (rule measure_eqI_generator_eq[where A=A]) |
|
1069 |
{ fix A assume A: "A \<in> E" |
|
1070 |
then have "A \<in> sigma_sets (space M1) E" by auto |
|
1071 |
then have "A \<in> sets M1" |
|
1072 |
using gen by simp |
|
1073 |
with f A eq[of A] X show "emeasure (distr M M1 X) A = emeasure (density M1 f) A" |
|
1074 |
by (simp add: emeasure_distr emeasure_density borel_measurable_ereal |
|
1075 |
times_ereal.simps[symmetric] ereal_indicator |
|
1076 |
del: times_ereal.simps) } |
|
1077 |
note eq_E = this |
|
1078 |
show "Int_stable E" by fact |
|
1079 |
{ fix e assume "e \<in> E" |
|
1080 |
then have "e \<in> sigma_sets (space M1) E" by auto |
|
1081 |
then have "e \<in> sets M1" unfolding gen . |
|
1082 |
then have "e \<subseteq> space M1" by (rule sets.sets_into_space) } |
|
1083 |
then show "E \<subseteq> Pow (space M1)" by auto |
|
1084 |
show "sets (distr M M1 X) = sigma_sets (space M1) E" |
|
1085 |
"sets (density M1 (\<lambda>x. ereal (f x))) = sigma_sets (space M1) E" |
|
1086 |
unfolding gen[symmetric] by auto |
|
1087 |
qed fact+ |
|
1088 |
qed (insert X f, auto) |
|
1089 |
||
1090 |
lemma distributedI_borel_atMost: |
|
1091 |
fixes f :: "real \<Rightarrow> real" |
|
1092 |
assumes [measurable]: "X \<in> borel_measurable M" |
|
1093 |
and [measurable]: "f \<in> borel_measurable borel" and f[simp]: "AE x in lborel. 0 \<le> f x" |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
1094 |
and g_eq: "\<And>a. (\<integral>\<^sup>+x. f x * indicator {..a} x \<partial>lborel) = ereal (g a)" |
50419 | 1095 |
and M_eq: "\<And>a. emeasure M {x\<in>space M. X x \<le> a} = ereal (g a)" |
1096 |
shows "distributed M lborel X f" |
|
1097 |
proof (rule distributedI_real) |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
1098 |
show "sets (lborel::real measure) = sigma_sets (space lborel) (range atMost)" |
50419 | 1099 |
by (simp add: borel_eq_atMost) |
1100 |
show "Int_stable (range atMost :: real set set)" |
|
1101 |
by (auto simp: Int_stable_def) |
|
1102 |
have vimage_eq: "\<And>a. (X -` {..a} \<inter> space M) = {x\<in>space M. X x \<le> a}" by auto |
|
1103 |
def A \<equiv> "\<lambda>i::nat. {.. real i}" |
|
1104 |
then show "range A \<subseteq> range atMost" "(\<Union>i. A i) = space lborel" |
|
1105 |
"\<And>i. emeasure (distr M lborel X) (A i) \<noteq> \<infinity>" |
|
1106 |
by (auto simp: real_arch_simple emeasure_distr vimage_eq M_eq) |
|
1107 |
||
1108 |
fix A :: "real set" assume "A \<in> range atMost" |
|
1109 |
then obtain a where A: "A = {..a}" by auto |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51683
diff
changeset
|
1110 |
show "emeasure M (X -` A \<inter> space M) = (\<integral>\<^sup>+x. f x * indicator A x \<partial>lborel)" |
50419 | 1111 |
unfolding vimage_eq A M_eq g_eq .. |
1112 |
qed auto |
|
1113 |
||
1114 |
lemma (in prob_space) uniform_distributed_params: |
|
1115 |
assumes X: "distributed M MX X (\<lambda>x. indicator A x / measure MX A)" |
|
1116 |
shows "A \<in> sets MX" "measure MX A \<noteq> 0" |
|
1117 |
proof - |
|
1118 |
interpret X: prob_space "distr M MX X" |
|
1119 |
using distributed_measurable[OF X] by (rule prob_space_distr) |
|
1120 |
||
1121 |
show "measure MX A \<noteq> 0" |
|
1122 |
proof |
|
1123 |
assume "measure MX A = 0" |
|
1124 |
with X.emeasure_space_1 X.prob_space distributed_distr_eq_density[OF X] |
|
1125 |
show False |
|
1126 |
by (simp add: emeasure_density zero_ereal_def[symmetric]) |
|
1127 |
qed |
|
1128 |
with measure_notin_sets[of A MX] show "A \<in> sets MX" |
|
1129 |
by blast |
|
1130 |
qed |
|
1131 |
||
47694 | 1132 |
lemma prob_space_uniform_measure: |
1133 |
assumes A: "emeasure M A \<noteq> 0" "emeasure M A \<noteq> \<infinity>" |
|
1134 |
shows "prob_space (uniform_measure M A)" |
|
1135 |
proof |
|
1136 |
show "emeasure (uniform_measure M A) (space (uniform_measure M A)) = 1" |
|
1137 |
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
|
1138 |
using sets.sets_into_space[OF emeasure_neq_0_sets[OF A(1)]] A |
47694 | 1139 |
by (simp add: Int_absorb2 emeasure_nonneg) |
1140 |
qed |
|
1141 |
||
1142 |
lemma prob_space_uniform_count_measure: "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> prob_space (uniform_count_measure A)" |
|
1143 |
by default (auto simp: emeasure_uniform_count_measure space_uniform_count_measure one_ereal_def) |
|
42860 | 1144 |
|
59000 | 1145 |
lemma (in prob_space) measure_uniform_measure_eq_cond_prob: |
1146 |
assumes [measurable]: "Measurable.pred M P" "Measurable.pred M Q" |
|
1147 |
shows "\<P>(x in uniform_measure M {x\<in>space M. Q x}. P x) = \<P>(x in M. P x \<bar> Q x)" |
|
1148 |
proof cases |
|
1149 |
assume Q: "measure M {x\<in>space M. Q x} = 0" |
|
1150 |
then have "AE x in M. \<not> Q x" |
|
1151 |
by (simp add: prob_eq_0) |
|
1152 |
then have "AE x in M. indicator {x\<in>space M. Q x} x / ereal 0 = 0" |
|
1153 |
by (auto split: split_indicator) |
|
1154 |
from density_cong[OF _ _ this] show ?thesis |
|
1155 |
by (simp add: uniform_measure_def emeasure_eq_measure cond_prob_def Q measure_density_const) |
|
1156 |
qed (auto simp add: emeasure_eq_measure cond_prob_def intro!: arg_cong[where f=prob]) |
|
1157 |
||
1158 |
lemma prob_space_point_measure: |
|
1159 |
"finite S \<Longrightarrow> (\<And>s. s \<in> S \<Longrightarrow> 0 \<le> p s) \<Longrightarrow> (\<Sum>s\<in>S. p s) = 1 \<Longrightarrow> prob_space (point_measure S p)" |
|
1160 |
by (rule prob_spaceI) (simp add: space_point_measure emeasure_point_measure_finite) |
|
1161 |
||
35582 | 1162 |
end |