Baire category and Baire measurable sets

This file defines some of the basic notions of Baire category and Baire measurable sets.

Main definitions

First, we define the notation =ᵇ. This denotes eventual equality with respect to the filter of residual sets in a topological space.

A set s in a topological space α is called a BaireMeasurableSet or said to have the property of Baire if it satisfies either of the following equivalent conditions:

• There is a Borel set u such that s =ᵇ u. (This is our definition)
• There is an open set u such that s =ᵇ u. (See BaireMeasurableSet.residual_eq_open)

def Topology.«term_=ᵇ_» : Lean.TrailingParserDescr

Notation for =ᶠ[residual _]. That is, eventual equality with respect to the filter of residual sets.

Equations

• Topology.«term_=ᵇ_» = Lean.ParserDescr.trailingNode `Topology.«term_=ᵇ_» 50 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " =ᵇ ") (Lean.ParserDescr.cat `term 50))

def Topology.«term∀ᵇ_,_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

def Topology.«term∀ᵇ_,_» : Lean.ParserDescr

Notation to say that a property of points in a topological space holds almost everywhere in the sense of Baire category. That is, on a residual set.

Equations

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

def Topology.«term∃ᵇ_,_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

def Topology.«term∃ᵇ_,_» : Lean.ParserDescr

Notation to say that a property of points in a topological space holds on a non meager set.

Equations

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

theorem coborder_mem_residual {α : Type u_1} [TopologicalSpace α] {s : Set α} (hs : IsLocallyClosed s) : coborder s ∈ residual α

theorem closure_residualEq {α : Type u_1} [TopologicalSpace α] {s : Set α} (hs : IsLocallyClosed s) : closure s =ᶠ[residual α] s

def BaireMeasurableSet {α : Type u_1} [TopologicalSpace α] (s : Set α) : Prop

We say a set is a BaireMeasurableSet if it differs from some Borel set by a meager set. This forms a σ-algebra.

It is equivalent, and a more standard definition, to say that the set differs from some open set by a meager set. See BaireMeasurableSet.iff_residualEq_isOpen

Equations

• BaireMeasurableSet s = MeasurableSet s

theorem BaireMeasurableSet.of_mem_residual {α : Type u_1} [TopologicalSpace α] {s : Set α} (h : s ∈ residual α) : BaireMeasurableSet s

theorem MeasurableSet.baireMeasurableSet {α : Type u_1} [TopologicalSpace α] {s : Set α} [MeasurableSpace α] [BorelSpace α] (h : MeasurableSet s) : BaireMeasurableSet s

theorem IsOpen.baireMeasurableSet {α : Type u_1} [TopologicalSpace α] {s : Set α} (h : IsOpen s) : BaireMeasurableSet s

theorem BaireMeasurableSet.compl {α : Type u_1} [TopologicalSpace α] {s : Set α} (h : BaireMeasurableSet s) : BaireMeasurableSet sᶜ

theorem BaireMeasurableSet.of_compl {α : Type u_1} [TopologicalSpace α] {s : Set α} (h : BaireMeasurableSet sᶜ) : BaireMeasurableSet s

theorem IsMeagre.baireMeasurableSet {α : Type u_1} [TopologicalSpace α] {s : Set α} (h : IsMeagre s) : BaireMeasurableSet s

theorem BaireMeasurableSet.iUnion {α : Type u_1} [TopologicalSpace α] {ι : Sort u_3} [Countable ι] {s : ι → Set α} (h : ∀ (i : ι), BaireMeasurableSet (s i)) : BaireMeasurableSet (⋃ (i : ι), s i)

theorem BaireMeasurableSet.biUnion {α : Type u_1} [TopologicalSpace α] {ι : Type u_3} {s : ι → Set α} {t : Set ι} (ht : t.Countable) (h : ∀ i ∈ t, BaireMeasurableSet (s i)) : BaireMeasurableSet (⋃ i ∈ t, s i)

theorem BaireMeasurableSet.sUnion {α : Type u_1} [TopologicalSpace α] {s : Set (Set α)} (hs : s.Countable) (h : ∀ t ∈ s, BaireMeasurableSet t) : BaireMeasurableSet (⋃₀ s)

theorem BaireMeasurableSet.iInter {α : Type u_1} [TopologicalSpace α] {ι : Sort u_3} [Countable ι] {s : ι → Set α} (h : ∀ (i : ι), BaireMeasurableSet (s i)) : BaireMeasurableSet (⋂ (i : ι), s i)

theorem BaireMeasurableSet.biInter {α : Type u_1} [TopologicalSpace α] {ι : Type u_3} {s : ι → Set α} {t : Set ι} (ht : t.Countable) (h : ∀ i ∈ t, BaireMeasurableSet (s i)) : BaireMeasurableSet (⋂ i ∈ t, s i)

theorem BaireMeasurableSet.sInter {α : Type u_1} [TopologicalSpace α] {s : Set (Set α)} (hs : s.Countable) (h : ∀ t ∈ s, BaireMeasurableSet t) : BaireMeasurableSet (⋂₀ s)

theorem BaireMeasurableSet.union {α : Type u_1} [TopologicalSpace α] {s t : Set α} (hs : BaireMeasurableSet s) (ht : BaireMeasurableSet t) : BaireMeasurableSet (s ∪ t)

theorem BaireMeasurableSet.inter {α : Type u_1} [TopologicalSpace α] {s t : Set α} (hs : BaireMeasurableSet s) (ht : BaireMeasurableSet t) : BaireMeasurableSet (s ∩ t)

theorem BaireMeasurableSet.diff {α : Type u_1} [TopologicalSpace α] {s t : Set α} (hs : BaireMeasurableSet s) (ht : BaireMeasurableSet t) : BaireMeasurableSet (s \ t)

theorem BaireMeasurableSet.congr {α : Type u_1} [TopologicalSpace α] {s t : Set α} (hs : BaireMeasurableSet s) (h : s =ᶠ[residual α] t) : BaireMeasurableSet t

theorem MeasurableSet.residualEq_isOpen {α : Type u_1} [TopologicalSpace α] {s : Set α} [MeasurableSpace α] [BorelSpace α] (h : MeasurableSet s) : ∃ (u : Set α), IsOpen u ∧ s =ᶠ[residual α] u

Any Borel set differs from some open set by a meager set.

theorem BaireMeasurableSet.residualEq_isOpen {α : Type u_1} [TopologicalSpace α] {s : Set α} (h : BaireMeasurableSet s) : ∃ (u : Set α), IsOpen u ∧ s =ᶠ[residual α] u

Any BaireMeasurableSet differs from some open set by a meager set.

theorem BaireMeasurableSet.iff_residualEq_isOpen {α : Type u_1} [TopologicalSpace α] {s : Set α} : BaireMeasurableSet s ↔ ∃ (u : Set α), IsOpen u ∧ s =ᶠ[residual α] u

A set is Baire measurable if and only if it differs from some open set by a meager set.

theorem tendsto_residual_of_isOpenMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hc : Continuous f) (ho : IsOpenMap f) : Filter.Tendsto f (residual α) (residual β)

theorem IsMeagre.preimage_of_isOpenMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hc : Continuous f) (ho : IsOpenMap f) {s : Set β} (h : IsMeagre s) : IsMeagre (f ⁻¹' s)

The preimage of a meager set under a continuous open map is meager.

theorem BaireMeasurableSet.preimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hc : Continuous f) (ho : IsOpenMap f) {s : Set β} (h : BaireMeasurableSet s) : BaireMeasurableSet (f ⁻¹' s)

The preimage of a BaireMeasurableSet under a continuous open map is Baire measurable.

theorem Homeomorph.residual_map_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) : Filter.map (⇑h) (residual α) = residual β