Commit 2022-10-08 05:41 a67fbae6

feat(measure_theory/covering): improve Vitali families and Lebesgue density theorem (#16830) #16762 has shown weaknesses of our current implementation of Vitali families. Notably, it enforces that the sets based at x all contain x, which is not natural for some applications. We refactor Vitali families to solve this issue. Here are the main changes:

• in the definition of Vitali families, in the covering property it is now allowed to use several sets based at the same point (which means that the covering is not indexed by α but by α × set α)
• We modify the Vitali covering theorem to deal with general indexed families, to fit in this framework.
• This makes it possible to define better Vitali families for doubling measures. In particular, for any K, we define a Vitali family such that the sets based at x contain all balls closed_ball y r when dist x y ≤ K * r.
• This gives a better Lebesgue density theorem, solving the issue pointed out in #16762