author  hoelzl 
Fri, 02 Nov 2012 14:23:40 +0100  
changeset 50002  ce0d316b5b44 
parent 50001  382bd3173584 
child 50003  8c213922ed49 
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 

47694  14 
definition borel :: "'a::topological_space measure" where 
15 
"borel = sigma UNIV {S. open S}" 

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

16 

47694  17 
abbreviation "borel_measurable M \<equiv> measurable M borel" 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

18 

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

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

20 
"f \<in> borel_measurable M \<longleftrightarrow> 
47694  21 
(\<forall>S \<in> sigma_sets UNIV {S. open S}. f ` S \<inter> space M \<in> sets M)" 
40859  22 
by (auto simp add: measurable_def borel_def) 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

23 

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

29 

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

38656  32 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

33 
lemma space_in_borel[measurable]: "UNIV \<in> sets borel" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

34 
unfolding borel_def by auto 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

35 

ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

36 
lemma pred_Collect_borel[measurable (raw)]: "Sigma_Algebra.pred borel P \<Longrightarrow> {x. P x} \<in> sets borel" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

37 
unfolding borel_def pred_def by auto 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

38 

ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

39 
lemma borel_open[simp, measurable (raw generic)]: 
40859  40 
assumes "open A" shows "A \<in> sets borel" 
38656  41 
proof  
44537
c10485a6a7af
make HOLProbability respect set/pred distinction
huffman
parents:
44282
diff
changeset

42 
have "A \<in> {S. open S}" unfolding mem_Collect_eq using assms . 
47694  43 
thus ?thesis unfolding borel_def by auto 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

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

45 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

46 
lemma borel_closed[simp, measurable (raw generic)]: 
40859  47 
assumes "closed A" shows "A \<in> sets borel" 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

48 
proof  
40859  49 
have "space borel  ( A) \<in> sets borel" 
50 
using assms unfolding closed_def by (blast intro: borel_open) 

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

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

53 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

54 
lemma borel_insert[measurable]: 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

55 
"A \<in> sets borel \<Longrightarrow> insert x A \<in> sets (borel :: 'a::t2_space measure)" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

56 
unfolding insert_def by (rule Un) auto 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

57 

ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

58 
lemma borel_comp[intro, simp, measurable]: "A \<in> sets borel \<Longrightarrow>  A \<in> sets borel" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

59 
unfolding Compl_eq_Diff_UNIV by simp 
41830  60 

47694  61 
lemma borel_measurable_vimage: 
38656  62 
fixes f :: "'a \<Rightarrow> 'x::t2_space" 
50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

63 
assumes borel[measurable]: "f \<in> borel_measurable M" 
38656  64 
shows "f ` {x} \<inter> space M \<in> sets M" 
50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

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

66 

47694  67 
lemma borel_measurableI: 
38656  68 
fixes f :: "'a \<Rightarrow> 'x\<Colon>topological_space" 
69 
assumes "\<And>S. open S \<Longrightarrow> f ` S \<inter> space M \<in> sets M" 

70 
shows "f \<in> borel_measurable M" 

40859  71 
unfolding borel_def 
47694  72 
proof (rule measurable_measure_of, simp_all) 
44537
c10485a6a7af
make HOLProbability respect set/pred distinction
huffman
parents:
44282
diff
changeset

73 
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

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

76 

40859  77 
lemma borel_singleton[simp, intro]: 
38656  78 
fixes x :: "'a::t1_space" 
40859  79 
shows "A \<in> sets borel \<Longrightarrow> insert x A \<in> sets borel" 
47694  80 
proof (rule insert_in_sets) 
40859  81 
show "{x} \<in> sets borel" 
41969  82 
using closed_singleton[of x] by (rule borel_closed) 
38656  83 
qed simp 
84 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

85 
lemma borel_measurable_const[simp, intro, measurable (raw)]: 
38656  86 
"(\<lambda>x. c) \<in> borel_measurable M" 
47694  87 
by auto 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

88 

47694  89 
lemma borel_measurable_indicator[simp, intro!]: 
38656  90 
assumes A: "A \<in> sets M" 
91 
shows "indicator A \<in> borel_measurable M" 

46905  92 
unfolding indicator_def [abs_def] using A 
47694  93 
by (auto intro!: measurable_If_set) 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

94 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

95 
lemma borel_measurable_indicator'[measurable]: 
50001
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49774
diff
changeset

96 
"{x\<in>space M. x \<in> A} \<in> sets M \<Longrightarrow> indicator A \<in> borel_measurable M" 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49774
diff
changeset

97 
unfolding indicator_def[abs_def] 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49774
diff
changeset

98 
by (auto intro!: measurable_If) 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49774
diff
changeset

99 

47694  100 
lemma borel_measurable_indicator_iff: 
40859  101 
"(indicator A :: 'a \<Rightarrow> 'x::{t1_space, zero_neq_one}) \<in> borel_measurable M \<longleftrightarrow> A \<inter> space M \<in> sets M" 
102 
(is "?I \<in> borel_measurable M \<longleftrightarrow> _") 

103 
proof 

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

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

106 
unfolding measurable_def by auto 

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

46905  108 
unfolding indicator_def [abs_def] by auto 
40859  109 
finally show "A \<inter> space M \<in> sets M" . 
110 
next 

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

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

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

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

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

116 
qed 

117 

47694  118 
lemma borel_measurable_subalgebra: 
41545  119 
assumes "sets N \<subseteq> sets M" "space N = space M" "f \<in> borel_measurable N" 
39092  120 
shows "f \<in> borel_measurable M" 
121 
using assms unfolding measurable_def by auto 

122 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

123 
lemma borel_measurable_continuous_on1: 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

124 
fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

125 
assumes "continuous_on UNIV f" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

126 
shows "f \<in> borel_measurable borel" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

127 
apply(rule borel_measurableI) 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

128 
using continuous_open_preimage[OF assms] unfolding vimage_def by auto 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

129 

38656  130 
section "Borel spaces on euclidean spaces" 
131 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

132 
lemma borel_measurable_euclidean_component'[measurable]: 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

133 
"(\<lambda>x::'a::euclidean_space. x $$ i) \<in> borel_measurable borel" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

134 
by (intro continuous_on_euclidean_component continuous_on_id borel_measurable_continuous_on1) 
38656  135 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

136 
lemma borel_measurable_euclidean_component: 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

137 
"(f :: 'a \<Rightarrow> 'b::euclidean_space) \<in> borel_measurable M \<Longrightarrow>(\<lambda>x. f x $$ i) \<in> borel_measurable M" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

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

139 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

140 
lemma [simp, intro, measurable]: 
38656  141 
fixes a b :: "'a\<Colon>ordered_euclidean_space" 
50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

142 
shows lessThan_borel: "{..< a} \<in> sets borel" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

143 
and greaterThan_borel: "{a <..} \<in> sets borel" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

144 
and greaterThanLessThan_borel: "{a<..<b} \<in> sets borel" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

145 
and atMost_borel: "{..a} \<in> sets borel" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

146 
and atLeast_borel: "{a..} \<in> sets borel" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

147 
and atLeastAtMost_borel: "{a..b} \<in> sets borel" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

148 
and greaterThanAtMost_borel: "{a<..b} \<in> sets borel" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

149 
and atLeastLessThan_borel: "{a..<b} \<in> sets borel" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

150 
unfolding greaterThanAtMost_def atLeastLessThan_def 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

151 
by (blast intro: borel_open borel_closed)+ 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

152 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

153 
lemma 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

154 
shows hafspace_less_borel[simp, intro]: "{x::'a::euclidean_space. a < x $$ i} \<in> sets borel" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

155 
and hafspace_greater_borel[simp, intro]: "{x::'a::euclidean_space. x $$ i < a} \<in> sets borel" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

156 
and hafspace_less_eq_borel[simp, intro]: "{x::'a::euclidean_space. a \<le> x $$ i} \<in> sets borel" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

157 
and hafspace_greater_eq_borel[simp, intro]: "{x::'a::euclidean_space. x $$ i \<le> a} \<in> sets borel" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

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

159 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

160 
lemma borel_measurable_less[simp, intro, measurable]: 
38656  161 
fixes f :: "'a \<Rightarrow> real" 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

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

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

164 
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

165 
proof  
50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

166 
have "{w \<in> space M. f w < g w} = {x \<in> space M. \<exists>r. f x < of_rat r \<and> of_rat r < g x}" 
38656  167 
using Rats_dense_in_real by (auto simp add: Rats_def) 
50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

168 
with f g show ?thesis 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

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

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

171 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

172 
lemma [simp, intro]: 
38656  173 
fixes f :: "'a \<Rightarrow> real" 
50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

174 
assumes f[measurable]: "f \<in> borel_measurable M" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

175 
assumes g[measurable]: "g \<in> borel_measurable M" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

176 
shows borel_measurable_le[measurable]: "{w \<in> space M. f w \<le> g w} \<in> sets M" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

177 
and borel_measurable_eq[measurable]: "{w \<in> space M. f w = g w} \<in> sets M" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

178 
and borel_measurable_neq: "{w \<in> space M. f w \<noteq> g w} \<in> sets M" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

179 
unfolding eq_iff not_less[symmetric] by measurable+ 
38656  180 

181 
subsection "Borel space equals sigma algebras over intervals" 

182 

183 
lemma rational_boxes: 

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

185 
assumes "0 < e" 

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

187 
proof  

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

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

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

191 
proof 

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

193 
show "?th i" by auto 

194 
qed 

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

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

197 
proof 

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

199 
show "?th i" by auto 

200 
qed 

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

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

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

204 
unfolding setL2_def[symmetric] by (rule euclidean_dist_l2) 

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

206 
proof (rule real_sqrt_less_mono, rule setsum_strict_mono) 

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

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

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

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

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

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

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

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

215 
by (rule power_strict_mono) auto 

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

217 
by (simp add: power_divide) 

218 
qed auto 

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

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

221 
with a b show ?thesis 

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

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

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

225 
qed 

226 

227 
lemma ex_rat_list: 

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

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

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

231 
proof  

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

233 
from choice[OF this] guess r .. 

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

235 
qed 

236 

237 
lemma open_UNION: 

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

239 
assumes "open M" 

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

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

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

243 
proof safe 

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

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

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

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

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

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

250 
"length q = DIM ('a)" 

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

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

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

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

255 
unfolding o_def by auto 

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

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

258 
unfolding o_def by auto 

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

260 
using p q ab by auto 

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

262 
qed auto 

263 

47694  264 
lemma borel_sigma_sets_subset: 
265 
"A \<subseteq> sets borel \<Longrightarrow> sigma_sets UNIV A \<subseteq> sets borel" 

266 
using sigma_sets_subset[of A borel] by simp 

267 

268 
lemma borel_eq_sigmaI1: 

269 
fixes F :: "'i \<Rightarrow> 'a::topological_space set" and X :: "'a::topological_space set set" 

270 
assumes borel_eq: "borel = sigma UNIV X" 

271 
assumes X: "\<And>x. x \<in> X \<Longrightarrow> x \<in> sets (sigma UNIV (range F))" 

272 
assumes F: "\<And>i. F i \<in> sets borel" 

273 
shows "borel = sigma UNIV (range F)" 

274 
unfolding borel_def 

275 
proof (intro sigma_eqI antisym) 

276 
have borel_rev_eq: "sigma_sets UNIV {S::'a set. open S} = sets borel" 

277 
unfolding borel_def by simp 

278 
also have "\<dots> = sigma_sets UNIV X" 

279 
unfolding borel_eq by simp 

280 
also have "\<dots> \<subseteq> sigma_sets UNIV (range F)" 

281 
using X by (intro sigma_algebra.sigma_sets_subset[OF sigma_algebra_sigma_sets]) auto 

282 
finally show "sigma_sets UNIV {S. open S} \<subseteq> sigma_sets UNIV (range F)" . 

283 
show "sigma_sets UNIV (range F) \<subseteq> sigma_sets UNIV {S. open S}" 

284 
unfolding borel_rev_eq using F by (intro borel_sigma_sets_subset) auto 

285 
qed auto 

38656  286 

47694  287 
lemma borel_eq_sigmaI2: 
288 
fixes F :: "'i \<Rightarrow> 'j \<Rightarrow> 'a::topological_space set" 

289 
and G :: "'l \<Rightarrow> 'k \<Rightarrow> 'a::topological_space set" 

290 
assumes borel_eq: "borel = sigma UNIV (range (\<lambda>(i, j). G i j))" 

291 
assumes X: "\<And>i j. G i j \<in> sets (sigma UNIV (range (\<lambda>(i, j). F i j)))" 

292 
assumes F: "\<And>i j. F i j \<in> sets borel" 

293 
shows "borel = sigma UNIV (range (\<lambda>(i, j). F i j))" 

294 
using assms by (intro borel_eq_sigmaI1[where X="range (\<lambda>(i, j). G i j)" and F="(\<lambda>(i, j). F i j)"]) auto 

295 

296 
lemma borel_eq_sigmaI3: 

297 
fixes F :: "'i \<Rightarrow> 'j \<Rightarrow> 'a::topological_space set" and X :: "'a::topological_space set set" 

298 
assumes borel_eq: "borel = sigma UNIV X" 

299 
assumes X: "\<And>x. x \<in> X \<Longrightarrow> x \<in> sets (sigma UNIV (range (\<lambda>(i, j). F i j)))" 

300 
assumes F: "\<And>i j. F i j \<in> sets borel" 

301 
shows "borel = sigma UNIV (range (\<lambda>(i, j). F i j))" 

302 
using assms by (intro borel_eq_sigmaI1[where X=X and F="(\<lambda>(i, j). F i j)"]) auto 

303 

304 
lemma borel_eq_sigmaI4: 

305 
fixes F :: "'i \<Rightarrow> 'a::topological_space set" 

306 
and G :: "'l \<Rightarrow> 'k \<Rightarrow> 'a::topological_space set" 

307 
assumes borel_eq: "borel = sigma UNIV (range (\<lambda>(i, j). G i j))" 

308 
assumes X: "\<And>i j. G i j \<in> sets (sigma UNIV (range F))" 

309 
assumes F: "\<And>i. F i \<in> sets borel" 

310 
shows "borel = sigma UNIV (range F)" 

311 
using assms by (intro borel_eq_sigmaI1[where X="range (\<lambda>(i, j). G i j)" and F=F]) auto 

312 

313 
lemma borel_eq_sigmaI5: 

314 
fixes F :: "'i \<Rightarrow> 'j \<Rightarrow> 'a::topological_space set" and G :: "'l \<Rightarrow> 'a::topological_space set" 

315 
assumes borel_eq: "borel = sigma UNIV (range G)" 

316 
assumes X: "\<And>i. G i \<in> sets (sigma UNIV (range (\<lambda>(i, j). F i j)))" 

317 
assumes F: "\<And>i j. F i j \<in> sets borel" 

318 
shows "borel = sigma UNIV (range (\<lambda>(i, j). F i j))" 

319 
using assms by (intro borel_eq_sigmaI1[where X="range G" and F="(\<lambda>(i, j). F i j)"]) auto 

38656  320 

321 
lemma halfspace_gt_in_halfspace: 

47694  322 
"{x\<Colon>'a. a < x $$ i} \<in> sigma_sets UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i < a}))" 
323 
(is "?set \<in> ?SIGMA") 

38656  324 
proof  
47694  325 
interpret sigma_algebra UNIV ?SIGMA 
326 
by (intro sigma_algebra_sigma_sets) simp_all 

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

38656  328 
proof (safe, simp_all add: not_less) 
50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

329 
fix x :: 'a assume "a < x $$ i" 
38656  330 
with reals_Archimedean[of "x $$ i  a"] 
331 
obtain n where "a + 1 / real (Suc n) < x $$ i" 

332 
by (auto simp: inverse_eq_divide field_simps) 

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

334 
by (blast intro: less_imp_le) 

335 
next 

336 
fix x n 

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

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

339 
finally show "a < x" . 

340 
qed 

47694  341 
show "?set \<in> ?SIGMA" unfolding * 
50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

342 
by (auto del: Diff intro!: Diff) 
40859  343 
qed 
38656  344 

47694  345 
lemma borel_eq_halfspace_less: 
346 
"borel = sigma UNIV (range (\<lambda>(a, i). {x::'a::ordered_euclidean_space. x $$ i < a}))" 

347 
(is "_ = ?SIGMA") 

348 
proof (rule borel_eq_sigmaI3[OF borel_def]) 

349 
fix S :: "'a set" assume "S \<in> {S. open S}" 

350 
then have "open S" by simp 

351 
from open_UNION[OF this] 

352 
obtain I where *: "S = 

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

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

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

356 
unfolding greaterThanLessThan_def 

357 
unfolding eucl_greaterThan_eq_halfspaces[where 'a='a] 

358 
unfolding eucl_lessThan_eq_halfspaces[where 'a='a] 

359 
by blast 

360 
show "S \<in> ?SIGMA" 

361 
unfolding * 

362 
by (safe intro!: countable_UN Int countable_INT) (auto intro!: halfspace_gt_in_halfspace) 

363 
qed auto 

38656  364 

47694  365 
lemma borel_eq_halfspace_le: 
366 
"borel = sigma UNIV (range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. x $$ i \<le> a}))" 

367 
(is "_ = ?SIGMA") 

368 
proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_less]) 

369 
fix a i 

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

371 
proof (safe, simp_all) 

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

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

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

375 
by (auto simp: field_simps inverse_eq_divide) 

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

377 
by (blast intro: less_imp_le) 

378 
next 

379 
fix x::'a and n 

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

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

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

383 
qed 

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

385 
by (safe intro!: countable_UN) auto 

386 
qed auto 

38656  387 

47694  388 
lemma borel_eq_halfspace_ge: 
389 
"borel = sigma UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. a \<le> x $$ i}))" 

390 
(is "_ = ?SIGMA") 

391 
proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_less]) 

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

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

394 
by (safe intro!: compl_sets) auto 

395 
qed auto 

38656  396 

47694  397 
lemma borel_eq_halfspace_greater: 
398 
"borel = sigma UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. a < x $$ i}))" 

399 
(is "_ = ?SIGMA") 

400 
proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_le]) 

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

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

403 
by (safe intro!: compl_sets) auto 

404 
qed auto 

405 

406 
lemma borel_eq_atMost: 

407 
"borel = sigma UNIV (range (\<lambda>a. {..a\<Colon>'a\<Colon>ordered_euclidean_space}))" 

408 
(is "_ = ?SIGMA") 

409 
proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_le]) 

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

38656  411 
proof cases 
47694  412 
assume "i < DIM('a)" 
38656  413 
then have *: "{x::'a. x$$i \<le> a} = (\<Union>k::nat. {.. (\<chi>\<chi> n. if n = i then a else real k)})" 
414 
proof (safe, simp_all add: eucl_le[where 'a='a] split: split_if_asm) 

415 
fix x 

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

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

418 
by (subst (asm) Max_le_iff) auto 

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

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

421 
qed 

47694  422 
show "{x. x$$i \<le> a} \<in> ?SIGMA" unfolding * 
423 
by (safe intro!: countable_UN) auto 

424 
qed (auto intro: sigma_sets_top sigma_sets.Empty) 

425 
qed auto 

38656  426 

47694  427 
lemma borel_eq_greaterThan: 
428 
"borel = sigma UNIV (range (\<lambda>a\<Colon>'a\<Colon>ordered_euclidean_space. {a<..}))" 

429 
(is "_ = ?SIGMA") 

430 
proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_le]) 

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

38656  432 
proof cases 
47694  433 
assume "i < DIM('a)" 
434 
have "{x::'a. x$$i \<le> a} = UNIV  {x::'a. a < x$$i}" by auto 

38656  435 
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)` 
436 
proof (safe, simp_all add: eucl_less[where 'a='a] split: split_if_asm) 

437 
fix x 

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

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

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

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

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

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

446 
qed 

47694  447 
finally show "{x. x$$i \<le> a} \<in> ?SIGMA" 
38656  448 
apply (simp only:) 
449 
apply (safe intro!: countable_UN Diff) 

47694  450 
apply (auto intro: sigma_sets_top) 
46731  451 
done 
47694  452 
qed (auto intro: sigma_sets_top sigma_sets.Empty) 
453 
qed auto 

40859  454 

47694  455 
lemma borel_eq_lessThan: 
456 
"borel = sigma UNIV (range (\<lambda>a\<Colon>'a\<Colon>ordered_euclidean_space. {..<a}))" 

457 
(is "_ = ?SIGMA") 

458 
proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_ge]) 

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

40859  460 
proof cases 
461 
fix a i assume "i < DIM('a)" 

47694  462 
have "{x::'a. a \<le> x$$i} = UNIV  {x::'a. x$$i < a}" by auto 
40859  463 
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)` 
464 
proof (safe, simp_all add: eucl_less[where 'a='a] split: split_if_asm) 

465 
fix x 

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

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

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

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

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

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

474 
qed 

47694  475 
finally show "{x. a \<le> x$$i} \<in> ?SIGMA" 
40859  476 
apply (simp only:) 
477 
apply (safe intro!: countable_UN Diff) 

47694  478 
apply (auto intro: sigma_sets_top) 
46731  479 
done 
47694  480 
qed (auto intro: sigma_sets_top sigma_sets.Empty) 
40859  481 
qed auto 
482 

483 
lemma borel_eq_atLeastAtMost: 

47694  484 
"borel = sigma UNIV (range (\<lambda>(a,b). {a..b} \<Colon>'a\<Colon>ordered_euclidean_space set))" 
485 
(is "_ = ?SIGMA") 

486 
proof (rule borel_eq_sigmaI5[OF borel_eq_atMost]) 

487 
fix a::'a 

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

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

490 
fix x 

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

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

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

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

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

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

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

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

499 
qed 

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

501 
by (safe intro!: countable_UN) 

502 
(auto intro!: sigma_sets_top) 

40859  503 
qed auto 
504 

505 
lemma borel_eq_greaterThanLessThan: 

47694  506 
"borel = sigma UNIV (range (\<lambda> (a, b). {a <..< b} :: 'a \<Colon> ordered_euclidean_space set))" 
40859  507 
(is "_ = ?SIGMA") 
47694  508 
proof (rule borel_eq_sigmaI1[OF borel_def]) 
509 
fix M :: "'a set" assume "M \<in> {S. open S}" 

510 
then have "open M" by simp 

511 
show "M \<in> ?SIGMA" 

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

513 
apply (safe intro!: countable_UN) 

514 
apply auto 

515 
done 

38656  516 
qed auto 
517 

42862  518 
lemma borel_eq_atLeastLessThan: 
47694  519 
"borel = sigma UNIV (range (\<lambda>(a, b). {a ..< b :: real}))" (is "_ = ?SIGMA") 
520 
proof (rule borel_eq_sigmaI5[OF borel_eq_lessThan]) 

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

522 
fix x :: real 

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

524 
by (auto simp: move_uminus real_arch_simple) 

525 
then show "{..< x} \<in> ?SIGMA" 

526 
by (auto intro: sigma_sets.intros) 

40859  527 
qed auto 
528 

47694  529 
lemma borel_measurable_halfspacesI: 
38656  530 
fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space" 
47694  531 
assumes F: "borel = sigma UNIV (range F)" 
532 
and S_eq: "\<And>a i. S a i = f ` F (a,i) \<inter> space M" 

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

38656  534 
shows "f \<in> borel_measurable M = (\<forall>i<DIM('c). \<forall>a::real. S a i \<in> sets M)" 
535 
proof safe 

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

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

47694  538 
by (auto intro!: measurable_sets sigma_sets.Basic simp: assms(1)) 
38656  539 
next 
540 
assume a: "\<forall>i<DIM('c). \<forall>a. S a i \<in> sets M" 

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

542 
proof cases 

543 
assume "i < DIM('c)" 

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

545 
next 

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

47694  547 
from S[OF this] show ?thesis . 
38656  548 
qed } 
47694  549 
then show "f \<in> borel_measurable M" 
550 
by (auto intro!: measurable_measure_of simp: S_eq F) 

38656  551 
qed 
552 

47694  553 
lemma borel_measurable_iff_halfspace_le: 
38656  554 
fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space" 
555 
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  556 
by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_le]) auto 
38656  557 

47694  558 
lemma borel_measurable_iff_halfspace_less: 
38656  559 
fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space" 
560 
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  561 
by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_less]) auto 
38656  562 

47694  563 
lemma borel_measurable_iff_halfspace_ge: 
38656  564 
fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space" 
565 
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  566 
by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_ge]) auto 
38656  567 

47694  568 
lemma borel_measurable_iff_halfspace_greater: 
38656  569 
fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space" 
570 
shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i<DIM('c). \<forall>a. {w \<in> space M. a < f w $$ i} \<in> sets M)" 

47694  571 
by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_greater]) auto 
38656  572 

47694  573 
lemma borel_measurable_iff_le: 
38656  574 
"(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w \<le> a} \<in> sets M)" 
575 
using borel_measurable_iff_halfspace_le[where 'c=real] by simp 

576 

47694  577 
lemma borel_measurable_iff_less: 
38656  578 
"(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w < a} \<in> sets M)" 
579 
using borel_measurable_iff_halfspace_less[where 'c=real] by simp 

580 

47694  581 
lemma borel_measurable_iff_ge: 
38656  582 
"(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a \<le> f w} \<in> sets M)" 
50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

583 
using borel_measurable_iff_halfspace_ge[where 'c=real] 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

584 
by simp 
38656  585 

47694  586 
lemma borel_measurable_iff_greater: 
38656  587 
"(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a < f w} \<in> sets M)" 
588 
using borel_measurable_iff_halfspace_greater[where 'c=real] by simp 

589 

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

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

592 
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

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

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

595 
then show "(\<lambda>x. f x $$ i) \<in> borel_measurable M" 
41025  596 
by (auto intro: borel_measurable_euclidean_component) 
39087
96984bf6fa5b
Measurable on euclidean space is equiv. to measurable components
hoelzl
parents:
39083
diff
changeset

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

598 
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

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

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

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

602 

38656  603 
subsection "Borel measurable operators" 
604 

49774  605 
lemma borel_measurable_continuous_on: 
606 
fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space" 

607 
assumes f: "continuous_on UNIV f" and g: "g \<in> borel_measurable M" 

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

609 
using measurable_comp[OF g borel_measurable_continuous_on1[OF f]] by (simp add: comp_def) 

610 

611 
lemma borel_measurable_continuous_on_open': 

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

613 
assumes cont: "continuous_on A f" "open A" 

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

615 
proof (rule borel_measurableI) 

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

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

618 
by (intro continuous_open_preimage[OF cont]) auto 

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

620 
have "?f ` S \<inter> space borel = 

621 
{x\<in>A. f x \<in> S} \<union> (if c \<in> S then space borel  A else {})" 

622 
by (auto split: split_if_asm) 

623 
also have "\<dots> \<in> sets borel" 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

624 
using * `open A` by auto 
49774  625 
finally show "?f ` S \<inter> space borel \<in> sets borel" . 
626 
qed 

627 

628 
lemma borel_measurable_continuous_on_open: 

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

630 
assumes cont: "continuous_on A f" "open A" 

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

632 
shows "(\<lambda>x. if g x \<in> A then f (g x) else c) \<in> borel_measurable M" 

633 
using measurable_comp[OF g borel_measurable_continuous_on_open'[OF cont], of c] 

634 
by (simp add: comp_def) 

635 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

636 
lemma borel_measurable_uminus[simp, intro, measurable (raw)]: 
49774  637 
fixes g :: "'a \<Rightarrow> real" 
638 
assumes g: "g \<in> borel_measurable M" 

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

640 
by (rule borel_measurable_continuous_on[OF _ g]) (auto intro: continuous_on_minus continuous_on_id) 

641 

642 
lemma euclidean_component_prod: 

643 
fixes x :: "'a :: euclidean_space \<times> 'b :: euclidean_space" 

644 
shows "x $$ i = (if i < DIM('a) then fst x $$ i else snd x $$ (i  DIM('a)))" 

645 
unfolding euclidean_component_def basis_prod_def inner_prod_def by auto 

646 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

647 
lemma borel_measurable_Pair[simp, intro, measurable (raw)]: 
49774  648 
fixes f :: "'a \<Rightarrow> 'b::ordered_euclidean_space" and g :: "'a \<Rightarrow> 'c::ordered_euclidean_space" 
649 
assumes f: "f \<in> borel_measurable M" 

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

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

652 
proof (intro borel_measurable_iff_halfspace_le[THEN iffD2] allI impI) 

653 
fix i and a :: real assume i: "i < DIM('b \<times> 'c)" 

654 
have [simp]: "\<And>P A B C. {w. (P \<longrightarrow> A w \<and> B w) \<and> (\<not> P \<longrightarrow> A w \<and> C w)} = 

655 
{w. A w \<and> (P \<longrightarrow> B w) \<and> (\<not> P \<longrightarrow> C w)}" by auto 

656 
from i f g show "{w \<in> space M. (f w, g w) $$ i \<le> a} \<in> sets M" 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

657 
by (auto simp: euclidean_component_prod) 
49774  658 
qed 
659 

660 
lemma continuous_on_fst: "continuous_on UNIV fst" 

661 
proof  

662 
have [simp]: "range fst = UNIV" by (auto simp: image_iff) 

663 
show ?thesis 

664 
using closed_vimage_fst 

665 
by (auto simp: continuous_on_closed closed_closedin vimage_def) 

666 
qed 

667 

668 
lemma continuous_on_snd: "continuous_on UNIV snd" 

669 
proof  

670 
have [simp]: "range snd = UNIV" by (auto simp: image_iff) 

671 
show ?thesis 

672 
using closed_vimage_snd 

673 
by (auto simp: continuous_on_closed closed_closedin vimage_def) 

674 
qed 

675 

676 
lemma borel_measurable_continuous_Pair: 

677 
fixes f :: "'a \<Rightarrow> 'b::ordered_euclidean_space" and g :: "'a \<Rightarrow> 'c::ordered_euclidean_space" 

678 
assumes [simp]: "f \<in> borel_measurable M" 

679 
assumes [simp]: "g \<in> borel_measurable M" 

680 
assumes H: "continuous_on UNIV (\<lambda>x. H (fst x) (snd x))" 

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

682 
proof  

683 
have eq: "(\<lambda>x. H (f x) (g x)) = (\<lambda>x. (\<lambda>x. H (fst x) (snd x)) (f x, g x))" by auto 

684 
show ?thesis 

685 
unfolding eq by (rule borel_measurable_continuous_on[OF H]) auto 

686 
qed 

687 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

688 
lemma borel_measurable_add[simp, intro, measurable (raw)]: 
49774  689 
fixes f g :: "'a \<Rightarrow> 'c::ordered_euclidean_space" 
690 
assumes f: "f \<in> borel_measurable M" 

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

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

693 
using f g 

694 
by (rule borel_measurable_continuous_Pair) 

695 
(auto intro: continuous_on_fst continuous_on_snd continuous_on_add) 

696 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

697 
lemma borel_measurable_setsum[simp, intro, measurable (raw)]: 
49774  698 
fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real" 
699 
assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M" 

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

701 
proof cases 

702 
assume "finite S" 

703 
thus ?thesis using assms by induct auto 

704 
qed simp 

705 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

706 
lemma borel_measurable_diff[simp, intro, measurable (raw)]: 
49774  707 
fixes f :: "'a \<Rightarrow> real" 
708 
assumes f: "f \<in> borel_measurable M" 

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

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

711 
unfolding diff_minus using assms by fast 

712 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

713 
lemma borel_measurable_times[simp, intro, measurable (raw)]: 
49774  714 
fixes f :: "'a \<Rightarrow> real" 
715 
assumes f: "f \<in> borel_measurable M" 

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

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

718 
using f g 

719 
by (rule borel_measurable_continuous_Pair) 

720 
(auto intro: continuous_on_fst continuous_on_snd continuous_on_mult) 

721 

722 
lemma continuous_on_dist: 

723 
fixes f :: "'a :: t2_space \<Rightarrow> 'b :: metric_space" 

724 
shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. dist (f x) (g x))" 

725 
unfolding continuous_on_eq_continuous_within by (auto simp: continuous_dist) 

726 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

727 
lemma borel_measurable_dist[simp, intro, measurable (raw)]: 
49774  728 
fixes g f :: "'a \<Rightarrow> 'b::ordered_euclidean_space" 
729 
assumes f: "f \<in> borel_measurable M" 

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

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

732 
using f g 

733 
by (rule borel_measurable_continuous_Pair) 

734 
(intro continuous_on_dist continuous_on_fst continuous_on_snd) 

735 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

736 
lemma borel_measurable_scaleR[measurable (raw)]: 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

737 
fixes g :: "'a \<Rightarrow> 'b::ordered_euclidean_space" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

738 
assumes f: "f \<in> borel_measurable M" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

739 
assumes g: "g \<in> borel_measurable M" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

740 
shows "(\<lambda>x. f x *\<^sub>R g x) \<in> borel_measurable M" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

741 
by (rule borel_measurable_continuous_Pair[OF f g]) 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

742 
(auto intro!: continuous_on_scaleR continuous_on_fst continuous_on_snd) 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

743 

47694  744 
lemma affine_borel_measurable_vector: 
38656  745 
fixes f :: "'a \<Rightarrow> 'x::real_normed_vector" 
746 
assumes "f \<in> borel_measurable M" 

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

748 
proof (rule borel_measurableI) 

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

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

751 
proof cases 

752 
assume "b \<noteq> 0" 

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

753 
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

754 
by (auto intro!: open_affinity simp: scaleR_add_right) 
47694  755 
hence "?S \<in> sets borel" by auto 
38656  756 
moreover 
757 
from `b \<noteq> 0` have "(\<lambda>x. a + b *\<^sub>R f x) ` S = f ` ?S" 

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

40859  759 
ultimately show ?thesis using assms unfolding in_borel_measurable_borel 
38656  760 
by auto 
761 
qed simp 

762 
qed 

763 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

764 
lemma borel_measurable_const_scaleR[measurable (raw)]: 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

765 
"f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. b *\<^sub>R f x ::'a::real_normed_vector) \<in> borel_measurable M" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

766 
using affine_borel_measurable_vector[of f M 0 b] by simp 
38656  767 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

768 
lemma borel_measurable_const_add[measurable (raw)]: 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

769 
"f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. a + f x ::'a::real_normed_vector) \<in> borel_measurable M" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

770 
using affine_borel_measurable_vector[of f M a 1] by simp 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

771 

ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

772 
lemma borel_measurable_setprod[simp, intro, measurable (raw)]: 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41025
diff
changeset

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

774 
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

775 
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

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

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

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

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

780 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

781 
lemma borel_measurable_inverse[simp, intro, measurable (raw)]: 
38656  782 
fixes f :: "'a \<Rightarrow> real" 
49774  783 
assumes f: "f \<in> borel_measurable M" 
35692  784 
shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M" 
49774  785 
proof  
786 
have *: "\<And>x::real. inverse x = (if x \<in> UNIV  {0} then inverse x else 0)" by auto 

787 
show ?thesis 

788 
apply (subst *) 

789 
apply (rule borel_measurable_continuous_on_open) 

790 
apply (auto intro!: f continuous_on_inverse continuous_on_id) 

791 
done 

35692  792 
qed 
793 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

794 
lemma borel_measurable_divide[simp, intro, measurable (raw)]: 
38656  795 
fixes f :: "'a \<Rightarrow> real" 
35692  796 
assumes "f \<in> borel_measurable M" 
797 
and "g \<in> borel_measurable M" 

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

799 
unfolding field_divide_inverse 

38656  800 
by (rule borel_measurable_inverse borel_measurable_times assms)+ 
801 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

802 
lemma borel_measurable_max[intro, simp, measurable (raw)]: 
38656  803 
fixes f g :: "'a \<Rightarrow> real" 
804 
assumes "f \<in> borel_measurable M" 

805 
assumes "g \<in> borel_measurable M" 

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

49774  807 
unfolding max_def by (auto intro!: assms measurable_If) 
38656  808 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

809 
lemma borel_measurable_min[intro, simp, measurable (raw)]: 
38656  810 
fixes f g :: "'a \<Rightarrow> real" 
811 
assumes "f \<in> borel_measurable M" 

812 
assumes "g \<in> borel_measurable M" 

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

49774  814 
unfolding min_def by (auto intro!: assms measurable_If) 
38656  815 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

816 
lemma borel_measurable_abs[simp, intro, measurable (raw)]: 
38656  817 
assumes "f \<in> borel_measurable M" 
818 
shows "(\<lambda>x. \<bar>f x :: real\<bar>) \<in> borel_measurable M" 

819 
proof  

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

821 
show ?thesis unfolding * using assms by auto 

822 
qed 

823 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

824 
lemma borel_measurable_nth[simp, intro, measurable (raw)]: 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41025
diff
changeset

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

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

828 

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

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

831 
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

832 
assumes q: "convex_on { a <..< b} q" 
49774  833 
shows "(\<lambda>x. q (X x)) \<in> borel_measurable M" 
42990
3706951a6421
composition of convex and measurable function is measurable
hoelzl
parents:
42950
diff
changeset

834 
proof  
49774  835 
have "(\<lambda>x. if X x \<in> {a <..< b} then q (X x) else 0) \<in> borel_measurable M" (is "?qX") 
836 
proof (rule borel_measurable_continuous_on_open[OF _ _ X(1)]) 

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

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

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

839 
by (rule convex_on_continuous) 
41830  840 
qed 
50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

841 
also have "?qX \<longleftrightarrow> (\<lambda>x. q (X x)) \<in> borel_measurable M" 
42990
3706951a6421
composition of convex and measurable function is measurable
hoelzl
parents:
42950
diff
changeset

842 
using X by (intro measurable_cong) auto 
50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

843 
finally show ?thesis . 
41830  844 
qed 
845 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

846 
lemma borel_measurable_ln[simp, intro, measurable (raw)]: 
49774  847 
assumes f: "f \<in> borel_measurable M" 
848 
shows "(\<lambda>x. ln (f x)) \<in> borel_measurable M" 

41830  849 
proof  
850 
{ fix x :: real assume x: "x \<le> 0" 

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

49774  852 
from this[of x] x this[of 0] have "ln 0 = ln x" 
853 
by (auto simp: ln_def) } 

854 
note ln_imp = this 

855 
have "(\<lambda>x. if f x \<in> {0<..} then ln (f x) else ln 0) \<in> borel_measurable M" 

856 
proof (rule borel_measurable_continuous_on_open[OF _ _ f]) 

857 
show "continuous_on {0<..} ln" 

858 
by (auto intro!: continuous_at_imp_continuous_on DERIV_ln DERIV_isCont 

41830  859 
simp: continuous_isCont[symmetric]) 
860 
show "open ({0<..}::real set)" by auto 

861 
qed 

49774  862 
also have "(\<lambda>x. if x \<in> {0<..} then ln x else ln 0) = ln" 
863 
by (simp add: fun_eq_iff not_less ln_imp) 

41830  864 
finally show ?thesis . 
865 
qed 

866 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

867 
lemma borel_measurable_log[simp, intro, measurable (raw)]: 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

868 
"f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. log (g x) (f x)) \<in> borel_measurable M" 
49774  869 
unfolding log_def by auto 
41830  870 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

871 
lemma measurable_count_space_eq2_countable: 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

872 
fixes f :: "'a => 'c::countable" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

873 
shows "f \<in> measurable M (count_space A) \<longleftrightarrow> (f \<in> space M \<rightarrow> A \<and> (\<forall>a\<in>A. f ` {a} \<inter> space M \<in> sets M))" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

874 
proof  
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

875 
{ fix X assume "X \<subseteq> A" "f \<in> space M \<rightarrow> A" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

876 
then have "f ` X \<inter> space M = (\<Union>a\<in>X. f ` {a} \<inter> space M)" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

877 
by auto 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

878 
moreover assume "\<And>a. a\<in>A \<Longrightarrow> f ` {a} \<inter> space M \<in> sets M" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

879 
ultimately have "f ` X \<inter> space M \<in> sets M" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

880 
using `X \<subseteq> A` by (simp add: subset_eq del: UN_simps) } 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

881 
then show ?thesis 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

882 
unfolding measurable_def by auto 
47761  883 
qed 
884 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

885 
lemma measurable_real_floor[measurable]: 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

886 
"(floor :: real \<Rightarrow> int) \<in> measurable borel (count_space UNIV)" 
47761  887 
proof  
50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

888 
have "\<And>a x. \<lfloor>x\<rfloor> = a \<longleftrightarrow> (real a \<le> x \<and> x < real (a + 1))" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

889 
by (auto intro: floor_eq2) 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

890 
then show ?thesis 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

891 
by (auto simp: vimage_def measurable_count_space_eq2_countable) 
47761  892 
qed 
893 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

894 
lemma measurable_real_natfloor[measurable]: 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

895 
"(natfloor :: real \<Rightarrow> nat) \<in> measurable borel (count_space UNIV)" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

896 
by (simp add: natfloor_def[abs_def]) 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

897 

ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

898 
lemma measurable_real_ceiling[measurable]: 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

899 
"(ceiling :: real \<Rightarrow> int) \<in> measurable borel (count_space UNIV)" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

900 
unfolding ceiling_def[abs_def] by simp 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

901 

ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

902 
lemma borel_measurable_real_floor: "(\<lambda>x::real. real \<lfloor>x\<rfloor>) \<in> borel_measurable borel" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

903 
by simp 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

904 

ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

905 
lemma borel_measurable_real_natfloor[intro, simp]: 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

906 
"f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. real (natfloor (f x))) \<in> borel_measurable M" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

907 
by simp 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

908 

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

909 
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

910 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

911 
lemma borel_measurable_ereal[simp, intro, measurable (raw)]: 
43920  912 
assumes f: "f \<in> borel_measurable M" shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M" 
49774  913 
using continuous_on_ereal f by (rule borel_measurable_continuous_on) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

914 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

915 
lemma borel_measurable_real_of_ereal[simp, intro, measurable (raw)]: 
49774  916 
fixes f :: "'a \<Rightarrow> ereal" 
917 
assumes f: "f \<in> borel_measurable M" 

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

919 
proof  

920 
have "(\<lambda>x. if f x \<in> UNIV  { \<infinity>,  \<infinity> } then real (f x) else 0) \<in> borel_measurable M" 

921 
using continuous_on_real 

922 
by (rule borel_measurable_continuous_on_open[OF _ _ f]) auto 

923 
also have "(\<lambda>x. if f x \<in> UNIV  { \<infinity>,  \<infinity> } then real (f x) else 0) = (\<lambda>x. real (f x))" 

924 
by auto 

925 
finally show ?thesis . 

926 
qed 

927 

928 
lemma borel_measurable_ereal_cases: 

929 
fixes f :: "'a \<Rightarrow> ereal" 

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

931 
assumes H: "(\<lambda>x. H (ereal (real (f x)))) \<in> borel_measurable M" 

932 
shows "(\<lambda>x. H (f x)) \<in> borel_measurable M" 

933 
proof  

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

934 
let ?F = "\<lambda>x. if f x = \<infinity> then H \<infinity> else if f x =  \<infinity> then H (\<infinity>) else H (ereal (real (f x)))" 
49774  935 
{ fix x have "H (f x) = ?F x" by (cases "f x") auto } 
50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

936 
with f H show ?thesis by simp 
47694  937 
qed 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

938 

49774  939 
lemma 
940 
fixes f :: "'a \<Rightarrow> ereal" assumes f[simp]: "f \<in> borel_measurable M" 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

941 
shows borel_measurable_ereal_abs[intro, simp, measurable(raw)]: "(\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

942 
and borel_measurable_ereal_inverse[simp, intro, measurable(raw)]: "(\<lambda>x. inverse (f x) :: ereal) \<in> borel_measurable M" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

943 
and borel_measurable_uminus_ereal[intro, measurable(raw)]: "(\<lambda>x.  f x :: ereal) \<in> borel_measurable M" 
49774  944 
by (auto simp del: abs_real_of_ereal simp: borel_measurable_ereal_cases[OF f] measurable_If) 
945 

946 
lemma borel_measurable_uminus_eq_ereal[simp]: 

947 
"(\<lambda>x.  f x :: ereal) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M" (is "?l = ?r") 

948 
proof 

949 
assume ?l from borel_measurable_uminus_ereal[OF this] show ?r by simp 

950 
qed auto 

951 

952 
lemma set_Collect_ereal2: 

953 
fixes f g :: "'a \<Rightarrow> ereal" 

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

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

956 
assumes H: "{x \<in> space M. H (ereal (real (f x))) (ereal (real (g x)))} \<in> sets M" 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

957 
"{x \<in> space borel. H (\<infinity>) (ereal x)} \<in> sets borel" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

958 
"{x \<in> space borel. H (\<infinity>) (ereal x)} \<in> sets borel" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

959 
"{x \<in> space borel. H (ereal x) (\<infinity>)} \<in> sets borel" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

960 
"{x \<in> space borel. H (ereal x) (\<infinity>)} \<in> sets borel" 
49774  961 
shows "{x \<in> space M. H (f x) (g x)} \<in> sets M" 
962 
proof  

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

963 
let ?G = "\<lambda>y x. if g x = \<infinity> then H y \<infinity> else if g x = \<infinity> then H y (\<infinity>) else H y (ereal (real (g x)))" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

964 
let ?F = "\<lambda>x. if f x = \<infinity> then ?G \<infinity> x else if f x = \<infinity> then ?G (\<infinity>) x else ?G (ereal (real (f x))) x" 
49774  965 
{ fix x have "H (f x) (g x) = ?F x" by (cases "f x" "g x" rule: ereal2_cases) auto } 
50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

966 
note * = this 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

967 
from assms show ?thesis 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

968 
by (subst *) (simp del: space_borel split del: split_if) 
49774  969 
qed 
970 

971 
lemma 

972 
fixes f g :: "'a \<Rightarrow> ereal" 

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

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

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

975 
shows borel_measurable_ereal_le[intro,simp,measurable(raw)]: "{x \<in> space M. f x \<le> g x} \<in> sets M" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

976 
and borel_measurable_ereal_less[intro,simp,measurable(raw)]: "{x \<in> space M. f x < g x} \<in> sets M" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

977 
and borel_measurable_ereal_eq[intro,simp,measurable(raw)]: "{w \<in> space M. f w = g w} \<in> sets M" 
49774  978 
and borel_measurable_ereal_neq[intro,simp]: "{w \<in> space M. f w \<noteq> g w} \<in> sets M" 
979 
using f g by (auto simp: f g set_Collect_ereal2[OF f g] intro!: sets_Collect_neg) 

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

980 

47694  981 
lemma borel_measurable_ereal_iff: 
43920  982 
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

983 
proof 
43920  984 
assume "(\<lambda>x. ereal (f x)) \<in> borel_measurable M" 
985 
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

986 
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

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

988 

47694  989 
lemma borel_measurable_ereal_iff_real: 
43923  990 
fixes f :: "'a \<Rightarrow> ereal" 
991 
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

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

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

994 
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

995 
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

996 
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 
46731  997 
let ?f = "\<lambda>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

998 
have "?f \<in> borel_measurable M" using * ** by (intro measurable_If) auto 
43920  999 
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

1000 
finally show "f \<in> borel_measurable M" . 
50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1001 
qed simp_all 
41830  1002 

47694  1003 
lemma borel_measurable_eq_atMost_ereal: 
43923  1004 
fixes f :: "'a \<Rightarrow> ereal" 
1005 
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

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

1007 
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

1008 
show "f \<in> borel_measurable M" 
43920  1009 
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

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

1011 
fix a :: real 
43920  1012 
{ 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

1013 
have "x = \<infinity>" 
43920  1014 
proof (rule ereal_top) 
44666  1015 
fix B from reals_Archimedean2[of B] guess n .. 
43920  1016 
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

1017 
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

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

1019 
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

1020 
by (auto simp: not_le) 
50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1021 
then show "f ` {\<infinity>} \<inter> space M \<in> sets M" using pos 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

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

1023 
moreover 
43923  1024 
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

1025 
then show "f ` {\<infinity>} \<inter> space M \<in> sets M" using pos by auto 
43920  1026 
moreover have "{x\<in>space M. f x \<le> ereal a} \<in> sets M" 
1027 
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

1028 
moreover have "{w \<in> space M. real (f w) \<le> a} = 
43920  1029 
(if a < 0 then {w \<in> space M. f w \<le> ereal a}  f ` {\<infinity>} \<inter> space M 
1030 
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

1031 
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

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

1034 
qed (simp add: measurable_sets) 
35582  1035 

47694  1036 
lemma borel_measurable_eq_atLeast_ereal: 
43920  1037 
"(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

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

1039 
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

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

1042 
ultimately have "(\<lambda>x.  f x) \<in> borel_measurable M" 
43920  1043 
unfolding borel_measurable_eq_atMost_ereal by auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

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

1045 
qed (simp add: measurable_sets) 
35582  1046 

49774  1047 
lemma greater_eq_le_measurable: 
1048 
fixes f :: "'a \<Rightarrow> 'c::linorder" 

1049 
shows "f ` {..< a} \<inter> space M \<in> sets M \<longleftrightarrow> f ` {a ..} \<inter> space M \<in> sets M" 

1050 
proof 

1051 
assume "f ` {a ..} \<inter> space M \<in> sets M" 

1052 
moreover have "f ` {..< a} \<inter> space M = space M  f ` {a ..} \<inter> space M" by auto 

1053 
ultimately show "f ` {..< a} \<inter> space M \<in> sets M" by auto 

1054 
next 

1055 
assume "f ` {..< a} \<inter> space M \<in> sets M" 

1056 
moreover have "f ` {a ..} \<inter> space M = space M  f ` {..< a} \<inter> space M" by auto 

1057 
ultimately show "f ` {a ..} \<inter> space M \<in> sets M" by auto 

1058 
qed 

1059 

47694  1060 
lemma borel_measurable_ereal_iff_less: 
43920  1061 
"(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f ` {..< a} \<inter> space M \<in> sets M)" 
1062 
unfolding borel_measurable_eq_atLeast_ereal greater_eq_le_measurable .. 

38656  1063 

49774  1064 
lemma less_eq_ge_measurable: 
1065 
fixes f :: "'a \<Rightarrow> 'c::linorder" 

1066 
shows "f ` {a <..} \<inter> space M \<in> sets M \<longleftrightarrow> f ` {..a} \<inter> space M \<in> sets M" 

1067 
proof 

1068 
assume "f ` {a <..} \<inter> space M \<in> sets M" 

1069 
moreover have "f ` {..a} \<inter> space M = space M  f ` {a <..} \<inter> space M" by auto 

1070 
ultimately show "f ` {..a} \<inter> space M \<in> sets M" by auto 

1071 
next 

1072 
assume "f ` {..a} \<inter> space M \<in> sets M" 

1073 
moreover have "f ` {a <..} \<inter> space M = space M  f ` {..a} \<inter> space M" by auto 

1074 
ultimately show "f ` {a <..} \<inter> space M \<in> sets M" by auto 

1075 
qed 

1076 

47694  1077 
lemma borel_measurable_ereal_iff_ge: 
43920  1078 
"(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f ` {a <..} \<inter> space M \<in> sets M)" 
1079 
unfolding borel_measurable_eq_atMost_ereal less_eq_ge_measurable .. 

38656  1080 

49774  1081 
lemma borel_measurable_ereal2: 
1082 
fixes f g :: "'a \<Rightarrow> ereal" 

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

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

1084 
assumes g: "g \<in> borel_measurable M" 
49774  1085 
assumes H: "(\<lambda>x. H (ereal (real (f x))) (ereal (real (g x)))) \<in> borel_measurable M" 
1086 
"(\<lambda>x. H (\<infinity>) (ereal (real (g x)))) \<in> borel_measurable M" 

1087 
"(\<lambda>x. H (\<infinity>) (ereal (real (g x)))) \<in> borel_measurable M" 

1088 
"(\<lambda>x. H (ereal (real (f x))) (\<infinity>)) \<in> borel_measurable M" 

1089 
"(\<lambda>x. H (ereal (real (f x))) (\<infinity>)) \<in> borel_measurable M" 

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

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

1091 
proof  
50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1092 
let ?G = "\<lambda>y x. if g x = \<infinity> then H y \<infinity> else if g x =  \<infinity> then H y (\<infinity>) else H y (ereal (real (g x)))" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1093 
let ?F = "\<lambda>x. if f x = \<infinity> then ?G \<infinity> x else if f x =  \<infinity> then ?G (\<infinity>) x else ?G (ereal (real (f x))) x" 
49774  1094 
{ fix x have "H (f x) (g x) = ?F x" by (cases "f x" "g x" rule: ereal2_cases) auto } 
50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1095 
note * = this 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1096 
from assms show ?thesis unfolding * by simp 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

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

1098 

49774  1099 
lemma 
1100 
fixes f :: "'a \<Rightarrow> ereal" assumes f: "f \<in> borel_measurable M" 

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

1102 
and borel_measurable_ereal_neq_const: "{x\<in>space M. f x \<noteq> c} \<in> sets M" 

1103 
using f by auto 

38656  1104 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1105 
lemma [intro, simp, measurable(raw)]: 
43920  1106 
fixes f :: "'a \<Rightarrow> ereal" 
49774  1107 
assumes [simp]: "f \<in> borel_measurable M" "g \<in> borel_measurable M" 
50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1108 
shows borel_measurable_ereal_add: "(\<lambda>x. f x + g x) \<in> borel_measurable M" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1109 
and borel_measurable_ereal_times: "(\<lambda>x. f x * g x) \<in> borel_measurable M" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1110 
and borel_measurable_ereal_min: "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1111 
and borel_measurable_ereal_max: "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M" 
49774  1112 
by (auto simp add: borel_measurable_ereal2 measurable_If min_def max_def) 
1113 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1114 
lemma [simp, intro, measurable(raw)]: 
49774  1115 
fixes f g :: "'a \<Rightarrow> ereal" 
1116 
assumes "f \<in> borel_measurable M" 

1117 
assumes "g \<in> borel_measurable M" 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1118 
shows borel_measurable_ereal_diff: "(\<lambda>x. f x  g x) \<in> borel_measurable M" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1119 
and borel_measurable_ereal_divide: "(\<lambda>x. f x / g x) \<in> borel_measurable M" 
49774  1120 
unfolding minus_ereal_def divide_ereal_def using assms by auto 
38656  1121 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1122 
lemma borel_measurable_ereal_setsum[simp, intro,measurable (raw)]: 
43920  1123 
fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal" 
41096  1124 
assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M" 
1125 
shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M" 

1126 
proof cases 

1127 
assume "finite S" 

1128 
thus ?thesis using assms 

1129 
by induct auto 

49774  1130 
qed simp 
38656  1131 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1132 
lemma borel_measurable_ereal_setprod[simp, intro,measurable (raw)]: 
43920  1133 
fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal" 
38656  1134 
assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M" 
41096  1135 
shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M" 
38656  1136 
proof cases 
1137 
assume "finite S" 

41096  1138 
thus ?thesis using assms by induct auto 
1139 
qed simp 

38656  1140 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1141 
lemma borel_measurable_SUP[simp, intro,measurable (raw)]: 
43920  1142 
fixes f :: "'d\<Colon>countable \<Rightarrow> 'a \<Rightarrow> ereal" 
38656  1143 
assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M" 
41097
a1abfa4e2b44
use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
hoelzl
parents:
41096
diff
changeset

1144 
shows "(\<lambda>x. SUP i : A. f i x) \<in> borel_measurable M" (is "?sup \<in> borel_measurable M") 
43920  1145 
unfolding borel_measurable_ereal_iff_ge 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1146 
proof 
38656  1147 
fix a 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1148 
have "?sup ` {a<..} \<inter> space M = (\<Union>i\<in>A. {x\<in>space M. a < f i x})" 
46884  1149 
by (auto simp: less_SUP_iff) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1150 
then show "?sup ` {a<..} \<inter> space M \<in> sets M" 
38656  1151 
using assms by auto 
1152 
qed 

1153 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1154 
lemma borel_measurable_INF[simp, intro,measurable (raw)]: 
43920  1155 
fixes f :: "'d :: countable \<Rightarrow> 'a \<Rightarrow> ereal" 
38656  1156 
assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M" 
41097
a1abfa4e2b44
use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
hoelzl
parents:
41096
diff
changeset

1157 
shows "(\<lambda>x. INF i : A. f i x) \<in> borel_measurable M" (is "?inf \<in> borel_measurable M") 
43920  1158 
unfolding borel_measurable_ereal_iff_less 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1159 
proof 
38656  1160 
fix a 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1161 
have "?inf ` {..<a} \<inter> space M = (\<Union>i\<in>A. {x\<in>space M. f i x < a})" 
46884  1162 
by (auto simp: INF_less_iff) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1163 
then show "?inf ` {..<a} \<inter> space M \<in> sets M" 
38656  1164 
using assms by auto 
1165 
qed 

1166 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1167 
lemma [simp, intro, measurable (raw)]: 
43920  1168 
fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1169 
assumes "\<And>i. f i \<in> borel_measurable M" 
50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1170 
shows borel_measurable_liminf: "(\<lambda>x. liminf (\<lambda>i. f i x)) \<in> borel_measurable M" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1171 
and borel_measurable_limsup: "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M" 
49774  1172 
unfolding liminf_SUPR_INFI limsup_INFI_SUPR using assms by auto 
35692  1173 

49774  1174 
lemma borel_measurable_ereal_LIMSEQ: 
1175 
fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ereal" 

1176 
assumes u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) > u' x" 

1177 
and u: "\<And>i. u i \<in> borel_measurable M" 

1178 
shows "u' \<in> borel_measurable M" 

47694  1179 
proof  
49774  1180 
have "\<And>x. x \<in> space M \<Longrightarrow> u' x = liminf (\<lambda>n. u n x)" 
1181 
using u' by (simp add: lim_imp_Liminf[symmetric]) 

1182 
then show ?thesis by (simp add: u cong: measurable_cong) 

47694  1183 
qed 
1184 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1185 
lemma borel_measurable_psuminf[simp, intro, measurable (raw)]: 
43920  1186 
fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1187 
assumes "\<And>i. f i \<in> borel_measurable M" and pos: "\<And>i x. x \<in> space M \<Longrightarrow> 0 \<le> f i x" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

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

1189 
apply (subst measurable_cong) 
43920  1190 
apply (subst suminf_ereal_eq_SUPR) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1191 
apply (rule pos) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1192 
using assms by auto 
39092  1193 

1194 
section "LIMSEQ is borel measurable" 

1195 

47694  1196 
lemma borel_measurable_LIMSEQ: 
39092  1197 
fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> real" 
1198 
assumes u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) > u' x" 

1199 
and u: "\<And>i. u i \<in> borel_measurable M" 

1200 
shows "u' \<in> borel_measurable M" 

1201 
proof  

43920  1202 
have "\<And>x. x \<in> space M \<Longrightarrow> liminf (\<lambda>n. ereal (u n x)) = ereal (u' x)" 
46731  1203 
using u' by (simp add: lim_imp_Liminf) 
43920  1204 
moreover from u have "(\<lambda>x. liminf (\<lambda>n. ereal (u n x))) \<in> borel_measurable M" 
39092  1205 
by auto 
43920  1206 
ultimately show ?thesis by (simp cong: measurable_cong add: borel_measurable_ereal_iff) 
39092  1207 
qed 
1208 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1209 
lemma sets_Collect_Cauchy[measurable]: 
49774  1210 
fixes f :: "nat \<Rightarrow> 'a => real" 
50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1211 
assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M" 
49774  1212 
shows "{x\<in>space M. Cauchy (\<lambda>i. f i x)} \<in> sets M" 
50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1213 
unfolding Cauchy_iff2 using f by auto 
49774  1214 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1215 
lemma borel_measurable_lim[measurable (raw)]: 
49774  1216 
fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> real" 
50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1217 
assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M" 
49774  1218 
shows "(\<lambda>x. lim (\<lambda>i. f i x)) \<in> borel_measurable M" 
1219 
proof  

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1220 
def u' \<equiv> "\<lambda>x. lim (\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0)" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1221 
then have *: "\<And>x. lim (\<lambda>i. f i x) = (if Cauchy (\<lambda>i. f i x) then u' x else (THE x. False))" 
< 