author  hoelzl 
Mon, 14 Jan 2013 17:29:04 +0100  
changeset 50881  ae630bab13da 
parent 50526  899c9c4e4a4c 
child 50882  a382bf90867e 
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 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

139 
show "X \<in> sigma_sets UNIV B" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

140 
proof cases 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

141 
assume "B' \<noteq> {}" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

142 
thus "X \<in> sigma_sets UNIV B" using assms B' 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

143 
by (metis from_nat_into Union_image_eq countable_subset range_from_nat_into 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

144 
in_mono sigma_sets.Basic sigma_sets.Union) 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

145 
qed (simp add: sigma_sets.Empty B') 
50087  146 
next 
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

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

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

149 
thus "b \<in> sigma_sets UNIV (Collect open)" by auto 
50087  150 
qed simp_all 
151 

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

152 
lemma borel_eq_union_closed_basis: 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

153 
"borel = sigma UNIV union_closed_basis" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

154 
by (rule borel_eq_countable_basis[OF countable_union_closed_basis basis_union_closed_basis]) 
50094
84ddcf5364b4
allow arbitrary enumerations of basis in locale for generation of borel sets
immler
parents:
50087
diff
changeset

155 

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

156 
lemma topological_basis_prod: 
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 
assumes A: "topological_basis A" and B: "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

158 
shows "topological_basis ((\<lambda>(a, b). a \<times> b) ` (A \<times> 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

159 
unfolding topological_basis_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

160 
proof (safe, simp_all del: ex_simps add: subset_image_iff ex_simps(1)[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

161 
fix S :: "('a \<times> 'b) set" assume "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

162 
then show "\<exists>X\<subseteq>A \<times> B. (\<Union>(a,b)\<in>X. a \<times> b) = 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

163 
proof (safe intro!: exI[of _ "{x\<in>A \<times> B. fst x \<times> snd x \<subseteq> 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

164 
fix x y assume "(x, y) \<in> 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

165 
from open_prod_elim[OF `open S` 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

166 
obtain a b where a: "open a""x \<in> a" and b: "open b" "y \<in> b" and "a \<times> b \<subseteq> 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

167 
by (metis mem_Sigma_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

168 
moreover from topological_basisE[OF A a] guess A0 . 
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 
moreover from topological_basisE[OF B b] guess B0 . 
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 
ultimately show "(x, y) \<in> (\<Union>(a, b)\<in>{X \<in> A \<times> B. fst X \<times> snd X \<subseteq> S}. a \<times> 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

171 
by (intro UN_I[of "(A0, B0)"]) 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

172 
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

173 
qed (metis A B topological_basis_open open_Times) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

174 

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

175 
instance prod :: (second_countable_topology, second_countable_topology) 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

176 
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

177 
obtain A :: "'a set set" where "countable A" "topological_basis 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

178 
using ex_countable_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

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

180 
obtain B :: "'b set set" where "countable B" "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

181 
using ex_countable_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

182 
ultimately show "\<exists>B::('a \<times> '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

183 
by (auto intro!: exI[of _ "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"] topological_basis_prod) 
38656  184 
qed 
185 

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

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

187 
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

188 
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

189 
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

190 
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

191 
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

192 
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

193 
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

194 
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

195 
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

196 
by (auto intro!: countable_basis topological_basis_prod is_basis) 
38656  197 

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

198 
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

199 
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

200 
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

201 
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

202 
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

203 
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

204 
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

205 
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

206 
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

207 
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

208 
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

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

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

211 

49774  212 
lemma borel_measurable_continuous_on: 
213 
fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space" 

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

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

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

217 

218 
lemma borel_measurable_continuous_on_open': 

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

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

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

222 
proof (rule borel_measurableI) 

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

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

225 
by (intro continuous_open_preimage[OF cont]) auto 

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

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

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

229 
by (auto split: split_if_asm) 

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

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

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

234 

235 
lemma borel_measurable_continuous_on_open: 

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

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

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

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

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

241 
by (simp add: comp_def) 

242 

243 
lemma continuous_on_fst: "continuous_on UNIV fst" 

244 
proof  

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

246 
show ?thesis 

247 
using closed_vimage_fst 

248 
by (auto simp: continuous_on_closed closed_closedin vimage_def) 

249 
qed 

250 

251 
lemma continuous_on_snd: "continuous_on UNIV snd" 

252 
proof  

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

254 
show ?thesis 

255 
using closed_vimage_snd 

256 
by (auto simp: continuous_on_closed closed_closedin vimage_def) 

257 
qed 

258 

259 
lemma borel_measurable_continuous_Pair: 

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

260 
fixes f :: "'a \<Rightarrow> 'b::second_countable_topology" and g :: "'a \<Rightarrow> 'c::second_countable_topology" 
50003  261 
assumes [measurable]: "f \<in> borel_measurable M" 
262 
assumes [measurable]: "g \<in> borel_measurable M" 

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

265 
proof  

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

267 
show ?thesis 

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

269 
qed 

270 

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

271 
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

272 

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_inner[measurable (raw)]: 
50881
ae630bab13da
renamed countable_basis_space to second_countable_topology
hoelzl
parents:
50526
diff
changeset

274 
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

275 
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

276 
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

277 
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

278 
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

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

280 
(intro continuous_on_inner continuous_on_snd continuous_on_fst) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

281 

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

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

283 
fixes a b :: "'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

284 
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

285 
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

286 
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

287 
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

288 
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

289 
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

290 
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

291 
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

292 
unfolding greaterThanAtMost_def atLeastLessThan_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

293 
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

294 

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 
lemma borel_measurable_less[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 
fixes f :: "'a \<Rightarrow> 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

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

298 
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

299 
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

300 
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

301 
have "{w \<in> space M. f w < g w} = {x \<in> space M. \<exists>r. f x < of_rat r \<and> of_rat r < g x}" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

302 
using Rats_dense_in_real by (auto simp add: Rats_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

303 
with f g show ?thesis 
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 
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

305 
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

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 
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 
fixes f :: "'a \<Rightarrow> 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

309 
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

310 
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

311 
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

312 
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

313 
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

314 
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

315 
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

316 

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 
lemma 
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 
shows hafspace_less_borel: "{x::'a::euclidean_space. a < x \<bullet> 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

319 
and hafspace_greater_borel: "{x::'a::euclidean_space. x \<bullet> i < 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

320 
and hafspace_less_eq_borel: "{x::'a::euclidean_space. a \<le> x \<bullet> 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

321 
and hafspace_greater_eq_borel: "{x::'a::euclidean_space. x \<bullet> i \<le> 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

322 
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

323 

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

325 

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

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

328 
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

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

331 
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

332 
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

333 
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

334 
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

335 
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

336 
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

337 
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

338 
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

339 
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

340 
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

341 
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

342 
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

343 
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

344 
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

345 
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

346 
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

347 
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

348 

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

350 
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

351 
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

352 
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

353 
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

354 
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

355 
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

356 
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

357 
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

358 

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

360 
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

361 
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

362 
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

363 
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

364 
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

365 
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

366 

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

368 
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

369 
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

370 
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

371 
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

372 
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

373 
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

374 
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

375 

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

377 
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

378 
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

379 
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

380 
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

381 
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

382 
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

383 

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

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

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

387 
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

388 
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

389 
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

390 
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

391 
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

392 
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

393 
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

394 
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

395 
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

396 

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

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

399 
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

400 
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

401 

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

403 
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

404 
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

405 
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

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

407 
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

408 
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

409 
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

410 
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

411 
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

412 
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

413 
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

414 
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

415 
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

416 
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

417 
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

418 
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

419 
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

420 
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

421 
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

422 
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

423 
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

424 
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

425 
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

426 
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

427 

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

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

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

431 
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

432 
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

433 
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

434 
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

435 
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

436 
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

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

438 
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

439 
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

440 

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

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

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

444 
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

445 
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

446 
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

447 
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

448 
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

449 
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

450 
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

451 
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

452 
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

453 
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

454 
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

455 
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

456 
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

457 
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

458 
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

459 
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

460 
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

461 
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

462 
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

463 
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

464 

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

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

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

468 
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

469 
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

470 
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

471 
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

472 
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

473 
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

474 

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

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

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

478 
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

479 
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

480 
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

481 
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

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

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

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

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

493 
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

494 
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

495 
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

496 
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

497 
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

498 
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

499 
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

500 
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

501 
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

502 
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

503 
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

504 

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

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

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

508 
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

509 
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

510 
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

511 
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

512 
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

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

514 
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

515 
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

516 
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

517 
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

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

519 
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

520 
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

521 
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

522 
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

523 
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

524 
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

525 
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

526 
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

527 
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

528 
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

529 
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

530 
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

531 

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

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

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

535 
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

536 
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

537 
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

538 
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

539 
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

540 
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

541 
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

542 
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

543 
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

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

545 
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

546 
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

547 
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

548 
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

549 
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

550 
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

551 
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

552 
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

553 
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

554 
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

555 
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

556 
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

557 

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

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

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

561 
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

562 
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

563 
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

564 
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

565 
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

566 
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

567 
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

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

569 
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

570 
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

571 
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

572 
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

573 
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

574 
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

575 
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

576 
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

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

578 
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

579 

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

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

582 
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

583 
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

584 
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

585 
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

586 
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

587 
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

588 
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

589 
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

590 

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

592 
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

593 
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

594 
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

595 
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

596 
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

597 
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

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

599 
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

600 
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

601 
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

602 
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

603 
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

604 
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

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

606 
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

607 
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

608 

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

610 
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

611 
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

612 
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

613 
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

614 
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

615 
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

616 
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

617 
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

618 
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

619 
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

620 
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

621 
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

622 
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

623 

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

625 
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

626 
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

627 
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

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

630 
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

631 
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

632 
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

633 

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

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

635 
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

636 
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

637 
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

638 

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

640 
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

641 
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

642 
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

643 

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

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

646 
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

647 

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

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

650 
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

651 

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

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

654 
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

655 
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

656 

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

657 
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

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

659 
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

660 

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

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

662 
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

663 
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

664 
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

665 
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

666 
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

667 
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

668 
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

669 

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

670 
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

671 

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

672 
lemma borel_measurable_uminus[measurable (raw)]: 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50419
diff
changeset

673 
fixes g :: "'a \<Rightarrow> 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

674 
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

675 
shows "(\<lambda>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

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

677 

50003  678 
lemma borel_measurable_add[measurable (raw)]: 
49774  679 
fixes f g :: "'a \<Rightarrow> 'c::ordered_euclidean_space" 
680 
assumes f: "f \<in> borel_measurable M" 

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

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

683 
using f g 

684 
by (rule borel_measurable_continuous_Pair) 

685 
(auto intro: continuous_on_fst continuous_on_snd continuous_on_add) 

686 

50003  687 
lemma borel_measurable_setsum[measurable (raw)]: 
49774  688 
fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real" 
689 
assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M" 

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

691 
proof cases 

692 
assume "finite S" 

693 
thus ?thesis using assms by induct auto 

694 
qed simp 

695 

50003  696 
lemma borel_measurable_diff[measurable (raw)]: 
49774  697 
fixes f :: "'a \<Rightarrow> real" 
698 
assumes f: "f \<in> borel_measurable M" 

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

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

50003  701 
unfolding diff_minus using assms by simp 
49774  702 

50003  703 
lemma borel_measurable_times[measurable (raw)]: 
49774  704 
fixes f :: "'a \<Rightarrow> real" 
705 
assumes f: "f \<in> borel_measurable M" 

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

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

708 
using f g 

709 
by (rule borel_measurable_continuous_Pair) 

710 
(auto intro: continuous_on_fst continuous_on_snd continuous_on_mult) 

711 

712 
lemma continuous_on_dist: 

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

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

715 
unfolding continuous_on_eq_continuous_within by (auto simp: continuous_dist) 

716 

50003  717 
lemma borel_measurable_dist[measurable (raw)]: 
49774  718 
fixes g f :: "'a \<Rightarrow> 'b::ordered_euclidean_space" 
719 
assumes f: "f \<in> borel_measurable M" 

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

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

722 
using f g 

723 
by (rule borel_measurable_continuous_Pair) 

724 
(intro continuous_on_dist continuous_on_fst continuous_on_snd) 

725 

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

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

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

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

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

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

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

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

733 

47694  734 
lemma affine_borel_measurable_vector: 
38656  735 
fixes f :: "'a \<Rightarrow> 'x::real_normed_vector" 
736 
assumes "f \<in> borel_measurable M" 

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

738 
proof (rule borel_measurableI) 

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

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

741 
proof cases 

742 
assume "b \<noteq> 0" 

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

743 
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

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

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

40859  749 
ultimately show ?thesis using assms unfolding in_borel_measurable_borel 
38656  750 
by auto 
751 
qed simp 

752 
qed 

753 

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

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

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

756 
using affine_borel_measurable_vector[of f M 0 b] by simp 
38656  757 

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

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

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

760 
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

761 

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

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

764 
assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M" 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41025
diff
changeset

765 
shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M" 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41025
diff
changeset

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

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

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

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

770 

50003  771 
lemma borel_measurable_inverse[measurable (raw)]: 
38656  772 
fixes f :: "'a \<Rightarrow> real" 
49774  773 
assumes f: "f \<in> borel_measurable M" 
35692  774 
shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M" 
49774  775 
proof  
50003  776 
have "(\<lambda>x::real. if x \<in> UNIV  {0} then inverse x else 0) \<in> borel_measurable borel" 
777 
by (intro borel_measurable_continuous_on_open' continuous_on_inverse continuous_on_id) auto 

778 
also have "(\<lambda>x::real. if x \<in> UNIV  {0} then inverse x else 0) = inverse" by (intro ext) auto 

779 
finally show ?thesis using f by simp 

35692  780 
qed 
781 

50003  782 
lemma borel_measurable_divide[measurable (raw)]: 
783 
"f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. f x / g x::real) \<in> borel_measurable M" 

784 
by (simp add: field_divide_inverse) 

38656  785 

50003  786 
lemma borel_measurable_max[measurable (raw)]: 
787 
"f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. max (g x) (f x) :: real) \<in> borel_measurable M" 

788 
by (simp add: max_def) 

38656  789 

50003  790 
lemma borel_measurable_min[measurable (raw)]: 
791 
"f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. min (g x) (f x) :: real) \<in> borel_measurable M" 

792 
by (simp add: min_def) 

38656  793 

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

796 
unfolding abs_real_def by simp 

38656  797 

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

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

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

801 

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

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

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

805 
assumes q: "convex_on { a <..< b} q" 
49774  806 
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

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

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

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

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

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

814 
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

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

816 
finally show ?thesis . 
41830  817 
qed 
818 

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

41830  822 
proof  
823 
{ fix x :: real assume x: "x \<le> 0" 

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

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

827 
note ln_imp = this 

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

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

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

831 
by (auto intro!: continuous_at_imp_continuous_on DERIV_ln DERIV_isCont 

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

834 
qed 

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

41830  837 
finally show ?thesis . 
838 
qed 

839 

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

841 
"f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. log (g x) (f x)) \<in> borel_measurable M" 
49774  842 
unfolding log_def by auto 
41830  843 

50419  844 
lemma borel_measurable_exp[measurable]: "exp \<in> borel_measurable borel" 
845 
by (intro borel_measurable_continuous_on1 continuous_at_imp_continuous_on ballI 

846 
continuous_isCont[THEN iffD1] isCont_exp) 

847 

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

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

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

850 
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

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

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

853 
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

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

855 
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

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

857 
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

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

859 
unfolding measurable_def by auto 
47761  860 
qed 
861 

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

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

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

865 
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

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

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

868 
by (auto simp: vimage_def measurable_count_space_eq2_countable) 
47761  869 
qed 
870 

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

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

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

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

874 

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

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

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

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

878 

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

879 
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

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

881 

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

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

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

885 

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

886 
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

887 

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

891 

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

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

896 
proof  

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

898 
using continuous_on_real 

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

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

901 
by auto 

902 
finally show ?thesis . 

903 
qed 

904 

905 
lemma borel_measurable_ereal_cases: 

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

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

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

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

910 
proof  

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

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

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

915 

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

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

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

49774  921 
by (auto simp del: abs_real_of_ereal simp: borel_measurable_ereal_cases[OF f] measurable_If) 
922 

923 
lemma borel_measurable_uminus_eq_ereal[simp]: 

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

925 
proof 

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

927 
qed auto 

928 

929 
lemma set_Collect_ereal2: 

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

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

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

933 
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

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

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

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

937 
"{x \<in> space borel. H (ereal x) (\<infinity>)} \<in> sets borel" 
49774  938 
shows "{x \<in> space M. H (f x) (g x)} \<in> sets M" 
939 
proof  

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

940 
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

941 
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  942 
{ 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

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

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

945 
by (subst *) (simp del: space_borel split del: split_if) 
49774  946 
qed 
947 

50003  948 
lemma [measurable]: 
49774  949 
fixes f g :: "'a \<Rightarrow> ereal" 
950 
assumes f: "f \<in> borel_measurable M" 

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

50003  952 
shows borel_measurable_ereal_le: "{x \<in> space M. f x \<le> g x} \<in> sets M" 
953 
and borel_measurable_ereal_less: "{x \<in> space M. f x < g x} \<in> sets M" 

954 
and borel_measurable_ereal_eq: "{w \<in> space M. f w = g w} \<in> sets M" 

955 
using f g by (simp_all add: set_Collect_ereal2) 

956 

957 
lemma borel_measurable_ereal_neq: 

958 
"f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> {w \<in> space M. f w \<noteq> (g w :: ereal)} \<in> sets M" 

959 
by simp 

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

960 

47694  961 
lemma borel_measurable_ereal_iff: 
43920  962 
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

963 
proof 
43920  964 
assume "(\<lambda>x. ereal (f x)) \<in> borel_measurable M" 
965 
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

966 
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

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

968 

47694  969 
lemma borel_measurable_ereal_iff_real: 
43923  970 
fixes f :: "'a \<Rightarrow> ereal" 
971 
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

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

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

974 
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

975 
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

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

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

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

981 
qed simp_all 
41830  982 

47694  983 
lemma borel_measurable_eq_atMost_ereal: 
43923  984 
fixes f :: "'a \<Rightarrow> ereal" 
985 
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

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

987 
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

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

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

991 
fix a :: real 
43920  992 
{ 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

993 
have "x = \<infinity>" 
43920  994 
proof (rule ereal_top) 
44666  995 
fix B from reals_Archimedean2[of B] guess n .. 
43920  996 
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

997 
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

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

999 
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

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

1001 
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

1002 
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

1003 
moreover 
43923  1004 
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

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

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

1011 
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

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

1014 
qed (simp add: measurable_sets) 
35582  1015 

47694  1016 
lemma borel_measurable_eq_atLeast_ereal: 
43920  1017 
"(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

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

1019 
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

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

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

1024 
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

1025 
qed (simp add: measurable_sets) 
35582  1026 

49774  1027 
lemma greater_eq_le_measurable: 
1028 
fixes f :: "'a \<Rightarrow> 'c::linorder" 

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

1030 
proof 

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

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

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

1034 
next 

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

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

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

1038 
qed 

1039 

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

38656  1043 

49774  1044 
lemma less_eq_ge_measurable: 
1045 
fixes f :: "'a \<Rightarrow> 'c::linorder" 

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

1047 
proof 

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

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

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

1051 
next 

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

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

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

1055 
qed 

1056 

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

38656  1060 

49774  1061 
lemma borel_measurable_ereal2: 
1062 
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

1063 
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

1064 
assumes g: "g \<in> borel_measurable M" 
49774  1065 
assumes H: "(\<lambda>x. H (ereal (real (f x))) (ereal (real (g x)))) \<in> borel_measurable M" 
1066 
"(\<lambda>x. H (\<infinity>) (ereal (real (g x)))) \<in> borel_measurable M" 

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

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

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

1070 
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

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

1072 
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

1073 
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  1074 
{ 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

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

1076 
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

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

1078 

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

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

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

1083 
using f by auto 

38656  1084 

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

1088 
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

1089 
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

1090 
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

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

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

1097 
assumes "g \<in> borel_measurable M" 

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

1098 
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

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

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

1106 
proof cases 

1107 
assume "finite S" 

1108 
thus ?thesis using assms 

1109 
by induct auto 

49774  1110 
qed simp 
38656  1111 

50003  1112 
lemma borel_measurable_ereal_setprod[measurable (raw)]: 
43920  1113 
fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal" 
38656  1114 
assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M" 
41096  1115 
shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M" 
38656  1116 
proof cases 
1117 
assume "finite S" 

41096  1118 
thus ?thesis using assms by induct auto 
1119 
qed simp 

38656  1120 

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

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

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

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

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

1133 

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

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

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

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

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

1146 

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

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

1150 
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

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

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

1157 

1158 
lemma sets_Collect_ereal_convergent[measurable]: 

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

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

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

1162 
unfolding convergent_ereal by auto 

1163 

1164 
lemma borel_measurable_extreal_lim[measurable (raw)]: 

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

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

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

1168 
proof  

1169 
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))" 

1170 
using convergent_ereal_limsup by (simp add: lim_def convergent_def) 

1171 
then show ?thesis 

1172 
by simp 

1173 
qed 

1174 

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

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

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

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

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

50003  1183 
with u show ?thesis by (simp cong: measurable_cong) 
47694  1184 
qed 
1185 

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

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

1192 
section "LIMSEQ is borel measurable" 

1193 

47694  1194 
lemma borel_measurable_LIMSEQ: 