Documentation

Mathlib.MeasureTheory.Constructions.EventuallyMeasurable

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 #

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
    def EventuallyMeasurableSet {α : Type u_1} (m : MeasurableSpace α) (l : Filter α) [CountableInterFilter l] (s : Set α) :

    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
    Instances For
      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) :

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

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

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

        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) :

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