mathlibdocumentation

measure_theory.covering.differentiation

Differentiation of measures #

On a 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 vitali_family.ae_tendsto_rn_deriv. Note that, almost surely, μ a is eventually positive and finite (see vitali_family.ae_eventually_measure_pos and vitali_family.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.vitali_family (for balls) or by vitali.vitali_family (for doubling measures).

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 (vitali_family.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 μ.with_density (v.lim_ratio ρ x), where v.lim_ratio ρ 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.lim_ratio ρ x = ρ.rn_deriv μ x almost everywhere, completing the proof.

There is a difficulty in this sketch: this argument works well when v.lim_ratio ρ 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.lim_ratio ρ is always almost everywhere measurable, again based on the disjoint subcovering argument (see vitali_family.exists_measurable_supersets_lim_ratio), and then proceed as sketched above but replacing v.lim_ratio ρ by a measurable version called v.lim_ratio_meas ρ.