author  wenzelm 
Thu, 18 Apr 2013 17:07:01 +0200  
changeset 51717  9e7d1c139569 
parent 51683  baefa3b461c2 
child 53216  ad2e09c30aa8 
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 
51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

224 
by (rule borel_measurable_continuous_Pair) (intro continuous_on_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 

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

240 
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

241 
fixes a b :: "'a\<Colon>ordered_euclidean_space" 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

242 
shows "{..< 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

243 
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

244 
and "{a<..<b} \<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

245 
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

246 
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

247 
and "{a..b} \<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

248 
and "{a<..b} \<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

249 
and "{a..<b} \<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

250 
unfolding greaterThanAtMost_def atLeastLessThan_def 
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

251 
by (blast intro: borel_open borel_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

252 

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

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

254 
fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {inner_dense_linorder, linorder_topology}" 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

255 
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

256 
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

257 
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

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

259 
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

260 
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

261 
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

262 
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

263 
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

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

265 

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

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

267 
fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {inner_dense_linorder, linorder_topology}" 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

268 
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

269 
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

270 
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

271 
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

272 

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

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

274 
fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, inner_dense_linorder, linorder_topology}" 
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 \<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

276 
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

277 
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

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

279 
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

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

281 
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

282 
by (intro measurable_sets[OF borel_measurable_Pair borel_open, OF assms open_Collect_less] 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

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

284 
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

285 
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

286 

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

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

288 
fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, inner_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

289 
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

290 
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

291 
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

292 
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

293 
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

294 
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

295 
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

296 

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 
lemma 
51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

298 
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

299 
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

300 
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

301 
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

302 
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

303 
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

304 

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

305 
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

306 

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

307 
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

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

309 
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

310 

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

312 
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

313 
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

314 
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

315 
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

316 
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

317 
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

318 
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

319 
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

320 
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

321 
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

322 
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

323 
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

324 
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

325 
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

326 
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

327 
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

328 
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

329 

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

331 
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

332 
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

333 
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

334 
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

335 
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

336 
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

337 
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

338 
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

339 

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

341 
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

342 
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

343 
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

344 
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

345 
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

346 
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

347 

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

349 
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

350 
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

351 
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

352 
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

353 
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

354 
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

355 
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

356 

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

358 
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

359 
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

360 
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

361 
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

362 
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

363 
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

364 

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

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

367 
(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

368 
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

369 
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

370 
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

371 
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

372 
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

373 
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

374 
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

375 
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

376 
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

377 

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 
lemma borel_eq_greaterThanLessThan: 
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 
"borel = sigma UNIV (range (\<lambda> (a, b). {a <..< b} :: '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

380 
unfolding borel_eq_box apply (rule arg_cong2[where f=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

381 
by (auto simp: box_def image_iff mem_interval set_eq_iff simp del: greaterThanLessThan_iff) 
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 

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

384 
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

385 
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

386 
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

387 
(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

388 
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

389 
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

390 
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

391 
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

392 
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

393 
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

394 
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

395 
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

396 
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

397 
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

398 
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

399 
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

400 
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

401 
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

402 
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

403 
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

404 
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

405 
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

406 
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

407 
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

408 

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

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

411 
(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

412 
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

413 
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

414 
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

415 
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

416 
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

417 
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

418 
(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

419 
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

420 
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

421 

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

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

424 
(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

425 
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

426 
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

427 
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

428 
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

429 
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

430 
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

431 
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

432 
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

433 
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

434 
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

435 
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

436 
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

437 
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

438 
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

439 
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

440 
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

441 
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

442 
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

443 
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

444 
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

445 

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

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

448 
(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

449 
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

450 
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

451 
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

452 
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

453 
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

454 
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

455 

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

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

458 
(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

459 
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

460 
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

461 
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

462 
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

463 
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

464 
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

465 
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

466 

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

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

469 
(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

470 
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

471 
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

472 
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

473 
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

474 
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

475 
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

476 
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

477 
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

478 
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

479 
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

480 
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

481 
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

482 
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

483 
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

484 
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

485 

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 
lemma borel_eq_greaterThan: 
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 
"borel = sigma UNIV (range (\<lambda>a\<Colon>'a\<Colon>ordered_euclidean_space. {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

488 
(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

489 
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

490 
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

491 
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

492 
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

493 
also have *: "{x::'a. 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

494 
(\<Union>k::nat. {\<Sum>n\<in>Basis. (if n = i then a else real k) *\<^sub>R n <..})" using 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

495 
proof (safe, simp_all add: eucl_less[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

496 
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

497 
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

498 
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

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

500 
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

501 
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

502 
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

503 
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

504 
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

505 
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

506 
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

507 
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

508 
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

509 
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

510 
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

511 
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

512 

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 
lemma 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

514 
"borel = sigma UNIV (range (\<lambda>a\<Colon>'a\<Colon>ordered_euclidean_space. {..<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

515 
(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

516 
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

517 
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

518 
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

519 
have "{x::'a. a \<le> x\<bullet>i} = UNIV  {x::'a. x\<bullet>i < 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

520 
also have *: "{x::'a. x\<bullet>i < a} = (\<Union>k::nat. {..< \<Sum>n\<in>Basis. (if n = i then a else real k) *\<^sub>R n})" using `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

521 
proof (safe, simp_all add: eucl_less[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

522 
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

523 
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

524 
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

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

526 
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

527 
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

528 
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

529 
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

530 
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

531 
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

532 
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

533 
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

534 
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

535 
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

536 
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

537 
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

538 

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

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

541 
(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

542 
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

543 
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

544 
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

545 
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

546 
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

547 
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

548 
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

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

550 
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

551 
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

552 
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

553 
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

554 
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

555 
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

556 
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

557 
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

558 
(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

559 
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

560 

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

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

563 
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

564 
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

565 
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

566 
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

567 
by (auto simp: move_uminus real_arch_simple) 
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 
then show "{..< x} \<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

569 
by (auto intro: sigma_sets.intros) 
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 
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

571 

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

573 
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

574 
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

575 
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

576 
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

577 
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

578 
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

579 
(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

580 
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

581 
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

582 
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

583 
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

584 
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

585 
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

586 
(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

587 
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

588 
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

589 

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

591 
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

592 
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

593 
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

594 
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

595 
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

596 
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

597 
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

598 
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

599 
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

600 
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

601 
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

602 
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

603 
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

604 

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

606 
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

607 
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

608 
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

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_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

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

613 
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

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_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

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

618 
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

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_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

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

623 
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

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_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

626 
"(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

627 
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

628 

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

630 
"(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

631 
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

632 

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

634 
"(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

635 
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

636 
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_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

639 
"(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

640 
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

641 

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

643 
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

644 
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

645 
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

646 
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

647 
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

648 
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

649 
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

650 

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

652 

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

654 
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

655 
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

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

657 
by (rule borel_measurable_continuous_on[OF _ g]) (intro continuous_on_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

658 

50003  659 
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

660 
fixes f g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}" 
49774  661 
assumes f: "f \<in> borel_measurable M" 
662 
assumes g: "g \<in> borel_measurable M" 

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

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

664 
using f g by (rule borel_measurable_continuous_Pair) (intro continuous_on_intros) 
49774  665 

50003  666 
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

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

670 
proof cases 

671 
assume "finite S" 

672 
thus ?thesis using assms by induct auto 

673 
qed simp 

674 

50003  675 
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

676 
fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}" 
49774  677 
assumes f: "f \<in> borel_measurable M" 
678 
assumes g: "g \<in> borel_measurable M" 

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

50003  680 
unfolding diff_minus using assms by simp 
49774  681 

50003  682 
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

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

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

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

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

688 

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

689 
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

690 
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

691 
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

692 
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

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

694 
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

695 
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

696 
qed simp 
49774  697 

50003  698 
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

699 
fixes g f :: "'a \<Rightarrow> 'b::{second_countable_topology, metric_space}" 
49774  700 
assumes f: "f \<in> borel_measurable M" 
701 
assumes g: "g \<in> borel_measurable M" 

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

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

703 
using f g by (rule borel_measurable_continuous_Pair) (intro continuous_on_intros) 
49774  704 

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

705 
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

706 
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

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

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

709 
shows "(\<lambda>x. f x *\<^sub>R g x) \<in> borel_measurable M" 
51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51478
diff
changeset

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

711 

47694  712 
lemma affine_borel_measurable_vector: 
38656  713 
fixes f :: "'a \<Rightarrow> 'x::real_normed_vector" 
714 
assumes "f \<in> borel_measurable M" 

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

716 
proof (rule borel_measurableI) 

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

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

719 
proof cases 

720 
assume "b \<noteq> 0" 

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

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

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

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

40859  727 
ultimately show ?thesis using assms unfolding in_borel_measurable_borel 
38656  728 
by auto 
729 
qed simp 

730 
qed 

731 

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

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

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

734 
using affine_borel_measurable_vector[of f M 0 b] by simp 
38656  735 

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

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

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

738 
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

739 

50003  740 
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

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

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

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

747 
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

748 
by (intro ext) auto 
50003  749 
finally show ?thesis using f by simp 
35692  750 
qed 
751 

50003  752 
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

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

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

50003  757 
lemma borel_measurable_max[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

758 
"f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. max (g x) (f x) :: 'b::{second_countable_topology, inner_dense_linorder, linorder_topology}) \<in> borel_measurable M" 
50003  759 
by (simp add: max_def) 
38656  760 

50003  761 
lemma borel_measurable_min[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> (\<lambda>x. min (g x) (f x) :: 'b::{second_countable_topology, inner_dense_linorder, linorder_topology}) \<in> borel_measurable M" 
50003  763 
by (simp add: min_def) 
38656  764 

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

767 
unfolding abs_real_def by simp 

38656  768 

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

770 
"(\<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

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

772 

47694  773 
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

774 
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

775 
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

776 
assumes q: "convex_on A q" 
49774  777 
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

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

779 
have "(\<lambda>x. if X x \<in> A then q (X x) else 0) \<in> borel_measurable M" (is "?qX") 
49774  780 
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

781 
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

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

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

785 
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

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

787 
finally show ?thesis . 
41830  788 
qed 
789 

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

41830  793 
proof  
794 
{ fix x :: real assume x: "x \<le> 0" 

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

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

798 
note ln_imp = this 

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

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

801 
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

802 
by (auto intro!: continuous_at_imp_continuous_on DERIV_ln DERIV_isCont) 
41830  803 
show "open ({0<..}::real set)" by auto 
804 
qed 

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

41830  807 
finally show ?thesis . 
808 
qed 

809 

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

811 
"f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. log (g x) (f x)) \<in> borel_measurable M" 
49774  812 
unfolding log_def by auto 
41830  813 

50419  814 
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

815 
by (intro borel_measurable_continuous_on1 continuous_at_imp_continuous_on ballI isCont_exp) 
50419  816 

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

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

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

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

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

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

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

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

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

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

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

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

828 
unfolding measurable_def by auto 
47761  829 
qed 
830 

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

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

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

834 
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

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

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

837 
by (auto simp: vimage_def measurable_count_space_eq2_countable) 
47761  838 
qed 
839 

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

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

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

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

843 

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

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

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

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

847 

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

848 
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

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

850 

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

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

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

854 

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

855 
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

856 

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

860 

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

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

865 
proof  

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

867 
using continuous_on_real 

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

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

870 
by auto 

871 
finally show ?thesis . 

872 
qed 

873 

874 
lemma borel_measurable_ereal_cases: 

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

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

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

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

879 
proof  

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

880 
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  881 
{ 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

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

884 

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

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

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

49774  890 
by (auto simp del: abs_real_of_ereal simp: borel_measurable_ereal_cases[OF f] measurable_If) 
891 

892 
lemma borel_measurable_uminus_eq_ereal[simp]: 

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

894 
proof 

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

896 
qed auto 

897 

898 
lemma set_Collect_ereal2: 

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

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

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

902 
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

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

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

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

906 
"{x \<in> space borel. H (ereal x) (\<infinity>)} \<in> sets borel" 
49774  907 
shows "{x \<in> space M. H (f x) (g x)} \<in> sets M" 
908 
proof  

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

909 
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

910 
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  911 
{ 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

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

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

914 
by (subst *) (simp del: space_borel split del: split_if) 
49774  915 
qed 
916 

47694  917 
lemma borel_measurable_ereal_iff: 
43920  918 
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

919 
proof 
43920  920 
assume "(\<lambda>x. ereal (f x)) \<in> borel_measurable M" 
921 
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

922 
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

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

924 

47694  925 
lemma borel_measurable_ereal_iff_real: 
43923  926 
fixes f :: "'a \<Rightarrow> ereal" 
927 
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

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

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

930 
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

931 
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

932 
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  933 
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

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

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

937 
qed simp_all 
41830  938 

47694  939 
lemma borel_measurable_eq_atMost_ereal: 
43923  940 
fixes f :: "'a \<Rightarrow> ereal" 
941 
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

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

943 
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

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

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

947 
fix a :: real 
43920  948 
{ 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

949 
have "x = \<infinity>" 
43920  950 
proof (rule ereal_top) 
44666  951 
fix B from reals_Archimedean2[of B] guess n .. 
43920  952 
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

953 
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

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

955 
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

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

957 
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

958 
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

959 
moreover 
43923  960 
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

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

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

967 
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

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

970 
qed (simp add: measurable_sets) 
35582  971 

47694  972 
lemma borel_measurable_eq_atLeast_ereal: 
43920  973 
"(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

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

975 
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

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

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

980 
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

981 
qed (simp add: measurable_sets) 
35582  982 

49774  983 
lemma greater_eq_le_measurable: 
984 
fixes f :: "'a \<Rightarrow> 'c::linorder" 

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

986 
proof 

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

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

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

990 
next 

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

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

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

994 
qed 

995 

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

38656  999 

49774  1000 
lemma less_eq_ge_measurable: 
1001 
fixes f :: "'a \<Rightarrow> 'c::linorder" 

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

1003 
proof 

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

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

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

1007 
next 

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

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

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

1011 
qed 

1012 

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

38656  1016 

49774  1017 
lemma borel_measurable_ereal2: 
1018 
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

1019 
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

1020 
assumes g: "g \<in> borel_measurable M" 
49774  1021 
assumes H: "(\<lambda>x. H (ereal (real (f x))) (ereal (real (g x)))) \<in> borel_measurable M" 
1022 
"(\<lambda>x. H (\<infinity>) (ereal (real (g x)))) \<in> borel_measurable M" 

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

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

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

1026 
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

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

1028 
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

1029 
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  1030 
{ 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

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

1032 
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

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

1034 

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

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

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

1039 
using f by auto 

38656  1040 

50003  1041 
lemma [measurable(raw)]: 
43920  1042 
fixes f :: "'a \<Rightarrow> ereal" 
50003  1043 
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

1044 
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

1045 
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

1046 
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

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

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

1053 
assumes "g \<in> borel_measurable M" 

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

1054 
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

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

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

1062 
proof cases 

1063 
assume "finite S" 

1064 
thus ?thesis using assms 

1065 
by induct auto 

49774  1066 
qed simp 
38656  1067 

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

41096  1074 
thus ?thesis using assms by induct auto 
1075 
qed simp 

38656  1076 

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

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

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

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

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

1089 

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

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

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

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

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

1102 

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

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

1106 
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

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

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

1113 

1114 
lemma sets_Collect_ereal_convergent[measurable]: 

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

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

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

1118 
unfolding convergent_ereal by auto 

1119 

1120 
lemma borel_measurable_extreal_lim[measurable (raw)]: 

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

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

1123 
shows "(\<lambda>x. lim (\<lambda>i. f i x)) \<in> borel_measurable M" 

1124 
proof  

1125 
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  1126 
by (simp add: lim_def convergent_def convergent_limsup_cl) 
50003  1127 
then show ?thesis 
1128 
by simp 

1129 
qed 

1130 

49774  1131 
lemma borel_measurable_ereal_LIMSEQ: 
1132 
fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ereal" 

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

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

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

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

50003  1139 
with u show ?thesis by (simp cong: measurable_cong) 
47694  1140 
qed 
1141 

50003  1142 
lemma borel_measurable_extreal_suminf[measurable (raw)]: 
43920  1143 
fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal" 
50003  1144 
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

1145 
shows "(\<lambda>x. (\<Sum>i. f i x)) \<in> borel_measurable M" 
50003  1146 
unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp 
39092  1147 

1148 
section "LIMSEQ is borel measurable" 

1149 

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

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

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

1155 
proof  

43920  1156 
have "\<And>x. x \<in> space M \<Longrightarrow> liminf (\<lambda>n. ereal (u n x)) = ereal (u' x)" 
46731  1157 
using u' by (simp add: lim_imp_Liminf) 
43920  1158 
moreover from u have "(\<lambda>x. liminf (\<lambda>n. ereal (u n x))) \<in> borel_measurable M" 
39092  1159 
by auto 
43920  1160 
ultimately show ?thesis by (simp cong: measurable_cong add: borel_measurable_ereal_iff) 
39092  1161 
qed 
1162 

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

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

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

1167 
unfolding Cauchy_iff2 using f by auto 
49774  1168 

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

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

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

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

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

1175 
then have *: "\<And>x. lim (\<lambda>i. f i x) = (if Cauchy (\<lambda>i. f i x) then u' x else (THE x. False))" 
49774  1176 
by (auto simp: lim_def convergent_eq_cauchy[symmetric]) 
50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1177 
have "u' \<in> borel_measurable M" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1178 
proof (rule borel_measurable_LIMSEQ) 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

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

1180 
have "convergent (\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0)" 
49774  1181 
by (cases "Cauchy (\<lambda>i. f i x)") 
50002
