# Borel (measurable) space #

## Main definitions #

• borel α : the least σ-algebra that contains all open sets;
• class BorelSpace : a space with TopologicalSpace and MeasurableSpace structures such that ‹MeasurableSpace α› = borel α;
• class OpensMeasurableSpace : a space with TopologicalSpace and MeasurableSpace structures such that all open sets are measurable; equivalently, borel α ≤ ‹MeasurableSpace α›.
• BorelSpace instances on Empty, Unit, Bool, Nat, Int, Rat;
• MeasurableSpace and BorelSpace instances on ℝ, ℝ≥0, ℝ≥0∞.

## Main statements #

• IsOpen.measurableSet, IsClosed.measurableSet: open and closed sets are measurable;
• Continuous.measurable : a continuous function is measurable;
• Continuous.measurable2 : if f : α → β and g : α → γ are measurable and op : β × γ → δ is continuous, then fun x => op (f x, g y) is measurable;
• Measurable.add etc : dot notation for arithmetic operations on Measurable predicates, and similarly for dist and edist;
• AEMeasurable.add : similar dot notation for almost everywhere measurable functions;
def borel (α : Type u) [] :

MeasurableSpace structure generated by TopologicalSpace.

Equations
Instances For
theorem borel_anti {α : Type u_1} :
theorem borel_eq_top_of_discrete {α : Type u_1} [] [] :
theorem borel_eq_top_of_countable {α : Type u_1} [] [] [] :
theorem borel_eq_generateFrom_of_subbasis {α : Type u_1} {s : Set (Set α)} [t : ] (hs : ) :
theorem isPiSystem_isOpen {α : Type u_1} [] :
IsPiSystem {s : Set α | }
theorem isPiSystem_isClosed {α : Type u_1} [] :
IsPiSystem {s : Set α | }
theorem borel_comap {α : Type u_1} {β : Type u_2} {f : αβ} {t : } :
=
theorem Continuous.borel_measurable {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) :
class OpensMeasurableSpace (α : Type u_6) [] [h : ] :

A space with MeasurableSpace and TopologicalSpace structures such that all open sets are measurable.

• borel_le : h

Borel-measurable sets are measurable.

Instances
theorem OpensMeasurableSpace.borel_le {α : Type u_6} [] [h : ] [self : ] :
h

Borel-measurable sets are measurable.

class BorelSpace (α : Type u_6) [] [] :

A space with MeasurableSpace and TopologicalSpace structures such that the σ-algebra of measurable sets is exactly the σ-algebra generated by open sets.

• measurable_eq : inst✝ =

The measurable sets are exactly the Borel-measurable sets.

Instances
theorem BorelSpace.measurable_eq {α : Type u_6} [] [] [self : ] :
inst✝ =

The measurable sets are exactly the Borel-measurable sets.

The behaviour of borelize α depends on the existing assumptions on α.

• if α is a topological space with instances [MeasurableSpace α] [BorelSpace α], then borelize α replaces the former instance by borel α;
• otherwise, borelize α adds instances borel α : MeasurableSpace α and ⟨rfl⟩ : BorelSpace α.

Finally, borelize α β γ runs borelize α; borelize β; borelize γ.

Equations
• One or more equations did not get rendered due to their size.
Instances For

Add instances borel e : MeasurableSpace e and ⟨rfl⟩ : BorelSpace e.

Equations
• One or more equations did not get rendered due to their size.
Instances For

Given a type e, an assumption i : MeasurableSpace e, and an instance [BorelSpace e], replace i with borel e.

Equations
• One or more equations did not get rendered due to their size.
Instances For

Given a type $t, if there is an assumption [i : MeasurableSpace$t], then try to prove [BorelSpace $t] and replace i with borel$t. Otherwise, add instances borel $t : MeasurableSpace$t and ⟨rfl⟩ : BorelSpace \$t.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[instance 100]
instance OrderDual.opensMeasurableSpace {α : Type u_6} [] [] [h : ] :
Equations
• =
@[instance 100]
instance OrderDual.borelSpace {α : Type u_6} [] [] [h : ] :
Equations
• =
@[instance 100]
instance BorelSpace.opensMeasurable {α : Type u_6} [] [] [] :

In a BorelSpace all open sets are measurable.

Equations
• =
instance Subtype.borelSpace {α : Type u_6} [] [] [hα : ] (s : Set α) :
Equations
• =
instance Countable.instBorelSpace {α : Type u_1} [] [] [] [] :
Equations
• =
instance Subtype.opensMeasurableSpace {α : Type u_6} [] [] [h : ] (s : Set α) :
Equations
• =
theorem opensMeasurableSpace_iff_forall_measurableSet {α : Type u_1} [] [] :
∀ (s : Set α),
@[instance 100]
instance BorelSpace.countablyGenerated {α : Type u_6} [] [] [] :
Equations
• =
theorem MeasurableSet.induction_on_open {α : Type u_1} [] [] [] {C : Set αProp} (h_open : ∀ (U : Set α), C U) (h_compl : ∀ (t : Set α), C tC t) (h_union : ∀ (f : Set α), Pairwise (Disjoint on f)(∀ (i : ), MeasurableSet (f i))(∀ (i : ), C (f i))C (⋃ (i : ), f i)) ⦃t : Set α :
C t
theorem IsOpen.measurableSet {α : Type u_1} {s : Set α} [] [] (h : ) :
Equations
• =
theorem measurableSet_interior {α : Type u_1} {s : Set α} [] [] :
theorem IsGδ.measurableSet {α : Type u_1} {s : Set α} [] [] (h : IsGδ s) :
theorem measurableSet_of_continuousAt {α : Type u_1} [] [] {β : Type u_6} [] (f : αβ) :
MeasurableSet {x : α | }
theorem IsClosed.measurableSet {α : Type u_1} {s : Set α} [] [] (h : ) :
theorem IsCompact.measurableSet {α : Type u_1} {s : Set α} [] [] [] (h : ) :
theorem Inseparable.mem_measurableSet_iff {γ : Type u_3} [] [] [] {x : γ} {y : γ} (h : ) {s : Set γ} (hs : ) :
x s y s

If two points are topologically inseparable, then they can't be separated by a Borel measurable set.

theorem IsCompact.closure_subset_measurableSet {γ : Type u_3} [] [] [] [] {K : Set γ} {s : Set γ} (hK : ) (hs : ) (hKs : K s) :
s

If K is a compact set in an R₁ space and s ⊇ K is a Borel measurable superset, then s includes the closure of K as well.

theorem IsCompact.measure_closure {γ : Type u_3} [] [] [] [] {K : Set γ} (hK : ) (μ : ) :
μ () = μ K

In an R₁ topological space with Borel measure μ, the measure of the closure of a compact set K is equal to the measure of K.

See also MeasureTheory.Measure.OuterRegular.measure_closure_eq_of_isCompact for a version that assumes μ to be outer regular but does not assume the σ-algebra to be Borel.

theorem measurableSet_closure {α : Type u_1} {s : Set α} [] [] :
theorem measurable_of_isOpen {γ : Type u_3} {δ : Type u_5} [] [] [] [] {f : δγ} (hf : ∀ (s : Set γ), MeasurableSet (f ⁻¹' s)) :
theorem measurable_of_isClosed {γ : Type u_3} {δ : Type u_5} [] [] [] [] {f : δγ} (hf : ∀ (s : Set γ), MeasurableSet (f ⁻¹' s)) :
theorem measurable_of_isClosed' {γ : Type u_3} {δ : Type u_5} [] [] [] [] {f : δγ} (hf : ∀ (s : Set γ), s.Nonemptys Set.univMeasurableSet (f ⁻¹' s)) :
instance nhds_isMeasurablyGenerated {α : Type u_1} [] [] (a : α) :
(nhds a).IsMeasurablyGenerated
Equations
• =
theorem MeasurableSet.nhdsWithin_isMeasurablyGenerated {α : Type u_1} [] [] {s : Set α} (hs : ) (a : α) :
().IsMeasurablyGenerated

If s is a measurable set, then 𝓝[s] a is a measurably generated filter for each a. This cannot be an instance because it depends on a non-instance hs : MeasurableSet s.

@[instance 100]
instance OpensMeasurableSpace.separatesPoints {α : Type u_1} [] [] [] :
Equations
• =
@[instance 100]
Equations
• =
instance Pi.opensMeasurableSpace {ι : Type u_6} {π : ιType u_7} [] [t' : (i : ι) → TopologicalSpace (π i)] [(i : ι) → MeasurableSpace (π i)] [∀ (i : ι), ] [∀ (i : ι), OpensMeasurableSpace (π i)] :
OpensMeasurableSpace ((i : ι) → π i)
Equations
• =
class SecondCountableTopologyEither (α : Type u_6) (β : Type u_7) [] [] :

The typeclass SecondCountableTopologyEither α β registers the fact that at least one of the two spaces has second countable topology. This is the right assumption to ensure that continuous maps from α to β are strongly measurable.

• The projection out of SecondCountableTopologyEither

Instances
theorem SecondCountableTopologyEither.out {α : Type u_6} {β : Type u_7} [] [] [self : ] :

The projection out of SecondCountableTopologyEither

@[instance 100]
instance secondCountableTopologyEither_of_left (α : Type u_6) (β : Type u_7) [] [] :
Equations
• =
@[instance 100]
instance secondCountableTopologyEither_of_right (α : Type u_6) (β : Type u_7) [] [] :
Equations
• =
instance Prod.opensMeasurableSpace {α : Type u_1} {β : Type u_2} [] [] [] [] [h : ] :

If either α or β has second-countable topology, then the open sets in α × β belong to the product sigma-algebra.

Equations
• =
theorem interior_ae_eq_of_null_frontier {α' : Type u_6} [] [] {μ : } {s : Set α'} (h : μ () = 0) :
=ᵐ[μ] s
theorem measure_interior_of_null_frontier {α' : Type u_6} [] [] {μ : } {s : Set α'} (h : μ () = 0) :
μ () = μ s
theorem nullMeasurableSet_of_null_frontier {α : Type u_1} [] [] {s : Set α} {μ : } (h : μ () = 0) :
theorem closure_ae_eq_of_null_frontier {α' : Type u_6} [] [] {μ : } {s : Set α'} (h : μ () = 0) :
=ᵐ[μ] s
theorem measure_closure_of_null_frontier {α' : Type u_6} [] [] {μ : } {s : Set α'} (h : μ () = 0) :
μ () = μ s
Equations
• =
theorem Continuous.measurable {α : Type u_1} {γ : Type u_3} [] [] [] [] [] {f : αγ} (hf : ) :

A continuous function from an OpensMeasurableSpace to a BorelSpace is measurable.

theorem Continuous.aemeasurable {α : Type u_1} {γ : Type u_3} [] [] [] [] [] {f : αγ} (h : ) {μ : } :

A continuous function from an OpensMeasurableSpace to a BorelSpace is ae-measurable.

theorem ClosedEmbedding.measurable {α : Type u_1} {γ : Type u_3} [] [] [] [] [] {f : αγ} (hf : ) :
theorem ContinuousOn.measurable_piecewise {α : Type u_1} {γ : Type u_3} [] [] [] [] [] {f : αγ} {g : αγ} {s : Set α} [(j : α) → Decidable (j s)] (hf : ) (hg : ) (hs : ) :
Measurable (s.piecewise f g)

If a function is defined piecewise in terms of functions which are continuous on their respective pieces, then it is measurable.

@[instance 100]
Equations
• =
@[instance 100]
instance ContinuousMul.measurableMul {γ : Type u_3} [] [] [] [Mul γ] [] :
Equations
• =
@[instance 100]
instance ContinuousSub.measurableSub {γ : Type u_3} [] [] [] [Sub γ] [] :
Equations
• =
@[instance 100]
instance TopologicalAddGroup.measurableNeg {γ : Type u_3} [] [] [] [] :
Equations
• =
@[instance 100]
instance TopologicalGroup.measurableInv {γ : Type u_3} [] [] [] [] [] :
Equations
• =
@[instance 100]
instance ContinuousSMul.measurableSMul {M : Type u_7} {α : Type u_8} [] [] [] [] [] [SMul M α] [] :
Equations
• =
theorem Homeomorph.measurable {α : Type u_1} {γ : Type u_3} [] [] [] [] [] (h : α ≃ₜ γ) :
def Homeomorph.toMeasurableEquiv {γ : Type u_3} {γ₂ : Type u_4} [] [] [] [] [] [] (h : γ ≃ₜ γ₂) :
γ ≃ᵐ γ₂

A homeomorphism between two Borel spaces is a measurable equivalence.

Equations
• h.toMeasurableEquiv = { toEquiv := h.toEquiv, measurable_toFun := , measurable_invFun := }
Instances For
theorem Homeomorph.measurableEmbedding {γ : Type u_3} {γ₂ : Type u_4} [] [] [] [] [] [] (h : γ ≃ₜ γ₂) :
@[simp]
theorem Homeomorph.toMeasurableEquiv_coe {γ : Type u_3} {γ₂ : Type u_4} [] [] [] [] [] [] (h : γ ≃ₜ γ₂) :
h.toMeasurableEquiv = h
@[simp]
theorem Homeomorph.toMeasurableEquiv_symm_coe {γ : Type u_3} {γ₂ : Type u_4} [] [] [] [] [] [] (h : γ ≃ₜ γ₂) :
h.toMeasurableEquiv.symm = h.symm
theorem ContinuousMap.measurable {α : Type u_1} {γ : Type u_3} [] [] [] [] [] (f : C(α, γ)) :
theorem measurable_of_continuousOn_compl_singleton {α : Type u_1} {γ : Type u_3} [] [] [] [] [] [] {f : αγ} (a : α) (hf : ContinuousOn f {a}) :
theorem Continuous.measurable2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_5} [] [] [] [] [] [] [] [] {f : δα} {g : δβ} {c : αβγ} (h : Continuous fun (p : α × β) => c p.1 p.2) (hf : ) (hg : ) :
Measurable fun (a : δ) => c (f a) (g a)
theorem Continuous.aemeasurable2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_5} [] [] [] [] [] [] [] [] {f : δα} {g : δβ} {c : αβγ} {μ : } (h : Continuous fun (p : α × β) => c p.1 p.2) (hf : ) (hg : ) :
AEMeasurable (fun (a : δ) => c (f a) (g a)) μ
@[instance 100]
instance HasContinuousInv₀.measurableInv {γ : Type u_3} [] [] [] [] [] :
Equations
• =
@[instance 100]
instance ContinuousAdd.measurableMul₂ {γ : Type u_3} [] [] [] [Add γ] [] :
Equations
• =
@[instance 100]
instance ContinuousMul.measurableMul₂ {γ : Type u_3} [] [] [] [Mul γ] [] :
Equations
• =
@[instance 100]
instance ContinuousSub.measurableSub₂ {γ : Type u_3} [] [] [] [Sub γ] [] :
Equations
• =
@[instance 100]
instance ContinuousSMul.measurableSMul₂ {M : Type u_7} {α : Type u_8} [] [] [] [] [] [SMul M α] [] :
Equations
• =
theorem pi_le_borel_pi {ι : Type u_6} {π : ιType u_7} [(i : ι) → TopologicalSpace (π i)] [(i : ι) → MeasurableSpace (π i)] [∀ (i : ι), BorelSpace (π i)] :
MeasurableSpace.pi borel ((i : ι) → π i)
theorem prod_le_borel_prod {α : Type u_1} {β : Type u_2} [] [] [] [] [] [] :
Prod.instMeasurableSpace borel (α × β)
instance Pi.borelSpace {ι : Type u_6} {π : ιType u_7} [] [(i : ι) → TopologicalSpace (π i)] [(i : ι) → MeasurableSpace (π i)] [∀ (i : ι), ] [∀ (i : ι), BorelSpace (π i)] :
BorelSpace ((i : ι) → π i)
Equations
• =
instance Prod.borelSpace {α : Type u_1} {β : Type u_2} [] [] [] [] [] [] :
BorelSpace (α × β)
Equations
• =
theorem MeasurableEmbedding.borelSpace {α : Type u_6} {β : Type u_7} [] [] [] [] [hβ : ] {e : αβ} (h'e : ) (h''e : ) :

Given a measurable embedding to a Borel space which is also a topological embedding, then the source space is also a Borel space.

instance ULift.instBorelSpace {α : Type u_1} [] [] [] :
Equations
• =
instance DiscreteMeasurableSpace.toBorelSpace {α : Type u_6} [] [] [] :
Equations
• =
theorem Embedding.measurableEmbedding {α : Type u_1} {β : Type u_2} [] [] [] [] [] [] {f : αβ} (h₁ : ) (h₂ : ) :
theorem ClosedEmbedding.measurableEmbedding {α : Type u_1} {β : Type u_2} [] [] [] [] [] [] {f : αβ} (h : ) :
theorem OpenEmbedding.measurableEmbedding {α : Type u_1} {β : Type u_2} [] [] [] [] [] [] {f : αβ} (h : ) :
instance Empty.borelSpace :
Equations
instance Unit.borelSpace :
Equations
instance Bool.borelSpace :
Equations
instance Nat.borelSpace :
Equations
instance Int.borelSpace :
Equations
instance Rat.borelSpace :
Equations
Equations
instance Real.borelSpace :
Equations
Equations
Equations
Equations
Equations
Equations
instance EReal.borelSpace :
Equations