author  hoelzl 
Fri, 28 Oct 2011 14:10:19 +0200  
changeset 45288  fc3c7db5bb2f 
parent 45287  97df8c08291c 
child 46731  5302e932d1e5 
permissions  rwrr 
42150  1 
(* Title: HOL/Probability/Borel_Space.thy 
42067  2 
Author: Johannes Hölzl, TU München 
3 
Author: Armin Heller, TU München 

4 
*) 

38656  5 

6 
header {*Borel spaces*} 

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

7 

40859  8 
theory Borel_Space 
45288  9 
imports Sigma_Algebra "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis" 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

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

11 

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

13 

44537
c10485a6a7af
make HOLProbability respect set/pred distinction
huffman
parents:
44282
diff
changeset

14 
definition "borel = sigma \<lparr> space = UNIV::'a::topological_space set, sets = {S. open S}\<rparr>" 
40859  15 
abbreviation "borel_measurable M \<equiv> measurable M borel" 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

16 

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

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

19 

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

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

21 
"f \<in> borel_measurable M \<longleftrightarrow> 
44537
c10485a6a7af
make HOLProbability respect set/pred distinction
huffman
parents:
44282
diff
changeset

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

25 

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

31 

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

38656  34 

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

38656  37 
proof  
44537
c10485a6a7af
make HOLProbability respect set/pred distinction
huffman
parents:
44282
diff
changeset

38 
have "A \<in> {S. open S}" unfolding mem_Collect_eq using assms . 
40859  39 
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

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

41 

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

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

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

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

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

49 

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

52 

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

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

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

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

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

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

65 
thus ?thesis by auto 

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

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

67 

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

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

71 
shows "f \<in> borel_measurable M" 

40859  72 
unfolding borel_def 
73 
proof (rule measurable_sigma, simp_all) 

44537
c10485a6a7af
make HOLProbability respect set/pred distinction
huffman
parents:
44282
diff
changeset

74 
fix S :: "'x set" assume "open S" thus "f ` S \<inter> space M \<in> sets M" 
c10485a6a7af
make HOLProbability respect set/pred distinction
huffman
parents:
44282
diff
changeset

75 
using assms[of S] by simp 
40859  76 
qed 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

77 

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

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

41969  83 
using closed_singleton[of x] by (rule borel_closed) 
38656  84 
qed simp 
85 

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

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

88 
by (auto intro!: measurable_const) 

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

89 

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

93 
unfolding indicator_def_raw using A 

94 
by (auto intro!: measurable_If_set borel_measurable_const) 

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

95 

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

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

99 
proof 

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

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

102 
unfolding measurable_def by auto 

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

104 
unfolding indicator_def_raw by auto 

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

106 
next 

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

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

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

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

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

112 
qed 

113 

39092  114 
lemma (in sigma_algebra) borel_measurable_restricted: 
43920  115 
fixes f :: "'a \<Rightarrow> ereal" assumes "A \<in> sets M" 
39092  116 
shows "f \<in> borel_measurable (restricted_space A) \<longleftrightarrow> 
117 
(\<lambda>x. f x * indicator A x) \<in> borel_measurable M" 

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

119 
proof  

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

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

122 
by (auto intro!: measurable_cong) 

123 
show ?thesis unfolding * 

40859  124 
unfolding in_borel_measurable_borel 
39092  125 
proof (simp, safe) 
43920  126 
fix S :: "ereal set" assume "S \<in> sets borel" 
40859  127 
"\<forall>S\<in>sets borel. ?f ` S \<inter> A \<in> op \<inter> A ` sets M" 
39092  128 
then have "?f ` S \<inter> A \<in> op \<inter> A ` sets M" by auto 
129 
then have f: "?f ` S \<inter> A \<in> sets M" 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44666
diff
changeset

130 
using `A \<in> sets M` sets_into_space by fastforce 
39092  131 
show "?f ` S \<inter> space M \<in> sets M" 
132 
proof cases 

133 
assume "0 \<in> S" 

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

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

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

137 
next 

138 
assume "0 \<notin> S" 

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

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

141 
by (auto simp: indicator_def split: split_if_asm) 

142 
then show ?thesis using f by auto 

143 
qed 

144 
next 

43920  145 
fix S :: "ereal set" assume "S \<in> sets borel" 
40859  146 
"\<forall>S\<in>sets borel. ?f ` S \<inter> space M \<in> sets M" 
39092  147 
then have f: "?f ` S \<inter> space M \<in> sets M" by auto 
148 
then show "?f ` S \<inter> A \<in> op \<inter> A ` sets M" 

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

150 
apply (simp add: image_iff) 

151 
apply (rule bexI[OF _ f]) 

152 
by auto 

153 
qed 

154 
qed 

155 

156 
lemma (in sigma_algebra) borel_measurable_subalgebra: 

41545  157 
assumes "sets N \<subseteq> sets M" "space N = space M" "f \<in> borel_measurable N" 
39092  158 
shows "f \<in> borel_measurable M" 
159 
using assms unfolding measurable_def by auto 

160 

38656  161 
section "Borel spaces on euclidean spaces" 
162 

163 
lemma lessThan_borel[simp, intro]: 

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

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

38656  167 

168 
lemma greaterThan_borel[simp, intro]: 

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

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

38656  172 

173 
lemma greaterThanLessThan_borel[simp, intro]: 

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

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

38656  177 

178 
lemma atMost_borel[simp, intro]: 

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

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

38656  182 

183 
lemma atLeast_borel[simp, intro]: 

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

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

38656  187 

188 
lemma atLeastAtMost_borel[simp, intro]: 

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

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

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

192 

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

40859  195 
shows "{a<..b} \<in> sets borel" 
38656  196 
unfolding greaterThanAtMost_def by blast 
197 

198 
lemma atLeastLessThan_borel[simp, intro]: 

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

40859  200 
shows "{a..<b} \<in> sets borel" 
38656  201 
unfolding atLeastLessThan_def by blast 
202 

203 
lemma hafspace_less_borel[simp, intro]: 

204 
fixes a :: real 

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

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

207 

38656  208 
lemma hafspace_greater_borel[simp, intro]: 
209 
fixes a :: real 

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

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

212 

38656  213 
lemma hafspace_less_eq_borel[simp, intro]: 
214 
fixes a :: real 

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

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

217 

38656  218 
lemma hafspace_greater_eq_borel[simp, intro]: 
219 
fixes a :: real 

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

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

222 

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

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

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

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

227 
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

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

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

232 
then show ?thesis using f g 

233 
by simp (blast intro: measurable_sets) 

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

234 
qed 
38656  235 

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

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

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

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

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

240 
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

241 
proof  
38656  242 
have "{w \<in> space M. f w \<le> g w} = space M  {w \<in> space M. g w < f w}" 
243 
by auto 

244 
thus ?thesis using f g 

245 
by simp blast 

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

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

247 

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

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

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

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

252 
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

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

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

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

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

259 

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

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

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

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

264 
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

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

266 
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

267 
by auto 
38656  268 
thus ?thesis using f g by auto 
269 
qed 

270 

271 
subsection "Borel space equals sigma algebras over intervals" 

272 

273 
lemma rational_boxes: 

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

275 
assumes "0 < e" 

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

277 
proof  

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

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

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

281 
proof 

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

283 
show "?th i" by auto 

284 
qed 

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

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

287 
proof 

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

289 
show "?th i" by auto 

290 
qed 

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

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

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

294 
unfolding setL2_def[symmetric] by (rule euclidean_dist_l2) 

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

296 
proof (rule real_sqrt_less_mono, rule setsum_strict_mono) 

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

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

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

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

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

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

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

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

305 
by (rule power_strict_mono) auto 

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

307 
by (simp add: power_divide) 

308 
qed auto 

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

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

311 
with a b show ?thesis 

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

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

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

315 
qed 

316 

317 
lemma ex_rat_list: 

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

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

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

321 
proof  

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

323 
from choice[OF this] guess r .. 

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

325 
qed 

326 

327 
lemma open_UNION: 

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

329 
assumes "open M" 

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

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

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

333 
proof safe 

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

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

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

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

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

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

340 
"length q = DIM ('a)" 

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

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

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

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

345 
unfolding o_def by auto 

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

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

348 
unfolding o_def by auto 

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

350 
using p q ab by auto 

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

352 
qed auto 

353 

354 
lemma halfspace_span_open: 

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

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

358 
open_halfspace_component_lt) 

38656  359 

360 
lemma halfspace_lt_in_halfspace: 

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

38656  363 

364 
lemma halfspace_gt_in_halfspace: 

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

38656  367 
proof  
40859  368 
interpret sigma_algebra "?SIGMA" 
369 
by (intro sigma_algebra_sigma_sets) (simp_all add: sets_sigma) 

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

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

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

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

375 
by (auto simp: inverse_eq_divide field_simps) 

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

377 
by (blast intro: less_imp_le) 

378 
next 

379 
fix x n 

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

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

382 
finally show "a < x" . 

383 
qed 

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

385 
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

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

387 

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

38656  393 
then interpret sigma_algebra ?SIGMA . 
44537
c10485a6a7af
make HOLProbability respect set/pred distinction
huffman
parents:
44282
diff
changeset

394 
{ fix S :: "'a set" assume "S \<in> {S. open S}" 
c10485a6a7af
make HOLProbability respect set/pred distinction
huffman
parents:
44282
diff
changeset

395 
then have "open S" unfolding mem_Collect_eq . 
40859  396 
from open_UNION[OF this] 
397 
obtain I where *: "S = 

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

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

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

401 
unfolding greaterThanLessThan_def 

402 
unfolding eucl_greaterThan_eq_halfspaces[where 'a='a] 

403 
unfolding eucl_lessThan_eq_halfspaces[where 'a='a] 

404 
by blast 

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

406 
unfolding * 

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

408 
then show ?thesis unfolding borel_def 

409 
by (intro sets_sigma_subset) auto 

410 
qed 

38656  411 

412 
lemma halfspace_span_halfspace_le: 

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

38656  415 
(is "_ \<subseteq> sets ?SIGMA") 
40859  416 
proof  
417 
have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto 

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

421 
proof (safe, simp_all) 

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

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

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

425 
by (auto simp: field_simps inverse_eq_divide) 

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

427 
by (blast intro: less_imp_le) 

428 
next 

429 
fix x::'a and n 

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

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

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

433 
qed 

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

435 
by (safe intro!: countable_UN) 

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

437 
then show ?thesis by (intro sets_sigma_subset) auto 

438 
qed 

38656  439 

440 
lemma halfspace_span_halfspace_ge: 

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

38656  443 
(is "_ \<subseteq> sets ?SIGMA") 
40859  444 
proof  
445 
have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto 

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

449 
by (safe intro!: Diff) 

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

451 
then show ?thesis by (intro sets_sigma_subset) auto 

452 
qed 

38656  453 

454 
lemma halfspace_le_span_halfspace_gt: 

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

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

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

463 
by (safe intro!: Diff) 

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

465 
then show ?thesis by (intro sets_sigma_subset) auto 

466 
qed 

38656  467 

468 
lemma halfspace_le_span_atMost: 

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

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

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

480 
fix x 

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

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

483 
by (subst (asm) Max_le_iff) auto 

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

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

486 
qed 

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

488 
by (safe intro!: countable_UN) 

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

490 
next 

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

494 
qed 

40859  495 
then show ?thesis by (intro sets_sigma_subset) auto 
496 
qed 

38656  497 

498 
lemma halfspace_le_span_greaterThan: 

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

38656  501 
(is "_ \<subseteq> sets ?SIGMA") 
40859  502 
proof  
503 
have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto 

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

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

511 
fix x 

44666  512 
from reals_Archimedean2[of "Max ((\<lambda>i. x$$i)`{..<DIM('a)})"] 
38656  513 
guess k::nat .. note k = this 
514 
{ fix i assume "i < DIM('a)" 

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

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

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

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

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

520 
qed 

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

522 
apply (simp only:) 

523 
apply (safe intro!: countable_UN Diff) 

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

525 
next 

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

529 
qed 

40859  530 
then show ?thesis by (intro sets_sigma_subset) auto 
531 
qed 

532 

533 
lemma halfspace_le_span_lessThan: 

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

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

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

537 
proof  

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

539 
then interpret sigma_algebra ?SIGMA . 

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

541 
proof cases 

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

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

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

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

546 
fix x 

44666  547 
from reals_Archimedean2[of "Max ((\<lambda>i. x$$i)`{..<DIM('a)})"] 
40859  548 
guess k::nat .. note k = this 
549 
{ fix i assume "i < DIM('a)" 

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

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

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

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

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

555 
qed 

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

557 
apply (simp only:) 

558 
apply (safe intro!: countable_UN Diff) 

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

560 
next 

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

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

563 
using top by auto 

564 
qed 

565 
then show ?thesis by (intro sets_sigma_subset) auto 

566 
qed 

567 

568 
lemma atMost_span_atLeastAtMost: 

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

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

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

572 
proof  

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

574 
then interpret sigma_algebra ?SIGMA . 

575 
{ fix a::'a 

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

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

578 
fix x 

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

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

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

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

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

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

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

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

587 
qed 

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

589 
by (safe intro!: countable_UN) 

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

591 
then show ?thesis by (intro sets_sigma_subset) auto 

592 
qed 

593 

594 
lemma borel_eq_atMost: 

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

596 
(is "_ = ?SIGMA") 

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

600 
by auto 

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

602 
by (rule borel.sets_sigma_subset) auto 

603 
qed auto 

604 

605 
lemma borel_eq_atLeastAtMost: 

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

607 
(is "_ = ?SIGMA") 

40869  608 
proof (intro algebra.equality antisym) 
40859  609 
show "sets borel \<subseteq> sets ?SIGMA" 
610 
using atMost_span_atLeastAtMost halfspace_le_span_atMost 

611 
halfspace_span_halfspace_le open_span_halfspace 

612 
by auto 

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

614 
by (rule borel.sets_sigma_subset) auto 

615 
qed auto 

616 

617 
lemma borel_eq_greaterThan: 

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

619 
(is "_ = ?SIGMA") 

40869  620 
proof (intro algebra.equality antisym) 
40859  621 
show "sets borel \<subseteq> sets ?SIGMA" 
622 
using halfspace_le_span_greaterThan 

623 
halfspace_span_halfspace_le open_span_halfspace 

624 
by auto 

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

626 
by (rule borel.sets_sigma_subset) auto 

627 
qed auto 

628 

629 
lemma borel_eq_lessThan: 

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

631 
(is "_ = ?SIGMA") 

40869  632 
proof (intro algebra.equality antisym) 
40859  633 
show "sets borel \<subseteq> sets ?SIGMA" 
634 
using halfspace_le_span_lessThan 

635 
halfspace_span_halfspace_ge open_span_halfspace 

636 
by auto 

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

638 
by (rule borel.sets_sigma_subset) auto 

639 
qed auto 

640 

641 
lemma borel_eq_greaterThanLessThan: 

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

643 
(is "_ = ?SIGMA") 

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

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

648 
proof  

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

650 
then interpret sigma_algebra ?SIGMA . 

44537
c10485a6a7af
make HOLProbability respect set/pred distinction
huffman
parents:
44282
diff
changeset

651 
{ fix M :: "'a set" assume "M \<in> {S. open S}" 
c10485a6a7af
make HOLProbability respect set/pred distinction
huffman
parents:
44282
diff
changeset

652 
then have "open M" by simp 
40859  653 
have "M \<in> sets ?SIGMA" 
654 
apply (subst open_UNION[OF `open M`]) 

655 
apply (safe intro!: countable_UN) 

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

657 
then show ?thesis 

658 
unfolding borel_def by (intro sets_sigma_subset) auto 

659 
qed 

38656  660 
qed auto 
661 

42862  662 
lemma borel_eq_atLeastLessThan: 
663 
"borel = sigma \<lparr>space=UNIV, sets=range (\<lambda>(a, b). {a ..< b :: real})\<rparr>" (is "_ = ?S") 

664 
proof (intro algebra.equality antisym) 

665 
interpret sigma_algebra ?S 

666 
by (rule sigma_algebra_sigma) auto 

667 
show "sets borel \<subseteq> sets ?S" 

668 
unfolding borel_eq_lessThan 

669 
proof (intro sets_sigma_subset subsetI) 

670 
have move_uminus: "\<And>x y::real. x \<le> y \<longleftrightarrow> y \<le> x" by auto 

671 
fix A :: "real set" assume "A \<in> sets \<lparr>space = UNIV, sets = range lessThan\<rparr>" 

672 
then obtain x where "A = {..< x}" by auto 

673 
then have "A = (\<Union>i::nat. {real i ..< x})" 

674 
by (auto simp: move_uminus real_arch_simple) 

675 
then show "A \<in> sets ?S" 

676 
by (auto simp: sets_sigma intro!: sigma_sets.intros) 

677 
qed simp 

678 
show "sets ?S \<subseteq> sets borel" 

679 
by (intro borel.sets_sigma_subset) auto 

680 
qed simp_all 

681 

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

684 
(is "_ = ?SIGMA") 

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

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

689 
by (rule borel.sets_sigma_subset) auto 

690 
qed auto 

691 

692 
lemma borel_eq_halfspace_less: 

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

694 
(is "_ = ?SIGMA") 

40869  695 
proof (intro algebra.equality antisym) 
40859  696 
show "sets borel \<subseteq> sets ?SIGMA" 
697 
using open_span_halfspace . 

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

699 
by (rule borel.sets_sigma_subset) auto 

38656  700 
qed auto 
701 

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

704 
(is "_ = ?SIGMA") 

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

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

709 
by (rule borel.sets_sigma_subset) auto 

710 
qed auto 

38656  711 

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

714 
(is "_ = ?SIGMA") 

40869  715 
proof (intro algebra.equality antisym) 
40859  716 
show "sets borel \<subseteq> sets ?SIGMA" 
38656  717 
using halfspace_span_halfspace_ge open_span_halfspace by auto 
40859  718 
show "sets ?SIGMA \<subseteq> sets borel" 
719 
by (rule borel.sets_sigma_subset) auto 

720 
qed auto 

38656  721 

722 
lemma (in sigma_algebra) borel_measurable_halfspacesI: 

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

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

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

728 
proof safe 

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

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

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

732 
next 

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

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

735 
proof cases 

736 
assume "i < DIM('c)" 

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

738 
next 

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

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

741 
qed } 

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

745 
unfolding assms(1) by simp 

746 
qed 

747 

748 
lemma (in sigma_algebra) borel_measurable_iff_halfspace_le: 

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

750 
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  751 
by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_le]) auto 
38656  752 

753 
lemma (in sigma_algebra) borel_measurable_iff_halfspace_less: 

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

755 
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  756 
by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_less]) auto 
38656  757 

758 
lemma (in sigma_algebra) borel_measurable_iff_halfspace_ge: 

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

760 
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  761 
by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_ge]) auto 
38656  762 

763 
lemma (in sigma_algebra) borel_measurable_iff_halfspace_greater: 

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

765 
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  766 
by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_gt]) auto 
38656  767 

768 
lemma (in sigma_algebra) borel_measurable_iff_le: 

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

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

771 

772 
lemma (in sigma_algebra) borel_measurable_iff_less: 

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

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

775 

776 
lemma (in sigma_algebra) borel_measurable_iff_ge: 

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

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

779 

780 
lemma (in sigma_algebra) borel_measurable_iff_greater: 

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

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

783 

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

787 
proof (rule borel.measurable_sigma, simp_all) 

44537
c10485a6a7af
make HOLProbability respect set/pred distinction
huffman
parents:
44282
diff
changeset

788 
fix S::"real set" assume "open S" 
39087
96984bf6fa5b
Measurable on euclidean space is equiv. to measurable components
hoelzl
parents:
39083
diff
changeset

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

792 
qed 

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

793 

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

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

796 
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

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

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

799 
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

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

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

803 
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

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

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

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

807 

38656  808 
subsection "Borel measurable operators" 
809 

810 
lemma (in sigma_algebra) affine_borel_measurable_vector: 

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

812 
assumes "f \<in> borel_measurable M" 

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

814 
proof (rule borel_measurableI) 

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

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

817 
proof cases 

818 
assume "b \<noteq> 0" 

44537
c10485a6a7af
make HOLProbability respect set/pred distinction
huffman
parents:
44282
diff
changeset

819 
with `open S` have "open ((\<lambda>x. ( a + x) /\<^sub>R b) ` S)" (is "open ?S") 
c10485a6a7af
make HOLProbability respect set/pred distinction
huffman
parents:
44282
diff
changeset

820 
by (auto intro!: open_affinity simp: scaleR_add_right) 
40859  821 
hence "?S \<in> sets borel" 
822 
unfolding borel_def by (auto simp: sigma_def intro!: sigma_sets.Basic) 

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

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

40859  826 
ultimately show ?thesis using assms unfolding in_borel_measurable_borel 
38656  827 
by auto 
828 
qed simp 

829 
qed 

830 

831 
lemma (in sigma_algebra) affine_borel_measurable: 

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

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

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

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

836 

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

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

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

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

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

841 
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

842 
proof  
38656  843 
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

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

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

848 
by auto 

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

850 
by (simp add: 1) 

851 
then show ?thesis 

852 
by (simp add: borel_measurable_iff_ge) 

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

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

854 

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

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

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

857 
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

858 
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

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

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

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

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

863 

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

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

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

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

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

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

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

871 
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

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

873 
case less 
38656  874 
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

875 
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

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

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

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

880 
case equal 
38656  881 
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

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

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

884 
also have "... \<in> sets M" 
38656  885 
apply (insert f) 
886 
apply (rule Int) 

887 
apply (simp add: borel_measurable_iff_le) 

888 
apply (simp add: borel_measurable_iff_ge) 

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

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

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

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

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

893 
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

894 
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

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

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

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

899 
also have "... \<in> sets M" 
38656  900 
apply (insert f) 
901 
apply (rule Int) 

902 
apply (simp add: borel_measurable_iff_ge) 

903 
apply (simp add: borel_measurable_iff_le) 

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

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

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

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

907 
} 
38656  908 
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

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

910 

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

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

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

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

915 

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

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

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

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

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

921 
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

922 
by simp 
38656  923 
also have "... \<in> borel_measurable M" 
924 
by (fast intro: affine_borel_measurable g) 

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

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

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

927 

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

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

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

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

932 
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

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

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

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

941 
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

942 
show ?thesis 
38656  943 
apply (simp add: times_eq_sum_squares diff_minus) 
944 
using 1 2 by simp 

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

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

946 

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

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

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

949 
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

950 
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

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

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

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

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

955 

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

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

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

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

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

962 

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

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

38656  967 
unfolding borel_measurable_iff_ge unfolding inverse_eq_divide 
968 
proof safe 

969 
fix a :: real 

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

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

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

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

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

975 
by (auto intro!: Int Un) 

35692  976 
qed 
977 

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

35692  980 
assumes "f \<in> borel_measurable M" 
981 
and "g \<in> borel_measurable M" 

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

983 
unfolding field_divide_inverse 

38656  984 
by (rule borel_measurable_inverse borel_measurable_times assms)+ 
985 

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

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

988 
assumes "f \<in> borel_measurable M" 

989 
assumes "g \<in> borel_measurable M" 

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

991 
unfolding borel_measurable_iff_le 

992 
proof safe 

993 
fix a 

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

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

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

997 
using assms unfolding borel_measurable_iff_le 

998 
by (auto intro!: Int) 

999 
qed 

1000 

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

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

1003 
assumes "f \<in> borel_measurable M" 

1004 
assumes "g \<in> borel_measurable M" 

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

1006 
unfolding borel_measurable_iff_ge 

1007 
proof safe 

1008 
fix a 

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

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

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

1012 
using assms unfolding borel_measurable_iff_ge 

1013 
by (auto intro!: Int) 

1014 
qed 

1015 

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

1017 
assumes "f \<in> borel_measurable M" 

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

1019 
proof  

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

1021 
show ?thesis unfolding * using assms by auto 

1022 
qed 

1023 

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

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

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

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

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

1028 

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

1031 
assumes "continuous_on UNIV f" 

1032 
shows "f \<in> borel_measurable borel" 

1033 
apply(rule borel.borel_measurableI) 

1034 
using continuous_open_preimage[OF assms] unfolding vimage_def by auto 

1035 

1036 
lemma borel_measurable_continuous_on: 

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

42990
3706951a6421
composition of convex and measurable function is measurable
hoelzl
parents:
42950
diff
changeset

1038 
assumes cont: "continuous_on A f" "open A" 
41830  1039 
shows "(\<lambda>x. if x \<in> A then f x else c) \<in> borel_measurable borel" (is "?f \<in> _") 
1040 
proof (rule borel.borel_measurableI) 

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

42990
3706951a6421
composition of convex and measurable function is measurable
hoelzl
parents:
42950
diff
changeset

1042 
then have "open {x\<in>A. f x \<in> S}" 
41830  1043 
by (intro continuous_open_preimage[OF cont]) auto 
42990
3706951a6421
composition of convex and measurable function is measurable
hoelzl
parents:
42950
diff
changeset

1044 
then have *: "{x\<in>A. f x \<in> S} \<in> sets borel" by auto 
3706951a6421
composition of convex and measurable function is measurable
hoelzl
parents:
42950
diff
changeset

1045 
have "?f ` S \<inter> space borel = 
3706951a6421
composition of convex and measurable function is measurable
hoelzl
parents:
42950
diff
changeset

1046 
{x\<in>A. f x \<in> S} \<union> (if c \<in> S then space borel  A else {})" 
3706951a6421
composition of convex and measurable function is measurable
hoelzl
parents:
42950
diff
changeset

1047 
by (auto split: split_if_asm) 
3706951a6421
composition of convex and measurable function is measurable
hoelzl
parents:
42950
diff
changeset

1048 
also have "\<dots> \<in> sets borel" 
3706951a6421
composition of convex and measurable function is measurable
hoelzl
parents:
42950
diff
changeset

1049 
using * `open A` by (auto simp del: space_borel intro!: borel.Un) 
3706951a6421
composition of convex and measurable function is measurable
hoelzl
parents:
42950
diff
changeset

1050 
finally show "?f ` S \<inter> space borel \<in> sets borel" . 
3706951a6421
composition of convex and measurable function is measurable
hoelzl
parents:
42950
diff
changeset

1051 
qed 
3706951a6421
composition of convex and measurable function is measurable
hoelzl
parents:
42950
diff
changeset

1052 

3706951a6421
composition of convex and measurable function is measurable
hoelzl
parents:
42950
diff
changeset

1053 
lemma (in sigma_algebra) convex_measurable: 
3706951a6421
composition of convex and measurable function is measurable
hoelzl
parents:
42950
diff
changeset

1054 
fixes a b :: real 
3706951a6421
composition of convex and measurable function is measurable
hoelzl
parents:
42950
diff
changeset

1055 
assumes X: "X \<in> borel_measurable M" "X ` space M \<subseteq> { a <..< b}" 
3706951a6421
composition of convex and measurable function is measurable
hoelzl
parents:
42950
diff
changeset

1056 
assumes q: "convex_on { a <..< b} q" 
3706951a6421
composition of convex and measurable function is measurable
hoelzl
parents:
42950
diff
changeset

1057 
shows "q \<circ> X \<in> borel_measurable M" 
3706951a6421
composition of convex and measurable function is measurable
hoelzl
parents:
42950
diff
changeset

1058 
proof  
3706951a6421
composition of convex and measurable function is measurable
hoelzl
parents:
42950
diff
changeset

1059 
have "(\<lambda>x. if x \<in> {a <..< b} then q x else 0) \<in> borel_measurable borel" 
3706951a6421
composition of convex and measurable function is measurable
hoelzl
parents:
42950
diff
changeset

1060 
proof (rule borel_measurable_continuous_on) 
3706951a6421
composition of convex and measurable function is measurable
hoelzl
parents:
42950
diff
changeset

1061 
show "open {a<..<b}" by auto 
3706951a6421
composition of convex and measurable function is measurable
hoelzl
parents:
42950
diff
changeset

1062 
from this q show "continuous_on {a<..<b} q" 
3706951a6421
composition of convex and measurable function is measurable
hoelzl
parents:
42950
diff
changeset

1063 
by (rule convex_on_continuous) 
41830  1064 
qed 
42990
3706951a6421
composition of convex and measurable function is measurable
hoelzl
parents:
42950
diff
changeset

1065 
then have "(\<lambda>x. if x \<in> {a <..< b} then q x else 0) \<circ> X \<in> borel_measurable M" (is ?qX) 
3706951a6421
composition of convex and measurable function is measurable
hoelzl
parents:
42950
diff
changeset

1066 
using X by (intro measurable_comp) auto 
3706951a6421
composition of convex and measurable function is measurable
hoelzl
parents:
42950
diff
changeset

1067 
moreover have "?qX \<longleftrightarrow> q \<circ> X \<in> borel_measurable M" 
3706951a6421
composition of convex and measurable function is measurable
hoelzl
parents:
42950
diff
changeset

1068 
using X by (intro measurable_cong) auto 
3706951a6421
composition of convex and measurable function is measurable
hoelzl
parents:
42950
diff
changeset

1069 
ultimately show ?thesis by simp 
41830  1070 
qed 
1071 

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

1073 
proof  

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

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

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

1077 
by (auto simp: ln_def log_def) } 

1078 
note log_imp = this 

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

1080 
proof (rule borel_measurable_continuous_on) 

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

1082 
by (auto intro!: continuous_at_imp_continuous_on DERIV_log DERIV_isCont 

1083 
simp: continuous_isCont[symmetric]) 

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

1085 
qed 

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

1087 
by (simp add: fun_eq_iff not_less log_imp) 

1088 
finally show ?thesis . 

1089 
qed 

1090 

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

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

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

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

1095 
by (simp add: comp_def) 

1096 

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

1097 
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

1098 

43920  1099 
lemma borel_measurable_ereal_borel: 
1100 
"ereal \<in> borel_measurable borel" 

1101 
unfolding borel_def[where 'a=ereal] 

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

1102 
proof (rule borel.measurable_sigma) 
44537
c10485a6a7af
make HOLProbability respect set/pred distinction
huffman
parents:
44282
diff
changeset

1103 
fix X :: "ereal set" assume "X \<in> sets \<lparr>space = UNIV, sets = {S. open S} \<rparr>" 
c10485a6a7af
make HOLProbability respect set/pred distinction
huffman
parents:
44282
diff
changeset

1104 
then have "open X" by simp 
43920  1105 
then have "open (ereal ` X \<inter> space borel)" 
1106 
by (simp add: open_ereal_vimage) 

1107 
then show "ereal ` X \<inter> space borel \<in> sets borel" by auto 

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

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

1109 

43920  1110 
lemma (in sigma_algebra) borel_measurable_ereal[simp, intro]: 
1111 
assumes f: "f \<in> borel_measurable M" shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M" 

1112 
using measurable_comp[OF f borel_measurable_ereal_borel] unfolding comp_def . 

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

1113 

43920  1114 
lemma borel_measurable_real_of_ereal_borel: 
1115 
"(real :: ereal \<Rightarrow> real) \<in> borel_measurable borel" 

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

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

1117 
proof (rule borel.measurable_sigma) 
44537
c10485a6a7af
make HOLProbability respect set/pred distinction
huffman
parents:
44282
diff
changeset

1118 
fix B :: "real set" assume "B \<in> sets \<lparr>space = UNIV, sets = {S. open S} \<rparr>" 
c10485a6a7af
make HOLProbability respect set/pred distinction
huffman
parents:
44282
diff
changeset

1119 
then have "open B" by simp 
43920  1120 
have *: "ereal ` real ` (B  {0}) = B  {0}" by auto 
1121 
have open_real: "open (real ` (B  {0}) :: ereal set)" 

1122 
unfolding open_ereal_def * using `open B` by auto 

1123 
show "(real ` B \<inter> space borel :: ereal set) \<in> sets borel" 

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

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

1125 
assume "0 \<in> B" 
43923  1126 
then have *: "real ` B = real ` (B  {0}) \<union> {\<infinity>, \<infinity>, 0::ereal}" 
43920  1127 
by (auto simp add: real_of_ereal_eq_0) 
1128 
then show "(real ` B :: ereal set) \<inter> space borel \<in> sets borel" 

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

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

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

1131 
assume "0 \<notin> B" 
43920  1132 
then have *: "(real ` B :: ereal set) = real ` (B  {0})" 
1133 
by (auto simp add: real_of_ereal_eq_0) 

1134 
then show "(real ` B :: ereal set) \<inter> space borel \<in> sets borel" 

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

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

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

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

1138 

43920  1139 
lemma (in sigma_algebra) borel_measurable_real_of_ereal[simp, intro]: 
1140 
assumes f: "f \<in> borel_measurable M" shows "(\<lambda>x. real (f x :: ereal)) \<in> borel_measurable M" 

1141 
using measurable_comp[OF f borel_measurable_real_of_ereal_borel] unfolding comp_def . 

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

1142 

43920  1143 
lemma (in sigma_algebra) borel_measurable_ereal_iff: 
1144 
shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M" 

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

1145 
proof 
43920  1146 
assume "(\<lambda>x. ereal (f x)) \<in> borel_measurable M" 
1147 
from borel_measurable_real_of_ereal[OF this] 

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

1148 
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

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

1150 

43920  1151 
lemma (in sigma_algebra) borel_measurable_ereal_iff_real: 
43923  1152 
fixes f :: "'a \<Rightarrow> ereal" 
1153 
shows "f \<in> borel_measurable M \<longleftrightarrow> 

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

1154 
((\<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

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

1156 
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

1157 
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

1158 
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 
43920  1159 
let "?f x" = "if f x = \<infinity> then \<infinity> else if f x = \<infinity> then \<infinity> else ereal (real (f x))" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1160 
have "?f \<in> borel_measurable M" using * ** by (intro measurable_If) auto 
43920  1161 
also have "?f = f" by (auto simp: fun_eq_iff ereal_real) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1162 
finally show "f \<in> borel_measurable M" . 
43920  1163 
qed (auto intro: measurable_sets borel_measurable_real_of_ereal) 
41830  1164 

38656  1165 
lemma (in sigma_algebra) less_eq_ge_measurable: 
1166 
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

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

1169 
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

1170 
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

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

1173 
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

1174 
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

1175 
ultimately show "f ` {a <..} \<inter> space M \<in> sets M" by auto 
38656  1176 
qed 
35692  1177 

38656  1178 
lemma (in sigma_algebra) greater_eq_le_measurable: 
1179 
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

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

1182 
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

1183 
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

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

1186 
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

1187 
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

1188 
ultimately show "f ` {a ..} \<inter> space M \<in> sets M" by auto 
38656  1189 
qed 
1190 

43920  1191 
lemma (in sigma_algebra) borel_measurable_uminus_borel_ereal: 
1192 
"(uminus :: ereal \<Rightarrow> ereal) \<in> borel_measurable borel" 

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

1193 
proof (subst borel_def, rule borel.measurable_sigma) 
44537
c10485a6a7af
make HOLProbability respect set/pred distinction
huffman
parents:
44282
diff
changeset

1194 
fix X :: "ereal set" assume "X \<in> sets \<lparr>space = UNIV, sets = {S. open S}\<rparr>" 
c10485a6a7af
make HOLProbability respect set/pred distinction
huffman
parents:
44282
diff
changeset

1195 
then have "open X" by simp 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1196 
have "uminus ` X = uminus ` X" by (force simp: image_iff) 
43920  1197 
then have "open (uminus ` X)" using `open X` ereal_open_uminus by auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1198 
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

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

1200 

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

1202 
assumes "f \<in> borel_measurable M" 
43920  1203 
shows "(\<lambda>x.  f x :: ereal) \<in> borel_measurable M" 
1204 
using measurable_comp[OF assms borel_measurable_uminus_borel_ereal] by (simp add: comp_def) 

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

1205 

43920  1206 
lemma (in sigma_algebra) borel_measurable_uminus_eq_ereal[simp]: 
1207 
"(\<lambda>x.  f x :: ereal) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M" (is "?l = ?r") 

38656  1208 
proof 
43920  1209 
assume ?l from borel_measurable_uminus_ereal[OF this] show ?r by simp 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

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

1211 

43920  1212 
lemma (in sigma_algebra) borel_measurable_eq_atMost_ereal: 
43923  1213 
fixes f :: "'a \<Rightarrow> ereal" 
1214 
shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f ` {..a} \<inter> space M \<in> sets M)" 

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

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

1216 
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

1217 
show "f \<in> borel_measurable M" 
43920  1218 
unfolding borel_measurable_ereal_iff_real borel_measurable_iff_le 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

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

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

1222 
have "x = \<infinity>" 
43920  1223 
proof (rule ereal_top) 
44666  1224 
fix B from reals_Archimedean2[of B] guess n .. 
43920  1225 
then have "ereal B < real n" by auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1226 
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

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

1228 
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

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

1230 
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

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

1233 
then show "f ` {\<infinity>} \<inter> space M \<in> sets M" using pos by auto 
43920  1234 
moreover have "{x\<in>space M. f x \<le> ereal a} \<in> sets M" 
1235 
using pos[of "ereal a"] by (simp add: vimage_def Int_def conj_commute) 

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

1236 
moreover have "{w \<in> space M. real (f w) \<le> a} = 
43920  1237 
(if a < 0 then {w \<in> space M. f w \<le> ereal a}  f ` {\<infinity>} \<inter> space M 
1238 
else {w \<in> space M. f w \<le> ereal a} \<union> (f ` {\<infinity>} \<inter> space M) \<union> (f ` {\<infinity>} \<inter> space M))" (is "?l = ?r") 

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

1239 
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

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

1242 
qed (simp add: measurable_sets) 
35582  1243 

43920  1244 
lemma (in sigma_algebra) borel_measurable_eq_atLeast_ereal: 
1245 
"(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f ` {a..} \<inter> space M \<in> sets M)" 

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

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

1247 
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

1248 
moreover have "\<And>a. (\<lambda>x.  f x) ` {..a} = f ` {a ..}" 
43920 