Measurability modulo a sigma filter

Stream: mathlib4

[Felix Weilacher]

I wanted to ask for feedback on a refactor I'm working on at #10856, since it is somewhat low-level in the MeasureTheory library and I'd like to make sure I'm doing it in the best way. I also am not sure if there is standard terminology related to this construction, or a good reference for it.

The idea is to generalize NullMeasurableSpace to measurability modulo an arbitrary sigma-filter. For example the main definitions are:

variable {α : Type*} (m : MeasurableSpace α) (l : Filter α) [CountableInterFilter l] {s t: Set α}

/-- The `MeasurableSpace` of sets which are measurable with respect to a given σ-algebra `m`
on `α`, modulo a given σ-filter `l` on `α`. -/
def EventuallyMeasurableSpace : MeasurableSpace α where
  MeasurableSet' s := ∃ t, MeasurableSet t ∧ s =ᶠ[l] t
  measurableSet_empty := ⟨∅, MeasurableSet.empty, EventuallyEq.refl _ _ ⟩
  measurableSet_compl := fun s ⟨t, ht, hts⟩ => ⟨tᶜ, ht.compl, hts.compl⟩
  measurableSet_iUnion s hs := by
    choose t ht hts using hs
    exact ⟨⋃ i, t i, MeasurableSet.iUnion ht, EventuallyEq.countable_iUnion hts⟩

/-- We say a set `s` is and `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`. -/
def EventuallyMeasurableSet (s : Set α) : Prop := @MeasurableSet _ (EventuallyMeasurableSpace

And then for example I redefine

instance NullMeasurableSpace.instMeasurableSpace : MeasurableSpace (NullMeasurableSpace α μ) :=
  @EventuallyMeasurableSpace α inferInstance (Measure.ae μ) _

[Yury G. Kudryashov]

Do you have specific filters in mind?

[Yury G. Kudryashov]

With your proposed change we can move parts of the theory about AEMeasurable/NullMeasurable functions to MeasurableSpace.

[Felix Weilacher]

The main reason I want to do this is to apply it with the residual filter to get the Baire measurable sets.

[Felix Weilacher]

And yeah, I'd like to move lemmas about Null measurability that don't actually have anything to do with Measure as you said, so as to not reprove them for Baire measurability

[Yury G. Kudryashov]

TIL that Baire measurability is a thing. When people need it?

[Yury G. Kudryashov]

(I hope it didn't sound like I doubt that they're useful; it's about me not knowing relevant parts of mathematics)

[Felix Weilacher]

For example, the Kuratowski-Ulam theorem, which I have a lean 3 formalization of, is an analogue of Fubini's theorem for the residual filter. It says for a subset of the plane, residually many horizontal slices are residual iff residually many vertical slices are residual.

Like Fubini, it requires that the set be Baire measurable in the plane.

[Felix Weilacher]

It also features heavily in the theory of Polish groups, which are just topological groups where the topology is Polish. Here, it tends to be the most useful regularity property of Borel sets/functions, since there is not necessarily a Haar measure.

For example, a very nice result is that Baire measurable homomorphisms between Polish groups are automatically continuous, from one which can conclude that if a group has a group topology compatible with some Borel structure, that topology is unique.

[Felix Weilacher]

These are just some examples of course. It shows up all over descriptive set theory.

[Yury G. Kudryashov]

So many things to learn...

[Anatole Dedecker]

Pinging @Michael Rothgang since I think this change would be relevant for #7076

[Felix Weilacher]

It looks like #7076 only defines the "conull" filter for now, but if there is a plan to define "null-measurable" subsets of a manifold in the future, then I agree

[Anatole Dedecker]

Ah right, sorry for the confusion

[Yury G. Kudryashov]

IMHO, we should define docs#dimH for manifolds and get "away from codimension r" filter.

[Yury G. Kudryashov]

But I had some issues with convexity when I tried, don't remember the details.