src/HOL/Analysis/Measurable.thy
 author wenzelm Fri Aug 18 20:47:47 2017 +0200 (2017-08-18) changeset 66453 cc19f7ca2ed6 parent 64320 ba194424b895 child 67962 0acdcd8f4ba1 permissions -rw-r--r--
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
1 (*  Title:      HOL/Analysis/Measurable.thy
2     Author:     Johannes Hölzl <hoelzl@in.tum.de>
3 *)
4 theory Measurable
5   imports
6     Sigma_Algebra
7     "HOL-Library.Order_Continuity"
8 begin
10 subsection \<open>Measurability prover\<close>
12 lemma (in algebra) sets_Collect_finite_All:
13   assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S"
14   shows "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} \<in> M"
15 proof -
16   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})"
17     by auto
18   with assms show ?thesis by (auto intro!: sets_Collect_finite_All')
19 qed
21 abbreviation "pred M P \<equiv> P \<in> measurable M (count_space (UNIV::bool set))"
23 lemma pred_def: "pred M P \<longleftrightarrow> {x\<in>space M. P x} \<in> sets M"
24 proof
25   assume "pred M P"
26   then have "P -` {True} \<inter> space M \<in> sets M"
27     by (auto simp: measurable_count_space_eq2)
28   also have "P -` {True} \<inter> space M = {x\<in>space M. P x}" by auto
29   finally show "{x\<in>space M. P x} \<in> sets M" .
30 next
31   assume P: "{x\<in>space M. P x} \<in> sets M"
32   moreover
33   { fix X
34     have "X \<in> Pow (UNIV :: bool set)" by simp
35     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> {})}"
36       unfolding UNIV_bool Pow_insert Pow_empty by auto
37     then have "P -` X \<inter> space M \<in> sets M"
38       by (auto intro!: sets.sets_Collect_neg sets.sets_Collect_imp sets.sets_Collect_conj sets.sets_Collect_const P) }
39   then show "pred M P"
40     by (auto simp: measurable_def)
41 qed
43 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))"
44   by (rule measurable_compose[where f=f and N=M]) (auto simp: pred_def)
46 lemma pred_sets2: "A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> pred M (\<lambda>x. f x \<in> A)"
47   by (rule measurable_compose[where f=f and N=N]) (auto simp: pred_def Int_def[symmetric])
49 ML_file "measurable.ML"
51 attribute_setup measurable = \<open>
52   Scan.lift (
53     (Args.add >> K true || Args.del >> K false || Scan.succeed true) --
54     Scan.optional (Args.parens (
55       Scan.optional (Args.\$\$\$ "raw" >> K true) false --
56       Scan.optional (Args.\$\$\$ "generic" >> K Measurable.Generic) Measurable.Concrete))
57     (false, Measurable.Concrete) >>
58     Measurable.measurable_thm_attr)
59 \<close> "declaration of measurability theorems"
61 attribute_setup measurable_dest = Measurable.dest_thm_attr
62   "add dest rule to measurability prover"
64 attribute_setup measurable_cong = Measurable.cong_thm_attr
65   "add congurence rules to measurability prover"
67 method_setup measurable = \<open> Scan.lift (Scan.succeed (METHOD o Measurable.measurable_tac)) \<close>
68   "measurability prover"
70 simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = \<open>K Measurable.simproc\<close>
72 setup \<open>
73   Global_Theory.add_thms_dynamic (@{binding measurable}, Measurable.get_all)
74 \<close>
76 declare
77   pred_sets1[measurable_dest]
78   pred_sets2[measurable_dest]
79   sets.sets_into_space[measurable_dest]
81 declare
82   sets.top[measurable]
83   sets.empty_sets[measurable (raw)]
84   sets.Un[measurable (raw)]
85   sets.Diff[measurable (raw)]
87 declare
88   measurable_count_space[measurable (raw)]
89   measurable_ident[measurable (raw)]
90   measurable_id[measurable (raw)]
91   measurable_const[measurable (raw)]
92   measurable_If[measurable (raw)]
93   measurable_comp[measurable (raw)]
94   measurable_sets[measurable (raw)]
96 declare measurable_cong_sets[measurable_cong]
97 declare sets_restrict_space_cong[measurable_cong]
98 declare sets_restrict_UNIV[measurable_cong]
100 lemma predE[measurable (raw)]:
101   "pred M P \<Longrightarrow> {x\<in>space M. P x} \<in> sets M"
102   unfolding pred_def .
104 lemma pred_intros_imp'[measurable (raw)]:
105   "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<longrightarrow> P x)"
106   by (cases K) auto
108 lemma pred_intros_conj1'[measurable (raw)]:
109   "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<and> P x)"
110   by (cases K) auto
112 lemma pred_intros_conj2'[measurable (raw)]:
113   "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<and> K)"
114   by (cases K) auto
116 lemma pred_intros_disj1'[measurable (raw)]:
117   "(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<or> P x)"
118   by (cases K) auto
120 lemma pred_intros_disj2'[measurable (raw)]:
121   "(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<or> K)"
122   by (cases K) auto
124 lemma pred_intros_logic[measurable (raw)]:
125   "pred M (\<lambda>x. x \<in> space M)"
126   "pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. \<not> P x)"
127   "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<and> P x)"
128   "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<longrightarrow> P x)"
129   "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<or> P x)"
130   "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x = P x)"
131   "pred M (\<lambda>x. f x \<in> UNIV)"
132   "pred M (\<lambda>x. f x \<in> {})"
133   "pred M (\<lambda>x. P' (f x) x) \<Longrightarrow> pred M (\<lambda>x. f x \<in> {y. P' y x})"
134   "pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> - (B x))"
135   "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))"
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) \<inter> (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) \<union> (B x))"
138   "pred M (\<lambda>x. g x (f x) \<in> (X x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (g x) -` (X x))"
139   by (auto simp: iff_conv_conj_imp pred_def)
141 lemma pred_intros_countable[measurable (raw)]:
142   fixes P :: "'a \<Rightarrow> 'i :: countable \<Rightarrow> bool"
143   shows
144     "(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i. P x i)"
145     "(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i. P x i)"
146   by (auto intro!: sets.sets_Collect_countable_All sets.sets_Collect_countable_Ex simp: pred_def)
148 lemma pred_intros_countable_bounded[measurable (raw)]:
149   fixes X :: "'i :: countable set"
150   shows
151     "(\<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))"
152     "(\<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))"
153     "(\<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)"
154     "(\<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)"
155   by simp_all (auto simp: Bex_def Ball_def)
157 lemma pred_intros_finite[measurable (raw)]:
158   "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))"
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> (\<Union>i\<in>I. N x i))"
160   "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)"
161   "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)"
162   by (auto intro!: sets.sets_Collect_finite_Ex sets.sets_Collect_finite_All simp: iff_conv_conj_imp pred_def)
164 lemma countable_Un_Int[measurable (raw)]:
165   "(\<And>i :: 'i :: countable. i \<in> I \<Longrightarrow> N i \<in> sets M) \<Longrightarrow> (\<Union>i\<in>I. N i) \<in> sets M"
166   "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"
167   by auto
169 declare
170   finite_UN[measurable (raw)]
171   finite_INT[measurable (raw)]
173 lemma sets_Int_pred[measurable (raw)]:
174   assumes space: "A \<inter> B \<subseteq> space M" and [measurable]: "pred M (\<lambda>x. x \<in> A)" "pred M (\<lambda>x. x \<in> B)"
175   shows "A \<inter> B \<in> sets M"
176 proof -
177   have "{x\<in>space M. x \<in> A \<inter> B} \<in> sets M" by auto
178   also have "{x\<in>space M. x \<in> A \<inter> B} = A \<inter> B"
179     using space by auto
180   finally show ?thesis .
181 qed
183 lemma [measurable (raw generic)]:
184   assumes f: "f \<in> measurable M N" and c: "c \<in> space N \<Longrightarrow> {c} \<in> sets N"
185   shows pred_eq_const1: "pred M (\<lambda>x. f x = c)"
186     and pred_eq_const2: "pred M (\<lambda>x. c = f x)"
187 proof -
188   show "pred M (\<lambda>x. f x = c)"
189   proof cases
190     assume "c \<in> space N"
191     with measurable_sets[OF f c] show ?thesis
192       by (auto simp: Int_def conj_commute pred_def)
193   next
194     assume "c \<notin> space N"
195     with f[THEN measurable_space] have "{x \<in> space M. f x = c} = {}" by auto
196     then show ?thesis by (auto simp: pred_def cong: conj_cong)
197   qed
198   then show "pred M (\<lambda>x. c = f x)"
199     by (simp add: eq_commute)
200 qed
202 lemma pred_count_space_const1[measurable (raw)]:
203   "f \<in> measurable M (count_space UNIV) \<Longrightarrow> Measurable.pred M (\<lambda>x. f x = c)"
204   by (intro pred_eq_const1[where N="count_space UNIV"]) (auto )
206 lemma pred_count_space_const2[measurable (raw)]:
207   "f \<in> measurable M (count_space UNIV) \<Longrightarrow> Measurable.pred M (\<lambda>x. c = f x)"
208   by (intro pred_eq_const2[where N="count_space UNIV"]) (auto )
210 lemma pred_le_const[measurable (raw generic)]:
211   assumes f: "f \<in> measurable M N" and c: "{.. c} \<in> sets N" shows "pred M (\<lambda>x. f x \<le> c)"
212   using measurable_sets[OF f c]
213   by (auto simp: Int_def conj_commute eq_commute pred_def)
215 lemma pred_const_le[measurable (raw generic)]:
216   assumes f: "f \<in> measurable M N" and c: "{c ..} \<in> sets N" shows "pred M (\<lambda>x. c \<le> f x)"
217   using measurable_sets[OF f c]
218   by (auto simp: Int_def conj_commute eq_commute pred_def)
220 lemma pred_less_const[measurable (raw generic)]:
221   assumes f: "f \<in> measurable M N" and c: "{..< c} \<in> sets N" shows "pred M (\<lambda>x. f x < c)"
222   using measurable_sets[OF f c]
223   by (auto simp: Int_def conj_commute eq_commute pred_def)
225 lemma pred_const_less[measurable (raw generic)]:
226   assumes f: "f \<in> measurable M N" and c: "{c <..} \<in> sets N" shows "pred M (\<lambda>x. c < f x)"
227   using measurable_sets[OF f c]
228   by (auto simp: Int_def conj_commute eq_commute pred_def)
230 declare
231   sets.Int[measurable (raw)]
233 lemma pred_in_If[measurable (raw)]:
234   "(P \<Longrightarrow> pred M (\<lambda>x. x \<in> A x)) \<Longrightarrow> (\<not> P \<Longrightarrow> pred M (\<lambda>x. x \<in> B x)) \<Longrightarrow>
235     pred M (\<lambda>x. x \<in> (if P then A x else B x))"
236   by auto
238 lemma sets_range[measurable_dest]:
239   "A ` I \<subseteq> sets M \<Longrightarrow> i \<in> I \<Longrightarrow> A i \<in> sets M"
240   by auto
242 lemma pred_sets_range[measurable_dest]:
243   "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)"
244   using pred_sets2[OF sets_range] by auto
246 lemma sets_All[measurable_dest]:
247   "\<forall>i. A i \<in> sets (M i) \<Longrightarrow> A i \<in> sets (M i)"
248   by auto
250 lemma pred_sets_All[measurable_dest]:
251   "\<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)"
252   using pred_sets2[OF sets_All, of A N f] by auto
254 lemma sets_Ball[measurable_dest]:
255   "\<forall>i\<in>I. A i \<in> sets (M i) \<Longrightarrow> i\<in>I \<Longrightarrow> A i \<in> sets (M i)"
256   by auto
258 lemma pred_sets_Ball[measurable_dest]:
259   "\<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)"
260   using pred_sets2[OF sets_Ball, of _ _ _ f] by auto
262 lemma measurable_finite[measurable (raw)]:
263   fixes S :: "'a \<Rightarrow> nat set"
264   assumes [measurable]: "\<And>i. {x\<in>space M. i \<in> S x} \<in> sets M"
265   shows "pred M (\<lambda>x. finite (S x))"
266   unfolding finite_nat_set_iff_bounded by (simp add: Ball_def)
268 lemma measurable_Least[measurable]:
269   assumes [measurable]: "(\<And>i::nat. (\<lambda>x. P i x) \<in> measurable M (count_space UNIV))"
270   shows "(\<lambda>x. LEAST i. P i x) \<in> measurable M (count_space UNIV)"
271   unfolding measurable_def by (safe intro!: sets_Least) simp_all
273 lemma measurable_Max_nat[measurable (raw)]:
274   fixes P :: "nat \<Rightarrow> 'a \<Rightarrow> bool"
275   assumes [measurable]: "\<And>i. Measurable.pred M (P i)"
276   shows "(\<lambda>x. Max {i. P i x}) \<in> measurable M (count_space UNIV)"
277   unfolding measurable_count_space_eq2_countable
278 proof safe
279   fix n
281   { fix x assume "\<forall>i. \<exists>n\<ge>i. P n x"
282     then have "infinite {i. P i x}"
283       unfolding infinite_nat_iff_unbounded_le by auto
284     then have "Max {i. P i x} = the None"
285       by (rule Max.infinite) }
286   note 1 = this
288   { fix x i j assume "P i x" "\<forall>n\<ge>j. \<not> P n x"
289     then have "finite {i. P i x}"
290       by (auto simp: subset_eq not_le[symmetric] finite_nat_iff_bounded)
291     with \<open>P i x\<close> have "P (Max {i. P i x}) x" "i \<le> Max {i. P i x}" "finite {i. P i x}"
292       using Max_in[of "{i. P i x}"] by auto }
293   note 2 = this
295   have "(\<lambda>x. Max {i. P i x}) -` {n} \<inter> space M = {x\<in>space M. Max {i. P i x} = n}"
296     by auto
297   also have "\<dots> =
298     {x\<in>space M. if (\<forall>i. \<exists>n\<ge>i. P n x) then the None = n else
299       if (\<exists>i. P i x) then P n x \<and> (\<forall>i>n. \<not> P i x)
300       else Max {} = n}"
301     by (intro arg_cong[where f=Collect] ext conj_cong)
302        (auto simp add: 1 2 not_le[symmetric] intro!: Max_eqI)
303   also have "\<dots> \<in> sets M"
304     by measurable
305   finally show "(\<lambda>x. Max {i. P i x}) -` {n} \<inter> space M \<in> sets M" .
306 qed simp
308 lemma measurable_Min_nat[measurable (raw)]:
309   fixes P :: "nat \<Rightarrow> 'a \<Rightarrow> bool"
310   assumes [measurable]: "\<And>i. Measurable.pred M (P i)"
311   shows "(\<lambda>x. Min {i. P i x}) \<in> measurable M (count_space UNIV)"
312   unfolding measurable_count_space_eq2_countable
313 proof safe
314   fix n
316   { fix x assume "\<forall>i. \<exists>n\<ge>i. P n x"
317     then have "infinite {i. P i x}"
318       unfolding infinite_nat_iff_unbounded_le by auto
319     then have "Min {i. P i x} = the None"
320       by (rule Min.infinite) }
321   note 1 = this
323   { fix x i j assume "P i x" "\<forall>n\<ge>j. \<not> P n x"
324     then have "finite {i. P i x}"
325       by (auto simp: subset_eq not_le[symmetric] finite_nat_iff_bounded)
326     with \<open>P i x\<close> have "P (Min {i. P i x}) x" "Min {i. P i x} \<le> i" "finite {i. P i x}"
327       using Min_in[of "{i. P i x}"] by auto }
328   note 2 = this
330   have "(\<lambda>x. Min {i. P i x}) -` {n} \<inter> space M = {x\<in>space M. Min {i. P i x} = n}"
331     by auto
332   also have "\<dots> =
333     {x\<in>space M. if (\<forall>i. \<exists>n\<ge>i. P n x) then the None = n else
334       if (\<exists>i. P i x) then P n x \<and> (\<forall>i<n. \<not> P i x)
335       else Min {} = n}"
336     by (intro arg_cong[where f=Collect] ext conj_cong)
337        (auto simp add: 1 2 not_le[symmetric] intro!: Min_eqI)
338   also have "\<dots> \<in> sets M"
339     by measurable
340   finally show "(\<lambda>x. Min {i. P i x}) -` {n} \<inter> space M \<in> sets M" .
341 qed simp
343 lemma measurable_count_space_insert[measurable (raw)]:
344   "s \<in> S \<Longrightarrow> A \<in> sets (count_space S) \<Longrightarrow> insert s A \<in> sets (count_space S)"
345   by simp
347 lemma sets_UNIV [measurable (raw)]: "A \<in> sets (count_space UNIV)"
348   by simp
350 lemma measurable_card[measurable]:
351   fixes S :: "'a \<Rightarrow> nat set"
352   assumes [measurable]: "\<And>i. {x\<in>space M. i \<in> S x} \<in> sets M"
353   shows "(\<lambda>x. card (S x)) \<in> measurable M (count_space UNIV)"
354   unfolding measurable_count_space_eq2_countable
355 proof safe
356   fix n show "(\<lambda>x. card (S x)) -` {n} \<inter> space M \<in> sets M"
357   proof (cases n)
358     case 0
359     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)}"
360       by auto
361     also have "\<dots> \<in> sets M"
362       by measurable
363     finally show ?thesis .
364   next
365     case (Suc i)
366     then have "(\<lambda>x. card (S x)) -` {n} \<inter> space M =
367       (\<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)})"
368       unfolding set_eq_iff[symmetric] Collect_bex_eq[symmetric] by (auto intro: card_ge_0_finite)
369     also have "\<dots> \<in> sets M"
370       by (intro sets.countable_UN' countable_Collect countable_Collect_finite) auto
371     finally show ?thesis .
372   qed
373 qed rule
375 lemma measurable_pred_countable[measurable (raw)]:
376   assumes "countable X"
377   shows
378     "(\<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)"
379     "(\<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)"
380   unfolding pred_def
381   by (auto intro!: sets.sets_Collect_countable_All' sets.sets_Collect_countable_Ex' assms)
383 subsection \<open>Measurability for (co)inductive predicates\<close>
385 lemma measurable_bot[measurable]: "bot \<in> measurable M (count_space UNIV)"
386   by (simp add: bot_fun_def)
388 lemma measurable_top[measurable]: "top \<in> measurable M (count_space UNIV)"
389   by (simp add: top_fun_def)
391 lemma measurable_SUP[measurable]:
392   fixes F :: "'i \<Rightarrow> 'a \<Rightarrow> 'b::{complete_lattice, countable}"
393   assumes [simp]: "countable I"
394   assumes [measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> measurable M (count_space UNIV)"
395   shows "(\<lambda>x. SUP i:I. F i x) \<in> measurable M (count_space UNIV)"
396   unfolding measurable_count_space_eq2_countable
397 proof (safe intro!: UNIV_I)
398   fix a
399   have "(\<lambda>x. SUP i:I. F i x) -` {a} \<inter> space M =
400     {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)}"
401     unfolding SUP_le_iff[symmetric] by auto
402   also have "\<dots> \<in> sets M"
403     by measurable
404   finally show "(\<lambda>x. SUP i:I. F i x) -` {a} \<inter> space M \<in> sets M" .
405 qed
407 lemma measurable_INF[measurable]:
408   fixes F :: "'i \<Rightarrow> 'a \<Rightarrow> 'b::{complete_lattice, countable}"
409   assumes [simp]: "countable I"
410   assumes [measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> measurable M (count_space UNIV)"
411   shows "(\<lambda>x. INF i:I. F i x) \<in> measurable M (count_space UNIV)"
412   unfolding measurable_count_space_eq2_countable
413 proof (safe intro!: UNIV_I)
414   fix a
415   have "(\<lambda>x. INF i:I. F i x) -` {a} \<inter> space M =
416     {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)}"
417     unfolding le_INF_iff[symmetric] by auto
418   also have "\<dots> \<in> sets M"
419     by measurable
420   finally show "(\<lambda>x. INF i:I. F i x) -` {a} \<inter> space M \<in> sets M" .
421 qed
423 lemma measurable_lfp_coinduct[consumes 1, case_names continuity step]:
424   fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})"
425   assumes "P M"
426   assumes F: "sup_continuous F"
427   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)"
428   shows "lfp F \<in> measurable M (count_space UNIV)"
429 proof -
430   { fix i from \<open>P M\<close> have "((F ^^ i) bot) \<in> measurable M (count_space UNIV)"
431       by (induct i arbitrary: M) (auto intro!: *) }
432   then have "(\<lambda>x. SUP i. (F ^^ i) bot x) \<in> measurable M (count_space UNIV)"
433     by measurable
434   also have "(\<lambda>x. SUP i. (F ^^ i) bot x) = lfp F"
435     by (subst sup_continuous_lfp) (auto intro: F)
436   finally show ?thesis .
437 qed
439 lemma measurable_lfp:
440   fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})"
441   assumes F: "sup_continuous F"
442   assumes *: "\<And>A. A \<in> measurable M (count_space UNIV) \<Longrightarrow> F A \<in> measurable M (count_space UNIV)"
443   shows "lfp F \<in> measurable M (count_space UNIV)"
444   by (coinduction rule: measurable_lfp_coinduct[OF _ F]) (blast intro: *)
446 lemma measurable_gfp_coinduct[consumes 1, case_names continuity step]:
447   fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})"
448   assumes "P M"
449   assumes F: "inf_continuous F"
450   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)"
451   shows "gfp F \<in> measurable M (count_space UNIV)"
452 proof -
453   { fix i from \<open>P M\<close> have "((F ^^ i) top) \<in> measurable M (count_space UNIV)"
454       by (induct i arbitrary: M) (auto intro!: *) }
455   then have "(\<lambda>x. INF i. (F ^^ i) top x) \<in> measurable M (count_space UNIV)"
456     by measurable
457   also have "(\<lambda>x. INF i. (F ^^ i) top x) = gfp F"
458     by (subst inf_continuous_gfp) (auto intro: F)
459   finally show ?thesis .
460 qed
462 lemma measurable_gfp:
463   fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})"
464   assumes F: "inf_continuous F"
465   assumes *: "\<And>A. A \<in> measurable M (count_space UNIV) \<Longrightarrow> F A \<in> measurable M (count_space UNIV)"
466   shows "gfp F \<in> measurable M (count_space UNIV)"
467   by (coinduction rule: measurable_gfp_coinduct[OF _ F]) (blast intro: *)
469 lemma measurable_lfp2_coinduct[consumes 1, case_names continuity step]:
470   fixes F :: "('a \<Rightarrow> 'c \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'c \<Rightarrow> 'b::{complete_lattice, countable})"
471   assumes "P M s"
472   assumes F: "sup_continuous F"
473   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)"
474   shows "lfp F s \<in> measurable M (count_space UNIV)"
475 proof -
476   { fix i from \<open>P M s\<close> have "(\<lambda>x. (F ^^ i) bot s x) \<in> measurable M (count_space UNIV)"
477       by (induct i arbitrary: M s) (auto intro!: *) }
478   then have "(\<lambda>x. SUP i. (F ^^ i) bot s x) \<in> measurable M (count_space UNIV)"
479     by measurable
480   also have "(\<lambda>x. SUP i. (F ^^ i) bot s x) = lfp F s"
481     by (subst sup_continuous_lfp) (auto simp: F)
482   finally show ?thesis .
483 qed
485 lemma measurable_gfp2_coinduct[consumes 1, case_names continuity step]:
486   fixes F :: "('a \<Rightarrow> 'c \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'c \<Rightarrow> 'b::{complete_lattice, countable})"
487   assumes "P M s"
488   assumes F: "inf_continuous F"
489   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)"
490   shows "gfp F s \<in> measurable M (count_space UNIV)"
491 proof -
492   { fix i from \<open>P M s\<close> have "(\<lambda>x. (F ^^ i) top s x) \<in> measurable M (count_space UNIV)"
493       by (induct i arbitrary: M s) (auto intro!: *) }
494   then have "(\<lambda>x. INF i. (F ^^ i) top s x) \<in> measurable M (count_space UNIV)"
495     by measurable
496   also have "(\<lambda>x. INF i. (F ^^ i) top s x) = gfp F s"
497     by (subst inf_continuous_gfp) (auto simp: F)
498   finally show ?thesis .
499 qed
501 lemma measurable_enat_coinduct:
502   fixes f :: "'a \<Rightarrow> enat"
503   assumes "R f"
504   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>
505     Measurable.pred M P \<and>
506     i \<in> measurable M M \<and>
507     h \<in> measurable M (count_space UNIV)"
508   shows "f \<in> measurable M (count_space UNIV)"
509 proof (simp add: measurable_count_space_eq2_countable, rule )
510   fix a :: enat
511   have "f -` {a} \<inter> space M = {x\<in>space M. f x = a}"
512     by auto
513   { fix i :: nat
514     from \<open>R f\<close> have "Measurable.pred M (\<lambda>x. f x = enat i)"
515     proof (induction i arbitrary: f)
516       case 0
517       from *[OF this] obtain g h i P
518         where f: "f = (\<lambda>x. if P x then h x else eSuc (g (i x)))" and
519           [measurable]: "Measurable.pred M P" "i \<in> measurable M M" "h \<in> measurable M (count_space UNIV)"
520         by auto
521       have "Measurable.pred M (\<lambda>x. P x \<and> h x = 0)"
522         by measurable
523       also have "(\<lambda>x. P x \<and> h x = 0) = (\<lambda>x. f x = enat 0)"
524         by (auto simp: f zero_enat_def[symmetric])
525       finally show ?case .
526     next
527       case (Suc n)
528       from *[OF Suc.prems] obtain g h i P
529         where f: "f = (\<lambda>x. if P x then h x else eSuc (g (i x)))" and "R g" and
530           M[measurable]: "Measurable.pred M P" "i \<in> measurable M M" "h \<in> measurable M (count_space UNIV)"
531         by auto
532       have "(\<lambda>x. f x = enat (Suc n)) =
533         (\<lambda>x. (P x \<longrightarrow> h x = enat (Suc n)) \<and> (\<not> P x \<longrightarrow> g (i x) = enat n))"
534         by (auto simp: f zero_enat_def[symmetric] eSuc_enat[symmetric])
535       also have "Measurable.pred M \<dots>"
536         by (intro pred_intros_logic measurable_compose[OF M(2)] Suc \<open>R g\<close>) measurable
537       finally show ?case .
538     qed
539     then have "f -` {enat i} \<inter> space M \<in> sets M"
540       by (simp add: pred_def Int_def conj_commute) }
541   note fin = this
542   show "f -` {a} \<inter> space M \<in> sets M"
543   proof (cases a)
544     case infinity
545     then have "f -` {a} \<inter> space M = space M - (\<Union>n. f -` {enat n} \<inter> space M)"
546       by auto
547     also have "\<dots> \<in> sets M"
548       by (intro sets.Diff sets.top sets.Un sets.countable_UN) (auto intro!: fin)
549     finally show ?thesis .
550   qed (simp add: fin)
551 qed
553 lemma measurable_THE:
554   fixes P :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
555   assumes [measurable]: "\<And>i. Measurable.pred M (P i)"
556   assumes I[simp]: "countable I" "\<And>i x. x \<in> space M \<Longrightarrow> P i x \<Longrightarrow> i \<in> I"
557   assumes unique: "\<And>x i j. x \<in> space M \<Longrightarrow> P i x \<Longrightarrow> P j x \<Longrightarrow> i = j"
558   shows "(\<lambda>x. THE i. P i x) \<in> measurable M (count_space UNIV)"
559   unfolding measurable_def
560 proof safe
561   fix X
562   define f where "f x = (THE i. P i x)" for x
563   define undef where "undef = (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
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
585 lemma measurable_Sup_nat[measurable (raw)]:
586   fixes F :: "'a \<Rightarrow> nat set"
587   assumes [measurable]: "\<And>i. Measurable.pred M (\<lambda>x. i \<in> F x)"
588   shows "(\<lambda>x. Sup (F x)) \<in> M \<rightarrow>\<^sub>M count_space UNIV"
589 proof (clarsimp simp add: measurable_count_space_eq2_countable)
590   fix a
591   have F_empty_iff: "F x = {} \<longleftrightarrow> (\<forall>i. i \<notin> F x)" for x
592     by auto
593   have "Measurable.pred M (\<lambda>x. if finite (F x) then if F x = {} then a = Max {}
594     else a \<in> F x \<and> (\<forall>j. j \<in> F x \<longrightarrow> j \<le> a) else a = the None)"
595     unfolding finite_nat_set_iff_bounded Ball_def F_empty_iff by measurable
596   moreover have "(\<lambda>x. Sup (F x)) -` {a} \<inter> space M =
597     {x\<in>space M. if finite (F x) then if F x = {} then a = Max {}
598       else a \<in> F x \<and> (\<forall>j. j \<in> F x \<longrightarrow> j \<le> a) else a = the None}"
599     by (intro set_eqI)
600        (auto simp: Sup_nat_def Max.infinite intro!: Max_in Max_eqI)
601   ultimately show "(\<lambda>x. Sup (F x)) -` {a} \<inter> space M \<in> sets M"
602     by auto
603 qed
605 lemma measurable_if_split[measurable (raw)]:
606   "(c \<Longrightarrow> Measurable.pred M f) \<Longrightarrow> (\<not> c \<Longrightarrow> Measurable.pred M g) \<Longrightarrow>
607    Measurable.pred M (if c then f else g)"
608   by simp
610 lemma pred_restrict_space:
611   assumes "S \<in> sets M"
612   shows "Measurable.pred (restrict_space M S) P \<longleftrightarrow> Measurable.pred M (\<lambda>x. x \<in> S \<and> P x)"
613   unfolding pred_def sets_Collect_restrict_space_iff[OF assms] ..
615 lemma measurable_predpow[measurable]:
616   assumes "Measurable.pred M T"
617   assumes "\<And>Q. Measurable.pred M Q \<Longrightarrow> Measurable.pred M (R Q)"
618   shows "Measurable.pred M ((R ^^ n) T)"
619   by (induct n) (auto intro: assms)
621 lemma measurable_compose_countable_restrict:
622   assumes P: "countable {i. P i}"
623     and f: "f \<in> M \<rightarrow>\<^sub>M count_space UNIV"
624     and Q: "\<And>i. P i \<Longrightarrow> pred M (Q i)"
625   shows "pred M (\<lambda>x. P (f x) \<and> Q (f x) x)"
626 proof -
627   have P_f: "{x \<in> space M. P (f x)} \<in> sets M"
628     unfolding pred_def[symmetric] by (rule measurable_compose[OF f]) simp
629   have "pred (restrict_space M {x\<in>space M. P (f x)}) (\<lambda>x. Q (f x) x)"
630   proof (rule measurable_compose_countable'[where g=f, OF _ _ P])
631     show "f \<in> restrict_space M {x\<in>space M. P (f x)} \<rightarrow>\<^sub>M count_space {i. P i}"
632       by (rule measurable_count_space_extend[OF subset_UNIV])
633          (auto simp: space_restrict_space intro!: measurable_restrict_space1 f)
634   qed (auto intro!: measurable_restrict_space1 Q)
635   then show ?thesis
636     unfolding pred_restrict_space[OF P_f] by (simp cong: measurable_cong)
637 qed
639 lemma measurable_limsup [measurable (raw)]:
640   assumes [measurable]: "\<And>n. A n \<in> sets M"
641   shows "limsup A \<in> sets M"
642 by (subst limsup_INF_SUP, auto)
644 lemma measurable_liminf [measurable (raw)]:
645   assumes [measurable]: "\<And>n. A n \<in> sets M"
646   shows "liminf A \<in> sets M"
647 by (subst liminf_SUP_INF, auto)
649 lemma measurable_case_enat[measurable (raw)]:
650   assumes f: "f \<in> M \<rightarrow>\<^sub>M count_space UNIV" and g: "\<And>i. g i \<in> M \<rightarrow>\<^sub>M N" and h: "h \<in> M \<rightarrow>\<^sub>M N"
651   shows "(\<lambda>x. case f x of enat i \<Rightarrow> g i x | \<infinity> \<Rightarrow> h x) \<in> M \<rightarrow>\<^sub>M N"
652   apply (rule measurable_compose_countable[OF _ f])
653   subgoal for i
654     by (cases i) (auto intro: g h)
655   done
657 hide_const (open) pred
659 end