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

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

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

A set which is `EventuallyEq`

to an `EventuallyMeasurableSet`

is an `EventuallyMeasurableSet`

.

## Equations

- ⋯ = ⋯

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

A function which is `EventuallyEq`

to some `EventuallyMeasurable`

function
is `EventuallyMeasurable`

.

A function which is `EventuallyEq`

to some `Measurable`

function is `EventuallyMeasurable`

.