author  hoelzl 
Mon, 19 May 2014 12:04:45 +0200  
changeset 56993  e5366291d6aa 
parent 56371  fb9ae0727548 
child 56994  8d5e5ec1cac3 
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 
50387  9 
imports 
10 
Measurable 

11 
"~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis" 

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

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

13 

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

15 

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

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

18 

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

20 

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

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

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

25 

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

31 

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

38656  34 

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

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

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

37 

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

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

40 

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

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

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

47 

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

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

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

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

55 

50003  56 
lemma borel_singleton[measurable]: 
57 
"A \<in> sets borel \<Longrightarrow> insert x A \<in> sets (borel :: 'a::t1_space measure)" 

50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50104
diff
changeset

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

59 

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

61 
unfolding Compl_eq_Diff_UNIV by simp 
41830  62 

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

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

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

68 

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

72 
shows "f \<in> borel_measurable M" 

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

75 
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

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

78 

50021
d96a3f468203
add support for function application to measurability prover
hoelzl
parents:
50003
diff
changeset

79 
lemma borel_measurable_const: 
38656  80 
"(\<lambda>x. c) \<in> borel_measurable M" 
47694  81 
by auto 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

82 

50003  83 
lemma borel_measurable_indicator: 
38656  84 
assumes A: "A \<in> sets M" 
85 
shows "indicator A \<in> borel_measurable M" 

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

88 

50096  89 
lemma borel_measurable_count_space[measurable (raw)]: 
90 
"f \<in> borel_measurable (count_space S)" 

91 
unfolding measurable_def by auto 

92 

93 
lemma borel_measurable_indicator'[measurable (raw)]: 

94 
assumes [measurable]: "{x\<in>space M. f x \<in> A x} \<in> sets M" 

95 
shows "(\<lambda>x. indicator (A x) (f x)) \<in> borel_measurable M" 

50001
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49774
diff
changeset

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

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

98 

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

102 
proof 

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

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

105 
unfolding measurable_def by auto 

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

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

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

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

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

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

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

115 
qed 

116 

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

121 

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

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

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

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

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

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

127 
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

128 

50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

129 
lemma borel_eq_countable_basis: 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

130 
fixes B::"'a::topological_space set set" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

131 
assumes "countable B" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

132 
assumes "topological_basis B" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

133 
shows "borel = sigma UNIV B" 
50087  134 
unfolding borel_def 
135 
proof (intro sigma_eqI sigma_sets_eqI, safe) 

50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

136 
interpret countable_basis using assms by unfold_locales 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

137 
fix X::"'a set" assume "open X" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

138 
from open_countable_basisE[OF this] guess B' . note B' = this 
51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

139 
then show "X \<in> sigma_sets UNIV B" 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

140 
by (blast intro: sigma_sets_UNION `countable B` countable_subset) 
50087  141 
next 
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

142 
fix b assume "b \<in> B" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

143 
hence "open b" by (rule topological_basis_open[OF assms(2)]) 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

144 
thus "b \<in> sigma_sets UNIV (Collect open)" by auto 
50087  145 
qed simp_all 
146 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

147 
lemma borel_measurable_Pair[measurable (raw)]: 
50881
ae630bab13da
renamed countable_basis_space to second_countable_topology
hoelzl
parents:
50526
diff
changeset

148 
fixes f :: "'a \<Rightarrow> 'b::second_countable_topology" and g :: "'a \<Rightarrow> 'c::second_countable_topology" 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

149 
assumes f[measurable]: "f \<in> borel_measurable M" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

150 
assumes g[measurable]: "g \<in> borel_measurable M" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

151 
shows "(\<lambda>x. (f x, g x)) \<in> borel_measurable M" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

152 
proof (subst borel_eq_countable_basis) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

153 
let ?B = "SOME B::'b set set. countable B \<and> topological_basis B" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

154 
let ?C = "SOME B::'c set set. countable B \<and> topological_basis B" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

155 
let ?P = "(\<lambda>(b, c). b \<times> c) ` (?B \<times> ?C)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

156 
show "countable ?P" "topological_basis ?P" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

157 
by (auto intro!: countable_basis topological_basis_prod is_basis) 
38656  158 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

159 
show "(\<lambda>x. (f x, g x)) \<in> measurable M (sigma UNIV ?P)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

160 
proof (rule measurable_measure_of) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

161 
fix S assume "S \<in> ?P" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

162 
then obtain b c where "b \<in> ?B" "c \<in> ?C" and S: "S = b \<times> c" by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

163 
then have borel: "open b" "open c" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

164 
by (auto intro: is_basis topological_basis_open) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

165 
have "(\<lambda>x. (f x, g x)) ` S \<inter> space M = (f ` b \<inter> space M) \<inter> (g ` c \<inter> space M)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

166 
unfolding S by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

167 
also have "\<dots> \<in> sets M" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

168 
using borel by simp 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

169 
finally show "(\<lambda>x. (f x, g x)) ` S \<inter> space M \<in> sets M" . 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

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

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

172 

49774  173 
lemma borel_measurable_continuous_on: 
174 
fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space" 

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

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

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

178 

179 
lemma borel_measurable_continuous_on_open': 

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

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

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

183 
proof (rule borel_measurableI) 

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

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

186 
by (intro continuous_open_preimage[OF cont]) auto 

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

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

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

190 
by (auto split: split_if_asm) 

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

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

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

195 

196 
lemma borel_measurable_continuous_on_open: 

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

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

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

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

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

202 
by (simp add: comp_def) 

203 

204 
lemma borel_measurable_continuous_Pair: 

50881
ae630bab13da
renamed countable_basis_space to second_countable_topology
hoelzl
parents:
50526
diff
changeset

205 
fixes f :: "'a \<Rightarrow> 'b::second_countable_topology" and g :: "'a \<Rightarrow> 'c::second_countable_topology" 
50003  206 
assumes [measurable]: "f \<in> borel_measurable M" 
207 
assumes [measurable]: "g \<in> borel_measurable M" 

49774  208 
assumes H: "continuous_on UNIV (\<lambda>x. H (fst x) (snd x))" 
209 
shows "(\<lambda>x. H (f x) (g x)) \<in> borel_measurable M" 

210 
proof  

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

212 
show ?thesis 

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

214 
qed 

215 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

216 
section "Borel spaces on euclidean spaces" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

217 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

218 
lemma borel_measurable_inner[measurable (raw)]: 
50881
ae630bab13da
renamed countable_basis_space to second_countable_topology
hoelzl
parents:
50526
diff
changeset

219 
fixes f g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_inner}" 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

220 
assumes "f \<in> borel_measurable M" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

221 
assumes "g \<in> borel_measurable M" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

222 
shows "(\<lambda>x. f x \<bullet> g x) \<in> borel_measurable M" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

223 
using assms 
56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56212
diff
changeset

224 
by (rule borel_measurable_continuous_Pair) (intro continuous_intros) 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

225 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

226 
lemma [measurable]: 
51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

227 
fixes a b :: "'a\<Colon>linorder_topology" 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

228 
shows lessThan_borel: "{..< a} \<in> sets borel" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

229 
and greaterThan_borel: "{a <..} \<in> sets borel" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

230 
and greaterThanLessThan_borel: "{a<..<b} \<in> sets borel" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

231 
and atMost_borel: "{..a} \<in> sets borel" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

232 
and atLeast_borel: "{a..} \<in> sets borel" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

233 
and atLeastAtMost_borel: "{a..b} \<in> sets borel" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

234 
and greaterThanAtMost_borel: "{a<..b} \<in> sets borel" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

235 
and atLeastLessThan_borel: "{a..<b} \<in> sets borel" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

236 
unfolding greaterThanAtMost_def atLeastLessThan_def 
51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

237 
by (blast intro: borel_open borel_closed open_lessThan open_greaterThan open_greaterThanLessThan 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

238 
closed_atMost closed_atLeast closed_atLeastAtMost)+ 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

239 

54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset

240 
notation 
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset

241 
eucl_less (infix "<e" 50) 
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset

242 

2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset

243 
lemma box_oc: "{x. a <e x \<and> x \<le> b} = {x. a <e x} \<inter> {..b}" 
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset

244 
and box_co: "{x. a \<le> x \<and> x <e b} = {a..} \<inter> {x. x <e b}" 
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset

245 
by auto 
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset

246 

51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

247 
lemma eucl_ivals[measurable]: 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

248 
fixes a b :: "'a\<Colon>ordered_euclidean_space" 
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset

249 
shows "{x. x <e a} \<in> sets borel" 
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset

250 
and "{x. a <e x} \<in> sets borel" 
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset

251 
and "box a b \<in> sets borel" 
51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

252 
and "{..a} \<in> sets borel" 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

253 
and "{a..} \<in> sets borel" 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

254 
and "{a..b} \<in> sets borel" 
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset

255 
and "{x. a <e x \<and> x \<le> b} \<in> sets borel" 
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset

256 
and "{x. a \<le> x \<and> x <e b} \<in> sets borel" 
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset

257 
unfolding box_oc box_co 
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset

258 
by (auto intro: borel_open borel_closed) 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

259 

51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

260 
lemma open_Collect_less: 
53216  261 
fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {dense_linorder, linorder_topology}" 
51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

262 
assumes "continuous_on UNIV f" 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

263 
assumes "continuous_on UNIV g" 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

264 
shows "open {x. f x < g x}" 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

265 
proof  
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

266 
have "open (\<Union>y. {x \<in> UNIV. f x \<in> {..< y}} \<inter> {x \<in> UNIV. g x \<in> {y <..}})" (is "open ?X") 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

267 
by (intro open_UN ballI open_Int continuous_open_preimage assms) auto 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

268 
also have "?X = {x. f x < g x}" 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

269 
by (auto intro: dense) 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

270 
finally show ?thesis . 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

271 
qed 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

272 

baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

273 
lemma closed_Collect_le: 
53216  274 
fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {dense_linorder, linorder_topology}" 
51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

275 
assumes f: "continuous_on UNIV f" 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

276 
assumes g: "continuous_on UNIV g" 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

277 
shows "closed {x. f x \<le> g x}" 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

278 
using open_Collect_less[OF g f] unfolding not_less[symmetric] Collect_neg_eq open_closed . 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

279 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

280 
lemma borel_measurable_less[measurable]: 
53216  281 
fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, dense_linorder, linorder_topology}" 
51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

282 
assumes "f \<in> borel_measurable M" 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

283 
assumes "g \<in> borel_measurable M" 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

284 
shows "{w \<in> space M. f w < g w} \<in> sets M" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

285 
proof  
51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

286 
have "{w \<in> space M. f w < g w} = (\<lambda>x. (f x, g x)) ` {x. fst x < snd x} \<inter> space M" 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

287 
by auto 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

288 
also have "\<dots> \<in> sets M" 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

289 
by (intro measurable_sets[OF borel_measurable_Pair borel_open, OF assms open_Collect_less] 
56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56212
diff
changeset

290 
continuous_intros) 
51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

291 
finally show ?thesis . 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

292 
qed 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

293 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

294 
lemma 
53216  295 
fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, dense_linorder, linorder_topology}" 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

296 
assumes f[measurable]: "f \<in> borel_measurable M" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

297 
assumes g[measurable]: "g \<in> borel_measurable M" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

298 
shows borel_measurable_le[measurable]: "{w \<in> space M. f w \<le> g w} \<in> sets M" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

299 
and borel_measurable_eq[measurable]: "{w \<in> space M. f w = g w} \<in> sets M" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

300 
and borel_measurable_neq: "{w \<in> space M. f w \<noteq> g w} \<in> sets M" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

301 
unfolding eq_iff not_less[symmetric] 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

302 
by measurable 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

303 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

304 
lemma 
51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

305 
fixes i :: "'a::{second_countable_topology, real_inner}" 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

306 
shows hafspace_less_borel: "{x. a < x \<bullet> i} \<in> sets borel" 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

307 
and hafspace_greater_borel: "{x. x \<bullet> i < a} \<in> sets borel" 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

308 
and hafspace_less_eq_borel: "{x. a \<le> x \<bullet> i} \<in> sets borel" 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

309 
and hafspace_greater_eq_borel: "{x. x \<bullet> i \<le> a} \<in> sets borel" 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

310 
by simp_all 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

311 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

312 
subsection "Borel space equals sigma algebras over intervals" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

313 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

314 
lemma borel_sigma_sets_subset: 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

315 
"A \<subseteq> sets borel \<Longrightarrow> sigma_sets UNIV A \<subseteq> sets borel" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

316 
using sets.sigma_sets_subset[of A borel] by simp 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

317 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

318 
lemma borel_eq_sigmaI1: 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

319 
fixes F :: "'i \<Rightarrow> 'a::topological_space set" and X :: "'a::topological_space set set" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

320 
assumes borel_eq: "borel = sigma UNIV X" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

321 
assumes X: "\<And>x. x \<in> X \<Longrightarrow> x \<in> sets (sigma UNIV (F ` A))" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

322 
assumes F: "\<And>i. i \<in> A \<Longrightarrow> F i \<in> sets borel" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

323 
shows "borel = sigma UNIV (F ` A)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

324 
unfolding borel_def 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

325 
proof (intro sigma_eqI antisym) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

326 
have borel_rev_eq: "sigma_sets UNIV {S::'a set. open S} = sets borel" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

327 
unfolding borel_def by simp 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

328 
also have "\<dots> = sigma_sets UNIV X" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

329 
unfolding borel_eq by simp 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

330 
also have "\<dots> \<subseteq> sigma_sets UNIV (F`A)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

331 
using X by (intro sigma_algebra.sigma_sets_subset[OF sigma_algebra_sigma_sets]) auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

332 
finally show "sigma_sets UNIV {S. open S} \<subseteq> sigma_sets UNIV (F`A)" . 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

333 
show "sigma_sets UNIV (F`A) \<subseteq> sigma_sets UNIV {S. open S}" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

334 
unfolding borel_rev_eq using F by (intro borel_sigma_sets_subset) auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

335 
qed auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

336 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

337 
lemma borel_eq_sigmaI2: 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

338 
fixes F :: "'i \<Rightarrow> 'j \<Rightarrow> 'a::topological_space set" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

339 
and G :: "'l \<Rightarrow> 'k \<Rightarrow> 'a::topological_space set" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

340 
assumes borel_eq: "borel = sigma UNIV ((\<lambda>(i, j). G i j)`B)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

341 
assumes X: "\<And>i j. (i, j) \<in> B \<Longrightarrow> G i j \<in> sets (sigma UNIV ((\<lambda>(i, j). F i j) ` A))" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

342 
assumes F: "\<And>i j. (i, j) \<in> A \<Longrightarrow> F i j \<in> sets borel" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

343 
shows "borel = sigma UNIV ((\<lambda>(i, j). F i j) ` A)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

344 
using assms 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

345 
by (intro borel_eq_sigmaI1[where X="(\<lambda>(i, j). G i j) ` B" and F="(\<lambda>(i, j). F i j)"]) auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

346 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

347 
lemma borel_eq_sigmaI3: 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

348 
fixes F :: "'i \<Rightarrow> 'j \<Rightarrow> 'a::topological_space set" and X :: "'a::topological_space set set" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

349 
assumes borel_eq: "borel = sigma UNIV X" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

350 
assumes X: "\<And>x. x \<in> X \<Longrightarrow> x \<in> sets (sigma UNIV ((\<lambda>(i, j). F i j) ` A))" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

351 
assumes F: "\<And>i j. (i, j) \<in> A \<Longrightarrow> F i j \<in> sets borel" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

352 
shows "borel = sigma UNIV ((\<lambda>(i, j). F i j) ` A)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

353 
using assms by (intro borel_eq_sigmaI1[where X=X and F="(\<lambda>(i, j). F i j)"]) auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

354 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

355 
lemma borel_eq_sigmaI4: 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

356 
fixes F :: "'i \<Rightarrow> 'a::topological_space set" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

357 
and G :: "'l \<Rightarrow> 'k \<Rightarrow> 'a::topological_space set" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

358 
assumes borel_eq: "borel = sigma UNIV ((\<lambda>(i, j). G i j)`A)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

359 
assumes X: "\<And>i j. (i, j) \<in> A \<Longrightarrow> G i j \<in> sets (sigma UNIV (range F))" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

360 
assumes F: "\<And>i. F i \<in> sets borel" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

361 
shows "borel = sigma UNIV (range F)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

362 
using assms by (intro borel_eq_sigmaI1[where X="(\<lambda>(i, j). G i j) ` A" and F=F]) auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

363 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

364 
lemma borel_eq_sigmaI5: 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

365 
fixes F :: "'i \<Rightarrow> 'j \<Rightarrow> 'a::topological_space set" and G :: "'l \<Rightarrow> 'a::topological_space set" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

366 
assumes borel_eq: "borel = sigma UNIV (range G)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

367 
assumes X: "\<And>i. G i \<in> sets (sigma UNIV (range (\<lambda>(i, j). F i j)))" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

368 
assumes F: "\<And>i j. F i j \<in> sets borel" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

369 
shows "borel = sigma UNIV (range (\<lambda>(i, j). F i j))" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

370 
using assms by (intro borel_eq_sigmaI1[where X="range G" and F="(\<lambda>(i, j). F i j)"]) auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

371 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

372 
lemma borel_eq_box: 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

373 
"borel = sigma UNIV (range (\<lambda> (a, b). box a b :: 'a \<Colon> euclidean_space set))" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

374 
(is "_ = ?SIGMA") 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

375 
proof (rule borel_eq_sigmaI1[OF borel_def]) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

376 
fix M :: "'a set" assume "M \<in> {S. open S}" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

377 
then have "open M" by simp 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

378 
show "M \<in> ?SIGMA" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

379 
apply (subst open_UNION_box[OF `open M`]) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

380 
apply (safe intro!: sets.countable_UN' countable_PiE countable_Collect) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

381 
apply (auto intro: countable_rat) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

382 
done 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

383 
qed (auto simp: box_def) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

384 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

385 
lemma halfspace_gt_in_halfspace: 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

386 
assumes i: "i \<in> A" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

387 
shows "{x\<Colon>'a. a < x \<bullet> i} \<in> 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

388 
sigma_sets UNIV ((\<lambda> (a, i). {x\<Colon>'a\<Colon>euclidean_space. x \<bullet> i < a}) ` (UNIV \<times> A))" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

389 
(is "?set \<in> ?SIGMA") 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

390 
proof  
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

391 
interpret sigma_algebra UNIV ?SIGMA 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

392 
by (intro sigma_algebra_sigma_sets) simp_all 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

393 
have *: "?set = (\<Union>n. UNIV  {x\<Colon>'a. x \<bullet> i < a + 1 / real (Suc n)})" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

394 
proof (safe, simp_all add: not_less) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

395 
fix x :: 'a assume "a < x \<bullet> i" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

396 
with reals_Archimedean[of "x \<bullet> i  a"] 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

397 
obtain n where "a + 1 / real (Suc n) < x \<bullet> i" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

398 
by (auto simp: inverse_eq_divide field_simps) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

399 
then show "\<exists>n. a + 1 / real (Suc n) \<le> x \<bullet> i" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

400 
by (blast intro: less_imp_le) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

401 
next 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

402 
fix x n 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

403 
have "a < a + 1 / real (Suc n)" by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

404 
also assume "\<dots> \<le> x" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

405 
finally show "a < x" . 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

406 
qed 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

407 
show "?set \<in> ?SIGMA" unfolding * 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

408 
by (auto del: Diff intro!: Diff i) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

409 
qed 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

410 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

411 
lemma borel_eq_halfspace_less: 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

412 
"borel = sigma UNIV ((\<lambda>(a, i). {x::'a::euclidean_space. x \<bullet> i < a}) ` (UNIV \<times> Basis))" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

413 
(is "_ = ?SIGMA") 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

414 
proof (rule borel_eq_sigmaI2[OF borel_eq_box]) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

415 
fix a b :: 'a 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

416 
have "box a b = {x\<in>space ?SIGMA. \<forall>i\<in>Basis. a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i}" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

417 
by (auto simp: box_def) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

418 
also have "\<dots> \<in> sets ?SIGMA" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

419 
by (intro sets.sets_Collect_conj sets.sets_Collect_finite_All sets.sets_Collect_const) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

420 
(auto intro!: halfspace_gt_in_halfspace countable_PiE countable_rat) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

421 
finally show "box a b \<in> sets ?SIGMA" . 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

422 
qed auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

423 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

424 
lemma borel_eq_halfspace_le: 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

425 
"borel = sigma UNIV ((\<lambda> (a, i). {x::'a::euclidean_space. x \<bullet> i \<le> a}) ` (UNIV \<times> Basis))" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

426 
(is "_ = ?SIGMA") 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

427 
proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_less]) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

428 
fix a :: real and i :: 'a assume "(a, i) \<in> UNIV \<times> Basis" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

429 
then have i: "i \<in> Basis" by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

430 
have *: "{x::'a. x\<bullet>i < a} = (\<Union>n. {x. x\<bullet>i \<le> a  1/real (Suc n)})" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

431 
proof (safe, simp_all) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

432 
fix x::'a assume *: "x\<bullet>i < a" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

433 
with reals_Archimedean[of "a  x\<bullet>i"] 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

434 
obtain n where "x \<bullet> i < a  1 / (real (Suc n))" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

435 
by (auto simp: field_simps inverse_eq_divide) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

436 
then show "\<exists>n. x \<bullet> i \<le> a  1 / (real (Suc n))" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

437 
by (blast intro: less_imp_le) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

438 
next 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

439 
fix x::'a and n 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

440 
assume "x\<bullet>i \<le> a  1 / real (Suc n)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

441 
also have "\<dots> < a" by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

442 
finally show "x\<bullet>i < a" . 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

443 
qed 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

444 
show "{x. x\<bullet>i < a} \<in> ?SIGMA" unfolding * 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

445 
by (safe intro!: sets.countable_UN) (auto intro: i) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

446 
qed auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

447 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

448 
lemma borel_eq_halfspace_ge: 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

449 
"borel = sigma UNIV ((\<lambda> (a, i). {x\<Colon>'a\<Colon>euclidean_space. a \<le> x \<bullet> i}) ` (UNIV \<times> Basis))" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

450 
(is "_ = ?SIGMA") 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

451 
proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_less]) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

452 
fix a :: real and i :: 'a assume i: "(a, i) \<in> UNIV \<times> Basis" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

453 
have *: "{x::'a. x\<bullet>i < a} = space ?SIGMA  {x::'a. a \<le> x\<bullet>i}" by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

454 
show "{x. x\<bullet>i < a} \<in> ?SIGMA" unfolding * 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

455 
using i by (safe intro!: sets.compl_sets) auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

456 
qed auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

457 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

458 
lemma borel_eq_halfspace_greater: 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

459 
"borel = sigma UNIV ((\<lambda> (a, i). {x\<Colon>'a\<Colon>euclidean_space. a < x \<bullet> i}) ` (UNIV \<times> Basis))" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

460 
(is "_ = ?SIGMA") 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

461 
proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_le]) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

462 
fix a :: real and i :: 'a assume "(a, i) \<in> (UNIV \<times> Basis)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

463 
then have i: "i \<in> Basis" by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

464 
have *: "{x::'a. x\<bullet>i \<le> a} = space ?SIGMA  {x::'a. a < x\<bullet>i}" by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

465 
show "{x. x\<bullet>i \<le> a} \<in> ?SIGMA" unfolding * 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

466 
by (safe intro!: sets.compl_sets) (auto intro: i) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

467 
qed auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

468 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

469 
lemma borel_eq_atMost: 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

470 
"borel = sigma UNIV (range (\<lambda>a. {..a\<Colon>'a\<Colon>ordered_euclidean_space}))" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

471 
(is "_ = ?SIGMA") 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

472 
proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_le]) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

473 
fix a :: real and i :: 'a assume "(a, i) \<in> UNIV \<times> Basis" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

474 
then have "i \<in> Basis" by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

475 
then have *: "{x::'a. x\<bullet>i \<le> a} = (\<Union>k::nat. {.. (\<Sum>n\<in>Basis. (if n = i then a else real k)*\<^sub>R n)})" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

476 
proof (safe, simp_all add: eucl_le[where 'a='a] split: split_if_asm) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

477 
fix x :: 'a 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

478 
from real_arch_simple[of "Max ((\<lambda>i. x\<bullet>i)`Basis)"] guess k::nat .. 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

479 
then have "\<And>i. i \<in> Basis \<Longrightarrow> x\<bullet>i \<le> real k" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

480 
by (subst (asm) Max_le_iff) auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

481 
then show "\<exists>k::nat. \<forall>ia\<in>Basis. ia \<noteq> i \<longrightarrow> x \<bullet> ia \<le> real k" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

482 
by (auto intro!: exI[of _ k]) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

483 
qed 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

484 
show "{x. x\<bullet>i \<le> a} \<in> ?SIGMA" unfolding * 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

485 
by (safe intro!: sets.countable_UN) auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

486 
qed auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

487 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

488 
lemma borel_eq_greaterThan: 
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset

489 
"borel = sigma UNIV (range (\<lambda>a\<Colon>'a\<Colon>ordered_euclidean_space. {x. a <e x}))" 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

490 
(is "_ = ?SIGMA") 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

491 
proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_le]) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

492 
fix a :: real and i :: 'a assume "(a, i) \<in> UNIV \<times> Basis" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

493 
then have i: "i \<in> Basis" by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

494 
have "{x::'a. x\<bullet>i \<le> a} = UNIV  {x::'a. a < x\<bullet>i}" by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

495 
also have *: "{x::'a. a < x\<bullet>i} = 
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset

496 
(\<Union>k::nat. {x. (\<Sum>n\<in>Basis. (if n = i then a else real k) *\<^sub>R n) <e x})" using i 
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset

497 
proof (safe, simp_all add: eucl_less_def split: split_if_asm) 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

498 
fix x :: 'a 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

499 
from reals_Archimedean2[of "Max ((\<lambda>i. x\<bullet>i)`Basis)"] 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

500 
guess k::nat .. note k = this 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

501 
{ fix i :: 'a assume "i \<in> Basis" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

502 
then have "x\<bullet>i < real k" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

503 
using k by (subst (asm) Max_less_iff) auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

504 
then have " real k < x\<bullet>i" by simp } 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

505 
then show "\<exists>k::nat. \<forall>ia\<in>Basis. ia \<noteq> i \<longrightarrow> real k < x \<bullet> ia" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

506 
by (auto intro!: exI[of _ k]) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

507 
qed 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

508 
finally show "{x. x\<bullet>i \<le> a} \<in> ?SIGMA" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

509 
apply (simp only:) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

510 
apply (safe intro!: sets.countable_UN sets.Diff) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

511 
apply (auto intro: sigma_sets_top) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

512 
done 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

513 
qed auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

514 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

515 
lemma borel_eq_lessThan: 
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset

516 
"borel = sigma UNIV (range (\<lambda>a\<Colon>'a\<Colon>ordered_euclidean_space. {x. x <e a}))" 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

517 
(is "_ = ?SIGMA") 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

518 
proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_ge]) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

519 
fix a :: real and i :: 'a assume "(a, i) \<in> UNIV \<times> Basis" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

520 
then have i: "i \<in> Basis" by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

521 
have "{x::'a. a \<le> x\<bullet>i} = UNIV  {x::'a. x\<bullet>i < a}" by auto 
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset

522 
also have *: "{x::'a. x\<bullet>i < a} = (\<Union>k::nat. {x. x <e (\<Sum>n\<in>Basis. (if n = i then a else real k) *\<^sub>R n)})" using `i\<in> Basis` 
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset

523 
proof (safe, simp_all add: eucl_less_def split: split_if_asm) 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

524 
fix x :: 'a 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

525 
from reals_Archimedean2[of "Max ((\<lambda>i. x\<bullet>i)`Basis)"] 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

526 
guess k::nat .. note k = this 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

527 
{ fix i :: 'a assume "i \<in> Basis" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

528 
then have "x\<bullet>i < real k" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

529 
using k by (subst (asm) Max_less_iff) auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

530 
then have "x\<bullet>i < real k" by simp } 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

531 
then show "\<exists>k::nat. \<forall>ia\<in>Basis. ia \<noteq> i \<longrightarrow> x \<bullet> ia < real k" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

532 
by (auto intro!: exI[of _ k]) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

533 
qed 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

534 
finally show "{x. a \<le> x\<bullet>i} \<in> ?SIGMA" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

535 
apply (simp only:) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

536 
apply (safe intro!: sets.countable_UN sets.Diff) 
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset

537 
apply (auto intro: sigma_sets_top ) 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

538 
done 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

539 
qed auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

540 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

541 
lemma borel_eq_atLeastAtMost: 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

542 
"borel = sigma UNIV (range (\<lambda>(a,b). {a..b} \<Colon>'a\<Colon>ordered_euclidean_space set))" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

543 
(is "_ = ?SIGMA") 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

544 
proof (rule borel_eq_sigmaI5[OF borel_eq_atMost]) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

545 
fix a::'a 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

546 
have *: "{..a} = (\<Union>n::nat. { real n *\<^sub>R One .. a})" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

547 
proof (safe, simp_all add: eucl_le[where 'a='a]) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

548 
fix x :: 'a 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

549 
from real_arch_simple[of "Max ((\<lambda>i.  x\<bullet>i)`Basis)"] 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

550 
guess k::nat .. note k = this 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

551 
{ fix i :: 'a assume "i \<in> Basis" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

552 
with k have " x\<bullet>i \<le> real k" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

553 
by (subst (asm) Max_le_iff) (auto simp: field_simps) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

554 
then have " real k \<le> x\<bullet>i" by simp } 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

555 
then show "\<exists>n::nat. \<forall>i\<in>Basis.  real n \<le> x \<bullet> i" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

556 
by (auto intro!: exI[of _ k]) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

557 
qed 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

558 
show "{..a} \<in> ?SIGMA" unfolding * 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

559 
by (safe intro!: sets.countable_UN) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

560 
(auto intro!: sigma_sets_top) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

561 
qed auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

562 

54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset

563 
lemma eucl_lessThan: "{x::real. x <e a} = lessThan a" 
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset

564 
by (simp add: eucl_less_def lessThan_def) 
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset

565 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

566 
lemma borel_eq_atLeastLessThan: 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

567 
"borel = sigma UNIV (range (\<lambda>(a, b). {a ..< b :: real}))" (is "_ = ?SIGMA") 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

568 
proof (rule borel_eq_sigmaI5[OF borel_eq_lessThan]) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

569 
have move_uminus: "\<And>x y::real. x \<le> y \<longleftrightarrow> y \<le> x" by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

570 
fix x :: real 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

571 
have "{..<x} = (\<Union>i::nat. {real i ..< x})" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

572 
by (auto simp: move_uminus real_arch_simple) 
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset

573 
then show "{y. y <e x} \<in> ?SIGMA" 
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset

574 
by (auto intro: sigma_sets.intros simp: eucl_lessThan) 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

575 
qed auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

576 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

577 
lemma borel_eq_closed: "borel = sigma UNIV (Collect closed)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

578 
unfolding borel_def 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

579 
proof (intro sigma_eqI sigma_sets_eqI, safe) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

580 
fix x :: "'a set" assume "open x" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

581 
hence "x = UNIV  (UNIV  x)" by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

582 
also have "\<dots> \<in> sigma_sets UNIV (Collect closed)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

583 
by (rule sigma_sets.Compl) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

584 
(auto intro!: sigma_sets.Basic simp: `open x`) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

585 
finally show "x \<in> sigma_sets UNIV (Collect closed)" by simp 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

586 
next 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

587 
fix x :: "'a set" assume "closed x" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

588 
hence "x = UNIV  (UNIV  x)" by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

589 
also have "\<dots> \<in> sigma_sets UNIV (Collect open)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

590 
by (rule sigma_sets.Compl) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

591 
(auto intro!: sigma_sets.Basic simp: `closed x`) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

592 
finally show "x \<in> sigma_sets UNIV (Collect open)" by simp 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

593 
qed simp_all 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

594 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

595 
lemma borel_measurable_halfspacesI: 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

596 
fixes f :: "'a \<Rightarrow> 'c\<Colon>euclidean_space" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

597 
assumes F: "borel = sigma UNIV (F ` (UNIV \<times> Basis))" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

598 
and S_eq: "\<And>a i. S a i = f ` F (a,i) \<inter> space M" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

599 
shows "f \<in> borel_measurable M = (\<forall>i\<in>Basis. \<forall>a::real. S a i \<in> sets M)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

600 
proof safe 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

601 
fix a :: real and i :: 'b assume i: "i \<in> Basis" and f: "f \<in> borel_measurable M" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

602 
then show "S a i \<in> sets M" unfolding assms 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

603 
by (auto intro!: measurable_sets simp: assms(1)) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

604 
next 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

605 
assume a: "\<forall>i\<in>Basis. \<forall>a. S a i \<in> sets M" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

606 
then show "f \<in> borel_measurable M" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

607 
by (auto intro!: measurable_measure_of simp: S_eq F) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

608 
qed 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

609 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

610 
lemma borel_measurable_iff_halfspace_le: 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

611 
fixes f :: "'a \<Rightarrow> 'c\<Colon>euclidean_space" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

612 
shows "f \<in> borel_measurable M = (\<forall>i\<in>Basis. \<forall>a. {w \<in> space M. f w \<bullet> i \<le> a} \<in> sets M)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

613 
by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_le]) auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

614 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

615 
lemma borel_measurable_iff_halfspace_less: 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

616 
fixes f :: "'a \<Rightarrow> 'c\<Colon>euclidean_space" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

617 
shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i\<in>Basis. \<forall>a. {w \<in> space M. f w \<bullet> i < a} \<in> sets M)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

618 
by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_less]) auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

619 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

620 
lemma borel_measurable_iff_halfspace_ge: 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

621 
fixes f :: "'a \<Rightarrow> 'c\<Colon>euclidean_space" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

622 
shows "f \<in> borel_measurable M = (\<forall>i\<in>Basis. \<forall>a. {w \<in> space M. a \<le> f w \<bullet> i} \<in> sets M)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

623 
by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_ge]) auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

624 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

625 
lemma borel_measurable_iff_halfspace_greater: 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

626 
fixes f :: "'a \<Rightarrow> 'c\<Colon>euclidean_space" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

627 
shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i\<in>Basis. \<forall>a. {w \<in> space M. a < f w \<bullet> i} \<in> sets M)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

628 
by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_greater]) auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

629 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

630 
lemma borel_measurable_iff_le: 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

631 
"(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w \<le> a} \<in> sets M)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

632 
using borel_measurable_iff_halfspace_le[where 'c=real] by simp 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

633 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

634 
lemma borel_measurable_iff_less: 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

635 
"(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w < a} \<in> sets M)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

636 
using borel_measurable_iff_halfspace_less[where 'c=real] by simp 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

637 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

638 
lemma borel_measurable_iff_ge: 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

639 
"(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a \<le> f w} \<in> sets M)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

640 
using borel_measurable_iff_halfspace_ge[where 'c=real] 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

641 
by simp 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

642 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

643 
lemma borel_measurable_iff_greater: 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

644 
"(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a < f w} \<in> sets M)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

645 
using borel_measurable_iff_halfspace_greater[where 'c=real] by simp 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

646 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

647 
lemma borel_measurable_euclidean_space: 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

648 
fixes f :: "'a \<Rightarrow> 'c::euclidean_space" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

649 
shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i\<in>Basis. (\<lambda>x. f x \<bullet> i) \<in> borel_measurable M)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

650 
proof safe 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

651 
assume f: "\<forall>i\<in>Basis. (\<lambda>x. f x \<bullet> i) \<in> borel_measurable M" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

652 
then show "f \<in> borel_measurable M" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

653 
by (subst borel_measurable_iff_halfspace_le) auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

654 
qed auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

655 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

656 
subsection "Borel measurable operators" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

657 

56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56371
diff
changeset

658 
lemma borel_measurable_norm[measurable]: "norm \<in> borel_measurable borel" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56371
diff
changeset

659 
by (intro borel_measurable_continuous_on1 continuous_intros) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56371
diff
changeset

660 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

661 
lemma borel_measurable_uminus[measurable (raw)]: 
51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

662 
fixes g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}" 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

663 
assumes g: "g \<in> borel_measurable M" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

664 
shows "(\<lambda>x.  g x) \<in> borel_measurable M" 
56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56212
diff
changeset

665 
by (rule borel_measurable_continuous_on[OF _ g]) (intro continuous_intros) 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

666 

50003  667 
lemma borel_measurable_add[measurable (raw)]: 
51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

668 
fixes f g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}" 
49774  669 
assumes f: "f \<in> borel_measurable M" 
670 
assumes g: "g \<in> borel_measurable M" 

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

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56212
diff
changeset

672 
using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros) 
49774  673 

50003  674 
lemma borel_measurable_setsum[measurable (raw)]: 
51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

675 
fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}" 
49774  676 
assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M" 
677 
shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M" 

678 
proof cases 

679 
assume "finite S" 

680 
thus ?thesis using assms by induct auto 

681 
qed simp 

682 

50003  683 
lemma borel_measurable_diff[measurable (raw)]: 
51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

684 
fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}" 
49774  685 
assumes f: "f \<in> borel_measurable M" 
686 
assumes g: "g \<in> borel_measurable M" 

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

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53216
diff
changeset

688 
using borel_measurable_add [of f M " g"] assms by (simp add: fun_Compl_def) 
49774  689 

50003  690 
lemma borel_measurable_times[measurable (raw)]: 
51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

691 
fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_algebra}" 
49774  692 
assumes f: "f \<in> borel_measurable M" 
693 
assumes g: "g \<in> borel_measurable M" 

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

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56212
diff
changeset

695 
using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros) 
51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

696 

baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

697 
lemma borel_measurable_setprod[measurable (raw)]: 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

698 
fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> 'b::{second_countable_topology, real_normed_field}" 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

699 
assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M" 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

700 
shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M" 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

701 
proof cases 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

702 
assume "finite S" 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

703 
thus ?thesis using assms by induct auto 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

704 
qed simp 
49774  705 

50003  706 
lemma borel_measurable_dist[measurable (raw)]: 
51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

707 
fixes g f :: "'a \<Rightarrow> 'b::{second_countable_topology, metric_space}" 
49774  708 
assumes f: "f \<in> borel_measurable M" 
709 
assumes g: "g \<in> borel_measurable M" 

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

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56212
diff
changeset

711 
using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros) 
49774  712 

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

713 
lemma borel_measurable_scaleR[measurable (raw)]: 
51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

714 
fixes g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}" 
50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

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

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

717 
shows "(\<lambda>x. f x *\<^sub>R g x) \<in> borel_measurable M" 
56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56212
diff
changeset

718 
using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros) 
50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

719 

47694  720 
lemma affine_borel_measurable_vector: 
38656  721 
fixes f :: "'a \<Rightarrow> 'x::real_normed_vector" 
722 
assumes "f \<in> borel_measurable M" 

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

724 
proof (rule borel_measurableI) 

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

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

727 
proof cases 

728 
assume "b \<noteq> 0" 

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

729 
with `open S` have "open ((\<lambda>x. ( a + x) /\<^sub>R b) ` S)" (is "open ?S") 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53216
diff
changeset

730 
using open_affinity [of S "inverse b" " a /\<^sub>R b"] 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53216
diff
changeset

731 
by (auto simp: algebra_simps) 
47694  732 
hence "?S \<in> sets borel" by auto 
38656  733 
moreover 
734 
from `b \<noteq> 0` have "(\<lambda>x. a + b *\<^sub>R f x) ` S = f ` ?S" 

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

40859  736 
ultimately show ?thesis using assms unfolding in_borel_measurable_borel 
38656  737 
by auto 
738 
qed simp 

739 
qed 

740 

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

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

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

743 
using affine_borel_measurable_vector[of f M 0 b] by simp 
38656  744 

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

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

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

747 
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

748 

50003  749 
lemma borel_measurable_inverse[measurable (raw)]: 
51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

750 
fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_div_algebra}" 
49774  751 
assumes f: "f \<in> borel_measurable M" 
35692  752 
shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M" 
49774  753 
proof  
51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

754 
have "(\<lambda>x::'b. if x \<in> UNIV  {0} then inverse x else inverse 0) \<in> borel_measurable borel" 
56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56212
diff
changeset

755 
by (intro borel_measurable_continuous_on_open' continuous_intros) auto 
51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

756 
also have "(\<lambda>x::'b. if x \<in> UNIV  {0} then inverse x else inverse 0) = inverse" 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

757 
by (intro ext) auto 
50003  758 
finally show ?thesis using f by simp 
35692  759 
qed 
760 

50003  761 
lemma borel_measurable_divide[measurable (raw)]: 
51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

762 
"f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

763 
(\<lambda>x. f x / g x::'b::{second_countable_topology, real_normed_field}) \<in> borel_measurable M" 
50003  764 
by (simp add: field_divide_inverse) 
38656  765 

50003  766 
lemma borel_measurable_max[measurable (raw)]: 
53216  767 
"f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. max (g x) (f x) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \<in> borel_measurable M" 
50003  768 
by (simp add: max_def) 
38656  769 

50003  770 
lemma borel_measurable_min[measurable (raw)]: 
53216  771 
"f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. min (g x) (f x) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \<in> borel_measurable M" 
50003  772 
by (simp add: min_def) 
38656  773 

50003  774 
lemma borel_measurable_abs[measurable (raw)]: 
775 
"f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. \<bar>f x :: real\<bar>) \<in> borel_measurable M" 

776 
unfolding abs_real_def by simp 

38656  777 

50003  778 
lemma borel_measurable_nth[measurable (raw)]: 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41025
diff
changeset

779 
"(\<lambda>x::real^'n. x $ i) \<in> borel_measurable borel" 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

780 
by (simp add: cart_eq_inner_axis) 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41025
diff
changeset

781 

47694  782 
lemma convex_measurable: 
51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

783 
fixes A :: "'a :: ordered_euclidean_space set" 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

784 
assumes X: "X \<in> borel_measurable M" "X ` space M \<subseteq> A" "open A" 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

785 
assumes q: "convex_on A q" 
49774  786 
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

787 
proof  
51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

788 
have "(\<lambda>x. if X x \<in> A then q (X x) else 0) \<in> borel_measurable M" (is "?qX") 
49774  789 
proof (rule borel_measurable_continuous_on_open[OF _ _ X(1)]) 
51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

790 
show "open A" by fact 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

791 
from this q show "continuous_on A q" 
42990
3706951a6421
composition of convex and measurable function is measurable
hoelzl
parents:
42950
diff
changeset

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

794 
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

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

796 
finally show ?thesis . 
41830  797 
qed 
798 

50003  799 
lemma borel_measurable_ln[measurable (raw)]: 
49774  800 
assumes f: "f \<in> borel_measurable M" 
801 
shows "(\<lambda>x. ln (f x)) \<in> borel_measurable M" 

41830  802 
proof  
803 
{ fix x :: real assume x: "x \<le> 0" 

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

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

807 
note ln_imp = this 

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

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

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

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51351
diff
changeset

811 
by (auto intro!: continuous_at_imp_continuous_on DERIV_ln DERIV_isCont) 
41830  812 
show "open ({0<..}::real set)" by auto 
813 
qed 

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

41830  816 
finally show ?thesis . 
817 
qed 

818 

50003  819 
lemma borel_measurable_log[measurable (raw)]: 
50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

820 
"f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. log (g x) (f x)) \<in> borel_measurable M" 
49774  821 
unfolding log_def by auto 
41830  822 

50419  823 
lemma borel_measurable_exp[measurable]: "exp \<in> borel_measurable borel" 
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51351
diff
changeset

824 
by (intro borel_measurable_continuous_on1 continuous_at_imp_continuous_on ballI isCont_exp) 
50419  825 

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

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

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

829 
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

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

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

832 
by (auto simp: vimage_def measurable_count_space_eq2_countable) 
47761  833 
qed 
834 

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

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

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

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

838 

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

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

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

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

842 

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

843 
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

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

845 

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

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

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

849 

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

850 
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

851 

50003  852 
lemma borel_measurable_ereal[measurable (raw)]: 
43920  853 
assumes f: "f \<in> borel_measurable M" shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M" 
49774  854 
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

855 

50003  856 
lemma borel_measurable_real_of_ereal[measurable (raw)]: 
49774  857 
fixes f :: "'a \<Rightarrow> ereal" 
858 
assumes f: "f \<in> borel_measurable M" 

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

860 
proof  

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

862 
using continuous_on_real 

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

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

865 
by auto 

866 
finally show ?thesis . 

867 
qed 

868 

869 
lemma borel_measurable_ereal_cases: 

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

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

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

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

874 
proof  

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

875 
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  876 
{ 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

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

879 

49774  880 
lemma 
50003  881 
fixes f :: "'a \<Rightarrow> ereal" assumes f[measurable]: "f \<in> borel_measurable M" 
882 
shows borel_measurable_ereal_abs[measurable(raw)]: "(\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M" 

883 
and borel_measurable_ereal_inverse[measurable(raw)]: "(\<lambda>x. inverse (f x) :: ereal) \<in> borel_measurable M" 

884 
and borel_measurable_uminus_ereal[measurable(raw)]: "(\<lambda>x.  f x :: ereal) \<in> borel_measurable M" 

49774  885 
by (auto simp del: abs_real_of_ereal simp: borel_measurable_ereal_cases[OF f] measurable_If) 
886 

887 
lemma borel_measurable_uminus_eq_ereal[simp]: 

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

889 
proof 

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

891 
qed auto 

892 

893 
lemma set_Collect_ereal2: 

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

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

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

897 
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

898 
"{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

899 
"{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

900 
"{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

901 
"{x \<in> space borel. H (ereal x) (\<infinity>)} \<in> sets borel" 
49774  902 
shows "{x \<in> space M. H (f x) (g x)} \<in> sets M" 
903 
proof  

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

904 
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

905 
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  906 
{ 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

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

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

909 
by (subst *) (simp del: space_borel split del: split_if) 
49774  910 
qed 
911 

47694  912 
lemma borel_measurable_ereal_iff: 
43920  913 
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

914 
proof 
43920  915 
assume "(\<lambda>x. ereal (f x)) \<in> borel_measurable M" 
916 
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

917 
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

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

919 

47694  920 
lemma borel_measurable_ereal_iff_real: 
43923  921 
fixes f :: "'a \<Rightarrow> ereal" 
922 
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

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

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

925 
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

926 
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

927 
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  928 
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

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

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

932 
qed simp_all 
41830  933 

47694  934 
lemma borel_measurable_eq_atMost_ereal: 
43923  935 
fixes f :: "'a \<Rightarrow> ereal" 
936 
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

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

938 
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

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

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

942 
fix a :: real 
43920  943 
{ 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

944 
have "x = \<infinity>" 
43920  945 
proof (rule ereal_top) 
44666  946 
fix B from reals_Archimedean2[of B] guess n .. 
43920  947 
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

948 
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

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

950 
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

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

952 
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

953 
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

954 
moreover 
43923  955 
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

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

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

962 
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

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

965 
qed (simp add: measurable_sets) 
35582  966 

47694  967 
lemma borel_measurable_eq_atLeast_ereal: 
43920  968 
"(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

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

970 
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

971 
moreover have "\<And>a. (\<lambda>x.  f x) ` {..a} = f ` {a ..}" 
43920  972 
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

973 
ultimately have "(\<lambda>x.  f x) \<in> borel_measurable M" 
43920  974 
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

975 
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

976 
qed (simp add: measurable_sets) 
35582  977 

49774  978 
lemma greater_eq_le_measurable: 
979 
fixes f :: "'a \<Rightarrow> 'c::linorder" 

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

981 
proof 

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

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

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

985 
next 

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

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

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

989 
qed 

990 

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

38656  994 

49774  995 
lemma less_eq_ge_measurable: 
996 
fixes f :: "'a \<Rightarrow> 'c::linorder" 

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

998 
proof 

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

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

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

1002 
next 

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

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

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

1006 
qed 

1007 

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

38656  1011 

49774  1012 
lemma borel_measurable_ereal2: 
1013 
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

1014 
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

1015 
assumes g: "g \<in> borel_measurable M" 
49774  1016 
assumes H: "(\<lambda>x. H (ereal (real (f x))) (ereal (real (g x)))) \<in> borel_measurable M" 
1017 
"(\<lambda>x. H (\<infinity>) (ereal (real (g x)))) \<in> borel_measurable M" 

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

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

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

1021 
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

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

1023 
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

1024 
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  1025 
{ 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

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

1027 
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

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

1029 

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

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

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

1034 
using f by auto 

38656  1035 

50003  1036 
lemma [measurable(raw)]: 
43920  1037 
fixes f :: "'a \<Rightarrow> ereal" 
50003  1038 
assumes [measurable]: "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

1039 
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

1040 
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

1041 
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

1042 
and borel_measurable_ereal_max: "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M" 
50003  1043 
by (simp_all add: borel_measurable_ereal2 min_def max_def) 
49774  1044 

50003  1045 
lemma [measurable(raw)]: 
49774  1046 
fixes f g :: "'a \<Rightarrow> ereal" 
1047 
assumes "f \<in> borel_measurable M" 

1048 
assumes "g \<in> borel_measurable M" 

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

1049 
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

1050 
and borel_measurable_ereal_divide: "(\<lambda>x. f x / g x) \<in> borel_measurable M" 
50003  1051 
using assms by (simp_all add: minus_ereal_def divide_ereal_def) 
38656  1052 

50003  1053 
lemma borel_measurable_ereal_setsum[measurable (raw)]: 
43920  1054 
fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal" 
41096  1055 
assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M" 
1056 
shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M" 

1057 
proof cases 

1058 
assume "finite S" 

1059 
thus ?thesis using assms 

1060 
by induct auto 

49774  1061 
qed simp 
38656  1062 

50003  1063 
lemma borel_measurable_ereal_setprod[measurable (raw)]: 
43920  1064 
fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal" 
38656  1065 
assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M" 
41096  1066 
shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M" 
38656  1067 
proof cases 
1068 
assume "finite S" 

41096  1069 
thus ?thesis using assms by induct auto 
1070 
qed simp 

38656  1071 

50003  1072 
lemma borel_measurable_SUP[measurable (raw)]: 
43920  1073 
fixes f :: "'d\<Colon>countable \<Rightarrow> 'a \<Rightarrow> ereal" 
38656  1074 
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

1075 
shows "(\<lambda>x. SUP i : A. f i x) \<in> borel_measurable M" (is "?sup \<in> borel_measurable M") 
43920  1076 
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

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

1079 
have "?sup ` {a<..} \<inter> space M = (\<Union>i\<in>A. {x\<in>space M. a < f i x})" 
46884  1080 
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

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

1084 

50003  1085 
lemma borel_measurable_INF[measurable (raw)]: 
43920  1086 
fixes f :: "'d :: countable \<Rightarrow> 'a \<Rightarrow> ereal" 
38656  1087 
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

1088 
shows "(\<lambda>x. INF i : A. f i x) \<in> borel_measurable M" (is "?inf \<in> borel_measurable M") 
43920  1089 
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

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

1092 
have "?inf ` {..<a} \<inter> space M = (\<Union>i\<in>A. {x\<in>space M. f i x < a})" 
46884  1093 
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

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

1097 

50003  1098 
lemma [measurable (raw)]: 
43920  1099 
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

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

1101 
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

1102 
and borel_measurable_limsup: "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M" 
56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
54775
diff
changeset

1103 
unfolding liminf_SUP_INF limsup_INF_SUP using assms by auto 
35692  1104 

50104  1105 
lemma sets_Collect_eventually_sequentially[measurable]: 
50003  1106 
"(\<And>i. {x\<in>space M. P x i} \<in> sets M) \<Longrightarrow> {x\<in>space M. eventually (P x) sequentially} \<in> sets M" 
1107 
unfolding eventually_sequentially by simp 

1108 

1109 
lemma sets_Collect_ereal_convergent[measurable]: 

1110 
fixes f :: "nat \<Rightarrow> 'a => ereal" 

1111 
assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M" 

1112 
shows "{x\<in>space M. convergent (\<lambda>i. f i x)} \<in> sets M" 

1113 
unfolding convergent_ereal by auto 

1114 

1115 
lemma borel_measurable_extreal_lim[measurable (raw)]: 

1116 
fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal" 

1117 
assumes [measurable]: "\<And>i. f i \<in> borel_measurable M" 

1118 
shows "(\<lambda>x. lim (\<lambda>i. f i x)) \<in> borel_measurable M" 

1119 
proof  

1120 
have "\<And>x. lim (\<lambda>i. f i x) = (if convergent (\<lambda>i. f i x) then limsup (\<lambda>i. f i x) else (THE i. False))" 

51351  1121 
by (simp add: lim_def convergent_def convergent_limsup_cl) 
50003  1122 
then show ?thesis 
1123 
by simp 

1124 
qed 

1125 

49774  1126 
lemma borel_measurable_ereal_LIMSEQ: 
1127 
fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ereal" 

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

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

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

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

50003  1134 
with u show ?thesis by (simp cong: measurable_cong) 
47694  1135 
qed 
1136 

50003  1137 
lemma borel_measurable_extreal_suminf[measurable (raw)]: 
43920  1138 
fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal" 
50003  1139 
assumes [measurable]: "\<And>i. f i \<in> borel_measurable M" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41969
diff
changeset

1140 
shows "(\<lambda>x. (\<Sum>i. f i x)) \<in> borel_measurable M" 
50003  1141 
unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp 
39092  1142 

1143 
section "LIMSEQ is borel measurable" 

1144 

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

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

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

1150 
proof  

43920  1151 
have "\<And>x. x \<in> space M \<Longrightarrow> liminf (\<lambda>n. ereal (u n x)) = ereal (u' x)" 
46731  1152 
using u' by (simp add: lim_imp_Liminf) 
43920  1153 
moreover from u have "(\<lambda>x. liminf (\<lambda>n. ereal (u n x))) \<in> borel_measurable M" 
39092  1154 
by auto 
43920  1155 
ultimately show ?thesis by (simp cong: measurable_cong add: borel_measurable_ereal_iff) 
39092  1156 
qed 
1157 

56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56371
diff
changeset

1158 
lemma borel_measurable_LIMSEQ_metric: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56371
diff
changeset

1159 
fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b :: metric_space" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56371
diff
changeset

1160 
assumes [measurable]: "\<And>i. f i \<in> borel_measurable M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56371
diff
changeset

1161 
assumes lim: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. f i x) > g x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56371
diff
changeset

1162 
shows "g \<in> borel_measurable M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56371
diff
changeset

1163 
unfolding borel_eq_closed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56371
diff
changeset

1164 
proof (safe intro!: measurable_measure_of) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56371
diff
changeset

1165 
fix A :: "'b set" assume "closed A" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56371
diff
changeset

1166 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56371
diff
changeset

1167 
have [measurable]: "(\<lambda>x. infdist (g x) A) \<in> borel_measurable M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56371
diff
changeset

1168 
proof (rule borel_measurable_LIMSEQ) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56371
diff
changeset

1169 
show "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. infdist (f i x) A) > infdist (g x) A" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56371
diff
changeset

1170 
by (intro tendsto_infdist lim) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56371
diff
changeset

1171 
show "\<And>i. (\<lambda>x. infdist (f i x) A) \<in> borel_measurable M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56371
diff
changeset

1172 
by (intro borel_measurable_continuous_on[where f="\<lambda>x. infdist x A"] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56371
diff
changeset

1173 
continuous_at_imp_continuous_on ballI continuous_infdist isCont_ident) auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56371
diff
changeset

1174 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56371
diff
changeset

1175 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56371
diff
changeset

1176 
show "g ` A \<inter> space M \<in> sets M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56371
diff
changeset

1177 
proof cases 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56371
diff
changeset

1178 
assume "A \<noteq> {}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56371
diff
changeset

1179 
then have "\<And>x. infdist x A = 0 \<longleftrightarrow> x \<in> A" 