50530
|
1 |
(* Title: HOL/Probability/Measurable.thy
|
50387
|
2 |
Author: Johannes Hölzl <hoelzl@in.tum.de>
|
|
3 |
*)
|
|
4 |
theory Measurable
|
|
5 |
imports Sigma_Algebra
|
|
6 |
begin
|
|
7 |
|
|
8 |
subsection {* Measurability prover *}
|
|
9 |
|
|
10 |
lemma (in algebra) sets_Collect_finite_All:
|
|
11 |
assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S"
|
|
12 |
shows "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} \<in> M"
|
|
13 |
proof -
|
|
14 |
have "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} = (if S = {} then \<Omega> else \<Inter>i\<in>S. {x\<in>\<Omega>. P i x})"
|
|
15 |
by auto
|
|
16 |
with assms show ?thesis by (auto intro!: sets_Collect_finite_All')
|
|
17 |
qed
|
|
18 |
|
|
19 |
abbreviation "pred M P \<equiv> P \<in> measurable M (count_space (UNIV::bool set))"
|
|
20 |
|
|
21 |
lemma pred_def: "pred M P \<longleftrightarrow> {x\<in>space M. P x} \<in> sets M"
|
|
22 |
proof
|
|
23 |
assume "pred M P"
|
|
24 |
then have "P -` {True} \<inter> space M \<in> sets M"
|
|
25 |
by (auto simp: measurable_count_space_eq2)
|
|
26 |
also have "P -` {True} \<inter> space M = {x\<in>space M. P x}" by auto
|
|
27 |
finally show "{x\<in>space M. P x} \<in> sets M" .
|
|
28 |
next
|
|
29 |
assume P: "{x\<in>space M. P x} \<in> sets M"
|
|
30 |
moreover
|
|
31 |
{ fix X
|
|
32 |
have "X \<in> Pow (UNIV :: bool set)" by simp
|
|
33 |
then have "P -` X \<inter> space M = {x\<in>space M. ((X = {True} \<longrightarrow> P x) \<and> (X = {False} \<longrightarrow> \<not> P x) \<and> X \<noteq> {})}"
|
|
34 |
unfolding UNIV_bool Pow_insert Pow_empty by auto
|
|
35 |
then have "P -` X \<inter> space M \<in> sets M"
|
|
36 |
by (auto intro!: sets.sets_Collect_neg sets.sets_Collect_imp sets.sets_Collect_conj sets.sets_Collect_const P) }
|
|
37 |
then show "pred M P"
|
|
38 |
by (auto simp: measurable_def)
|
|
39 |
qed
|
|
40 |
|
|
41 |
lemma pred_sets1: "{x\<in>space M. P x} \<in> sets M \<Longrightarrow> f \<in> measurable N M \<Longrightarrow> pred N (\<lambda>x. P (f x))"
|
|
42 |
by (rule measurable_compose[where f=f and N=M]) (auto simp: pred_def)
|
|
43 |
|
|
44 |
lemma pred_sets2: "A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> pred M (\<lambda>x. f x \<in> A)"
|
|
45 |
by (rule measurable_compose[where f=f and N=N]) (auto simp: pred_def Int_def[symmetric])
|
|
46 |
|
|
47 |
ML_file "measurable.ML"
|
|
48 |
|
|
49 |
attribute_setup measurable = {* Measurable.attr *} "declaration of measurability theorems"
|
|
50 |
attribute_setup measurable_dest = {* Measurable.dest_attr *} "add dest rule for measurability prover"
|
|
51 |
attribute_setup measurable_app = {* Measurable.app_attr *} "add application rule for measurability prover"
|
|
52 |
method_setup measurable = {* Measurable.method *} "measurability prover"
|
|
53 |
simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = {* K Measurable.simproc *}
|
|
54 |
|
|
55 |
declare
|
|
56 |
measurable_compose_rev[measurable_dest]
|
|
57 |
pred_sets1[measurable_dest]
|
|
58 |
pred_sets2[measurable_dest]
|
|
59 |
sets.sets_into_space[measurable_dest]
|
|
60 |
|
|
61 |
declare
|
|
62 |
sets.top[measurable]
|
|
63 |
sets.empty_sets[measurable (raw)]
|
|
64 |
sets.Un[measurable (raw)]
|
|
65 |
sets.Diff[measurable (raw)]
|
|
66 |
|
|
67 |
declare
|
|
68 |
measurable_count_space[measurable (raw)]
|
|
69 |
measurable_ident[measurable (raw)]
|
|
70 |
measurable_ident_sets[measurable (raw)]
|
|
71 |
measurable_const[measurable (raw)]
|
|
72 |
measurable_If[measurable (raw)]
|
|
73 |
measurable_comp[measurable (raw)]
|
|
74 |
measurable_sets[measurable (raw)]
|
|
75 |
|
|
76 |
lemma predE[measurable (raw)]:
|
|
77 |
"pred M P \<Longrightarrow> {x\<in>space M. P x} \<in> sets M"
|
|
78 |
unfolding pred_def .
|
|
79 |
|
|
80 |
lemma pred_intros_imp'[measurable (raw)]:
|
|
81 |
"(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<longrightarrow> P x)"
|
|
82 |
by (cases K) auto
|
|
83 |
|
|
84 |
lemma pred_intros_conj1'[measurable (raw)]:
|
|
85 |
"(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<and> P x)"
|
|
86 |
by (cases K) auto
|
|
87 |
|
|
88 |
lemma pred_intros_conj2'[measurable (raw)]:
|
|
89 |
"(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<and> K)"
|
|
90 |
by (cases K) auto
|
|
91 |
|
|
92 |
lemma pred_intros_disj1'[measurable (raw)]:
|
|
93 |
"(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<or> P x)"
|
|
94 |
by (cases K) auto
|
|
95 |
|
|
96 |
lemma pred_intros_disj2'[measurable (raw)]:
|
|
97 |
"(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<or> K)"
|
|
98 |
by (cases K) auto
|
|
99 |
|
|
100 |
lemma pred_intros_logic[measurable (raw)]:
|
|
101 |
"pred M (\<lambda>x. x \<in> space M)"
|
|
102 |
"pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. \<not> P x)"
|
|
103 |
"pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<and> P x)"
|
|
104 |
"pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<longrightarrow> P x)"
|
|
105 |
"pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<or> P x)"
|
|
106 |
"pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x = P x)"
|
|
107 |
"pred M (\<lambda>x. f x \<in> UNIV)"
|
|
108 |
"pred M (\<lambda>x. f x \<in> {})"
|
|
109 |
"pred M (\<lambda>x. P' (f x) x) \<Longrightarrow> pred M (\<lambda>x. f x \<in> {y. P' y x})"
|
|
110 |
"pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> - (B x))"
|
|
111 |
"pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) - (B x))"
|
|
112 |
"pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) \<inter> (B x))"
|
|
113 |
"pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) \<union> (B x))"
|
|
114 |
"pred M (\<lambda>x. g x (f x) \<in> (X x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (g x) -` (X x))"
|
|
115 |
by (auto simp: iff_conv_conj_imp pred_def)
|
|
116 |
|
|
117 |
lemma pred_intros_countable[measurable (raw)]:
|
|
118 |
fixes P :: "'a \<Rightarrow> 'i :: countable \<Rightarrow> bool"
|
|
119 |
shows
|
|
120 |
"(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i. P x i)"
|
|
121 |
"(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i. P x i)"
|
|
122 |
by (auto intro!: sets.sets_Collect_countable_All sets.sets_Collect_countable_Ex simp: pred_def)
|
|
123 |
|
|
124 |
lemma pred_intros_countable_bounded[measurable (raw)]:
|
|
125 |
fixes X :: "'i :: countable set"
|
|
126 |
shows
|
|
127 |
"(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Inter>i\<in>X. N x i))"
|
|
128 |
"(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Union>i\<in>X. N x i))"
|
|
129 |
"(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i\<in>X. P x i)"
|
|
130 |
"(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i\<in>X. P x i)"
|
|
131 |
by (auto simp: Bex_def Ball_def)
|
|
132 |
|
|
133 |
lemma pred_intros_finite[measurable (raw)]:
|
|
134 |
"finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Inter>i\<in>I. N x i))"
|
|
135 |
"finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Union>i\<in>I. N x i))"
|
|
136 |
"finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i\<in>I. P x i)"
|
|
137 |
"finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i\<in>I. P x i)"
|
|
138 |
by (auto intro!: sets.sets_Collect_finite_Ex sets.sets_Collect_finite_All simp: iff_conv_conj_imp pred_def)
|
|
139 |
|
|
140 |
lemma countable_Un_Int[measurable (raw)]:
|
|
141 |
"(\<And>i :: 'i :: countable. i \<in> I \<Longrightarrow> N i \<in> sets M) \<Longrightarrow> (\<Union>i\<in>I. N i) \<in> sets M"
|
|
142 |
"I \<noteq> {} \<Longrightarrow> (\<And>i :: 'i :: countable. i \<in> I \<Longrightarrow> N i \<in> sets M) \<Longrightarrow> (\<Inter>i\<in>I. N i) \<in> sets M"
|
|
143 |
by auto
|
|
144 |
|
|
145 |
declare
|
|
146 |
finite_UN[measurable (raw)]
|
|
147 |
finite_INT[measurable (raw)]
|
|
148 |
|
|
149 |
lemma sets_Int_pred[measurable (raw)]:
|
|
150 |
assumes space: "A \<inter> B \<subseteq> space M" and [measurable]: "pred M (\<lambda>x. x \<in> A)" "pred M (\<lambda>x. x \<in> B)"
|
|
151 |
shows "A \<inter> B \<in> sets M"
|
|
152 |
proof -
|
|
153 |
have "{x\<in>space M. x \<in> A \<inter> B} \<in> sets M" by auto
|
|
154 |
also have "{x\<in>space M. x \<in> A \<inter> B} = A \<inter> B"
|
|
155 |
using space by auto
|
|
156 |
finally show ?thesis .
|
|
157 |
qed
|
|
158 |
|
|
159 |
lemma [measurable (raw generic)]:
|
|
160 |
assumes f: "f \<in> measurable M N" and c: "c \<in> space N \<Longrightarrow> {c} \<in> sets N"
|
|
161 |
shows pred_eq_const1: "pred M (\<lambda>x. f x = c)"
|
|
162 |
and pred_eq_const2: "pred M (\<lambda>x. c = f x)"
|
|
163 |
proof -
|
|
164 |
show "pred M (\<lambda>x. f x = c)"
|
|
165 |
proof cases
|
|
166 |
assume "c \<in> space N"
|
|
167 |
with measurable_sets[OF f c] show ?thesis
|
|
168 |
by (auto simp: Int_def conj_commute pred_def)
|
|
169 |
next
|
|
170 |
assume "c \<notin> space N"
|
|
171 |
with f[THEN measurable_space] have "{x \<in> space M. f x = c} = {}" by auto
|
|
172 |
then show ?thesis by (auto simp: pred_def cong: conj_cong)
|
|
173 |
qed
|
|
174 |
then show "pred M (\<lambda>x. c = f x)"
|
|
175 |
by (simp add: eq_commute)
|
|
176 |
qed
|
|
177 |
|
|
178 |
lemma pred_le_const[measurable (raw generic)]:
|
|
179 |
assumes f: "f \<in> measurable M N" and c: "{.. c} \<in> sets N" shows "pred M (\<lambda>x. f x \<le> c)"
|
|
180 |
using measurable_sets[OF f c]
|
|
181 |
by (auto simp: Int_def conj_commute eq_commute pred_def)
|
|
182 |
|
|
183 |
lemma pred_const_le[measurable (raw generic)]:
|
|
184 |
assumes f: "f \<in> measurable M N" and c: "{c ..} \<in> sets N" shows "pred M (\<lambda>x. c \<le> f x)"
|
|
185 |
using measurable_sets[OF f c]
|
|
186 |
by (auto simp: Int_def conj_commute eq_commute pred_def)
|
|
187 |
|
|
188 |
lemma pred_less_const[measurable (raw generic)]:
|
|
189 |
assumes f: "f \<in> measurable M N" and c: "{..< c} \<in> sets N" shows "pred M (\<lambda>x. f x < c)"
|
|
190 |
using measurable_sets[OF f c]
|
|
191 |
by (auto simp: Int_def conj_commute eq_commute pred_def)
|
|
192 |
|
|
193 |
lemma pred_const_less[measurable (raw generic)]:
|
|
194 |
assumes f: "f \<in> measurable M N" and c: "{c <..} \<in> sets N" shows "pred M (\<lambda>x. c < f x)"
|
|
195 |
using measurable_sets[OF f c]
|
|
196 |
by (auto simp: Int_def conj_commute eq_commute pred_def)
|
|
197 |
|
|
198 |
declare
|
|
199 |
sets.Int[measurable (raw)]
|
|
200 |
|
|
201 |
lemma pred_in_If[measurable (raw)]:
|
|
202 |
"(P \<Longrightarrow> pred M (\<lambda>x. x \<in> A x)) \<Longrightarrow> (\<not> P \<Longrightarrow> pred M (\<lambda>x. x \<in> B x)) \<Longrightarrow>
|
|
203 |
pred M (\<lambda>x. x \<in> (if P then A x else B x))"
|
|
204 |
by auto
|
|
205 |
|
|
206 |
lemma sets_range[measurable_dest]:
|
|
207 |
"A ` I \<subseteq> sets M \<Longrightarrow> i \<in> I \<Longrightarrow> A i \<in> sets M"
|
|
208 |
by auto
|
|
209 |
|
|
210 |
lemma pred_sets_range[measurable_dest]:
|
|
211 |
"A ` I \<subseteq> sets N \<Longrightarrow> i \<in> I \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> pred M (\<lambda>x. f x \<in> A i)"
|
|
212 |
using pred_sets2[OF sets_range] by auto
|
|
213 |
|
|
214 |
lemma sets_All[measurable_dest]:
|
|
215 |
"\<forall>i. A i \<in> sets (M i) \<Longrightarrow> A i \<in> sets (M i)"
|
|
216 |
by auto
|
|
217 |
|
|
218 |
lemma pred_sets_All[measurable_dest]:
|
|
219 |
"\<forall>i. A i \<in> sets (N i) \<Longrightarrow> f \<in> measurable M (N i) \<Longrightarrow> pred M (\<lambda>x. f x \<in> A i)"
|
|
220 |
using pred_sets2[OF sets_All, of A N f] by auto
|
|
221 |
|
|
222 |
lemma sets_Ball[measurable_dest]:
|
|
223 |
"\<forall>i\<in>I. A i \<in> sets (M i) \<Longrightarrow> i\<in>I \<Longrightarrow> A i \<in> sets (M i)"
|
|
224 |
by auto
|
|
225 |
|
|
226 |
lemma pred_sets_Ball[measurable_dest]:
|
|
227 |
"\<forall>i\<in>I. A i \<in> sets (N i) \<Longrightarrow> i\<in>I \<Longrightarrow> f \<in> measurable M (N i) \<Longrightarrow> pred M (\<lambda>x. f x \<in> A i)"
|
|
228 |
using pred_sets2[OF sets_Ball, of _ _ _ f] by auto
|
|
229 |
|
|
230 |
lemma measurable_finite[measurable (raw)]:
|
|
231 |
fixes S :: "'a \<Rightarrow> nat set"
|
|
232 |
assumes [measurable]: "\<And>i. {x\<in>space M. i \<in> S x} \<in> sets M"
|
|
233 |
shows "pred M (\<lambda>x. finite (S x))"
|
|
234 |
unfolding finite_nat_set_iff_bounded by (simp add: Ball_def)
|
|
235 |
|
|
236 |
lemma measurable_Least[measurable]:
|
|
237 |
assumes [measurable]: "(\<And>i::nat. (\<lambda>x. P i x) \<in> measurable M (count_space UNIV))"q
|
|
238 |
shows "(\<lambda>x. LEAST i. P i x) \<in> measurable M (count_space UNIV)"
|
|
239 |
unfolding measurable_def by (safe intro!: sets_Least) simp_all
|
|
240 |
|
|
241 |
lemma measurable_count_space_insert[measurable (raw)]:
|
|
242 |
"s \<in> S \<Longrightarrow> A \<in> sets (count_space S) \<Longrightarrow> insert s A \<in> sets (count_space S)"
|
|
243 |
by simp
|
|
244 |
|
|
245 |
hide_const (open) pred
|
|
246 |
|
|
247 |
end
|