author  hoelzl 
Wed, 08 Dec 2010 16:15:14 +0100  
changeset 41096  843c40bbc379 
parent 41083  c987429a1298 
child 41097  a1abfa4e2b44 
permissions  rwrr 
38656  1 
(* Author: Armin Heller, Johannes Hoelzl, TU Muenchen *) 
2 

3 
header {*Borel spaces*} 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

4 

40859  5 
theory Borel_Space 
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40870
diff
changeset

6 
imports Sigma_Algebra Positive_Extended_Real Multivariate_Analysis 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

7 
begin 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

8 

39092  9 
lemma LIMSEQ_max: 
10 
"u > (x::real) \<Longrightarrow> (\<lambda>i. max (u i) 0) > max x 0" 

11 
by (fastsimp intro!: LIMSEQ_I dest!: LIMSEQ_D) 

12 

38656  13 
section "Generic Borel spaces" 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

14 

40859  15 
definition "borel = sigma \<lparr> space = UNIV::'a::topological_space set, sets = open\<rparr>" 
16 
abbreviation "borel_measurable M \<equiv> measurable M borel" 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

17 

40859  18 
interpretation borel: sigma_algebra borel 
19 
by (auto simp: borel_def intro!: sigma_algebra_sigma) 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

20 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

21 
lemma in_borel_measurable: 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

22 
"f \<in> borel_measurable M \<longleftrightarrow> 
40859  23 
(\<forall>S \<in> sets (sigma \<lparr> space = UNIV, sets = open\<rparr>). 
38656  24 
f ` S \<inter> space M \<in> sets M)" 
40859  25 
by (auto simp add: measurable_def borel_def) 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

26 

40859  27 
lemma in_borel_measurable_borel: 
38656  28 
"f \<in> borel_measurable M \<longleftrightarrow> 
40859  29 
(\<forall>S \<in> sets borel. 
38656  30 
f ` S \<inter> space M \<in> sets M)" 
40859  31 
by (auto simp add: measurable_def borel_def) 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

32 

40859  33 
lemma space_borel[simp]: "space borel = UNIV" 
34 
unfolding borel_def by auto 

38656  35 

40859  36 
lemma borel_open[simp]: 
37 
assumes "open A" shows "A \<in> sets borel" 

38656  38 
proof  
39 
have "A \<in> open" unfolding mem_def using assms . 

40859  40 
thus ?thesis unfolding borel_def sigma_def by (auto intro!: sigma_sets.Basic) 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

41 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

42 

40859  43 
lemma borel_closed[simp]: 
44 
assumes "closed A" shows "A \<in> sets borel" 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

45 
proof  
40859  46 
have "space borel  ( A) \<in> sets borel" 
47 
using assms unfolding closed_def by (blast intro: borel_open) 

38656  48 
thus ?thesis by simp 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

49 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

50 

38656  51 
lemma (in sigma_algebra) borel_measurable_vimage: 
52 
fixes f :: "'a \<Rightarrow> 'x::t2_space" 

53 
assumes borel: "f \<in> borel_measurable M" 

54 
shows "f ` {x} \<inter> space M \<in> sets M" 

55 
proof (cases "x \<in> f ` space M") 

56 
case True then obtain y where "x = f y" by auto 

57 
from closed_sing[of "f y"] 

40859  58 
have "{f y} \<in> sets borel" by (rule borel_closed) 
38656  59 
with assms show ?thesis 
40859  60 
unfolding in_borel_measurable_borel `x = f y` by auto 
38656  61 
next 
62 
case False hence "f ` {x} \<inter> space M = {}" by auto 

63 
thus ?thesis by auto 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

64 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

65 

38656  66 
lemma (in sigma_algebra) borel_measurableI: 
67 
fixes f :: "'a \<Rightarrow> 'x\<Colon>topological_space" 

68 
assumes "\<And>S. open S \<Longrightarrow> f ` S \<inter> space M \<in> sets M" 

69 
shows "f \<in> borel_measurable M" 

40859  70 
unfolding borel_def 
71 
proof (rule measurable_sigma, simp_all) 

38656  72 
fix S :: "'x set" assume "S \<in> open" thus "f ` S \<inter> space M \<in> sets M" 
73 
using assms[of S] by (simp add: mem_def) 

40859  74 
qed 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

75 

40859  76 
lemma borel_singleton[simp, intro]: 
38656  77 
fixes x :: "'a::t1_space" 
40859  78 
shows "A \<in> sets borel \<Longrightarrow> insert x A \<in> sets borel" 
79 
proof (rule borel.insert_in_sets) 

80 
show "{x} \<in> sets borel" 

81 
using closed_sing[of x] by (rule borel_closed) 

38656  82 
qed simp 
83 

84 
lemma (in sigma_algebra) borel_measurable_const[simp, intro]: 

85 
"(\<lambda>x. c) \<in> borel_measurable M" 

86 
by (auto intro!: measurable_const) 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

87 

39083  88 
lemma (in sigma_algebra) borel_measurable_indicator[simp, intro!]: 
38656  89 
assumes A: "A \<in> sets M" 
90 
shows "indicator A \<in> borel_measurable M" 

91 
unfolding indicator_def_raw using A 

92 
by (auto intro!: measurable_If_set borel_measurable_const) 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

93 

40859  94 
lemma (in sigma_algebra) borel_measurable_indicator_iff: 
95 
"(indicator A :: 'a \<Rightarrow> 'x::{t1_space, zero_neq_one}) \<in> borel_measurable M \<longleftrightarrow> A \<inter> space M \<in> sets M" 

96 
(is "?I \<in> borel_measurable M \<longleftrightarrow> _") 

97 
proof 

98 
assume "?I \<in> borel_measurable M" 

99 
then have "?I ` {1} \<inter> space M \<in> sets M" 

100 
unfolding measurable_def by auto 

101 
also have "?I ` {1} \<inter> space M = A \<inter> space M" 

102 
unfolding indicator_def_raw by auto 

103 
finally show "A \<inter> space M \<in> sets M" . 

104 
next 

105 
assume "A \<inter> space M \<in> sets M" 

106 
moreover have "?I \<in> borel_measurable M \<longleftrightarrow> 

107 
(indicator (A \<inter> space M) :: 'a \<Rightarrow> 'x) \<in> borel_measurable M" 

108 
by (intro measurable_cong) (auto simp: indicator_def) 

109 
ultimately show "?I \<in> borel_measurable M" by auto 

110 
qed 

111 

38656  112 
lemma borel_measurable_translate: 
40859  113 
assumes "A \<in> sets borel" and trans: "\<And>B. open B \<Longrightarrow> f ` B \<in> sets borel" 
114 
shows "f ` A \<in> sets borel" 

38656  115 
proof  
116 
have "A \<in> sigma_sets UNIV open" using assms 

40859  117 
by (simp add: borel_def sigma_def) 
38656  118 
thus ?thesis 
119 
proof (induct rule: sigma_sets.induct) 

120 
case (Basic a) thus ?case using trans[of a] by (simp add: mem_def) 

121 
next 

122 
case (Compl a) 

40859  123 
moreover have "UNIV \<in> sets borel" 
124 
using borel.top by simp 

38656  125 
ultimately show ?case 
40859  126 
by (auto simp: vimage_Diff borel.Diff) 
38656  127 
qed (auto simp add: vimage_UN) 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

128 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

129 

39092  130 
lemma (in sigma_algebra) borel_measurable_restricted: 
131 
fixes f :: "'a \<Rightarrow> 'x\<Colon>{topological_space, semiring_1}" assumes "A \<in> sets M" 

132 
shows "f \<in> borel_measurable (restricted_space A) \<longleftrightarrow> 

133 
(\<lambda>x. f x * indicator A x) \<in> borel_measurable M" 

134 
(is "f \<in> borel_measurable ?R \<longleftrightarrow> ?f \<in> borel_measurable M") 

135 
proof  

136 
interpret R: sigma_algebra ?R by (rule restricted_sigma_algebra[OF `A \<in> sets M`]) 

137 
have *: "f \<in> borel_measurable ?R \<longleftrightarrow> ?f \<in> borel_measurable ?R" 

138 
by (auto intro!: measurable_cong) 

139 
show ?thesis unfolding * 

40859  140 
unfolding in_borel_measurable_borel 
39092  141 
proof (simp, safe) 
40859  142 
fix S :: "'x set" assume "S \<in> sets borel" 
143 
"\<forall>S\<in>sets borel. ?f ` S \<inter> A \<in> op \<inter> A ` sets M" 

39092  144 
then have "?f ` S \<inter> A \<in> op \<inter> A ` sets M" by auto 
145 
then have f: "?f ` S \<inter> A \<in> sets M" 

146 
using `A \<in> sets M` sets_into_space by fastsimp 

147 
show "?f ` S \<inter> space M \<in> sets M" 

148 
proof cases 

149 
assume "0 \<in> S" 

150 
then have "?f ` S \<inter> space M = ?f ` S \<inter> A \<union> (space M  A)" 

151 
using `A \<in> sets M` sets_into_space by auto 

152 
then show ?thesis using f `A \<in> sets M` by (auto intro!: Un Diff) 

153 
next 

154 
assume "0 \<notin> S" 

155 
then have "?f ` S \<inter> space M = ?f ` S \<inter> A" 

156 
using `A \<in> sets M` sets_into_space 

157 
by (auto simp: indicator_def split: split_if_asm) 

158 
then show ?thesis using f by auto 

159 
qed 

160 
next 

40859  161 
fix S :: "'x set" assume "S \<in> sets borel" 
162 
"\<forall>S\<in>sets borel. ?f ` S \<inter> space M \<in> sets M" 

39092  163 
then have f: "?f ` S \<inter> space M \<in> sets M" by auto 
164 
then show "?f ` S \<inter> A \<in> op \<inter> A ` sets M" 

165 
using `A \<in> sets M` sets_into_space 

166 
apply (simp add: image_iff) 

167 
apply (rule bexI[OF _ f]) 

168 
by auto 

169 
qed 

170 
qed 

171 

172 
lemma (in sigma_algebra) borel_measurable_subalgebra: 

173 
assumes "N \<subseteq> sets M" "f \<in> borel_measurable (M\<lparr>sets:=N\<rparr>)" 

174 
shows "f \<in> borel_measurable M" 

175 
using assms unfolding measurable_def by auto 

176 

38656  177 
section "Borel spaces on euclidean spaces" 
178 

179 
lemma lessThan_borel[simp, intro]: 

180 
fixes a :: "'a\<Colon>ordered_euclidean_space" 

40859  181 
shows "{..< a} \<in> sets borel" 
182 
by (blast intro: borel_open) 

38656  183 

184 
lemma greaterThan_borel[simp, intro]: 

185 
fixes a :: "'a\<Colon>ordered_euclidean_space" 

40859  186 
shows "{a <..} \<in> sets borel" 
187 
by (blast intro: borel_open) 

38656  188 

189 
lemma greaterThanLessThan_borel[simp, intro]: 

190 
fixes a b :: "'a\<Colon>ordered_euclidean_space" 

40859  191 
shows "{a<..<b} \<in> sets borel" 
192 
by (blast intro: borel_open) 

38656  193 

194 
lemma atMost_borel[simp, intro]: 

195 
fixes a :: "'a\<Colon>ordered_euclidean_space" 

40859  196 
shows "{..a} \<in> sets borel" 
197 
by (blast intro: borel_closed) 

38656  198 

199 
lemma atLeast_borel[simp, intro]: 

200 
fixes a :: "'a\<Colon>ordered_euclidean_space" 

40859  201 
shows "{a..} \<in> sets borel" 
202 
by (blast intro: borel_closed) 

38656  203 

204 
lemma atLeastAtMost_borel[simp, intro]: 

205 
fixes a b :: "'a\<Colon>ordered_euclidean_space" 

40859  206 
shows "{a..b} \<in> sets borel" 
207 
by (blast intro: borel_closed) 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

208 

38656  209 
lemma greaterThanAtMost_borel[simp, intro]: 
210 
fixes a b :: "'a\<Colon>ordered_euclidean_space" 

40859  211 
shows "{a<..b} \<in> sets borel" 
38656  212 
unfolding greaterThanAtMost_def by blast 
213 

214 
lemma atLeastLessThan_borel[simp, intro]: 

215 
fixes a b :: "'a\<Colon>ordered_euclidean_space" 

40859  216 
shows "{a..<b} \<in> sets borel" 
38656  217 
unfolding atLeastLessThan_def by blast 
218 

219 
lemma hafspace_less_borel[simp, intro]: 

220 
fixes a :: real 

40859  221 
shows "{x::'a::euclidean_space. a < x $$ i} \<in> sets borel" 
222 
by (auto intro!: borel_open open_halfspace_component_gt) 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

223 

38656  224 
lemma hafspace_greater_borel[simp, intro]: 
225 
fixes a :: real 

40859  226 
shows "{x::'a::euclidean_space. x $$ i < a} \<in> sets borel" 
227 
by (auto intro!: borel_open open_halfspace_component_lt) 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

228 

38656  229 
lemma hafspace_less_eq_borel[simp, intro]: 
230 
fixes a :: real 

40859  231 
shows "{x::'a::euclidean_space. a \<le> x $$ i} \<in> sets borel" 
232 
by (auto intro!: borel_closed closed_halfspace_component_ge) 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

233 

38656  234 
lemma hafspace_greater_eq_borel[simp, intro]: 
235 
fixes a :: real 

40859  236 
shows "{x::'a::euclidean_space. x $$ i \<le> a} \<in> sets borel" 
237 
by (auto intro!: borel_closed closed_halfspace_component_le) 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

238 

38656  239 
lemma (in sigma_algebra) borel_measurable_less[simp, intro]: 
240 
fixes f :: "'a \<Rightarrow> real" 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

241 
assumes f: "f \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

242 
assumes g: "g \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

243 
shows "{w \<in> space M. f w < g w} \<in> sets M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

244 
proof  
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

245 
have "{w \<in> space M. f w < g w} = 
38656  246 
(\<Union>r. (f ` {..< of_rat r} \<inter> space M) \<inter> (g ` {of_rat r <..} \<inter> space M))" 
247 
using Rats_dense_in_real by (auto simp add: Rats_def) 

248 
then show ?thesis using f g 

249 
by simp (blast intro: measurable_sets) 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

250 
qed 
38656  251 

252 
lemma (in sigma_algebra) borel_measurable_le[simp, intro]: 

253 
fixes f :: "'a \<Rightarrow> real" 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

254 
assumes f: "f \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

255 
assumes g: "g \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

256 
shows "{w \<in> space M. f w \<le> g w} \<in> sets M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

257 
proof  
38656  258 
have "{w \<in> space M. f w \<le> g w} = space M  {w \<in> space M. g w < f w}" 
259 
by auto 

260 
thus ?thesis using f g 

261 
by simp blast 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

262 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

263 

38656  264 
lemma (in sigma_algebra) borel_measurable_eq[simp, intro]: 
265 
fixes f :: "'a \<Rightarrow> real" 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

266 
assumes f: "f \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

267 
assumes g: "g \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

268 
shows "{w \<in> space M. f w = g w} \<in> sets M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

269 
proof  
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

270 
have "{w \<in> space M. f w = g w} = 
33536  271 
{w \<in> space M. f w \<le> g w} \<inter> {w \<in> space M. g w \<le> f w}" 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

272 
by auto 
38656  273 
thus ?thesis using f g by auto 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

274 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

275 

38656  276 
lemma (in sigma_algebra) borel_measurable_neq[simp, intro]: 
277 
fixes f :: "'a \<Rightarrow> real" 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

278 
assumes f: "f \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

279 
assumes g: "g \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

280 
shows "{w \<in> space M. f w \<noteq> g w} \<in> sets M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

281 
proof  
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

282 
have "{w \<in> space M. f w \<noteq> g w} = space M  {w \<in> space M. f w = g w}" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

283 
by auto 
38656  284 
thus ?thesis using f g by auto 
285 
qed 

286 

287 
subsection "Borel space equals sigma algebras over intervals" 

288 

289 
lemma rational_boxes: 

290 
fixes x :: "'a\<Colon>ordered_euclidean_space" 

291 
assumes "0 < e" 

292 
shows "\<exists>a b. (\<forall>i. a $$ i \<in> \<rat>) \<and> (\<forall>i. b $$ i \<in> \<rat>) \<and> x \<in> {a <..< b} \<and> {a <..< b} \<subseteq> ball x e" 

293 
proof  

294 
def e' \<equiv> "e / (2 * sqrt (real (DIM ('a))))" 

295 
then have e: "0 < e'" using assms by (auto intro!: divide_pos_pos) 

296 
have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x $$ i \<and> x $$ i  y < e'" (is "\<forall>i. ?th i") 

297 
proof 

298 
fix i from Rats_dense_in_real[of "x $$ i  e'" "x $$ i"] e 

299 
show "?th i" by auto 

300 
qed 

301 
from choice[OF this] guess a .. note a = this 

302 
have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x $$ i < y \<and> y  x $$ i < e'" (is "\<forall>i. ?th i") 

303 
proof 

304 
fix i from Rats_dense_in_real[of "x $$ i" "x $$ i + e'"] e 

305 
show "?th i" by auto 

306 
qed 

307 
from choice[OF this] guess b .. note b = this 

308 
{ fix y :: 'a assume *: "Chi a < y" "y < Chi b" 

309 
have "dist x y = sqrt (\<Sum>i<DIM('a). (dist (x $$ i) (y $$ i))\<twosuperior>)" 

310 
unfolding setL2_def[symmetric] by (rule euclidean_dist_l2) 

311 
also have "\<dots> < sqrt (\<Sum>i<DIM('a). e^2 / real (DIM('a)))" 

312 
proof (rule real_sqrt_less_mono, rule setsum_strict_mono) 

313 
fix i assume i: "i \<in> {..<DIM('a)}" 

314 
have "a i < y$$i \<and> y$$i < b i" using * i eucl_less[where 'a='a] by auto 

315 
moreover have "a i < x$$i" "x$$i  a i < e'" using a by auto 

316 
moreover have "x$$i < b i" "b i  x$$i < e'" using b by auto 

317 
ultimately have "\<bar>x$$i  y$$i\<bar> < 2 * e'" by auto 

318 
then have "dist (x $$ i) (y $$ i) < e/sqrt (real (DIM('a)))" 

319 
unfolding e'_def by (auto simp: dist_real_def) 

320 
then have "(dist (x $$ i) (y $$ i))\<twosuperior> < (e/sqrt (real (DIM('a))))\<twosuperior>" 

321 
by (rule power_strict_mono) auto 

322 
then show "(dist (x $$ i) (y $$ i))\<twosuperior> < e\<twosuperior> / real DIM('a)" 

323 
by (simp add: power_divide) 

324 
qed auto 

325 
also have "\<dots> = e" using `0 < e` by (simp add: real_eq_of_nat DIM_positive) 

326 
finally have "dist x y < e" . } 

327 
with a b show ?thesis 

328 
apply (rule_tac exI[of _ "Chi a"]) 

329 
apply (rule_tac exI[of _ "Chi b"]) 

330 
using eucl_less[where 'a='a] by auto 

331 
qed 

332 

333 
lemma ex_rat_list: 

334 
fixes x :: "'a\<Colon>ordered_euclidean_space" 

335 
assumes "\<And> i. x $$ i \<in> \<rat>" 

336 
shows "\<exists> r. length r = DIM('a) \<and> (\<forall> i < DIM('a). of_rat (r ! i) = x $$ i)" 

337 
proof  

338 
have "\<forall>i. \<exists>r. x $$ i = of_rat r" using assms unfolding Rats_def by blast 

339 
from choice[OF this] guess r .. 

340 
then show ?thesis by (auto intro!: exI[of _ "map r [0 ..< DIM('a)]"]) 

341 
qed 

342 

343 
lemma open_UNION: 

344 
fixes M :: "'a\<Colon>ordered_euclidean_space set" 

345 
assumes "open M" 

346 
shows "M = UNION {(a, b)  a b. {Chi (of_rat \<circ> op ! a) <..< Chi (of_rat \<circ> op ! b)} \<subseteq> M} 

347 
(\<lambda> (a, b). {Chi (of_rat \<circ> op ! a) <..< Chi (of_rat \<circ> op ! b)})" 

348 
(is "M = UNION ?idx ?box") 

349 
proof safe 

350 
fix x assume "x \<in> M" 

351 
obtain e where e: "e > 0" "ball x e \<subseteq> M" 

352 
using openE[OF assms `x \<in> M`] by auto 

353 
then obtain a b where ab: "x \<in> {a <..< b}" "\<And>i. a $$ i \<in> \<rat>" "\<And>i. b $$ i \<in> \<rat>" "{a <..< b} \<subseteq> ball x e" 

354 
using rational_boxes[OF e(1)] by blast 

355 
then obtain p q where pq: "length p = DIM ('a)" 

356 
"length q = DIM ('a)" 

357 
"\<forall> i < DIM ('a). of_rat (p ! i) = a $$ i \<and> of_rat (q ! i) = b $$ i" 

358 
using ex_rat_list[OF ab(2)] ex_rat_list[OF ab(3)] by blast 

359 
hence p: "Chi (of_rat \<circ> op ! p) = a" 

360 
using euclidean_eq[of "Chi (of_rat \<circ> op ! p)" a] 

361 
unfolding o_def by auto 

362 
from pq have q: "Chi (of_rat \<circ> op ! q) = b" 

363 
using euclidean_eq[of "Chi (of_rat \<circ> op ! q)" b] 

364 
unfolding o_def by auto 

365 
have "x \<in> ?box (p, q)" 

366 
using p q ab by auto 

367 
thus "x \<in> UNION ?idx ?box" using ab e p q exI[of _ p] exI[of _ q] by auto 

368 
qed auto 

369 

370 
lemma halfspace_span_open: 

40859  371 
"sigma_sets UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i < a})) 
372 
\<subseteq> sets borel" 

373 
by (auto intro!: borel.sigma_sets_subset[simplified] borel_open 

374 
open_halfspace_component_lt) 

38656  375 

376 
lemma halfspace_lt_in_halfspace: 

40859  377 
"{x\<Colon>'a. x $$ i < a} \<in> sets (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i < a})\<rparr>)" 
378 
by (auto intro!: sigma_sets.Basic simp: sets_sigma) 

38656  379 

380 
lemma halfspace_gt_in_halfspace: 

40859  381 
"{x\<Colon>'a. a < x $$ i} \<in> sets (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i < a})\<rparr>)" 
382 
(is "?set \<in> sets ?SIGMA") 

38656  383 
proof  
40859  384 
interpret sigma_algebra "?SIGMA" 
385 
by (intro sigma_algebra_sigma_sets) (simp_all add: sets_sigma) 

38656  386 
have *: "?set = (\<Union>n. space ?SIGMA  {x\<Colon>'a. x $$ i < a + 1 / real (Suc n)})" 
387 
proof (safe, simp_all add: not_less) 

388 
fix x assume "a < x $$ i" 

389 
with reals_Archimedean[of "x $$ i  a"] 

390 
obtain n where "a + 1 / real (Suc n) < x $$ i" 

391 
by (auto simp: inverse_eq_divide field_simps) 

392 
then show "\<exists>n. a + 1 / real (Suc n) \<le> x $$ i" 

393 
by (blast intro: less_imp_le) 

394 
next 

395 
fix x n 

396 
have "a < a + 1 / real (Suc n)" by auto 

397 
also assume "\<dots> \<le> x" 

398 
finally show "a < x" . 

399 
qed 

400 
show "?set \<in> sets ?SIGMA" unfolding * 

401 
by (safe intro!: countable_UN Diff halfspace_lt_in_halfspace) 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

402 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

403 

38656  404 
lemma open_span_halfspace: 
40859  405 
"sets borel \<subseteq> sets (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. x $$ i < a})\<rparr>)" 
38656  406 
(is "_ \<subseteq> sets ?SIGMA") 
40859  407 
proof  
408 
have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) simp 

38656  409 
then interpret sigma_algebra ?SIGMA . 
40859  410 
{ fix S :: "'a set" assume "S \<in> open" then have "open S" unfolding mem_def . 
411 
from open_UNION[OF this] 

412 
obtain I where *: "S = 

413 
(\<Union>(a, b)\<in>I. 

414 
(\<Inter> i<DIM('a). {x. (Chi (real_of_rat \<circ> op ! a)::'a) $$ i < x $$ i}) \<inter> 

415 
(\<Inter> i<DIM('a). {x. x $$ i < (Chi (real_of_rat \<circ> op ! b)::'a) $$ i}))" 

416 
unfolding greaterThanLessThan_def 

417 
unfolding eucl_greaterThan_eq_halfspaces[where 'a='a] 

418 
unfolding eucl_lessThan_eq_halfspaces[where 'a='a] 

419 
by blast 

420 
have "S \<in> sets ?SIGMA" 

421 
unfolding * 

422 
by (auto intro!: countable_UN Int countable_INT halfspace_lt_in_halfspace halfspace_gt_in_halfspace) } 

423 
then show ?thesis unfolding borel_def 

424 
by (intro sets_sigma_subset) auto 

425 
qed 

38656  426 

427 
lemma halfspace_span_halfspace_le: 

40859  428 
"sets (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i < a})\<rparr>) \<subseteq> 
429 
sets (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x. x $$ i \<le> a})\<rparr>)" 

38656  430 
(is "_ \<subseteq> sets ?SIGMA") 
40859  431 
proof  
432 
have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto 

38656  433 
then interpret sigma_algebra ?SIGMA . 
40859  434 
{ fix a i 
435 
have *: "{x::'a. x$$i < a} = (\<Union>n. {x. x$$i \<le> a  1/real (Suc n)})" 

436 
proof (safe, simp_all) 

437 
fix x::'a assume *: "x$$i < a" 

438 
with reals_Archimedean[of "a  x$$i"] 

439 
obtain n where "x $$ i < a  1 / (real (Suc n))" 

440 
by (auto simp: field_simps inverse_eq_divide) 

441 
then show "\<exists>n. x $$ i \<le> a  1 / (real (Suc n))" 

442 
by (blast intro: less_imp_le) 

443 
next 

444 
fix x::'a and n 

445 
assume "x$$i \<le> a  1 / real (Suc n)" 

446 
also have "\<dots> < a" by auto 

447 
finally show "x$$i < a" . 

448 
qed 

449 
have "{x. x$$i < a} \<in> sets ?SIGMA" unfolding * 

450 
by (safe intro!: countable_UN) 

451 
(auto simp: sets_sigma intro!: sigma_sets.Basic) } 

452 
then show ?thesis by (intro sets_sigma_subset) auto 

453 
qed 

38656  454 

455 
lemma halfspace_span_halfspace_ge: 

40859  456 
"sets (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i < a})\<rparr>) \<subseteq> 
457 
sets (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x. a \<le> x $$ i})\<rparr>)" 

38656  458 
(is "_ \<subseteq> sets ?SIGMA") 
40859  459 
proof  
460 
have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto 

38656  461 
then interpret sigma_algebra ?SIGMA . 
40859  462 
{ fix a i have *: "{x::'a. x$$i < a} = space ?SIGMA  {x::'a. a \<le> x$$i}" by auto 
463 
have "{x. x$$i < a} \<in> sets ?SIGMA" unfolding * 

464 
by (safe intro!: Diff) 

465 
(auto simp: sets_sigma intro!: sigma_sets.Basic) } 

466 
then show ?thesis by (intro sets_sigma_subset) auto 

467 
qed 

38656  468 

469 
lemma halfspace_le_span_halfspace_gt: 

40859  470 
"sets (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i \<le> a})\<rparr>) \<subseteq> 
471 
sets (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x. a < x $$ i})\<rparr>)" 

38656  472 
(is "_ \<subseteq> sets ?SIGMA") 
40859  473 
proof  
474 
have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto 

38656  475 
then interpret sigma_algebra ?SIGMA . 
40859  476 
{ fix a i have *: "{x::'a. x$$i \<le> a} = space ?SIGMA  {x::'a. a < x$$i}" by auto 
477 
have "{x. x$$i \<le> a} \<in> sets ?SIGMA" unfolding * 

478 
by (safe intro!: Diff) 

479 
(auto simp: sets_sigma intro!: sigma_sets.Basic) } 

480 
then show ?thesis by (intro sets_sigma_subset) auto 

481 
qed 

38656  482 

483 
lemma halfspace_le_span_atMost: 

40859  484 
"sets (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i \<le> a})\<rparr>) \<subseteq> 
485 
sets (sigma \<lparr>space=UNIV, sets=range (\<lambda>a. {..a\<Colon>'a\<Colon>ordered_euclidean_space})\<rparr>)" 

38656  486 
(is "_ \<subseteq> sets ?SIGMA") 
40859  487 
proof  
488 
have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto 

38656  489 
then interpret sigma_algebra ?SIGMA . 
40859  490 
have "\<And>a i. {x. x$$i \<le> a} \<in> sets ?SIGMA" 
38656  491 
proof cases 
40859  492 
fix a i assume "i < DIM('a)" 
38656  493 
then have *: "{x::'a. x$$i \<le> a} = (\<Union>k::nat. {.. (\<chi>\<chi> n. if n = i then a else real k)})" 
494 
proof (safe, simp_all add: eucl_le[where 'a='a] split: split_if_asm) 

495 
fix x 

496 
from real_arch_simple[of "Max ((\<lambda>i. x$$i)`{..<DIM('a)})"] guess k::nat .. 

497 
then have "\<And>i. i < DIM('a) \<Longrightarrow> x$$i \<le> real k" 

498 
by (subst (asm) Max_le_iff) auto 

499 
then show "\<exists>k::nat. \<forall>ia. ia \<noteq> i \<longrightarrow> ia < DIM('a) \<longrightarrow> x $$ ia \<le> real k" 

500 
by (auto intro!: exI[of _ k]) 

501 
qed 

502 
show "{x. x$$i \<le> a} \<in> sets ?SIGMA" unfolding * 

503 
by (safe intro!: countable_UN) 

504 
(auto simp: sets_sigma intro!: sigma_sets.Basic) 

505 
next 

40859  506 
fix a i assume "\<not> i < DIM('a)" 
38656  507 
then show "{x. x$$i \<le> a} \<in> sets ?SIGMA" 
508 
using top by auto 

509 
qed 

40859  510 
then show ?thesis by (intro sets_sigma_subset) auto 
511 
qed 

38656  512 

513 
lemma halfspace_le_span_greaterThan: 

40859  514 
"sets (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i \<le> a})\<rparr>) \<subseteq> 
515 
sets (sigma \<lparr>space=UNIV, sets=range (\<lambda>a. {a<..})\<rparr>)" 

38656  516 
(is "_ \<subseteq> sets ?SIGMA") 
40859  517 
proof  
518 
have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto 

38656  519 
then interpret sigma_algebra ?SIGMA . 
40859  520 
have "\<And>a i. {x. x$$i \<le> a} \<in> sets ?SIGMA" 
38656  521 
proof cases 
40859  522 
fix a i assume "i < DIM('a)" 
38656  523 
have "{x::'a. x$$i \<le> a} = space ?SIGMA  {x::'a. a < x$$i}" by auto 
524 
also have *: "{x::'a. a < x$$i} = (\<Union>k::nat. {(\<chi>\<chi> n. if n = i then a else real k) <..})" using `i <DIM('a)` 

525 
proof (safe, simp_all add: eucl_less[where 'a='a] split: split_if_asm) 

526 
fix x 

527 
from real_arch_lt[of "Max ((\<lambda>i. x$$i)`{..<DIM('a)})"] 

528 
guess k::nat .. note k = this 

529 
{ fix i assume "i < DIM('a)" 

530 
then have "x$$i < real k" 

531 
using k by (subst (asm) Max_less_iff) auto 

532 
then have " real k < x$$i" by simp } 

533 
then show "\<exists>k::nat. \<forall>ia. ia \<noteq> i \<longrightarrow> ia < DIM('a) \<longrightarrow> real k < x $$ ia" 

534 
by (auto intro!: exI[of _ k]) 

535 
qed 

536 
finally show "{x. x$$i \<le> a} \<in> sets ?SIGMA" 

537 
apply (simp only:) 

538 
apply (safe intro!: countable_UN Diff) 

539 
by (auto simp: sets_sigma intro!: sigma_sets.Basic) 

540 
next 

40859  541 
fix a i assume "\<not> i < DIM('a)" 
38656  542 
then show "{x. x$$i \<le> a} \<in> sets ?SIGMA" 
543 
using top by auto 

544 
qed 

40859  545 
then show ?thesis by (intro sets_sigma_subset) auto 
546 
qed 

547 

548 
lemma halfspace_le_span_lessThan: 

549 
"sets (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. a \<le> x $$ i})\<rparr>) \<subseteq> 

550 
sets (sigma \<lparr>space=UNIV, sets=range (\<lambda>a. {..<a})\<rparr>)" 

551 
(is "_ \<subseteq> sets ?SIGMA") 

552 
proof  

553 
have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto 

554 
then interpret sigma_algebra ?SIGMA . 

555 
have "\<And>a i. {x. a \<le> x$$i} \<in> sets ?SIGMA" 

556 
proof cases 

557 
fix a i assume "i < DIM('a)" 

558 
have "{x::'a. a \<le> x$$i} = space ?SIGMA  {x::'a. x$$i < a}" by auto 

559 
also have *: "{x::'a. x$$i < a} = (\<Union>k::nat. {..< (\<chi>\<chi> n. if n = i then a else real k)})" using `i <DIM('a)` 

560 
proof (safe, simp_all add: eucl_less[where 'a='a] split: split_if_asm) 

561 
fix x 

562 
from real_arch_lt[of "Max ((\<lambda>i. x$$i)`{..<DIM('a)})"] 

563 
guess k::nat .. note k = this 

564 
{ fix i assume "i < DIM('a)" 

565 
then have "x$$i < real k" 

566 
using k by (subst (asm) Max_less_iff) auto 

567 
then have "x$$i < real k" by simp } 

568 
then show "\<exists>k::nat. \<forall>ia. ia \<noteq> i \<longrightarrow> ia < DIM('a) \<longrightarrow> x $$ ia < real k" 

569 
by (auto intro!: exI[of _ k]) 

570 
qed 

571 
finally show "{x. a \<le> x$$i} \<in> sets ?SIGMA" 

572 
apply (simp only:) 

573 
apply (safe intro!: countable_UN Diff) 

574 
by (auto simp: sets_sigma intro!: sigma_sets.Basic) 

575 
next 

576 
fix a i assume "\<not> i < DIM('a)" 

577 
then show "{x. a \<le> x$$i} \<in> sets ?SIGMA" 

578 
using top by auto 

579 
qed 

580 
then show ?thesis by (intro sets_sigma_subset) auto 

581 
qed 

582 

583 
lemma atMost_span_atLeastAtMost: 

584 
"sets (sigma \<lparr>space=UNIV, sets=range (\<lambda>a. {..a\<Colon>'a\<Colon>ordered_euclidean_space})\<rparr>) \<subseteq> 

585 
sets (sigma \<lparr>space=UNIV, sets=range (\<lambda>(a,b). {a..b})\<rparr>)" 

586 
(is "_ \<subseteq> sets ?SIGMA") 

587 
proof  

588 
have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto 

589 
then interpret sigma_algebra ?SIGMA . 

590 
{ fix a::'a 

591 
have *: "{..a} = (\<Union>n::nat. { real n *\<^sub>R One .. a})" 

592 
proof (safe, simp_all add: eucl_le[where 'a='a]) 

593 
fix x 

594 
from real_arch_simple[of "Max ((\<lambda>i.  x$$i)`{..<DIM('a)})"] 

595 
guess k::nat .. note k = this 

596 
{ fix i assume "i < DIM('a)" 

597 
with k have " x$$i \<le> real k" 

598 
by (subst (asm) Max_le_iff) (auto simp: field_simps) 

599 
then have " real k \<le> x$$i" by simp } 

600 
then show "\<exists>n::nat. \<forall>i<DIM('a).  real n \<le> x $$ i" 

601 
by (auto intro!: exI[of _ k]) 

602 
qed 

603 
have "{..a} \<in> sets ?SIGMA" unfolding * 

604 
by (safe intro!: countable_UN) 

605 
(auto simp: sets_sigma intro!: sigma_sets.Basic) } 

606 
then show ?thesis by (intro sets_sigma_subset) auto 

607 
qed 

608 

609 
lemma borel_eq_atMost: 

610 
"borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> a. {.. a::'a\<Colon>ordered_euclidean_space})\<rparr>)" 

611 
(is "_ = ?SIGMA") 

40869  612 
proof (intro algebra.equality antisym) 
40859  613 
show "sets borel \<subseteq> sets ?SIGMA" 
614 
using halfspace_le_span_atMost halfspace_span_halfspace_le open_span_halfspace 

615 
by auto 

616 
show "sets ?SIGMA \<subseteq> sets borel" 

617 
by (rule borel.sets_sigma_subset) auto 

618 
qed auto 

619 

620 
lemma borel_eq_atLeastAtMost: 

621 
"borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a :: 'a\<Colon>ordered_euclidean_space, b). {a .. b})\<rparr>)" 

622 
(is "_ = ?SIGMA") 

40869  623 
proof (intro algebra.equality antisym) 
40859  624 
show "sets borel \<subseteq> sets ?SIGMA" 
625 
using atMost_span_atLeastAtMost halfspace_le_span_atMost 

626 
halfspace_span_halfspace_le open_span_halfspace 

627 
by auto 

628 
show "sets ?SIGMA \<subseteq> sets borel" 

629 
by (rule borel.sets_sigma_subset) auto 

630 
qed auto 

631 

632 
lemma borel_eq_greaterThan: 

633 
"borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a :: 'a\<Colon>ordered_euclidean_space). {a <..})\<rparr>)" 

634 
(is "_ = ?SIGMA") 

40869  635 
proof (intro algebra.equality antisym) 
40859  636 
show "sets borel \<subseteq> sets ?SIGMA" 
637 
using halfspace_le_span_greaterThan 

638 
halfspace_span_halfspace_le open_span_halfspace 

639 
by auto 

640 
show "sets ?SIGMA \<subseteq> sets borel" 

641 
by (rule borel.sets_sigma_subset) auto 

642 
qed auto 

643 

644 
lemma borel_eq_lessThan: 

645 
"borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a :: 'a\<Colon>ordered_euclidean_space). {..< a})\<rparr>)" 

646 
(is "_ = ?SIGMA") 

40869  647 
proof (intro algebra.equality antisym) 
40859  648 
show "sets borel \<subseteq> sets ?SIGMA" 
649 
using halfspace_le_span_lessThan 

650 
halfspace_span_halfspace_ge open_span_halfspace 

651 
by auto 

652 
show "sets ?SIGMA \<subseteq> sets borel" 

653 
by (rule borel.sets_sigma_subset) auto 

654 
qed auto 

655 

656 
lemma borel_eq_greaterThanLessThan: 

657 
"borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, b). {a <..< (b :: 'a \<Colon> ordered_euclidean_space)})\<rparr>)" 

658 
(is "_ = ?SIGMA") 

40869  659 
proof (intro algebra.equality antisym) 
40859  660 
show "sets ?SIGMA \<subseteq> sets borel" 
661 
by (rule borel.sets_sigma_subset) auto 

662 
show "sets borel \<subseteq> sets ?SIGMA" 

663 
proof  

664 
have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto 

665 
then interpret sigma_algebra ?SIGMA . 

666 
{ fix M :: "'a set" assume "M \<in> open" 

667 
then have "open M" by (simp add: mem_def) 

668 
have "M \<in> sets ?SIGMA" 

669 
apply (subst open_UNION[OF `open M`]) 

670 
apply (safe intro!: countable_UN) 

671 
by (auto simp add: sigma_def intro!: sigma_sets.Basic) } 

672 
then show ?thesis 

673 
unfolding borel_def by (intro sets_sigma_subset) auto 

674 
qed 

38656  675 
qed auto 
676 

40859  677 
lemma borel_eq_halfspace_le: 
678 
"borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. x$$i \<le> a})\<rparr>)" 

679 
(is "_ = ?SIGMA") 

40869  680 
proof (intro algebra.equality antisym) 
40859  681 
show "sets borel \<subseteq> sets ?SIGMA" 
682 
using open_span_halfspace halfspace_span_halfspace_le by auto 

683 
show "sets ?SIGMA \<subseteq> sets borel" 

684 
by (rule borel.sets_sigma_subset) auto 

685 
qed auto 

686 

687 
lemma borel_eq_halfspace_less: 

688 
"borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. x$$i < a})\<rparr>)" 

689 
(is "_ = ?SIGMA") 

40869  690 
proof (intro algebra.equality antisym) 
40859  691 
show "sets borel \<subseteq> sets ?SIGMA" 
692 
using open_span_halfspace . 

693 
show "sets ?SIGMA \<subseteq> sets borel" 

694 
by (rule borel.sets_sigma_subset) auto 

38656  695 
qed auto 
696 

40859  697 
lemma borel_eq_halfspace_gt: 
698 
"borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. a < x$$i})\<rparr>)" 

699 
(is "_ = ?SIGMA") 

40869  700 
proof (intro algebra.equality antisym) 
40859  701 
show "sets borel \<subseteq> sets ?SIGMA" 
702 
using halfspace_le_span_halfspace_gt open_span_halfspace halfspace_span_halfspace_le by auto 

703 
show "sets ?SIGMA \<subseteq> sets borel" 

704 
by (rule borel.sets_sigma_subset) auto 

705 
qed auto 

38656  706 

40859  707 
lemma borel_eq_halfspace_ge: 
708 
"borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. a \<le> x$$i})\<rparr>)" 

709 
(is "_ = ?SIGMA") 

40869  710 
proof (intro algebra.equality antisym) 
40859  711 
show "sets borel \<subseteq> sets ?SIGMA" 
38656  712 
using halfspace_span_halfspace_ge open_span_halfspace by auto 
40859  713 
show "sets ?SIGMA \<subseteq> sets borel" 
714 
by (rule borel.sets_sigma_subset) auto 

715 
qed auto 

38656  716 

717 
lemma (in sigma_algebra) borel_measurable_halfspacesI: 

718 
fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space" 

40859  719 
assumes "borel = (sigma \<lparr>space=UNIV, sets=range F\<rparr>)" 
38656  720 
and "\<And>a i. S a i = f ` F (a,i) \<inter> space M" 
721 
and "\<And>a i. \<not> i < DIM('c) \<Longrightarrow> S a i \<in> sets M" 

722 
shows "f \<in> borel_measurable M = (\<forall>i<DIM('c). \<forall>a::real. S a i \<in> sets M)" 

723 
proof safe 

724 
fix a :: real and i assume i: "i < DIM('c)" and f: "f \<in> borel_measurable M" 

725 
then show "S a i \<in> sets M" unfolding assms 

726 
by (auto intro!: measurable_sets sigma_sets.Basic simp: assms(1) sigma_def) 

727 
next 

728 
assume a: "\<forall>i<DIM('c). \<forall>a. S a i \<in> sets M" 

729 
{ fix a i have "S a i \<in> sets M" 

730 
proof cases 

731 
assume "i < DIM('c)" 

732 
with a show ?thesis unfolding assms(2) by simp 

733 
next 

734 
assume "\<not> i < DIM('c)" 

735 
from assms(3)[OF this] show ?thesis . 

736 
qed } 

40859  737 
then have "f \<in> measurable M (sigma \<lparr>space=UNIV, sets=range F\<rparr>)" 
38656  738 
by (auto intro!: measurable_sigma simp: assms(2)) 
739 
then show "f \<in> borel_measurable M" unfolding measurable_def 

740 
unfolding assms(1) by simp 

741 
qed 

742 

743 
lemma (in sigma_algebra) borel_measurable_iff_halfspace_le: 

744 
fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space" 

745 
shows "f \<in> borel_measurable M = (\<forall>i<DIM('c). \<forall>a. {w \<in> space M. f w $$ i \<le> a} \<in> sets M)" 

40859  746 
by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_le]) auto 
38656  747 

748 
lemma (in sigma_algebra) borel_measurable_iff_halfspace_less: 

749 
fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space" 

750 
shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i<DIM('c). \<forall>a. {w \<in> space M. f w $$ i < a} \<in> sets M)" 

40859  751 
by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_less]) auto 
38656  752 

753 
lemma (in sigma_algebra) borel_measurable_iff_halfspace_ge: 

754 
fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space" 

755 
shows "f \<in> borel_measurable M = (\<forall>i<DIM('c). \<forall>a. {w \<in> space M. a \<le> f w $$ i} \<in> sets M)" 

40859  756 
by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_ge]) auto 
38656  757 

758 
lemma (in sigma_algebra) borel_measurable_iff_halfspace_greater: 

759 
fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space" 

760 
shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i<DIM('c). \<forall>a. {w \<in> space M. a < f w $$ i} \<in> sets M)" 

40859  761 
by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_gt]) auto 
38656  762 

763 
lemma (in sigma_algebra) borel_measurable_iff_le: 

764 
"(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w \<le> a} \<in> sets M)" 

765 
using borel_measurable_iff_halfspace_le[where 'c=real] by simp 

766 

767 
lemma (in sigma_algebra) borel_measurable_iff_less: 

768 
"(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w < a} \<in> sets M)" 

769 
using borel_measurable_iff_halfspace_less[where 'c=real] by simp 

770 

771 
lemma (in sigma_algebra) borel_measurable_iff_ge: 

772 
"(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a \<le> f w} \<in> sets M)" 

773 
using borel_measurable_iff_halfspace_ge[where 'c=real] by simp 

774 

775 
lemma (in sigma_algebra) borel_measurable_iff_greater: 

776 
"(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a < f w} \<in> sets M)" 

777 
using borel_measurable_iff_halfspace_greater[where 'c=real] by simp 

778 

41025  779 
lemma borel_measurable_euclidean_component: 
40859  780 
"(\<lambda>x::'a::euclidean_space. x $$ i) \<in> borel_measurable borel" 
781 
unfolding borel_def[where 'a=real] 

782 
proof (rule borel.measurable_sigma, simp_all) 

39087
96984bf6fa5b
Measurable on euclidean space is equiv. to measurable components
hoelzl
parents:
39083
diff
changeset

783 
fix S::"real set" assume "S \<in> open" then have "open S" unfolding mem_def . 
96984bf6fa5b
Measurable on euclidean space is equiv. to measurable components
hoelzl
parents:
39083
diff
changeset

784 
from open_vimage_euclidean_component[OF this] 
40859  785 
show "(\<lambda>x. x $$ i) ` S \<in> sets borel" 
786 
by (auto intro: borel_open) 

787 
qed 

39087
96984bf6fa5b
Measurable on euclidean space is equiv. to measurable components
hoelzl
parents:
39083
diff
changeset

788 

41025  789 
lemma (in sigma_algebra) borel_measurable_euclidean_space: 
39087
96984bf6fa5b
Measurable on euclidean space is equiv. to measurable components
hoelzl
parents:
39083
diff
changeset

790 
fixes f :: "'a \<Rightarrow> 'c::ordered_euclidean_space" 
96984bf6fa5b
Measurable on euclidean space is equiv. to measurable components
hoelzl
parents:
39083
diff
changeset

791 
shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i<DIM('c). (\<lambda>x. f x $$ i) \<in> borel_measurable M)" 
96984bf6fa5b
Measurable on euclidean space is equiv. to measurable components
hoelzl
parents:
39083
diff
changeset

792 
proof safe 
96984bf6fa5b
Measurable on euclidean space is equiv. to measurable components
hoelzl
parents:
39083
diff
changeset

793 
fix i assume "f \<in> borel_measurable M" 
96984bf6fa5b
Measurable on euclidean space is equiv. to measurable components
hoelzl
parents:
39083
diff
changeset

794 
then show "(\<lambda>x. f x $$ i) \<in> borel_measurable M" 
96984bf6fa5b
Measurable on euclidean space is equiv. to measurable components
hoelzl
parents:
39083
diff
changeset

795 
using measurable_comp[of f _ _ "\<lambda>x. x $$ i", unfolded comp_def] 
41025  796 
by (auto intro: borel_measurable_euclidean_component) 
39087
96984bf6fa5b
Measurable on euclidean space is equiv. to measurable components
hoelzl
parents:
39083
diff
changeset

797 
next 
96984bf6fa5b
Measurable on euclidean space is equiv. to measurable components
hoelzl
parents:
39083
diff
changeset

798 
assume f: "\<forall>i<DIM('c). (\<lambda>x. f x $$ i) \<in> borel_measurable M" 
96984bf6fa5b
Measurable on euclidean space is equiv. to measurable components
hoelzl
parents:
39083
diff
changeset

799 
then show "f \<in> borel_measurable M" 
96984bf6fa5b
Measurable on euclidean space is equiv. to measurable components
hoelzl
parents:
39083
diff
changeset

800 
unfolding borel_measurable_iff_halfspace_le by auto 
96984bf6fa5b
Measurable on euclidean space is equiv. to measurable components
hoelzl
parents:
39083
diff
changeset

801 
qed 
96984bf6fa5b
Measurable on euclidean space is equiv. to measurable components
hoelzl
parents:
39083
diff
changeset

802 

38656  803 
subsection "Borel measurable operators" 
804 

805 
lemma (in sigma_algebra) affine_borel_measurable_vector: 

806 
fixes f :: "'a \<Rightarrow> 'x::real_normed_vector" 

807 
assumes "f \<in> borel_measurable M" 

808 
shows "(\<lambda>x. a + b *\<^sub>R f x) \<in> borel_measurable M" 

809 
proof (rule borel_measurableI) 

810 
fix S :: "'x set" assume "open S" 

811 
show "(\<lambda>x. a + b *\<^sub>R f x) ` S \<inter> space M \<in> sets M" 

812 
proof cases 

813 
assume "b \<noteq> 0" 

814 
with `open S` have "((\<lambda>x. ( a + x) /\<^sub>R b) ` S) \<in> open" (is "?S \<in> open") 

815 
by (auto intro!: open_affinity simp: scaleR.add_right mem_def) 

40859  816 
hence "?S \<in> sets borel" 
817 
unfolding borel_def by (auto simp: sigma_def intro!: sigma_sets.Basic) 

38656  818 
moreover 
819 
from `b \<noteq> 0` have "(\<lambda>x. a + b *\<^sub>R f x) ` S = f ` ?S" 

820 
apply auto by (rule_tac x="a + b *\<^sub>R f x" in image_eqI, simp_all) 

40859  821 
ultimately show ?thesis using assms unfolding in_borel_measurable_borel 
38656  822 
by auto 
823 
qed simp 

824 
qed 

825 

826 
lemma (in sigma_algebra) affine_borel_measurable: 

827 
fixes g :: "'a \<Rightarrow> real" 

828 
assumes g: "g \<in> borel_measurable M" 

829 
shows "(\<lambda>x. a + (g x) * b) \<in> borel_measurable M" 

830 
using affine_borel_measurable_vector[OF assms] by (simp add: mult_commute) 

831 

832 
lemma (in sigma_algebra) borel_measurable_add[simp, intro]: 

833 
fixes f :: "'a \<Rightarrow> real" 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

834 
assumes f: "f \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

835 
assumes g: "g \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

836 
shows "(\<lambda>x. f x + g x) \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

837 
proof  
38656  838 
have 1: "\<And>a. {w\<in>space M. a \<le> f w + g w} = {w \<in> space M. a + g w * 1 \<le> f w}" 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

839 
by auto 
38656  840 
have "\<And>a. (\<lambda>w. a + (g w) * 1) \<in> borel_measurable M" 
841 
by (rule affine_borel_measurable [OF g]) 

842 
then have "\<And>a. {w \<in> space M. (\<lambda>w. a + (g w) * 1)(w) \<le> f w} \<in> sets M" using f 

843 
by auto 

844 
then have "\<And>a. {w \<in> space M. a \<le> f w + g w} \<in> sets M" 

845 
by (simp add: 1) 

846 
then show ?thesis 

847 
by (simp add: borel_measurable_iff_ge) 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

848 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

849 

41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41025
diff
changeset

850 
lemma (in sigma_algebra) borel_measurable_setsum[simp, intro]: 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41025
diff
changeset

851 
fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real" 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41025
diff
changeset

852 
assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M" 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41025
diff
changeset

853 
shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M" 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41025
diff
changeset

854 
proof cases 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41025
diff
changeset

855 
assume "finite S" 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41025
diff
changeset

856 
thus ?thesis using assms by induct auto 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41025
diff
changeset

857 
qed simp 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41025
diff
changeset

858 

38656  859 
lemma (in sigma_algebra) borel_measurable_square: 
860 
fixes f :: "'a \<Rightarrow> real" 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

861 
assumes f: "f \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

862 
shows "(\<lambda>x. (f x)^2) \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

863 
proof  
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

864 
{ 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

865 
fix a 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

866 
have "{w \<in> space M. (f w)\<twosuperior> \<le> a} \<in> sets M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

867 
proof (cases rule: linorder_cases [of a 0]) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

868 
case less 
38656  869 
hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} = {}" 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

870 
by auto (metis less order_le_less_trans power2_less_0) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

871 
also have "... \<in> sets M" 
38656  872 
by (rule empty_sets) 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

873 
finally show ?thesis . 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

874 
next 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

875 
case equal 
38656  876 
hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} = 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

877 
{w \<in> space M. f w \<le> 0} \<inter> {w \<in> space M. 0 \<le> f w}" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

878 
by auto 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

879 
also have "... \<in> sets M" 
38656  880 
apply (insert f) 
881 
apply (rule Int) 

882 
apply (simp add: borel_measurable_iff_le) 

883 
apply (simp add: borel_measurable_iff_ge) 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

884 
done 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

885 
finally show ?thesis . 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

886 
next 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

887 
case greater 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

888 
have "\<forall>x. (f x ^ 2 \<le> sqrt a ^ 2) = ( sqrt a \<le> f x & f x \<le> sqrt a)" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

889 
by (metis abs_le_interval_iff abs_of_pos greater real_sqrt_abs 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

890 
real_sqrt_le_iff real_sqrt_power) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

891 
hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} = 
38656  892 
{w \<in> space M. (sqrt a) \<le> f w} \<inter> {w \<in> space M. f w \<le> sqrt a}" 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

893 
using greater by auto 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

894 
also have "... \<in> sets M" 
38656  895 
apply (insert f) 
896 
apply (rule Int) 

897 
apply (simp add: borel_measurable_iff_ge) 

898 
apply (simp add: borel_measurable_iff_le) 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

899 
done 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

900 
finally show ?thesis . 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

901 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

902 
} 
38656  903 
thus ?thesis by (auto simp add: borel_measurable_iff_le) 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

904 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

905 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

906 
lemma times_eq_sum_squares: 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

907 
fixes x::real 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

908 
shows"x*y = ((x+y)^2)/4  ((xy)^ 2)/4" 
38656  909 
by (simp add: power2_eq_square ring_distribs diff_divide_distrib [symmetric]) 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

910 

38656  911 
lemma (in sigma_algebra) borel_measurable_uminus[simp, intro]: 
912 
fixes g :: "'a \<Rightarrow> real" 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

913 
assumes g: "g \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

914 
shows "(\<lambda>x.  g x) \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

915 
proof  
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

916 
have "(\<lambda>x.  g x) = (\<lambda>x. 0 + (g x) * 1)" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

917 
by simp 
38656  918 
also have "... \<in> borel_measurable M" 
919 
by (fast intro: affine_borel_measurable g) 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

920 
finally show ?thesis . 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

921 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

922 

38656  923 
lemma (in sigma_algebra) borel_measurable_times[simp, intro]: 
924 
fixes f :: "'a \<Rightarrow> real" 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

925 
assumes f: "f \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

926 
assumes g: "g \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

927 
shows "(\<lambda>x. f x * g x) \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

928 
proof  
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

929 
have 1: "(\<lambda>x. 0 + (f x + g x)\<twosuperior> * inverse 4) \<in> borel_measurable M" 
38656  930 
using assms by (fast intro: affine_borel_measurable borel_measurable_square) 
931 
have "(\<lambda>x. ((f x + g x) ^ 2 * inverse 4)) = 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

932 
(\<lambda>x. 0 + ((f x + g x) ^ 2 * inverse 4))" 
35582  933 
by (simp add: minus_divide_right) 
38656  934 
also have "... \<in> borel_measurable M" 
935 
using f g by (fast intro: affine_borel_measurable borel_measurable_square f g) 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

936 
finally have 2: "(\<lambda>x. ((f x + g x) ^ 2 * inverse 4)) \<in> borel_measurable M" . 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

937 
show ?thesis 
38656  938 
apply (simp add: times_eq_sum_squares diff_minus) 
939 
using 1 2 by simp 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

940 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

941 

41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41025
diff
changeset

942 
lemma (in sigma_algebra) borel_measurable_setprod[simp, intro]: 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41025
diff
changeset

943 
fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real" 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41025
diff
changeset

944 
assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M" 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41025
diff
changeset

945 
shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M" 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41025
diff
changeset

946 
proof cases 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41025
diff
changeset

947 
assume "finite S" 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41025
diff
changeset

948 
thus ?thesis using assms by induct auto 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41025
diff
changeset

949 
qed simp 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41025
diff
changeset

950 

38656  951 
lemma (in sigma_algebra) borel_measurable_diff[simp, intro]: 
952 
fixes f :: "'a \<Rightarrow> real" 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

953 
assumes f: "f \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

954 
assumes g: "g \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

955 
shows "(\<lambda>x. f x  g x) \<in> borel_measurable M" 
38656  956 
unfolding diff_minus using assms by fast 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

957 

38656  958 
lemma (in sigma_algebra) borel_measurable_inverse[simp, intro]: 
959 
fixes f :: "'a \<Rightarrow> real" 

35692  960 
assumes "f \<in> borel_measurable M" 
961 
shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M" 

38656  962 
unfolding borel_measurable_iff_ge unfolding inverse_eq_divide 
963 
proof safe 

964 
fix a :: real 

965 
have *: "{w \<in> space M. a \<le> 1 / f w} = 

966 
({w \<in> space M. 0 < f w} \<inter> {w \<in> space M. a * f w \<le> 1}) \<union> 

967 
({w \<in> space M. f w < 0} \<inter> {w \<in> space M. 1 \<le> a * f w}) \<union> 

968 
({w \<in> space M. f w = 0} \<inter> {w \<in> space M. a \<le> 0})" by (auto simp: le_divide_eq) 

969 
show "{w \<in> space M. a \<le> 1 / f w} \<in> sets M" using assms unfolding * 

970 
by (auto intro!: Int Un) 

35692  971 
qed 
972 

38656  973 
lemma (in sigma_algebra) borel_measurable_divide[simp, intro]: 
974 
fixes f :: "'a \<Rightarrow> real" 

35692  975 
assumes "f \<in> borel_measurable M" 
976 
and "g \<in> borel_measurable M" 

977 
shows "(\<lambda>x. f x / g x) \<in> borel_measurable M" 

978 
unfolding field_divide_inverse 

38656  979 
by (rule borel_measurable_inverse borel_measurable_times assms)+ 
980 

981 
lemma (in sigma_algebra) borel_measurable_max[intro, simp]: 

982 
fixes f g :: "'a \<Rightarrow> real" 

983 
assumes "f \<in> borel_measurable M" 

984 
assumes "g \<in> borel_measurable M" 

985 
shows "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M" 

986 
unfolding borel_measurable_iff_le 

987 
proof safe 

988 
fix a 

989 
have "{x \<in> space M. max (g x) (f x) \<le> a} = 

990 
{x \<in> space M. g x \<le> a} \<inter> {x \<in> space M. f x \<le> a}" by auto 

991 
thus "{x \<in> space M. max (g x) (f x) \<le> a} \<in> sets M" 

992 
using assms unfolding borel_measurable_iff_le 

993 
by (auto intro!: Int) 

994 
qed 

995 

996 
lemma (in sigma_algebra) borel_measurable_min[intro, simp]: 

997 
fixes f g :: "'a \<Rightarrow> real" 

998 
assumes "f \<in> borel_measurable M" 

999 
assumes "g \<in> borel_measurable M" 

1000 
shows "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M" 

1001 
unfolding borel_measurable_iff_ge 

1002 
proof safe 

1003 
fix a 

1004 
have "{x \<in> space M. a \<le> min (g x) (f x)} = 

1005 
{x \<in> space M. a \<le> g x} \<inter> {x \<in> space M. a \<le> f x}" by auto 

1006 
thus "{x \<in> space M. a \<le> min (g x) (f x)} \<in> sets M" 

1007 
using assms unfolding borel_measurable_iff_ge 

1008 
by (auto intro!: Int) 

1009 
qed 

1010 

1011 
lemma (in sigma_algebra) borel_measurable_abs[simp, intro]: 

1012 
assumes "f \<in> borel_measurable M" 

1013 
shows "(\<lambda>x. \<bar>f x :: real\<bar>) \<in> borel_measurable M" 

1014 
proof  

1015 
have *: "\<And>x. \<bar>f x\<bar> = max 0 (f x) + max 0 ( f x)" by (simp add: max_def) 

1016 
show ?thesis unfolding * using assms by auto 

1017 
qed 

1018 

41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41025
diff
changeset

1019 
lemma borel_measurable_nth[simp, intro]: 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41025
diff
changeset

1020 
"(\<lambda>x::real^'n. x $ i) \<in> borel_measurable borel" 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41025
diff
changeset

1021 
using borel_measurable_euclidean_component 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41025
diff
changeset

1022 
unfolding nth_conv_component by auto 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41025
diff
changeset

1023 

38656  1024 
section "Borel space over the real line with infinity" 
35692  1025 

40859  1026 
lemma borel_Real_measurable: 
1027 
"A \<in> sets borel \<Longrightarrow> Real ` A \<in> sets borel" 

38656  1028 
proof (rule borel_measurable_translate) 
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40870
diff
changeset

1029 
fix B :: "pextreal set" assume "open B" 
38656  1030 
then obtain T x where T: "open T" "Real ` (T \<inter> {0..}) = B  {\<omega>}" and 
1031 
x: "\<omega> \<in> B \<Longrightarrow> 0 \<le> x" "\<omega> \<in> B \<Longrightarrow> {Real x <..} \<subseteq> B" 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40870
diff
changeset

1032 
unfolding open_pextreal_def by blast 
38656  1033 
have "Real ` B = Real ` (B  {\<omega>})" by auto 
1034 
also have "\<dots> = Real ` (Real ` (T \<inter> {0..}))" using T by simp 

1035 
also have "\<dots> = (if 0 \<in> T then T \<union> {.. 0} else T \<inter> {0..})" 

1036 
apply (auto simp add: Real_eq_Real image_iff) 

1037 
apply (rule_tac x="max 0 x" in bexI) 

1038 
by (auto simp: max_def) 

40859  1039 
finally show "Real ` B \<in> sets borel" 
38656  1040 
using `open T` by auto 
1041 
qed simp 

1042 

40859  1043 
lemma borel_real_measurable: 
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40870
diff
changeset

1044 
"A \<in> sets borel \<Longrightarrow> (real ` A :: pextreal set) \<in> sets borel" 
38656  1045 
proof (rule borel_measurable_translate) 
1046 
fix B :: "real set" assume "open B" 

1047 
{ fix x have "0 < real x \<longleftrightarrow> (\<exists>r>0. x = Real r)" by (cases x) auto } 

1048 
note Ex_less_real = this 

1049 
have *: "real ` B = (if 0 \<in> B then real ` (B \<inter> {0 <..}) \<union> {0, \<omega>} else real ` (B \<inter> {0 <..}))" 

1050 
by (force simp: Ex_less_real) 

1051 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40870
diff
changeset

1052 
have "open (real ` (B \<inter> {0 <..}) :: pextreal set)" 
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40870
diff
changeset

1053 
unfolding open_pextreal_def using `open B` 
38656  1054 
by (auto intro!: open_Int exI[of _ "B \<inter> {0 <..}"] simp: image_iff Ex_less_real) 
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40870
diff
changeset

1055 
then show "(real ` B :: pextreal set) \<in> sets borel" unfolding * by auto 
38656  1056 
qed simp 
1057 

1058 
lemma (in sigma_algebra) borel_measurable_Real[intro, simp]: 

1059 
assumes "f \<in> borel_measurable M" 

1060 
shows "(\<lambda>x. Real (f x)) \<in> borel_measurable M" 

40859  1061 
unfolding in_borel_measurable_borel 
38656  1062 
proof safe 
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40870
diff
changeset

1063 
fix S :: "pextreal set" assume "S \<in> sets borel" 
40859  1064 
from borel_Real_measurable[OF this] 
38656  1065 
have "(Real \<circ> f) ` S \<inter> space M \<in> sets M" 
1066 
using assms 

40859  1067 
unfolding vimage_compose in_borel_measurable_borel 
38656  1068 
by auto 
1069 
thus "(\<lambda>x. Real (f x)) ` S \<inter> space M \<in> sets M" by (simp add: comp_def) 

35748  1070 
qed 
35692  1071 

38656  1072 
lemma (in sigma_algebra) borel_measurable_real[intro, simp]: 
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40870
diff
changeset

1073 
fixes f :: "'a \<Rightarrow> pextreal" 
38656  1074 
assumes "f \<in> borel_measurable M" 
1075 
shows "(\<lambda>x. real (f x)) \<in> borel_measurable M" 

40859  1076 
unfolding in_borel_measurable_borel 
38656  1077 
proof safe 
40859  1078 
fix S :: "real set" assume "S \<in> sets borel" 
1079 
from borel_real_measurable[OF this] 

38656  1080 
have "(real \<circ> f) ` S \<inter> space M \<in> sets M" 
1081 
using assms 

40859  1082 
unfolding vimage_compose in_borel_measurable_borel 
38656  1083 
by auto 
1084 
thus "(\<lambda>x. real (f x)) ` S \<inter> space M \<in> sets M" by (simp add: comp_def) 

1085 
qed 

35692  1086 

38656  1087 
lemma (in sigma_algebra) borel_measurable_Real_eq: 
1088 
assumes "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x" 

1089 
shows "(\<lambda>x. Real (f x)) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M" 

1090 
proof 

1091 
have [simp]: "(\<lambda>x. Real (f x)) ` {\<omega>} \<inter> space M = {}" 

1092 
by auto 

1093 
assume "(\<lambda>x. Real (f x)) \<in> borel_measurable M" 

1094 
hence "(\<lambda>x. real (Real (f x))) \<in> borel_measurable M" 

1095 
by (rule borel_measurable_real) 

1096 
moreover have "\<And>x. x \<in> space M \<Longrightarrow> real (Real (f x)) = f x" 

1097 
using assms by auto 

1098 
ultimately show "f \<in> borel_measurable M" 

1099 
by (simp cong: measurable_cong) 

1100 
qed auto 

35692  1101 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40870
diff
changeset

1102 
lemma (in sigma_algebra) borel_measurable_pextreal_eq_real: 
38656  1103 
"f \<in> borel_measurable M \<longleftrightarrow> 
1104 
((\<lambda>x. real (f x)) \<in> borel_measurable M \<and> f ` {\<omega>} \<inter> space M \<in> sets M)" 

1105 
proof safe 

1106 
assume "f \<in> borel_measurable M" 

1107 
then show "(\<lambda>x. real (f x)) \<in> borel_measurable M" "f ` {\<omega>} \<inter> space M \<in> sets M" 

1108 
by (auto intro: borel_measurable_vimage borel_measurable_real) 

1109 
next 

1110 
assume *: "(\<lambda>x. real (f x)) \<in> borel_measurable M" "f ` {\<omega>} \<inter> space M \<in> sets M" 

1111 
have "f ` {\<omega>} \<inter> space M = {x\<in>space M. f x = \<omega>}" by auto 

1112 
with * have **: "{x\<in>space M. f x = \<omega>} \<in> sets M" by simp 

1113 
have f: "f = (\<lambda>x. if f x = \<omega> then \<omega> else Real (real (f x)))" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

1114 
by (simp add: fun_eq_iff Real_real) 
38656  1115 
show "f \<in> borel_measurable M" 
1116 
apply (subst f) 

1117 
apply (rule measurable_If) 

1118 
using * ** by auto 

1119 
qed 

1120 

1121 
lemma (in sigma_algebra) less_eq_ge_measurable: 

1122 
fixes f :: "'a \<Rightarrow> 'c::linorder" 

1123 
shows "{x\<in>space M. a < f x} \<in> sets M \<longleftrightarrow> {x\<in>space M. f x \<le> a} \<in> sets M" 

1124 
proof 

1125 
assume "{x\<in>space M. f x \<le> a} \<in> sets M" 

1126 
moreover have "{x\<in>space M. a < f x} = space M  {x\<in>space M. f x \<le> a}" by auto 

1127 
ultimately show "{x\<in>space M. a < f x} \<in> sets M" by auto 

1128 
next 

1129 
assume "{x\<in>space M. a < f x} \<in> sets M" 

1130 
moreover have "{x\<in>space M. f x \<le> a} = space M  {x\<in>space M. a < f x}" by auto 

1131 
ultimately show "{x\<in>space M. f x \<le> a} \<in> sets M" by auto 

1132 
qed 

35692  1133 

38656  1134 
lemma (in sigma_algebra) greater_eq_le_measurable: 
1135 
fixes f :: "'a \<Rightarrow> 'c::linorder" 

1136 
shows "{x\<in>space M. f x < a} \<in> sets M \<longleftrightarrow> {x\<in>space M. a \<le> f x} \<in> sets M" 

1137 
proof 

1138 
assume "{x\<in>space M. a \<le> f x} \<in> sets M" 

1139 
moreover have "{x\<in>space M. f x < a} = space M  {x\<in>space M. a \<le> f x}" by auto 

1140 
ultimately show "{x\<in>space M. f x < a} \<in> sets M" by auto 

1141 
next 

1142 
assume "{x\<in>space M. f x < a} \<in> sets M" 

1143 
moreover have "{x\<in>space M. a \<le> f x} = space M  {x\<in>space M. f x < a}" by auto 

1144 
ultimately show "{x\<in>space M. a \<le> f x} \<in> sets M" by auto 

1145 
qed 

1146 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40870
diff
changeset

1147 
lemma (in sigma_algebra) less_eq_le_pextreal_measurable: 
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40870
diff
changeset

1148 
fixes f :: "'a \<Rightarrow> pextreal" 
38656  1149 
shows "(\<forall>a. {x\<in>space M. a < f x} \<in> sets M) \<longleftrightarrow> (\<forall>a. {x\<in>space M. a \<le> f x} \<in> sets M)" 
1150 
proof 

1151 
assume a: "\<forall>a. {x\<in>space M. a \<le> f x} \<in> sets M" 

1152 
show "\<forall>a. {x \<in> space M. a < f x} \<in> sets M" 

1153 
proof 

1154 
fix a show "{x \<in> space M. a < f x} \<in> sets M" 

1155 
proof (cases a) 

1156 
case (preal r) 

1157 
have "{x\<in>space M. a < f x} = (\<Union>i. {x\<in>space M. a + inverse (of_nat (Suc i)) \<le> f x})" 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

1158 
proof safe 
38656  1159 
fix x assume "a < f x" and [simp]: "x \<in> space M" 
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40870
diff
changeset

1160 
with ex_pextreal_inverse_of_nat_Suc_less[of "f x  a"] 
38656  1161 
obtain n where "a + inverse (of_nat (Suc n)) < f x" 
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40870
diff
changeset

1162 
by (cases "f x", auto simp: pextreal_minus_order) 
38656  1163 
then have "a + inverse (of_nat (Suc n)) \<le> f x" by simp 
1164 
then show "x \<in> (\<Union>i. {x \<in> space M. a + inverse (of_nat (Suc i)) \<le> f x})" 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

1165 
by auto 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

1166 
next 
38656  1167 
fix i x assume [simp]: "x \<in> space M" 
1168 
have "a < a + inverse (of_nat (Suc i))" using preal by auto 

1169 
also assume "a + inverse (of_nat (Suc i)) \<le> f x" 

1170 
finally show "a < f x" . 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

1171 
qed 
38656  1172 
with a show ?thesis by auto 
1173 
qed simp 

35582  1174 
qed 
1175 
next 

38656  1176 
assume a': "\<forall>a. {x \<in> space M. a < f x} \<in> sets M" 
1177 
then have a: "\<forall>a. {x \<in> space M. f x \<le> a} \<in> sets M" unfolding less_eq_ge_measurable . 

1178 
show "\<forall>a. {x \<in> space M. a \<le> f x} \<in> sets M" unfolding greater_eq_le_measurable[symmetric] 

1179 
proof 

1180 
fix a show "{x \<in> space M. f x < a} \<in> sets M" 

1181 
proof (cases a) 

1182 
case (preal r) 

1183 
show ?thesis 

1184 
proof cases 

1185 
assume "a = 0" then show ?thesis by simp 

1186 
next 

1187 
assume "a \<noteq> 0" 

1188 
have "{x\<in>space M. f x < a} = (\<Union>i. {x\<in>space M. f x \<le> a  inverse (of_nat (Suc i))})" 

1189 
proof safe 

1190 
fix x assume "f x < a" and [simp]: "x \<in> space M" 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40870
diff
changeset

1191 
with ex_pextreal_inverse_of_nat_Suc_less[of "a  f x"] 
38656  1192 
obtain n where "inverse (of_nat (Suc n)) < a  f x" 
1193 
using preal by (cases "f x") auto 

1194 
then have "f x \<le> a  inverse (of_nat (Suc n)) " 

1195 
using preal by (cases "f x") (auto split: split_if_asm) 

1196 
then show "x \<in> (\<Union>i. {x \<in> space M. f x \<le> a  inverse (of_nat (Suc i))})" 

1197 
by auto 

1198 
next 

1199 
fix i x assume [simp]: "x \<in> space M" 

1200 
assume "f x \<le> a  inverse (of_nat (Suc i))" 

1201 
also have "\<dots> < a" using `a \<noteq> 0` preal by auto 

1202 
finally show "f x < a" . 

1203 
qed 

1204 
with a show ?thesis by auto 

1205 
qed 

1206 
next 

1207 
case infinite 

1208 
have "f ` {\<omega>} \<inter> space M = (\<Inter>n. {x\<in>space M. of_nat n < f x})" 

1209 
proof (safe, simp_all, safe) 

1210 
fix x assume *: "\<forall>n::nat. Real (real n) < f x" 

1211 
show "f x = \<omega>" proof (rule ccontr) 

1212 
assume "f x \<noteq> \<omega>" 

1213 
with real_arch_lt[of "real (f x)"] obtain n where "f x < of_nat n" 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40870
diff
changeset

1214 
by (auto simp: pextreal_noteq_omega_Ex) 
38656  1215 
with *[THEN spec, of n] show False by auto 
1216 
qed 

1217 
qed 

1218 
with a' have \<omega>: "f ` {\<omega>} \<inter> space M \<in> sets M" by auto 

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

1220 
using infinite by auto 

1221 
ultimately show ?thesis by auto 

1222 
qed 

35582  1223 
qed 
1224 
qed 

1225 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40870
diff
changeset

1226 
lemma (in sigma_algebra) borel_measurable_pextreal_iff_greater: 
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40870
diff
changeset

1227 
"(f::'a \<Rightarrow> pextreal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. {x\<in>space M. a < f x} \<in> sets M)" 
38656  1228 
proof safe 
1229 
fix a assume f: "f \<in> borel_measurable M" 

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

1231 
with f show "{x\<in>space M. a < f x} \<in> sets M" 

1232 
by (auto intro!: measurable_sets) 

1233 
next 

1234 
assume *: "\<forall>a. {x\<in>space M. a < f x} \<in> sets M" 

1235 
hence **: "\<forall>a. {x\<in>space M. f x < a} \<in> sets M" 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40870
diff
changeset

1236 
unfolding less_eq_le_pextreal_measurable 
38656  1237 
unfolding greater_eq_le_measurable . 
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40870
diff
changeset

1238 
show "f \<in> borel_measurable M" unfolding borel_measurable_pextreal_eq_real borel_measurable_iff_greater 
38656  1239 
proof safe 
1240 
have "f ` {\<omega>} \<inter> space M = space M  {x\<in>space M. f x < \<omega>}" by auto 

1241 
then show \<omega>: "f ` {\<omega>} \<inter> space M \<in> sets M" using ** by auto 

1242 
fix a 

1243 
have "{w \<in> space M. a < real (f w)} = 

1244 
(if 0 \<le> a then {w\<in>space M. Real a < f w}  (f ` {\<omega>} \<inter> space M) else space M)" 

1245 
proof (split split_if, safe del: notI) 

1246 
fix x assume "0 \<le> a" 

1247 
{ assume "a < real (f x)" then show "Real a < f x" "x \<notin> f ` {\<omega>} \<inter> space M" 

1248 
using `0 \<le> a` by (cases "f x", auto) } 

1249 
{ assume "Real a < f x" "x \<notin> f ` {\<omega>}" then show "a < real (f x)" 

1250 
using `0 \<le> a` by (cases "f x", auto) } 

1251 
next 

1252 
fix x assume "\<not> 0 \<le> a" then show "a < real (f x)" by (cases "f x") auto 

1253 
qed 

1254 
then show "{w \<in> space M. a < real (f w)} \<in> sets M" 

1255 
using \<omega> * by (auto intro!: Diff) 

35582  1256 
qed 
1257 
qed 

1258 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40870
diff
changeset

1259 
lemma (in sigma_algebra) borel_measurable_pextreal_iff_less: 
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40870
diff
changeset

1260 
"(f::'a \<Rightarrow> pextreal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. {x\<in>space M. f x < a} \<in> sets M)" 
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40870
diff
changeset

1261 
using borel_measurable_pextreal_iff_greater unfolding less_eq_le_pextreal_measurable greater_eq_le_measurable . 
38656  1262 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40870
diff
changeset

1263 
lemma (in sigma_algebra) borel_measurable_pextreal_iff_le: 