# 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.

source
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.

Instances For

source
@[deprecated eventuallyMeasurableSpace (since := "2025-06-21")]
def EventuallyMeasurableSpace {α : Type u_1} (m : MeasurableSpace α) (l : Filter α) [CountableInterFilter l] :
MeasurableSpace α

Alias of `eventuallyMeasurableSpace`.

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

Equations

- @EventuallyMeasurableSpace = @eventuallyMeasurableSpace

Instances For

source
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

Instances For

source
theorem MeasurableSet.eventuallyMeasurableSet {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {l : Filter α} [CountableInterFilter l] (hs : MeasurableSet s) :
EventuallyMeasurableSet m l s
source
theorem le_eventuallyMeasurableSpace {α : Type u_1} {m : MeasurableSpace α} {l : Filter α} [CountableInterFilter l] :
m ≤ eventuallyMeasurableSpace m l
source
@[deprecated le_eventuallyMeasurableSpace (since := "2025-06-21")]
theorem EventuallyMeasurableSpace.measurable_le {α : Type u_1} {m : MeasurableSpace α} {l : Filter α} [CountableInterFilter l] :
m ≤ eventuallyMeasurableSpace m l

Alias of `le_eventuallyMeasurableSpace`.

source
theorem eventuallyMeasurableSet_of_mem_filter {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {l : Filter α} [CountableInterFilter l] (hs : s ∈ l) :
EventuallyMeasurableSet m l s
source
theorem EventuallyMeasurableSet.congr {α : Type u_1} {m : MeasurableSpace α} {s 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`.

source
instance eventuallyMeasurableSingleton {α : Type u_1} {m : MeasurableSpace α} {l : Filter α} [CountableInterFilter l] [MeasurableSingletonClass α] :
MeasurableSingletonClass α
source
@[deprecated eventuallyMeasurableSingleton (since := "2025-06-21")]
theorem EventuallyMeasurableSpace.measurableSingleton {α : Type u_1} {m : MeasurableSpace α} {l : Filter α} [CountableInterFilter l] [MeasurableSingletonClass α] :
MeasurableSingletonClass α

Alias of `eventuallyMeasurableSingleton`.

source
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

Instances For

source
theorem Measurable.eventuallyMeasurable {α : Type u_1} {m : MeasurableSpace α} {l : Filter α} [CountableInterFilter l] {β : Type u_2} [MeasurableSpace β] {f : α → β} (hf : Measurable f) :
EventuallyMeasurable m l f
source
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)
source
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`.

source
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`.