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 ρ.
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 μ.
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.