Vitali families

Stream: maths

[Yury G. Kudryashov]

Hi @Sébastien Gouëzel,

I'm comparing docs#VitaliFamily to the definition of a Vitali relation in Geometric Measure Theory. I see a few differences:

• Federer requires ∀ x, ∀ s ∈ setsAt x, x ∈ s;
• I can't find the "nonempty interior" assumption in Federer's definition;
• I can't find the "measurable set" assumption in Federer's definition though he might assume it without saying

[Yury G. Kudryashov]

What were the reasons for the changes? I'm mostly interested in the first one: are there any examples when we can't assume ∀ x, ∀ s ∈ setsAt x, s ∈ nhds x instead of nonempty_interior?

[Yury G. Kudryashov]

Or even ∀ x, HasBasis (nhds x) (⋅ ∈ setsAt x) id instead of nontrivial and nonempty_interior

[Yury G. Kudryashov]

Are there any Vitali families we should care about besides those coming from Vitali and Besicovitch covering theorems?

[Yury G. Kudryashov]

Also, is there a name for "Vitali family + ∀ ε > 0, any set of measure zero admits covering by elements of total measure <ε"?

[Yury G. Kudryashov]

#xy: I want to generalize some theorems you prove in `Function/Jacobian' to the following settings:

• μ is a measure, ν is an outer measure (for me, the most interesting case is OuterMeasure.comap _ _);
• we have a Vitali family v with the additional axiom above; note that both Vitali and Besicovitch theorems can give this for an outer regular measure;
• we have an upper estimate on liminf (fun s ↦ ν (s ∩ t) / μ (s ∩ t)) f.filterAt at all points of a set t.

Instead of the second assumption, we can require that ν is absolutely continuous w.r.t. μ and prove it provided that we have the second assumption.

[Yury G. Kudryashov]

Why do I want this:

• this way the Jacobian file will apply more general theorems;
• I want to generalize docs#MeasureTheory.addHaar_image_eq_zero_of_det_fderivWithin_eq_zero to f : E → F and the findim ℝ E-dimensional Hausdorff measure in the codomain (which may be infinitely dimensional)

[Yury G. Kudryashov]

BTW, am I right that this version of Sard's theorem was first proved by Moreira in 2001 (Hausdorff measures and the Morse-Sard theorem)?

[Yury G. Kudryashov]

It's Theorem 3.3 in that paper.

[Yury G. Kudryashov]

Or this was known before?

[Yury G. Kudryashov]

One more question: if we require ∀ s in setsAt x, x ∈ s, should we switch covering to output g : α → Set α and t : Set α instead of a set in α × Set α?

[Sébastien Gouëzel]

About the condition ∀ x, ∀ s ∈ setsAt x, x ∈ s, we had it in a first version, and then we removed it because it was too restrictive: it is not satisfied by some families coming from the Vitali covering theorem, with

setsAt x := { a | IsClosed a ∧ (interior a).Nonempty ∧
    ∃ r, a ⊆ closedBall x r ∧ μ (closedBall x (3 * r)) ≤ C * μ a }

In particular, balls of the form B (y, r) with d (x, y) \le 10 r belong to this Vitali family, while they don't contain x. And this is important for applications we already have in mathlib.

[Yury G. Kudryashov]

Thank you! Probably, this difference should be documented somewhere.

[Sébastien Gouëzel]

For the two other conditions (nonempty interior, measurable sets), I don't remember exactly but I think they were needed for some proofs. Nonempty interior ensures that a disjoint subfamily is countable (as the topology is second-countable), which is needed for many measure estimates. Measurable set is used all over the place.

[Yury G. Kudryashov]

About measurable set: I guess, Federer assumes this without mentioning.

[Sébastien Gouëzel]

Yury G. Kudryashov said:

Also, is there a name for "Vitali family + ∀ ∃ > 0, any set of measure zero admits covering by elements of total measure <ε"?

Not that I know of. Feel free to invent one! All interesting Vitali families I know will satisfy this condition, so maybe we could even add it to the definition (or try to derive it from an easier to check property?)

[Yury G. Kudryashov]

If we add this to the definition, then we'll lose a nice property "a subfamily of a Vitaly family with nontrivial property is a Vitaly family"

[Yury G. Kudryashov]

Let me call this StrongVitaliFamily

[Yury G. Kudryashov]

What about this version of Sard's theorem? Did you see it somewhere else?

[Yury G. Kudryashov]

One more question: what do you think about giving definition of VitaliFamily in terms of filters? Something like (not tested):

structure VitaliFamily {X : Type*} [TopologicalSpace X] {_ : MeasurableSpace X} (μ : Measure X) where
  filterAt : X → Filter (Set X)
  neBot : ∀ x, NeBot (filterAt x)
  eventually_measurableSet : ∀ x, ∀ᶠ s in filterAt x, MeasurableSet s
  le_smallSets : ∀ x, filterAt x ≤ (𝓝 x).smallSets
  covering : ∀ (s : Set X) (f : X → Set (Set X)) (∀ x ∈ s, ∃ᶠ t in filterAt x, t ∈ f x) →
    ∃ t : Set (α × Set α), t.Countable ∧ (∀ p ∈ t, p.1 ∈ s) ∧ (t.PairwiseDisjoint fun p ↦ p.2) ∧
      (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, p.2) = 0

In fact, I made 1 more modification here: instead of asking for a nonempty interior, I ask for t.Countable in the last axiom. AFAICS, we have this in both cases (Vitali and Besicovitch) and this is closer to the source material. Also, this way we can remove [SecondCountableTopology α] assumptions from some lemmas.

[Yury G. Kudryashov]

I don't know if there is any VitaliFamily in the sense of this definition that does not require a (Pseudo)MetricSpace structure.

[Yury G. Kudryashov]

I've just realized that VitaliFamily only needs [TopologicalSpace X] [MeasurableSpace X] (f : Filter X), where f = ae μ and MeasurableSpace is needed for measurableSet : ∀ x : X, ∀ s ∈ setsAt x, MeasurableSet s only.