Theory Borel_Space
section ‹Borel Space›
theory Borel_Space
imports
Measurable Derivative Ordered_Euclidean_Space Extended_Real_Limits
begin
lemma is_interval_real_ereal_oo: "is_interval (real_of_ereal ` {N<..<M::ereal})"
by (auto simp: real_atLeastGreaterThan_eq)
lemma sets_Collect_eventually_sequentially[measurable]:
"(⋀i. {x∈space M. P x i} ∈ sets M) ⟹ {x∈space M. eventually (P x) sequentially} ∈ sets M"
unfolding eventually_sequentially by simp
lemma topological_basis_trivial: "topological_basis {A. open A}"
by (auto simp: topological_basis_def)
proposition open_prod_generated: "open = generate_topology {A × B | A B. open A ∧ open B}"
proof -
have "{A × B :: ('a × 'b) set | A B. open A ∧ open B} = ((λ(a, b). a × b) ` ({A. open A} × {A. open A}))"
by auto
then show ?thesis
by (auto intro: topological_basis_prod topological_basis_trivial topological_basis_imp_subbasis)
qed
proposition mono_on_imp_deriv_nonneg:
assumes mono: "mono_on A f" and deriv: "(f has_real_derivative D) (at x)"
assumes "x ∈ interior A"
shows "D ≥ 0"
proof (rule tendsto_lowerbound)
let ?A' = "(λy. y - x) ` interior A"
from deriv show "((λh. (f (x + h) - f x) / h) ⤏ D) (at 0)"
by (simp add: field_has_derivative_at has_field_derivative_def)
from mono have mono': "mono_on (interior A) f" by (rule mono_on_subset) (rule interior_subset)
show "eventually (λh. (f (x + h) - f x) / h ≥ 0) (at 0)"
proof (subst eventually_at_topological, intro exI conjI ballI impI)
have "open (interior A)" by simp
hence "open ((+) (-x) ` interior A)" by (rule open_translation)
also have "((+) (-x) ` interior A) = ?A'" by auto
finally show "open ?A'" .
next
from ‹x ∈ interior A› show "0 ∈ ?A'" by auto
next
fix h assume "h ∈ ?A'"
hence "x + h ∈ interior A" by auto
with mono' and ‹x ∈ interior A› show "(f (x + h) - f x) / h ≥ 0"
by (cases h rule: linorder_cases[of _ 0])
(simp_all add: divide_nonpos_neg divide_nonneg_pos mono_onD field_simps)
qed
qed simp
proposition mono_on_ctble_discont:
fixes f :: "real ⇒ real"
fixes A :: "real set"
assumes "mono_on A f"
shows "countable {a∈A. ¬ continuous (at a within A) f}"
proof -
have mono: "⋀x y. x ∈ A ⟹ y ∈ A ⟹ x ≤ y ⟹ f x ≤ f y"
using ‹mono_on A f› by (simp add: mono_on_def)
have "∀a ∈ {a∈A. ¬ continuous (at a within A) f}. ∃q :: nat × rat.
(fst q = 0 ∧ of_rat (snd q) < f a ∧ (∀x ∈ A. x < a ⟶ f x < of_rat (snd q))) ∨
(fst q = 1 ∧ of_rat (snd q) > f a ∧ (∀x ∈ A. x > a ⟶ f x > of_rat (snd q)))"
proof (clarsimp simp del: One_nat_def)
fix a assume "a ∈ A" assume "¬ continuous (at a within A) f"
thus "∃q1 q2.
q1 = 0 ∧ real_of_rat q2 < f a ∧ (∀x∈A. x < a ⟶ f x < real_of_rat q2) ∨
q1 = 1 ∧ f a < real_of_rat q2 ∧ (∀x∈A. a < x ⟶ real_of_rat q2 < f x)"
proof (auto simp add: continuous_within order_tendsto_iff eventually_at)
fix l assume "l < f a"
then obtain q2 where q2: "l < of_rat q2" "of_rat q2 < f a"
using of_rat_dense by blast
assume * [rule_format]: "∀d>0. ∃x∈A. x ≠ a ∧ dist x a < d ∧ ¬ l < f x"
from q2 have "real_of_rat q2 < f a ∧ (∀x∈A. x < a ⟶ f x < real_of_rat q2)"
using q2 *[of "a - _"] dist_real_def mono by fastforce
thus ?thesis by auto
next
fix u assume "u > f a"
then obtain q2 where q2: "f a < of_rat q2" "of_rat q2 < u"
using of_rat_dense by blast
assume *[rule_format]: "∀d>0. ∃x∈A. x ≠ a ∧ dist x a < d ∧ ¬ u > f x"
from q2 have "real_of_rat q2 > f a ∧ (∀x∈A. x > a ⟶ f x > real_of_rat q2)"
using q2 *[of "_ - a"] dist_real_def mono by fastforce
thus ?thesis by auto
qed
qed
then obtain g :: "real ⇒ nat × rat" where "∀a ∈ {a∈A. ¬ continuous (at a within A) f}.
(fst (g a) = 0 ∧ of_rat (snd (g a)) < f a ∧ (∀x ∈ A. x < a ⟶ f x < of_rat (snd (g a)))) |
(fst (g a) = 1 ∧ of_rat (snd (g a)) > f a ∧ (∀x ∈ A. x > a ⟶ f x > of_rat (snd (g a))))"
by (rule bchoice [THEN exE]) blast
hence g: "⋀a x. a ∈ A ⟹ ¬ continuous (at a within A) f ⟹ x ∈ A ⟹
(fst (g a) = 0 ∧ of_rat (snd (g a)) < f a ∧ (x < a ⟶ f x < of_rat (snd (g a)))) |
(fst (g a) = 1 ∧ of_rat (snd (g a)) > f a ∧ (x > a ⟶ f x > of_rat (snd (g a))))"
by auto
have "inj_on g {a∈A. ¬ continuous (at a within A) f}"
proof (auto simp add: inj_on_def)
fix w z
assume 1: "w ∈ A" and 2: "¬ continuous (at w within A) f" and
3: "z ∈ A" and 4: "¬ continuous (at z within A) f" and
5: "g w = g z"
from g [OF 1 2 3] g [OF 3 4 1] 5
show "w = z" by auto
qed
thus ?thesis
by (rule countableI')
qed
lemma mono_on_ctble_discont_open:
fixes f :: "real ⇒ real"
fixes A :: "real set"
assumes "open A" "mono_on A f"
shows "countable {a∈A. ¬isCont f a}"
using continuous_within_open [OF _ ‹open A›] ‹mono_on A f›
by (smt (verit, ccfv_threshold) Collect_cong mono_on_ctble_discont)
lemma mono_ctble_discont:
fixes f :: "real ⇒ real"
assumes "mono f"
shows "countable {a. ¬ isCont f a}"
using assms mono_on_ctble_discont [of UNIV f] unfolding mono_on_def mono_def by auto
lemma has_real_derivative_imp_continuous_on:
assumes "⋀x. x ∈ A ⟹ (f has_real_derivative f' x) (at x)"
shows "continuous_on A f"
by (meson DERIV_isCont assms continuous_at_imp_continuous_on)
lemma continuous_interval_vimage_Int:
assumes "continuous_on {a::real..b} g" and mono: "⋀x y. a ≤ x ⟹ x ≤ y ⟹ y ≤ b ⟹ g x ≤ g y"
assumes "a ≤ b" "(c::real) ≤ d" "{c..d} ⊆ {g a..g b}"
obtains c' d' where "{a..b} ∩ g -` {c..d} = {c'..d'}" "c' ≤ d'" "g c' = c" "g d' = d"
proof-
let ?A = "{a..b} ∩ g -` {c..d}"
from IVT'[of g a c b, OF _ _ ‹a ≤ b› assms(1)] assms(4,5)
obtain c'' where c'': "c'' ∈ ?A" "g c'' = c" by auto
from IVT'[of g a d b, OF _ _ ‹a ≤ b› assms(1)] assms(4,5)
obtain d'' where d'': "d'' ∈ ?A" "g d'' = d" by auto
hence [simp]: "?A ≠ {}" by blast
define c' where "c' = Inf ?A"
define d' where "d' = Sup ?A"
have "?A ⊆ {c'..d'}" unfolding c'_def d'_def
by (intro subsetI) (auto intro: cInf_lower cSup_upper)
moreover from assms have "closed ?A"
using continuous_on_closed_vimage[of "{a..b}" g] by (subst Int_commute) simp
hence c'd'_in_set: "c' ∈ ?A" "d' ∈ ?A" unfolding c'_def d'_def
by ((intro closed_contains_Inf closed_contains_Sup, simp_all)[])+
hence "{c'..d'} ⊆ ?A" using assms
by (intro subsetI)
(auto intro!: order_trans[of c "g c'" "g x" for x] order_trans[of "g x" "g d'" d for x]
intro!: mono)
moreover have "c' ≤ d'" using c'd'_in_set(2) unfolding c'_def by (intro cInf_lower) auto
moreover have "g c' ≤ c" "g d' ≥ d"
using c'' d'' calculation by (metis IntE atLeastAtMost_iff mono order_class.order_eq_iff)+
with c'd'_in_set have "g c' = c" "g d' = d"
by auto
ultimately show ?thesis
using that by blast
qed
subsection ‹Generic Borel spaces›
definition (in topological_space) borel :: "'a measure" where
"borel = sigma UNIV {S. open S}"
abbreviation "borel_measurable M ≡ measurable M borel"
lemma in_borel_measurable:
"f ∈ borel_measurable M ⟷
(∀S ∈ sigma_sets UNIV {S. open S}. f -` S ∩ space M ∈ sets M)"
by (auto simp add: measurable_def borel_def)
lemma in_borel_measurable_borel:
"f ∈ borel_measurable M ⟷ (∀S ∈ sets borel. f -` S ∩ space M ∈ sets M)"
by (auto simp add: measurable_def borel_def)
lemma space_borel[simp]: "space borel = UNIV"
unfolding borel_def by auto
lemma space_in_borel[measurable]: "UNIV ∈ sets borel"
unfolding borel_def by auto
lemma sets_borel: "sets borel = sigma_sets UNIV {S. open S}"
unfolding borel_def by (rule sets_measure_of) simp
lemma measurable_sets_borel:
"⟦f ∈ measurable borel M; A ∈ sets M⟧ ⟹ f -` A ∈ sets borel"
by (drule (1) measurable_sets) simp
lemma pred_Collect_borel[measurable (raw)]: "Measurable.pred borel P ⟹ {x. P x} ∈ sets borel"
unfolding borel_def pred_def by auto
lemma borel_open[measurable (raw generic)]:
assumes "open A" shows "A ∈ sets borel"
by (simp add: assms sets_borel)
lemma borel_closed[measurable (raw generic)]:
assumes "closed A" shows "A ∈ sets borel"
proof -
have "space borel - (- A) ∈ sets borel"
using assms unfolding closed_def by (blast intro: borel_open)
thus ?thesis by simp
qed
lemma borel_singleton[measurable]:
"A ∈ sets borel ⟹ insert x A ∈ sets (borel :: 'a::t1_space measure)"
unfolding insert_def by (rule sets.Un) auto
lemma sets_borel_eq_count_space: "sets (borel :: 'a::{countable, t2_space} measure) = count_space UNIV"
by (simp add: set_eq_iff sets.countable)
lemma borel_comp[measurable]: "A ∈ sets borel ⟹ - A ∈ sets borel"
unfolding Compl_eq_Diff_UNIV by simp
lemma borel_measurable_vimage:
fixes f :: "'a ⇒ 'x::t2_space"
assumes borel[measurable]: "f ∈ borel_measurable M"
shows "f -` {x} ∩ space M ∈ sets M"
by simp
lemma borel_measurableI:
fixes f :: "'a ⇒ 'x::topological_space"
assumes "⋀S. open S ⟹ f -` S ∩ space M ∈ sets M"
shows "f ∈ borel_measurable M"
unfolding borel_def
proof (rule measurable_measure_of, simp_all)
fix S :: "'x set" assume "open S" thus "f -` S ∩ space M ∈ sets M"
using assms[of S] by simp
qed
lemma borel_measurable_const:
"(λx. c) ∈ borel_measurable M"
by auto
lemma borel_measurable_indicator:
assumes A: "A ∈ sets M"
shows "indicator A ∈ borel_measurable M"
unfolding indicator_def [abs_def] using A
by (auto intro!: measurable_If_set)
lemma borel_measurable_count_space[measurable (raw)]:
"f ∈ borel_measurable (count_space S)"
unfolding measurable_def by auto
lemma borel_measurable_indicator'[measurable (raw)]:
assumes [measurable]: "{x∈space M. f x ∈ A x} ∈ sets M"
shows "(λx. indicator (A x) (f x)) ∈ borel_measurable M"
unfolding indicator_def[abs_def]
by (auto intro!: measurable_If)
lemma borel_measurable_indicator_iff:
"(indicator A :: 'a ⇒ 'x::{t1_space, zero_neq_one}) ∈ borel_measurable M ⟷ A ∩ space M ∈ sets M"
(is "?I ∈ borel_measurable M ⟷ _")
proof
assume "?I ∈ borel_measurable M"
then have "?I -` {1} ∩ space M ∈ sets M"
unfolding measurable_def by auto
also have "?I -` {1} ∩ space M = A ∩ space M"
unfolding indicator_def [abs_def] by auto
finally show "A ∩ space M ∈ sets M" .
next
assume "A ∩ space M ∈ sets M"
moreover have "?I ∈ borel_measurable M ⟷
(indicator (A ∩ space M) :: 'a ⇒ 'x) ∈ borel_measurable M"
by (intro measurable_cong) (auto simp: indicator_def)
ultimately show "?I ∈ borel_measurable M" by auto
qed
lemma borel_measurable_subalgebra:
assumes "sets N ⊆ sets M" "space N = space M" "f ∈ borel_measurable N"
shows "f ∈ borel_measurable M"
using assms unfolding measurable_def by auto
lemma borel_measurable_restrict_space_iff_ereal:
fixes f :: "'a ⇒ ereal"
assumes Ω[measurable, simp]: "Ω ∩ space M ∈ sets M"
shows "f ∈ borel_measurable (restrict_space M Ω) ⟷
(λx. f x * indicator Ω x) ∈ borel_measurable M"
by (subst measurable_restrict_space_iff)
(auto simp: indicator_def of_bool_def if_distrib[where f="λx. a * x" for a] cong: if_cong)
lemma borel_measurable_restrict_space_iff_ennreal:
fixes f :: "'a ⇒ ennreal"
assumes Ω[measurable, simp]: "Ω ∩ space M ∈ sets M"
shows "f ∈ borel_measurable (restrict_space M Ω) ⟷
(λx. f x * indicator Ω x) ∈ borel_measurable M"
by (subst measurable_restrict_space_iff)
(auto simp: indicator_def of_bool_def if_distrib[where f="λx. a * x" for a] cong: if_cong)
lemma borel_measurable_restrict_space_iff:
fixes f :: "'a ⇒ 'b::real_normed_vector"
assumes Ω[measurable, simp]: "Ω ∩ space M ∈ sets M"
shows "f ∈ borel_measurable (restrict_space M Ω) ⟷
(λx. indicator Ω x *⇩R f x) ∈ borel_measurable M"
by (subst measurable_restrict_space_iff)
(auto simp: indicator_def of_bool_def if_distrib[where f="λx. x *⇩R a" for a] ac_simps
cong: if_cong)
lemma cbox_borel[measurable]: "cbox a b ∈ sets borel"
by (auto intro: borel_closed)
lemma box_borel[measurable]: "box a b ∈ sets borel"
by (auto intro: borel_open)
lemma borel_compact: "compact (A::'a::t2_space set) ⟹ A ∈ sets borel"
by (simp add: borel_closed compact_imp_closed)
lemma borel_sigma_sets_subset:
"A ⊆ sets borel ⟹ sigma_sets UNIV A ⊆ sets borel"
using sets.sigma_sets_subset[of A borel] by simp
lemma borel_eq_sigmaI1:
fixes F :: "'i ⇒ 'a::topological_space set" and X :: "'a::topological_space set set"
assumes borel_eq: "borel = sigma UNIV X"
assumes X: "⋀x. x ∈ X ⟹ x ∈ sets (sigma UNIV (F ` A))"
assumes F: "⋀i. i ∈ A ⟹ F i ∈ sets borel"
shows "borel = sigma UNIV (F ` A)"
unfolding borel_def
proof (intro sigma_eqI antisym)
have borel_rev_eq: "sigma_sets UNIV {S::'a set. open S} = sets borel"
unfolding borel_def by simp
also have "… = sigma_sets UNIV X"
unfolding borel_eq by simp
also have "… ⊆ sigma_sets UNIV (F`A)"
using X by (intro sigma_algebra.sigma_sets_subset[OF sigma_algebra_sigma_sets]) auto
finally show "sigma_sets UNIV {S. open S} ⊆ sigma_sets UNIV (F`A)" .
show "sigma_sets UNIV (F`A) ⊆ sigma_sets UNIV {S. open S}"
by (metis F image_subset_iff sets_borel sigma_sets_mono)
qed auto
lemma borel_eq_sigmaI2:
fixes F :: "'i ⇒ 'j ⇒ 'a::topological_space set"
and G :: "'l ⇒ 'k ⇒ 'a::topological_space set"
assumes borel_eq: "borel = sigma UNIV ((λ(i, j). G i j)`B)"
assumes X: "⋀i j. (i, j) ∈ B ⟹ G i j ∈ sets (sigma UNIV ((λ(i, j). F i j) ` A))"
assumes F: "⋀i j. (i, j) ∈ A ⟹ F i j ∈ sets borel"
shows "borel = sigma UNIV ((λ(i, j). F i j) ` A)"
using assms
by (smt (verit, del_insts) borel_eq_sigmaI1 image_iff prod.collapse split_beta)
lemma borel_eq_sigmaI3:
fixes F :: "'i ⇒ 'j ⇒ 'a::topological_space set" and X :: "'a::topological_space set set"
assumes borel_eq: "borel = sigma UNIV X"
assumes X: "⋀x. x ∈ X ⟹ x ∈ sets (sigma UNIV ((λ(i, j). F i j) ` A))"
assumes F: "⋀i j. (i, j) ∈ A ⟹ F i j ∈ sets borel"
shows "borel = sigma UNIV ((λ(i, j). F i j) ` A)"
using assms by (intro borel_eq_sigmaI1[where X=X and F="(λ(i, j). F i j)"]) auto
lemma borel_eq_sigmaI4:
fixes F :: "'i ⇒ 'a::topological_space set"
and G :: "'l ⇒ 'k ⇒ 'a::topological_space set"
assumes borel_eq: "borel = sigma UNIV ((λ(i, j). G i j)`A)"
assumes X: "⋀i j. (i, j) ∈ A ⟹ G i j ∈ sets (sigma UNIV (range F))"
assumes F: "⋀i. F i ∈ sets borel"
shows "borel = sigma UNIV (range F)"
using assms by (intro borel_eq_sigmaI1[where X="(λ(i, j). G i j) ` A" and F=F]) auto
lemma borel_eq_sigmaI5:
fixes F :: "'i ⇒ 'j ⇒ 'a::topological_space set" and G :: "'l ⇒ 'a::topological_space set"
assumes borel_eq: "borel = sigma UNIV (range G)"
assumes X: "⋀i. G i ∈ sets (sigma UNIV (range (λ(i, j). F i j)))"
assumes F: "⋀i j. F i j ∈ sets borel"
shows "borel = sigma UNIV (range (λ(i, j). F i j))"
using assms by (intro borel_eq_sigmaI1[where X="range G" and F="(λ(i, j). F i j)"]) auto
theorem second_countable_borel_measurable:
fixes X :: "'a::second_countable_topology set set"
assumes eq: "open = generate_topology X"
shows "borel = sigma UNIV X"
unfolding borel_def
proof (intro sigma_eqI sigma_sets_eqI)
interpret X: sigma_algebra UNIV "sigma_sets UNIV X"
by (rule sigma_algebra_sigma_sets) simp
fix S :: "'a set" assume "S ∈ Collect open"
then have "generate_topology X S"
by (auto simp: eq)
then show "S ∈ sigma_sets UNIV X"
proof induction
case (UN K)
then have K: "⋀k. k ∈ K ⟹ open k"
unfolding eq by auto
from ex_countable_basis obtain B :: "'a set set" where
B: "⋀b. b ∈ B ⟹ open b" "⋀X. open X ⟹ ∃b⊆B. (⋃b) = X" and "countable B"
by (auto simp: topological_basis_def)
from B(2)[OF K] obtain m where m: "⋀k. k ∈ K ⟹ m k ⊆ B" "⋀k. k ∈ K ⟹ ⋃(m k) = k"
by metis
define U where "U = (⋃k∈K. m k)"
with m have "countable U"
by (intro countable_subset[OF _ ‹countable B›]) auto
have "⋃U = (⋃A∈U. A)" by simp
also have "… = ⋃K"
unfolding U_def UN_simps by (simp add: m)
finally have "⋃U = ⋃K" .
have "∀b∈U. ∃k∈K. b ⊆ k"
using m by (auto simp: U_def)
then obtain u where u: "⋀b. b ∈ U ⟹ u b ∈ K" and "⋀b. b ∈ U ⟹ b ⊆ u b"
by metis
then have "(⋃b∈U. u b) ⊆ ⋃K" "⋃U ⊆ (⋃b∈U. u b)"
by auto
then have "⋃K = (⋃b∈U. u b)"
unfolding ‹⋃U = ⋃K› by auto
also have "… ∈ sigma_sets UNIV X"
using u UN by (intro X.countable_UN' ‹countable U›) auto
finally show "⋃K ∈ sigma_sets UNIV X" .
qed auto
qed (auto simp: eq intro: generate_topology.Basis)
lemma borel_eq_closed: "borel = sigma UNIV (Collect closed)"
proof -
have "x ∈ sigma_sets UNIV (Collect closed)"
if "open x" for x :: "'a set"
by (metis that Compl_eq_Diff_UNIV closed_Compl double_complement mem_Collect_eq
sigma_sets.Basic sigma_sets.Compl)
then show ?thesis
unfolding borel_def
by (metis Pow_UNIV borel_closed mem_Collect_eq sets_borel sigma_eqI sigma_sets_eqI top_greatest)
qed
proposition borel_eq_countable_basis:
fixes B::"'a::topological_space set set"
assumes "countable B"
assumes "topological_basis B"
shows "borel = sigma UNIV B"
unfolding borel_def
proof (intro sigma_eqI sigma_sets_eqI, safe)
interpret countable_basis "open" B using assms by (rule countable_basis_openI)
fix X::"'a set" assume "open X"
from open_countable_basisE[OF this] obtain B' where B': "B' ⊆ B" "X = ⋃ B'" .
then show "X ∈ sigma_sets UNIV B"
by (blast intro: sigma_sets_UNION ‹countable B› countable_subset)
next
fix b assume "b ∈ B"
hence "open b" by (rule topological_basis_open[OF assms(2)])
thus "b ∈ sigma_sets UNIV (Collect open)" by auto
qed simp_all
lemma borel_measurable_continuous_on_restrict:
fixes f :: "'a::topological_space ⇒ 'b::topological_space"
assumes f: "continuous_on A f"
shows "f ∈ borel_measurable (restrict_space borel A)"
proof (rule borel_measurableI)
fix S :: "'b set" assume "open S"
with f obtain T where "f -` S ∩ A = T ∩ A" "open T"
by (metis continuous_on_open_invariant)
then show "f -` S ∩ space (restrict_space borel A) ∈ sets (restrict_space borel A)"
by (force simp add: sets_restrict_space space_restrict_space)
qed
lemma borel_measurable_continuous_onI: "continuous_on UNIV f ⟹ f ∈ borel_measurable borel"
by (drule borel_measurable_continuous_on_restrict) simp
lemma borel_measurable_continuous_on_if:
"A ∈ sets borel ⟹ continuous_on A f ⟹ continuous_on (- A) g ⟹
(λx. if x ∈ A then f x else g x) ∈ borel_measurable borel"
by (auto simp add: measurable_If_restrict_space_iff Collect_neg_eq
intro!: borel_measurable_continuous_on_restrict)
lemma borel_measurable_continuous_countable_exceptions:
fixes f :: "'a::t1_space ⇒ 'b::topological_space"
assumes X: "countable X"
assumes "continuous_on (- X) f"
shows "f ∈ borel_measurable borel"
proof (rule measurable_discrete_difference[OF _ X])
have "X ∈ sets borel"
by (rule sets.countable[OF _ X]) auto
then show "(λx. if x ∈ X then undefined else f x) ∈ borel_measurable borel"
by (intro borel_measurable_continuous_on_if assms continuous_intros)
qed auto
lemma borel_measurable_continuous_on:
assumes f: "continuous_on UNIV f" and g: "g ∈ borel_measurable M"
shows "(λx. f (g x)) ∈ borel_measurable M"
using measurable_comp[OF g borel_measurable_continuous_onI[OF f]] by (simp add: comp_def)
lemma borel_measurable_continuous_on_indicator:
fixes f g :: "'a::topological_space ⇒ 'b::real_normed_vector"
shows "A ∈ sets borel ⟹ continuous_on A f ⟹ (λx. indicator A x *⇩R f x) ∈ borel_measurable borel"
using borel_measurable_continuous_on_restrict borel_measurable_restrict_space_iff inf_top.right_neutral by blast
lemma borel_measurable_Pair[measurable (raw)]:
fixes f :: "'a ⇒ 'b::second_countable_topology" and g :: "'a ⇒ 'c::second_countable_topology"
assumes f[measurable]: "f ∈ borel_measurable M"
assumes g[measurable]: "g ∈ borel_measurable M"
shows "(λx. (f x, g x)) ∈ borel_measurable M"
proof (subst borel_eq_countable_basis)
let ?B = "SOME B::'b set set. countable B ∧ topological_basis B"
let ?C = "SOME B::'c set set. countable B ∧ topological_basis B"
let ?P = "(λ(b, c). b × c) ` (?B × ?C)"
show "countable ?P" "topological_basis ?P"
by (auto intro!: countable_basis topological_basis_prod is_basis)
show "(λx. (f x, g x)) ∈ measurable M (sigma UNIV ?P)"
proof (rule measurable_measure_of)
fix S assume "S ∈ ?P"
then obtain b c where "b ∈ ?B" "c ∈ ?C" and S: "S = b × c" by auto
then have borel: "open b" "open c"
by (auto intro: is_basis topological_basis_open)
have "(λx. (f x, g x)) -` S ∩ space M = (f -` b ∩ space M) ∩ (g -` c ∩ space M)"
unfolding S by auto
also have "… ∈ sets M"
using borel by simp
finally show "(λx. (f x, g x)) -` S ∩ space M ∈ sets M" .
qed auto
qed
lemma borel_measurable_continuous_Pair:
fixes f :: "'a ⇒ 'b::second_countable_topology" and g :: "'a ⇒ 'c::second_countable_topology"
assumes [measurable]: "f ∈ borel_measurable M"
assumes [measurable]: "g ∈ borel_measurable M"
assumes H: "continuous_on UNIV (λx. H (fst x) (snd x))"
shows "(λx. H (f x) (g x)) ∈ borel_measurable M"
proof -
have eq: "(λx. H (f x) (g x)) = (λx. (λx. H (fst x) (snd x)) (f x, g x))" by auto
show ?thesis
unfolding eq by (rule borel_measurable_continuous_on[OF H]) auto
qed
subsection ‹Borel spaces on order topologies›
lemma [measurable]:
fixes a b :: "'a::linorder_topology"
shows lessThan_borel: "{..< a} ∈ sets borel"
and greaterThan_borel: "{a <..} ∈ sets borel"
and greaterThanLessThan_borel: "{a<..<b} ∈ sets borel"
and atMost_borel: "{..a} ∈ sets borel"
and atLeast_borel: "{a..} ∈ sets borel"
and atLeastAtMost_borel: "{a..b} ∈ sets borel"
and greaterThanAtMost_borel: "{a<..b} ∈ sets borel"
and atLeastLessThan_borel: "{a..<b} ∈ sets borel"
unfolding greaterThanAtMost_def atLeastLessThan_def
by (blast intro: borel_open borel_closed open_lessThan open_greaterThan open_greaterThanLessThan
closed_atMost closed_atLeast closed_atLeastAtMost)+
lemma borel_Iio:
"borel = sigma UNIV (range lessThan :: 'a::{linorder_topology, second_countable_topology} set set)"
unfolding second_countable_borel_measurable[OF open_generated_order]
proof (intro sigma_eqI sigma_sets_eqI)
obtain D :: "'a set" where D: "countable D" "⋀X. open X ⟹ X ≠ {} ⟹ ∃d∈D. d ∈ X"
by (rule countable_dense_setE) blast
interpret L: sigma_algebra UNIV "sigma_sets UNIV (range lessThan)"
by (rule sigma_algebra_sigma_sets) simp
fix A :: "'a set" assume "A ∈ range lessThan ∪ range greaterThan"
then obtain y where "A = {y <..} ∨ A = {..< y}"
by blast
then show "A ∈ sigma_sets UNIV (range lessThan)"
proof
assume A: "A = {y <..}"
show ?thesis
proof cases
assume "∀x>y. ∃d. y < d ∧ d < x"
with D(2)[of "{y <..< x}" for x] have "∀x>y. ∃d∈D. y < d ∧ d < x"
by (auto simp: set_eq_iff)
then have "A = UNIV - (⋂d∈{d∈D. y < d}. {..< d})"
by (auto simp: A) (metis less_asym)
also have "… ∈ sigma_sets UNIV (range lessThan)"
using D(1) by (intro L.Diff L.top L.countable_INT'') auto
finally show ?thesis .
next
assume "¬ (∀x>y. ∃d. y < d ∧ d < x)"
then obtain x where "y < x" "⋀d. y < d ⟹ ¬ d < x"
by auto
then have "A = UNIV - {..< x}"
unfolding A by (auto simp: not_less[symmetric])
also have "… ∈ sigma_sets UNIV (range lessThan)"
by auto
finally show ?thesis .
qed
qed auto
qed auto
lemma borel_Ioi:
"borel = sigma UNIV (range greaterThan :: 'a::{linorder_topology, second_countable_topology} set set)"
unfolding second_countable_borel_measurable[OF open_generated_order]
proof (intro sigma_eqI sigma_sets_eqI)
obtain D :: "'a set" where D: "countable D" "⋀X. open X ⟹ X ≠ {} ⟹ ∃d∈D. d ∈ X"
by (rule countable_dense_setE) blast
interpret L: sigma_algebra UNIV "sigma_sets UNIV (range greaterThan)"
by (rule sigma_algebra_sigma_sets) simp
fix A :: "'a set" assume "A ∈ range lessThan ∪ range greaterThan"
then obtain y where "A = {y <..} ∨ A = {..< y}"
by blast
then show "A ∈ sigma_sets UNIV (range greaterThan)"
proof
assume A: "A = {..< y}"
show ?thesis
proof cases
assume "∀x<y. ∃d. x < d ∧ d < y"
with D(2)[of "{x <..< y}" for x] have "∀x<y. ∃d∈D. x < d ∧ d < y"
by (auto simp: set_eq_iff)
then have "A = UNIV - (⋂d∈{d∈D. d < y}. {d <..})"
by (auto simp: A) (metis less_asym)
also have "… ∈ sigma_sets UNIV (range greaterThan)"
using D(1) by (intro L.Diff L.top L.countable_INT'') auto
finally show ?thesis .
next
assume "¬ (∀x<y. ∃d. x < d ∧ d < y)"
then obtain x where "x < y" "⋀d. y > d ⟹ x ≥ d"
by (auto simp: not_less[symmetric])
then have "A = UNIV - {x <..}"
unfolding A Compl_eq_Diff_UNIV[symmetric] by auto
also have "… ∈ sigma_sets UNIV (range greaterThan)"
by auto
finally show ?thesis .
qed
qed auto
qed auto
lemma borel_measurableI_less:
fixes f :: "'a ⇒ 'b::{linorder_topology, second_countable_topology}"
shows "(⋀y. {x∈space M. f x < y} ∈ sets M) ⟹ f ∈ borel_measurable M"
unfolding borel_Iio
by (rule measurable_measure_of) (auto simp: Int_def conj_commute)
lemma borel_measurableI_greater:
fixes f :: "'a ⇒ 'b::{linorder_topology, second_countable_topology}"
shows "(⋀y. {x∈space M. y < f x} ∈ sets M) ⟹ f ∈ borel_measurable M"
unfolding borel_Ioi
by (rule measurable_measure_of) (auto simp: Int_def conj_commute)
lemma borel_measurableI_le:
fixes f :: "'a ⇒ 'b::{linorder_topology, second_countable_topology}"
shows "(⋀y. {x∈space M. f x ≤ y} ∈ sets M) ⟹ f ∈ borel_measurable M"
by (rule borel_measurableI_greater) (auto simp: not_le[symmetric])
lemma borel_measurableI_ge:
fixes f :: "'a ⇒ 'b::{linorder_topology, second_countable_topology}"
shows "(⋀y. {x∈space M. y ≤ f x} ∈ sets M) ⟹ f ∈ borel_measurable M"
by (rule borel_measurableI_less) (auto simp: not_le[symmetric])
lemma borel_measurable_less[measurable]:
fixes f :: "'a ⇒ 'b::{second_countable_topology, linorder_topology}"
assumes "f ∈ borel_measurable M"
assumes "g ∈ borel_measurable M"
shows "{w ∈ space M. f w < g w} ∈ sets M"
proof -
have "{w ∈ space M. f w < g w} = (λx. (f x, g x)) -` {x. fst x < snd x} ∩ space M"
by auto
also have "… ∈ sets M"
by (intro measurable_sets[OF borel_measurable_Pair borel_open, OF assms open_Collect_less]
continuous_intros)
finally show ?thesis .
qed
lemma
fixes f :: "'a ⇒ 'b::{second_countable_topology, linorder_topology}"
assumes f[measurable]: "f ∈ borel_measurable M"
assumes g[measurable]: "g ∈ borel_measurable M"
shows borel_measurable_le[measurable]: "{w ∈ space M. f w ≤ g w} ∈ sets M"
and borel_measurable_eq[measurable]: "{w ∈ space M. f w = g w} ∈ sets M"
and borel_measurable_neq: "{w ∈ space M. f w ≠ g w} ∈ sets M"
unfolding eq_iff not_less[symmetric]
by measurable
lemma borel_measurable_SUP[measurable (raw)]:
fixes F :: "_ ⇒ _ ⇒ _::{complete_linorder, linorder_topology, second_countable_topology}"
assumes [simp]: "countable I"
assumes [measurable]: "⋀i. i ∈ I ⟹ F i ∈ borel_measurable M"
shows "(λx. SUP i∈I. F i x) ∈ borel_measurable M"
by (rule borel_measurableI_greater) (simp add: less_SUP_iff)
lemma borel_measurable_INF[measurable (raw)]:
fixes F :: "_ ⇒ _ ⇒ _::{complete_linorder, linorder_topology, second_countable_topology}"
assumes [simp]: "countable I"
assumes [measurable]: "⋀i. i ∈ I ⟹ F i ∈ borel_measurable M"
shows "(λx. INF i∈I. F i x) ∈ borel_measurable M"
by (rule borel_measurableI_less) (simp add: INF_less_iff)
lemma borel_measurable_cSUP[measurable (raw)]:
fixes F :: "_ ⇒ _ ⇒ 'a::{conditionally_complete_linorder, linorder_topology, second_countable_topology}"
assumes [simp]: "countable I"
assumes [measurable]: "⋀i. i ∈ I ⟹ F i ∈ borel_measurable M"
assumes bdd: "⋀x. x ∈ space M ⟹ bdd_above ((λi. F i x) ` I)"
shows "(λx. SUP i∈I. F i x) ∈ borel_measurable M"
proof cases
assume "I = {}" then show ?thesis
by (simp add: borel_measurable_const)
next
assume "I ≠ {}"
show ?thesis
proof (rule borel_measurableI_le)
fix y
have "{x ∈ space M. ∀i∈I. F i x ≤ y} ∈ sets M"
by measurable
also have "{x ∈ space M. ∀i∈I. F i x ≤ y} = {x ∈ space M. (SUP i∈I. F i x) ≤ y}"
by (simp add: cSUP_le_iff ‹I ≠ {}› bdd cong: conj_cong)
finally show "{x ∈ space M. (SUP i∈I. F i x) ≤ y} ∈ sets M" .
qed
qed
lemma borel_measurable_cINF[measurable (raw)]:
fixes F :: "_ ⇒ _ ⇒ 'a::{conditionally_complete_linorder, linorder_topology, second_countable_topology}"
assumes [simp]: "countable I"
assumes [measurable]: "⋀i. i ∈ I ⟹ F i ∈ borel_measurable M"
assumes bdd: "⋀x. x ∈ space M ⟹ bdd_below ((λi. F i x) ` I)"
shows "(λx. INF i∈I. F i x) ∈ borel_measurable M"
proof cases
assume "I = {}" then show ?thesis
by (simp add: borel_measurable_const)
next
assume "I ≠ {}"
show ?thesis
proof (rule borel_measurableI_ge)
fix y
have "{x ∈ space M. ∀i∈I. y ≤ F i x} ∈ sets M"
by measurable
also have "{x ∈ space M. ∀i∈I. y ≤ F i x} = {x ∈ space M. y ≤ (INF i∈I. F i x)}"
by (simp add: le_cINF_iff ‹I ≠ {}› bdd cong: conj_cong)
finally show "{x ∈ space M. y ≤ (INF i∈I. F i x)} ∈ sets M" .
qed
qed
lemma borel_measurable_lfp[consumes 1, case_names continuity step]:
fixes F :: "('a ⇒ 'b) ⇒ ('a ⇒ 'b::{complete_linorder, linorder_topology, second_countable_topology})"
assumes "sup_continuous F"
assumes *: "⋀f. f ∈ borel_measurable M ⟹ F f ∈ borel_measurable M"
shows "lfp F ∈ borel_measurable M"
proof -
{ fix i have "((F ^^ i) bot) ∈ borel_measurable M"
by (induct i) (auto intro!: *) }
then have "(λx. SUP i. (F ^^ i) bot x) ∈ borel_measurable M"
by measurable
also have "(λx. SUP i. (F ^^ i) bot x) = (SUP i. (F ^^ i) bot)"
by (auto simp add: image_comp)
also have "(SUP i. (F ^^ i) bot) = lfp F"
by (rule sup_continuous_lfp[symmetric]) fact
finally show ?thesis .
qed
lemma borel_measurable_gfp[consumes 1, case_names continuity step]:
fixes F :: "('a ⇒ 'b) ⇒ ('a ⇒ 'b::{complete_linorder, linorder_topology, second_countable_topology})"
assumes "inf_continuous F"
assumes *: "⋀f. f ∈ borel_measurable M ⟹ F f ∈ borel_measurable M"
shows "gfp F ∈ borel_measurable M"
proof -
{ fix i have "((F ^^ i) top) ∈ borel_measurable M"
by (induct i) (auto intro!: * simp: bot_fun_def) }
then have "(λx. INF i. (F ^^ i) top x) ∈ borel_measurable M"
by measurable
also have "(λx. INF i. (F ^^ i) top x) = (INF i. (F ^^ i) top)"
by (auto simp add: image_comp)
also have "… = gfp F"
by (rule inf_continuous_gfp[symmetric]) fact
finally show ?thesis .
qed
lemma borel_measurable_max[measurable (raw)]:
"f ∈ borel_measurable M ⟹ g ∈ borel_measurable M ⟹ (λx. max (g x) (f x) :: 'b::{second_countable_topology, linorder_topology}) ∈ borel_measurable M"
by (rule borel_measurableI_less) simp
lemma borel_measurable_min[measurable (raw)]:
"f ∈ borel_measurable M ⟹ g ∈ borel_measurable M ⟹ (λx. min (g x) (f x) :: 'b::{second_countable_topology, linorder_topology}) ∈ borel_measurable M"
by (rule borel_measurableI_greater) simp
lemma borel_measurable_Min[measurable (raw)]:
"finite I ⟹ (⋀i. i ∈ I ⟹ f i ∈ borel_measurable M) ⟹ (λx. Min ((λi. f i x)`I) :: 'b::{second_countable_topology, linorder_topology}) ∈ borel_measurable M"
proof (induct I rule: finite_induct)
case (insert i I) then show ?case
by (cases "I = {}") auto
qed auto
lemma borel_measurable_Max[measurable (raw)]:
"finite I ⟹ (⋀i. i ∈ I ⟹ f i ∈ borel_measurable M) ⟹ (λx. Max ((λi. f i x)`I) :: 'b::{second_countable_topology, linorder_topology}) ∈ borel_measurable M"
proof (induct I rule: finite_induct)
case (insert i I) then show ?case
by (cases "I = {}") auto
qed auto
lemma borel_measurable_sup[measurable (raw)]:
"f ∈ borel_measurable M ⟹ g ∈ borel_measurable M ⟹ (λx. sup (g x) (f x) :: 'b::{lattice, second_countable_topology, linorder_topology}) ∈ borel_measurable M"
unfolding sup_max by measurable
lemma borel_measurable_inf[measurable (raw)]:
"f ∈ borel_measurable M ⟹ g ∈ borel_measurable M ⟹ (λx. inf (g x) (f x) :: 'b::{lattice, second_countable_topology, linorder_topology}) ∈ borel_measurable M"
unfolding inf_min by measurable
lemma [measurable (raw)]:
fixes f :: "nat ⇒ 'a ⇒ 'b::{complete_linorder, second_countable_topology, linorder_topology}"
assumes "⋀i. f i ∈ borel_measurable M"
shows borel_measurable_liminf: "(λx. liminf (λi. f i x)) ∈ borel_measurable M"
and borel_measurable_limsup: "(λx. limsup (λi. f i x)) ∈ borel_measurable M"
unfolding liminf_SUP_INF limsup_INF_SUP using assms by auto
lemma measurable_convergent[measurable (raw)]:
fixes f :: "nat ⇒ 'a ⇒ 'b::{complete_linorder, second_countable_topology, linorder_topology}"
assumes [measurable]: "⋀i. f i ∈ borel_measurable M"
shows "Measurable.pred M (λx. convergent (λi. f i x))"
unfolding convergent_ereal by measurable
lemma sets_Collect_convergent[measurable]:
fixes f :: "nat ⇒ 'a ⇒ 'b::{complete_linorder, second_countable_topology, linorder_topology}"
assumes f[measurable]: "⋀i. f i ∈ borel_measurable M"
shows "{x∈space M. convergent (λi. f i x)} ∈ sets M"
by measurable
lemma borel_measurable_lim[measurable (raw)]:
fixes f :: "nat ⇒ 'a ⇒ 'b::{complete_linorder, second_countable_topology, linorder_topology}"
assumes [measurable]: "⋀i. f i ∈ borel_measurable M"
shows "(λx. lim (λi. f i x)) ∈ borel_measurable M"
proof -
have "⋀x. lim (λi. f i x) = (if convergent (λi. f i x) then limsup (λi. f i x) else (THE i. False))"
by (simp add: lim_def convergent_def convergent_limsup_cl)
then show ?thesis
by simp
qed
lemma borel_measurable_LIMSEQ_order:
fixes u :: "nat ⇒ 'a ⇒ 'b::{complete_linorder, second_countable_topology, linorder_topology}"
assumes u': "⋀x. x ∈ space M ⟹ (λi. u i x) ⇢ u' x"
and u: "⋀i. u i ∈ borel_measurable M"
shows "u' ∈ borel_measurable M"
proof -
have "⋀x. x ∈ space M ⟹ u' x = liminf (λn. u n x)"
using u' by (simp add: lim_imp_Liminf[symmetric])
with u show ?thesis by (simp cong: measurable_cong)
qed
subsection ‹Borel spaces on topological monoids›
lemma borel_measurable_add[measurable (raw)]:
fixes f g :: "'a ⇒ 'b::{second_countable_topology, topological_monoid_add}"
assumes f: "f ∈ borel_measurable M"
assumes g: "g ∈ borel_measurable M"
shows "(λx. f x + g x) ∈ borel_measurable M"
using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros)
lemma borel_measurable_sum[measurable (raw)]:
fixes f :: "'c ⇒ 'a ⇒ 'b::{second_countable_topology, topological_comm_monoid_add}"
assumes "⋀i. i ∈ S ⟹ f i ∈ borel_measurable M"
shows "(λx. ∑i∈S. f i x) ∈ borel_measurable M"
proof cases
assume "finite S"
thus ?thesis using assms by induct auto
qed simp
lemma borel_measurable_suminf_order[measurable (raw)]:
fixes f :: "nat ⇒ 'a ⇒ 'b::{complete_linorder, second_countable_topology, linorder_topology, topological_comm_monoid_add}"
assumes f[measurable]: "⋀i. f i ∈ borel_measurable M"
shows "(λx. suminf (λi. f i x)) ∈ borel_measurable M"
unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp
subsection ‹Borel spaces on Euclidean spaces›
lemma borel_measurable_inner[measurable (raw)]:
fixes f g :: "'a ⇒ 'b::{second_countable_topology, real_inner}"
assumes "f ∈ borel_measurable M"
assumes "g ∈ borel_measurable M"
shows "(λx. f x ∙ g x) ∈ borel_measurable M"
using assms
by (rule borel_measurable_continuous_Pair) (intro continuous_intros)
notation
eucl_less (infix "<e" 50)
lemma box_oc: "{x. a <e x ∧ x ≤ b} = {x. a <e x} ∩ {..b}"
and box_co: "{x. a ≤ x ∧ x <e b} = {a..} ∩ {x. x <e b}"
by auto
lemma eucl_ivals[measurable]:
fixes a b :: "'a::ordered_euclidean_space"
shows "{x. x <e a} ∈ sets borel"
and "{x. a <e x} ∈ sets borel"
and "{..a} ∈ sets borel"
and "{a..} ∈ sets borel"
and "{a..b} ∈ sets borel"
and "{x. a <e x ∧ x ≤ b} ∈ sets borel"
and "{x. a ≤ x ∧ x <e b} ∈ sets borel"
unfolding box_oc box_co
by (auto intro: borel_open borel_closed)
lemma
fixes i :: "'a::{second_countable_topology, real_inner}"
shows hafspace_less_borel: "{x. a < x ∙ i} ∈ sets borel"
and hafspace_greater_borel: "{x. x ∙ i < a} ∈ sets borel"
and hafspace_less_eq_borel: "{x. a ≤ x ∙ i} ∈ sets borel"
and hafspace_greater_eq_borel: "{x. x ∙ i ≤ a} ∈ sets borel"
by simp_all
lemma borel_eq_box:
"borel = sigma UNIV (range (λ (a, b). box a b :: 'a :: euclidean_space set))"
(is "_ = ?SIGMA")
proof (rule borel_eq_sigmaI1[OF borel_def])
fix M :: "'a set" assume "M ∈ {S. open S}"
then have "open M" by simp
show "M ∈ ?SIGMA"
apply (subst open_UNION_box[OF ‹open M›])
apply (safe intro!: sets.countable_UN' countable_PiE countable_Collect)
apply (auto intro: countable_rat)
done
qed (auto simp: box_def)
lemma halfspace_gt_in_halfspace:
assumes i: "i ∈ A"
shows "{x::'a. a < x ∙ i} ∈
sigma_sets UNIV ((λ (a, i). {x::'a::euclidean_space. x ∙ i < a}) ` (UNIV × A))"
(is "?set ∈ ?SIGMA")
proof -
interpret sigma_algebra UNIV ?SIGMA
by (intro sigma_algebra_sigma_sets) simp_all
have *: "?set = (⋃n. UNIV - {x::'a. x ∙ i < a + 1 / real (Suc n)})"
proof (safe, simp_all add: not_less del: of_nat_Suc)
fix x :: 'a assume "a < x ∙ i"
with reals_Archimedean[of "x ∙ i - a"]
obtain n where "a + 1 / real (Suc n) < x ∙ i"
by (auto simp: field_simps)
then show "∃n. a + 1 / real (Suc n) ≤ x ∙ i"
by (blast intro: less_imp_le)
next
fix x n
have "a < a + 1 / real (Suc n)" by auto
also assume "… ≤ x"
finally show "a < x" .
qed
show "?set ∈ ?SIGMA" unfolding *
by (auto intro!: Diff sigma_sets_Inter i)
qed
lemma borel_eq_halfspace_less:
"borel = sigma UNIV ((λ(a, i). {x::'a::euclidean_space. x ∙ i < a}) ` (UNIV × Basis))"
(is "_ = ?SIGMA")
proof (rule borel_eq_sigmaI2[OF borel_eq_box])
fix a b :: 'a
have "box a b = {x∈space ?SIGMA. ∀i∈Basis. a ∙ i < x ∙ i ∧ x ∙ i < b ∙ i}"
by (auto simp: box_def)
also have "… ∈ sets ?SIGMA"
by (intro sets.sets_Collect_conj sets.sets_Collect_finite_All sets.sets_Collect_const)
(auto intro!: halfspace_gt_in_halfspace countable_PiE countable_rat)
finally show "box a b ∈ sets ?SIGMA" .
qed auto
lemma borel_eq_halfspace_le:
"borel = sigma UNIV ((λ (a, i). {x::'a::euclidean_space. x ∙ i ≤ a}) ` (UNIV × Basis))"
(is "_ = ?SIGMA")
proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_less])
fix a :: real and i :: 'a assume "(a, i) ∈ UNIV × Basis"
then have i: "i ∈ Basis" by auto
have *: "{x::'a. x∙i < a} = (⋃n. {x. x∙i ≤ a - 1/real (Suc n)})"
proof (safe, simp_all del: of_nat_Suc)
fix x::'a assume *: "x∙i < a"
with reals_Archimedean[of "a - x∙i"]
obtain n where "x ∙ i < a - 1 / (real (Suc n))"
by (auto simp: field_simps)
then show "∃n. x ∙ i ≤ a - 1 / (real (Suc n))"
by (blast intro: less_imp_le)
next
fix x::'a and n
assume "x∙i ≤ a - 1 / real (Suc n)"
also have "… < a" by auto
finally show "x∙i < a" .
qed
show "{x. x∙i < a} ∈ ?SIGMA" unfolding *
by (intro sets.countable_UN) (auto intro: i)
qed auto
lemma borel_eq_halfspace_ge:
"borel = sigma UNIV ((λ (a, i). {x::'a::euclidean_space. a ≤ x ∙ i}) ` (UNIV × Basis))"
(is "_ = ?SIGMA")
proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_less])
fix a :: real and i :: 'a assume i: "(a, i) ∈ UNIV × Basis"
have *: "{x::'a. x∙i < a} = space ?SIGMA - {x::'a. a ≤ x∙i}" by auto
show "{x. x∙i < a} ∈ ?SIGMA" unfolding *
using i by (intro sets.compl_sets) auto
qed auto
lemma borel_eq_halfspace_greater:
"borel = sigma UNIV ((λ (a, i). {x::'a::euclidean_space. a < x ∙ i}) ` (UNIV × Basis))"
(is "_ = ?SIGMA")
proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_le])
fix a :: real and i :: 'a assume "(a, i) ∈ (UNIV × Basis)"
then have i: "i ∈ Basis" by auto
have *: "{x::'a. x∙i ≤ a} = space ?SIGMA - {x::'a. a < x∙i}" by auto
show "{x. x∙i ≤ a} ∈ ?SIGMA" unfolding *
by (intro sets.compl_sets) (auto intro: i)
qed auto
lemma borel_eq_atMost:
"borel = sigma UNIV (range (λa. {..a::'a::ordered_euclidean_space}))"
(is "_ = ?SIGMA")
proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_le])
fix a :: real and i :: 'a assume "(a, i) ∈ UNIV × Basis"
then have "i ∈ Basis" by auto
then have *: "{x::'a. x∙i ≤ a} = (⋃k::nat. {.. (∑n∈Basis. (if n = i then a else real k)*⇩R n)})"
proof (safe, simp_all add: eucl_le[where 'a='a] split: if_split_asm)
fix x :: 'a
obtain k where "Max ((∙) x ` Basis) ≤ real k"
using real_arch_simple by blast
then have "⋀i. i ∈ Basis ⟹ x∙i ≤ real k"
by (subst (asm) Max_le_iff) auto
then show "∃k::nat. ∀ia∈Basis. ia ≠ i ⟶ x ∙ ia ≤ real k"
by (auto intro!: exI[of _ k])
qed
show "{x. x∙i ≤ a} ∈ ?SIGMA" unfolding *
by (intro sets.countable_UN) auto
qed auto
lemma borel_eq_greaterThan:
"borel = sigma UNIV (range (λa::'a::ordered_euclidean_space. {x. a <e x}))"
(is "_ = ?SIGMA")
proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_le])
fix a :: real and i :: 'a assume "(a, i) ∈ UNIV × Basis"
then have i: "i ∈ Basis" by auto
have **: "∃y. ∀j∈Basis. j ≠ i ⟶ - real y < x ∙ j" if "a < x ∙ i" for x
proof -
obtain k where k: "Max ((∙) (- x) ` Basis) < real k"
using reals_Archimedean2 by blast
{ fix i :: 'a assume "i ∈ Basis"
then have "-x∙i < real k"
using k by (subst (asm) Max_less_iff) auto
then have "- real k < x∙i" by simp }
then show ?thesis
by (auto intro!: exI[of _ k])
qed
have "{x::'a. x∙i ≤ a} = UNIV - {x::'a. a < x∙i}" by auto
also have *: "{x::'a. a < x∙i} = (⋃k::nat. {x. (∑n∈Basis. (if n = i then a else -k) *⇩R n) <e x})"
using i ** by (force simp add: eucl_less_def split: if_split_asm)
finally have eq: "{x. x ∙ i ≤ a} = UNIV - (⋃x. {xa. (∑n∈Basis. (if n = i then a else - real x) *⇩R n) <e xa})" .
show "{x. x∙i ≤ a} ∈ ?SIGMA"
unfolding eq by (fastforce intro!: sigma_sets_top sets.Diff)
qed auto
lemma borel_eq_lessThan:
"borel = sigma UNIV (range (λa::'a::ordered_euclidean_space. {x. x <e a}))"
(is "_ = ?SIGMA")
proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_ge])
fix a :: real and i :: 'a assume "(a, i) ∈ UNIV × Basis"
then have i: "i ∈ Basis" by auto
have **: "∃y. ∀j∈Basis. j ≠ i ⟶ real y > x ∙ j" if "a > x ∙ i" for x
proof -
obtain k where k: "Max ((∙) x ` Basis) < real k"
using reals_Archimedean2 by blast
{ fix i :: 'a assume "i ∈ Basis"
then have "x∙i < real k"
using k by (subst (asm) Max_less_iff) auto
then have "x∙i < real k" by simp }
then show ?thesis
by (auto intro!: exI[of _ k])
qed
have "{x::'a. a ≤ x∙i} = UNIV - {x::'a. x∙i < a}" by auto
also have *: "{x::'a. x∙i < a} = (⋃k::nat. {x. x <e (∑n∈Basis. (if n = i then a else real k) *⇩R n)})" using ‹i∈ Basis›
using i ** by (force simp add: eucl_less_def split: if_split_asm)
finally
have eq: "{x. a ≤ x ∙ i} =
UNIV - (⋃k. {x. x <e (∑n∈Basis. (if n = i then a else real k) *⇩R n)})" .
show "{x. a ≤ x∙i} ∈ ?SIGMA"
unfolding eq by (fastforce intro!: sigma_sets_top sets.Diff)
qed auto
lemma borel_eq_atLeastAtMost:
"borel = sigma UNIV (range (λ(a,b). {a..b} ::'a::ordered_euclidean_space set))"
(is "_ = ?SIGMA")
proof (rule borel_eq_sigmaI5[OF borel_eq_atMost])
fix a::'a
have *: "{..a} = (⋃n::nat. {- real n *⇩R One .. a})"
proof (safe, simp_all add: eucl_le[where 'a='a])
fix x :: 'a
obtain k where k: "Max ((∙) (- x) ` Basis) ≤ real k"
using real_arch_simple by blast
{ fix i :: 'a assume "i ∈ Basis"
with k have "- x∙i ≤ real k"
by (subst (asm) Max_le_iff) (auto simp: field_simps)
then have "- real k ≤ x∙i" by simp }
then show "∃n::nat. ∀i∈Basis. - real n ≤ x ∙ i"
by (auto intro!: exI[of _ k])
qed
show "{..a} ∈ ?SIGMA" unfolding *
by (intro sets.countable_UN)
(auto intro!: sigma_sets_top)
qed auto
lemma borel_set_induct[consumes 1, case_names empty interval compl union]:
assumes "A ∈ sets borel"
assumes empty: "P {}" and int: "⋀a b. a ≤ b ⟹ P {a..b}" and compl: "⋀A. A ∈ sets borel ⟹ P A ⟹ P (-A)" and
un: "⋀f. disjoint_family f ⟹ (⋀i. f i ∈ sets borel) ⟹ (⋀i. P (f i)) ⟹ P (⋃i::nat. f i)"
shows "P (A::real set)"
proof -
let ?G = "range (λ(a,b). {a..b::real})"
have "Int_stable ?G" "?G ⊆ Pow UNIV" "A ∈ sigma_sets UNIV ?G"
using assms(1) by (auto simp add: borel_eq_atLeastAtMost Int_stable_def)
thus ?thesis
proof (induction rule: sigma_sets_induct_disjoint)
case (union f)
from union.hyps(2) have "⋀i. f i ∈ sets borel" by (auto simp: borel_eq_atLeastAtMost)
with union show ?case by (auto intro: un)
next
case (basic A)
then obtain a b where "A = {a .. b}" by auto
then show ?case
by (cases "a ≤ b") (auto intro: int empty)
qed (auto intro: empty compl simp: Compl_eq_Diff_UNIV[symmetric] borel_eq_atLeastAtMost)
qed
lemma borel_sigma_sets_Ioc: "borel = sigma UNIV (range (λ(a, b). {a <.. b::real}))"
proof (rule borel_eq_sigmaI5[OF borel_eq_atMost])
fix i :: real
have "{..i} = (⋃j::nat. {-j <.. i})"
by (auto simp: minus_less_iff reals_Archimedean2)
also have "… ∈ sets (sigma UNIV (range (λ(i, j). {i<..j})))"
by (intro sets.countable_nat_UN) auto
finally show "{..i} ∈ sets (sigma UNIV (range (λ(i, j). {i<..j})))" .
qed simp
lemma eucl_lessThan: "{x::real. x <e a} = lessThan a"
by (simp add: eucl_less_def lessThan_def)
lemma borel_eq_atLeastLessThan:
"borel = sigma UNIV (range (λ(a, b). {a ..< b :: real}))" (is "_ = ?SIGMA")
proof (rule borel_eq_sigmaI5[OF borel_eq_lessThan])
have move_uminus: "⋀x y::real. -x ≤ y ⟷ -y ≤ x" by auto
fix x :: real
have "{..<x} = (⋃i::nat. {-real i ..< x})"
by (auto simp: move_uminus real_arch_simple)
then show "{y. y <e x} ∈ ?SIGMA"
by (auto intro: sigma_sets.intros(2-) simp: eucl_lessThan)
qed auto
lemma borel_measurable_halfspacesI:
fixes f :: "'a ⇒ 'c::euclidean_space"
assumes F: "borel = sigma UNIV (F ` (UNIV × Basis))"
and S_eq: "⋀a i. S a i = f -` F (a,i) ∩ space M"
shows "f ∈ borel_measurable M = (∀i∈Basis. ∀a::real. S a i ∈ sets M)"
proof safe
fix a :: real and i :: 'b assume i: "i ∈ Basis" and f: "f ∈ borel_measurable M"
then show "S a i ∈ sets M" unfolding assms
by (auto intro!: measurable_sets simp: assms(1))
next
assume a: "∀i∈Basis. ∀a. S a i ∈ sets M"
then show "f ∈ borel_measurable M"
by (auto intro!: measurable_measure_of simp: S_eq F)
qed
lemma borel_measurable_iff_halfspace_le:
fixes f :: "'a ⇒ 'c::euclidean_space"
shows "f ∈ borel_measurable M = (∀i∈Basis. ∀a. {w ∈ space M. f w ∙ i ≤ a} ∈ sets M)"
by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_le]) auto
lemma borel_measurable_iff_halfspace_less:
fixes f :: "'a ⇒ 'c::euclidean_space"
shows "f ∈ borel_measurable M ⟷ (∀i∈Basis. ∀a. {w ∈ space M. f w ∙ i < a} ∈ sets M)"
by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_less]) auto
lemma borel_measurable_iff_halfspace_ge:
fixes f :: "'a ⇒ 'c::euclidean_space"
shows "f ∈ borel_measurable M = (∀i∈Basis. ∀a. {w ∈ space M. a ≤ f w ∙ i} ∈ sets M)"
by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_ge]) auto
lemma borel_measurable_iff_halfspace_greater:
fixes f :: "'a ⇒ 'c::euclidean_space"
shows "f ∈ borel_measurable M ⟷ (∀i∈Basis. ∀a. {w ∈ space M. a < f w ∙ i} ∈ sets M)"
by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_greater]) auto
lemma borel_measurable_iff_le:
"(f::'a ⇒ real) ∈ borel_measurable M = (∀a. {w ∈ space M. f w ≤ a} ∈ sets M)"
using borel_measurable_iff_halfspace_le[where 'c=real] by simp
lemma borel_measurable_iff_less:
"(f::'a ⇒ real) ∈ borel_measurable M = (∀a. {w ∈ space M. f w < a} ∈ sets M)"
using borel_measurable_iff_halfspace_less[where 'c=real] by simp
lemma borel_measurable_iff_ge:
"(f::'a ⇒ real) ∈ borel_measurable M = (∀a. {w ∈ space M. a ≤ f w} ∈ sets M)"
using borel_measurable_iff_halfspace_ge[where 'c=real]
by simp
lemma borel_measurable_iff_greater:
"(f::'a ⇒ real) ∈ borel_measurable M = (∀a. {w ∈ space M. a < f w} ∈ sets M)"
using borel_measurable_iff_halfspace_greater[where 'c=real] by simp
lemma borel_measurable_euclidean_space:
fixes f :: "'a ⇒ 'c::euclidean_space"
shows "f ∈ borel_measurable M ⟷ (∀i∈Basis. (λx. f x ∙ i) ∈ borel_measurable M)"
proof safe
assume f: "∀i∈Basis. (λx. f x ∙ i) ∈ borel_measurable M"
then show "f ∈ borel_measurable M"
by (subst borel_measurable_iff_halfspace_le) auto
qed auto
subsection "Borel measurable operators"
lemma borel_measurable_norm[measurable]: "norm ∈ borel_measurable borel"
by (intro borel_measurable_continuous_onI continuous_intros)
lemma borel_measurable_sgn [measurable]: "(sgn::'a::real_normed_vector ⇒ 'a) ∈ borel_measurable borel"
by (rule borel_measurable_continuous_countable_exceptions[where X="{0}"])
(auto intro!: continuous_on_sgn continuous_on_id)
lemma borel_measurable_uminus[measurable (raw)]:
fixes g :: "'a ⇒ 'b::{second_countable_topology, real_normed_vector}"
assumes g: "g ∈ borel_measurable M"
shows "(λx. - g x) ∈ borel_measurable M"
by (rule borel_measurable_continuous_on[OF _ g]) (intro continuous_intros)
lemma borel_measurable_diff[measurable (raw)]:
fixes f :: "'a ⇒ 'b::{second_countable_topology, real_normed_vector}"
assumes f: "f ∈ borel_measurable M"
assumes g: "g ∈ borel_measurable M"
shows "(λx. f x - g x) ∈ borel_measurable M"
using borel_measurable_add [of f M "- g"] assms by (simp add: fun_Compl_def)
lemma borel_measurable_times[measurable (raw)]:
fixes f :: "'a ⇒ 'b::{second_countable_topology, real_normed_algebra}"
assumes f: "f ∈ borel_measurable M"
assumes g: "g ∈ borel_measurable M"
shows "(λx. f x * g x) ∈ borel_measurable M"
using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros)
lemma borel_measurable_prod[measurable (raw)]:
fixes f :: "'c ⇒ 'a ⇒ 'b::{second_countable_topology, real_normed_field}"
assumes "⋀i. i ∈ S ⟹ f i ∈ borel_measurable M"
shows "(λx. ∏i∈S. f i x) ∈ borel_measurable M"
proof cases
assume "finite S"
thus ?thesis using assms by induct auto
qed simp
lemma borel_measurable_dist[measurable (raw)]:
fixes g f :: "'a ⇒ 'b::{second_countable_topology, metric_space}"
assumes f: "f ∈ borel_measurable M"
assumes g: "g ∈ borel_measurable M"
shows "(λx. dist (f x) (g x)) ∈ borel_measurable M"
using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros)
lemma borel_measurable_scaleR[measurable (raw)]:
fixes g :: "'a ⇒ 'b::{second_countable_topology, real_normed_vector}"
assumes f: "f ∈ borel_measurable M"
assumes g: "g ∈ borel_measurable M"
shows "(λx. f x *⇩R g x) ∈ borel_measurable M"
using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros)
lemma borel_measurable_uminus_eq [simp]:
fixes f :: "'a ⇒ 'b::{second_countable_topology, real_normed_vector}"
shows "(λx. - f x) ∈ borel_measurable M ⟷ f ∈ borel_measurable M" (is "?l = ?r")
by (smt (verit, ccfv_SIG) borel_measurable_uminus equation_minus_iff measurable_cong)
lemma affine_borel_measurable_vector:
fixes f :: "'a ⇒ 'x::real_normed_vector"
assumes "f ∈ borel_measurable M"
shows "(λx. a + b *⇩R f x) ∈ borel_measurable M"
proof (rule borel_measurableI)
fix S :: "'x set" assume "open S"
show "(λx. a + b *⇩R f x) -` S ∩ space M ∈ sets M"
proof cases
assume "b ≠ 0"
with ‹open S› have "open ((λx. (- a + x) /⇩R b) ` S)" (is "open ?S")
using open_affinity [of S "inverse b" "- a /⇩R b"]
by (auto simp: algebra_simps)
hence "?S ∈ sets borel" by auto
moreover
have "⋀x. ⟦a + b *⇩R f x ∈ S⟧ ⟹ f x ∈ (λx. (x - a) /⇩R b) ` S"
using ‹b ≠ 0› image_iff by fastforce
with ‹b ≠ 0› have "(λx. a + b *⇩R f x) -` S = f -` ?S"
by auto
ultimately show ?thesis using assms unfolding in_borel_measurable_borel
by auto
qed simp
qed
lemma borel_measurable_const_scaleR[measurable (raw)]:
"f ∈ borel_measurable M ⟹ (λx. b *⇩R f x ::'a::real_normed_vector) ∈ borel_measurable M"
using affine_borel_measurable_vector[of f M 0 b] by simp
lemma borel_measurable_const_add[measurable (raw)]:
"f ∈ borel_measurable M ⟹ (λx. a + f x ::'a::real_normed_vector) ∈ borel_measurable M"
using affine_borel_measurable_vector[of f M a 1] by simp
lemma borel_measurable_inverse[measurable (raw)]:
fixes f :: "'a ⇒ 'b::real_normed_div_algebra"
assumes f: "f ∈ borel_measurable M"
shows "(λx. inverse (f x)) ∈ borel_measurable M"
proof -
have "countable {0::'b}" "continuous_on (- {0::'b}) inverse"
by (auto intro!: continuous_on_inverse continuous_on_id)
then show ?thesis
by (metis borel_measurable_continuous_countable_exceptions f measurable_compose)
qed
lemma borel_measurable_divide[measurable (raw)]:
"f ∈ borel_measurable M ⟹ g ∈ borel_measurable M ⟹
(λx. f x / g x::'b::{second_countable_topology, real_normed_div_algebra}) ∈ borel_measurable M"
by (simp add: divide_inverse)
lemma borel_measurable_abs[measurable (raw)]:
"f ∈ borel_measurable M ⟹ (λx. ¦f x :: real¦) ∈ borel_measurable M"
unfolding abs_real_def by simp
lemma borel_measurable_nth[measurable (raw)]:
"(λx::real^'n. x $ i) ∈ borel_measurable borel"
by (simp add: cart_eq_inner_axis)
lemma convex_measurable:
fixes A :: "'a :: euclidean_space set"
shows "X ∈ borel_measurable M ⟹ X ` space M ⊆ A ⟹ open A ⟹ convex_on A q ⟹
(λx. q (X x)) ∈ borel_measurable M"
by (rule measurable_compose[where f=X and N="restrict_space borel A"])
(auto intro!: borel_measurable_continuous_on_restrict convex_on_continuous measurable_restrict_space2)
lemma borel_measurable_ln[measurable (raw)]:
assumes f: "f ∈ borel_measurable M"
shows "(λx. ln (f x :: real)) ∈ borel_measurable M"
using borel_measurable_continuous_countable_exceptions[of "{0}"] measurable_compose[OF f]
by (auto intro!: continuous_on_ln continuous_on_id)
lemma borel_measurable_log[measurable (raw)]:
"f ∈ borel_measurable M ⟹ g ∈ borel_measurable M ⟹ (λx. log (g x) (f x)) ∈ borel_measurable M"
unfolding log_def by auto
lemma borel_measurable_exp[measurable]:
"(exp::'a::{real_normed_field,banach}⇒'a) ∈ borel_measurable borel"
by (intro borel_measurable_continuous_onI continuous_at_imp_continuous_on ballI isCont_exp)
lemma measurable_real_floor[measurable]:
"(floor :: real ⇒ int) ∈ measurable borel (count_space UNIV)"
proof -
have "⋀a x. ⌊x⌋ = a ⟷ (real_of_int a ≤ x ∧ x < real_of_int (a + 1))"
by (auto intro: floor_eq2)
then show ?thesis
by (auto simp: vimage_def measurable_count_space_eq2_countable)
qed
lemma measurable_real_ceiling[measurable]:
"(ceiling :: real ⇒ int) ∈ measurable borel (count_space UNIV)"
unfolding ceiling_def[abs_def] by simp
lemma borel_measurable_real_floor: "(λx::real. real_of_int ⌊x⌋) ∈ borel_measurable borel"
by simp
lemma borel_measurable_root [measurable]: "root n ∈ borel_measurable borel"
by (intro borel_measurable_continuous_onI continuous_intros)
lemma borel_measurable_sqrt [measurable]: "sqrt ∈ borel_measurable borel"
by (intro borel_measurable_continuous_onI continuous_intros)
lemma borel_measurable_power [measurable (raw)]:
fixes f :: "_ ⇒ 'b::{power,real_normed_algebra}"
assumes f: "f ∈ borel_measurable M"
shows "(λx. (f x) ^ n) ∈ borel_measurable M"
by (intro borel_measurable_continuous_on [OF _ f] continuous_intros)
lemma borel_measurable_Re [measurable]: "Re ∈ borel_measurable borel"
by (intro borel_measurable_continuous_onI continuous_intros)
lemma borel_measurable_Im [measurable]: "Im ∈ borel_measurable borel"
by (intro borel_measurable_continuous_onI continuous_intros)
lemma borel_measurable_of_real [measurable]: "(of_real :: _ ⇒ (_::real_normed_algebra)) ∈ borel_measurable borel"
by (intro borel_measurable_continuous_onI continuous_intros)
lemma borel_measurable_sin [measurable]: "(sin :: _ ⇒ (_::{real_normed_field,banach})) ∈ borel_measurable borel"
by (intro borel_measurable_continuous_onI continuous_intros)
lemma borel_measurable_cos [measurable]: "(cos :: _ ⇒ (_::{real_normed_field,banach})) ∈ borel_measurable borel"
by (intro borel_measurable_continuous_onI continuous_intros)
lemma borel_measurable_arctan [measurable]: "arctan ∈ borel_measurable borel"
by (intro borel_measurable_continuous_onI continuous_intros)
lemma borel_measurable_complex_iff:
"f ∈ borel_measurable M ⟷
(λx. Re (f x)) ∈ borel_measurable M ∧ (λx. Im (f x)) ∈ borel_measurable M" (is "?lhs ⟷ ?rhs")
proof
show "?lhs ⟹ ?rhs"
using borel_measurable_Im borel_measurable_Re measurable_compose by blast
assume R: ?rhs
then have "(λx. complex_of_real (Re (f x)) + 𝗂 * complex_of_real (Im (f x))) ∈ borel_measurable M"
by (intro borel_measurable_add) auto
then show ?lhs
using complex_eq by force
qed
lemma powr_real_measurable [measurable]:
assumes "f ∈ measurable M borel" "g ∈ measurable M borel"
shows "(λx. f x powr g x :: real) ∈ measurable M borel"
using assms by (simp_all add: powr_def)
lemma measurable_of_bool[measurable]: "of_bool ∈ count_space UNIV →⇩M borel"
by simp
subsection "Borel space on the extended reals"
lemma borel_measurable_ereal[measurable (raw)]:
assumes f: "f ∈ borel_measurable M" shows "(λx. ereal (f x)) ∈ borel_measurable M"
using continuous_on_ereal f by (rule borel_measurable_continuous_on) (rule continuous_on_id)
lemma borel_measurable_real_of_ereal[measurable (raw)]:
fixes f :: "'a ⇒ ereal"
assumes f: "f ∈ borel_measurable M"
shows "(λx. real_of_ereal (f x)) ∈ borel_measurable M"
using measurable_compose[OF f] borel_measurable_continuous_countable_exceptions[of "{∞, -∞ }"]
by (auto intro: continuous_on_real simp: Compl_eq_Diff_UNIV)
lemma borel_measurable_ereal_cases:
fixes f :: "'a ⇒ ereal"
assumes f: "f ∈ borel_measurable M"
assumes H: "(λx. H (ereal (real_of_ereal (f x)))) ∈ borel_measurable M"
shows "(λx. H (f x)) ∈ borel_measurable M"
proof -
let ?F = "λx. if f x = ∞ then H ∞ else if f x = - ∞ then H (-∞) else H (ereal (real_of_ereal (f x)))"
{ fix x have "H (f x) = ?F x" by (cases "f x") auto }
with f H show ?thesis by simp
qed
lemma
fixes f :: "'a ⇒ ereal" assumes f[measurable]: "f ∈ borel_measurable M"
shows borel_measurable_ereal_abs[measurable(raw)]: "(λx. ¦f x¦) ∈ borel_measurable M"
and borel_measurable_ereal_inverse[measurable(raw)]: "(λx. inverse (f x) :: ereal) ∈ borel_measurable M"
and borel_measurable_uminus_ereal[measurable(raw)]: "(λx. - f x :: ereal) ∈ borel_measurable M"
by (auto simp del: abs_real_of_ereal simp: borel_measurable_ereal_cases[OF f] measurable_If)
lemma borel_measurable_uminus_eq_ereal[simp]:
"(λx. - f x :: ereal) ∈ borel_measurable M ⟷ f ∈ borel_measurable M"
by (smt (verit, ccfv_SIG) borel_measurable_uminus_ereal ereal_uminus_uminus measurable_cong)
lemma set_Collect_ereal2:
fixes f g :: "'a ⇒ ereal"
assumes f: "f ∈ borel_measurable M"
assumes g: "g ∈ borel_measurable M"
assumes H: "{x ∈ space M. H (ereal (real_of_ereal (f x))) (ereal (real_of_ereal (g x)))} ∈ sets M"
"{x ∈ space borel. H (-∞) (ereal x)} ∈ sets borel"
"{x ∈ space borel. H (∞) (ereal x)} ∈ sets borel"
"{x ∈ space borel. H (ereal x) (-∞)} ∈ sets borel"
"{x ∈ space borel. H (ereal x) (∞)} ∈ sets borel"
shows "{x ∈ space M. H (f x) (g x)} ∈ sets M"
proof -
let ?G = "λy x. if g x = ∞ then H y ∞ else if g x = -∞ then H y (-∞) else H y (ereal (real_of_ereal (g x)))"
let ?F = "λx. if f x = ∞ then ?G ∞ x else if f x = -∞ then ?G (-∞) x else ?G (ereal (real_of_ereal (f x))) x"
{ fix x have "H (f x) (g x) = ?F x" by (cases "f x" "g x" rule: ereal2_cases) auto }
note * = this
from assms show ?thesis
by (subst *) (simp del: space_borel split del: if_split)
qed
lemma borel_measurable_ereal_iff:
shows "(λx. ereal (f x)) ∈ borel_measurable M ⟷ f ∈ borel_measurable M"
proof
assume "(λx. ereal (f x)) ∈ borel_measurable M"
from borel_measurable_real_of_ereal[OF this]
show "f ∈ borel_measurable M" by auto
qed auto
lemma borel_measurable_erealD[measurable_dest]:
"(λx. ereal (f x)) ∈ borel_measurable M ⟹ g ∈ measurable N M ⟹ (λx. f (g x)) ∈ borel_measurable N"
unfolding borel_measurable_ereal_iff by simp
theorem borel_measurable_ereal_iff_real:
fixes f :: "'a ⇒ ereal"
shows "f ∈ borel_measurable M ⟷
((λx. real_of_ereal (f x)) ∈ borel_measurable M ∧ f -` {∞} ∩ space M ∈ sets M ∧ f -` {-∞} ∩ space M ∈ sets M)"
proof safe
assume *: "(λx. real_of_ereal (f x)) ∈ borel_measurable M" "f -` {∞} ∩ space M ∈ sets M" "f -` {-∞} ∩ space M ∈ sets M"
have "f -` {∞} ∩ space M = {x∈space M. f x = ∞}" "f -` {-∞} ∩ space M = {x∈space M. f x = -∞}" by auto
with * have **: "{x∈space M. f x = ∞} ∈ sets M" "{x∈space M. f x = -∞} ∈ sets M" by simp_all
let ?f = "λx. if f x = ∞ then ∞ else if f x = -∞ then -∞ else ereal (real_of_ereal (f x))"
have "?f ∈ borel_measurable M" using * ** by (intro measurable_If) auto
also have "?f = f" by (auto simp: fun_eq_iff ereal_real)
finally show "f ∈ borel_measurable M" .
qed simp_all
lemma borel_measurable_ereal_iff_Iio:
"(f::'a ⇒ ereal) ∈ borel_measurable M ⟷ (∀a. f -` {..< a} ∩ space M ∈ sets M)"
by (auto simp: borel_Iio measurable_iff_measure_of)
lemma borel_measurable_ereal_iff_Ioi:
"(f::'a ⇒ ereal) ∈ borel_measurable M ⟷ (∀a. f -` {a <..} ∩ space M ∈ sets M)"
by (auto simp: borel_Ioi measurable_iff_measure_of)
lemma vimage_sets_compl_iff:
"f -` A ∩ space M ∈ sets M ⟷ f -` (- A) ∩ space M ∈ sets M"
by (metis Diff_Compl Diff_Diff_Int diff_eq inf_aci(1) sets.Diff sets.top vimage_Compl)
lemma borel_measurable_iff_Iic_ereal:
"(f::'a⇒ereal) ∈ borel_measurable M ⟷ (∀a. f -` {..a} ∩ space M ∈ sets M)"
unfolding borel_measurable_ereal_iff_Ioi vimage_sets_compl_iff[where A="{a <..}" for a] by simp
lemma borel_measurable_iff_Ici_ereal:
"(f::'a ⇒ ereal) ∈ borel_measurable M ⟷ (∀a. f -` {a..} ∩ space M ∈ sets M)"
unfolding borel_measurable_ereal_iff_Iio vimage_sets_compl_iff[where A="{..< a}" for a] by simp
lemma borel_measurable_ereal2:
fixes f g :: "'a ⇒ ereal"
assumes f: "f ∈ borel_measurable M"
assumes g: "g ∈ borel_measurable M"
assumes H: "(λx. H (ereal (real_of_ereal (f x))) (ereal (real_of_ereal (g x)))) ∈ borel_measurable M"
"(λx. H (-∞) (ereal (real_of_ereal (g x)))) ∈ borel_measurable M"
"(λx. H (∞) (ereal (real_of_ereal (g x)))) ∈ borel_measurable M"
"(λx. H (ereal (real_of_ereal (f x))) (-∞)) ∈ borel_measurable M"
"(λx. H (ereal (real_of_ereal (f x))) (∞)) ∈ borel_measurable M"
shows "(λx. H (f x) (g x)) ∈ borel_measurable M"
proof -
let ?G = "λy x. if g x = ∞ then H y ∞ else if g x = - ∞ then H y (-∞) else H y (ereal (real_of_ereal (g x)))"
let ?F = "λx. if f x = ∞ then ?G ∞ x else if f x = - ∞ then ?G (-∞) x else ?G (ereal (real_of_ereal (f x))) x"
{ fix x have "H (f x) (g x) = ?F x" by (cases "f x" "g x" rule: ereal2_cases) auto }
note * = this
from assms show ?thesis unfolding * by simp
qed
lemma [measurable(raw)]:
fixes f :: "'a ⇒ ereal"
assumes [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M"
shows borel_measurable_ereal_add: "(λx. f x + g x) ∈ borel_measurable M"
and borel_measurable_ereal_times: "(λx. f x * g x) ∈ borel_measurable M"
by (simp_all add: borel_measurable_ereal2)
lemma [measurable(raw)]:
fixes f g :: "'a ⇒ ereal"
assumes "f ∈ borel_measurable M"
assumes "g ∈ borel_measurable M"
shows borel_measurable_ereal_diff: "(λx. f x - g x) ∈ borel_measurable M"
and borel_measurable_ereal_divide: "(λx. f x / g x) ∈ borel_measurable M"
using assms by (simp_all add: minus_ereal_def divide_ereal_def)
lemma borel_measurable_ereal_sum[measurable (raw)]:
fixes f :: "'c ⇒ 'a ⇒ ereal"
assumes "⋀i. i ∈ S ⟹ f i ∈ borel_measurable M"
shows "(λx. ∑i∈S. f i x) ∈ borel_measurable M"
using assms by (induction S rule: infinite_finite_induct) auto
lemma borel_measurable_ereal_prod[measurable (raw)]:
fixes f :: "'c ⇒ 'a ⇒ ereal"
assumes "⋀i. i ∈ S ⟹ f i ∈ borel_measurable M"
shows "(λx. ∏i∈S. f i x) ∈ borel_measurable M"
using assms by (induction S rule: infinite_finite_induct) auto
lemma borel_measurable_extreal_suminf[measurable (raw)]:
fixes f :: "nat ⇒ 'a ⇒ ereal"
assumes [measurable]: "⋀i. f i ∈ borel_measurable M"
shows "(λx. (∑i. f i x)) ∈ borel_measurable M"
unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp
subsection "Borel space on the extended non-negative reals"
text ‹ \<^type>‹ennreal› is a topological monoid, so no rules for plus are required, also all order
statements are usually done on type classes. ›
lemma measurable_enn2ereal[measurable]: "enn2ereal ∈ borel →⇩M borel"
by (intro borel_measurable_continuous_onI continuous_on_enn2ereal)
lemma measurable_e2ennreal[measurable]: "e2ennreal ∈ borel →⇩M borel"
by (intro borel_measurable_continuous_onI continuous_on_e2ennreal)
lemma borel_measurable_enn2real[measurable (raw)]:
"f ∈ M →⇩M borel ⟹ (λx. enn2real (f x)) ∈ M →⇩M borel"
unfolding enn2real_def[abs_def] by measurable
definition [simp]: "is_borel f M ⟷ f ∈ borel_measurable M"
lemma is_borel_transfer[transfer_rule]: "rel_fun (rel_fun (=) pcr_ennreal) (=) is_borel is_borel"
unfolding is_borel_def[abs_def]
proof (safe intro!: rel_funI ext dest!: rel_fun_eq_pcr_ennreal[THEN iffD1])
fix f and M :: "'a measure"
show "f ∈ borel_measurable M" if f: "enn2ereal ∘ f ∈ borel_measurable M"
using measurable_compose[OF f measurable_e2ennreal] by simp
qed simp
context
includes ennreal.lifting
begin
lemma measurable_ennreal[measurable]: "ennreal ∈ borel →⇩M borel"
unfolding is_borel_def[symmetric]
by transfer simp
lemma borel_measurable_ennreal_iff[simp]:
assumes [simp]: "⋀x. x ∈ space M ⟹ 0 ≤ f x"
shows "(λx. ennreal (f x)) ∈ M →⇩M borel ⟷ f ∈ M →⇩M borel"
proof safe
assume "(λx. ennreal (f x)) ∈ M →⇩M borel"
then have "(λx. enn2real (ennreal (f x))) ∈ M →⇩M borel"
by measurable
then show "f ∈ M →⇩M borel"
by (rule measurable_cong[THEN iffD1, rotated]) auto
qed measurable
lemma borel_measurable_times_ennreal[measurable (raw)]:
fixes f g :: "'a ⇒ ennreal"
shows "f ∈ M →⇩M borel ⟹ g ∈ M →⇩M borel ⟹ (λx. f x * g x) ∈ M →⇩M borel"
unfolding is_borel_def[symmetric] by transfer simp
lemma borel_measurable_inverse_ennreal[measurable (raw)]:
fixes f :: "'a ⇒ ennreal"
shows "f ∈ M →⇩M borel ⟹ (λx. inverse (f x)) ∈ M →⇩M borel"
unfolding is_borel_def[symmetric] by transfer simp
lemma borel_measurable_divide_ennreal[measurable (raw)]:
fixes f :: "'a ⇒ ennreal"
shows "f ∈ M →⇩M borel ⟹ g ∈ M →⇩M borel ⟹ (λx. f x / g x) ∈ M →⇩M borel"
unfolding divide_ennreal_def by simp
lemma borel_measurable_minus_ennreal[measurable (raw)]:
fixes f :: "'a ⇒ ennreal"
shows "f ∈ M →⇩M borel ⟹ g ∈ M →⇩M borel ⟹ (λx. f x - g x) ∈ M →⇩M borel"
unfolding is_borel_def[symmetric] by transfer simp
lemma borel_measurable_power_ennreal [measurable (raw)]:
fixes f :: "_ ⇒ ennreal"
assumes f: "f ∈ borel_measurable M"
shows "(λx. (f x) ^ n) ∈ borel_measurable M"
by (induction n) (use f in auto)
lemma borel_measurable_prod_ennreal[measurable (raw)]:
fixes f :: "'c ⇒ 'a ⇒ ennreal"
assumes "⋀i. i ∈ S ⟹ f i ∈ borel_measurable M"
shows "(λx. ∏i∈S. f i x) ∈ borel_measurable M"
using assms by (induction S rule: infinite_finite_induct) auto
end
hide_const (open) is_borel
subsection ‹LIMSEQ is borel measurable›
lemma borel_measurable_LIMSEQ_real:
fixes u :: "nat ⇒ 'a ⇒ real"
assumes u': "⋀x. x ∈ space M ⟹ (λi. u i x) ⇢ u' x"
and u: "⋀i. u i ∈ borel_measurable M"
shows "u' ∈ borel_measurable M"
proof -
have "⋀x. x ∈ space M ⟹ liminf (λn. ereal (u n x)) = ereal (u' x)"
using u' by (simp add: lim_imp_Liminf)
moreover from u have "(λx. liminf (λn. ereal (u n x))) ∈ borel_measurable M"
by auto
ultimately show ?thesis by (simp cong: measurable_cong add: borel_measurable_ereal_iff)
qed
lemma borel_measurable_LIMSEQ_metric:
fixes f :: "nat ⇒ 'a ⇒ 'b :: metric_space"
assumes [measurable]: "⋀i. f i ∈ borel_measurable M"
assumes lim: "⋀x. x ∈ space M ⟹ (λi. f i x) ⇢ g x"
shows "g ∈ borel_measurable M"
unfolding borel_eq_closed
proof (safe intro!: measurable_measure_of)
fix A :: "'b set" assume "closed A"
have [measurable]: "(λx. infdist (g x) A) ∈ borel_measurable M"
proof (rule borel_measurable_LIMSEQ_real)
show "⋀x. x ∈ space M ⟹ (λi. infdist (f i x) A) ⇢ infdist (g x) A"
by (intro tendsto_infdist lim)
show "⋀i. (λx. infdist (f i x) A) ∈ borel_measurable M"
by (intro borel_measurable_continuous_on[where f="λx. infdist x A"]
continuous_at_imp_continuous_on ballI continuous_infdist continuous_ident) auto
qed
show "g -` A ∩ space M ∈ sets M"
proof cases
assume "A ≠ {}"
then have "⋀x. infdist x A = 0 ⟷ x ∈ A"
using ‹closed A› by (simp add: in_closed_iff_infdist_zero)
then have "g -` A ∩ space M = {x∈space M. infdist (g x) A = 0}"
by auto
also have "… ∈ sets M"
by measurable
finally show ?thesis .
qed simp
qed auto
lemma sets_Collect_Cauchy[measurable]:
fixes f :: "nat ⇒ 'a => 'b::{metric_space, second_countable_topology}"
assumes f[measurable]: "⋀i. f i ∈ borel_measurable M"
shows "{x∈space M. Cauchy (λi. f i x)} ∈ sets M"
unfolding metric_Cauchy_iff2 using f by auto
lemma borel_measurable_lim_metric[measurable (raw)]:
fixes f :: "nat ⇒ 'a ⇒ 'b::{banach, second_countable_topology}"
assumes f[measurable]: "⋀i. f i ∈ borel_measurable M"
shows "(λx. lim (λi. f i x)) ∈ borel_measurable M"
proof -
define u' where "u' x = lim (λi. if Cauchy (λi. f i x) then f i x else 0)" for x
then have *: "⋀x. lim (λi. f i x) = (if Cauchy (λi. f i x) then u' x else (THE x. False))"
by (auto simp: lim_def convergent_eq_Cauchy[symmetric])
have "u' ∈ borel_measurable M"
proof (rule borel_measurable_LIMSEQ_metric)
fix x
have "convergent (λi. if Cauchy (λi. f i x) then f i x else 0)"
by (cases "Cauchy (λi. f i x)")
(auto simp add: convergent_eq_Cauchy[symmetric] convergent_def)
then show "(λi. if Cauchy (λi. f i x) then f i x else 0) ⇢ u' x"
unfolding u'_def
by (rule convergent_LIMSEQ_iff[THEN iffD1])
qed measurable
then show ?thesis
unfolding * by measurable
qed
lemma borel_measurable_suminf[measurable (raw)]:
fixes f :: "nat ⇒ 'a ⇒ 'b::{banach, second_countable_topology}"
assumes f[measurable]: "⋀i. f i ∈ borel_measurable M"
shows "(λx. suminf (λi. f i x)) ∈ borel_measurable M"
unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp
lemma Collect_closed_imp_pred_borel: "closed {x. P x} ⟹ Measurable.pred borel P"
by (simp add: pred_def)
text ‹Proof by Jeremy Avigad and Luke Serafin›
lemma isCont_borel_pred[measurable]:
fixes f :: "'b::metric_space ⇒ 'a::metric_space"
shows "Measurable.pred borel (isCont f)"
proof (subst measurable_cong)
let ?I = "λj. inverse(real (Suc j))"
show "isCont f x = (∀i. ∃j. ∀y z. dist x y < ?I j ∧ dist x z < ?I j ⟶ dist (f y) (f z) ≤ ?I i)" for x
unfolding continuous_at_eps_delta
proof safe
fix i assume "∀e>0. ∃d>0. ∀y. dist y x < d ⟶ dist (f y) (f x) < e"
moreover have "0 < ?I i / 2"
by simp
ultimately obtain d where d: "0 < d" "⋀y. dist x y < d ⟹ dist (f y) (f x) < ?I i / 2"
by (metis dist_commute)
then obtain j where j: "?I j < d"
by (metis reals_Archimedean)
show "∃j. ∀y z. dist x y < ?I j ∧ dist x z < ?I j ⟶ dist (f y) (f z) ≤ ?I i"
proof (safe intro!: exI[where x=j])
fix y z assume *: "dist x y < ?I j" "dist x z < ?I j"
have "dist (f y) (f z) ≤ dist (f y) (f x) + dist (f z) (f x)"
by (rule dist_triangle2)
also have "… < ?I i / 2 + ?I i / 2"
by (intro add_strict_mono d less_trans[OF _ j] *)
also have "… ≤ ?I i"
by (simp add: field_simps)
finally show "dist (f y) (f z) ≤ ?I i"
by simp
qed
next
fix e::real assume "0 < e"
then obtain n where n: "?I n < e"
by (metis reals_Archimedean)
assume "∀i. ∃j. ∀y z. dist x y < ?I j ∧ dist x z < ?I j ⟶ dist (f y) (f z) ≤ ?I i"
from this[THEN spec, of "Suc n"]
obtain j where j: "⋀y z. dist x y < ?I j ⟹ dist x z < ?I j ⟹ dist (f y) (f z) ≤ ?I (Suc n)"
by auto
show "∃d>0. ∀y. dist y x < d ⟶ dist (f y) (f x) < e"
proof (safe intro!: exI[of _ "?I j"])
fix y assume "dist y x < ?I j"
then have "dist (f y) (f x) ≤ ?I (Suc n)"
by (intro j) (auto simp: dist_commute)
also have "?I (Suc n) < ?I n"
by simp
also note n
finally show "dist (f y) (f x) < e" .
qed simp
qed
qed (intro pred_intros_countable closed_Collect_all closed_Collect_le open_Collect_less
Collect_closed_imp_pred_borel closed_Collect_imp open_Collect_conj continuous_intros)
lemma isCont_borel:
fixes f :: "'b::metric_space ⇒ 'a::metric_space"
shows "{x. isCont f x} ∈ sets borel"
by simp
lemma is_real_interval:
assumes S: "is_interval S"
shows "∃a b::real. S = {} ∨ S = UNIV ∨ S = {..<b} ∨ S = {..b} ∨ S = {a<..} ∨ S = {a..} ∨
S = {a<..<b} ∨ S = {a<..b} ∨ S = {a..<b} ∨ S = {a..b}"
using S unfolding is_interval_1 by (blast intro: interval_cases)
lemma real_interval_borel_measurable:
assumes "is_interval (S::real set)"
shows "S ∈ sets borel"
proof -
from assms is_real_interval have "∃a b::real. S = {} ∨ S = UNIV ∨ S = {..<b} ∨ S = {..b} ∨
S = {a<..} ∨ S = {a..} ∨ S = {a<..<b} ∨ S = {a<..b} ∨ S = {a..<b} ∨ S = {a..b}" by auto
then show ?thesis
by auto
qed
text ‹The next lemmas hold in any second countable linorder (including ennreal or ereal for instance),
but in the current state they are restricted to reals.›
lemma borel_measurable_mono_on_fnc:
fixes f :: "real ⇒ real" and A :: "real set"
assumes "mono_on A f"
shows "f ∈ borel_measurable (restrict_space borel A)"
proof -
have "⋀x. x ∈ A ⟹ {x} ∈ sets (restrict_space borel A)"
using sets_restrict_space by fastforce
moreover
have "continuous_on (A ∩ - {a ∈ A. ¬ continuous (at a within A) f}) f"
by (force simp: continuous_on_eq_continuous_within intro: continuous_within_subset)
then have "f ∈ borel_measurable (restrict_space (restrict_space borel A)
(- {a ∈ A. ¬ continuous (at a within A) f}))"
by (smt (verit, best) borel_measurable_continuous_on_restrict measurable_cong_sets sets_restrict_restrict_space)
ultimately show ?thesis
using measurable_restrict_countable[OF mono_on_ctble_discont[OF assms]]
by (smt (verit, del_insts) UNIV_I mem_Collect_eq space_borel)
qed
lemma borel_measurable_piecewise_mono:
fixes f::"real ⇒ real" and C::"real set set"
assumes "countable C" "⋀c. c ∈ C ⟹ c ∈ sets borel" "⋀c. c ∈ C ⟹ mono_on c f" "(⋃C) = UNIV"
shows "f ∈ borel_measurable borel"
by (rule measurable_piecewise_restrict[of C], auto intro: borel_measurable_mono_on_fnc simp: assms)
lemma borel_measurable_mono:
fixes f :: "real ⇒ real"
shows "mono f ⟹ f ∈ borel_measurable borel"
using borel_measurable_mono_on_fnc[of UNIV f] by (simp add: mono_def mono_on_def)
lemma measurable_bdd_below_real[measurable (raw)]:
fixes F :: "'a ⇒ 'i ⇒ real"
assumes [simp]: "countable I" and [measurable]: "⋀i. i ∈ I ⟹ F i ∈ M →⇩M borel"
shows "Measurable.pred M (λx. bdd_below ((λi. F i x)`I))"
proof (subst measurable_cong)
show "bdd_below ((λi. F i x)`I) ⟷ (∃q∈ℤ. ∀i∈I. q ≤ F i x)" for x
by (auto simp: bdd_below_def intro!: bexI[of _ "of_int (floor _)"] intro: order_trans of_int_floor_le)
show "Measurable.pred M (λw. ∃q∈ℤ. ∀i∈I. q ≤ F i w)"
using countable_int by measurable
qed
lemma borel_measurable_cINF_real[measurable (raw)]:
fixes F :: "_ ⇒ _ ⇒ real"
assumes [simp]: "countable I"
assumes F[measurable]: "⋀i. i ∈ I ⟹ F i ∈ borel_measurable M"
shows "(λx. INF i∈I. F i x) ∈ borel_measurable M"
proof (rule measurable_piecewise_restrict)
let ?Ω = "{x∈space M. bdd_below ((λi. F i x)`I)}"
show "countable {?Ω, - ?Ω}" "space M ⊆ ⋃{?Ω, - ?Ω}" "⋀X. X ∈ {?Ω, - ?Ω} ⟹ X ∩ space M ∈ sets M"
by auto
fix X assume "X ∈ {?Ω, - ?Ω}" then show "(λx. INF i∈I. F i x) ∈ borel_measurable (restrict_space M X)"
proof safe
show "(λx. INF i∈I. F i x) ∈ borel_measurable (restrict_space M ?Ω)"
by (intro borel_measurable_cINF measurable_restrict_space1 F)
(auto simp: space_restrict_space)
show "(λx. INF i∈I. F i x) ∈ borel_measurable (restrict_space M (-?Ω))"
proof (subst measurable_cong)
fix x assume "x ∈ space (restrict_space M (-?Ω))"
then have "¬ (∀i∈I. - F i x ≤ y)" for y
by (auto simp: space_restrict_space bdd_above_def bdd_above_uminus[symmetric])
then show "(INF i∈I. F i x) = - (THE x. False)"
by (auto simp: space_restrict_space Inf_real_def Sup_real_def Least_def simp del: Set.ball_simps(10))
qed simp
qed
qed
lemma borel_Ici: "borel = sigma UNIV (range (λx::real. {x ..}))"
proof (safe intro!: borel_eq_sigmaI1[OF borel_Iio])
fix x :: real
have eq: "{..<x} = space (sigma UNIV (range atLeast)) - {x ..}"
by auto
show "{..<x} ∈ sets (sigma UNIV (range atLeast))"
unfolding eq by (intro sets.compl_sets) auto
qed auto
lemma borel_measurable_pred_less[measurable (raw)]:
fixes f :: "'a ⇒ 'b::{second_countable_topology, linorder_topology}"
shows "f ∈ borel_measurable M ⟹ g ∈ borel_measurable M ⟹ Measurable.pred M (λw. f w < g w)"
unfolding Measurable.pred_def by (rule borel_measurable_less)
no_notation
eucl_less (infix "<e" 50)
lemma borel_measurable_Max2[measurable (raw)]:
fixes f::"_ ⇒ _ ⇒ 'a::{second_countable_topology, dense_linorder, linorder_topology}"
assumes "finite I"
and [measurable]: "⋀i. f i ∈ borel_measurable M"
shows "(λx. Max{f i x |i. i ∈ I}) ∈ borel_measurable M"
by (simp add: borel_measurable_Max[OF assms(1), where ?f=f and ?M=M] Setcompr_eq_image)
lemma measurable_compose_n [measurable (raw)]:
assumes "T ∈ measurable M M"
shows "(T^^n) ∈ measurable M M"
by (induction n, auto simp add: measurable_compose[OF _ assms])
lemma measurable_real_imp_nat:
fixes f::"'a ⇒ nat"
assumes [measurable]: "(λx. real(f x)) ∈ borel_measurable M"
shows "f ∈ measurable M (count_space UNIV)"
proof -
let ?g = "(λx. real(f x))"
have "⋀(n::nat). ?g-`({real n}) ∩ space M = f-`{n} ∩ space M" by auto
moreover have "⋀(n::nat). ?g-`({real n}) ∩ space M ∈ sets M" using assms by measurable
ultimately have "⋀(n::nat). f-`{n} ∩ space M ∈ sets M" by simp
then show ?thesis using measurable_count_space_eq2_countable by blast
qed
lemma measurable_equality_set [measurable]:
fixes f g::"_⇒ 'a::{second_countable_topology, t2_space}"
assumes [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M"
shows "{x ∈ space M. f x = g x} ∈ sets M"
proof -
define A where "A = {x ∈ space M. f x = g x}"
define B where "B = {y. ∃x::'a. y = (x,x)}"
have "A = (λx. (f x, g x))-`B ∩ space M" unfolding A_def B_def by auto
moreover have "(λx. (f x, g x)) ∈ borel_measurable M" by simp
moreover have "B ∈ sets borel" unfolding B_def by (simp add: closed_diagonal)
ultimately have "A ∈ sets M" by simp
then show ?thesis unfolding A_def by simp
qed
text ‹Logically equivalent to those with the opposite orientation, still these are needed›
lemma measurable_inequality_set_flipped:
fixes f g::"_ ⇒ 'a::{second_countable_topology, linorder_topology}"
assumes [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M"
shows "{x ∈ space M. f x ≥ g x} ∈ sets M"
"{x ∈ space M. f x > g x} ∈ sets M"
by auto
lemmas measurable_inequality_set [measurable] =
borel_measurable_le borel_measurable_less measurable_inequality_set_flipped
proposition measurable_limit [measurable]:
fixes f::"nat ⇒ 'a ⇒ 'b::first_countable_topology"
assumes [measurable]: "⋀n::nat. f n ∈ borel_measurable M"
shows "Measurable.pred M (λx. (λn. f n x) ⇢ c)"
proof -
obtain A :: "nat ⇒ 'b set" where A:
"⋀i. open (A i)"
"⋀i. c ∈ A i"
"⋀S. open S ⟹ c ∈ S ⟹ eventually (λi. A i ⊆ S) sequentially"
by (rule countable_basis_at_decseq) blast
have [measurable]: "⋀N i. (f N)-`(A i) ∩ space M ∈ sets M" using A(1) by auto
then have mes: "(⋂i. ⋃n. ⋂N∈{n..}. (f N)-`(A i) ∩ space M) ∈ sets M" by blast
have "(u ⇢ c) ⟷ (∀i. eventually (λn. u n ∈ A i) sequentially)" for u::"nat ⇒ 'b"
proof
assume "u ⇢ c"
then have "eventually (λn. u n ∈ A i) sequentially" for i using A(1)[of i] A(2)[of i]
by (simp add: topological_tendstoD)
then show "(∀i. eventually (λn. u n ∈ A i) sequentially)" by auto
next
assume H: "(∀i. eventually (λn. u n ∈ A i) sequentially)"
show "(u ⇢ c)"
proof (rule topological_tendstoI)
fix S assume "open S" "c ∈ S"
with A(3)[OF this] obtain i where "A i ⊆ S"
using eventually_False_sequentially eventually_mono by blast
moreover have "eventually (λn. u n ∈ A i) sequentially" using H by simp
ultimately show "∀⇩F n in sequentially. u n ∈ S"
by (simp add: eventually_mono subset_eq)
qed
qed
then have "{x. (λn. f n x) ⇢ c} = (⋂i. ⋃n. ⋂N∈{n..}. (f N)-`(A i))"
by (auto simp add: atLeast_def eventually_at_top_linorder)
then have "{x ∈ space M. (λn. f n x) ⇢ c} = (⋂i. ⋃n. ⋂N∈{n..}. (f N)-`(A i) ∩ space M)"
by auto
then have "{x ∈ space M. (λn. f n x) ⇢ c} ∈ sets M" using mes by simp
then show ?thesis by auto
qed
lemma measurable_limit2 [measurable]:
fixes u::"nat ⇒ 'a ⇒ real"
assumes [measurable]: "⋀n. u n ∈ borel_measurable M" "v ∈ borel_measurable M"
shows "Measurable.pred M (λx. (λn. u n x) ⇢ v x)"
proof -
define w where "w = (λn x. u n x - v x)"
have [measurable]: "w n ∈ borel_measurable M" for n unfolding w_def by auto
have "((λn. u n x) ⇢ v x) ⟷ ((λn. w n x) ⇢ 0)" for x
unfolding w_def using Lim_null by auto
then show ?thesis using measurable_limit by auto
qed
lemma measurable_P_restriction [measurable (raw)]:
assumes [measurable]: "Measurable.pred M P" "A ∈ sets M"
shows "{x ∈ A. P x} ∈ sets M"
proof -
have "A ⊆ space M" using sets.sets_into_space[OF assms(2)].
then have "{x ∈ A. P x} = A ∩ {x ∈ space M. P x}" by blast
then show ?thesis by auto
qed
lemma measurable_sum_nat [measurable (raw)]:
fixes f :: "'c ⇒ 'a ⇒ nat"
assumes "⋀i. i ∈ S ⟹ f i ∈ measurable M (count_space UNIV)"
shows "(λx. ∑i∈S. f i x) ∈ measurable M (count_space UNIV)"
proof cases
assume "finite S"
then show ?thesis using assms by induct auto
qed simp
lemma measurable_abs_powr [measurable]:
fixes p::real
assumes [measurable]: "f ∈ borel_measurable M"
shows "(λx. ¦f x¦ powr p) ∈ borel_measurable M"
by simp
text ‹The next one is a variation around ‹measurable_restrict_space›.›
lemma measurable_restrict_space3:
assumes "f ∈ measurable M N" and
"f ∈ A → B"
shows "f ∈ measurable (restrict_space M A) (restrict_space N B)"
proof -
have "f ∈ measurable (restrict_space M A) N" using assms(1) measurable_restrict_space1 by auto
then show ?thesis by (metis Int_iff funcsetI funcset_mem
measurable_restrict_space2[of f, of "restrict_space M A", of B, of N] assms(2) space_restrict_space)
qed
lemma measurable_restrict_mono:
assumes f: "f ∈ restrict_space M A →⇩M N" and "B ⊆ A"
shows "f ∈ restrict_space M B →⇩M N"
by (rule measurable_compose[OF measurable_restrict_space3 f]) (use ‹B ⊆ A› in auto)
text ‹The next one is a variation around ‹measurable_piecewise_restrict›.›
lemma measurable_piecewise_restrict2:
assumes [measurable]: "⋀n. A n ∈ sets M"
and "space M = (⋃(n::nat). A n)"
"⋀n. ∃h ∈ measurable M N. (∀x ∈ A n. f x = h x)"
shows "f ∈ measurable M N"
proof (rule measurableI)
fix B assume [measurable]: "B ∈ sets N"
{
fix n::nat
obtain h where [measurable]: "h ∈ measurable M N" and "∀x ∈ A n. f x = h x"
using assms(3) by blast
then have *: "f-`B ∩ A n = h-`B ∩ A n" by auto
have "h-`B ∩ A n = h-`B ∩ space M ∩ A n"
using assms(2) sets.sets_into_space by auto
then have "f-`B ∩ A n ∈ sets M"
by (simp add: "*")
}
then have "(⋃n. f-`B ∩ A n) ∈ sets M"
by measurable
moreover have "f-`B ∩ space M = (⋃n. f-`B ∩ A n)"
using assms(2) by blast
ultimately show "f-`B ∩ space M ∈ sets M" by simp
next
fix x assume "x ∈ space M"
then obtain n where "x ∈ A n"
using assms(2) by blast
obtain h where [measurable]: "h ∈ measurable M N" and "∀x ∈ A n. f x = h x"
using assms(3) by blast
then show "f x ∈ space N"
by (metis ‹x ∈ A n› ‹x ∈ space M› measurable_space)
qed
end