Differentiation of measures #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 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).
Specific applications to Lebesgue density points and the Lebesgue differentiation theorem are also derived:
vitali_family.ae_tendsto_measure_inter_divstates that, for almost every pointx ∈ s, thenμ (s ∩ a) / μ atends to1asashrinks toxalong a Vitali family.vitali_family.ae_tendsto_average_norm_substates that, for almost every pointx, then the average ofy ↦ ‖f y - f x‖onatends to0asashrinks toxalong 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 (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 ρ.
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.
References #
The limit along a Vitali family of ρ a / μ a where it makes sense, and garbage otherwise.
Do not use this definition: it is only a temporary device to show that this ratio tends almost
everywhere to the Radon-Nikodym derivative.
For almost every point x, sufficiently small sets in a Vitali family around x have positive
measure. (This is a nontrivial result, following from the covering property of Vitali families).
For every point x, sufficiently small sets in a Vitali family around x have finite measure.
(This is a trivial result, following from the fact that the measure is locally finite).
If two measures ρ and ν have, at every point of a set s, arbitrarily small sets in a
Vitali family satisfying ρ a ≤ ν a, then ρ s ≤ ν s if ρ ≪ μ.
If a measure ρ is singular with respect to μ, then for μ almost every x, the ratio
ρ a / μ a tends to zero when a shrinks to x along the Vitali family. This makes sense
as μ a is eventually positive by ae_eventually_measure_pos.
A set of points s satisfying both ρ a ≤ c * μ a and ρ a ≥ d * μ a at arbitrarily small
sets in a Vitali family has measure 0 if c < d. Indeed, the first inequality should imply
that ρ s ≤ c * μ s, and the second one that ρ s ≥ d * μ s, a contradiction if 0 < μ s.
If ρ is absolutely continuous with respect to μ, then for almost every x,
the ratio ρ a / μ a converges as a shrinks to x along a Vitali family for μ.
Given two thresholds p < q, the sets {x | v.lim_ratio ρ x < p}
and {x | q < v.lim_ratio ρ x} are obviously disjoint. The key to proving that v.lim_ratio ρ is
almost everywhere measurable is to show that these sets have measurable supersets which are also
disjoint, up to zero measure. This is the content of this lemma.
A measurable version of v.lim_ratio ρ. Do not use this definition: it is only a temporary
device to show that v.lim_ratio is almost everywhere equal to the Radon-Nikodym derivative.
Equations
- v.lim_ratio_meas hρ = ae_measurable.mk (v.lim_ratio ρ) _
If, for all x in a set s, one has frequently ρ a / μ a < p, then ρ s ≤ p * μ s, as
proved in measure_le_of_frequently_le. Since ρ a / μ a tends almost everywhere to
v.lim_ratio_meas hρ x, the same property holds for sets s on which v.lim_ratio_meas hρ < p.
If, for all x in a set s, one has frequently q < ρ a / μ a, then q * μ s ≤ ρ s, as
proved in measure_le_of_frequently_le. Since ρ a / μ a tends almost everywhere to
v.lim_ratio_meas hρ x, the same property holds for sets s on which q < v.lim_ratio_meas hρ.
The points with v.lim_ratio_meas hρ x = ∞ have measure 0 for μ.
The points with v.lim_ratio_meas hρ x = 0 have measure 0 for ρ.
As an intermediate step to show that μ.with_density (v.lim_ratio_meas hρ) = ρ, we show here
that μ.with_density (v.lim_ratio_meas hρ) ≤ t^2 ρ for any t > 1.
As an intermediate step to show that μ.with_density (v.lim_ratio_meas hρ) = ρ, we show here
that ρ ≤ t μ.with_density (v.lim_ratio_meas hρ) for any t > 1.
Weak version of the main theorem on differentiation of measures: given a Vitali family v
for a locally finite measure μ, and another locally finite 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 version assumes that ρ is absolutely continuous with respect to μ. The general version
without this superfluous assumption is vitali_family.ae_tendsto_rn_deriv.
Main theorem on differentiation of measures: given a Vitali family v for a locally finite
measure μ, and another locally finite 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 μ.
Lebesgue density points #
Given a measurable set s, then μ (s ∩ a) / μ a converges when a shrinks to a typical
point x along a Vitali family. The limit is 1 for x ∈ s and 0 for x ∉ s. This shows that
almost every point of s is a Lebesgue density point for s. A version for non-measurable sets
holds, but it only gives the first conclusion, see ae_tendsto_measure_inter_div.
Given an arbitrary set s, then μ (s ∩ a) / μ a converges to 1 when a shrinks to a
typical point of s along a Vitali family. This shows that almost every point of s is a
Lebesgue density point for s. A stronger version for measurable sets is given
in ae_tendsto_measure_inter_div_of_measurable_set.
Lebesgue differentiation theorem #
Lebesgue differentiation theorem: for almost every point x, the
average of ‖f y - f x‖ on a tends to 0 as a shrinks to x along a Vitali family.
Lebesgue differentiation theorem: for almost every point x, the
average of f on a tends to f x as a shrinks to x along a Vitali family.