author  hoelzl 
Mon, 14 Mar 2011 14:37:49 +0100  
changeset 41981  cdf7693bbe08 
parent 41969  1cf3e4107a2a 
child 42067  66c8281349ec 
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 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

6 
imports Sigma_Algebra 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 

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

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

13 

40859  14 
interpretation borel: sigma_algebra borel 
15 
by (auto simp: borel_def intro!: sigma_algebra_sigma) 

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> 
40859  19 
(\<forall>S \<in> sets (sigma \<lparr> space = UNIV, sets = open\<rparr>). 
38656  20 
f ` S \<inter> space M \<in> sets M)" 
40859  21 
by (auto simp add: measurable_def borel_def) 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

22 

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

28 

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

38656  31 

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

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

40859  36 
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

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

38 

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

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

41 
proof  
40859  42 
have "space borel  ( A) \<in> sets borel" 
43 
using assms unfolding closed_def by (blast intro: borel_open) 

38656  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 

41830  47 
lemma borel_comp[intro,simp]: "A \<in> sets borel \<Longrightarrow>  A \<in> sets borel" 
48 
unfolding Compl_eq_Diff_UNIV by (intro borel.Diff) auto 

49 

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

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

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

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

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

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

62 
thus ?thesis by auto 

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

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

64 

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

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

68 
shows "f \<in> borel_measurable M" 

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

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

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

74 

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

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

41969  80 
using closed_singleton[of x] by (rule borel_closed) 
38656  81 
qed simp 
82 

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

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

85 
by (auto intro!: measurable_const) 

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

86 

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

90 
unfolding indicator_def_raw using A 

91 
by (auto intro!: measurable_If_set borel_measurable_const) 

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

92 

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

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

96 
proof 

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

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

99 
unfolding measurable_def by auto 

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

101 
unfolding indicator_def_raw by auto 

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

103 
next 

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

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

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

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

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

109 
qed 

110 

39092  111 
lemma (in sigma_algebra) borel_measurable_restricted: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

112 
fixes f :: "'a \<Rightarrow> extreal" assumes "A \<in> sets M" 
39092  113 
shows "f \<in> borel_measurable (restricted_space A) \<longleftrightarrow> 
114 
(\<lambda>x. f x * indicator A x) \<in> borel_measurable M" 

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

116 
proof  

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

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

119 
by (auto intro!: measurable_cong) 

120 
show ?thesis unfolding * 

40859  121 
unfolding in_borel_measurable_borel 
39092  122 
proof (simp, safe) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

123 
fix S :: "extreal set" assume "S \<in> sets borel" 
40859  124 
"\<forall>S\<in>sets borel. ?f ` S \<inter> A \<in> op \<inter> A ` sets M" 
39092  125 
then have "?f ` S \<inter> A \<in> op \<inter> A ` sets M" by auto 
126 
then have f: "?f ` S \<inter> A \<in> sets M" 

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

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

129 
proof cases 

130 
assume "0 \<in> S" 

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

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

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

134 
next 

135 
assume "0 \<notin> S" 

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

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

138 
by (auto simp: indicator_def split: split_if_asm) 

139 
then show ?thesis using f by auto 

140 
qed 

141 
next 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

142 
fix S :: "extreal set" assume "S \<in> sets borel" 
40859  143 
"\<forall>S\<in>sets borel. ?f ` S \<inter> space M \<in> sets M" 
39092  144 
then have f: "?f ` S \<inter> space M \<in> sets M" by auto 
145 
then show "?f ` S \<inter> A \<in> op \<inter> A ` sets M" 

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

147 
apply (simp add: image_iff) 

148 
apply (rule bexI[OF _ f]) 

149 
by auto 

150 
qed 

151 
qed 

152 

153 
lemma (in sigma_algebra) borel_measurable_subalgebra: 

41545  154 
assumes "sets N \<subseteq> sets M" "space N = space M" "f \<in> borel_measurable N" 
39092  155 
shows "f \<in> borel_measurable M" 
156 
using assms unfolding measurable_def by auto 

157 

38656  158 
section "Borel spaces on euclidean spaces" 
159 

160 
lemma lessThan_borel[simp, intro]: 

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

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

38656  164 

165 
lemma greaterThan_borel[simp, intro]: 

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

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

38656  169 

170 
lemma greaterThanLessThan_borel[simp, intro]: 

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

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

38656  174 

175 
lemma atMost_borel[simp, intro]: 

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

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

38656  179 

180 
lemma atLeast_borel[simp, intro]: 

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

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

38656  184 

185 
lemma atLeastAtMost_borel[simp, intro]: 

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

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

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

189 

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

40859  192 
shows "{a<..b} \<in> sets borel" 
38656  193 
unfolding greaterThanAtMost_def by blast 
194 

195 
lemma atLeastLessThan_borel[simp, intro]: 

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

40859  197 
shows "{a..<b} \<in> sets borel" 
38656  198 
unfolding atLeastLessThan_def by blast 
199 

200 
lemma hafspace_less_borel[simp, intro]: 

201 
fixes a :: real 

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

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

204 

38656  205 
lemma hafspace_greater_borel[simp, intro]: 
206 
fixes a :: real 

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

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

209 

38656  210 
lemma hafspace_less_eq_borel[simp, intro]: 
211 
fixes a :: real 

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

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

214 

38656  215 
lemma hafspace_greater_eq_borel[simp, intro]: 
216 
fixes a :: real 

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

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

219 

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

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

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

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

224 
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

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

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

229 
then show ?thesis using f g 

230 
by simp (blast intro: measurable_sets) 

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

231 
qed 
38656  232 

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

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

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

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

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

237 
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

238 
proof  
38656  239 
have "{w \<in> space M. f w \<le> g w} = space M  {w \<in> space M. g w < f w}" 
240 
by auto 

241 
thus ?thesis using f g 

242 
by simp blast 

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

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

244 

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

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

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

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

249 
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

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

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

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

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

256 

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

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

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

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

261 
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

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

263 
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

264 
by auto 
38656  265 
thus ?thesis using f g by auto 
266 
qed 

267 

268 
subsection "Borel space equals sigma algebras over intervals" 

269 

270 
lemma rational_boxes: 

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

272 
assumes "0 < e" 

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

274 
proof  

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

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

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

278 
proof 

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

280 
show "?th i" by auto 

281 
qed 

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

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

284 
proof 

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

286 
show "?th i" by auto 

287 
qed 

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

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

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

291 
unfolding setL2_def[symmetric] by (rule euclidean_dist_l2) 

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

293 
proof (rule real_sqrt_less_mono, rule setsum_strict_mono) 

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

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

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

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

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

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

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

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

302 
by (rule power_strict_mono) auto 

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

304 
by (simp add: power_divide) 

305 
qed auto 

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

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

308 
with a b show ?thesis 

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

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

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

312 
qed 

313 

314 
lemma ex_rat_list: 

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

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

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

318 
proof  

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

320 
from choice[OF this] guess r .. 

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

322 
qed 

323 

324 
lemma open_UNION: 

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

326 
assumes "open M" 

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

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

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

330 
proof safe 

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

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

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

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

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

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

337 
"length q = DIM ('a)" 

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

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

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

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

342 
unfolding o_def by auto 

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

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

345 
unfolding o_def by auto 

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

347 
using p q ab by auto 

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

349 
qed auto 

350 

351 
lemma halfspace_span_open: 

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

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

355 
open_halfspace_component_lt) 

38656  356 

357 
lemma halfspace_lt_in_halfspace: 

40859  358 
"{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>)" 
359 
by (auto intro!: sigma_sets.Basic simp: sets_sigma) 

38656  360 

361 
lemma halfspace_gt_in_halfspace: 

40859  362 
"{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>)" 
363 
(is "?set \<in> sets ?SIGMA") 

38656  364 
proof  
40859  365 
interpret sigma_algebra "?SIGMA" 
366 
by (intro sigma_algebra_sigma_sets) (simp_all add: sets_sigma) 

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

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

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

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

372 
by (auto simp: inverse_eq_divide field_simps) 

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

374 
by (blast intro: less_imp_le) 

375 
next 

376 
fix x n 

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

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

379 
finally show "a < x" . 

380 
qed 

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

382 
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

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

384 

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

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

393 
obtain I where *: "S = 

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

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

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

397 
unfolding greaterThanLessThan_def 

398 
unfolding eucl_greaterThan_eq_halfspaces[where 'a='a] 

399 
unfolding eucl_lessThan_eq_halfspaces[where 'a='a] 

400 
by blast 

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

402 
unfolding * 

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

404 
then show ?thesis unfolding borel_def 

405 
by (intro sets_sigma_subset) auto 

406 
qed 

38656  407 

408 
lemma halfspace_span_halfspace_le: 

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

38656  411 
(is "_ \<subseteq> sets ?SIGMA") 
40859  412 
proof  
413 
have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto 

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

417 
proof (safe, simp_all) 

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

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

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

421 
by (auto simp: field_simps inverse_eq_divide) 

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

423 
by (blast intro: less_imp_le) 

424 
next 

425 
fix x::'a and n 

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

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

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

429 
qed 

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

431 
by (safe intro!: countable_UN) 

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

433 
then show ?thesis by (intro sets_sigma_subset) auto 

434 
qed 

38656  435 

436 
lemma halfspace_span_halfspace_ge: 

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

38656  439 
(is "_ \<subseteq> sets ?SIGMA") 
40859  440 
proof  
441 
have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto 

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

445 
by (safe intro!: Diff) 

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

447 
then show ?thesis by (intro sets_sigma_subset) auto 

448 
qed 

38656  449 

450 
lemma halfspace_le_span_halfspace_gt: 

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

38656  453 
(is "_ \<subseteq> sets ?SIGMA") 
40859  454 
proof  
455 
have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto 

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

459 
by (safe intro!: Diff) 

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

461 
then show ?thesis by (intro sets_sigma_subset) auto 

462 
qed 

38656  463 

464 
lemma halfspace_le_span_atMost: 

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

38656  467 
(is "_ \<subseteq> sets ?SIGMA") 
40859  468 
proof  
469 
have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto 

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

476 
fix x 

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

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

479 
by (subst (asm) Max_le_iff) auto 

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

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

482 
qed 

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

484 
by (safe intro!: countable_UN) 

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

486 
next 

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

490 
qed 

40859  491 
then show ?thesis by (intro sets_sigma_subset) auto 
492 
qed 

38656  493 

494 
lemma halfspace_le_span_greaterThan: 

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

38656  497 
(is "_ \<subseteq> sets ?SIGMA") 
40859  498 
proof  
499 
have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto 

38656  500 
then interpret sigma_algebra ?SIGMA . 
40859  501 
have "\<And>a i. {x. x$$i \<le> a} \<in> sets ?SIGMA" 
38656  502 
proof cases 
40859  503 
fix a i assume "i < DIM('a)" 
38656  504 
have "{x::'a. x$$i \<le> a} = space ?SIGMA  {x::'a. a < x$$i}" by auto 
505 
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)` 

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

507 
fix x 

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

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

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

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

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

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

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

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

516 
qed 

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

518 
apply (simp only:) 

519 
apply (safe intro!: countable_UN Diff) 

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

521 
next 

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

525 
qed 

40859  526 
then show ?thesis by (intro sets_sigma_subset) auto 
527 
qed 

528 

529 
lemma halfspace_le_span_lessThan: 

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

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

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

533 
proof  

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

535 
then interpret sigma_algebra ?SIGMA . 

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

537 
proof cases 

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

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

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

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

542 
fix x 

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

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

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

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

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

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

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

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

551 
qed 

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

553 
apply (simp only:) 

554 
apply (safe intro!: countable_UN Diff) 

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

556 
next 

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

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

559 
using top by auto 

560 
qed 

561 
then show ?thesis by (intro sets_sigma_subset) auto 

562 
qed 

563 

564 
lemma atMost_span_atLeastAtMost: 

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

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

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

568 
proof  

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

570 
then interpret sigma_algebra ?SIGMA . 

571 
{ fix a::'a 

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

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

574 
fix x 

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

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

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

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

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

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

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

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

583 
qed 

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

585 
by (safe intro!: countable_UN) 

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

587 
then show ?thesis by (intro sets_sigma_subset) auto 

588 
qed 

589 

590 
lemma borel_eq_atMost: 

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

592 
(is "_ = ?SIGMA") 

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

596 
by auto 

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

598 
by (rule borel.sets_sigma_subset) auto 

599 
qed auto 

600 

601 
lemma borel_eq_atLeastAtMost: 

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

603 
(is "_ = ?SIGMA") 

40869  604 
proof (intro algebra.equality antisym) 
40859  605 
show "sets borel \<subseteq> sets ?SIGMA" 
606 
using atMost_span_atLeastAtMost halfspace_le_span_atMost 

607 
halfspace_span_halfspace_le open_span_halfspace 

608 
by auto 

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

610 
by (rule borel.sets_sigma_subset) auto 

611 
qed auto 

612 

613 
lemma borel_eq_greaterThan: 

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

615 
(is "_ = ?SIGMA") 

40869  616 
proof (intro algebra.equality antisym) 
40859  617 
show "sets borel \<subseteq> sets ?SIGMA" 
618 
using halfspace_le_span_greaterThan 

619 
halfspace_span_halfspace_le open_span_halfspace 

620 
by auto 

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

622 
by (rule borel.sets_sigma_subset) auto 

623 
qed auto 

624 

625 
lemma borel_eq_lessThan: 

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

627 
(is "_ = ?SIGMA") 

40869  628 
proof (intro algebra.equality antisym) 
40859  629 
show "sets borel \<subseteq> sets ?SIGMA" 
630 
using halfspace_le_span_lessThan 

631 
halfspace_span_halfspace_ge open_span_halfspace 

632 
by auto 

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

634 
by (rule borel.sets_sigma_subset) auto 

635 
qed auto 

636 

637 
lemma borel_eq_greaterThanLessThan: 

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

639 
(is "_ = ?SIGMA") 

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

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

644 
proof  

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

646 
then interpret sigma_algebra ?SIGMA . 

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

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

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

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

651 
apply (safe intro!: countable_UN) 

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

653 
then show ?thesis 

654 
unfolding borel_def by (intro sets_sigma_subset) auto 

655 
qed 

38656  656 
qed auto 
657 

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

660 
(is "_ = ?SIGMA") 

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

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

665 
by (rule borel.sets_sigma_subset) auto 

666 
qed auto 

667 

668 
lemma borel_eq_halfspace_less: 

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

670 
(is "_ = ?SIGMA") 

40869  671 
proof (intro algebra.equality antisym) 
40859  672 
show "sets borel \<subseteq> sets ?SIGMA" 
673 
using open_span_halfspace . 

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

675 
by (rule borel.sets_sigma_subset) auto 

38656  676 
qed auto 
677 

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

680 
(is "_ = ?SIGMA") 

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

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

685 
by (rule borel.sets_sigma_subset) auto 

686 
qed auto 

38656  687 

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

690 
(is "_ = ?SIGMA") 

40869  691 
proof (intro algebra.equality antisym) 
40859  692 
show "sets borel \<subseteq> sets ?SIGMA" 
38656  693 
using halfspace_span_halfspace_ge open_span_halfspace by auto 
40859  694 
show "sets ?SIGMA \<subseteq> sets borel" 
695 
by (rule borel.sets_sigma_subset) auto 

696 
qed auto 

38656  697 

698 
lemma (in sigma_algebra) borel_measurable_halfspacesI: 

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

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

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

704 
proof safe 

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

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

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

708 
next 

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

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

711 
proof cases 

712 
assume "i < DIM('c)" 

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

714 
next 

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

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

717 
qed } 

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

721 
unfolding assms(1) by simp 

722 
qed 

723 

724 
lemma (in sigma_algebra) borel_measurable_iff_halfspace_le: 

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

726 
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  727 
by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_le]) auto 
38656  728 

729 
lemma (in sigma_algebra) borel_measurable_iff_halfspace_less: 

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

731 
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  732 
by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_less]) auto 
38656  733 

734 
lemma (in sigma_algebra) borel_measurable_iff_halfspace_ge: 

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

736 
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  737 
by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_ge]) auto 
38656  738 

739 
lemma (in sigma_algebra) borel_measurable_iff_halfspace_greater: 

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

741 
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  742 
by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_gt]) auto 
38656  743 

744 
lemma (in sigma_algebra) borel_measurable_iff_le: 

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

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

747 

748 
lemma (in sigma_algebra) borel_measurable_iff_less: 

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

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

751 

752 
lemma (in sigma_algebra) borel_measurable_iff_ge: 

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

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

755 

756 
lemma (in sigma_algebra) borel_measurable_iff_greater: 

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

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

759 

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

763 
proof (rule borel.measurable_sigma, simp_all) 

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

764 
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

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

768 
qed 

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

769 

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

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

772 
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

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

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

775 
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

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

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

779 
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

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

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

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

783 

38656  784 
subsection "Borel measurable operators" 
785 

786 
lemma (in sigma_algebra) affine_borel_measurable_vector: 

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

788 
assumes "f \<in> borel_measurable M" 

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

790 
proof (rule borel_measurableI) 

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

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

793 
proof cases 

794 
assume "b \<noteq> 0" 

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

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

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

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

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

40859  802 
ultimately show ?thesis using assms unfolding in_borel_measurable_borel 
38656  803 
by auto 
804 
qed simp 

805 
qed 

806 

807 
lemma (in sigma_algebra) affine_borel_measurable: 

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

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

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

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

812 

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

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

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

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

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

817 
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

818 
proof  
38656  819 
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

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

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

824 
by auto 

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

826 
by (simp add: 1) 

827 
then show ?thesis 

828 
by (simp add: borel_measurable_iff_ge) 

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

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

830 

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

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

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

833 
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

834 
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

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

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

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

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

839 

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

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

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

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

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

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

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

847 
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

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

849 
case less 
38656  850 
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

851 
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

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

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

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

856 
case equal 
38656  857 
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

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

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

860 
also have "... \<in> sets M" 
38656  861 
apply (insert f) 
862 
apply (rule Int) 

863 
apply (simp add: borel_measurable_iff_le) 

864 
apply (simp add: borel_measurable_iff_ge) 

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

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

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

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

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

869 
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

870 
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

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

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

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

875 
also have "... \<in> sets M" 
38656  876 
apply (insert f) 
877 
apply (rule Int) 

878 
apply (simp add: borel_measurable_iff_ge) 

879 
apply (simp add: borel_measurable_iff_le) 

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

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

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

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

883 
} 
38656  884 
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

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

886 

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

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

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

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

891 

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

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

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

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

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

897 
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

898 
by simp 
38656  899 
also have "... \<in> borel_measurable M" 
900 
by (fast intro: affine_borel_measurable g) 

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

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

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

903 

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

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

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

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

908 
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

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

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

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

917 
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

918 
show ?thesis 
38656  919 
apply (simp add: times_eq_sum_squares diff_minus) 
920 
using 1 2 by simp 

33533
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 

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

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

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

925 
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

926 
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

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

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

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

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

931 

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

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

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

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

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

938 

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

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

38656  943 
unfolding borel_measurable_iff_ge unfolding inverse_eq_divide 
944 
proof safe 

945 
fix a :: real 

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

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

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

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

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

951 
by (auto intro!: Int Un) 

35692  952 
qed 
953 

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

35692  956 
assumes "f \<in> borel_measurable M" 
957 
and "g \<in> borel_measurable M" 

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

959 
unfolding field_divide_inverse 

38656  960 
by (rule borel_measurable_inverse borel_measurable_times assms)+ 
961 

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

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

964 
assumes "f \<in> borel_measurable M" 

965 
assumes "g \<in> borel_measurable M" 

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

967 
unfolding borel_measurable_iff_le 

968 
proof safe 

969 
fix a 

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

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

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

973 
using assms unfolding borel_measurable_iff_le 

974 
by (auto intro!: Int) 

975 
qed 

976 

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

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

979 
assumes "f \<in> borel_measurable M" 

980 
assumes "g \<in> borel_measurable M" 

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

982 
unfolding borel_measurable_iff_ge 

983 
proof safe 

984 
fix a 

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

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

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

988 
using assms unfolding borel_measurable_iff_ge 

989 
by (auto intro!: Int) 

990 
qed 

991 

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

993 
assumes "f \<in> borel_measurable M" 

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

995 
proof  

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

997 
show ?thesis unfolding * using assms by auto 

998 
qed 

999 

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

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

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

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

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

1004 

41830  1005 
lemma borel_measurable_continuous_on1: 
1006 
fixes f :: "'a::topological_space \<Rightarrow> 'b::t1_space" 

1007 
assumes "continuous_on UNIV f" 

1008 
shows "f \<in> borel_measurable borel" 

1009 
apply(rule borel.borel_measurableI) 

1010 
using continuous_open_preimage[OF assms] unfolding vimage_def by auto 

1011 

1012 
lemma borel_measurable_continuous_on: 

1013 
fixes f :: "'a::topological_space \<Rightarrow> 'b::t1_space" 

1014 
assumes cont: "continuous_on A f" "open A" and f: "f ` {c} \<inter> A \<in> sets borel" 

1015 
shows "(\<lambda>x. if x \<in> A then f x else c) \<in> borel_measurable borel" (is "?f \<in> _") 

1016 
proof (rule borel.borel_measurableI) 

1017 
fix S :: "'b set" assume "open S" 

1018 
then have "open {x\<in>A. f x \<in> S  {c}}" 

1019 
by (intro continuous_open_preimage[OF cont]) auto 

1020 
then have *: "{x\<in>A. f x \<in> S  {c}} \<in> sets borel" by auto 

1021 
show "?f ` S \<inter> space borel \<in> sets borel" 

1022 
proof cases 

1023 
assume "c \<in> S" 

1024 
then have "?f ` S = {x\<in>A. f x \<in> S  {c}} \<union> (f ` {c} \<inter> A) \<union> A" 

1025 
by auto 

1026 
with * show "?f ` S \<inter> space borel \<in> sets borel" 

1027 
using `open A` f by (auto intro!: borel.Un) 

1028 
next 

1029 
assume "c \<notin> S" 

1030 
then have "?f ` S = {x\<in>A. f x \<in> S  {c}}" by (auto split: split_if_asm) 

1031 
with * show "?f ` S \<inter> space borel \<in> sets borel" by auto 

1032 
qed 

1033 
qed 

1034 

1035 
lemma borel_measurable_borel_log: assumes "1 < b" shows "log b \<in> borel_measurable borel" 

1036 
proof  

1037 
{ fix x :: real assume x: "x \<le> 0" 

1038 
{ fix x::real assume "x \<le> 0" then have "\<And>u. exp u = x \<longleftrightarrow> False" by auto } 

1039 
from this[of x] x this[of 0] have "log b 0 = log b x" 

1040 
by (auto simp: ln_def log_def) } 

1041 
note log_imp = this 

1042 
have "(\<lambda>x. if x \<in> {0<..} then log b x else log b 0) \<in> borel_measurable borel" 

1043 
proof (rule borel_measurable_continuous_on) 

1044 
show "continuous_on {0<..} (log b)" 

1045 
by (auto intro!: continuous_at_imp_continuous_on DERIV_log DERIV_isCont 

1046 
simp: continuous_isCont[symmetric]) 

1047 
show "open ({0<..}::real set)" by auto 

1048 
show "log b ` {log b 0} \<inter> {0<..} \<in> sets borel" 

1049 
proof cases 

1050 
assume "log b ` {log b 0} \<inter> {0<..} = {}" 

1051 
then show ?thesis by simp 

1052 
next 

1053 
assume "log b ` {log b 0} \<inter> {0<..} \<noteq> {}" 

1054 
then obtain x where "0 < x" "log b x = log b 0" by auto 

1055 
with log_inj[OF `1 < b`] have "log b ` {log b 0} \<inter> {0<..} = {x}" 

1056 
by (auto simp: inj_on_def) 

1057 
then show ?thesis by simp 

1058 
qed 

1059 
qed 

1060 
also have "(\<lambda>x. if x \<in> {0<..} then log b x else log b 0) = log b" 

1061 
by (simp add: fun_eq_iff not_less log_imp) 

1062 
finally show ?thesis . 

1063 
qed 

1064 

1065 
lemma (in sigma_algebra) borel_measurable_log[simp,intro]: 

1066 
assumes f: "f \<in> borel_measurable M" and "1 < b" 

1067 
shows "(\<lambda>x. log b (f x)) \<in> borel_measurable M" 

1068 
using measurable_comp[OF f borel_measurable_borel_log[OF `1 < b`]] 

1069 
by (simp add: comp_def) 

1070 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1071 
subsection "Borel space on the extended reals" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1072 

cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1073 
lemma borel_measurable_extreal_borel: 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1074 
"extreal \<in> borel_measurable borel" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1075 
unfolding borel_def[where 'a=extreal] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1076 
proof (rule borel.measurable_sigma) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1077 
fix X :: "extreal set" assume "X \<in> sets \<lparr>space = UNIV, sets = open \<rparr>" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1078 
then have "open X" by (auto simp: mem_def) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1079 
then have "open (extreal ` X \<inter> space borel)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1080 
by (simp add: open_extreal_vimage) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1081 
then show "extreal ` X \<inter> space borel \<in> sets borel" by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1082 
qed auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1083 

cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1084 
lemma (in sigma_algebra) borel_measurable_extreal[simp, intro]: 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1085 
assumes f: "f \<in> borel_measurable M" shows "(\<lambda>x. extreal (f x)) \<in> borel_measurable M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1086 
using measurable_comp[OF f borel_measurable_extreal_borel] unfolding comp_def . 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1087 

cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1088 
lemma borel_measurable_real_of_extreal_borel: 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1089 
"(real :: extreal \<Rightarrow> real) \<in> borel_measurable borel" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1090 
unfolding borel_def[where 'a=real] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1091 
proof (rule borel.measurable_sigma) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1092 
fix B :: "real set" assume "B \<in> sets \<lparr>space = UNIV, sets = open \<rparr>" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1093 
then have "open B" by (auto simp: mem_def) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1094 
have *: "extreal ` real ` (B  {0}) = B  {0}" by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1095 
have open_real: "open (real ` (B  {0}) :: extreal set)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1096 
unfolding open_extreal_def * using `open B` by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1097 
show "(real ` B \<inter> space borel :: extreal set) \<in> sets borel" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1098 
proof cases 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1099 
assume "0 \<in> B" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1100 
then have *: "real ` B = real ` (B  {0}) \<union> {\<infinity>, \<infinity>, 0}" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1101 
by (auto simp add: real_of_extreal_eq_0) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1102 
then show "(real ` B :: extreal set) \<inter> space borel \<in> sets borel" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1103 
using open_real by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1104 
next 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1105 
assume "0 \<notin> B" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1106 
then have *: "(real ` B :: extreal set) = real ` (B  {0})" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1107 
by (auto simp add: real_of_extreal_eq_0) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1108 
then show "(real ` B :: extreal set) \<inter> space borel \<in> sets borel" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1109 
using open_real by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1110 
qed 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1111 
qed auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1112 

cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1113 
lemma (in sigma_algebra) borel_measurable_real_of_extreal[simp, intro]: 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1114 
assumes f: "f \<in> borel_measurable M" shows "(\<lambda>x. real (f x :: extreal)) \<in> borel_measurable M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1115 
using measurable_comp[OF f borel_measurable_real_of_extreal_borel] unfolding comp_def . 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1116 

cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1117 
lemma (in sigma_algebra) borel_measurable_extreal_iff: 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1118 
shows "(\<lambda>x. extreal (f x)) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1119 
proof 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1120 
assume "(\<lambda>x. extreal (f x)) \<in> borel_measurable M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1121 
from borel_measurable_real_of_extreal[OF this] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1122 
show "f \<in> borel_measurable M" by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1123 
qed auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1124 

cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1125 
lemma (in sigma_algebra) borel_measurable_extreal_iff_real: 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1126 
"f \<in> borel_measurable M \<longleftrightarrow> 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1127 
((\<lambda>x. real (f x)) \<in> borel_measurable M \<and> f ` {\<infinity>} \<inter> space M \<in> sets M \<and> f ` {\<infinity>} \<inter> space M \<in> sets M)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1128 
proof safe 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1129 
assume *: "(\<lambda>x. real (f x)) \<in> borel_measurable M" "f ` {\<infinity>} \<inter> space M \<in> sets M" "f ` {\<infinity>} \<inter> space M \<in> sets M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1130 
have "f ` {\<infinity>} \<inter> space M = {x\<in>space M. f x = \<infinity>}" "f ` {\<infinity>} \<inter> space M = {x\<in>space M. f x = \<infinity>}" by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1131 
with * have **: "{x\<in>space M. f x = \<infinity>} \<in> sets M" "{x\<in>space M. f x = \<infinity>} \<in> sets M" by simp_all 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1132 
let "?f x" = "if f x = \<infinity> then \<infinity> else if f x = \<infinity> then \<infinity> else extreal (real (f x))" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1133 
have "?f \<in> borel_measurable M" using * ** by (intro measurable_If) auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1134 
also have "?f = f" by (auto simp: fun_eq_iff extreal_real) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1135 
finally show "f \<in> borel_measurable M" . 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1136 
qed (auto intro: measurable_sets borel_measurable_real_of_extreal) 
41830  1137 

38656  1138 
lemma (in sigma_algebra) less_eq_ge_measurable: 
1139 
fixes f :: "'a \<Rightarrow> 'c::linorder" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1140 
shows "f ` {a <..} \<inter> space M \<in> sets M \<longleftrightarrow> f ` {..a} \<inter> space M \<in> sets M" 
38656  1141 
proof 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1142 
assume "f ` {a <..} \<inter> space M \<in> sets M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1143 
moreover have "f ` {..a} \<inter> space M = space M  f ` {a <..} \<inter> space M" by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1144 
ultimately show "f ` {..a} \<inter> space M \<in> sets M" by auto 
38656  1145 
next 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1146 
assume "f ` {..a} \<inter> space M \<in> sets M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1147 
moreover have "f ` {a <..} \<inter> space M = space M  f ` {..a} \<inter> space M" by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1148 
ultimately show "f ` {a <..} \<inter> space M \<in> sets M" by auto 
38656  1149 
qed 
35692  1150 

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

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1153 
shows "f ` {..< a} \<inter> space M \<in> sets M \<longleftrightarrow> f ` {a ..} \<inter> space M \<in> sets M" 
38656  1154 
proof 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1155 
assume "f ` {a ..} \<inter> space M \<in> sets M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1156 
moreover have "f ` {..< a} \<inter> space M = space M  f ` {a ..} \<inter> space M" by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1157 
ultimately show "f ` {..< a} \<inter> space M \<in> sets M" by auto 
38656  1158 
next 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1159 
assume "f ` {..< a} \<inter> space M \<in> sets M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1160 
moreover have "f ` {a ..} \<inter> space M = space M  f ` {..< a} \<inter> space M" by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1161 
ultimately show "f ` {a ..} \<inter> space M \<in> sets M" by auto 
38656  1162 
qed 
1163 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1164 
lemma (in sigma_algebra) borel_measurable_uminus_borel_extreal: 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1165 
"(uminus :: extreal \<Rightarrow> extreal) \<in> borel_measurable borel" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1166 
proof (subst borel_def, rule borel.measurable_sigma) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1167 
fix X :: "extreal set" assume "X \<in> sets \<lparr>space = UNIV, sets = open\<rparr>" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1168 
then have "open X" by (simp add: mem_def) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1169 
have "uminus ` X = uminus ` X" by (force simp: image_iff) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1170 
then have "open (uminus ` X)" using `open X` extreal_open_uminus by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1171 
then show "uminus ` X \<inter> space borel \<in> sets borel" by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1172 
qed auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1173 

cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1174 
lemma (in sigma_algebra) borel_measurable_uminus_extreal[intro]: 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1175 
assumes "f \<in> borel_measurable M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1176 
shows "(\<lambda>x.  f x :: extreal) \<in> borel_measurable M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1177 
using measurable_comp[OF assms borel_measurable_uminus_borel_extreal] by (simp add: comp_def) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1178 

cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1179 
lemma (in sigma_algebra) borel_measurable_uminus_eq_extreal[simp]: 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1180 
"(\<lambda>x.  f x :: extreal) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M" (is "?l = ?r") 
38656  1181 
proof 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1182 
assume ?l from borel_measurable_uminus_extreal[OF this] show ?r by simp 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1183 
qed auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1184 

cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1185 
lemma (in sigma_algebra) borel_measurable_eq_atMost_extreal: 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1186 
"(f::'a \<Rightarrow> extreal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f ` {..a} \<inter> space M \<in> sets M)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1187 
proof (intro iffI allI) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1188 
assume pos[rule_format]: "\<forall>a. f ` {..a} \<inter> space M \<in> sets M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1189 
show "f \<in> borel_measurable M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1190 
unfolding borel_measurable_extreal_iff_real borel_measurable_iff_le 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1191 
proof (intro conjI allI) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1192 
fix a :: real 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1193 
{ fix x :: extreal assume *: "\<forall>i::nat. real i < x" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1194 
have "x = \<infinity>" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1195 
proof (rule extreal_top) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1196 
fix B from real_arch_lt[of B] guess n .. 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1197 
then have "extreal B < real n" by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1198 
with * show "B \<le> x" by (metis less_trans less_imp_le) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1199 
qed } 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1200 
then have "f ` {\<infinity>} \<inter> space M = space M  (\<Union>i::nat. f ` {.. real i} \<inter> space M)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1201 
by (auto simp: not_le) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1202 
then show "f ` {\<infinity>} \<inter> space M \<in> sets M" using pos by (auto simp del: UN_simps intro!: Diff) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1203 
moreover 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1204 
have "{\<infinity>} = {..\<infinity>}" by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1205 
then show "f ` {\<infinity>} \<inter> space M \<in> sets M" using pos by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1206 
moreover have "{x\<in>space M. f x \<le> extreal a} \<in> sets M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1207 
using pos[of "extreal a"] by (simp add: vimage_def Int_def conj_commute) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1208 
moreover have "{w \<in> space M. real (f w) \<le> a} = 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1209 
(if a < 0 then {w \<in> space M. f w \<le> extreal a}  f ` {\<infinity>} \<inter> space M 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1210 
else {w \<in> space M. f w \<le> extreal a} \<union> (f ` {\<infinity>} \<inter> space M) \<union> (f ` {\<infinity>} \<inter> space M))" (is "?l = ?r") 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1211 
proof (intro set_eqI) fix x show "x \<in> ?l \<longleftrightarrow> x \<in> ?r" by (cases "f x") auto qed 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1212 
ultimately show "{w \<in> space M. real (f w) \<le> a} \<in> sets M" by auto 
35582  1213 
qed 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1214 
qed (simp add: measurable_sets) 
35582  1215 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1216 
lemma (in sigma_algebra) borel_measurable_eq_atLeast_extreal: 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1217 
"(f::'a \<Rightarrow> extreal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f ` {a..} \<inter> space M \<in> sets M)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1218 
proof 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1219 
assume pos: "\<forall>a. f ` {a..} \<inter> space M \<in> sets M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1220 
moreover have "\<And>a. (\<lambda>x.  f x) ` {..a} = f ` {a ..}" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1221 
by (auto simp: extreal_uminus_le_reorder) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1222 
ultimately have "(\<lambda>x.  f x) \<in> borel_measurable M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1223 
unfolding borel_measurable_eq_atMost_extreal by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1224 
then show "f \<in> borel_measurable M" by simp 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1225 
qed (simp add: measurable_sets) 
35582  1226 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1227 
lemma (in sigma_algebra) borel_measurable_extreal_iff_less: 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1228 
"(f::'a \<Rightarrow> extreal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f ` {..< a} \<inter> space M \<in> sets M)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1229 
unfolding borel_measurable_eq_atLeast_extreal greater_eq_le_measurable .. 
38656  1230 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1231 
lemma (in sigma_algebra) borel_measurable_extreal_iff_ge: 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1232 
"(f::'a \<Rightarrow> extreal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f ` {a <..} \<inter> space M \<in> sets M)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1233 
unfolding borel_measurable_eq_atMost_extreal less_eq_ge_measurable .. 
38656  1234 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1235 
lemma (in sigma_algebra) borel_measurable_extreal_eq_const: 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1236 
fixes f :: "'a \<Rightarrow> extreal" assumes "f \<in> borel_measurable M" 
38656  1237 
shows "{x\<in>space M. f x = c} \<in> sets M" 
1238 
proof  

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

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

1241 
qed 

1242 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1243 
lemma (in sigma_algebra) borel_measurable_extreal_neq_const: 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1244 
fixes f :: "'a \<Rightarrow> extreal" assumes "f \<in> borel_measurable M" 
38656  1245 
shows "{x\<in>space M. f x \<noteq> c} \<in> sets M" 
1246 
proof  

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

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

1249 
qed 

1250 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1251 
lemma (in sigma_algebra) borel_measurable_extreal_le[intro,simp]: 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969< 