author | hoelzl |
Tue, 13 Jan 2015 19:10:36 +0100 | |
changeset 59353 | f0707dc3d9aa |
parent 59088 | ff2bd4a14ddb |
child 59361 | fd5da2434be4 |
permissions | -rw-r--r-- |
50530 | 1 |
(* Title: HOL/Probability/Measurable.thy |
50387 | 2 |
Author: Johannes Hölzl <hoelzl@in.tum.de> |
3 |
*) |
|
4 |
theory Measurable |
|
56021
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
5 |
imports |
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
6 |
Sigma_Algebra |
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
7 |
"~~/src/HOL/Library/Order_Continuity" |
50387 | 8 |
begin |
9 |
||
56021
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
10 |
hide_const (open) Order_Continuity.continuous |
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
11 |
|
50387 | 12 |
subsection {* Measurability prover *} |
13 |
||
14 |
lemma (in algebra) sets_Collect_finite_All: |
|
15 |
assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S" |
|
16 |
shows "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} \<in> M" |
|
17 |
proof - |
|
18 |
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})" |
|
19 |
by auto |
|
20 |
with assms show ?thesis by (auto intro!: sets_Collect_finite_All') |
|
21 |
qed |
|
22 |
||
23 |
abbreviation "pred M P \<equiv> P \<in> measurable M (count_space (UNIV::bool set))" |
|
24 |
||
25 |
lemma pred_def: "pred M P \<longleftrightarrow> {x\<in>space M. P x} \<in> sets M" |
|
26 |
proof |
|
27 |
assume "pred M P" |
|
28 |
then have "P -` {True} \<inter> space M \<in> sets M" |
|
29 |
by (auto simp: measurable_count_space_eq2) |
|
30 |
also have "P -` {True} \<inter> space M = {x\<in>space M. P x}" by auto |
|
31 |
finally show "{x\<in>space M. P x} \<in> sets M" . |
|
32 |
next |
|
33 |
assume P: "{x\<in>space M. P x} \<in> sets M" |
|
34 |
moreover |
|
35 |
{ fix X |
|
36 |
have "X \<in> Pow (UNIV :: bool set)" by simp |
|
37 |
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> {})}" |
|
38 |
unfolding UNIV_bool Pow_insert Pow_empty by auto |
|
39 |
then have "P -` X \<inter> space M \<in> sets M" |
|
40 |
by (auto intro!: sets.sets_Collect_neg sets.sets_Collect_imp sets.sets_Collect_conj sets.sets_Collect_const P) } |
|
41 |
then show "pred M P" |
|
42 |
by (auto simp: measurable_def) |
|
43 |
qed |
|
44 |
||
45 |
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))" |
|
46 |
by (rule measurable_compose[where f=f and N=M]) (auto simp: pred_def) |
|
47 |
||
48 |
lemma pred_sets2: "A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> pred M (\<lambda>x. f x \<in> A)" |
|
49 |
by (rule measurable_compose[where f=f and N=N]) (auto simp: pred_def Int_def[symmetric]) |
|
50 |
||
51 |
ML_file "measurable.ML" |
|
52 |
||
53043
8cbfbeb566a4
more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset
|
53 |
attribute_setup measurable = {* |
59047 | 54 |
Scan.lift ( |
55 |
(Args.add >> K true || Args.del >> K false || Scan.succeed true) -- |
|
56 |
Scan.optional (Args.parens ( |
|
57 |
Scan.optional (Args.$$$ "raw" >> K true) false -- |
|
58965 | 58 |
Scan.optional (Args.$$$ "generic" >> K Measurable.Generic) Measurable.Concrete)) |
59047 | 59 |
(false, Measurable.Concrete) >> |
60 |
Measurable.measurable_thm_attr) |
|
53043
8cbfbeb566a4
more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset
|
61 |
*} "declaration of measurability theorems" |
8cbfbeb566a4
more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset
|
62 |
|
59047 | 63 |
attribute_setup measurable_dest = Measurable.dest_thm_attr |
59048 | 64 |
"add dest rule to measurability prover" |
53043
8cbfbeb566a4
more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset
|
65 |
|
59048 | 66 |
attribute_setup measurable_cong = Measurable.cong_thm_attr |
67 |
"add congurence rules to measurability prover" |
|
53043
8cbfbeb566a4
more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset
|
68 |
|
59047 | 69 |
method_setup measurable = \<open> Scan.lift (Scan.succeed (METHOD o Measurable.measurable_tac)) \<close> |
70 |
"measurability prover" |
|
53043
8cbfbeb566a4
more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset
|
71 |
|
50387 | 72 |
simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = {* K Measurable.simproc *} |
73 |
||
58965 | 74 |
setup {* |
59048 | 75 |
Global_Theory.add_thms_dynamic (@{binding measurable}, Measurable.get_all) |
58965 | 76 |
*} |
59353
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59088
diff
changeset
|
77 |
|
50387 | 78 |
declare |
79 |
pred_sets1[measurable_dest] |
|
80 |
pred_sets2[measurable_dest] |
|
81 |
sets.sets_into_space[measurable_dest] |
|
82 |
||
83 |
declare |
|
84 |
sets.top[measurable] |
|
85 |
sets.empty_sets[measurable (raw)] |
|
86 |
sets.Un[measurable (raw)] |
|
87 |
sets.Diff[measurable (raw)] |
|
88 |
||
89 |
declare |
|
90 |
measurable_count_space[measurable (raw)] |
|
91 |
measurable_ident[measurable (raw)] |
|
59048 | 92 |
measurable_id[measurable (raw)] |
50387 | 93 |
measurable_const[measurable (raw)] |
94 |
measurable_If[measurable (raw)] |
|
95 |
measurable_comp[measurable (raw)] |
|
96 |
measurable_sets[measurable (raw)] |
|
97 |
||
59048 | 98 |
declare measurable_cong_sets[measurable_cong] |
99 |
declare sets_restrict_space_cong[measurable_cong] |
|
100 |
||
50387 | 101 |
lemma predE[measurable (raw)]: |
102 |
"pred M P \<Longrightarrow> {x\<in>space M. P x} \<in> sets M" |
|
103 |
unfolding pred_def . |
|
104 |
||
105 |
lemma pred_intros_imp'[measurable (raw)]: |
|
106 |
"(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<longrightarrow> P x)" |
|
107 |
by (cases K) auto |
|
108 |
||
109 |
lemma pred_intros_conj1'[measurable (raw)]: |
|
110 |
"(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<and> P x)" |
|
111 |
by (cases K) auto |
|
112 |
||
113 |
lemma pred_intros_conj2'[measurable (raw)]: |
|
114 |
"(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<and> K)" |
|
115 |
by (cases K) auto |
|
116 |
||
117 |
lemma pred_intros_disj1'[measurable (raw)]: |
|
118 |
"(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<or> P x)" |
|
119 |
by (cases K) auto |
|
120 |
||
121 |
lemma pred_intros_disj2'[measurable (raw)]: |
|
122 |
"(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<or> K)" |
|
123 |
by (cases K) auto |
|
124 |
||
125 |
lemma pred_intros_logic[measurable (raw)]: |
|
126 |
"pred M (\<lambda>x. x \<in> space M)" |
|
127 |
"pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. \<not> P x)" |
|
128 |
"pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<and> P x)" |
|
129 |
"pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<longrightarrow> P x)" |
|
130 |
"pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<or> P x)" |
|
131 |
"pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x = P x)" |
|
132 |
"pred M (\<lambda>x. f x \<in> UNIV)" |
|
133 |
"pred M (\<lambda>x. f x \<in> {})" |
|
134 |
"pred M (\<lambda>x. P' (f x) x) \<Longrightarrow> pred M (\<lambda>x. f x \<in> {y. P' y x})" |
|
135 |
"pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> - (B x))" |
|
136 |
"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))" |
|
137 |
"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))" |
|
138 |
"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))" |
|
139 |
"pred M (\<lambda>x. g x (f x) \<in> (X x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (g x) -` (X x))" |
|
140 |
by (auto simp: iff_conv_conj_imp pred_def) |
|
141 |
||
142 |
lemma pred_intros_countable[measurable (raw)]: |
|
143 |
fixes P :: "'a \<Rightarrow> 'i :: countable \<Rightarrow> bool" |
|
144 |
shows |
|
145 |
"(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i. P x i)" |
|
146 |
"(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i. P x i)" |
|
147 |
by (auto intro!: sets.sets_Collect_countable_All sets.sets_Collect_countable_Ex simp: pred_def) |
|
148 |
||
149 |
lemma pred_intros_countable_bounded[measurable (raw)]: |
|
150 |
fixes X :: "'i :: countable set" |
|
151 |
shows |
|
152 |
"(\<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))" |
|
153 |
"(\<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))" |
|
154 |
"(\<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)" |
|
155 |
"(\<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)" |
|
156 |
by (auto simp: Bex_def Ball_def) |
|
157 |
||
158 |
lemma pred_intros_finite[measurable (raw)]: |
|
159 |
"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))" |
|
160 |
"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))" |
|
161 |
"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)" |
|
162 |
"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)" |
|
163 |
by (auto intro!: sets.sets_Collect_finite_Ex sets.sets_Collect_finite_All simp: iff_conv_conj_imp pred_def) |
|
164 |
||
165 |
lemma countable_Un_Int[measurable (raw)]: |
|
166 |
"(\<And>i :: 'i :: countable. i \<in> I \<Longrightarrow> N i \<in> sets M) \<Longrightarrow> (\<Union>i\<in>I. N i) \<in> sets M" |
|
167 |
"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" |
|
168 |
by auto |
|
169 |
||
170 |
declare |
|
171 |
finite_UN[measurable (raw)] |
|
172 |
finite_INT[measurable (raw)] |
|
173 |
||
174 |
lemma sets_Int_pred[measurable (raw)]: |
|
175 |
assumes space: "A \<inter> B \<subseteq> space M" and [measurable]: "pred M (\<lambda>x. x \<in> A)" "pred M (\<lambda>x. x \<in> B)" |
|
176 |
shows "A \<inter> B \<in> sets M" |
|
177 |
proof - |
|
178 |
have "{x\<in>space M. x \<in> A \<inter> B} \<in> sets M" by auto |
|
179 |
also have "{x\<in>space M. x \<in> A \<inter> B} = A \<inter> B" |
|
180 |
using space by auto |
|
181 |
finally show ?thesis . |
|
182 |
qed |
|
183 |
||
184 |
lemma [measurable (raw generic)]: |
|
185 |
assumes f: "f \<in> measurable M N" and c: "c \<in> space N \<Longrightarrow> {c} \<in> sets N" |
|
186 |
shows pred_eq_const1: "pred M (\<lambda>x. f x = c)" |
|
187 |
and pred_eq_const2: "pred M (\<lambda>x. c = f x)" |
|
188 |
proof - |
|
189 |
show "pred M (\<lambda>x. f x = c)" |
|
190 |
proof cases |
|
191 |
assume "c \<in> space N" |
|
192 |
with measurable_sets[OF f c] show ?thesis |
|
193 |
by (auto simp: Int_def conj_commute pred_def) |
|
194 |
next |
|
195 |
assume "c \<notin> space N" |
|
196 |
with f[THEN measurable_space] have "{x \<in> space M. f x = c} = {}" by auto |
|
197 |
then show ?thesis by (auto simp: pred_def cong: conj_cong) |
|
198 |
qed |
|
199 |
then show "pred M (\<lambda>x. c = f x)" |
|
200 |
by (simp add: eq_commute) |
|
201 |
qed |
|
202 |
||
59000 | 203 |
lemma pred_count_space_const1[measurable (raw)]: |
204 |
"f \<in> measurable M (count_space UNIV) \<Longrightarrow> Measurable.pred M (\<lambda>x. f x = c)" |
|
205 |
by (intro pred_eq_const1[where N="count_space UNIV"]) (auto ) |
|
206 |
||
207 |
lemma pred_count_space_const2[measurable (raw)]: |
|
208 |
"f \<in> measurable M (count_space UNIV) \<Longrightarrow> Measurable.pred M (\<lambda>x. c = f x)" |
|
209 |
by (intro pred_eq_const2[where N="count_space UNIV"]) (auto ) |
|
210 |
||
50387 | 211 |
lemma pred_le_const[measurable (raw generic)]: |
212 |
assumes f: "f \<in> measurable M N" and c: "{.. c} \<in> sets N" shows "pred M (\<lambda>x. f x \<le> c)" |
|
213 |
using measurable_sets[OF f c] |
|
214 |
by (auto simp: Int_def conj_commute eq_commute pred_def) |
|
215 |
||
216 |
lemma pred_const_le[measurable (raw generic)]: |
|
217 |
assumes f: "f \<in> measurable M N" and c: "{c ..} \<in> sets N" shows "pred M (\<lambda>x. c \<le> f x)" |
|
218 |
using measurable_sets[OF f c] |
|
219 |
by (auto simp: Int_def conj_commute eq_commute pred_def) |
|
220 |
||
221 |
lemma pred_less_const[measurable (raw generic)]: |
|
222 |
assumes f: "f \<in> measurable M N" and c: "{..< c} \<in> sets N" shows "pred M (\<lambda>x. f x < c)" |
|
223 |
using measurable_sets[OF f c] |
|
224 |
by (auto simp: Int_def conj_commute eq_commute pred_def) |
|
225 |
||
226 |
lemma pred_const_less[measurable (raw generic)]: |
|
227 |
assumes f: "f \<in> measurable M N" and c: "{c <..} \<in> sets N" shows "pred M (\<lambda>x. c < f x)" |
|
228 |
using measurable_sets[OF f c] |
|
229 |
by (auto simp: Int_def conj_commute eq_commute pred_def) |
|
230 |
||
231 |
declare |
|
232 |
sets.Int[measurable (raw)] |
|
233 |
||
234 |
lemma pred_in_If[measurable (raw)]: |
|
235 |
"(P \<Longrightarrow> pred M (\<lambda>x. x \<in> A x)) \<Longrightarrow> (\<not> P \<Longrightarrow> pred M (\<lambda>x. x \<in> B x)) \<Longrightarrow> |
|
236 |
pred M (\<lambda>x. x \<in> (if P then A x else B x))" |
|
237 |
by auto |
|
238 |
||
239 |
lemma sets_range[measurable_dest]: |
|
240 |
"A ` I \<subseteq> sets M \<Longrightarrow> i \<in> I \<Longrightarrow> A i \<in> sets M" |
|
241 |
by auto |
|
242 |
||
243 |
lemma pred_sets_range[measurable_dest]: |
|
244 |
"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)" |
|
245 |
using pred_sets2[OF sets_range] by auto |
|
246 |
||
247 |
lemma sets_All[measurable_dest]: |
|
248 |
"\<forall>i. A i \<in> sets (M i) \<Longrightarrow> A i \<in> sets (M i)" |
|
249 |
by auto |
|
250 |
||
251 |
lemma pred_sets_All[measurable_dest]: |
|
252 |
"\<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)" |
|
253 |
using pred_sets2[OF sets_All, of A N f] by auto |
|
254 |
||
255 |
lemma sets_Ball[measurable_dest]: |
|
256 |
"\<forall>i\<in>I. A i \<in> sets (M i) \<Longrightarrow> i\<in>I \<Longrightarrow> A i \<in> sets (M i)" |
|
257 |
by auto |
|
258 |
||
259 |
lemma pred_sets_Ball[measurable_dest]: |
|
260 |
"\<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)" |
|
261 |
using pred_sets2[OF sets_Ball, of _ _ _ f] by auto |
|
262 |
||
263 |
lemma measurable_finite[measurable (raw)]: |
|
264 |
fixes S :: "'a \<Rightarrow> nat set" |
|
265 |
assumes [measurable]: "\<And>i. {x\<in>space M. i \<in> S x} \<in> sets M" |
|
266 |
shows "pred M (\<lambda>x. finite (S x))" |
|
267 |
unfolding finite_nat_set_iff_bounded by (simp add: Ball_def) |
|
268 |
||
269 |
lemma measurable_Least[measurable]: |
|
270 |
assumes [measurable]: "(\<And>i::nat. (\<lambda>x. P i x) \<in> measurable M (count_space UNIV))"q |
|
271 |
shows "(\<lambda>x. LEAST i. P i x) \<in> measurable M (count_space UNIV)" |
|
272 |
unfolding measurable_def by (safe intro!: sets_Least) simp_all |
|
273 |
||
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
274 |
lemma measurable_Max_nat[measurable (raw)]: |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
275 |
fixes P :: "nat \<Rightarrow> 'a \<Rightarrow> bool" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
276 |
assumes [measurable]: "\<And>i. Measurable.pred M (P i)" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
277 |
shows "(\<lambda>x. Max {i. P i x}) \<in> measurable M (count_space UNIV)" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
278 |
unfolding measurable_count_space_eq2_countable |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
279 |
proof safe |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
280 |
fix n |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
281 |
|
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
282 |
{ fix x assume "\<forall>i. \<exists>n\<ge>i. P n x" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
283 |
then have "infinite {i. P i x}" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
284 |
unfolding infinite_nat_iff_unbounded_le by auto |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
285 |
then have "Max {i. P i x} = the None" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
286 |
by (rule Max.infinite) } |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
287 |
note 1 = this |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
288 |
|
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
289 |
{ fix x i j assume "P i x" "\<forall>n\<ge>j. \<not> P n x" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
290 |
then have "finite {i. P i x}" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
291 |
by (auto simp: subset_eq not_le[symmetric] finite_nat_iff_bounded) |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
292 |
with `P i x` have "P (Max {i. P i x}) x" "i \<le> Max {i. P i x}" "finite {i. P i x}" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
293 |
using Max_in[of "{i. P i x}"] by auto } |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
294 |
note 2 = this |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
295 |
|
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
296 |
have "(\<lambda>x. Max {i. P i x}) -` {n} \<inter> space M = {x\<in>space M. Max {i. P i x} = n}" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
297 |
by auto |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
298 |
also have "\<dots> = |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
299 |
{x\<in>space M. if (\<forall>i. \<exists>n\<ge>i. P n x) then the None = n else |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
300 |
if (\<exists>i. P i x) then P n x \<and> (\<forall>i>n. \<not> P i x) |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
301 |
else Max {} = n}" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
302 |
by (intro arg_cong[where f=Collect] ext conj_cong) |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
303 |
(auto simp add: 1 2 not_le[symmetric] intro!: Max_eqI) |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
304 |
also have "\<dots> \<in> sets M" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
305 |
by measurable |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
306 |
finally show "(\<lambda>x. Max {i. P i x}) -` {n} \<inter> space M \<in> sets M" . |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
307 |
qed simp |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
308 |
|
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
309 |
lemma measurable_Min_nat[measurable (raw)]: |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
310 |
fixes P :: "nat \<Rightarrow> 'a \<Rightarrow> bool" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
311 |
assumes [measurable]: "\<And>i. Measurable.pred M (P i)" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
312 |
shows "(\<lambda>x. Min {i. P i x}) \<in> measurable M (count_space UNIV)" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
313 |
unfolding measurable_count_space_eq2_countable |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
314 |
proof safe |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
315 |
fix n |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
316 |
|
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
317 |
{ fix x assume "\<forall>i. \<exists>n\<ge>i. P n x" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
318 |
then have "infinite {i. P i x}" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
319 |
unfolding infinite_nat_iff_unbounded_le by auto |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
320 |
then have "Min {i. P i x} = the None" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
321 |
by (rule Min.infinite) } |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
322 |
note 1 = this |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
323 |
|
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
324 |
{ fix x i j assume "P i x" "\<forall>n\<ge>j. \<not> P n x" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
325 |
then have "finite {i. P i x}" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
326 |
by (auto simp: subset_eq not_le[symmetric] finite_nat_iff_bounded) |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
327 |
with `P i x` have "P (Min {i. P i x}) x" "Min {i. P i x} \<le> i" "finite {i. P i x}" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
328 |
using Min_in[of "{i. P i x}"] by auto } |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
329 |
note 2 = this |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
330 |
|
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
331 |
have "(\<lambda>x. Min {i. P i x}) -` {n} \<inter> space M = {x\<in>space M. Min {i. P i x} = n}" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
332 |
by auto |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
333 |
also have "\<dots> = |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
334 |
{x\<in>space M. if (\<forall>i. \<exists>n\<ge>i. P n x) then the None = n else |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
335 |
if (\<exists>i. P i x) then P n x \<and> (\<forall>i<n. \<not> P i x) |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
336 |
else Min {} = n}" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
337 |
by (intro arg_cong[where f=Collect] ext conj_cong) |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
338 |
(auto simp add: 1 2 not_le[symmetric] intro!: Min_eqI) |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
339 |
also have "\<dots> \<in> sets M" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
340 |
by measurable |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
341 |
finally show "(\<lambda>x. Min {i. P i x}) -` {n} \<inter> space M \<in> sets M" . |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
342 |
qed simp |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56045
diff
changeset
|
343 |
|
50387 | 344 |
lemma measurable_count_space_insert[measurable (raw)]: |
345 |
"s \<in> S \<Longrightarrow> A \<in> sets (count_space S) \<Longrightarrow> insert s A \<in> sets (count_space S)" |
|
346 |
by simp |
|
347 |
||
59000 | 348 |
lemma sets_UNIV [measurable (raw)]: "A \<in> sets (count_space UNIV)" |
349 |
by simp |
|
350 |
||
57025 | 351 |
lemma measurable_card[measurable]: |
352 |
fixes S :: "'a \<Rightarrow> nat set" |
|
353 |
assumes [measurable]: "\<And>i. {x\<in>space M. i \<in> S x} \<in> sets M" |
|
354 |
shows "(\<lambda>x. card (S x)) \<in> measurable M (count_space UNIV)" |
|
355 |
unfolding measurable_count_space_eq2_countable |
|
356 |
proof safe |
|
357 |
fix n show "(\<lambda>x. card (S x)) -` {n} \<inter> space M \<in> sets M" |
|
358 |
proof (cases n) |
|
359 |
case 0 |
|
360 |
then have "(\<lambda>x. card (S x)) -` {n} \<inter> space M = {x\<in>space M. infinite (S x) \<or> (\<forall>i. i \<notin> S x)}" |
|
361 |
by auto |
|
362 |
also have "\<dots> \<in> sets M" |
|
363 |
by measurable |
|
364 |
finally show ?thesis . |
|
365 |
next |
|
366 |
case (Suc i) |
|
367 |
then have "(\<lambda>x. card (S x)) -` {n} \<inter> space M = |
|
368 |
(\<Union>F\<in>{A\<in>{A. finite A}. card A = n}. {x\<in>space M. (\<forall>i. i \<in> S x \<longleftrightarrow> i \<in> F)})" |
|
369 |
unfolding set_eq_iff[symmetric] Collect_bex_eq[symmetric] by (auto intro: card_ge_0_finite) |
|
370 |
also have "\<dots> \<in> sets M" |
|
371 |
by (intro sets.countable_UN' countable_Collect countable_Collect_finite) auto |
|
372 |
finally show ?thesis . |
|
373 |
qed |
|
374 |
qed rule |
|
375 |
||
59088
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
376 |
lemma measurable_pred_countable[measurable (raw)]: |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
377 |
assumes "countable X" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
378 |
shows |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
379 |
"(\<And>i. i \<in> X \<Longrightarrow> Measurable.pred M (\<lambda>x. P x i)) \<Longrightarrow> Measurable.pred M (\<lambda>x. \<forall>i\<in>X. P x i)" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
380 |
"(\<And>i. i \<in> X \<Longrightarrow> Measurable.pred M (\<lambda>x. P x i)) \<Longrightarrow> Measurable.pred M (\<lambda>x. \<exists>i\<in>X. P x i)" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
381 |
unfolding pred_def |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
382 |
by (auto intro!: sets.sets_Collect_countable_All' sets.sets_Collect_countable_Ex' assms) |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
383 |
|
56021
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
384 |
subsection {* Measurability for (co)inductive predicates *} |
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
385 |
|
59088
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
386 |
lemma measurable_bot[measurable]: "bot \<in> measurable M (count_space UNIV)" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
387 |
by (simp add: bot_fun_def) |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
388 |
|
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
389 |
lemma measurable_top[measurable]: "top \<in> measurable M (count_space UNIV)" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
390 |
by (simp add: top_fun_def) |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
391 |
|
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
392 |
lemma measurable_SUP[measurable]: |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
393 |
fixes F :: "'i \<Rightarrow> 'a \<Rightarrow> 'b::{complete_lattice, countable}" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
394 |
assumes [simp]: "countable I" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
395 |
assumes [measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> measurable M (count_space UNIV)" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
396 |
shows "(\<lambda>x. SUP i:I. F i x) \<in> measurable M (count_space UNIV)" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
397 |
unfolding measurable_count_space_eq2_countable |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
398 |
proof (safe intro!: UNIV_I) |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
399 |
fix a |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
400 |
have "(\<lambda>x. SUP i:I. F i x) -` {a} \<inter> space M = |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
401 |
{x\<in>space M. (\<forall>i\<in>I. F i x \<le> a) \<and> (\<forall>b. (\<forall>i\<in>I. F i x \<le> b) \<longrightarrow> a \<le> b)}" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
402 |
unfolding SUP_le_iff[symmetric] by auto |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
403 |
also have "\<dots> \<in> sets M" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
404 |
by measurable |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
405 |
finally show "(\<lambda>x. SUP i:I. F i x) -` {a} \<inter> space M \<in> sets M" . |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
406 |
qed |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
407 |
|
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
408 |
lemma measurable_INF[measurable]: |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
409 |
fixes F :: "'i \<Rightarrow> 'a \<Rightarrow> 'b::{complete_lattice, countable}" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
410 |
assumes [simp]: "countable I" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
411 |
assumes [measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> measurable M (count_space UNIV)" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
412 |
shows "(\<lambda>x. INF i:I. F i x) \<in> measurable M (count_space UNIV)" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
413 |
unfolding measurable_count_space_eq2_countable |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
414 |
proof (safe intro!: UNIV_I) |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
415 |
fix a |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
416 |
have "(\<lambda>x. INF i:I. F i x) -` {a} \<inter> space M = |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
417 |
{x\<in>space M. (\<forall>i\<in>I. a \<le> F i x) \<and> (\<forall>b. (\<forall>i\<in>I. b \<le> F i x) \<longrightarrow> b \<le> a)}" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
418 |
unfolding le_INF_iff[symmetric] by auto |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
419 |
also have "\<dots> \<in> sets M" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
420 |
by measurable |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
421 |
finally show "(\<lambda>x. INF i:I. F i x) -` {a} \<inter> space M \<in> sets M" . |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
422 |
qed |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
423 |
|
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
424 |
lemma measurable_lfp_coinduct[consumes 1, case_names continuity step]: |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
425 |
fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
426 |
assumes "P M" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
427 |
assumes F: "Order_Continuity.continuous F" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
428 |
assumes *: "\<And>M A. P M \<Longrightarrow> (\<And>N. P N \<Longrightarrow> A \<in> measurable N (count_space UNIV)) \<Longrightarrow> F A \<in> measurable M (count_space UNIV)" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
429 |
shows "lfp F \<in> measurable M (count_space UNIV)" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
430 |
proof - |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
431 |
{ fix i from `P M` have "((F ^^ i) bot) \<in> measurable M (count_space UNIV)" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
432 |
by (induct i arbitrary: M) (auto intro!: *) } |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
433 |
then have "(\<lambda>x. SUP i. (F ^^ i) bot x) \<in> measurable M (count_space UNIV)" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
434 |
by measurable |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
435 |
also have "(\<lambda>x. SUP i. (F ^^ i) bot x) = lfp F" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
436 |
by (subst continuous_lfp) (auto intro: F) |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
437 |
finally show ?thesis . |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
438 |
qed |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
439 |
|
56021
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
440 |
lemma measurable_lfp: |
59088
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
441 |
fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
442 |
assumes F: "Order_Continuity.continuous F" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
443 |
assumes *: "\<And>A. A \<in> measurable M (count_space UNIV) \<Longrightarrow> F A \<in> measurable M (count_space UNIV)" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
444 |
shows "lfp F \<in> measurable M (count_space UNIV)" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
445 |
by (coinduction rule: measurable_lfp_coinduct[OF _ F]) (blast intro: *) |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
446 |
|
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
447 |
lemma measurable_gfp_coinduct[consumes 1, case_names continuity step]: |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
448 |
fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
449 |
assumes "P M" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
450 |
assumes F: "Order_Continuity.down_continuous F" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
451 |
assumes *: "\<And>M A. P M \<Longrightarrow> (\<And>N. P N \<Longrightarrow> A \<in> measurable N (count_space UNIV)) \<Longrightarrow> F A \<in> measurable M (count_space UNIV)" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
452 |
shows "gfp F \<in> measurable M (count_space UNIV)" |
56021
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
453 |
proof - |
59088
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
454 |
{ fix i from `P M` have "((F ^^ i) top) \<in> measurable M (count_space UNIV)" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
455 |
by (induct i arbitrary: M) (auto intro!: *) } |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
456 |
then have "(\<lambda>x. INF i. (F ^^ i) top x) \<in> measurable M (count_space UNIV)" |
56021
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
457 |
by measurable |
59088
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
458 |
also have "(\<lambda>x. INF i. (F ^^ i) top x) = gfp F" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
459 |
by (subst down_continuous_gfp) (auto intro: F) |
56021
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
460 |
finally show ?thesis . |
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
461 |
qed |
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
462 |
|
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
463 |
lemma measurable_gfp: |
59088
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
464 |
fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
465 |
assumes F: "Order_Continuity.down_continuous F" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
466 |
assumes *: "\<And>A. A \<in> measurable M (count_space UNIV) \<Longrightarrow> F A \<in> measurable M (count_space UNIV)" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
467 |
shows "gfp F \<in> measurable M (count_space UNIV)" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
468 |
by (coinduction rule: measurable_gfp_coinduct[OF _ F]) (blast intro: *) |
59000 | 469 |
|
470 |
lemma measurable_lfp2_coinduct[consumes 1, case_names continuity step]: |
|
59088
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
471 |
fixes F :: "('a \<Rightarrow> 'c \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'c \<Rightarrow> 'b::{complete_lattice, countable})" |
59000 | 472 |
assumes "P M s" |
59088
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
473 |
assumes F: "Order_Continuity.continuous F" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
474 |
assumes *: "\<And>M A s. P M s \<Longrightarrow> (\<And>N t. P N t \<Longrightarrow> A t \<in> measurable N (count_space UNIV)) \<Longrightarrow> F A s \<in> measurable M (count_space UNIV)" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
475 |
shows "lfp F s \<in> measurable M (count_space UNIV)" |
59000 | 476 |
proof - |
59088
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
477 |
{ fix i from `P M s` have "(\<lambda>x. (F ^^ i) bot s x) \<in> measurable M (count_space UNIV)" |
59000 | 478 |
by (induct i arbitrary: M s) (auto intro!: *) } |
59088
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
479 |
then have "(\<lambda>x. SUP i. (F ^^ i) bot s x) \<in> measurable M (count_space UNIV)" |
59000 | 480 |
by measurable |
59088
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
481 |
also have "(\<lambda>x. SUP i. (F ^^ i) bot s x) = lfp F s" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
482 |
by (subst continuous_lfp) (auto simp: F) |
59000 | 483 |
finally show ?thesis . |
484 |
qed |
|
485 |
||
486 |
lemma measurable_gfp2_coinduct[consumes 1, case_names continuity step]: |
|
59088
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
487 |
fixes F :: "('a \<Rightarrow> 'c \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'c \<Rightarrow> 'b::{complete_lattice, countable})" |
59000 | 488 |
assumes "P M s" |
59088
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
489 |
assumes F: "Order_Continuity.down_continuous F" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
490 |
assumes *: "\<And>M A s. P M s \<Longrightarrow> (\<And>N t. P N t \<Longrightarrow> A t \<in> measurable N (count_space UNIV)) \<Longrightarrow> F A s \<in> measurable M (count_space UNIV)" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
491 |
shows "gfp F s \<in> measurable M (count_space UNIV)" |
59000 | 492 |
proof - |
59088
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
493 |
{ fix i from `P M s` have "(\<lambda>x. (F ^^ i) top s x) \<in> measurable M (count_space UNIV)" |
59000 | 494 |
by (induct i arbitrary: M s) (auto intro!: *) } |
59088
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
495 |
then have "(\<lambda>x. INF i. (F ^^ i) top s x) \<in> measurable M (count_space UNIV)" |
59000 | 496 |
by measurable |
59088
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
497 |
also have "(\<lambda>x. INF i. (F ^^ i) top s x) = gfp F s" |
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
hoelzl
parents:
59048
diff
changeset
|
498 |
by (subst down_continuous_gfp) (auto simp: F) |
59000 | 499 |
finally show ?thesis . |
500 |
qed |
|
501 |
||
502 |
lemma measurable_enat_coinduct: |
|
503 |
fixes f :: "'a \<Rightarrow> enat" |
|
504 |
assumes "R f" |
|
505 |
assumes *: "\<And>f. R f \<Longrightarrow> \<exists>g h i P. R g \<and> f = (\<lambda>x. if P x then h x else eSuc (g (i x))) \<and> |
|
506 |
Measurable.pred M P \<and> |
|
507 |
i \<in> measurable M M \<and> |
|
508 |
h \<in> measurable M (count_space UNIV)" |
|
509 |
shows "f \<in> measurable M (count_space UNIV)" |
|
510 |
proof (simp add: measurable_count_space_eq2_countable, rule ) |
|
511 |
fix a :: enat |
|
512 |
have "f -` {a} \<inter> space M = {x\<in>space M. f x = a}" |
|
513 |
by auto |
|
514 |
{ fix i :: nat |
|
515 |
from `R f` have "Measurable.pred M (\<lambda>x. f x = enat i)" |
|
516 |
proof (induction i arbitrary: f) |
|
517 |
case 0 |
|
518 |
from *[OF this] obtain g h i P |
|
519 |
where f: "f = (\<lambda>x. if P x then h x else eSuc (g (i x)))" and |
|
520 |
[measurable]: "Measurable.pred M P" "i \<in> measurable M M" "h \<in> measurable M (count_space UNIV)" |
|
521 |
by auto |
|
522 |
have "Measurable.pred M (\<lambda>x. P x \<and> h x = 0)" |
|
523 |
by measurable |
|
524 |
also have "(\<lambda>x. P x \<and> h x = 0) = (\<lambda>x. f x = enat 0)" |
|
525 |
by (auto simp: f zero_enat_def[symmetric]) |
|
526 |
finally show ?case . |
|
527 |
next |
|
528 |
case (Suc n) |
|
529 |
from *[OF Suc.prems] obtain g h i P |
|
530 |
where f: "f = (\<lambda>x. if P x then h x else eSuc (g (i x)))" and "R g" and |
|
531 |
M[measurable]: "Measurable.pred M P" "i \<in> measurable M M" "h \<in> measurable M (count_space UNIV)" |
|
532 |
by auto |
|
533 |
have "(\<lambda>x. f x = enat (Suc n)) = |
|
534 |
(\<lambda>x. (P x \<longrightarrow> h x = enat (Suc n)) \<and> (\<not> P x \<longrightarrow> g (i x) = enat n))" |
|
535 |
by (auto simp: f zero_enat_def[symmetric] eSuc_enat[symmetric]) |
|
536 |
also have "Measurable.pred M \<dots>" |
|
537 |
by (intro pred_intros_logic measurable_compose[OF M(2)] Suc `R g`) measurable |
|
538 |
finally show ?case . |
|
539 |
qed |
|
540 |
then have "f -` {enat i} \<inter> space M \<in> sets M" |
|
541 |
by (simp add: pred_def Int_def conj_commute) } |
|
542 |
note fin = this |
|
543 |
show "f -` {a} \<inter> space M \<in> sets M" |
|
544 |
proof (cases a) |
|
545 |
case infinity |
|
546 |
then have "f -` {a} \<inter> space M = space M - (\<Union>n. f -` {enat n} \<inter> space M)" |
|
547 |
by auto |
|
548 |
also have "\<dots> \<in> sets M" |
|
549 |
by (intro sets.Diff sets.top sets.Un sets.countable_UN) (auto intro!: fin) |
|
550 |
finally show ?thesis . |
|
551 |
qed (simp add: fin) |
|
552 |
qed |
|
553 |
||
554 |
lemma measurable_THE: |
|
555 |
fixes P :: "'a \<Rightarrow> 'b \<Rightarrow> bool" |
|
556 |
assumes [measurable]: "\<And>i. Measurable.pred M (P i)" |
|
557 |
assumes I[simp]: "countable I" "\<And>i x. x \<in> space M \<Longrightarrow> P i x \<Longrightarrow> i \<in> I" |
|
558 |
assumes unique: "\<And>x i j. x \<in> space M \<Longrightarrow> P i x \<Longrightarrow> P j x \<Longrightarrow> i = j" |
|
559 |
shows "(\<lambda>x. THE i. P i x) \<in> measurable M (count_space UNIV)" |
|
560 |
unfolding measurable_def |
|
561 |
proof safe |
|
562 |
fix X |
|
563 |
def f \<equiv> "\<lambda>x. THE i. P i x" def undef \<equiv> "THE i::'a. False" |
|
564 |
{ fix i x assume "x \<in> space M" "P i x" then have "f x = i" |
|
565 |
unfolding f_def using unique by auto } |
|
566 |
note f_eq = this |
|
567 |
{ fix x assume "x \<in> space M" "\<forall>i\<in>I. \<not> P i x" |
|
568 |
then have "\<And>i. \<not> P i x" |
|
569 |
using I(2)[of x] by auto |
|
570 |
then have "f x = undef" |
|
571 |
by (auto simp: undef_def f_def) } |
|
572 |
then have "f -` X \<inter> space M = (\<Union>i\<in>I \<inter> X. {x\<in>space M. P i x}) \<union> |
|
573 |
(if undef \<in> X then space M - (\<Union>i\<in>I. {x\<in>space M. P i x}) else {})" |
|
574 |
by (auto dest: f_eq) |
|
575 |
also have "\<dots> \<in> sets M" |
|
576 |
by (auto intro!: sets.Diff sets.countable_UN') |
|
577 |
finally show "f -` X \<inter> space M \<in> sets M" . |
|
578 |
qed simp |
|
579 |
||
580 |
lemma measurable_Ex1[measurable (raw)]: |
|
581 |
assumes [simp]: "countable I" and [measurable]: "\<And>i. i \<in> I \<Longrightarrow> Measurable.pred M (P i)" |
|
582 |
shows "Measurable.pred M (\<lambda>x. \<exists>!i\<in>I. P i x)" |
|
583 |
unfolding bex1_def by measurable |
|
584 |
||
585 |
lemma measurable_split_if[measurable (raw)]: |
|
586 |
"(c \<Longrightarrow> Measurable.pred M f) \<Longrightarrow> (\<not> c \<Longrightarrow> Measurable.pred M g) \<Longrightarrow> |
|
587 |
Measurable.pred M (if c then f else g)" |
|
588 |
by simp |
|
589 |
||
590 |
lemma pred_restrict_space: |
|
591 |
assumes "S \<in> sets M" |
|
592 |
shows "Measurable.pred (restrict_space M S) P \<longleftrightarrow> Measurable.pred M (\<lambda>x. x \<in> S \<and> P x)" |
|
593 |
unfolding pred_def sets_Collect_restrict_space_iff[OF assms] .. |
|
594 |
||
595 |
lemma measurable_predpow[measurable]: |
|
596 |
assumes "Measurable.pred M T" |
|
597 |
assumes "\<And>Q. Measurable.pred M Q \<Longrightarrow> Measurable.pred M (R Q)" |
|
598 |
shows "Measurable.pred M ((R ^^ n) T)" |
|
599 |
by (induct n) (auto intro: assms) |
|
600 |
||
50387 | 601 |
hide_const (open) pred |
602 |
||
603 |
end |
|
59048 | 604 |