author  hoelzl 
Thu, 04 Dec 2014 17:05:58 +0100  
changeset 59088  ff2bd4a14ddb 
parent 59048  7dc8ac6f0895 
child 59353  f0707dc3d9aa 
permissions  rwrr 
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 

59047  66 
attribute_setup measurable_app = Measurable.app_thm_attr 
59048  67 
"add application rule to measurability prover" 
68 

69 
attribute_setup measurable_cong = Measurable.cong_thm_attr 

70 
"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

71 

59047  72 
method_setup measurable = \<open> Scan.lift (Scan.succeed (METHOD o Measurable.measurable_tac)) \<close> 
73 
"measurability prover" 

53043
8cbfbeb566a4
more standard attribute_setup / method_setup  export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset

74 

50387  75 
simproc_setup measurable ("A \<in> sets M"  "f \<in> measurable M N") = {* K Measurable.simproc *} 
76 

58965  77 
setup {* 
59048  78 
Global_Theory.add_thms_dynamic (@{binding measurable}, Measurable.get_all) 
58965  79 
*} 
80 

50387  81 
declare 
82 
measurable_compose_rev[measurable_dest] 

83 
pred_sets1[measurable_dest] 

84 
pred_sets2[measurable_dest] 

85 
sets.sets_into_space[measurable_dest] 

86 

87 
declare 

88 
sets.top[measurable] 

89 
sets.empty_sets[measurable (raw)] 

90 
sets.Un[measurable (raw)] 

91 
sets.Diff[measurable (raw)] 

92 

93 
declare 

94 
measurable_count_space[measurable (raw)] 

95 
measurable_ident[measurable (raw)] 

59048  96 
measurable_id[measurable (raw)] 
50387  97 
measurable_const[measurable (raw)] 
98 
measurable_If[measurable (raw)] 

99 
measurable_comp[measurable (raw)] 

100 
measurable_sets[measurable (raw)] 

101 

59048  102 
declare measurable_cong_sets[measurable_cong] 
103 
declare sets_restrict_space_cong[measurable_cong] 

104 

50387  105 
lemma predE[measurable (raw)]: 
106 
"pred M P \<Longrightarrow> {x\<in>space M. P x} \<in> sets M" 

107 
unfolding pred_def . 

108 

109 
lemma pred_intros_imp'[measurable (raw)]: 

110 
"(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<longrightarrow> P x)" 

111 
by (cases K) auto 

112 

113 
lemma pred_intros_conj1'[measurable (raw)]: 

114 
"(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<and> P x)" 

115 
by (cases K) auto 

116 

117 
lemma pred_intros_conj2'[measurable (raw)]: 

118 
"(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<and> K)" 

119 
by (cases K) auto 

120 

121 
lemma pred_intros_disj1'[measurable (raw)]: 

122 
"(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<or> P x)" 

123 
by (cases K) auto 

124 

125 
lemma pred_intros_disj2'[measurable (raw)]: 

126 
"(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<or> K)" 

127 
by (cases K) auto 

128 

129 
lemma pred_intros_logic[measurable (raw)]: 

130 
"pred M (\<lambda>x. x \<in> space M)" 

131 
"pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. \<not> P x)" 

132 
"pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<and> P x)" 

133 
"pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<longrightarrow> P x)" 

134 
"pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<or> P x)" 

135 
"pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x = P x)" 

136 
"pred M (\<lambda>x. f x \<in> UNIV)" 

137 
"pred M (\<lambda>x. f x \<in> {})" 

138 
"pred M (\<lambda>x. P' (f x) x) \<Longrightarrow> pred M (\<lambda>x. f x \<in> {y. P' y x})" 

139 
"pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in>  (B x))" 

140 
"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))" 

141 
"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))" 

142 
"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))" 

143 
"pred M (\<lambda>x. g x (f x) \<in> (X x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (g x) ` (X x))" 

144 
by (auto simp: iff_conv_conj_imp pred_def) 

145 

146 
lemma pred_intros_countable[measurable (raw)]: 

147 
fixes P :: "'a \<Rightarrow> 'i :: countable \<Rightarrow> bool" 

148 
shows 

149 
"(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i. P x i)" 

150 
"(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i. P x i)" 

151 
by (auto intro!: sets.sets_Collect_countable_All sets.sets_Collect_countable_Ex simp: pred_def) 

152 

153 
lemma pred_intros_countable_bounded[measurable (raw)]: 

154 
fixes X :: "'i :: countable set" 

155 
shows 

156 
"(\<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))" 

157 
"(\<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))" 

158 
"(\<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)" 

159 
"(\<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)" 

160 
by (auto simp: Bex_def Ball_def) 

161 

162 
lemma pred_intros_finite[measurable (raw)]: 

163 
"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))" 

164 
"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))" 

165 
"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)" 

166 
"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)" 

167 
by (auto intro!: sets.sets_Collect_finite_Ex sets.sets_Collect_finite_All simp: iff_conv_conj_imp pred_def) 

168 

169 
lemma countable_Un_Int[measurable (raw)]: 

170 
"(\<And>i :: 'i :: countable. i \<in> I \<Longrightarrow> N i \<in> sets M) \<Longrightarrow> (\<Union>i\<in>I. N i) \<in> sets M" 

171 
"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" 

172 
by auto 

173 

174 
declare 

175 
finite_UN[measurable (raw)] 

176 
finite_INT[measurable (raw)] 

177 

178 
lemma sets_Int_pred[measurable (raw)]: 

179 
assumes space: "A \<inter> B \<subseteq> space M" and [measurable]: "pred M (\<lambda>x. x \<in> A)" "pred M (\<lambda>x. x \<in> B)" 

180 
shows "A \<inter> B \<in> sets M" 

181 
proof  

182 
have "{x\<in>space M. x \<in> A \<inter> B} \<in> sets M" by auto 

183 
also have "{x\<in>space M. x \<in> A \<inter> B} = A \<inter> B" 

184 
using space by auto 

185 
finally show ?thesis . 

186 
qed 

187 

188 
lemma [measurable (raw generic)]: 

189 
assumes f: "f \<in> measurable M N" and c: "c \<in> space N \<Longrightarrow> {c} \<in> sets N" 

190 
shows pred_eq_const1: "pred M (\<lambda>x. f x = c)" 

191 
and pred_eq_const2: "pred M (\<lambda>x. c = f x)" 

192 
proof  

193 
show "pred M (\<lambda>x. f x = c)" 

194 
proof cases 

195 
assume "c \<in> space N" 

196 
with measurable_sets[OF f c] show ?thesis 

197 
by (auto simp: Int_def conj_commute pred_def) 

198 
next 

199 
assume "c \<notin> space N" 

200 
with f[THEN measurable_space] have "{x \<in> space M. f x = c} = {}" by auto 

201 
then show ?thesis by (auto simp: pred_def cong: conj_cong) 

202 
qed 

203 
then show "pred M (\<lambda>x. c = f x)" 

204 
by (simp add: eq_commute) 

205 
qed 

206 

59000  207 
lemma pred_count_space_const1[measurable (raw)]: 
208 
"f \<in> measurable M (count_space UNIV) \<Longrightarrow> Measurable.pred M (\<lambda>x. f x = c)" 

209 
by (intro pred_eq_const1[where N="count_space UNIV"]) (auto ) 

210 

211 
lemma pred_count_space_const2[measurable (raw)]: 

212 
"f \<in> measurable M (count_space UNIV) \<Longrightarrow> Measurable.pred M (\<lambda>x. c = f x)" 

213 
by (intro pred_eq_const2[where N="count_space UNIV"]) (auto ) 

214 

50387  215 
lemma pred_le_const[measurable (raw generic)]: 
216 
assumes f: "f \<in> measurable M N" and c: "{.. c} \<in> sets N" shows "pred M (\<lambda>x. f x \<le> c)" 

217 
using measurable_sets[OF f c] 

218 
by (auto simp: Int_def conj_commute eq_commute pred_def) 

219 

220 
lemma pred_const_le[measurable (raw generic)]: 

221 
assumes f: "f \<in> measurable M N" and c: "{c ..} \<in> sets N" shows "pred M (\<lambda>x. c \<le> f x)" 

222 
using measurable_sets[OF f c] 

223 
by (auto simp: Int_def conj_commute eq_commute pred_def) 

224 

225 
lemma pred_less_const[measurable (raw generic)]: 

226 
assumes f: "f \<in> measurable M N" and c: "{..< c} \<in> sets N" shows "pred M (\<lambda>x. f x < c)" 

227 
using measurable_sets[OF f c] 

228 
by (auto simp: Int_def conj_commute eq_commute pred_def) 

229 

230 
lemma pred_const_less[measurable (raw generic)]: 

231 
assumes f: "f \<in> measurable M N" and c: "{c <..} \<in> sets N" shows "pred M (\<lambda>x. c < f x)" 

232 
using measurable_sets[OF f c] 

233 
by (auto simp: Int_def conj_commute eq_commute pred_def) 

234 

235 
declare 

236 
sets.Int[measurable (raw)] 

237 

238 
lemma pred_in_If[measurable (raw)]: 

239 
"(P \<Longrightarrow> pred M (\<lambda>x. x \<in> A x)) \<Longrightarrow> (\<not> P \<Longrightarrow> pred M (\<lambda>x. x \<in> B x)) \<Longrightarrow> 

240 
pred M (\<lambda>x. x \<in> (if P then A x else B x))" 

241 
by auto 

242 

243 
lemma sets_range[measurable_dest]: 

244 
"A ` I \<subseteq> sets M \<Longrightarrow> i \<in> I \<Longrightarrow> A i \<in> sets M" 

245 
by auto 

246 

247 
lemma pred_sets_range[measurable_dest]: 

248 
"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)" 

249 
using pred_sets2[OF sets_range] by auto 

250 

251 
lemma sets_All[measurable_dest]: 

252 
"\<forall>i. A i \<in> sets (M i) \<Longrightarrow> A i \<in> sets (M i)" 

253 
by auto 

254 

255 
lemma pred_sets_All[measurable_dest]: 

256 
"\<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)" 

257 
using pred_sets2[OF sets_All, of A N f] by auto 

258 

259 
lemma sets_Ball[measurable_dest]: 

260 
"\<forall>i\<in>I. A i \<in> sets (M i) \<Longrightarrow> i\<in>I \<Longrightarrow> A i \<in> sets (M i)" 

261 
by auto 

262 

263 
lemma pred_sets_Ball[measurable_dest]: 

264 
"\<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)" 

265 
using pred_sets2[OF sets_Ball, of _ _ _ f] by auto 

266 

267 
lemma measurable_finite[measurable (raw)]: 

268 
fixes S :: "'a \<Rightarrow> nat set" 

269 
assumes [measurable]: "\<And>i. {x\<in>space M. i \<in> S x} \<in> sets M" 

270 
shows "pred M (\<lambda>x. finite (S x))" 

271 
unfolding finite_nat_set_iff_bounded by (simp add: Ball_def) 

272 

273 
lemma measurable_Least[measurable]: 

274 
assumes [measurable]: "(\<And>i::nat. (\<lambda>x. P i x) \<in> measurable M (count_space UNIV))"q 

275 
shows "(\<lambda>x. LEAST i. P i x) \<in> measurable M (count_space UNIV)" 

276 
unfolding measurable_def by (safe intro!: sets_Least) simp_all 

277 

56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

278 
lemma measurable_Max_nat[measurable (raw)]: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

279 
fixes P :: "nat \<Rightarrow> 'a \<Rightarrow> bool" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

280 
assumes [measurable]: "\<And>i. Measurable.pred M (P i)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

281 
shows "(\<lambda>x. Max {i. P i x}) \<in> measurable M (count_space UNIV)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

282 
unfolding measurable_count_space_eq2_countable 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

283 
proof safe 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

284 
fix n 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

285 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

286 
{ fix x assume "\<forall>i. \<exists>n\<ge>i. P n x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

287 
then have "infinite {i. P i x}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

288 
unfolding infinite_nat_iff_unbounded_le by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

289 
then have "Max {i. P i x} = the None" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

290 
by (rule Max.infinite) } 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

291 
note 1 = this 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

292 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

293 
{ fix x i j assume "P i x" "\<forall>n\<ge>j. \<not> P n x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

294 
then have "finite {i. P i x}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

295 
by (auto simp: subset_eq not_le[symmetric] finite_nat_iff_bounded) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

296 
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 realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

297 
using Max_in[of "{i. P i x}"] by auto } 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

298 
note 2 = this 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

299 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

300 
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 realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

301 
by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

302 
also have "\<dots> = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

303 
{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 realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

304 
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 realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

305 
else Max {} = n}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

306 
by (intro arg_cong[where f=Collect] ext conj_cong) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

307 
(auto simp add: 1 2 not_le[symmetric] intro!: Max_eqI) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

308 
also have "\<dots> \<in> sets M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

309 
by measurable 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

310 
finally show "(\<lambda>x. Max {i. P i x}) ` {n} \<inter> space M \<in> sets M" . 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

311 
qed simp 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

312 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

313 
lemma measurable_Min_nat[measurable (raw)]: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

314 
fixes P :: "nat \<Rightarrow> 'a \<Rightarrow> bool" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

315 
assumes [measurable]: "\<And>i. Measurable.pred M (P i)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

316 
shows "(\<lambda>x. Min {i. P i x}) \<in> measurable M (count_space UNIV)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

317 
unfolding measurable_count_space_eq2_countable 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

318 
proof safe 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

319 
fix n 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

320 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

321 
{ fix x assume "\<forall>i. \<exists>n\<ge>i. P n x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

322 
then have "infinite {i. P i x}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

323 
unfolding infinite_nat_iff_unbounded_le by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

324 
then have "Min {i. P i x} = the None" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

325 
by (rule Min.infinite) } 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

326 
note 1 = this 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

327 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

328 
{ fix x i j assume "P i x" "\<forall>n\<ge>j. \<not> P n x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

329 
then have "finite {i. P i x}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

330 
by (auto simp: subset_eq not_le[symmetric] finite_nat_iff_bounded) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

331 
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 realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

332 
using Min_in[of "{i. P i x}"] by auto } 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

333 
note 2 = this 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

334 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

335 
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 realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

336 
by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

337 
also have "\<dots> = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

338 
{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 realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

339 
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 realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

340 
else Min {} = n}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

341 
by (intro arg_cong[where f=Collect] ext conj_cong) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

342 
(auto simp add: 1 2 not_le[symmetric] intro!: Min_eqI) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

343 
also have "\<dots> \<in> sets M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

344 
by measurable 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

345 
finally show "(\<lambda>x. Min {i. P i x}) ` {n} \<inter> space M \<in> sets M" . 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

346 
qed simp 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56045
diff
changeset

347 

50387  348 
lemma measurable_count_space_insert[measurable (raw)]: 
349 
"s \<in> S \<Longrightarrow> A \<in> sets (count_space S) \<Longrightarrow> insert s A \<in> sets (count_space S)" 

350 
by simp 

351 

59000  352 
lemma sets_UNIV [measurable (raw)]: "A \<in> sets (count_space UNIV)" 
353 
by simp 

354 

57025  355 
lemma measurable_card[measurable]: 
356 
fixes S :: "'a \<Rightarrow> nat set" 

357 
assumes [measurable]: "\<And>i. {x\<in>space M. i \<in> S x} \<in> sets M" 

358 
shows "(\<lambda>x. card (S x)) \<in> measurable M (count_space UNIV)" 

359 
unfolding measurable_count_space_eq2_countable 

360 
proof safe 

361 
fix n show "(\<lambda>x. card (S x)) ` {n} \<inter> space M \<in> sets M" 

362 
proof (cases n) 

363 
case 0 

364 
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)}" 

365 
by auto 

366 
also have "\<dots> \<in> sets M" 

367 
by measurable 

368 
finally show ?thesis . 

369 
next 

370 
case (Suc i) 

371 
then have "(\<lambda>x. card (S x)) ` {n} \<inter> space M = 

372 
(\<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)})" 

373 
unfolding set_eq_iff[symmetric] Collect_bex_eq[symmetric] by (auto intro: card_ge_0_finite) 

374 
also have "\<dots> \<in> sets M" 

375 
by (intro sets.countable_UN' countable_Collect countable_Collect_finite) auto 

376 
finally show ?thesis . 

377 
qed 

378 
qed rule 

379 

59088
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

380 
lemma measurable_pred_countable[measurable (raw)]: 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

381 
assumes "countable X" 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

382 
shows 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

383 
"(\<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 sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

384 
"(\<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 sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

385 
unfolding pred_def 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

386 
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 sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

387 

56021
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset

388 
subsection {* Measurability for (co)inductive predicates *} 
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset

389 

59088
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

390 
lemma measurable_bot[measurable]: "bot \<in> measurable M (count_space UNIV)" 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

391 
by (simp add: bot_fun_def) 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

392 

ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

393 
lemma measurable_top[measurable]: "top \<in> measurable M (count_space UNIV)" 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

394 
by (simp add: top_fun_def) 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

395 

ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

396 
lemma measurable_SUP[measurable]: 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

397 
fixes F :: "'i \<Rightarrow> 'a \<Rightarrow> 'b::{complete_lattice, countable}" 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

398 
assumes [simp]: "countable I" 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

399 
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 sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

400 
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 sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

401 
unfolding measurable_count_space_eq2_countable 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

402 
proof (safe intro!: UNIV_I) 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

403 
fix a 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

404 
have "(\<lambda>x. SUP i:I. F i x) ` {a} \<inter> space M = 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

405 
{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 sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

406 
unfolding SUP_le_iff[symmetric] by auto 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

407 
also have "\<dots> \<in> sets M" 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

408 
by measurable 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

409 
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 sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

410 
qed 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

411 

ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

412 
lemma measurable_INF[measurable]: 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

413 
fixes F :: "'i \<Rightarrow> 'a \<Rightarrow> 'b::{complete_lattice, countable}" 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

414 
assumes [simp]: "countable I" 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

415 
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 sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

416 
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 sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

417 
unfolding measurable_count_space_eq2_countable 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

418 
proof (safe intro!: UNIV_I) 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

419 
fix a 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

420 
have "(\<lambda>x. INF i:I. F i x) ` {a} \<inter> space M = 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

421 
{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 sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

422 
unfolding le_INF_iff[symmetric] by auto 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

423 
also have "\<dots> \<in> sets M" 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

424 
by measurable 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

425 
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 sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

426 
qed 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

427 

ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

428 
lemma measurable_lfp_coinduct[consumes 1, case_names continuity step]: 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

429 
fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})" 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

430 
assumes "P M" 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

431 
assumes F: "Order_Continuity.continuous F" 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

432 
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 sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

433 
shows "lfp F \<in> measurable M (count_space UNIV)" 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

434 
proof  
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

435 
{ 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 sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

436 
by (induct i arbitrary: M) (auto intro!: *) } 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

437 
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 sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

438 
by measurable 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

439 
also have "(\<lambda>x. SUP i. (F ^^ i) bot x) = lfp F" 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

440 
by (subst continuous_lfp) (auto intro: F) 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

441 
finally show ?thesis . 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

442 
qed 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

443 

56021
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset

444 
lemma measurable_lfp: 
59088
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

445 
fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})" 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

446 
assumes F: "Order_Continuity.continuous F" 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

447 
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 sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

448 
shows "lfp F \<in> measurable M (count_space UNIV)" 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

449 
by (coinduction rule: measurable_lfp_coinduct[OF _ F]) (blast intro: *) 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

450 

ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

451 
lemma measurable_gfp_coinduct[consumes 1, case_names continuity step]: 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

452 
fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})" 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

453 
assumes "P M" 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

454 
assumes F: "Order_Continuity.down_continuous F" 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

455 
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 sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

456 
shows "gfp F \<in> measurable M (count_space UNIV)" 
56021
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset

457 
proof  
59088
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

458 
{ 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 sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

459 
by (induct i arbitrary: M) (auto intro!: *) } 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

460 
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

461 
by measurable 
59088
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

462 
also have "(\<lambda>x. INF i. (F ^^ i) top x) = gfp F" 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

463 
by (subst down_continuous_gfp) (auto intro: F) 
56021
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset

464 
finally show ?thesis . 
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset

465 
qed 
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset

466 

e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset

467 
lemma measurable_gfp: 
59088
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

468 
fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})" 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

469 
assumes F: "Order_Continuity.down_continuous F" 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

470 
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 sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

471 
shows "gfp F \<in> measurable M (count_space UNIV)" 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

472 
by (coinduction rule: measurable_gfp_coinduct[OF _ F]) (blast intro: *) 
59000  473 

474 
lemma measurable_lfp2_coinduct[consumes 1, case_names continuity step]: 

59088
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

475 
fixes F :: "('a \<Rightarrow> 'c \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'c \<Rightarrow> 'b::{complete_lattice, countable})" 
59000  476 
assumes "P M s" 
59088
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

477 
assumes F: "Order_Continuity.continuous F" 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

478 
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 sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

479 
shows "lfp F s \<in> measurable M (count_space UNIV)" 
59000  480 
proof  
59088
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

481 
{ fix i from `P M s` have "(\<lambda>x. (F ^^ i) bot s x) \<in> measurable M (count_space UNIV)" 
59000  482 
by (induct i arbitrary: M s) (auto intro!: *) } 
59088
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

483 
then have "(\<lambda>x. SUP i. (F ^^ i) bot s x) \<in> measurable M (count_space UNIV)" 
59000  484 
by measurable 
59088
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

485 
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 sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

486 
by (subst continuous_lfp) (auto simp: F) 
59000  487 
finally show ?thesis . 
488 
qed 

489 

490 
lemma measurable_gfp2_coinduct[consumes 1, case_names continuity step]: 

59088
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

491 
fixes F :: "('a \<Rightarrow> 'c \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'c \<Rightarrow> 'b::{complete_lattice, countable})" 
59000  492 
assumes "P M s" 
59088
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

493 
assumes F: "Order_Continuity.down_continuous F" 
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

494 
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 sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

495 
shows "gfp F s \<in> measurable M (count_space UNIV)" 
59000  496 
proof  
59088
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

497 
{ fix i from `P M s` have "(\<lambda>x. (F ^^ i) top s x) \<in> measurable M (count_space UNIV)" 
59000  498 
by (induct i arbitrary: M s) (auto intro!: *) } 
59088
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

499 
then have "(\<lambda>x. INF i. (F ^^ i) top s x) \<in> measurable M (count_space UNIV)" 
59000  500 
by measurable 
59088
ff2bd4a14ddb
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

501 
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 sigmaclosure of product spaces
hoelzl
parents:
59048
diff
changeset

502 
by (subst down_continuous_gfp) (auto simp: F) 
59000  503 
finally show ?thesis . 
504 
qed 

505 

506 
lemma measurable_enat_coinduct: 

507 
fixes f :: "'a \<Rightarrow> enat" 

508 
assumes "R f" 

509 
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> 

510 
Measurable.pred M P \<and> 

511 
i \<in> measurable M M \<and> 

512 
h \<in> measurable M (count_space UNIV)" 

513 
shows "f \<in> measurable M (count_space UNIV)" 

514 
proof (simp add: measurable_count_space_eq2_countable, rule ) 

515 
fix a :: enat 

516 
have "f ` {a} \<inter> space M = {x\<in>space M. f x = a}" 

517 
by auto 

518 
{ fix i :: nat 

519 
from `R f` have "Measurable.pred M (\<lambda>x. f x = enat i)" 

520 
proof (induction i arbitrary: f) 

521 
case 0 

522 
from *[OF this] obtain g h i P 

523 
where f: "f = (\<lambda>x. if P x then h x else eSuc (g (i x)))" and 

524 
[measurable]: "Measurable.pred M P" "i \<in> measurable M M" "h \<in> measurable M (count_space UNIV)" 

525 
by auto 

526 
have "Measurable.pred M (\<lambda>x. P x \<and> h x = 0)" 

527 
by measurable 

528 
also have "(\<lambda>x. P x \<and> h x = 0) = (\<lambda>x. f x = enat 0)" 

529 
by (auto simp: f zero_enat_def[symmetric]) 

530 
finally show ?case . 

531 
next 

532 
case (Suc n) 

533 
from *[OF Suc.prems] obtain g h i P 

534 
where f: "f = (\<lambda>x. if P x then h x else eSuc (g (i x)))" and "R g" and 

535 
M[measurable]: "Measurable.pred M P" "i \<in> measurable M M" "h \<in> measurable M (count_space UNIV)" 

536 
by auto 

537 
have "(\<lambda>x. f x = enat (Suc n)) = 

538 
(\<lambda>x. (P x \<longrightarrow> h x = enat (Suc n)) \<and> (\<not> P x \<longrightarrow> g (i x) = enat n))" 

539 
by (auto simp: f zero_enat_def[symmetric] eSuc_enat[symmetric]) 

540 
also have "Measurable.pred M \<dots>" 

541 
by (intro pred_intros_logic measurable_compose[OF M(2)] Suc `R g`) measurable 

542 
finally show ?case . 

543 
qed 

544 
then have "f ` {enat i} \<inter> space M \<in> sets M" 

545 
by (simp add: pred_def Int_def conj_commute) } 

546 
note fin = this 

547 
show "f ` {a} \<inter> space M \<in> sets M" 

548 
proof (cases a) 

549 
case infinity 

550 
then have "f ` {a} \<inter> space M = space M  (\<Union>n. f ` {enat n} \<inter> space M)" 

551 
by auto 

552 
also have "\<dots> \<in> sets M" 

553 
by (intro sets.Diff sets.top sets.Un sets.countable_UN) (auto intro!: fin) 

554 
finally show ?thesis . 

555 
qed (simp add: fin) 

556 
qed 

557 

558 
lemma measurable_THE: 

559 
fixes P :: "'a \<Rightarrow> 'b \<Rightarrow> bool" 

560 
assumes [measurable]: "\<And>i. Measurable.pred M (P i)" 

561 
assumes I[simp]: "countable I" "\<And>i x. x \<in> space M \<Longrightarrow> P i x \<Longrightarrow> i \<in> I" 

562 
assumes unique: "\<And>x i j. x \<in> space M \<Longrightarrow> P i x \<Longrightarrow> P j x \<Longrightarrow> i = j" 

563 
shows "(\<lambda>x. THE i. P i x) \<in> measurable M (count_space UNIV)" 

564 
unfolding measurable_def 

565 
proof safe 

566 
fix X 

567 
def f \<equiv> "\<lambda>x. THE i. P i x" def undef \<equiv> "THE i::'a. False" 

568 
{ fix i x assume "x \<in> space M" "P i x" then have "f x = i" 

569 
unfolding f_def using unique by auto } 

570 
note f_eq = this 

571 
{ fix x assume "x \<in> space M" "\<forall>i\<in>I. \<not> P i x" 

572 
then have "\<And>i. \<not> P i x" 

573 
using I(2)[of x] by auto 

574 
then have "f x = undef" 

575 
by (auto simp: undef_def f_def) } 

576 
then have "f ` X \<inter> space M = (\<Union>i\<in>I \<inter> X. {x\<in>space M. P i x}) \<union> 

577 
(if undef \<in> X then space M  (\<Union>i\<in>I. {x\<in>space M. P i x}) else {})" 

578 
by (auto dest: f_eq) 

579 
also have "\<dots> \<in> sets M" 

580 
by (auto intro!: sets.Diff sets.countable_UN') 

581 
finally show "f ` X \<inter> space M \<in> sets M" . 

582 
qed simp 

583 

584 
lemma measurable_Ex1[measurable (raw)]: 

585 
assumes [simp]: "countable I" and [measurable]: "\<And>i. i \<in> I \<Longrightarrow> Measurable.pred M (P i)" 

586 
shows "Measurable.pred M (\<lambda>x. \<exists>!i\<in>I. P i x)" 

587 
unfolding bex1_def by measurable 

588 

589 
lemma measurable_split_if[measurable (raw)]: 

590 
"(c \<Longrightarrow> Measurable.pred M f) \<Longrightarrow> (\<not> c \<Longrightarrow> Measurable.pred M g) \<Longrightarrow> 

591 
Measurable.pred M (if c then f else g)" 

592 
by simp 

593 

594 
lemma pred_restrict_space: 

595 
assumes "S \<in> sets M" 

596 
shows "Measurable.pred (restrict_space M S) P \<longleftrightarrow> Measurable.pred M (\<lambda>x. x \<in> S \<and> P x)" 

597 
unfolding pred_def sets_Collect_restrict_space_iff[OF assms] .. 

598 

599 
lemma measurable_predpow[measurable]: 

600 
assumes "Measurable.pred M T" 

601 
assumes "\<And>Q. Measurable.pred M Q \<Longrightarrow> Measurable.pred M (R Q)" 

602 
shows "Measurable.pred M ((R ^^ n) T)" 

603 
by (induct n) (auto intro: assms) 

604 

50387  605 
hide_const (open) pred 
606 

607 
end 

59048  608 