RFC: generalization of `VitaliFamily`

Stream: mathlib4

[Yury G. Kudryashov]

I suggest that we redefine docs#VitaliFamily this way:

structure VitaliFamily {m : MeasurableSpace X} (μ : Measure X) where
  /-- Small sets of the family "centered" at a given point. -/
  filterAt : X → Filter (Set X)
  filterAt_le_smallSets_nhds (x : X) : filterAt x ≤ (𝓝 x).smallSets
  /-- All sets of the family are measurable. -/
  eventually_measurableSet (x : X) : ∀ᶠ s in filterAt x, MeasurableSet s
  /-- The filter `filterAt x` is nontrivial for all `x`.

  TODO: review if we actually need it.
  -/
  filterAt_neBot (x : X) : (filterAt x).NeBot
  exists_covering (s : Set X) (P : X → Set X → Prop)
    (frequently_filterAt : ∀ x ∈ s, ∃ᶠ t in filterAt x, P x t) :
    ∃ t : Set (X × Set X), Countable t ∧ MapsTo Prod.fst t s ∧ t.PairwiseDisjoint Prod.snd ∧
      (∀ p ∈ t, P p.1 p.2) ∧ s ≤ᵐ[μ] ⋃ p ∈ t, p.2

This highlights the fact that everything depends on filterAt only. Also, it gets rid of the metric and moves countability of t to the definition instead of deducing it from SecondCountableTopology. I'm not sure yet if we can define families that use something other than (nhds x).smallSets ⊓ 𝓟 _ for filterAt. CC: @Sébastien Gouëzel

[Yury G. Kudryashov]

UPD: yes, we can redefine docs#Vitali.vitaliFamily to take iSup over all C.

[Sébastien Gouëzel]

Are you motivated by an example which is not covered by the current theory but which becomes possible with the generalization?

[Yury G. Kudryashov]

The proof I have in mind can be done with the current definitions, if you use a family of vitally families. However, it becomes more elegant with the family I described above.

[Yury G. Kudryashov]

I'm on a phone now, I'll write down the details when I get home.

[Yury G. Kudryashov]

Here are the details. Let f : E → F be a map from a finite dimensional space E, n = dim E, to a normed space. If f is differentiable on s with derivative f', and f'.ker is nontrivial at all points of s. Then μH[n] (f '' s) = 0. This is a version of docs#MeasureTheory.addHaar_image_eq_zero_of_det_fderivWithin_eq_zero with weaker assumptions on the codomain. With the family I've described above, we can use a version of docs#VitaliFamily.measure_le_of_frequently_le with ρ being an outer measure, namely a large number multiplied by the pullback of docs#OuterMeasure.mkMetric'.pre for some fixed d > 0, and take s = {x} + (scaling by a factor of C in the direction of ker f') '' ball 0 ε to show that the liminf is zero.

[Yury G. Kudryashov]

Of course, we can rewrite this proof with the current definition, but IMHO these are 2 nice tricks (generalizing Vitali families and generalizing measure differentiation to outer measures).

[Yury G. Kudryashov]

Also, I think that we can prove something like ρ s ≤ ∫⁻ x in s, (liminf of the ratio) ∂μ

[Yury G. Kudryashov]

... for an outer measure ρ. Then we just show that liminf is zero.

[Yury G. Kudryashov]

I've started generalizing stuff to outer measures in #33269. It doesn't build right now, because we don't auto coerce measures to outer measures (also, because I've changed the definition to use liminf).

[Sébastien Gouëzel]

I'm not sure I understand the advantages of the new definition compared to the current one, i.e., is the definition really more general (does it give access to new Vitali families) or is it just for ease of use? I think there several criteria for a definition:

a) Elegance
b) Generality
c) Ease of use of the definition to prove theorems
d) Ease of construction of instances of the definition
e) How close is it to the informal litterature

I have the impression that your definition is more elegant, and easier to use to prove theorems, so better wrt a) and c). However, I also have the impression that it will be slightly more complicated to construct Vitali families using this definition, i.e., d) is a little bit worse. Also, it is further away from the informal litterature (the bible there is Federer, and I had tried to follow it rather closely when defining Vitali families).

Given this, I'd say the tie-breaker would be b): if the new definition gives access to new interesting examples, then we should probably go for it. Otherwise, I would probably keep the current definition, but add some API to make your applications easier: in the end, if the definitions are equivalent, then the precise definition we use shouldn't be important because everything can be hidden behind suitable API, so keeping the current definition seems to be less work.

[Yury G. Kudryashov]

The only example I have in mind where the two definitions differ is the one above (docs#Vitali.vitaliFamily without fixed constant C). With the current definition, one can manually apply a theorem (e.g., something like ν s ≤ ∫⁻ x in s, v.limRatio μ ν ∂μ for an outer measure ν, where limRatio is redefined to be liminf) to each Vitali family with a specific C, then take the limit as C → ∞, but this may require an extra swapping of an integral and a limit.

[Sébastien Gouëzel]

Can you elaborate on what you mean by docs#Vitali.vitaliFamily without a fixed constant C? It is not obvious to me that the new definition would satisfy the covering property (exists_covering in your notation). If that's indeed the case that it works for the covering lemma without a fixed C, it would definitely be worth changing the definition to be able to cover it (or would the old definition also work without a fixed C? What is the difference that would make it work for the new definition but not the old one?)

[Yury G. Kudryashov]

Take filterAt x := ⨆ C, (old filterAt)

[Yury G. Kudryashov]

Then a family is a fine subfamily on iff for each point, there exists C (that depends on this point) such that (old property for being fine at x with this C).

[Yury G. Kudryashov]

I'll try to formally prove exists_covering for this filter tonight (it's less straightforward than I thought).

[Yury G. Kudryashov]

AFAICT, it doesn't work. I probably can prove that there exists a cover of total measure (tsum) ≤ μ s + ε, but not a disjoint cover required by the definition. I'm sorry for wasting your time.