# Documentation

Mathlib.MeasureTheory.Covering.Differentiation

# Differentiation of measures #

On a second countable metric space with a measure μ, consider a Vitali family (i.e., for each x one has a family of sets shrinking to x, with a good behavior with respect to covering theorems). Consider also another measure ρ. Then, for almost every x, the ratio ρ a / μ a converges when a shrinks to x along the Vitali family, towards the Radon-Nikodym derivative of ρ with respect to μ. This is the main theorem on differentiation of measures.

This theorem is proved in this file, under the name VitaliFamily.ae_tendsto_rnDeriv. Note that, almost surely, μ a is eventually positive and finite (see VitaliFamily.ae_eventually_measure_pos and VitaliFamily.eventually_measure_lt_top), so the ratio really makes sense.

For concrete applications, one needs concrete instances of Vitali families, as provided for instance by Besicovitch.vitaliFamily (for balls) or by Vitali.vitaliFamily (for doubling measures).

Specific applications to Lebesgue density points and the Lebesgue differentiation theorem are also derived:

• VitaliFamily.ae_tendsto_measure_inter_div states that, for almost every point x ∈ s, then μ (s ∩ a) / μ a tends to 1 as a shrinks to x along a Vitali family.
• VitaliFamily.ae_tendsto_average_norm_sub states that, for almost every point x, then the average of y ↦ ‖f y - f x‖ on a tends to 0 as a shrinks to x along a Vitali family.

## Sketch of proof #

Let v be a Vitali family for μ. Assume for simplicity that ρ is absolutely continuous with respect to μ, as the case of a singular measure is easier.

It is easy to see that a set s on which liminf ρ a / μ a < q satisfies ρ s ≤ q * μ s, by using a disjoint subcovering provided by the definition of Vitali families. Similarly for the limsup. It follows that a set on which ρ a / μ a oscillates has measure 0, and therefore that ρ a / μ a converges almost surely (VitaliFamily.ae_tendsto_div). Moreover, on a set where the limit is close to a constant c, one gets ρ s ∼ c μ s, using again a covering lemma as above. It follows that ρ is equal to μ.withDensity (v.limRatio ρ x), where v.limRatio ρ x is the limit of ρ a / μ a at x (which is well defined almost everywhere). By uniqueness of the Radon-Nikodym derivative, one gets v.limRatio ρ x = ρ.rnDeriv μ x almost everywhere, completing the proof.

There is a difficulty in this sketch: this argument works well when v.limRatio ρ is measurable, but there is no guarantee that this is the case, especially if one doesn't make further assumptions on the Vitali family. We use an indirect argument to show that v.limRatio ρ is always almost everywhere measurable, again based on the disjoint subcovering argument (see VitaliFamily.exists_measurable_supersets_limRatio), and then proceed as sketched above but replacing v.limRatio ρ by a measurable version called v.limRatioMeas ρ.

## Counterexample #

The standing assumption in this file is that spaces are second countable. Without this assumption, measures may be zero locally but nonzero globally, which is not compatible with differentiation theory (which deduces global information from local one). Here is an example displaying this behavior.

Define a measure μ by μ s = 0 if s is covered by countably many balls of radius 1, and μ s = ∞ otherwise. This is indeed a countably additive measure, which is moreover locally finite and doubling at small scales. It vanishes on every ball of radius 1, so all the quantities in differentiation theory (defined as ratios of measures as the radius tends to zero) make no sense. However, the measure is not globally zero if the space is big enough.

• [Herbert Federer, Geometric Measure Theory, Chapter 2.9][Federer1996]