1 (* Title: HOL/Analysis/Borel_Space.thy |
1 (* Title: HOL/Analysis/Borel_Space.thy |
2 Author: Johannes Hölzl, TU München |
2 Author: Johannes Hölzl, TU München |
3 Author: Armin Heller, TU München |
3 Author: Armin Heller, TU München |
4 *) |
4 *) |
5 |
5 |
6 section \<open>Borel spaces\<close> |
6 section%important \<open>Borel spaces\<close> |
7 |
7 |
8 theory Borel_Space |
8 theory Borel_Space |
9 imports |
9 imports |
10 Measurable Derivative Ordered_Euclidean_Space Extended_Real_Limits |
10 Measurable Derivative Ordered_Euclidean_Space Extended_Real_Limits |
11 begin |
11 begin |
12 |
12 |
13 lemma sets_Collect_eventually_sequentially[measurable]: |
13 lemma%unimportant sets_Collect_eventually_sequentially[measurable]: |
14 "(\<And>i. {x\<in>space M. P x i} \<in> sets M) \<Longrightarrow> {x\<in>space M. eventually (P x) sequentially} \<in> sets M" |
14 "(\<And>i. {x\<in>space M. P x i} \<in> sets M) \<Longrightarrow> {x\<in>space M. eventually (P x) sequentially} \<in> sets M" |
15 unfolding eventually_sequentially by simp |
15 unfolding eventually_sequentially by simp |
16 |
16 |
17 lemma topological_basis_trivial: "topological_basis {A. open A}" |
17 lemma%unimportant topological_basis_trivial: "topological_basis {A. open A}" |
18 by (auto simp: topological_basis_def) |
18 by (auto simp: topological_basis_def) |
19 |
19 |
20 lemma open_prod_generated: "open = generate_topology {A \<times> B | A B. open A \<and> open B}" |
20 lemma%important open_prod_generated: "open = generate_topology {A \<times> B | A B. open A \<and> open B}" |
21 proof - |
21 proof%unimportant - |
22 have "{A \<times> B :: ('a \<times> 'b) set | A B. open A \<and> open B} = ((\<lambda>(a, b). a \<times> b) ` ({A. open A} \<times> {A. open A}))" |
22 have "{A \<times> B :: ('a \<times> 'b) set | A B. open A \<and> open B} = ((\<lambda>(a, b). a \<times> b) ` ({A. open A} \<times> {A. open A}))" |
23 by auto |
23 by auto |
24 then show ?thesis |
24 then show ?thesis |
25 by (auto intro: topological_basis_prod topological_basis_trivial topological_basis_imp_subbasis) |
25 by (auto intro: topological_basis_prod topological_basis_trivial topological_basis_imp_subbasis) |
26 qed |
26 qed |
27 |
27 |
28 definition "mono_on f A \<equiv> \<forall>r s. r \<in> A \<and> s \<in> A \<and> r \<le> s \<longrightarrow> f r \<le> f s" |
28 definition%important "mono_on f A \<equiv> \<forall>r s. r \<in> A \<and> s \<in> A \<and> r \<le> s \<longrightarrow> f r \<le> f s" |
29 |
29 |
30 lemma mono_onI: |
30 lemma%unimportant mono_onI: |
31 "(\<And>r s. r \<in> A \<Longrightarrow> s \<in> A \<Longrightarrow> r \<le> s \<Longrightarrow> f r \<le> f s) \<Longrightarrow> mono_on f A" |
31 "(\<And>r s. r \<in> A \<Longrightarrow> s \<in> A \<Longrightarrow> r \<le> s \<Longrightarrow> f r \<le> f s) \<Longrightarrow> mono_on f A" |
32 unfolding mono_on_def by simp |
32 unfolding mono_on_def by simp |
33 |
33 |
34 lemma mono_onD: |
34 lemma%unimportant mono_onD: |
35 "\<lbrakk>mono_on f A; r \<in> A; s \<in> A; r \<le> s\<rbrakk> \<Longrightarrow> f r \<le> f s" |
35 "\<lbrakk>mono_on f A; r \<in> A; s \<in> A; r \<le> s\<rbrakk> \<Longrightarrow> f r \<le> f s" |
36 unfolding mono_on_def by simp |
36 unfolding mono_on_def by simp |
37 |
37 |
38 lemma mono_imp_mono_on: "mono f \<Longrightarrow> mono_on f A" |
38 lemma%unimportant mono_imp_mono_on: "mono f \<Longrightarrow> mono_on f A" |
39 unfolding mono_def mono_on_def by auto |
39 unfolding mono_def mono_on_def by auto |
40 |
40 |
41 lemma mono_on_subset: "mono_on f A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> mono_on f B" |
41 lemma%unimportant mono_on_subset: "mono_on f A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> mono_on f B" |
42 unfolding mono_on_def by auto |
42 unfolding mono_on_def by auto |
43 |
43 |
44 definition "strict_mono_on f A \<equiv> \<forall>r s. r \<in> A \<and> s \<in> A \<and> r < s \<longrightarrow> f r < f s" |
44 definition%important "strict_mono_on f A \<equiv> \<forall>r s. r \<in> A \<and> s \<in> A \<and> r < s \<longrightarrow> f r < f s" |
45 |
45 |
46 lemma strict_mono_onI: |
46 lemma%unimportant strict_mono_onI: |
47 "(\<And>r s. r \<in> A \<Longrightarrow> s \<in> A \<Longrightarrow> r < s \<Longrightarrow> f r < f s) \<Longrightarrow> strict_mono_on f A" |
47 "(\<And>r s. r \<in> A \<Longrightarrow> s \<in> A \<Longrightarrow> r < s \<Longrightarrow> f r < f s) \<Longrightarrow> strict_mono_on f A" |
48 unfolding strict_mono_on_def by simp |
48 unfolding strict_mono_on_def by simp |
49 |
49 |
50 lemma strict_mono_onD: |
50 lemma%unimportant strict_mono_onD: |
51 "\<lbrakk>strict_mono_on f A; r \<in> A; s \<in> A; r < s\<rbrakk> \<Longrightarrow> f r < f s" |
51 "\<lbrakk>strict_mono_on f A; r \<in> A; s \<in> A; r < s\<rbrakk> \<Longrightarrow> f r < f s" |
52 unfolding strict_mono_on_def by simp |
52 unfolding strict_mono_on_def by simp |
53 |
53 |
54 lemma mono_on_greaterD: |
54 lemma%unimportant mono_on_greaterD: |
55 assumes "mono_on g A" "x \<in> A" "y \<in> A" "g x > (g (y::_::linorder) :: _ :: linorder)" |
55 assumes "mono_on g A" "x \<in> A" "y \<in> A" "g x > (g (y::_::linorder) :: _ :: linorder)" |
56 shows "x > y" |
56 shows "x > y" |
57 proof (rule ccontr) |
57 proof (rule ccontr) |
58 assume "\<not>x > y" |
58 assume "\<not>x > y" |
59 hence "x \<le> y" by (simp add: not_less) |
59 hence "x \<le> y" by (simp add: not_less) |
60 from assms(1-3) and this have "g x \<le> g y" by (rule mono_onD) |
60 from assms(1-3) and this have "g x \<le> g y" by (rule mono_onD) |
61 with assms(4) show False by simp |
61 with assms(4) show False by simp |
62 qed |
62 qed |
63 |
63 |
64 lemma strict_mono_inv: |
64 lemma%unimportant strict_mono_inv: |
65 fixes f :: "('a::linorder) \<Rightarrow> ('b::linorder)" |
65 fixes f :: "('a::linorder) \<Rightarrow> ('b::linorder)" |
66 assumes "strict_mono f" and "surj f" and inv: "\<And>x. g (f x) = x" |
66 assumes "strict_mono f" and "surj f" and inv: "\<And>x. g (f x) = x" |
67 shows "strict_mono g" |
67 shows "strict_mono g" |
68 proof |
68 proof |
69 fix x y :: 'b assume "x < y" |
69 fix x y :: 'b assume "x < y" |
70 from \<open>surj f\<close> obtain x' y' where [simp]: "x = f x'" "y = f y'" by blast |
70 from \<open>surj f\<close> obtain x' y' where [simp]: "x = f x'" "y = f y'" by blast |
71 with \<open>x < y\<close> and \<open>strict_mono f\<close> have "x' < y'" by (simp add: strict_mono_less) |
71 with \<open>x < y\<close> and \<open>strict_mono f\<close> have "x' < y'" by (simp add: strict_mono_less) |
72 with inv show "g x < g y" by simp |
72 with inv show "g x < g y" by simp |
73 qed |
73 qed |
74 |
74 |
75 lemma strict_mono_on_imp_inj_on: |
75 lemma%unimportant strict_mono_on_imp_inj_on: |
76 assumes "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> (_ :: preorder)) A" |
76 assumes "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> (_ :: preorder)) A" |
77 shows "inj_on f A" |
77 shows "inj_on f A" |
78 proof (rule inj_onI) |
78 proof (rule inj_onI) |
79 fix x y assume "x \<in> A" "y \<in> A" "f x = f y" |
79 fix x y assume "x \<in> A" "y \<in> A" "f x = f y" |
80 thus "x = y" |
80 thus "x = y" |
81 by (cases x y rule: linorder_cases) |
81 by (cases x y rule: linorder_cases) |
82 (auto dest: strict_mono_onD[OF assms, of x y] strict_mono_onD[OF assms, of y x]) |
82 (auto dest: strict_mono_onD[OF assms, of x y] strict_mono_onD[OF assms, of y x]) |
83 qed |
83 qed |
84 |
84 |
85 lemma strict_mono_on_leD: |
85 lemma%unimportant strict_mono_on_leD: |
86 assumes "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) A" "x \<in> A" "y \<in> A" "x \<le> y" |
86 assumes "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) A" "x \<in> A" "y \<in> A" "x \<le> y" |
87 shows "f x \<le> f y" |
87 shows "f x \<le> f y" |
88 proof (insert le_less_linear[of y x], elim disjE) |
88 proof (insert le_less_linear[of y x], elim disjE) |
89 assume "x < y" |
89 assume "x < y" |
90 with assms have "f x < f y" by (rule_tac strict_mono_onD[OF assms(1)]) simp_all |
90 with assms have "f x < f y" by (rule_tac strict_mono_onD[OF assms(1)]) simp_all |
91 thus ?thesis by (rule less_imp_le) |
91 thus ?thesis by (rule less_imp_le) |
92 qed (insert assms, simp) |
92 qed (insert assms, simp) |
93 |
93 |
94 lemma strict_mono_on_eqD: |
94 lemma%unimportant strict_mono_on_eqD: |
95 fixes f :: "(_ :: linorder) \<Rightarrow> (_ :: preorder)" |
95 fixes f :: "(_ :: linorder) \<Rightarrow> (_ :: preorder)" |
96 assumes "strict_mono_on f A" "f x = f y" "x \<in> A" "y \<in> A" |
96 assumes "strict_mono_on f A" "f x = f y" "x \<in> A" "y \<in> A" |
97 shows "y = x" |
97 shows "y = x" |
98 using assms by (rule_tac linorder_cases[of x y]) (auto dest: strict_mono_onD) |
98 using assms by (rule_tac linorder_cases[of x y]) (auto dest: strict_mono_onD) |
99 |
99 |
100 lemma mono_on_imp_deriv_nonneg: |
100 lemma%important mono_on_imp_deriv_nonneg: |
101 assumes mono: "mono_on f A" and deriv: "(f has_real_derivative D) (at x)" |
101 assumes mono: "mono_on f A" and deriv: "(f has_real_derivative D) (at x)" |
102 assumes "x \<in> interior A" |
102 assumes "x \<in> interior A" |
103 shows "D \<ge> 0" |
103 shows "D \<ge> 0" |
104 proof (rule tendsto_lowerbound) |
104 proof%unimportant (rule tendsto_lowerbound) |
105 let ?A' = "(\<lambda>y. y - x) ` interior A" |
105 let ?A' = "(\<lambda>y. y - x) ` interior A" |
106 from deriv show "((\<lambda>h. (f (x + h) - f x) / h) \<longlongrightarrow> D) (at 0)" |
106 from deriv show "((\<lambda>h. (f (x + h) - f x) / h) \<longlongrightarrow> D) (at 0)" |
107 by (simp add: field_has_derivative_at has_field_derivative_def) |
107 by (simp add: field_has_derivative_at has_field_derivative_def) |
108 from mono have mono': "mono_on f (interior A)" by (rule mono_on_subset) (rule interior_subset) |
108 from mono have mono': "mono_on f (interior A)" by (rule mono_on_subset) (rule interior_subset) |
109 |
109 |
194 qed |
194 qed |
195 thus ?thesis |
195 thus ?thesis |
196 by (rule countableI') |
196 by (rule countableI') |
197 qed |
197 qed |
198 |
198 |
199 lemma mono_on_ctble_discont_open: |
199 lemma%important mono_on_ctble_discont_open: |
200 fixes f :: "real \<Rightarrow> real" |
200 fixes f :: "real \<Rightarrow> real" |
201 fixes A :: "real set" |
201 fixes A :: "real set" |
202 assumes "open A" "mono_on f A" |
202 assumes "open A" "mono_on f A" |
203 shows "countable {a\<in>A. \<not>isCont f a}" |
203 shows "countable {a\<in>A. \<not>isCont f a}" |
204 proof - |
204 proof%unimportant - |
205 have "{a\<in>A. \<not>isCont f a} = {a\<in>A. \<not>(continuous (at a within A) f)}" |
205 have "{a\<in>A. \<not>isCont f a} = {a\<in>A. \<not>(continuous (at a within A) f)}" |
206 by (auto simp add: continuous_within_open [OF _ \<open>open A\<close>]) |
206 by (auto simp add: continuous_within_open [OF _ \<open>open A\<close>]) |
207 thus ?thesis |
207 thus ?thesis |
208 apply (elim ssubst) |
208 apply (elim ssubst) |
209 by (rule mono_on_ctble_discont, rule assms) |
209 by (rule mono_on_ctble_discont, rule assms) |
210 qed |
210 qed |
211 |
211 |
212 lemma mono_ctble_discont: |
212 lemma%important mono_ctble_discont: |
213 fixes f :: "real \<Rightarrow> real" |
213 fixes f :: "real \<Rightarrow> real" |
214 assumes "mono f" |
214 assumes "mono f" |
215 shows "countable {a. \<not> isCont f a}" |
215 shows "countable {a. \<not> isCont f a}" |
216 using assms mono_on_ctble_discont [of f UNIV] unfolding mono_on_def mono_def by auto |
216 using%unimportant assms mono_on_ctble_discont [of f UNIV] unfolding mono_on_def mono_def by auto |
217 |
217 |
218 lemma has_real_derivative_imp_continuous_on: |
218 lemma%important has_real_derivative_imp_continuous_on: |
219 assumes "\<And>x. x \<in> A \<Longrightarrow> (f has_real_derivative f' x) (at x)" |
219 assumes "\<And>x. x \<in> A \<Longrightarrow> (f has_real_derivative f' x) (at x)" |
220 shows "continuous_on A f" |
220 shows "continuous_on A f" |
221 apply (intro differentiable_imp_continuous_on, unfold differentiable_on_def) |
221 apply (intro differentiable_imp_continuous_on, unfold differentiable_on_def) |
222 apply (intro ballI Deriv.differentiableI) |
222 apply (intro ballI Deriv.differentiableI) |
223 apply (rule has_field_derivative_subset[OF assms]) |
223 apply (rule has_field_derivative_subset[OF assms]) |
224 apply simp_all |
224 apply simp_all |
225 done |
225 done |
226 |
226 |
227 lemma closure_contains_Sup: |
227 lemma%important closure_contains_Sup: |
228 fixes S :: "real set" |
228 fixes S :: "real set" |
229 assumes "S \<noteq> {}" "bdd_above S" |
229 assumes "S \<noteq> {}" "bdd_above S" |
230 shows "Sup S \<in> closure S" |
230 shows "Sup S \<in> closure S" |
231 proof- |
231 proof%unimportant - |
232 have "Inf (uminus ` S) \<in> closure (uminus ` S)" |
232 have "Inf (uminus ` S) \<in> closure (uminus ` S)" |
233 using assms by (intro closure_contains_Inf) auto |
233 using assms by (intro closure_contains_Inf) auto |
234 also have "Inf (uminus ` S) = -Sup S" by (simp add: Inf_real_def) |
234 also have "Inf (uminus ` S) = -Sup S" by (simp add: Inf_real_def) |
235 also have "closure (uminus ` S) = uminus ` closure S" |
235 also have "closure (uminus ` S) = uminus ` closure S" |
236 by (rule sym, intro closure_injective_linear_image) (auto intro: linearI) |
236 by (rule sym, intro closure_injective_linear_image) (auto intro: linearI) |
237 finally show ?thesis by auto |
237 finally show ?thesis by auto |
238 qed |
238 qed |
239 |
239 |
240 lemma closed_contains_Sup: |
240 lemma%unimportant closed_contains_Sup: |
241 fixes S :: "real set" |
241 fixes S :: "real set" |
242 shows "S \<noteq> {} \<Longrightarrow> bdd_above S \<Longrightarrow> closed S \<Longrightarrow> Sup S \<in> S" |
242 shows "S \<noteq> {} \<Longrightarrow> bdd_above S \<Longrightarrow> closed S \<Longrightarrow> Sup S \<in> S" |
243 by (subst closure_closed[symmetric], assumption, rule closure_contains_Sup) |
243 by (subst closure_closed[symmetric], assumption, rule closure_contains_Sup) |
244 |
244 |
245 lemma closed_subset_contains_Sup: |
245 lemma%unimportant closed_subset_contains_Sup: |
246 fixes A C :: "real set" |
246 fixes A C :: "real set" |
247 shows "closed C \<Longrightarrow> A \<subseteq> C \<Longrightarrow> A \<noteq> {} \<Longrightarrow> bdd_above A \<Longrightarrow> Sup A \<in> C" |
247 shows "closed C \<Longrightarrow> A \<subseteq> C \<Longrightarrow> A \<noteq> {} \<Longrightarrow> bdd_above A \<Longrightarrow> Sup A \<in> C" |
248 by (metis closure_contains_Sup closure_minimal subset_eq) |
248 by (metis closure_contains_Sup closure_minimal subset_eq) |
249 |
249 |
250 lemma deriv_nonneg_imp_mono: |
250 lemma%important deriv_nonneg_imp_mono: |
251 assumes deriv: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)" |
251 assumes deriv: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)" |
252 assumes nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0" |
252 assumes nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0" |
253 assumes ab: "a \<le> b" |
253 assumes ab: "a \<le> b" |
254 shows "g a \<le> g b" |
254 shows "g a \<le> g b" |
255 proof (cases "a < b") |
255 proof%unimportant (cases "a < b") |
256 assume "a < b" |
256 assume "a < b" |
257 from deriv have "\<And>x. \<lbrakk>x \<ge> a; x \<le> b\<rbrakk> \<Longrightarrow> (g has_real_derivative g' x) (at x)" by simp |
257 from deriv have "\<And>x. \<lbrakk>x \<ge> a; x \<le> b\<rbrakk> \<Longrightarrow> (g has_real_derivative g' x) (at x)" by simp |
258 with MVT2[OF \<open>a < b\<close>] and deriv |
258 with MVT2[OF \<open>a < b\<close>] and deriv |
259 obtain \<xi> where \<xi>_ab: "\<xi> > a" "\<xi> < b" and g_ab: "g b - g a = (b - a) * g' \<xi>" by blast |
259 obtain \<xi> where \<xi>_ab: "\<xi> > a" "\<xi> < b" and g_ab: "g b - g a = (b - a) * g' \<xi>" by blast |
260 from \<xi>_ab ab nonneg have "(b - a) * g' \<xi> \<ge> 0" by simp |
260 from \<xi>_ab ab nonneg have "(b - a) * g' \<xi> \<ge> 0" by simp |
261 with g_ab show ?thesis by simp |
261 with g_ab show ?thesis by simp |
262 qed (insert ab, simp) |
262 qed (insert ab, simp) |
263 |
263 |
264 lemma continuous_interval_vimage_Int: |
264 lemma%important continuous_interval_vimage_Int: |
265 assumes "continuous_on {a::real..b} g" and mono: "\<And>x y. a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b \<Longrightarrow> g x \<le> g y" |
265 assumes "continuous_on {a::real..b} g" and mono: "\<And>x y. a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b \<Longrightarrow> g x \<le> g y" |
266 assumes "a \<le> b" "(c::real) \<le> d" "{c..d} \<subseteq> {g a..g b}" |
266 assumes "a \<le> b" "(c::real) \<le> d" "{c..d} \<subseteq> {g a..g b}" |
267 obtains c' d' where "{a..b} \<inter> g -` {c..d} = {c'..d'}" "c' \<le> d'" "g c' = c" "g d' = d" |
267 obtains c' d' where "{a..b} \<inter> g -` {c..d} = {c'..d'}" "c' \<le> d'" "g c' = c" "g d' = d" |
268 proof- |
268 proof%unimportant- |
269 let ?A = "{a..b} \<inter> g -` {c..d}" |
269 let ?A = "{a..b} \<inter> g -` {c..d}" |
270 from IVT'[of g a c b, OF _ _ \<open>a \<le> b\<close> assms(1)] assms(4,5) |
270 from IVT'[of g a c b, OF _ _ \<open>a \<le> b\<close> assms(1)] assms(4,5) |
271 obtain c'' where c'': "c'' \<in> ?A" "g c'' = c" by auto |
271 obtain c'' where c'': "c'' \<in> ?A" "g c'' = c" by auto |
272 from IVT'[of g a d b, OF _ _ \<open>a \<le> b\<close> assms(1)] assms(4,5) |
272 from IVT'[of g a d b, OF _ _ \<open>a \<le> b\<close> assms(1)] assms(4,5) |
273 obtain d'' where d'': "d'' \<in> ?A" "g d'' = d" by auto |
273 obtain d'' where d'': "d'' \<in> ?A" "g d'' = d" by auto |
295 done |
295 done |
296 with c'd'_in_set have "g c' = c" "g d' = d" by auto |
296 with c'd'_in_set have "g c' = c" "g d' = d" by auto |
297 ultimately show ?thesis using that by blast |
297 ultimately show ?thesis using that by blast |
298 qed |
298 qed |
299 |
299 |
300 subsection \<open>Generic Borel spaces\<close> |
300 subsection%important \<open>Generic Borel spaces\<close> |
301 |
301 |
302 definition (in topological_space) borel :: "'a measure" where |
302 definition%important (in topological_space) borel :: "'a measure" where |
303 "borel = sigma UNIV {S. open S}" |
303 "borel = sigma UNIV {S. open S}" |
304 |
304 |
305 abbreviation "borel_measurable M \<equiv> measurable M borel" |
305 abbreviation "borel_measurable M \<equiv> measurable M borel" |
306 |
306 |
307 lemma in_borel_measurable: |
307 lemma%important in_borel_measurable: |
308 "f \<in> borel_measurable M \<longleftrightarrow> |
308 "f \<in> borel_measurable M \<longleftrightarrow> |
309 (\<forall>S \<in> sigma_sets UNIV {S. open S}. f -` S \<inter> space M \<in> sets M)" |
309 (\<forall>S \<in> sigma_sets UNIV {S. open S}. f -` S \<inter> space M \<in> sets M)" |
310 by (auto simp add: measurable_def borel_def) |
310 by%unimportant (auto simp add: measurable_def borel_def) |
311 |
311 |
312 lemma in_borel_measurable_borel: |
312 lemma%important in_borel_measurable_borel: |
313 "f \<in> borel_measurable M \<longleftrightarrow> |
313 "f \<in> borel_measurable M \<longleftrightarrow> |
314 (\<forall>S \<in> sets borel. |
314 (\<forall>S \<in> sets borel. |
315 f -` S \<inter> space M \<in> sets M)" |
315 f -` S \<inter> space M \<in> sets M)" |
316 by (auto simp add: measurable_def borel_def) |
316 by%unimportant (auto simp add: measurable_def borel_def) |
317 |
317 |
318 lemma space_borel[simp]: "space borel = UNIV" |
318 lemma%unimportant space_borel[simp]: "space borel = UNIV" |
319 unfolding borel_def by auto |
319 unfolding borel_def by auto |
320 |
320 |
321 lemma space_in_borel[measurable]: "UNIV \<in> sets borel" |
321 lemma%unimportant space_in_borel[measurable]: "UNIV \<in> sets borel" |
322 unfolding borel_def by auto |
322 unfolding borel_def by auto |
323 |
323 |
324 lemma sets_borel: "sets borel = sigma_sets UNIV {S. open S}" |
324 lemma%unimportant sets_borel: "sets borel = sigma_sets UNIV {S. open S}" |
325 unfolding borel_def by (rule sets_measure_of) simp |
325 unfolding borel_def by (rule sets_measure_of) simp |
326 |
326 |
327 lemma measurable_sets_borel: |
327 lemma%unimportant measurable_sets_borel: |
328 "\<lbrakk>f \<in> measurable borel M; A \<in> sets M\<rbrakk> \<Longrightarrow> f -` A \<in> sets borel" |
328 "\<lbrakk>f \<in> measurable borel M; A \<in> sets M\<rbrakk> \<Longrightarrow> f -` A \<in> sets borel" |
329 by (drule (1) measurable_sets) simp |
329 by (drule (1) measurable_sets) simp |
330 |
330 |
331 lemma pred_Collect_borel[measurable (raw)]: "Measurable.pred borel P \<Longrightarrow> {x. P x} \<in> sets borel" |
331 lemma%unimportant pred_Collect_borel[measurable (raw)]: "Measurable.pred borel P \<Longrightarrow> {x. P x} \<in> sets borel" |
332 unfolding borel_def pred_def by auto |
332 unfolding borel_def pred_def by auto |
333 |
333 |
334 lemma borel_open[measurable (raw generic)]: |
334 lemma%unimportant borel_open[measurable (raw generic)]: |
335 assumes "open A" shows "A \<in> sets borel" |
335 assumes "open A" shows "A \<in> sets borel" |
336 proof - |
336 proof - |
337 have "A \<in> {S. open S}" unfolding mem_Collect_eq using assms . |
337 have "A \<in> {S. open S}" unfolding mem_Collect_eq using assms . |
338 thus ?thesis unfolding borel_def by auto |
338 thus ?thesis unfolding borel_def by auto |
339 qed |
339 qed |
340 |
340 |
341 lemma borel_closed[measurable (raw generic)]: |
341 lemma%unimportant borel_closed[measurable (raw generic)]: |
342 assumes "closed A" shows "A \<in> sets borel" |
342 assumes "closed A" shows "A \<in> sets borel" |
343 proof - |
343 proof - |
344 have "space borel - (- A) \<in> sets borel" |
344 have "space borel - (- A) \<in> sets borel" |
345 using assms unfolding closed_def by (blast intro: borel_open) |
345 using assms unfolding closed_def by (blast intro: borel_open) |
346 thus ?thesis by simp |
346 thus ?thesis by simp |
347 qed |
347 qed |
348 |
348 |
349 lemma borel_singleton[measurable]: |
349 lemma%unimportant borel_singleton[measurable]: |
350 "A \<in> sets borel \<Longrightarrow> insert x A \<in> sets (borel :: 'a::t1_space measure)" |
350 "A \<in> sets borel \<Longrightarrow> insert x A \<in> sets (borel :: 'a::t1_space measure)" |
351 unfolding insert_def by (rule sets.Un) auto |
351 unfolding insert_def by (rule sets.Un) auto |
352 |
352 |
353 lemma sets_borel_eq_count_space: "sets (borel :: 'a::{countable, t2_space} measure) = count_space UNIV" |
353 lemma%unimportant sets_borel_eq_count_space: "sets (borel :: 'a::{countable, t2_space} measure) = count_space UNIV" |
354 proof - |
354 proof - |
355 have "(\<Union>a\<in>A. {a}) \<in> sets borel" for A :: "'a set" |
355 have "(\<Union>a\<in>A. {a}) \<in> sets borel" for A :: "'a set" |
356 by (intro sets.countable_UN') auto |
356 by (intro sets.countable_UN') auto |
357 then show ?thesis |
357 then show ?thesis |
358 by auto |
358 by auto |
359 qed |
359 qed |
360 |
360 |
361 lemma borel_comp[measurable]: "A \<in> sets borel \<Longrightarrow> - A \<in> sets borel" |
361 lemma%unimportant borel_comp[measurable]: "A \<in> sets borel \<Longrightarrow> - A \<in> sets borel" |
362 unfolding Compl_eq_Diff_UNIV by simp |
362 unfolding Compl_eq_Diff_UNIV by simp |
363 |
363 |
364 lemma borel_measurable_vimage: |
364 lemma%unimportant borel_measurable_vimage: |
365 fixes f :: "'a \<Rightarrow> 'x::t2_space" |
365 fixes f :: "'a \<Rightarrow> 'x::t2_space" |
366 assumes borel[measurable]: "f \<in> borel_measurable M" |
366 assumes borel[measurable]: "f \<in> borel_measurable M" |
367 shows "f -` {x} \<inter> space M \<in> sets M" |
367 shows "f -` {x} \<inter> space M \<in> sets M" |
368 by simp |
368 by simp |
369 |
369 |
370 lemma borel_measurableI: |
370 lemma%unimportant borel_measurableI: |
371 fixes f :: "'a \<Rightarrow> 'x::topological_space" |
371 fixes f :: "'a \<Rightarrow> 'x::topological_space" |
372 assumes "\<And>S. open S \<Longrightarrow> f -` S \<inter> space M \<in> sets M" |
372 assumes "\<And>S. open S \<Longrightarrow> f -` S \<inter> space M \<in> sets M" |
373 shows "f \<in> borel_measurable M" |
373 shows "f \<in> borel_measurable M" |
374 unfolding borel_def |
374 unfolding borel_def |
375 proof (rule measurable_measure_of, simp_all) |
375 proof (rule measurable_measure_of, simp_all) |
376 fix S :: "'x set" assume "open S" thus "f -` S \<inter> space M \<in> sets M" |
376 fix S :: "'x set" assume "open S" thus "f -` S \<inter> space M \<in> sets M" |
377 using assms[of S] by simp |
377 using assms[of S] by simp |
378 qed |
378 qed |
379 |
379 |
380 lemma borel_measurable_const: |
380 lemma%unimportant borel_measurable_const: |
381 "(\<lambda>x. c) \<in> borel_measurable M" |
381 "(\<lambda>x. c) \<in> borel_measurable M" |
382 by auto |
382 by auto |
383 |
383 |
384 lemma borel_measurable_indicator: |
384 lemma%unimportant borel_measurable_indicator: |
385 assumes A: "A \<in> sets M" |
385 assumes A: "A \<in> sets M" |
386 shows "indicator A \<in> borel_measurable M" |
386 shows "indicator A \<in> borel_measurable M" |
387 unfolding indicator_def [abs_def] using A |
387 unfolding indicator_def [abs_def] using A |
388 by (auto intro!: measurable_If_set) |
388 by (auto intro!: measurable_If_set) |
389 |
389 |
390 lemma borel_measurable_count_space[measurable (raw)]: |
390 lemma%unimportant borel_measurable_count_space[measurable (raw)]: |
391 "f \<in> borel_measurable (count_space S)" |
391 "f \<in> borel_measurable (count_space S)" |
392 unfolding measurable_def by auto |
392 unfolding measurable_def by auto |
393 |
393 |
394 lemma borel_measurable_indicator'[measurable (raw)]: |
394 lemma%unimportant borel_measurable_indicator'[measurable (raw)]: |
395 assumes [measurable]: "{x\<in>space M. f x \<in> A x} \<in> sets M" |
395 assumes [measurable]: "{x\<in>space M. f x \<in> A x} \<in> sets M" |
396 shows "(\<lambda>x. indicator (A x) (f x)) \<in> borel_measurable M" |
396 shows "(\<lambda>x. indicator (A x) (f x)) \<in> borel_measurable M" |
397 unfolding indicator_def[abs_def] |
397 unfolding indicator_def[abs_def] |
398 by (auto intro!: measurable_If) |
398 by (auto intro!: measurable_If) |
399 |
399 |
400 lemma borel_measurable_indicator_iff: |
400 lemma%important borel_measurable_indicator_iff: |
401 "(indicator A :: 'a \<Rightarrow> 'x::{t1_space, zero_neq_one}) \<in> borel_measurable M \<longleftrightarrow> A \<inter> space M \<in> sets M" |
401 "(indicator A :: 'a \<Rightarrow> 'x::{t1_space, zero_neq_one}) \<in> borel_measurable M \<longleftrightarrow> A \<inter> space M \<in> sets M" |
402 (is "?I \<in> borel_measurable M \<longleftrightarrow> _") |
402 (is "?I \<in> borel_measurable M \<longleftrightarrow> _") |
403 proof |
403 proof%unimportant |
404 assume "?I \<in> borel_measurable M" |
404 assume "?I \<in> borel_measurable M" |
405 then have "?I -` {1} \<inter> space M \<in> sets M" |
405 then have "?I -` {1} \<inter> space M \<in> sets M" |
406 unfolding measurable_def by auto |
406 unfolding measurable_def by auto |
407 also have "?I -` {1} \<inter> space M = A \<inter> space M" |
407 also have "?I -` {1} \<inter> space M = A \<inter> space M" |
408 unfolding indicator_def [abs_def] by auto |
408 unfolding indicator_def [abs_def] by auto |
413 (indicator (A \<inter> space M) :: 'a \<Rightarrow> 'x) \<in> borel_measurable M" |
413 (indicator (A \<inter> space M) :: 'a \<Rightarrow> 'x) \<in> borel_measurable M" |
414 by (intro measurable_cong) (auto simp: indicator_def) |
414 by (intro measurable_cong) (auto simp: indicator_def) |
415 ultimately show "?I \<in> borel_measurable M" by auto |
415 ultimately show "?I \<in> borel_measurable M" by auto |
416 qed |
416 qed |
417 |
417 |
418 lemma borel_measurable_subalgebra: |
418 lemma%unimportant borel_measurable_subalgebra: |
419 assumes "sets N \<subseteq> sets M" "space N = space M" "f \<in> borel_measurable N" |
419 assumes "sets N \<subseteq> sets M" "space N = space M" "f \<in> borel_measurable N" |
420 shows "f \<in> borel_measurable M" |
420 shows "f \<in> borel_measurable M" |
421 using assms unfolding measurable_def by auto |
421 using assms unfolding measurable_def by auto |
422 |
422 |
423 lemma borel_measurable_restrict_space_iff_ereal: |
423 lemma%unimportant borel_measurable_restrict_space_iff_ereal: |
424 fixes f :: "'a \<Rightarrow> ereal" |
424 fixes f :: "'a \<Rightarrow> ereal" |
425 assumes \<Omega>[measurable, simp]: "\<Omega> \<inter> space M \<in> sets M" |
425 assumes \<Omega>[measurable, simp]: "\<Omega> \<inter> space M \<in> sets M" |
426 shows "f \<in> borel_measurable (restrict_space M \<Omega>) \<longleftrightarrow> |
426 shows "f \<in> borel_measurable (restrict_space M \<Omega>) \<longleftrightarrow> |
427 (\<lambda>x. f x * indicator \<Omega> x) \<in> borel_measurable M" |
427 (\<lambda>x. f x * indicator \<Omega> x) \<in> borel_measurable M" |
428 by (subst measurable_restrict_space_iff) |
428 by (subst measurable_restrict_space_iff) |
429 (auto simp: indicator_def if_distrib[where f="\<lambda>x. a * x" for a] cong del: if_weak_cong) |
429 (auto simp: indicator_def if_distrib[where f="\<lambda>x. a * x" for a] cong del: if_weak_cong) |
430 |
430 |
431 lemma borel_measurable_restrict_space_iff_ennreal: |
431 lemma%unimportant borel_measurable_restrict_space_iff_ennreal: |
432 fixes f :: "'a \<Rightarrow> ennreal" |
432 fixes f :: "'a \<Rightarrow> ennreal" |
433 assumes \<Omega>[measurable, simp]: "\<Omega> \<inter> space M \<in> sets M" |
433 assumes \<Omega>[measurable, simp]: "\<Omega> \<inter> space M \<in> sets M" |
434 shows "f \<in> borel_measurable (restrict_space M \<Omega>) \<longleftrightarrow> |
434 shows "f \<in> borel_measurable (restrict_space M \<Omega>) \<longleftrightarrow> |
435 (\<lambda>x. f x * indicator \<Omega> x) \<in> borel_measurable M" |
435 (\<lambda>x. f x * indicator \<Omega> x) \<in> borel_measurable M" |
436 by (subst measurable_restrict_space_iff) |
436 by (subst measurable_restrict_space_iff) |
437 (auto simp: indicator_def if_distrib[where f="\<lambda>x. a * x" for a] cong del: if_weak_cong) |
437 (auto simp: indicator_def if_distrib[where f="\<lambda>x. a * x" for a] cong del: if_weak_cong) |
438 |
438 |
439 lemma borel_measurable_restrict_space_iff: |
439 lemma%unimportant borel_measurable_restrict_space_iff: |
440 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
440 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
441 assumes \<Omega>[measurable, simp]: "\<Omega> \<inter> space M \<in> sets M" |
441 assumes \<Omega>[measurable, simp]: "\<Omega> \<inter> space M \<in> sets M" |
442 shows "f \<in> borel_measurable (restrict_space M \<Omega>) \<longleftrightarrow> |
442 shows "f \<in> borel_measurable (restrict_space M \<Omega>) \<longleftrightarrow> |
443 (\<lambda>x. indicator \<Omega> x *\<^sub>R f x) \<in> borel_measurable M" |
443 (\<lambda>x. indicator \<Omega> x *\<^sub>R f x) \<in> borel_measurable M" |
444 by (subst measurable_restrict_space_iff) |
444 by (subst measurable_restrict_space_iff) |
445 (auto simp: indicator_def if_distrib[where f="\<lambda>x. x *\<^sub>R a" for a] ac_simps |
445 (auto simp: indicator_def if_distrib[where f="\<lambda>x. x *\<^sub>R a" for a] ac_simps |
446 cong del: if_weak_cong) |
446 cong del: if_weak_cong) |
447 |
447 |
448 lemma cbox_borel[measurable]: "cbox a b \<in> sets borel" |
448 lemma%unimportant cbox_borel[measurable]: "cbox a b \<in> sets borel" |
449 by (auto intro: borel_closed) |
449 by (auto intro: borel_closed) |
450 |
450 |
451 lemma box_borel[measurable]: "box a b \<in> sets borel" |
451 lemma%unimportant box_borel[measurable]: "box a b \<in> sets borel" |
452 by (auto intro: borel_open) |
452 by (auto intro: borel_open) |
453 |
453 |
454 lemma borel_compact: "compact (A::'a::t2_space set) \<Longrightarrow> A \<in> sets borel" |
454 lemma%unimportant borel_compact: "compact (A::'a::t2_space set) \<Longrightarrow> A \<in> sets borel" |
455 by (auto intro: borel_closed dest!: compact_imp_closed) |
455 by (auto intro: borel_closed dest!: compact_imp_closed) |
456 |
456 |
457 lemma borel_sigma_sets_subset: |
457 lemma%unimportant borel_sigma_sets_subset: |
458 "A \<subseteq> sets borel \<Longrightarrow> sigma_sets UNIV A \<subseteq> sets borel" |
458 "A \<subseteq> sets borel \<Longrightarrow> sigma_sets UNIV A \<subseteq> sets borel" |
459 using sets.sigma_sets_subset[of A borel] by simp |
459 using sets.sigma_sets_subset[of A borel] by simp |
460 |
460 |
461 lemma borel_eq_sigmaI1: |
461 lemma%important borel_eq_sigmaI1: |
462 fixes F :: "'i \<Rightarrow> 'a::topological_space set" and X :: "'a::topological_space set set" |
462 fixes F :: "'i \<Rightarrow> 'a::topological_space set" and X :: "'a::topological_space set set" |
463 assumes borel_eq: "borel = sigma UNIV X" |
463 assumes borel_eq: "borel = sigma UNIV X" |
464 assumes X: "\<And>x. x \<in> X \<Longrightarrow> x \<in> sets (sigma UNIV (F ` A))" |
464 assumes X: "\<And>x. x \<in> X \<Longrightarrow> x \<in> sets (sigma UNIV (F ` A))" |
465 assumes F: "\<And>i. i \<in> A \<Longrightarrow> F i \<in> sets borel" |
465 assumes F: "\<And>i. i \<in> A \<Longrightarrow> F i \<in> sets borel" |
466 shows "borel = sigma UNIV (F ` A)" |
466 shows "borel = sigma UNIV (F ` A)" |
467 unfolding borel_def |
467 unfolding borel_def |
468 proof (intro sigma_eqI antisym) |
468 proof%unimportant (intro sigma_eqI antisym) |
469 have borel_rev_eq: "sigma_sets UNIV {S::'a set. open S} = sets borel" |
469 have borel_rev_eq: "sigma_sets UNIV {S::'a set. open S} = sets borel" |
470 unfolding borel_def by simp |
470 unfolding borel_def by simp |
471 also have "\<dots> = sigma_sets UNIV X" |
471 also have "\<dots> = sigma_sets UNIV X" |
472 unfolding borel_eq by simp |
472 unfolding borel_eq by simp |
473 also have "\<dots> \<subseteq> sigma_sets UNIV (F`A)" |
473 also have "\<dots> \<subseteq> sigma_sets UNIV (F`A)" |
475 finally show "sigma_sets UNIV {S. open S} \<subseteq> sigma_sets UNIV (F`A)" . |
475 finally show "sigma_sets UNIV {S. open S} \<subseteq> sigma_sets UNIV (F`A)" . |
476 show "sigma_sets UNIV (F`A) \<subseteq> sigma_sets UNIV {S. open S}" |
476 show "sigma_sets UNIV (F`A) \<subseteq> sigma_sets UNIV {S. open S}" |
477 unfolding borel_rev_eq using F by (intro borel_sigma_sets_subset) auto |
477 unfolding borel_rev_eq using F by (intro borel_sigma_sets_subset) auto |
478 qed auto |
478 qed auto |
479 |
479 |
480 lemma borel_eq_sigmaI2: |
480 lemma%unimportant borel_eq_sigmaI2: |
481 fixes F :: "'i \<Rightarrow> 'j \<Rightarrow> 'a::topological_space set" |
481 fixes F :: "'i \<Rightarrow> 'j \<Rightarrow> 'a::topological_space set" |
482 and G :: "'l \<Rightarrow> 'k \<Rightarrow> 'a::topological_space set" |
482 and G :: "'l \<Rightarrow> 'k \<Rightarrow> 'a::topological_space set" |
483 assumes borel_eq: "borel = sigma UNIV ((\<lambda>(i, j). G i j)`B)" |
483 assumes borel_eq: "borel = sigma UNIV ((\<lambda>(i, j). G i j)`B)" |
484 assumes X: "\<And>i j. (i, j) \<in> B \<Longrightarrow> G i j \<in> sets (sigma UNIV ((\<lambda>(i, j). F i j) ` A))" |
484 assumes X: "\<And>i j. (i, j) \<in> B \<Longrightarrow> G i j \<in> sets (sigma UNIV ((\<lambda>(i, j). F i j) ` A))" |
485 assumes F: "\<And>i j. (i, j) \<in> A \<Longrightarrow> F i j \<in> sets borel" |
485 assumes F: "\<And>i j. (i, j) \<in> A \<Longrightarrow> F i j \<in> sets borel" |
486 shows "borel = sigma UNIV ((\<lambda>(i, j). F i j) ` A)" |
486 shows "borel = sigma UNIV ((\<lambda>(i, j). F i j) ` A)" |
487 using assms |
487 using assms |
488 by (intro borel_eq_sigmaI1[where X="(\<lambda>(i, j). G i j) ` B" and F="(\<lambda>(i, j). F i j)"]) auto |
488 by (intro borel_eq_sigmaI1[where X="(\<lambda>(i, j). G i j) ` B" and F="(\<lambda>(i, j). F i j)"]) auto |
489 |
489 |
490 lemma borel_eq_sigmaI3: |
490 lemma%unimportant borel_eq_sigmaI3: |
491 fixes F :: "'i \<Rightarrow> 'j \<Rightarrow> 'a::topological_space set" and X :: "'a::topological_space set set" |
491 fixes F :: "'i \<Rightarrow> 'j \<Rightarrow> 'a::topological_space set" and X :: "'a::topological_space set set" |
492 assumes borel_eq: "borel = sigma UNIV X" |
492 assumes borel_eq: "borel = sigma UNIV X" |
493 assumes X: "\<And>x. x \<in> X \<Longrightarrow> x \<in> sets (sigma UNIV ((\<lambda>(i, j). F i j) ` A))" |
493 assumes X: "\<And>x. x \<in> X \<Longrightarrow> x \<in> sets (sigma UNIV ((\<lambda>(i, j). F i j) ` A))" |
494 assumes F: "\<And>i j. (i, j) \<in> A \<Longrightarrow> F i j \<in> sets borel" |
494 assumes F: "\<And>i j. (i, j) \<in> A \<Longrightarrow> F i j \<in> sets borel" |
495 shows "borel = sigma UNIV ((\<lambda>(i, j). F i j) ` A)" |
495 shows "borel = sigma UNIV ((\<lambda>(i, j). F i j) ` A)" |
496 using assms by (intro borel_eq_sigmaI1[where X=X and F="(\<lambda>(i, j). F i j)"]) auto |
496 using assms by (intro borel_eq_sigmaI1[where X=X and F="(\<lambda>(i, j). F i j)"]) auto |
497 |
497 |
498 lemma borel_eq_sigmaI4: |
498 lemma%unimportant borel_eq_sigmaI4: |
499 fixes F :: "'i \<Rightarrow> 'a::topological_space set" |
499 fixes F :: "'i \<Rightarrow> 'a::topological_space set" |
500 and G :: "'l \<Rightarrow> 'k \<Rightarrow> 'a::topological_space set" |
500 and G :: "'l \<Rightarrow> 'k \<Rightarrow> 'a::topological_space set" |
501 assumes borel_eq: "borel = sigma UNIV ((\<lambda>(i, j). G i j)`A)" |
501 assumes borel_eq: "borel = sigma UNIV ((\<lambda>(i, j). G i j)`A)" |
502 assumes X: "\<And>i j. (i, j) \<in> A \<Longrightarrow> G i j \<in> sets (sigma UNIV (range F))" |
502 assumes X: "\<And>i j. (i, j) \<in> A \<Longrightarrow> G i j \<in> sets (sigma UNIV (range F))" |
503 assumes F: "\<And>i. F i \<in> sets borel" |
503 assumes F: "\<And>i. F i \<in> sets borel" |
504 shows "borel = sigma UNIV (range F)" |
504 shows "borel = sigma UNIV (range F)" |
505 using assms by (intro borel_eq_sigmaI1[where X="(\<lambda>(i, j). G i j) ` A" and F=F]) auto |
505 using assms by (intro borel_eq_sigmaI1[where X="(\<lambda>(i, j). G i j) ` A" and F=F]) auto |
506 |
506 |
507 lemma borel_eq_sigmaI5: |
507 lemma%unimportant borel_eq_sigmaI5: |
508 fixes F :: "'i \<Rightarrow> 'j \<Rightarrow> 'a::topological_space set" and G :: "'l \<Rightarrow> 'a::topological_space set" |
508 fixes F :: "'i \<Rightarrow> 'j \<Rightarrow> 'a::topological_space set" and G :: "'l \<Rightarrow> 'a::topological_space set" |
509 assumes borel_eq: "borel = sigma UNIV (range G)" |
509 assumes borel_eq: "borel = sigma UNIV (range G)" |
510 assumes X: "\<And>i. G i \<in> sets (sigma UNIV (range (\<lambda>(i, j). F i j)))" |
510 assumes X: "\<And>i. G i \<in> sets (sigma UNIV (range (\<lambda>(i, j). F i j)))" |
511 assumes F: "\<And>i j. F i j \<in> sets borel" |
511 assumes F: "\<And>i j. F i j \<in> sets borel" |
512 shows "borel = sigma UNIV (range (\<lambda>(i, j). F i j))" |
512 shows "borel = sigma UNIV (range (\<lambda>(i, j). F i j))" |
513 using assms by (intro borel_eq_sigmaI1[where X="range G" and F="(\<lambda>(i, j). F i j)"]) auto |
513 using assms by (intro borel_eq_sigmaI1[where X="range G" and F="(\<lambda>(i, j). F i j)"]) auto |
514 |
514 |
515 lemma second_countable_borel_measurable: |
515 lemma%important second_countable_borel_measurable: |
516 fixes X :: "'a::second_countable_topology set set" |
516 fixes X :: "'a::second_countable_topology set set" |
517 assumes eq: "open = generate_topology X" |
517 assumes eq: "open = generate_topology X" |
518 shows "borel = sigma UNIV X" |
518 shows "borel = sigma UNIV X" |
519 unfolding borel_def |
519 unfolding borel_def |
520 proof (intro sigma_eqI sigma_sets_eqI) |
520 proof%unimportant (intro sigma_eqI sigma_sets_eqI) |
521 interpret X: sigma_algebra UNIV "sigma_sets UNIV X" |
521 interpret X: sigma_algebra UNIV "sigma_sets UNIV X" |
522 by (rule sigma_algebra_sigma_sets) simp |
522 by (rule sigma_algebra_sigma_sets) simp |
523 |
523 |
524 fix S :: "'a set" assume "S \<in> Collect open" |
524 fix S :: "'a set" assume "S \<in> Collect open" |
525 then have "generate_topology X S" |
525 then have "generate_topology X S" |
900 also have "\<dots> = gfp F" |
900 also have "\<dots> = gfp F" |
901 by (rule inf_continuous_gfp[symmetric]) fact |
901 by (rule inf_continuous_gfp[symmetric]) fact |
902 finally show ?thesis . |
902 finally show ?thesis . |
903 qed |
903 qed |
904 |
904 |
905 lemma borel_measurable_max[measurable (raw)]: |
905 lemma%unimportant borel_measurable_max[measurable (raw)]: |
906 "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. max (g x) (f x) :: 'b::{second_countable_topology, linorder_topology}) \<in> borel_measurable M" |
906 "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. max (g x) (f x) :: 'b::{second_countable_topology, linorder_topology}) \<in> borel_measurable M" |
907 by (rule borel_measurableI_less) simp |
907 by (rule borel_measurableI_less) simp |
908 |
908 |
909 lemma borel_measurable_min[measurable (raw)]: |
909 lemma%unimportant borel_measurable_min[measurable (raw)]: |
910 "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. min (g x) (f x) :: 'b::{second_countable_topology, linorder_topology}) \<in> borel_measurable M" |
910 "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. min (g x) (f x) :: 'b::{second_countable_topology, linorder_topology}) \<in> borel_measurable M" |
911 by (rule borel_measurableI_greater) simp |
911 by (rule borel_measurableI_greater) simp |
912 |
912 |
913 lemma borel_measurable_Min[measurable (raw)]: |
913 lemma%unimportant borel_measurable_Min[measurable (raw)]: |
914 "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable M) \<Longrightarrow> (\<lambda>x. Min ((\<lambda>i. f i x)`I) :: 'b::{second_countable_topology, linorder_topology}) \<in> borel_measurable M" |
914 "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable M) \<Longrightarrow> (\<lambda>x. Min ((\<lambda>i. f i x)`I) :: 'b::{second_countable_topology, linorder_topology}) \<in> borel_measurable M" |
915 proof (induct I rule: finite_induct) |
915 proof (induct I rule: finite_induct) |
916 case (insert i I) then show ?case |
916 case (insert i I) then show ?case |
917 by (cases "I = {}") auto |
917 by (cases "I = {}") auto |
918 qed auto |
918 qed auto |
919 |
919 |
920 lemma borel_measurable_Max[measurable (raw)]: |
920 lemma%unimportant borel_measurable_Max[measurable (raw)]: |
921 "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable M) \<Longrightarrow> (\<lambda>x. Max ((\<lambda>i. f i x)`I) :: 'b::{second_countable_topology, linorder_topology}) \<in> borel_measurable M" |
921 "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable M) \<Longrightarrow> (\<lambda>x. Max ((\<lambda>i. f i x)`I) :: 'b::{second_countable_topology, linorder_topology}) \<in> borel_measurable M" |
922 proof (induct I rule: finite_induct) |
922 proof (induct I rule: finite_induct) |
923 case (insert i I) then show ?case |
923 case (insert i I) then show ?case |
924 by (cases "I = {}") auto |
924 by (cases "I = {}") auto |
925 qed auto |
925 qed auto |
926 |
926 |
927 lemma borel_measurable_sup[measurable (raw)]: |
927 lemma%unimportant borel_measurable_sup[measurable (raw)]: |
928 "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. sup (g x) (f x) :: 'b::{lattice, second_countable_topology, linorder_topology}) \<in> borel_measurable M" |
928 "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. sup (g x) (f x) :: 'b::{lattice, second_countable_topology, linorder_topology}) \<in> borel_measurable M" |
929 unfolding sup_max by measurable |
929 unfolding sup_max by measurable |
930 |
930 |
931 lemma borel_measurable_inf[measurable (raw)]: |
931 lemma%unimportant borel_measurable_inf[measurable (raw)]: |
932 "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. inf (g x) (f x) :: 'b::{lattice, second_countable_topology, linorder_topology}) \<in> borel_measurable M" |
932 "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. inf (g x) (f x) :: 'b::{lattice, second_countable_topology, linorder_topology}) \<in> borel_measurable M" |
933 unfolding inf_min by measurable |
933 unfolding inf_min by measurable |
934 |
934 |
935 lemma [measurable (raw)]: |
935 lemma%unimportant [measurable (raw)]: |
936 fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_linorder, second_countable_topology, linorder_topology}" |
936 fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_linorder, second_countable_topology, linorder_topology}" |
937 assumes "\<And>i. f i \<in> borel_measurable M" |
937 assumes "\<And>i. f i \<in> borel_measurable M" |
938 shows borel_measurable_liminf: "(\<lambda>x. liminf (\<lambda>i. f i x)) \<in> borel_measurable M" |
938 shows borel_measurable_liminf: "(\<lambda>x. liminf (\<lambda>i. f i x)) \<in> borel_measurable M" |
939 and borel_measurable_limsup: "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M" |
939 and borel_measurable_limsup: "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M" |
940 unfolding liminf_SUP_INF limsup_INF_SUP using assms by auto |
940 unfolding liminf_SUP_INF limsup_INF_SUP using assms by auto |
941 |
941 |
942 lemma measurable_convergent[measurable (raw)]: |
942 lemma%unimportant measurable_convergent[measurable (raw)]: |
943 fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_linorder, second_countable_topology, linorder_topology}" |
943 fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_linorder, second_countable_topology, linorder_topology}" |
944 assumes [measurable]: "\<And>i. f i \<in> borel_measurable M" |
944 assumes [measurable]: "\<And>i. f i \<in> borel_measurable M" |
945 shows "Measurable.pred M (\<lambda>x. convergent (\<lambda>i. f i x))" |
945 shows "Measurable.pred M (\<lambda>x. convergent (\<lambda>i. f i x))" |
946 unfolding convergent_ereal by measurable |
946 unfolding convergent_ereal by measurable |
947 |
947 |
948 lemma sets_Collect_convergent[measurable]: |
948 lemma%unimportant sets_Collect_convergent[measurable]: |
949 fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_linorder, second_countable_topology, linorder_topology}" |
949 fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_linorder, second_countable_topology, linorder_topology}" |
950 assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M" |
950 assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M" |
951 shows "{x\<in>space M. convergent (\<lambda>i. f i x)} \<in> sets M" |
951 shows "{x\<in>space M. convergent (\<lambda>i. f i x)} \<in> sets M" |
952 by measurable |
952 by measurable |
953 |
953 |
954 lemma borel_measurable_lim[measurable (raw)]: |
954 lemma%unimportant borel_measurable_lim[measurable (raw)]: |
955 fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_linorder, second_countable_topology, linorder_topology}" |
955 fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_linorder, second_countable_topology, linorder_topology}" |
956 assumes [measurable]: "\<And>i. f i \<in> borel_measurable M" |
956 assumes [measurable]: "\<And>i. f i \<in> borel_measurable M" |
957 shows "(\<lambda>x. lim (\<lambda>i. f i x)) \<in> borel_measurable M" |
957 shows "(\<lambda>x. lim (\<lambda>i. f i x)) \<in> borel_measurable M" |
958 proof - |
958 proof - |
959 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))" |
959 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))" |
960 by (simp add: lim_def convergent_def convergent_limsup_cl) |
960 by (simp add: lim_def convergent_def convergent_limsup_cl) |
961 then show ?thesis |
961 then show ?thesis |
962 by simp |
962 by simp |
963 qed |
963 qed |
964 |
964 |
965 lemma borel_measurable_LIMSEQ_order: |
965 lemma%unimportant borel_measurable_LIMSEQ_order: |
966 fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_linorder, second_countable_topology, linorder_topology}" |
966 fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_linorder, second_countable_topology, linorder_topology}" |
967 assumes u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) \<longlonglongrightarrow> u' x" |
967 assumes u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) \<longlonglongrightarrow> u' x" |
968 and u: "\<And>i. u i \<in> borel_measurable M" |
968 and u: "\<And>i. u i \<in> borel_measurable M" |
969 shows "u' \<in> borel_measurable M" |
969 shows "u' \<in> borel_measurable M" |
970 proof - |
970 proof - |
971 have "\<And>x. x \<in> space M \<Longrightarrow> u' x = liminf (\<lambda>n. u n x)" |
971 have "\<And>x. x \<in> space M \<Longrightarrow> u' x = liminf (\<lambda>n. u n x)" |
972 using u' by (simp add: lim_imp_Liminf[symmetric]) |
972 using u' by (simp add: lim_imp_Liminf[symmetric]) |
973 with u show ?thesis by (simp cong: measurable_cong) |
973 with u show ?thesis by (simp cong: measurable_cong) |
974 qed |
974 qed |
975 |
975 |
976 subsection \<open>Borel spaces on topological monoids\<close> |
976 subsection%important \<open>Borel spaces on topological monoids\<close> |
977 |
977 |
978 lemma borel_measurable_add[measurable (raw)]: |
978 lemma%unimportant borel_measurable_add[measurable (raw)]: |
979 fixes f g :: "'a \<Rightarrow> 'b::{second_countable_topology, topological_monoid_add}" |
979 fixes f g :: "'a \<Rightarrow> 'b::{second_countable_topology, topological_monoid_add}" |
980 assumes f: "f \<in> borel_measurable M" |
980 assumes f: "f \<in> borel_measurable M" |
981 assumes g: "g \<in> borel_measurable M" |
981 assumes g: "g \<in> borel_measurable M" |
982 shows "(\<lambda>x. f x + g x) \<in> borel_measurable M" |
982 shows "(\<lambda>x. f x + g x) \<in> borel_measurable M" |
983 using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros) |
983 using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros) |
984 |
984 |
985 lemma borel_measurable_sum[measurable (raw)]: |
985 lemma%unimportant borel_measurable_sum[measurable (raw)]: |
986 fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> 'b::{second_countable_topology, topological_comm_monoid_add}" |
986 fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> 'b::{second_countable_topology, topological_comm_monoid_add}" |
987 assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M" |
987 assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M" |
988 shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M" |
988 shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M" |
989 proof cases |
989 proof cases |
990 assume "finite S" |
990 assume "finite S" |
991 thus ?thesis using assms by induct auto |
991 thus ?thesis using assms by induct auto |
992 qed simp |
992 qed simp |
993 |
993 |
994 lemma borel_measurable_suminf_order[measurable (raw)]: |
994 lemma%important borel_measurable_suminf_order[measurable (raw)]: |
995 fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_linorder, second_countable_topology, linorder_topology, topological_comm_monoid_add}" |
995 fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_linorder, second_countable_topology, linorder_topology, topological_comm_monoid_add}" |
996 assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M" |
996 assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M" |
997 shows "(\<lambda>x. suminf (\<lambda>i. f i x)) \<in> borel_measurable M" |
997 shows "(\<lambda>x. suminf (\<lambda>i. f i x)) \<in> borel_measurable M" |
998 unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp |
998 unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp |
999 |
999 |
1000 subsection \<open>Borel spaces on Euclidean spaces\<close> |
1000 subsection%important \<open>Borel spaces on Euclidean spaces\<close> |
1001 |
1001 |
1002 lemma borel_measurable_inner[measurable (raw)]: |
1002 lemma%important borel_measurable_inner[measurable (raw)]: |
1003 fixes f g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_inner}" |
1003 fixes f g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_inner}" |
1004 assumes "f \<in> borel_measurable M" |
1004 assumes "f \<in> borel_measurable M" |
1005 assumes "g \<in> borel_measurable M" |
1005 assumes "g \<in> borel_measurable M" |
1006 shows "(\<lambda>x. f x \<bullet> g x) \<in> borel_measurable M" |
1006 shows "(\<lambda>x. f x \<bullet> g x) \<in> borel_measurable M" |
1007 using assms |
1007 using assms |
1008 by (rule borel_measurable_continuous_Pair) (intro continuous_intros) |
1008 by%unimportant (rule borel_measurable_continuous_Pair) (intro continuous_intros) |
1009 |
1009 |
1010 notation |
1010 notation |
1011 eucl_less (infix "<e" 50) |
1011 eucl_less (infix "<e" 50) |
1012 |
1012 |
1013 lemma box_oc: "{x. a <e x \<and> x \<le> b} = {x. a <e x} \<inter> {..b}" |
1013 lemma%important box_oc: "{x. a <e x \<and> x \<le> b} = {x. a <e x} \<inter> {..b}" |
1014 and box_co: "{x. a \<le> x \<and> x <e b} = {a..} \<inter> {x. x <e b}" |
1014 and box_co: "{x. a \<le> x \<and> x <e b} = {a..} \<inter> {x. x <e b}" |
1015 by auto |
1015 by auto |
1016 |
1016 |
1017 lemma eucl_ivals[measurable]: |
1017 lemma%important eucl_ivals[measurable]: |
1018 fixes a b :: "'a::ordered_euclidean_space" |
1018 fixes a b :: "'a::ordered_euclidean_space" |
1019 shows "{x. x <e a} \<in> sets borel" |
1019 shows "{x. x <e a} \<in> sets borel" |
1020 and "{x. a <e x} \<in> sets borel" |
1020 and "{x. a <e x} \<in> sets borel" |
1021 and "{..a} \<in> sets borel" |
1021 and "{..a} \<in> sets borel" |
1022 and "{a..} \<in> sets borel" |
1022 and "{a..} \<in> sets borel" |
1284 assume a: "\<forall>i\<in>Basis. \<forall>a. S a i \<in> sets M" |
1284 assume a: "\<forall>i\<in>Basis. \<forall>a. S a i \<in> sets M" |
1285 then show "f \<in> borel_measurable M" |
1285 then show "f \<in> borel_measurable M" |
1286 by (auto intro!: measurable_measure_of simp: S_eq F) |
1286 by (auto intro!: measurable_measure_of simp: S_eq F) |
1287 qed |
1287 qed |
1288 |
1288 |
1289 lemma borel_measurable_iff_halfspace_le: |
1289 lemma%unimportant borel_measurable_iff_halfspace_le: |
1290 fixes f :: "'a \<Rightarrow> 'c::euclidean_space" |
1290 fixes f :: "'a \<Rightarrow> 'c::euclidean_space" |
1291 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)" |
1291 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)" |
1292 by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_le]) auto |
1292 by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_le]) auto |
1293 |
1293 |
1294 lemma borel_measurable_iff_halfspace_less: |
1294 lemma%unimportant borel_measurable_iff_halfspace_less: |
1295 fixes f :: "'a \<Rightarrow> 'c::euclidean_space" |
1295 fixes f :: "'a \<Rightarrow> 'c::euclidean_space" |
1296 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)" |
1296 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)" |
1297 by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_less]) auto |
1297 by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_less]) auto |
1298 |
1298 |
1299 lemma borel_measurable_iff_halfspace_ge: |
1299 lemma%unimportant borel_measurable_iff_halfspace_ge: |
1300 fixes f :: "'a \<Rightarrow> 'c::euclidean_space" |
1300 fixes f :: "'a \<Rightarrow> 'c::euclidean_space" |
1301 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)" |
1301 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)" |
1302 by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_ge]) auto |
1302 by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_ge]) auto |
1303 |
1303 |
1304 lemma borel_measurable_iff_halfspace_greater: |
1304 lemma%unimportant borel_measurable_iff_halfspace_greater: |
1305 fixes f :: "'a \<Rightarrow> 'c::euclidean_space" |
1305 fixes f :: "'a \<Rightarrow> 'c::euclidean_space" |
1306 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)" |
1306 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)" |
1307 by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_greater]) auto |
1307 by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_greater]) auto |
1308 |
1308 |
1309 lemma borel_measurable_iff_le: |
1309 lemma%unimportant borel_measurable_iff_le: |
1310 "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w \<le> a} \<in> sets M)" |
1310 "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w \<le> a} \<in> sets M)" |
1311 using borel_measurable_iff_halfspace_le[where 'c=real] by simp |
1311 using borel_measurable_iff_halfspace_le[where 'c=real] by simp |
1312 |
1312 |
1313 lemma borel_measurable_iff_less: |
1313 lemma%unimportant borel_measurable_iff_less: |
1314 "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w < a} \<in> sets M)" |
1314 "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w < a} \<in> sets M)" |
1315 using borel_measurable_iff_halfspace_less[where 'c=real] by simp |
1315 using borel_measurable_iff_halfspace_less[where 'c=real] by simp |
1316 |
1316 |
1317 lemma borel_measurable_iff_ge: |
1317 lemma%unimportant borel_measurable_iff_ge: |
1318 "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a \<le> f w} \<in> sets M)" |
1318 "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a \<le> f w} \<in> sets M)" |
1319 using borel_measurable_iff_halfspace_ge[where 'c=real] |
1319 using borel_measurable_iff_halfspace_ge[where 'c=real] |
1320 by simp |
1320 by simp |
1321 |
1321 |
1322 lemma borel_measurable_iff_greater: |
1322 lemma%unimportant borel_measurable_iff_greater: |
1323 "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a < f w} \<in> sets M)" |
1323 "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a < f w} \<in> sets M)" |
1324 using borel_measurable_iff_halfspace_greater[where 'c=real] by simp |
1324 using borel_measurable_iff_halfspace_greater[where 'c=real] by simp |
1325 |
1325 |
1326 lemma borel_measurable_euclidean_space: |
1326 lemma%important borel_measurable_euclidean_space: |
1327 fixes f :: "'a \<Rightarrow> 'c::euclidean_space" |
1327 fixes f :: "'a \<Rightarrow> 'c::euclidean_space" |
1328 shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i\<in>Basis. (\<lambda>x. f x \<bullet> i) \<in> borel_measurable M)" |
1328 shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i\<in>Basis. (\<lambda>x. f x \<bullet> i) \<in> borel_measurable M)" |
1329 proof safe |
1329 proof%unimportant safe |
1330 assume f: "\<forall>i\<in>Basis. (\<lambda>x. f x \<bullet> i) \<in> borel_measurable M" |
1330 assume f: "\<forall>i\<in>Basis. (\<lambda>x. f x \<bullet> i) \<in> borel_measurable M" |
1331 then show "f \<in> borel_measurable M" |
1331 then show "f \<in> borel_measurable M" |
1332 by (subst borel_measurable_iff_halfspace_le) auto |
1332 by (subst borel_measurable_iff_halfspace_le) auto |
1333 qed auto |
1333 qed auto |
1334 |
1334 |
1335 subsection "Borel measurable operators" |
1335 subsection%important "Borel measurable operators" |
1336 |
1336 |
1337 lemma borel_measurable_norm[measurable]: "norm \<in> borel_measurable borel" |
1337 lemma%important borel_measurable_norm[measurable]: "norm \<in> borel_measurable borel" |
1338 by (intro borel_measurable_continuous_on1 continuous_intros) |
1338 by%unimportant (intro borel_measurable_continuous_on1 continuous_intros) |
1339 |
1339 |
1340 lemma borel_measurable_sgn [measurable]: "(sgn::'a::real_normed_vector \<Rightarrow> 'a) \<in> borel_measurable borel" |
1340 lemma%unimportant borel_measurable_sgn [measurable]: "(sgn::'a::real_normed_vector \<Rightarrow> 'a) \<in> borel_measurable borel" |
1341 by (rule borel_measurable_continuous_countable_exceptions[where X="{0}"]) |
1341 by (rule borel_measurable_continuous_countable_exceptions[where X="{0}"]) |
1342 (auto intro!: continuous_on_sgn continuous_on_id) |
1342 (auto intro!: continuous_on_sgn continuous_on_id) |
1343 |
1343 |
1344 lemma borel_measurable_uminus[measurable (raw)]: |
1344 lemma%important borel_measurable_uminus[measurable (raw)]: |
1345 fixes g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}" |
1345 fixes g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}" |
1346 assumes g: "g \<in> borel_measurable M" |
1346 assumes g: "g \<in> borel_measurable M" |
1347 shows "(\<lambda>x. - g x) \<in> borel_measurable M" |
1347 shows "(\<lambda>x. - g x) \<in> borel_measurable M" |
1348 by (rule borel_measurable_continuous_on[OF _ g]) (intro continuous_intros) |
1348 by%unimportant (rule borel_measurable_continuous_on[OF _ g]) (intro continuous_intros) |
1349 |
1349 |
1350 lemma borel_measurable_diff[measurable (raw)]: |
1350 lemma%important borel_measurable_diff[measurable (raw)]: |
1351 fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}" |
1351 fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}" |
1352 assumes f: "f \<in> borel_measurable M" |
1352 assumes f: "f \<in> borel_measurable M" |
1353 assumes g: "g \<in> borel_measurable M" |
1353 assumes g: "g \<in> borel_measurable M" |
1354 shows "(\<lambda>x. f x - g x) \<in> borel_measurable M" |
1354 shows "(\<lambda>x. f x - g x) \<in> borel_measurable M" |
1355 using borel_measurable_add [of f M "- g"] assms by (simp add: fun_Compl_def) |
1355 using%unimportant borel_measurable_add [of f M "- g"] assms by (simp add: fun_Compl_def) |
1356 |
1356 |
1357 lemma borel_measurable_times[measurable (raw)]: |
1357 lemma%unimportant borel_measurable_times[measurable (raw)]: |
1358 fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_algebra}" |
1358 fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_algebra}" |
1359 assumes f: "f \<in> borel_measurable M" |
1359 assumes f: "f \<in> borel_measurable M" |
1360 assumes g: "g \<in> borel_measurable M" |
1360 assumes g: "g \<in> borel_measurable M" |
1361 shows "(\<lambda>x. f x * g x) \<in> borel_measurable M" |
1361 shows "(\<lambda>x. f x * g x) \<in> borel_measurable M" |
1362 using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros) |
1362 using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros) |
1363 |
1363 |
1364 lemma borel_measurable_prod[measurable (raw)]: |
1364 lemma%important borel_measurable_prod[measurable (raw)]: |
1365 fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> 'b::{second_countable_topology, real_normed_field}" |
1365 fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> 'b::{second_countable_topology, real_normed_field}" |
1366 assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M" |
1366 assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M" |
1367 shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M" |
1367 shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M" |
1368 proof cases |
1368 proof%unimportant cases |
1369 assume "finite S" |
1369 assume "finite S" |
1370 thus ?thesis using assms by induct auto |
1370 thus ?thesis using assms by induct auto |
1371 qed simp |
1371 qed simp |
1372 |
1372 |
1373 lemma borel_measurable_dist[measurable (raw)]: |
1373 lemma%important borel_measurable_dist[measurable (raw)]: |
1374 fixes g f :: "'a \<Rightarrow> 'b::{second_countable_topology, metric_space}" |
1374 fixes g f :: "'a \<Rightarrow> 'b::{second_countable_topology, metric_space}" |
1375 assumes f: "f \<in> borel_measurable M" |
1375 assumes f: "f \<in> borel_measurable M" |
1376 assumes g: "g \<in> borel_measurable M" |
1376 assumes g: "g \<in> borel_measurable M" |
1377 shows "(\<lambda>x. dist (f x) (g x)) \<in> borel_measurable M" |
1377 shows "(\<lambda>x. dist (f x) (g x)) \<in> borel_measurable M" |
1378 using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros) |
1378 using%unimportant f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros) |
1379 |
1379 |
1380 lemma borel_measurable_scaleR[measurable (raw)]: |
1380 lemma%unimportant borel_measurable_scaleR[measurable (raw)]: |
1381 fixes g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}" |
1381 fixes g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}" |
1382 assumes f: "f \<in> borel_measurable M" |
1382 assumes f: "f \<in> borel_measurable M" |
1383 assumes g: "g \<in> borel_measurable M" |
1383 assumes g: "g \<in> borel_measurable M" |
1384 shows "(\<lambda>x. f x *\<^sub>R g x) \<in> borel_measurable M" |
1384 shows "(\<lambda>x. f x *\<^sub>R g x) \<in> borel_measurable M" |
1385 using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros) |
1385 using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros) |
1386 |
1386 |
1387 lemma borel_measurable_uminus_eq [simp]: |
1387 lemma%unimportant borel_measurable_uminus_eq [simp]: |
1388 fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}" |
1388 fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}" |
1389 shows "(\<lambda>x. - f x) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M" (is "?l = ?r") |
1389 shows "(\<lambda>x. - f x) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M" (is "?l = ?r") |
1390 proof |
1390 proof |
1391 assume ?l from borel_measurable_uminus[OF this] show ?r by simp |
1391 assume ?l from borel_measurable_uminus[OF this] show ?r by simp |
1392 qed auto |
1392 qed auto |
1393 |
1393 |
1394 lemma affine_borel_measurable_vector: |
1394 lemma%unimportant affine_borel_measurable_vector: |
1395 fixes f :: "'a \<Rightarrow> 'x::real_normed_vector" |
1395 fixes f :: "'a \<Rightarrow> 'x::real_normed_vector" |
1396 assumes "f \<in> borel_measurable M" |
1396 assumes "f \<in> borel_measurable M" |
1397 shows "(\<lambda>x. a + b *\<^sub>R f x) \<in> borel_measurable M" |
1397 shows "(\<lambda>x. a + b *\<^sub>R f x) \<in> borel_measurable M" |
1398 proof (rule borel_measurableI) |
1398 proof (rule borel_measurableI) |
1399 fix S :: "'x set" assume "open S" |
1399 fix S :: "'x set" assume "open S" |
1410 ultimately show ?thesis using assms unfolding in_borel_measurable_borel |
1410 ultimately show ?thesis using assms unfolding in_borel_measurable_borel |
1411 by auto |
1411 by auto |
1412 qed simp |
1412 qed simp |
1413 qed |
1413 qed |
1414 |
1414 |
1415 lemma borel_measurable_const_scaleR[measurable (raw)]: |
1415 lemma%unimportant borel_measurable_const_scaleR[measurable (raw)]: |
1416 "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. b *\<^sub>R f x ::'a::real_normed_vector) \<in> borel_measurable M" |
1416 "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. b *\<^sub>R f x ::'a::real_normed_vector) \<in> borel_measurable M" |
1417 using affine_borel_measurable_vector[of f M 0 b] by simp |
1417 using affine_borel_measurable_vector[of f M 0 b] by simp |
1418 |
1418 |
1419 lemma borel_measurable_const_add[measurable (raw)]: |
1419 lemma%unimportant borel_measurable_const_add[measurable (raw)]: |
1420 "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. a + f x ::'a::real_normed_vector) \<in> borel_measurable M" |
1420 "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. a + f x ::'a::real_normed_vector) \<in> borel_measurable M" |
1421 using affine_borel_measurable_vector[of f M a 1] by simp |
1421 using affine_borel_measurable_vector[of f M a 1] by simp |
1422 |
1422 |
1423 lemma borel_measurable_inverse[measurable (raw)]: |
1423 lemma%unimportant borel_measurable_inverse[measurable (raw)]: |
1424 fixes f :: "'a \<Rightarrow> 'b::real_normed_div_algebra" |
1424 fixes f :: "'a \<Rightarrow> 'b::real_normed_div_algebra" |
1425 assumes f: "f \<in> borel_measurable M" |
1425 assumes f: "f \<in> borel_measurable M" |
1426 shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M" |
1426 shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M" |
1427 apply (rule measurable_compose[OF f]) |
1427 apply (rule measurable_compose[OF f]) |
1428 apply (rule borel_measurable_continuous_countable_exceptions[of "{0}"]) |
1428 apply (rule borel_measurable_continuous_countable_exceptions[of "{0}"]) |
1429 apply (auto intro!: continuous_on_inverse continuous_on_id) |
1429 apply (auto intro!: continuous_on_inverse continuous_on_id) |
1430 done |
1430 done |
1431 |
1431 |
1432 lemma borel_measurable_divide[measurable (raw)]: |
1432 lemma%unimportant borel_measurable_divide[measurable (raw)]: |
1433 "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> |
1433 "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> |
1434 (\<lambda>x. f x / g x::'b::{second_countable_topology, real_normed_div_algebra}) \<in> borel_measurable M" |
1434 (\<lambda>x. f x / g x::'b::{second_countable_topology, real_normed_div_algebra}) \<in> borel_measurable M" |
1435 by (simp add: divide_inverse) |
1435 by (simp add: divide_inverse) |
1436 |
1436 |
1437 lemma borel_measurable_abs[measurable (raw)]: |
1437 lemma%unimportant borel_measurable_abs[measurable (raw)]: |
1438 "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. \<bar>f x :: real\<bar>) \<in> borel_measurable M" |
1438 "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. \<bar>f x :: real\<bar>) \<in> borel_measurable M" |
1439 unfolding abs_real_def by simp |
1439 unfolding abs_real_def by simp |
1440 |
1440 |
1441 lemma borel_measurable_nth[measurable (raw)]: |
1441 lemma%unimportant borel_measurable_nth[measurable (raw)]: |
1442 "(\<lambda>x::real^'n. x $ i) \<in> borel_measurable borel" |
1442 "(\<lambda>x::real^'n. x $ i) \<in> borel_measurable borel" |
1443 by (simp add: cart_eq_inner_axis) |
1443 by (simp add: cart_eq_inner_axis) |
1444 |
1444 |
1445 lemma convex_measurable: |
1445 lemma%important convex_measurable: |
1446 fixes A :: "'a :: euclidean_space set" |
1446 fixes A :: "'a :: euclidean_space set" |
1447 shows "X \<in> borel_measurable M \<Longrightarrow> X ` space M \<subseteq> A \<Longrightarrow> open A \<Longrightarrow> convex_on A q \<Longrightarrow> |
1447 shows "X \<in> borel_measurable M \<Longrightarrow> X ` space M \<subseteq> A \<Longrightarrow> open A \<Longrightarrow> convex_on A q \<Longrightarrow> |
1448 (\<lambda>x. q (X x)) \<in> borel_measurable M" |
1448 (\<lambda>x. q (X x)) \<in> borel_measurable M" |
1449 by (rule measurable_compose[where f=X and N="restrict_space borel A"]) |
1449 by%unimportant (rule measurable_compose[where f=X and N="restrict_space borel A"]) |
1450 (auto intro!: borel_measurable_continuous_on_restrict convex_on_continuous measurable_restrict_space2) |
1450 (auto intro!: borel_measurable_continuous_on_restrict convex_on_continuous measurable_restrict_space2) |
1451 |
1451 |
1452 lemma borel_measurable_ln[measurable (raw)]: |
1452 lemma%unimportant borel_measurable_ln[measurable (raw)]: |
1453 assumes f: "f \<in> borel_measurable M" |
1453 assumes f: "f \<in> borel_measurable M" |
1454 shows "(\<lambda>x. ln (f x :: real)) \<in> borel_measurable M" |
1454 shows "(\<lambda>x. ln (f x :: real)) \<in> borel_measurable M" |
1455 apply (rule measurable_compose[OF f]) |
1455 apply (rule measurable_compose[OF f]) |
1456 apply (rule borel_measurable_continuous_countable_exceptions[of "{0}"]) |
1456 apply (rule borel_measurable_continuous_countable_exceptions[of "{0}"]) |
1457 apply (auto intro!: continuous_on_ln continuous_on_id) |
1457 apply (auto intro!: continuous_on_ln continuous_on_id) |
1458 done |
1458 done |
1459 |
1459 |
1460 lemma borel_measurable_log[measurable (raw)]: |
1460 lemma%unimportant borel_measurable_log[measurable (raw)]: |
1461 "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. log (g x) (f x)) \<in> borel_measurable M" |
1461 "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. log (g x) (f x)) \<in> borel_measurable M" |
1462 unfolding log_def by auto |
1462 unfolding log_def by auto |
1463 |
1463 |
1464 lemma borel_measurable_exp[measurable]: |
1464 lemma%unimportant borel_measurable_exp[measurable]: |
1465 "(exp::'a::{real_normed_field,banach}\<Rightarrow>'a) \<in> borel_measurable borel" |
1465 "(exp::'a::{real_normed_field,banach}\<Rightarrow>'a) \<in> borel_measurable borel" |
1466 by (intro borel_measurable_continuous_on1 continuous_at_imp_continuous_on ballI isCont_exp) |
1466 by (intro borel_measurable_continuous_on1 continuous_at_imp_continuous_on ballI isCont_exp) |
1467 |
1467 |
1468 lemma measurable_real_floor[measurable]: |
1468 lemma%unimportant measurable_real_floor[measurable]: |
1469 "(floor :: real \<Rightarrow> int) \<in> measurable borel (count_space UNIV)" |
1469 "(floor :: real \<Rightarrow> int) \<in> measurable borel (count_space UNIV)" |
1470 proof - |
1470 proof - |
1471 have "\<And>a x. \<lfloor>x\<rfloor> = a \<longleftrightarrow> (real_of_int a \<le> x \<and> x < real_of_int (a + 1))" |
1471 have "\<And>a x. \<lfloor>x\<rfloor> = a \<longleftrightarrow> (real_of_int a \<le> x \<and> x < real_of_int (a + 1))" |
1472 by (auto intro: floor_eq2) |
1472 by (auto intro: floor_eq2) |
1473 then show ?thesis |
1473 then show ?thesis |
1474 by (auto simp: vimage_def measurable_count_space_eq2_countable) |
1474 by (auto simp: vimage_def measurable_count_space_eq2_countable) |
1475 qed |
1475 qed |
1476 |
1476 |
1477 lemma measurable_real_ceiling[measurable]: |
1477 lemma%unimportant measurable_real_ceiling[measurable]: |
1478 "(ceiling :: real \<Rightarrow> int) \<in> measurable borel (count_space UNIV)" |
1478 "(ceiling :: real \<Rightarrow> int) \<in> measurable borel (count_space UNIV)" |
1479 unfolding ceiling_def[abs_def] by simp |
1479 unfolding ceiling_def[abs_def] by simp |
1480 |
1480 |
1481 lemma borel_measurable_real_floor: "(\<lambda>x::real. real_of_int \<lfloor>x\<rfloor>) \<in> borel_measurable borel" |
1481 lemma%unimportant borel_measurable_real_floor: "(\<lambda>x::real. real_of_int \<lfloor>x\<rfloor>) \<in> borel_measurable borel" |
1482 by simp |
1482 by simp |
1483 |
1483 |
1484 lemma borel_measurable_root [measurable]: "root n \<in> borel_measurable borel" |
1484 lemma%unimportant borel_measurable_root [measurable]: "root n \<in> borel_measurable borel" |
1485 by (intro borel_measurable_continuous_on1 continuous_intros) |
1485 by (intro borel_measurable_continuous_on1 continuous_intros) |
1486 |
1486 |
1487 lemma borel_measurable_sqrt [measurable]: "sqrt \<in> borel_measurable borel" |
1487 lemma%unimportant borel_measurable_sqrt [measurable]: "sqrt \<in> borel_measurable borel" |
1488 by (intro borel_measurable_continuous_on1 continuous_intros) |
1488 by (intro borel_measurable_continuous_on1 continuous_intros) |
1489 |
1489 |
1490 lemma borel_measurable_power [measurable (raw)]: |
1490 lemma%unimportant borel_measurable_power [measurable (raw)]: |
1491 fixes f :: "_ \<Rightarrow> 'b::{power,real_normed_algebra}" |
1491 fixes f :: "_ \<Rightarrow> 'b::{power,real_normed_algebra}" |
1492 assumes f: "f \<in> borel_measurable M" |
1492 assumes f: "f \<in> borel_measurable M" |
1493 shows "(\<lambda>x. (f x) ^ n) \<in> borel_measurable M" |
1493 shows "(\<lambda>x. (f x) ^ n) \<in> borel_measurable M" |
1494 by (intro borel_measurable_continuous_on [OF _ f] continuous_intros) |
1494 by (intro borel_measurable_continuous_on [OF _ f] continuous_intros) |
1495 |
1495 |
1496 lemma borel_measurable_Re [measurable]: "Re \<in> borel_measurable borel" |
1496 lemma%unimportant borel_measurable_Re [measurable]: "Re \<in> borel_measurable borel" |
1497 by (intro borel_measurable_continuous_on1 continuous_intros) |
1497 by (intro borel_measurable_continuous_on1 continuous_intros) |
1498 |
1498 |
1499 lemma borel_measurable_Im [measurable]: "Im \<in> borel_measurable borel" |
1499 lemma%unimportant borel_measurable_Im [measurable]: "Im \<in> borel_measurable borel" |
1500 by (intro borel_measurable_continuous_on1 continuous_intros) |
1500 by (intro borel_measurable_continuous_on1 continuous_intros) |
1501 |
1501 |
1502 lemma borel_measurable_of_real [measurable]: "(of_real :: _ \<Rightarrow> (_::real_normed_algebra)) \<in> borel_measurable borel" |
1502 lemma%unimportant borel_measurable_of_real [measurable]: "(of_real :: _ \<Rightarrow> (_::real_normed_algebra)) \<in> borel_measurable borel" |
1503 by (intro borel_measurable_continuous_on1 continuous_intros) |
1503 by (intro borel_measurable_continuous_on1 continuous_intros) |
1504 |
1504 |
1505 lemma borel_measurable_sin [measurable]: "(sin :: _ \<Rightarrow> (_::{real_normed_field,banach})) \<in> borel_measurable borel" |
1505 lemma%unimportant borel_measurable_sin [measurable]: "(sin :: _ \<Rightarrow> (_::{real_normed_field,banach})) \<in> borel_measurable borel" |
1506 by (intro borel_measurable_continuous_on1 continuous_intros) |
1506 by (intro borel_measurable_continuous_on1 continuous_intros) |
1507 |
1507 |
1508 lemma borel_measurable_cos [measurable]: "(cos :: _ \<Rightarrow> (_::{real_normed_field,banach})) \<in> borel_measurable borel" |
1508 lemma%unimportant borel_measurable_cos [measurable]: "(cos :: _ \<Rightarrow> (_::{real_normed_field,banach})) \<in> borel_measurable borel" |
1509 by (intro borel_measurable_continuous_on1 continuous_intros) |
1509 by (intro borel_measurable_continuous_on1 continuous_intros) |
1510 |
1510 |
1511 lemma borel_measurable_arctan [measurable]: "arctan \<in> borel_measurable borel" |
1511 lemma%unimportant borel_measurable_arctan [measurable]: "arctan \<in> borel_measurable borel" |
1512 by (intro borel_measurable_continuous_on1 continuous_intros) |
1512 by (intro borel_measurable_continuous_on1 continuous_intros) |
1513 |
1513 |
1514 lemma borel_measurable_complex_iff: |
1514 lemma%important borel_measurable_complex_iff: |
1515 "f \<in> borel_measurable M \<longleftrightarrow> |
1515 "f \<in> borel_measurable M \<longleftrightarrow> |
1516 (\<lambda>x. Re (f x)) \<in> borel_measurable M \<and> (\<lambda>x. Im (f x)) \<in> borel_measurable M" |
1516 (\<lambda>x. Re (f x)) \<in> borel_measurable M \<and> (\<lambda>x. Im (f x)) \<in> borel_measurable M" |
1517 apply auto |
1517 apply auto |
1518 apply (subst fun_complex_eq) |
1518 apply (subst fun_complex_eq) |
1519 apply (intro borel_measurable_add) |
1519 apply (intro borel_measurable_add) |
1520 apply auto |
1520 apply auto |
1521 done |
1521 done |
1522 |
1522 |
1523 lemma powr_real_measurable [measurable]: |
1523 lemma%important powr_real_measurable [measurable]: |
1524 assumes "f \<in> measurable M borel" "g \<in> measurable M borel" |
1524 assumes "f \<in> measurable M borel" "g \<in> measurable M borel" |
1525 shows "(\<lambda>x. f x powr g x :: real) \<in> measurable M borel" |
1525 shows "(\<lambda>x. f x powr g x :: real) \<in> measurable M borel" |
1526 using assms by (simp_all add: powr_def) |
1526 using%unimportant assms by (simp_all add: powr_def) |
1527 |
1527 |
1528 lemma measurable_of_bool[measurable]: "of_bool \<in> count_space UNIV \<rightarrow>\<^sub>M borel" |
1528 lemma%unimportant measurable_of_bool[measurable]: "of_bool \<in> count_space UNIV \<rightarrow>\<^sub>M borel" |
1529 by simp |
1529 by simp |
1530 |
1530 |
1531 subsection "Borel space on the extended reals" |
1531 subsection%important "Borel space on the extended reals" |
1532 |
1532 |
1533 lemma borel_measurable_ereal[measurable (raw)]: |
1533 lemma%unimportant borel_measurable_ereal[measurable (raw)]: |
1534 assumes f: "f \<in> borel_measurable M" shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M" |
1534 assumes f: "f \<in> borel_measurable M" shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M" |
1535 using continuous_on_ereal f by (rule borel_measurable_continuous_on) (rule continuous_on_id) |
1535 using continuous_on_ereal f by (rule borel_measurable_continuous_on) (rule continuous_on_id) |
1536 |
1536 |
1537 lemma borel_measurable_real_of_ereal[measurable (raw)]: |
1537 lemma%unimportant borel_measurable_real_of_ereal[measurable (raw)]: |
1538 fixes f :: "'a \<Rightarrow> ereal" |
1538 fixes f :: "'a \<Rightarrow> ereal" |
1539 assumes f: "f \<in> borel_measurable M" |
1539 assumes f: "f \<in> borel_measurable M" |
1540 shows "(\<lambda>x. real_of_ereal (f x)) \<in> borel_measurable M" |
1540 shows "(\<lambda>x. real_of_ereal (f x)) \<in> borel_measurable M" |
1541 apply (rule measurable_compose[OF f]) |
1541 apply (rule measurable_compose[OF f]) |
1542 apply (rule borel_measurable_continuous_countable_exceptions[of "{\<infinity>, -\<infinity> }"]) |
1542 apply (rule borel_measurable_continuous_countable_exceptions[of "{\<infinity>, -\<infinity> }"]) |
1543 apply (auto intro: continuous_on_real simp: Compl_eq_Diff_UNIV) |
1543 apply (auto intro: continuous_on_real simp: Compl_eq_Diff_UNIV) |
1544 done |
1544 done |
1545 |
1545 |
1546 lemma borel_measurable_ereal_cases: |
1546 lemma%unimportant borel_measurable_ereal_cases: |
1547 fixes f :: "'a \<Rightarrow> ereal" |
1547 fixes f :: "'a \<Rightarrow> ereal" |
1548 assumes f: "f \<in> borel_measurable M" |
1548 assumes f: "f \<in> borel_measurable M" |
1549 assumes H: "(\<lambda>x. H (ereal (real_of_ereal (f x)))) \<in> borel_measurable M" |
1549 assumes H: "(\<lambda>x. H (ereal (real_of_ereal (f x)))) \<in> borel_measurable M" |
1550 shows "(\<lambda>x. H (f x)) \<in> borel_measurable M" |
1550 shows "(\<lambda>x. H (f x)) \<in> borel_measurable M" |
1551 proof - |
1551 proof - |
1552 let ?F = "\<lambda>x. if f x = \<infinity> then H \<infinity> else if f x = - \<infinity> then H (-\<infinity>) else H (ereal (real_of_ereal (f x)))" |
1552 let ?F = "\<lambda>x. if f x = \<infinity> then H \<infinity> else if f x = - \<infinity> then H (-\<infinity>) else H (ereal (real_of_ereal (f x)))" |
1553 { fix x have "H (f x) = ?F x" by (cases "f x") auto } |
1553 { fix x have "H (f x) = ?F x" by (cases "f x") auto } |
1554 with f H show ?thesis by simp |
1554 with f H show ?thesis by simp |
1555 qed |
1555 qed |
1556 |
1556 |
1557 lemma |
1557 lemma%unimportant (*FIX ME needs a name *) |
1558 fixes f :: "'a \<Rightarrow> ereal" assumes f[measurable]: "f \<in> borel_measurable M" |
1558 fixes f :: "'a \<Rightarrow> ereal" assumes f[measurable]: "f \<in> borel_measurable M" |
1559 shows borel_measurable_ereal_abs[measurable(raw)]: "(\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M" |
1559 shows borel_measurable_ereal_abs[measurable(raw)]: "(\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M" |
1560 and borel_measurable_ereal_inverse[measurable(raw)]: "(\<lambda>x. inverse (f x) :: ereal) \<in> borel_measurable M" |
1560 and borel_measurable_ereal_inverse[measurable(raw)]: "(\<lambda>x. inverse (f x) :: ereal) \<in> borel_measurable M" |
1561 and borel_measurable_uminus_ereal[measurable(raw)]: "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M" |
1561 and borel_measurable_uminus_ereal[measurable(raw)]: "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M" |
1562 by (auto simp del: abs_real_of_ereal simp: borel_measurable_ereal_cases[OF f] measurable_If) |
1562 by (auto simp del: abs_real_of_ereal simp: borel_measurable_ereal_cases[OF f] measurable_If) |
1563 |
1563 |
1564 lemma borel_measurable_uminus_eq_ereal[simp]: |
1564 lemma%unimportant borel_measurable_uminus_eq_ereal[simp]: |
1565 "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M" (is "?l = ?r") |
1565 "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M" (is "?l = ?r") |
1566 proof |
1566 proof |
1567 assume ?l from borel_measurable_uminus_ereal[OF this] show ?r by simp |
1567 assume ?l from borel_measurable_uminus_ereal[OF this] show ?r by simp |
1568 qed auto |
1568 qed auto |
1569 |
1569 |
1570 lemma set_Collect_ereal2: |
1570 lemma%important set_Collect_ereal2: |
1571 fixes f g :: "'a \<Rightarrow> ereal" |
1571 fixes f g :: "'a \<Rightarrow> ereal" |
1572 assumes f: "f \<in> borel_measurable M" |
1572 assumes f: "f \<in> borel_measurable M" |
1573 assumes g: "g \<in> borel_measurable M" |
1573 assumes g: "g \<in> borel_measurable M" |
1574 assumes H: "{x \<in> space M. H (ereal (real_of_ereal (f x))) (ereal (real_of_ereal (g x)))} \<in> sets M" |
1574 assumes H: "{x \<in> space M. H (ereal (real_of_ereal (f x))) (ereal (real_of_ereal (g x)))} \<in> sets M" |
1575 "{x \<in> space borel. H (-\<infinity>) (ereal x)} \<in> sets borel" |
1575 "{x \<in> space borel. H (-\<infinity>) (ereal x)} \<in> sets borel" |
1576 "{x \<in> space borel. H (\<infinity>) (ereal x)} \<in> sets borel" |
1576 "{x \<in> space borel. H (\<infinity>) (ereal x)} \<in> sets borel" |
1577 "{x \<in> space borel. H (ereal x) (-\<infinity>)} \<in> sets borel" |
1577 "{x \<in> space borel. H (ereal x) (-\<infinity>)} \<in> sets borel" |
1578 "{x \<in> space borel. H (ereal x) (\<infinity>)} \<in> sets borel" |
1578 "{x \<in> space borel. H (ereal x) (\<infinity>)} \<in> sets borel" |
1579 shows "{x \<in> space M. H (f x) (g x)} \<in> sets M" |
1579 shows "{x \<in> space M. H (f x) (g x)} \<in> sets M" |
1580 proof - |
1580 proof%unimportant - |
1581 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_of_ereal (g x)))" |
1581 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_of_ereal (g x)))" |
1582 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_of_ereal (f x))) x" |
1582 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_of_ereal (f x))) x" |
1583 { fix x have "H (f x) (g x) = ?F x" by (cases "f x" "g x" rule: ereal2_cases) auto } |
1583 { fix x have "H (f x) (g x) = ?F x" by (cases "f x" "g x" rule: ereal2_cases) auto } |
1584 note * = this |
1584 note * = this |
1585 from assms show ?thesis |
1585 from assms show ?thesis |
1586 by (subst *) (simp del: space_borel split del: if_split) |
1586 by (subst *) (simp del: space_borel split del: if_split) |
1587 qed |
1587 qed |
1588 |
1588 |
1589 lemma borel_measurable_ereal_iff: |
1589 lemma%unimportant borel_measurable_ereal_iff: |
1590 shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M" |
1590 shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M" |
1591 proof |
1591 proof |
1592 assume "(\<lambda>x. ereal (f x)) \<in> borel_measurable M" |
1592 assume "(\<lambda>x. ereal (f x)) \<in> borel_measurable M" |
1593 from borel_measurable_real_of_ereal[OF this] |
1593 from borel_measurable_real_of_ereal[OF this] |
1594 show "f \<in> borel_measurable M" by auto |
1594 show "f \<in> borel_measurable M" by auto |
1595 qed auto |
1595 qed auto |
1596 |
1596 |
1597 lemma borel_measurable_erealD[measurable_dest]: |
1597 lemma%unimportant borel_measurable_erealD[measurable_dest]: |
1598 "(\<lambda>x. ereal (f x)) \<in> borel_measurable M \<Longrightarrow> g \<in> measurable N M \<Longrightarrow> (\<lambda>x. f (g x)) \<in> borel_measurable N" |
1598 "(\<lambda>x. ereal (f x)) \<in> borel_measurable M \<Longrightarrow> g \<in> measurable N M \<Longrightarrow> (\<lambda>x. f (g x)) \<in> borel_measurable N" |
1599 unfolding borel_measurable_ereal_iff by simp |
1599 unfolding borel_measurable_ereal_iff by simp |
1600 |
1600 |
1601 lemma borel_measurable_ereal_iff_real: |
1601 lemma%important borel_measurable_ereal_iff_real: |
1602 fixes f :: "'a \<Rightarrow> ereal" |
1602 fixes f :: "'a \<Rightarrow> ereal" |
1603 shows "f \<in> borel_measurable M \<longleftrightarrow> |
1603 shows "f \<in> borel_measurable M \<longleftrightarrow> |
1604 ((\<lambda>x. real_of_ereal (f x)) \<in> borel_measurable M \<and> f -` {\<infinity>} \<inter> space M \<in> sets M \<and> f -` {-\<infinity>} \<inter> space M \<in> sets M)" |
1604 ((\<lambda>x. real_of_ereal (f x)) \<in> borel_measurable M \<and> f -` {\<infinity>} \<inter> space M \<in> sets M \<and> f -` {-\<infinity>} \<inter> space M \<in> sets M)" |
1605 proof safe |
1605 proof%unimportant safe |
1606 assume *: "(\<lambda>x. real_of_ereal (f x)) \<in> borel_measurable M" "f -` {\<infinity>} \<inter> space M \<in> sets M" "f -` {-\<infinity>} \<inter> space M \<in> sets M" |
1606 assume *: "(\<lambda>x. real_of_ereal (f x)) \<in> borel_measurable M" "f -` {\<infinity>} \<inter> space M \<in> sets M" "f -` {-\<infinity>} \<inter> space M \<in> sets M" |
1607 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 |
1607 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 |
1608 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 |
1608 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 |
1609 let ?f = "\<lambda>x. if f x = \<infinity> then \<infinity> else if f x = -\<infinity> then -\<infinity> else ereal (real_of_ereal (f x))" |
1609 let ?f = "\<lambda>x. if f x = \<infinity> then \<infinity> else if f x = -\<infinity> then -\<infinity> else ereal (real_of_ereal (f x))" |
1610 have "?f \<in> borel_measurable M" using * ** by (intro measurable_If) auto |
1610 have "?f \<in> borel_measurable M" using * ** by (intro measurable_If) auto |
1611 also have "?f = f" by (auto simp: fun_eq_iff ereal_real) |
1611 also have "?f = f" by (auto simp: fun_eq_iff ereal_real) |
1612 finally show "f \<in> borel_measurable M" . |
1612 finally show "f \<in> borel_measurable M" . |
1613 qed simp_all |
1613 qed simp_all |
1614 |
1614 |
1615 lemma borel_measurable_ereal_iff_Iio: |
1615 lemma%unimportant borel_measurable_ereal_iff_Iio: |
1616 "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {..< a} \<inter> space M \<in> sets M)" |
1616 "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {..< a} \<inter> space M \<in> sets M)" |
1617 by (auto simp: borel_Iio measurable_iff_measure_of) |
1617 by (auto simp: borel_Iio measurable_iff_measure_of) |
1618 |
1618 |
1619 lemma borel_measurable_ereal_iff_Ioi: |
1619 lemma%unimportant borel_measurable_ereal_iff_Ioi: |
1620 "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {a <..} \<inter> space M \<in> sets M)" |
1620 "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {a <..} \<inter> space M \<in> sets M)" |
1621 by (auto simp: borel_Ioi measurable_iff_measure_of) |
1621 by (auto simp: borel_Ioi measurable_iff_measure_of) |
1622 |
1622 |
1623 lemma vimage_sets_compl_iff: |
1623 lemma%unimportant vimage_sets_compl_iff: |
1624 "f -` A \<inter> space M \<in> sets M \<longleftrightarrow> f -` (- A) \<inter> space M \<in> sets M" |
1624 "f -` A \<inter> space M \<in> sets M \<longleftrightarrow> f -` (- A) \<inter> space M \<in> sets M" |
1625 proof - |
1625 proof - |
1626 { fix A assume "f -` A \<inter> space M \<in> sets M" |
1626 { fix A assume "f -` A \<inter> space M \<in> sets M" |
1627 moreover have "f -` (- A) \<inter> space M = space M - f -` A \<inter> space M" by auto |
1627 moreover have "f -` (- A) \<inter> space M = space M - f -` A \<inter> space M" by auto |
1628 ultimately have "f -` (- A) \<inter> space M \<in> sets M" by auto } |
1628 ultimately have "f -` (- A) \<inter> space M \<in> sets M" by auto } |
1629 from this[of A] this[of "-A"] show ?thesis |
1629 from this[of A] this[of "-A"] show ?thesis |
1630 by (metis double_complement) |
1630 by (metis double_complement) |
1631 qed |
1631 qed |
1632 |
1632 |
1633 lemma borel_measurable_iff_Iic_ereal: |
1633 lemma%unimportant borel_measurable_iff_Iic_ereal: |
1634 "(f::'a\<Rightarrow>ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {..a} \<inter> space M \<in> sets M)" |
1634 "(f::'a\<Rightarrow>ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {..a} \<inter> space M \<in> sets M)" |
1635 unfolding borel_measurable_ereal_iff_Ioi vimage_sets_compl_iff[where A="{a <..}" for a] by simp |
1635 unfolding borel_measurable_ereal_iff_Ioi vimage_sets_compl_iff[where A="{a <..}" for a] by simp |
1636 |
1636 |
1637 lemma borel_measurable_iff_Ici_ereal: |
1637 lemma%unimportant borel_measurable_iff_Ici_ereal: |
1638 "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {a..} \<inter> space M \<in> sets M)" |
1638 "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {a..} \<inter> space M \<in> sets M)" |
1639 unfolding borel_measurable_ereal_iff_Iio vimage_sets_compl_iff[where A="{..< a}" for a] by simp |
1639 unfolding borel_measurable_ereal_iff_Iio vimage_sets_compl_iff[where A="{..< a}" for a] by simp |
1640 |
1640 |
1641 lemma borel_measurable_ereal2: |
1641 lemma%important borel_measurable_ereal2: |
1642 fixes f g :: "'a \<Rightarrow> ereal" |
1642 fixes f g :: "'a \<Rightarrow> ereal" |
1643 assumes f: "f \<in> borel_measurable M" |
1643 assumes f: "f \<in> borel_measurable M" |
1644 assumes g: "g \<in> borel_measurable M" |
1644 assumes g: "g \<in> borel_measurable M" |
1645 assumes H: "(\<lambda>x. H (ereal (real_of_ereal (f x))) (ereal (real_of_ereal (g x)))) \<in> borel_measurable M" |
1645 assumes H: "(\<lambda>x. H (ereal (real_of_ereal (f x))) (ereal (real_of_ereal (g x)))) \<in> borel_measurable M" |
1646 "(\<lambda>x. H (-\<infinity>) (ereal (real_of_ereal (g x)))) \<in> borel_measurable M" |
1646 "(\<lambda>x. H (-\<infinity>) (ereal (real_of_ereal (g x)))) \<in> borel_measurable M" |
1647 "(\<lambda>x. H (\<infinity>) (ereal (real_of_ereal (g x)))) \<in> borel_measurable M" |
1647 "(\<lambda>x. H (\<infinity>) (ereal (real_of_ereal (g x)))) \<in> borel_measurable M" |
1648 "(\<lambda>x. H (ereal (real_of_ereal (f x))) (-\<infinity>)) \<in> borel_measurable M" |
1648 "(\<lambda>x. H (ereal (real_of_ereal (f x))) (-\<infinity>)) \<in> borel_measurable M" |
1649 "(\<lambda>x. H (ereal (real_of_ereal (f x))) (\<infinity>)) \<in> borel_measurable M" |
1649 "(\<lambda>x. H (ereal (real_of_ereal (f x))) (\<infinity>)) \<in> borel_measurable M" |
1650 shows "(\<lambda>x. H (f x) (g x)) \<in> borel_measurable M" |
1650 shows "(\<lambda>x. H (f x) (g x)) \<in> borel_measurable M" |
1651 proof - |
1651 proof%unimportant - |
1652 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_of_ereal (g x)))" |
1652 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_of_ereal (g x)))" |
1653 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_of_ereal (f x))) x" |
1653 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_of_ereal (f x))) x" |
1654 { fix x have "H (f x) (g x) = ?F x" by (cases "f x" "g x" rule: ereal2_cases) auto } |
1654 { fix x have "H (f x) (g x) = ?F x" by (cases "f x" "g x" rule: ereal2_cases) auto } |
1655 note * = this |
1655 note * = this |
1656 from assms show ?thesis unfolding * by simp |
1656 from assms show ?thesis unfolding * by simp |
1657 qed |
1657 qed |
1658 |
1658 |
1659 lemma [measurable(raw)]: |
1659 lemma%unimportant [measurable(raw)]: |
1660 fixes f :: "'a \<Rightarrow> ereal" |
1660 fixes f :: "'a \<Rightarrow> ereal" |
1661 assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M" |
1661 assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M" |
1662 shows borel_measurable_ereal_add: "(\<lambda>x. f x + g x) \<in> borel_measurable M" |
1662 shows borel_measurable_ereal_add: "(\<lambda>x. f x + g x) \<in> borel_measurable M" |
1663 and borel_measurable_ereal_times: "(\<lambda>x. f x * g x) \<in> borel_measurable M" |
1663 and borel_measurable_ereal_times: "(\<lambda>x. f x * g x) \<in> borel_measurable M" |
1664 by (simp_all add: borel_measurable_ereal2) |
1664 by (simp_all add: borel_measurable_ereal2) |
1665 |
1665 |
1666 lemma [measurable(raw)]: |
1666 lemma%unimportant [measurable(raw)]: |
1667 fixes f g :: "'a \<Rightarrow> ereal" |
1667 fixes f g :: "'a \<Rightarrow> ereal" |
1668 assumes "f \<in> borel_measurable M" |
1668 assumes "f \<in> borel_measurable M" |
1669 assumes "g \<in> borel_measurable M" |
1669 assumes "g \<in> borel_measurable M" |
1670 shows borel_measurable_ereal_diff: "(\<lambda>x. f x - g x) \<in> borel_measurable M" |
1670 shows borel_measurable_ereal_diff: "(\<lambda>x. f x - g x) \<in> borel_measurable M" |
1671 and borel_measurable_ereal_divide: "(\<lambda>x. f x / g x) \<in> borel_measurable M" |
1671 and borel_measurable_ereal_divide: "(\<lambda>x. f x / g x) \<in> borel_measurable M" |
1672 using assms by (simp_all add: minus_ereal_def divide_ereal_def) |
1672 using assms by (simp_all add: minus_ereal_def divide_ereal_def) |
1673 |
1673 |
1674 lemma borel_measurable_ereal_sum[measurable (raw)]: |
1674 lemma%unimportant borel_measurable_ereal_sum[measurable (raw)]: |
1675 fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal" |
1675 fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal" |
1676 assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M" |
1676 assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M" |
1677 shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M" |
1677 shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M" |
1678 using assms by (induction S rule: infinite_finite_induct) auto |
1678 using assms by (induction S rule: infinite_finite_induct) auto |
1679 |
1679 |
1680 lemma borel_measurable_ereal_prod[measurable (raw)]: |
1680 lemma%unimportant borel_measurable_ereal_prod[measurable (raw)]: |
1681 fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal" |
1681 fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal" |
1682 assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M" |
1682 assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M" |
1683 shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M" |
1683 shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M" |
1684 using assms by (induction S rule: infinite_finite_induct) auto |
1684 using assms by (induction S rule: infinite_finite_induct) auto |
1685 |
1685 |
1686 lemma borel_measurable_extreal_suminf[measurable (raw)]: |
1686 lemma%unimportant borel_measurable_extreal_suminf[measurable (raw)]: |
1687 fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal" |
1687 fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal" |
1688 assumes [measurable]: "\<And>i. f i \<in> borel_measurable M" |
1688 assumes [measurable]: "\<And>i. f i \<in> borel_measurable M" |
1689 shows "(\<lambda>x. (\<Sum>i. f i x)) \<in> borel_measurable M" |
1689 shows "(\<lambda>x. (\<Sum>i. f i x)) \<in> borel_measurable M" |
1690 unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp |
1690 unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp |
1691 |
1691 |
1692 subsection "Borel space on the extended non-negative reals" |
1692 subsection%important "Borel space on the extended non-negative reals" |
1693 |
1693 |
1694 text \<open> @{type ennreal} is a topological monoid, so no rules for plus are required, also all order |
1694 text \<open> @{type ennreal} is a topological monoid, so no rules for plus are required, also all order |
1695 statements are usually done on type classes. \<close> |
1695 statements are usually done on type classes. \<close> |
1696 |
1696 |
1697 lemma measurable_enn2ereal[measurable]: "enn2ereal \<in> borel \<rightarrow>\<^sub>M borel" |
1697 lemma%unimportant measurable_enn2ereal[measurable]: "enn2ereal \<in> borel \<rightarrow>\<^sub>M borel" |
1698 by (intro borel_measurable_continuous_on1 continuous_on_enn2ereal) |
1698 by (intro borel_measurable_continuous_on1 continuous_on_enn2ereal) |
1699 |
1699 |
1700 lemma measurable_e2ennreal[measurable]: "e2ennreal \<in> borel \<rightarrow>\<^sub>M borel" |
1700 lemma%unimportant measurable_e2ennreal[measurable]: "e2ennreal \<in> borel \<rightarrow>\<^sub>M borel" |
1701 by (intro borel_measurable_continuous_on1 continuous_on_e2ennreal) |
1701 by (intro borel_measurable_continuous_on1 continuous_on_e2ennreal) |
1702 |
1702 |
1703 lemma borel_measurable_enn2real[measurable (raw)]: |
1703 lemma%unimportant borel_measurable_enn2real[measurable (raw)]: |
1704 "f \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> (\<lambda>x. enn2real (f x)) \<in> M \<rightarrow>\<^sub>M borel" |
1704 "f \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> (\<lambda>x. enn2real (f x)) \<in> M \<rightarrow>\<^sub>M borel" |
1705 unfolding enn2real_def[abs_def] by measurable |
1705 unfolding enn2real_def[abs_def] by measurable |
1706 |
1706 |
1707 definition [simp]: "is_borel f M \<longleftrightarrow> f \<in> borel_measurable M" |
1707 definition%important [simp]: "is_borel f M \<longleftrightarrow> f \<in> borel_measurable M" |
1708 |
1708 |
1709 lemma is_borel_transfer[transfer_rule]: "rel_fun (rel_fun (=) pcr_ennreal) (=) is_borel is_borel" |
1709 lemma%unimportant is_borel_transfer[transfer_rule]: "rel_fun (rel_fun (=) pcr_ennreal) (=) is_borel is_borel" |
1710 unfolding is_borel_def[abs_def] |
1710 unfolding is_borel_def[abs_def] |
1711 proof (safe intro!: rel_funI ext dest!: rel_fun_eq_pcr_ennreal[THEN iffD1]) |
1711 proof (safe intro!: rel_funI ext dest!: rel_fun_eq_pcr_ennreal[THEN iffD1]) |
1712 fix f and M :: "'a measure" |
1712 fix f and M :: "'a measure" |
1713 show "f \<in> borel_measurable M" if f: "enn2ereal \<circ> f \<in> borel_measurable M" |
1713 show "f \<in> borel_measurable M" if f: "enn2ereal \<circ> f \<in> borel_measurable M" |
1714 using measurable_compose[OF f measurable_e2ennreal] by simp |
1714 using measurable_compose[OF f measurable_e2ennreal] by simp |
1716 |
1716 |
1717 context |
1717 context |
1718 includes ennreal.lifting |
1718 includes ennreal.lifting |
1719 begin |
1719 begin |
1720 |
1720 |
1721 lemma measurable_ennreal[measurable]: "ennreal \<in> borel \<rightarrow>\<^sub>M borel" |
1721 lemma%unimportant measurable_ennreal[measurable]: "ennreal \<in> borel \<rightarrow>\<^sub>M borel" |
1722 unfolding is_borel_def[symmetric] |
1722 unfolding is_borel_def[symmetric] |
1723 by transfer simp |
1723 by transfer simp |
1724 |
1724 |
1725 lemma borel_measurable_ennreal_iff[simp]: |
1725 lemma%important borel_measurable_ennreal_iff[simp]: |
1726 assumes [simp]: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x" |
1726 assumes [simp]: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x" |
1727 shows "(\<lambda>x. ennreal (f x)) \<in> M \<rightarrow>\<^sub>M borel \<longleftrightarrow> f \<in> M \<rightarrow>\<^sub>M borel" |
1727 shows "(\<lambda>x. ennreal (f x)) \<in> M \<rightarrow>\<^sub>M borel \<longleftrightarrow> f \<in> M \<rightarrow>\<^sub>M borel" |
1728 proof safe |
1728 proof%unimportant safe |
1729 assume "(\<lambda>x. ennreal (f x)) \<in> M \<rightarrow>\<^sub>M borel" |
1729 assume "(\<lambda>x. ennreal (f x)) \<in> M \<rightarrow>\<^sub>M borel" |
1730 then have "(\<lambda>x. enn2real (ennreal (f x))) \<in> M \<rightarrow>\<^sub>M borel" |
1730 then have "(\<lambda>x. enn2real (ennreal (f x))) \<in> M \<rightarrow>\<^sub>M borel" |
1731 by measurable |
1731 by measurable |
1732 then show "f \<in> M \<rightarrow>\<^sub>M borel" |
1732 then show "f \<in> M \<rightarrow>\<^sub>M borel" |
1733 by (rule measurable_cong[THEN iffD1, rotated]) auto |
1733 by (rule measurable_cong[THEN iffD1, rotated]) auto |
1734 qed measurable |
1734 qed measurable |
1735 |
1735 |
1736 lemma borel_measurable_times_ennreal[measurable (raw)]: |
1736 lemma%unimportant borel_measurable_times_ennreal[measurable (raw)]: |
1737 fixes f g :: "'a \<Rightarrow> ennreal" |
1737 fixes f g :: "'a \<Rightarrow> ennreal" |
1738 shows "f \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> g \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> (\<lambda>x. f x * g x) \<in> M \<rightarrow>\<^sub>M borel" |
1738 shows "f \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> g \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> (\<lambda>x. f x * g x) \<in> M \<rightarrow>\<^sub>M borel" |
1739 unfolding is_borel_def[symmetric] by transfer simp |
1739 unfolding is_borel_def[symmetric] by transfer simp |
1740 |
1740 |
1741 lemma borel_measurable_inverse_ennreal[measurable (raw)]: |
1741 lemma%unimportant borel_measurable_inverse_ennreal[measurable (raw)]: |
1742 fixes f :: "'a \<Rightarrow> ennreal" |
1742 fixes f :: "'a \<Rightarrow> ennreal" |
1743 shows "f \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> (\<lambda>x. inverse (f x)) \<in> M \<rightarrow>\<^sub>M borel" |
1743 shows "f \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> (\<lambda>x. inverse (f x)) \<in> M \<rightarrow>\<^sub>M borel" |
1744 unfolding is_borel_def[symmetric] by transfer simp |
1744 unfolding is_borel_def[symmetric] by transfer simp |
1745 |
1745 |
1746 lemma borel_measurable_divide_ennreal[measurable (raw)]: |
1746 lemma%unimportant borel_measurable_divide_ennreal[measurable (raw)]: |
1747 fixes f :: "'a \<Rightarrow> ennreal" |
1747 fixes f :: "'a \<Rightarrow> ennreal" |
1748 shows "f \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> g \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> (\<lambda>x. f x / g x) \<in> M \<rightarrow>\<^sub>M borel" |
1748 shows "f \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> g \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> (\<lambda>x. f x / g x) \<in> M \<rightarrow>\<^sub>M borel" |
1749 unfolding divide_ennreal_def by simp |
1749 unfolding divide_ennreal_def by simp |
1750 |
1750 |
1751 lemma borel_measurable_minus_ennreal[measurable (raw)]: |
1751 lemma%unimportant borel_measurable_minus_ennreal[measurable (raw)]: |
1752 fixes f :: "'a \<Rightarrow> ennreal" |
1752 fixes f :: "'a \<Rightarrow> ennreal" |
1753 shows "f \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> g \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> (\<lambda>x. f x - g x) \<in> M \<rightarrow>\<^sub>M borel" |
1753 shows "f \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> g \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> (\<lambda>x. f x - g x) \<in> M \<rightarrow>\<^sub>M borel" |
1754 unfolding is_borel_def[symmetric] by transfer simp |
1754 unfolding is_borel_def[symmetric] by transfer simp |
1755 |
1755 |
1756 lemma borel_measurable_prod_ennreal[measurable (raw)]: |
1756 lemma%important borel_measurable_prod_ennreal[measurable (raw)]: |
1757 fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ennreal" |
1757 fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ennreal" |
1758 assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M" |
1758 assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M" |
1759 shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M" |
1759 shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M" |
1760 using assms by (induction S rule: infinite_finite_induct) auto |
1760 using%unimportant assms by (induction S rule: infinite_finite_induct) auto |
1761 |
1761 |
1762 end |
1762 end |
1763 |
1763 |
1764 hide_const (open) is_borel |
1764 hide_const (open) is_borel |
1765 |
1765 |
1766 subsection \<open>LIMSEQ is borel measurable\<close> |
1766 subsection%important \<open>LIMSEQ is borel measurable\<close> |
1767 |
1767 |
1768 lemma borel_measurable_LIMSEQ_real: |
1768 lemma%important borel_measurable_LIMSEQ_real: |
1769 fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> real" |
1769 fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> real" |
1770 assumes u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) \<longlonglongrightarrow> u' x" |
1770 assumes u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) \<longlonglongrightarrow> u' x" |
1771 and u: "\<And>i. u i \<in> borel_measurable M" |
1771 and u: "\<And>i. u i \<in> borel_measurable M" |
1772 shows "u' \<in> borel_measurable M" |
1772 shows "u' \<in> borel_measurable M" |
1773 proof - |
1773 proof%unimportant - |
1774 have "\<And>x. x \<in> space M \<Longrightarrow> liminf (\<lambda>n. ereal (u n x)) = ereal (u' x)" |
1774 have "\<And>x. x \<in> space M \<Longrightarrow> liminf (\<lambda>n. ereal (u n x)) = ereal (u' x)" |
1775 using u' by (simp add: lim_imp_Liminf) |
1775 using u' by (simp add: lim_imp_Liminf) |
1776 moreover from u have "(\<lambda>x. liminf (\<lambda>n. ereal (u n x))) \<in> borel_measurable M" |
1776 moreover from u have "(\<lambda>x. liminf (\<lambda>n. ereal (u n x))) \<in> borel_measurable M" |
1777 by auto |
1777 by auto |
1778 ultimately show ?thesis by (simp cong: measurable_cong add: borel_measurable_ereal_iff) |
1778 ultimately show ?thesis by (simp cong: measurable_cong add: borel_measurable_ereal_iff) |
1779 qed |
1779 qed |
1780 |
1780 |
1781 lemma borel_measurable_LIMSEQ_metric: |
1781 lemma%important borel_measurable_LIMSEQ_metric: |
1782 fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b :: metric_space" |
1782 fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b :: metric_space" |
1783 assumes [measurable]: "\<And>i. f i \<in> borel_measurable M" |
1783 assumes [measurable]: "\<And>i. f i \<in> borel_measurable M" |
1784 assumes lim: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. f i x) \<longlonglongrightarrow> g x" |
1784 assumes lim: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. f i x) \<longlonglongrightarrow> g x" |
1785 shows "g \<in> borel_measurable M" |
1785 shows "g \<in> borel_measurable M" |
1786 unfolding borel_eq_closed |
1786 unfolding borel_eq_closed |
1787 proof (safe intro!: measurable_measure_of) |
1787 proof%unimportant (safe intro!: measurable_measure_of) |
1788 fix A :: "'b set" assume "closed A" |
1788 fix A :: "'b set" assume "closed A" |
1789 |
1789 |
1790 have [measurable]: "(\<lambda>x. infdist (g x) A) \<in> borel_measurable M" |
1790 have [measurable]: "(\<lambda>x. infdist (g x) A) \<in> borel_measurable M" |
1791 proof (rule borel_measurable_LIMSEQ_real) |
1791 proof (rule borel_measurable_LIMSEQ_real) |
1792 show "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. infdist (f i x) A) \<longlonglongrightarrow> infdist (g x) A" |
1792 show "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. infdist (f i x) A) \<longlonglongrightarrow> infdist (g x) A" |