Measurability modulo a filter

In this file we consider the general notion of measurability modulo a σ-filter. Two important instances of this construction are null-measurability with respect to a measure, where the filter is the collection of co-null sets, and Baire-measurability with respect to a topology, where the filter is the collection of comeager (residual) sets. (not to be confused with measurability with respect to the sigma algebra of Baire sets, which is sometimes also called this.) TODO: Implement the latter.

Main definitions

• EventuallyMeasurableSpace: A MeasurableSpace on a type α consisting of sets which are Filter.EventuallyEq to a measurable set with respect to a given CountableInterFilter on α and MeasurableSpace on α.
• EventuallyMeasurableSet: A Prop for sets which are measurable with respect to some EventuallyMeasurableSpace.
• EventuallyMeasurable: A Prop for functions which are measurable with respect to some EventuallyMeasurableSpace on the domain.

def EventuallyMeasurableSpace {α : Type u_1} (m : MeasurableSpace α) (l : Filter α) [CountableInterFilter l] : MeasurableSpace α

The MeasurableSpace of sets which are measurable with respect to a given σ-algebra m on α, modulo a given σ-filter l on α.

Equations

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

def EventuallyMeasurableSet {α : Type u_1} (m : MeasurableSpace α) (l : Filter α) [CountableInterFilter l] (s : Set α) : Prop

We say a set s is an EventuallyMeasurableSet with respect to a given σ-algebra m and σ-filter l if it differs from a set in m by a set in the dual ideal of l.

Equations

• EventuallyMeasurableSet m l s = MeasurableSet s

theorem MeasurableSet.eventuallyMeasurableSet {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {l : Filter α} [CountableInterFilter l] (hs : MeasurableSet s) : EventuallyMeasurableSet m l s

theorem EventuallyMeasurableSpace.measurable_le {α : Type u_1} {m : MeasurableSpace α} {l : Filter α} [CountableInterFilter l] : m ≤ EventuallyMeasurableSpace m l

theorem eventuallyMeasurableSet_of_mem_filter {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {l : Filter α} [CountableInterFilter l] (hs : s ∈ l) : EventuallyMeasurableSet m l s

theorem EventuallyMeasurableSet.congr {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {t : Set α} {l : Filter α} [CountableInterFilter l] (ht : EventuallyMeasurableSet m l t) (hst : s =ᶠ[l] t) : EventuallyMeasurableSet m l s

A set which is EventuallyEq to an EventuallyMeasurableSet is an EventuallyMeasurableSet.

instance EventuallyMeasurableSpace.measurableSingleton {α : Type u_1} {m : MeasurableSpace α} {l : Filter α} [CountableInterFilter l] [MeasurableSingletonClass α] : MeasurableSingletonClass α

Equations

• ⋯ = ⋯

def EventuallyMeasurable {α : Type u_1} (m : MeasurableSpace α) (l : Filter α) [CountableInterFilter l] {β : Type u_2} [MeasurableSpace β] (f : α → β) : Prop

We say a function is EventuallyMeasurable with respect to a given σ-algebra m and σ-filter l if the preimage of any measurable set is equal to some m-measurable set modulo l. Warning: This is not always the same as being equal to some m-measurable function modulo l. In general it is weaker. See Measurable.eventuallyMeasurable_of_eventuallyEq. TODO: Add lemmas about when these are equivalent.

Equations

• EventuallyMeasurable m l f = Measurable f

theorem Measurable.eventuallyMeasurable {α : Type u_1} {m : MeasurableSpace α} {l : Filter α} [CountableInterFilter l] {β : Type u_2} [MeasurableSpace β] {f : α → β} (hf : Measurable f) : EventuallyMeasurable m l f

theorem Measurable.comp_eventuallyMeasurable {α : Type u_1} {m : MeasurableSpace α} {l : Filter α} [CountableInterFilter l] {β : Type u_2} {γ : Type u_3} [MeasurableSpace β] [MeasurableSpace γ] {f : α → β} {h : β → γ} (hh : Measurable h) (hf : EventuallyMeasurable m l f) : EventuallyMeasurable m l (h ∘ f)

theorem EventuallyMeasurable.congr {α : Type u_1} {m : MeasurableSpace α} {l : Filter α} [CountableInterFilter l] {β : Type u_2} [MeasurableSpace β] {f : α → β} {g : α → β} (hf : EventuallyMeasurable m l f) (hgf : g =ᶠ[l] f) : EventuallyMeasurable m l g

A function which is EventuallyEq to some EventuallyMeasurable function is EventuallyMeasurable.

theorem Measurable.eventuallyMeasurable_of_eventuallyEq {α : Type u_1} {m : MeasurableSpace α} {l : Filter α} [CountableInterFilter l] {β : Type u_2} [MeasurableSpace β] {f : α → β} {g : α → β} (hf : Measurable f) (hgf : g =ᶠ[l] f) : EventuallyMeasurable m l g

A function which is EventuallyEq to some Measurable function is EventuallyMeasurable.