author  hoelzl 
Fri, 27 Aug 2010 14:05:03 +0200  
changeset 39087  96984bf6fa5b 
parent 39083  e46acc0ea1fe 
child 39092  98de40859858 
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 

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

5 
theory Borel 
38656  6 
imports Sigma_Algebra Positive_Infinite_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 

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

10 

38656  11 
definition "borel_space = sigma (UNIV::'a::topological_space set) open" 
12 
abbreviation "borel_measurable M \<equiv> measurable M borel_space" 

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

13 

38656  14 
interpretation borel_space: sigma_algebra borel_space 
15 
using sigma_algebra_sigma by (auto simp: borel_space_def) 

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

16 

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

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

18 
"f \<in> borel_measurable M \<longleftrightarrow> 
38656  19 
(\<forall>S \<in> sets (sigma UNIV open). 
20 
f ` S \<inter> space M \<in> sets M)" 

21 
by (auto simp add: measurable_def borel_space_def) 

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

22 

38656  23 
lemma in_borel_measurable_borel_space: 
24 
"f \<in> borel_measurable M \<longleftrightarrow> 

25 
(\<forall>S \<in> sets borel_space. 

26 
f ` S \<inter> space M \<in> sets M)" 

27 
by (auto simp add: measurable_def borel_space_def) 

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

28 

38656  29 
lemma space_borel_space[simp]: "space borel_space = UNIV" 
30 
unfolding borel_space_def by auto 

31 

32 
lemma borel_space_open[simp]: 

33 
assumes "open A" shows "A \<in> sets borel_space" 

34 
proof  

35 
have "A \<in> open" unfolding mem_def using assms . 

36 
thus ?thesis unfolding borel_space_def sigma_def by (auto intro!: sigma_sets.Basic) 

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

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

38 

38656  39 
lemma borel_space_closed[simp]: 
40 
assumes "closed A" shows "A \<in> sets borel_space" 

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

41 
proof  
38656  42 
have "space borel_space  ( A) \<in> sets borel_space" 
43 
using assms unfolding closed_def by (blast intro: borel_space_open) 

44 
thus ?thesis by simp 

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

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

46 

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

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

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

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

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

53 
from closed_sing[of "f y"] 

54 
have "{f y} \<in> sets borel_space" by (rule borel_space_closed) 

55 
with assms show ?thesis 

56 
unfolding in_borel_measurable_borel_space `x = f y` by auto 

57 
next 

58 
case False hence "f ` {x} \<inter> space M = {}" by auto 

59 
thus ?thesis by auto 

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

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

61 

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

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

65 
shows "f \<in> borel_measurable M" 

66 
unfolding borel_space_def 

67 
proof (rule measurable_sigma) 

68 
fix S :: "'x set" assume "S \<in> open" thus "f ` S \<inter> space M \<in> sets M" 

69 
using assms[of S] by (simp add: mem_def) 

70 
qed simp_all 

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

71 

38656  72 
lemma borel_space_singleton[simp, intro]: 
73 
fixes x :: "'a::t1_space" 

74 
shows "A \<in> sets borel_space \<Longrightarrow> insert x A \<in> sets borel_space" 

75 
proof (rule borel_space.insert_in_sets) 

76 
show "{x} \<in> sets borel_space" 

77 
using closed_sing[of x] by (rule borel_space_closed) 

78 
qed simp 

79 

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

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

82 
by (auto intro!: measurable_const) 

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

83 

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

87 
unfolding indicator_def_raw using A 

88 
by (auto intro!: measurable_If_set borel_measurable_const) 

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

89 

38656  90 
lemma borel_measurable_translate: 
91 
assumes "A \<in> sets borel_space" and trans: "\<And>B. open B \<Longrightarrow> f ` B \<in> sets borel_space" 

92 
shows "f ` A \<in> sets borel_space" 

93 
proof  

94 
have "A \<in> sigma_sets UNIV open" using assms 

95 
by (simp add: borel_space_def sigma_def) 

96 
thus ?thesis 

97 
proof (induct rule: sigma_sets.induct) 

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

99 
next 

100 
case (Compl a) 

101 
moreover have "UNIV \<in> sets borel_space" 

102 
by (metis borel_space.top borel_space_def_raw mem_def space_sigma) 

103 
ultimately show ?case 

104 
by (auto simp: vimage_Diff borel_space.Diff) 

105 
qed (auto simp add: vimage_UN) 

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

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

107 

38656  108 
section "Borel spaces on euclidean spaces" 
109 

110 
lemma lessThan_borel[simp, intro]: 

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

112 
shows "{..< a} \<in> sets borel_space" 

113 
by (blast intro: borel_space_open) 

114 

115 
lemma greaterThan_borel[simp, intro]: 

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

117 
shows "{a <..} \<in> sets borel_space" 

118 
by (blast intro: borel_space_open) 

119 

120 
lemma greaterThanLessThan_borel[simp, intro]: 

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

122 
shows "{a<..<b} \<in> sets borel_space" 

123 
by (blast intro: borel_space_open) 

124 

125 
lemma atMost_borel[simp, intro]: 

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

127 
shows "{..a} \<in> sets borel_space" 

128 
by (blast intro: borel_space_closed) 

129 

130 
lemma atLeast_borel[simp, intro]: 

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

132 
shows "{a..} \<in> sets borel_space" 

133 
by (blast intro: borel_space_closed) 

134 

135 
lemma atLeastAtMost_borel[simp, intro]: 

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

137 
shows "{a..b} \<in> sets borel_space" 

138 
by (blast intro: borel_space_closed) 

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

139 

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

142 
shows "{a<..b} \<in> sets borel_space" 

143 
unfolding greaterThanAtMost_def by blast 

144 

145 
lemma atLeastLessThan_borel[simp, intro]: 

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

147 
shows "{a..<b} \<in> sets borel_space" 

148 
unfolding atLeastLessThan_def by blast 

149 

150 
lemma hafspace_less_borel[simp, intro]: 

151 
fixes a :: real 

152 
shows "{x::'a::euclidean_space. a < x $$ i} \<in> sets borel_space" 

153 
by (auto intro!: borel_space_open open_halfspace_component_gt) 

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

154 

38656  155 
lemma hafspace_greater_borel[simp, intro]: 
156 
fixes a :: real 

157 
shows "{x::'a::euclidean_space. x $$ i < a} \<in> sets borel_space" 

158 
by (auto intro!: borel_space_open open_halfspace_component_lt) 

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

159 

38656  160 
lemma hafspace_less_eq_borel[simp, intro]: 
161 
fixes a :: real 

162 
shows "{x::'a::euclidean_space. a \<le> x $$ i} \<in> sets borel_space" 

163 
by (auto intro!: borel_space_closed closed_halfspace_component_ge) 

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

164 

38656  165 
lemma hafspace_greater_eq_borel[simp, intro]: 
166 
fixes a :: real 

167 
shows "{x::'a::euclidean_space. x $$ i \<le> a} \<in> sets borel_space" 

168 
by (auto intro!: borel_space_closed closed_halfspace_component_le) 

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

169 

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

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

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

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

174 
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

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

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

179 
then show ?thesis using f g 

180 
by simp (blast intro: measurable_sets) 

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

181 
qed 
38656  182 

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

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

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

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

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

187 
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

188 
proof  
38656  189 
have "{w \<in> space M. f w \<le> g w} = space M  {w \<in> space M. g w < f w}" 
190 
by auto 

191 
thus ?thesis using f g 

192 
by simp blast 

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

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

194 

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

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

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

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

199 
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

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

201 
have "{w \<in> space M. f w = g w} = 
33536  202 
{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

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

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

206 

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

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

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

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

211 
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

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

213 
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

214 
by auto 
38656  215 
thus ?thesis using f g by auto 
216 
qed 

217 

218 
subsection "Borel space equals sigma algebras over intervals" 

219 

220 
lemma rational_boxes: 

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

222 
assumes "0 < e" 

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

224 
proof  

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

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

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

228 
proof 

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

230 
show "?th i" by auto 

231 
qed 

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

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

234 
proof 

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

236 
show "?th i" by auto 

237 
qed 

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

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

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

241 
unfolding setL2_def[symmetric] by (rule euclidean_dist_l2) 

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

243 
proof (rule real_sqrt_less_mono, rule setsum_strict_mono) 

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

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

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

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

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

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

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

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

252 
by (rule power_strict_mono) auto 

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

254 
by (simp add: power_divide) 

255 
qed auto 

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

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

258 
with a b show ?thesis 

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

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

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

262 
qed 

263 

264 
lemma ex_rat_list: 

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

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

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

268 
proof  

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

270 
from choice[OF this] guess r .. 

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

272 
qed 

273 

274 
lemma open_UNION: 

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

276 
assumes "open M" 

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

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

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

280 
proof safe 

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

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

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

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

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

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

287 
"length q = DIM ('a)" 

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

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

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

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

292 
unfolding o_def by auto 

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

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

295 
unfolding o_def by auto 

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

297 
using p q ab by auto 

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

299 
qed auto 

300 

301 
lemma halfspace_span_open: 

302 
"sets (sigma UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i < a}))) 

303 
\<subseteq> sets borel_space" 

304 
by (auto intro!: borel_space.sigma_sets_subset[simplified] borel_space_open 

305 
open_halfspace_component_lt simp: sets_sigma) 

306 

307 
lemma halfspace_lt_in_halfspace: 

308 
"{x\<Colon>'a. x $$ i < a} \<in> sets (sigma UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i < a})))" 

309 
unfolding sets_sigma by (rule sigma_sets.Basic) auto 

310 

311 
lemma halfspace_gt_in_halfspace: 

312 
"{x\<Colon>'a. a < x $$ i} \<in> sets (sigma UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i < a})))" 

313 
(is "?set \<in> sets ?SIGMA") 

314 
proof  

315 
interpret sigma_algebra ?SIGMA by (rule sigma_algebra_sigma) simp 

316 
have *: "?set = (\<Union>n. space ?SIGMA  {x\<Colon>'a. x $$ i < a + 1 / real (Suc n)})" 

317 
proof (safe, simp_all add: not_less) 

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

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

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

321 
by (auto simp: inverse_eq_divide field_simps) 

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

323 
by (blast intro: less_imp_le) 

324 
next 

325 
fix x n 

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

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

328 
finally show "a < x" . 

329 
qed 

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

331 
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

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

333 

38656  334 
lemma (in sigma_algebra) sets_sigma_subset: 
335 
assumes "A = space M" 

336 
assumes "B \<subseteq> sets M" 

337 
shows "sets (sigma A B) \<subseteq> sets M" 

338 
by (unfold assms sets_sigma, rule sigma_sets_subset, rule assms) 

339 

340 
lemma open_span_halfspace: 

341 
"sets borel_space \<subseteq> sets (sigma UNIV (range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. x $$ i < a})))" 

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

343 
proof (unfold borel_space_def, rule sigma_algebra.sets_sigma_subset, safe) 

344 
show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) simp 

345 
then interpret sigma_algebra ?SIGMA . 

346 
fix S :: "'a set" assume "S \<in> open" then have "open S" unfolding mem_def . 

347 
from open_UNION[OF this] 

348 
obtain I where *: "S = 

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

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

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

352 
unfolding greaterThanLessThan_def 

353 
unfolding eucl_greaterThan_eq_halfspaces[where 'a='a] 

354 
unfolding eucl_lessThan_eq_halfspaces[where 'a='a] 

355 
by blast 

356 
show "S \<in> sets ?SIGMA" 

357 
unfolding * 

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

359 
qed auto 

360 

361 
lemma halfspace_span_halfspace_le: 

362 
"sets (sigma UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i < a}))) \<subseteq> 

363 
sets (sigma UNIV (range (\<lambda> (a, i). {x. x $$ i \<le> a})))" 

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

365 
proof (rule sigma_algebra.sets_sigma_subset, safe) 

366 
show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto 

367 
then interpret sigma_algebra ?SIGMA . 

368 
fix a i 

369 
have *: "{x::'a. x$$i < a} = (\<Union>n. {x. x$$i \<le> a  1/real (Suc n)})" 

370 
proof (safe, simp_all) 

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

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

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

374 
by (auto simp: field_simps inverse_eq_divide) 

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

376 
by (blast intro: less_imp_le) 

377 
next 

378 
fix x::'a and n 

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

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

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

382 
qed 

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

384 
by (safe intro!: countable_UN) 

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

386 
qed auto 

387 

388 
lemma halfspace_span_halfspace_ge: 

389 
"sets (sigma UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i < a}))) \<subseteq> 

390 
sets (sigma UNIV (range (\<lambda> (a, i). {x. a \<le> x $$ i})))" 

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

392 
proof (rule sigma_algebra.sets_sigma_subset, safe) 

393 
show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto 

394 
then interpret sigma_algebra ?SIGMA . 

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

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

397 
by (safe intro!: Diff) 

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

399 
qed auto 

400 

401 
lemma halfspace_le_span_halfspace_gt: 

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

403 
sets (sigma UNIV (range (\<lambda> (a, i). {x. a < x $$ i})))" 

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

405 
proof (rule sigma_algebra.sets_sigma_subset, safe) 

406 
show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto 

407 
then interpret sigma_algebra ?SIGMA . 

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

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

410 
by (safe intro!: Diff) 

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

412 
qed auto 

413 

414 
lemma halfspace_le_span_atMost: 

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

416 
sets (sigma UNIV (range (\<lambda>a. {..a\<Colon>'a\<Colon>ordered_euclidean_space})))" 

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

418 
proof (rule sigma_algebra.sets_sigma_subset, safe) 

419 
show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto 

420 
then interpret sigma_algebra ?SIGMA . 

421 
fix a i 

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

423 
proof cases 

424 
assume "i < DIM('a)" 

425 
then have *: "{x::'a. x$$i \<le> a} = (\<Union>k::nat. {.. (\<chi>\<chi> n. if n = i then a else real k)})" 

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

427 
fix x 

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

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

430 
by (subst (asm) Max_le_iff) auto 

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

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

433 
qed 

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

435 
by (safe intro!: countable_UN) 

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

437 
next 

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

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

440 
using top by auto 

441 
qed 

442 
qed auto 

443 

444 
lemma halfspace_le_span_greaterThan: 

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

446 
sets (sigma UNIV (range (\<lambda>a. {a<..})))" 

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

448 
proof (rule sigma_algebra.sets_sigma_subset, safe) 

449 
show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto 

450 
then interpret sigma_algebra ?SIGMA . 

451 
fix a i 

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

453 
proof cases 

454 
assume "i < DIM('a)" 

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

456 
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)` 

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

458 
fix x 

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

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

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

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

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

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

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

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

467 
qed 

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

469 
apply (simp only:) 

470 
apply (safe intro!: countable_UN Diff) 

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

472 
next 

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

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

475 
using top by auto 

476 
qed 

477 
qed auto 

478 

479 
lemma atMost_span_atLeastAtMost: 

480 
"sets (sigma UNIV (range (\<lambda>a. {..a\<Colon>'a\<Colon>ordered_euclidean_space}))) \<subseteq> 

481 
sets (sigma UNIV (range (\<lambda>(a,b). {a..b})))" 

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

483 
proof (rule sigma_algebra.sets_sigma_subset, safe) 

484 
show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto 

485 
then interpret sigma_algebra ?SIGMA . 

486 
fix a::'a 

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

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

489 
fix x 

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

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

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

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

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

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

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

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

498 
qed 

499 
show "{..a} \<in> sets ?SIGMA" unfolding * 

500 
by (safe intro!: countable_UN) 

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

502 
qed auto 

503 

504 
lemma borel_space_eq_greaterThanLessThan: 

505 
"sets borel_space = sets (sigma UNIV (range (\<lambda> (a, b). {a <..< (b :: 'a \<Colon> ordered_euclidean_space)})))" 

506 
(is "_ = sets ?SIGMA") 

507 
proof (rule antisym) 

508 
show "sets ?SIGMA \<subseteq> sets borel_space" 

509 
by (rule borel_space.sets_sigma_subset) auto 

510 
show "sets borel_space \<subseteq> sets ?SIGMA" 

511 
unfolding borel_space_def 

512 
proof (rule sigma_algebra.sets_sigma_subset, safe) 

513 
show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto 

514 
then interpret sigma_algebra ?SIGMA . 

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

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

517 
show "M \<in> sets ?SIGMA" 

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

519 
apply (safe intro!: countable_UN) 

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

521 
qed auto 

522 
qed 

523 

524 
lemma borel_space_eq_atMost: 

525 
"sets borel_space = sets (sigma UNIV (range (\<lambda> a. {.. a::'a\<Colon>ordered_euclidean_space})))" 

526 
(is "_ = sets ?SIGMA") 

527 
proof (rule antisym) 

528 
show "sets borel_space \<subseteq> sets ?SIGMA" 

529 
using halfspace_le_span_atMost halfspace_span_halfspace_le open_span_halfspace 

530 
by auto 

531 
show "sets ?SIGMA \<subseteq> sets borel_space" 

532 
by (rule borel_space.sets_sigma_subset) auto 

533 
qed 

534 

535 
lemma borel_space_eq_atLeastAtMost: 

536 
"sets borel_space = sets (sigma UNIV (range (\<lambda> (a :: 'a\<Colon>ordered_euclidean_space, b). {a .. b})))" 

537 
(is "_ = sets ?SIGMA") 

538 
proof (rule antisym) 

539 
show "sets borel_space \<subseteq> sets ?SIGMA" 

540 
using atMost_span_atLeastAtMost halfspace_le_span_atMost 

541 
halfspace_span_halfspace_le open_span_halfspace 

542 
by auto 

543 
show "sets ?SIGMA \<subseteq> sets borel_space" 

544 
by (rule borel_space.sets_sigma_subset) auto 

545 
qed 

546 

547 
lemma borel_space_eq_greaterThan: 

548 
"sets borel_space = sets (sigma UNIV (range (\<lambda> (a :: 'a\<Colon>ordered_euclidean_space). {a <..})))" 

549 
(is "_ = sets ?SIGMA") 

550 
proof (rule antisym) 

551 
show "sets borel_space \<subseteq> sets ?SIGMA" 

552 
using halfspace_le_span_greaterThan 

553 
halfspace_span_halfspace_le open_span_halfspace 

554 
by auto 

555 
show "sets ?SIGMA \<subseteq> sets borel_space" 

556 
by (rule borel_space.sets_sigma_subset) auto 

557 
qed 

558 

559 
lemma borel_space_eq_halfspace_le: 

560 
"sets borel_space = sets (sigma UNIV (range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. x$$i \<le> a})))" 

561 
(is "_ = sets ?SIGMA") 

562 
proof (rule antisym) 

563 
show "sets borel_space \<subseteq> sets ?SIGMA" 

564 
using open_span_halfspace halfspace_span_halfspace_le by auto 

565 
show "sets ?SIGMA \<subseteq> sets borel_space" 

566 
by (rule borel_space.sets_sigma_subset) auto 

567 
qed 

568 

569 
lemma borel_space_eq_halfspace_less: 

570 
"sets borel_space = sets (sigma UNIV (range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. x$$i < a})))" 

571 
(is "_ = sets ?SIGMA") 

572 
proof (rule antisym) 

573 
show "sets borel_space \<subseteq> sets ?SIGMA" 

574 
using open_span_halfspace . 

575 
show "sets ?SIGMA \<subseteq> sets borel_space" 

576 
by (rule borel_space.sets_sigma_subset) auto 

577 
qed 

578 

579 
lemma borel_space_eq_halfspace_gt: 

580 
"sets borel_space = sets (sigma UNIV (range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. a < x$$i})))" 

581 
(is "_ = sets ?SIGMA") 

582 
proof (rule antisym) 

583 
show "sets borel_space \<subseteq> sets ?SIGMA" 

584 
using halfspace_le_span_halfspace_gt open_span_halfspace halfspace_span_halfspace_le by auto 

585 
show "sets ?SIGMA \<subseteq> sets borel_space" 

586 
by (rule borel_space.sets_sigma_subset) auto 

587 
qed 

588 

589 
lemma borel_space_eq_halfspace_ge: 

590 
"sets borel_space = sets (sigma UNIV (range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. a \<le> x$$i})))" 

591 
(is "_ = sets ?SIGMA") 

592 
proof (rule antisym) 

593 
show "sets borel_space \<subseteq> sets ?SIGMA" 

594 
using halfspace_span_halfspace_ge open_span_halfspace by auto 

595 
show "sets ?SIGMA \<subseteq> sets borel_space" 

596 
by (rule borel_space.sets_sigma_subset) auto 

597 
qed 

598 

599 
lemma (in sigma_algebra) borel_measurable_halfspacesI: 

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

601 
assumes "sets borel_space = sets (sigma UNIV (range F))" 

602 
and "\<And>a i. S a i = f ` F (a,i) \<inter> space M" 

603 
and "\<And>a i. \<not> i < DIM('c) \<Longrightarrow> S a i \<in> sets M" 

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

605 
proof safe 

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

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

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

609 
next 

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

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

612 
proof cases 

613 
assume "i < DIM('c)" 

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

615 
next 

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

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

618 
qed } 

619 
then have "f \<in> measurable M (sigma UNIV (range F))" 

620 
by (auto intro!: measurable_sigma simp: assms(2)) 

621 
then show "f \<in> borel_measurable M" unfolding measurable_def 

622 
unfolding assms(1) by simp 

623 
qed 

624 

625 
lemma (in sigma_algebra) borel_measurable_iff_halfspace_le: 

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

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

628 
by (rule borel_measurable_halfspacesI[OF borel_space_eq_halfspace_le]) auto 

629 

630 
lemma (in sigma_algebra) borel_measurable_iff_halfspace_less: 

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

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

633 
by (rule borel_measurable_halfspacesI[OF borel_space_eq_halfspace_less]) auto 

634 

635 
lemma (in sigma_algebra) borel_measurable_iff_halfspace_ge: 

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

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

638 
by (rule borel_measurable_halfspacesI[OF borel_space_eq_halfspace_ge]) auto 

639 

640 
lemma (in sigma_algebra) borel_measurable_iff_halfspace_greater: 

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

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

643 
by (rule borel_measurable_halfspacesI[OF borel_space_eq_halfspace_gt]) auto 

644 

645 
lemma (in sigma_algebra) borel_measurable_iff_le: 

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

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

648 

649 
lemma (in sigma_algebra) borel_measurable_iff_less: 

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

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

652 

653 
lemma (in sigma_algebra) borel_measurable_iff_ge: 

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

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

656 

657 
lemma (in sigma_algebra) borel_measurable_iff_greater: 

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

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

660 

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

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

662 
"(\<lambda>x::'a::euclidean_space. x $$ i) \<in> borel_measurable borel_space" 
96984bf6fa5b
Measurable on euclidean space is equiv. to measurable components
hoelzl
parents:
39083
diff
changeset

663 
unfolding borel_space_def[where 'a=real] 
96984bf6fa5b
Measurable on euclidean space is equiv. to measurable components
hoelzl
parents:
39083
diff
changeset

664 
proof (rule borel_space.measurable_sigma) 
96984bf6fa5b
Measurable on euclidean space is equiv. to measurable components
hoelzl
parents:
39083
diff
changeset

665 
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

666 
from open_vimage_euclidean_component[OF this] 
96984bf6fa5b
Measurable on euclidean space is equiv. to measurable components
hoelzl
parents:
39083
diff
changeset

667 
show "(\<lambda>x. x $$ i) ` S \<inter> space borel_space \<in> sets borel_space" 
96984bf6fa5b
Measurable on euclidean space is equiv. to measurable components
hoelzl
parents:
39083
diff
changeset

668 
by (auto intro: borel_space_open) 
96984bf6fa5b
Measurable on euclidean space is equiv. to measurable components
hoelzl
parents:
39083
diff
changeset

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

670 

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

671 
lemma (in sigma_algebra) borel_measureable_euclidean_space: 
96984bf6fa5b
Measurable on euclidean space is equiv. to measurable components
hoelzl
parents:
39083
diff
changeset

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

673 
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

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

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

676 
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

677 
using measurable_comp[of f _ _ "\<lambda>x. x $$ i", unfolded comp_def] 
96984bf6fa5b
Measurable on euclidean space is equiv. to measurable components
hoelzl
parents:
39083
diff
changeset

678 
by (auto intro: borel_measureable_euclidean_component) 
96984bf6fa5b
Measurable on euclidean space is equiv. to measurable components
hoelzl
parents:
39083
diff
changeset

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

680 
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

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

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

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

684 

38656  685 
subsection "Borel measurable operators" 
686 

687 
lemma (in sigma_algebra) affine_borel_measurable_vector: 

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

689 
assumes "f \<in> borel_measurable M" 

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

691 
proof (rule borel_measurableI) 

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

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

694 
proof cases 

695 
assume "b \<noteq> 0" 

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

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

698 
hence "?S \<in> sets borel_space" 

699 
unfolding borel_space_def by (auto simp: sigma_def intro!: sigma_sets.Basic) 

700 
moreover 

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

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

703 
ultimately show ?thesis using assms unfolding in_borel_measurable_borel_space 

704 
by auto 

705 
qed simp 

706 
qed 

707 

708 
lemma (in sigma_algebra) affine_borel_measurable: 

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

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

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

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

713 

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

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

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

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

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

718 
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

719 
proof  
38656  720 
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

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

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

725 
by auto 

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

727 
by (simp add: 1) 

728 
then show ?thesis 

729 
by (simp add: borel_measurable_iff_ge) 

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

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

731 

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

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

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

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

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

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

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

739 
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

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

741 
case less 
38656  742 
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

743 
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

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

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

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

748 
case equal 
38656  749 
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

750 
{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

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

752 
also have "... \<in> sets M" 
38656  753 
apply (insert f) 
754 
apply (rule Int) 

755 
apply (simp add: borel_measurable_iff_le) 

756 
apply (simp add: borel_measurable_iff_ge) 

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

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

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

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

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

761 
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

762 
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

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

764 
hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} = 
38656  765 
{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

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

767 
also have "... \<in> sets M" 
38656  768 
apply (insert f) 
769 
apply (rule Int) 

770 
apply (simp add: borel_measurable_iff_ge) 

771 
apply (simp add: borel_measurable_iff_le) 

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

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

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

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

775 
} 
38656  776 
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

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

778 

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

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

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

781 
shows"x*y = ((x+y)^2)/4  ((xy)^ 2)/4" 
38656  782 
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

783 

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

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

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

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

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

789 
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

790 
by simp 
38656  791 
also have "... \<in> borel_measurable M" 
792 
by (fast intro: affine_borel_measurable g) 

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

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

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

795 

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

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

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

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

800 
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

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

802 
have 1: "(\<lambda>x. 0 + (f x + g x)\<twosuperior> * inverse 4) \<in> borel_measurable M" 
38656  803 
using assms by (fast intro: affine_borel_measurable borel_measurable_square) 
804 
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

805 
(\<lambda>x. 0 + ((f x + g x) ^ 2 * inverse 4))" 
35582  806 
by (simp add: minus_divide_right) 
38656  807 
also have "... \<in> borel_measurable M" 
808 
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

809 
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

810 
show ?thesis 
38656  811 
apply (simp add: times_eq_sum_squares diff_minus) 
812 
using 1 2 by simp 

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

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

814 

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

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

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

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

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

821 

38656  822 
lemma (in sigma_algebra) borel_measurable_setsum[simp, intro]: 
823 
fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real" 

824 
assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M" 

825 
shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M" 

826 
proof cases 

827 
assume "finite S" 

828 
thus ?thesis using assms by induct auto 

829 
qed simp 

35692  830 

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

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

38656  835 
unfolding borel_measurable_iff_ge unfolding inverse_eq_divide 
836 
proof safe 

837 
fix a :: real 

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

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

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

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

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

843 
by (auto intro!: Int Un) 

35692  844 
qed 
845 

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

35692  848 
assumes "f \<in> borel_measurable M" 
849 
and "g \<in> borel_measurable M" 

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

851 
unfolding field_divide_inverse 

38656  852 
by (rule borel_measurable_inverse borel_measurable_times assms)+ 
853 

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

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

856 
assumes "f \<in> borel_measurable M" 

857 
assumes "g \<in> borel_measurable M" 

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

859 
unfolding borel_measurable_iff_le 

860 
proof safe 

861 
fix a 

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

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

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

865 
using assms unfolding borel_measurable_iff_le 

866 
by (auto intro!: Int) 

867 
qed 

868 

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

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

871 
assumes "f \<in> borel_measurable M" 

872 
assumes "g \<in> borel_measurable M" 

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

874 
unfolding borel_measurable_iff_ge 

875 
proof safe 

876 
fix a 

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

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

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

880 
using assms unfolding borel_measurable_iff_ge 

881 
by (auto intro!: Int) 

882 
qed 

883 

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

885 
assumes "f \<in> borel_measurable M" 

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

887 
proof  

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

889 
show ?thesis unfolding * using assms by auto 

890 
qed 

891 

892 
section "Borel space over the real line with infinity" 

35692  893 

38656  894 
lemma borel_space_Real_measurable: 
895 
"A \<in> sets borel_space \<Longrightarrow> Real ` A \<in> sets borel_space" 

896 
proof (rule borel_measurable_translate) 

897 
fix B :: "pinfreal set" assume "open B" 

898 
then obtain T x where T: "open T" "Real ` (T \<inter> {0..}) = B  {\<omega>}" and 

899 
x: "\<omega> \<in> B \<Longrightarrow> 0 \<le> x" "\<omega> \<in> B \<Longrightarrow> {Real x <..} \<subseteq> B" 

900 
unfolding open_pinfreal_def by blast 

901 

902 
have "Real ` B = Real ` (B  {\<omega>})" by auto 

903 
also have "\<dots> = Real ` (Real ` (T \<inter> {0..}))" using T by simp 

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

905 
apply (auto simp add: Real_eq_Real image_iff) 

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

907 
by (auto simp: max_def) 

908 
finally show "Real ` B \<in> sets borel_space" 

909 
using `open T` by auto 

910 
qed simp 

911 

912 
lemma borel_space_real_measurable: 

913 
"A \<in> sets borel_space \<Longrightarrow> (real ` A :: pinfreal set) \<in> sets borel_space" 

914 
proof (rule borel_measurable_translate) 

915 
fix B :: "real set" assume "open B" 

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

917 
note Ex_less_real = this 

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

919 
by (force simp: Ex_less_real) 

920 

921 
have "open (real ` (B \<inter> {0 <..}) :: pinfreal set)" 

922 
unfolding open_pinfreal_def using `open B` 

923 
by (auto intro!: open_Int exI[of _ "B \<inter> {0 <..}"] simp: image_iff Ex_less_real) 

924 
then show "(real ` B :: pinfreal set) \<in> sets borel_space" unfolding * by auto 

925 
qed simp 

926 

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

928 
assumes "f \<in> borel_measurable M" 

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

930 
unfolding in_borel_measurable_borel_space 

931 
proof safe 

932 
fix S :: "pinfreal set" assume "S \<in> sets borel_space" 

933 
from borel_space_Real_measurable[OF this] 

934 
have "(Real \<circ> f) ` S \<inter> space M \<in> sets M" 

935 
using assms 

936 
unfolding vimage_compose in_borel_measurable_borel_space 

937 
by auto 

938 
thus "(\<lambda>x. Real (f x)) ` S \<inter> space M \<in> sets M" by (simp add: comp_def) 

35748  939 
qed 
35692  940 

38656  941 
lemma (in sigma_algebra) borel_measurable_real[intro, simp]: 
942 
fixes f :: "'a \<Rightarrow> pinfreal" 

943 
assumes "f \<in> borel_measurable M" 

944 
shows "(\<lambda>x. real (f x)) \<in> borel_measurable M" 

945 
unfolding in_borel_measurable_borel_space 

946 
proof safe 

947 
fix S :: "real set" assume "S \<in> sets borel_space" 

948 
from borel_space_real_measurable[OF this] 

949 
have "(real \<circ> f) ` S \<inter> space M \<in> sets M" 

950 
using assms 

951 
unfolding vimage_compose in_borel_measurable_borel_space 

952 
by auto 

953 
thus "(\<lambda>x. real (f x)) ` S \<inter> space M \<in> sets M" by (simp add: comp_def) 

954 
qed 

35692  955 

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

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

959 
proof 

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

961 
by auto 

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

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

964 
by (rule borel_measurable_real) 

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

966 
using assms by auto 

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

968 
by (simp cong: measurable_cong) 

969 
qed auto 

35692  970 

38656  971 
lemma (in sigma_algebra) borel_measurable_pinfreal_eq_real: 
972 
"f \<in> borel_measurable M \<longleftrightarrow> 

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

974 
proof safe 

975 
assume "f \<in> borel_measurable M" 

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

977 
by (auto intro: borel_measurable_vimage borel_measurable_real) 

978 
next 

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

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

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

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

983 
by (simp add: expand_fun_eq Real_real) 

984 
show "f \<in> borel_measurable M" 

985 
apply (subst f) 

986 
apply (rule measurable_If) 

987 
using * ** by auto 

988 
qed 

989 

990 
lemma (in sigma_algebra) less_eq_ge_measurable: 

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

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

993 
proof 

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

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

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

997 
next 

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

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

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

1001 
qed 

35692  1002 

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

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

1006 
proof 

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

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

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

1010 
next 

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

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

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

1014 
qed 

1015 

1016 
lemma (in sigma_algebra) less_eq_le_pinfreal_measurable: 

1017 
fixes f :: "'a \<Rightarrow> pinfreal" 

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

1019 
proof 

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

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

1022 
proof 

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

1024 
proof (cases a) 

1025 
case (preal r) 

1026 
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

1027 
proof safe 
38656  1028 
fix x assume "a < f x" and [simp]: "x \<in> space M" 
1029 
with ex_pinfreal_inverse_of_nat_Suc_less[of "f x  a"] 

1030 
obtain n where "a + inverse (of_nat (Suc n)) < f x" 

1031 
by (cases "f x", auto simp: pinfreal_minus_order) 

1032 
then have "a + inverse (of_nat (Suc n)) \<le> f x" by simp 

1033 
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

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

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

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

1039 
finally show "a < f x" . 

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

1040 
qed 
38656  1041 
with a show ?thesis by auto 
1042 
qed simp 

35582  1043 
qed 
1044 
next 

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

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

1048 
proof 

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

1050 
proof (cases a) 

1051 
case (preal r) 

1052 
show ?thesis 

1053 
proof cases 

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

1055 
next 

1056 
assume "a \<noteq> 0" 

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

1058 
proof safe 

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

1060 
with ex_pinfreal_inverse_of_nat_Suc_less[of "a  f x"] 

1061 
obtain n where "inverse (of_nat (Suc n)) < a  f x" 

1062 
using preal by (cases "f x") auto 

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

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

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

1066 
by auto 

1067 
next 

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

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

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

1071 
finally show "f x < a" . 

1072 
qed 

1073 
with a show ?thesis by auto 

1074 
qed 

1075 
next 

1076 
case infinite 

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

1078 
proof (safe, simp_all, safe) 

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

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

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

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

1083 
by (auto simp: pinfreal_noteq_omega_Ex) 

1084 
with *[THEN spec, of n] show False by auto 

1085 
qed 

1086 
qed 

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

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

1089 
using infinite by auto 

1090 
ultimately show ?thesis by auto 

1091 
qed 

35582  1092 
qed 
1093 
qed 

1094 

38656  1095 
lemma (in sigma_algebra) borel_measurable_pinfreal_iff_greater: 
1096 
"(f::'a \<Rightarrow> pinfreal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. {x\<in>space M. a < f x} \<in> sets M)" 

1097 
proof safe 

1098 
fix a assume f: "f \<in> borel_measurable M" 

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

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

1101 
by (auto intro!: measurable_sets) 

1102 
next 

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

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

1105 
unfolding less_eq_le_pinfreal_measurable 

1106 
unfolding greater_eq_le_measurable . 

35582  1107 

38656  1108 
show "f \<in> borel_measurable M" unfolding borel_measurable_pinfreal_eq_real borel_measurable_iff_greater 
1109 
proof safe 

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

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

35582  1112 

38656  1113 
fix a 
1114 
have "{w \<in> space M. a < real (f w)} = 

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

1116 
proof (split split_if, safe del: notI) 

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

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

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

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

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

1122 
next 

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

1124 
qed 

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

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

35582  1127 
qed 
1128 
qed 

1129 

38656  1130 
lemma (in sigma_algebra) borel_measurable_pinfreal_iff_less: 
1131 
"(f::'a \<Rightarrow> pinfreal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. {x\<in>space M. f x < a} \<in> sets M)" 

1132 
using borel_measurable_pinfreal_iff_greater unfolding less_eq_le_pinfreal_measurable greater_eq_le_measurable . 

1133 

1134 
lemma (in sigma_algebra) borel_measurable_pinfreal_iff_le: 

1135 
"(f::'a \<Rightarrow> pinfreal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. {x\<in>space M. f x \<le> a} \<in> sets M)" 

1136 
using borel_measurable_pinfreal_iff_greater unfolding less_eq_ge_measurable . 

1137 

1138 
lemma (in sigma_algebra) borel_measurable_pinfreal_iff_ge: 

1139 
"(f::'a \<Rightarrow> pinfreal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. {x\<in>space M. a \<le> f x} \<in> sets M)" 

1140 
using borel_measurable_pinfreal_iff_greater unfolding less_eq_le_pinfreal_measurable . 

1141 

1142 
lemma (in sigma_algebra) borel_measurable_pinfreal_eq_const: 

1143 
fixes f :: "'a \<Rightarrow> pinfreal" assumes "f \<in> borel_measurable M" 

1144 
shows "{x\<in>space M. f x = c} \<in> sets M" 

1145 
proof  

1146 
have "{x\<in>space M. f x = c} = (f ` {c} \<inter> space M)" by auto 

1147 
then show ?thesis using assms by (auto intro!: measurable_sets) 

1148 
qed 

1149 

1150 
lemma (in sigma_algebra) borel_measurable_pinfreal_neq_const: 

1151 
fixes f :: "'a \<Rightarrow> pinfreal" 

1152 
assumes "f \<in> borel_measurable M" 

1153 
shows "{x\<in>space M. f x \<noteq> c} \<in> sets M" 

1154 
proof  

1155 
have "{x\<in>space M. f x \<noteq> c} = space M  (f ` {c} \<inter> space M)" by auto 

1156 
then show ?thesis using assms by (auto intro!: measurable_sets) 

1157 
qed 

1158 

1159 
lemma (in sigma_algebra) borel_measurable_pinfreal_less[intro,simp]: 

1160 
fixes f g :: "'a \<Rightarrow> pinfreal" 

1161 
assumes f: "f \<in> borel_measurable M" 

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

1163 
shows "{x \<in> space M. f x < g x} \<in> sets M" 

1164 
proof  

1165 
have "(\<lambda>x. real (f x)) \<in> borel_measurable M" 

1166 
"(\<lambda>x. real (g x)) \<in> borel_measurable M" 

1167 
using assms by (auto intro!: borel_measurable_real) 

1168 
from borel_measurable_less[OF this] 

1169 
have "{x \<in> space M. real (f x) < real (g x)} \<in> sets M" . 

1170 
moreover have "{x \<in> space M. f x \<noteq> \<omega>} \<in> sets M" using f by (rule borel_measurable_pinfreal_neq_const) 

1171 
moreover have "{x \<in> space M. g x = \<omega>} \<in> sets M" using g by (rule borel_measurable_pinfreal_eq_const) 

1172 
moreover have "{x \<in> space M. g x \<noteq> \<omega>} \<in> sets M" using g by (rule borel_measurable_pinfreal_neq_const) 

1173 
moreover have "{x \<in> space M. f x < g x} = ({x \<in> space M. g x = \<omega>} \<inter> {x \<in> space M. f x \<noteq> \<omega>}) \<union> 

1174 
({x \<in> space M. g x \<noteq> \<omega>} \<inter> {x \<in> space M. f x \<noteq> \<omega>} \<inter> {x \<in> space M. real (f x) < real (g x)})" 

1175 
by (auto simp: real_of_pinfreal_strict_mono_iff) 

1176 
ultimately show ?thesis by auto 

1177 
qed 

1178 

1179 
lemma (in sigma_algebra) borel_measurable_pinfreal_le[intro,simp]: 

1180 
fixes f :: "'a \<Rightarrow> pinfreal" 

1181 
assumes f: "f \<in> borel_measurable M" 

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

1183 
shows "{x \<in> space M. f x \<le> g x} \<in> sets M" 

1184 
proof  

1185 
have "{x \<in> space M. f x \<le> g x} = space M  {x \<in> space M. g x < f x}" by auto 

1186 
then show ?thesis using g f by auto 

1187 
qed 

1188 

1189 
lemma (in sigma_algebra) borel_measurable_pinfreal_eq[intro,simp]: 

1190 
fixes f :: "'a \<Rightarrow> pinfreal" 

1191 
assumes f: "f \<in> borel_measurable M" 

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

1193 
shows "{w \<in> space M. f w = g w} \<in> sets M" 

1194 
proof  

1195 
have "{x \<in> space M. f x = g x} = {x \<in> space M. g x \<le> f x} \<inter> {x \<in> space M. f x \<le> g x}" by auto 

1196 
then show ?thesis using g f by auto 

1197 
qed 

1198 

1199 
lemma (in sigma_algebra) borel_measurable_pinfreal_neq[intro,simp]: 

1200 
fixes f :: "'a \<Rightarrow> pinfreal" 

1201 
assumes f: "f \<in> borel_measurable M" 

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

1203 
shows "{w \<in> space M. f w \<noteq> g w} \<in> sets M" 

35692  1204 
proof  
38656  1205 
have "{w \<in> space M. f w \<noteq> g w} = space M  {w \<in> space M. f w = g w}" by auto 
1206 
thus ?thesis using f g by auto 

1207 
qed 

1208 

1209 
lemma (in sigma_algebra) borel_measurable_pinfreal_add[intro, simp]: 

1210 
fixes f :: "'a \<Rightarrow> pinfreal" 

1211 
assumes measure: "f \<in> borel_measurable M" "g \<in> borel_measurable M" 

1212 
shows "(\<lambda>x. f x + g x) \<in> borel_measurable M" 

1213 
proof  

1214 
have *: "(\<lambda>x. f x + g x) = 

1215 
(\<lambda>x. if f x = \<omega> then \<omega> else if g x = \<omega> then \<omega> else Real (real (f x) + real (g x)))" 

1216 
by (auto simp: expand_fun_eq pinfreal_noteq_omega_Ex) 

1217 
show ?thesis using assms unfolding * 

1218 
by (auto intro!: measurable_If) 

1219 
qed 

1220 

1221 
lemma (in sigma_algebra) borel_measurable_pinfreal_times[intro, simp]: 

1222 
fixes f :: "'a \<Rightarrow> pinfreal" assumes "f \<in> borel_measurable M" "g \<in> borel_measurable M" 

1223 
shows "(\<lambda>x. f x * g x) \<in> borel_measurable M" 

1224 
proof  

1225 
have *: "(\<lambda>x. f x * g x) = 

1226 
(\<lambda>x. if f x = 0 then 0 else if g x = 0 then 0 else if f x = \<omega> then \<omega> else if g x = \<omega> then \<omega> else 

1227 
Real (real (f x) * real (g x)))" 

1228 
by (auto simp: expand_fun_eq pinfreal_noteq_omega_Ex) 

1229 
show ?thesis using assms unfolding * 

1230 
by (auto intro!: measurable_If) 

1231 
qed 

1232 

1233 
lemma (in sigma_algebra) borel_measurable_pinfreal_setsum[simp, intro]: 

1234 
fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> pinfreal" 

1235 
assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M" 

1236 
shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M" 

1237 
proof cases 

1238 
assume "finite S" 

1239 
thus ?thesis using assms 

1240 
by induct auto 

1241 
qed (simp add: borel_measurable_const) 

1242 

1243 
lemma (in sigma_algebra) borel_measurable_pinfreal_min[intro, simp]: 

1244 
fixes f g :: "'a \<Rightarrow> pinfreal" 

1245 
assumes "f \<in> borel_measurable M" 

1246 
assumes "g \<in> borel_measurable M" 

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

1248 
using assms unfolding min_def by (auto intro!: measurable_If) 

1249 

1250 
lemma (in sigma_algebra) borel_measurable_pinfreal_max[intro]: 

1251 
fixes f g :: "'a \<Rightarrow> pinfreal" 

1252 
assumes "f \<in> borel_measurable M" 

1253 
and "g \<in> borel_measurable M" 

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

1255 
using assms unfolding max_def by (auto intro!: measurable_If) 

1256 

1257 
lemma (in sigma_algebra) borel_measurable_SUP[simp, intro]: 

1258 
fixes f :: "'d\<Colon>countable \<Rightarrow> 'a \<Rightarrow> pinfreal" 

1259 
assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M" 

1260 
shows "(SUP i : A. f i) \<in> borel_measurable M" (is "?sup \<in> borel_measurable M") 

1261 
unfolding borel_measurable_pinfreal_iff_greater 

1262 
proof safe 

1263 
fix a 

1264 
have "{x\<in>space M. a < ?sup x} = (\<Union>i\<in>A. {x\<in>space M. a < f i x})" 

38705  1265 
by (auto simp: less_Sup_iff SUPR_def[where 'a=pinfreal] SUPR_fun_expand[where 'c=pinfreal]) 
38656  1266 
then show "{x\<in>space M. a < ?sup x} \<in> sets M" 
1267 
using assms by auto 

1268 
qed 

1269 

1270 
lemma (in sigma_algebra) borel_measurable_INF[simp, intro]: 

1271 
fixes f :: "'d :: countable \<Rightarrow> 'a \<Rightarrow> pinfreal" 

1272 
assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M" 

1273 
shows "(INF i : A. f i) \<in> borel_measurable M" (is "?inf \<in> borel_measurable M") 

1274 
unfolding borel_measurable_pinfreal_iff_less 

1275 
proof safe 

1276 
fix a 

1277 
have "{x\<in>space M. ?inf x < a} = (\<Union>i\<in>A. {x\<in>space M. f i x < a})" 

1278 
by (auto simp: Inf_less_iff INFI_def[where 'a=pinfreal] INFI_fun_expand) 

1279 
then show "{x\<in>space M. ?inf x < a} \<in> sets M" 

1280 
using assms by auto 

1281 
qed 

1282 

1283 
lemma (in sigma_algebra) borel_measurable_pinfreal_diff: 

1284 
fixes f g :: "'a \<Rightarrow> pinfreal" 

1285 
assumes "f \<in> borel_measurable M" 

1286 
assumes "g \<in> borel_measurable M" 

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

1288 
unfolding borel_measurable_pinfreal_iff_greater 

1289 
proof safe 

1290 
fix a 

1291 
have "{x \<in> space M. a < f x  g x} = {x \<in> space M. g x + a < f x}" 

1292 
by (simp add: pinfreal_less_minus_iff) 

1293 
then show "{x \<in> space M. a < f x  g x} \<in> sets M" 

1294 
using assms by auto 

35692  1295 
qed 
1296 

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

1297 
end 