# 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.

## References #

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

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.

## Equations

- VitaliFamily.limRatio v ρ x = limUnder (VitaliFamily.filterAt v x) fun (a : Set α) => ↑↑ρ a / ↑↑μ a

## Instances For

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.limRatio ρ x < p}`

and `{x | q < v.limRatio ρ x}`

are obviously disjoint. The key to proving that `v.limRatio ρ`

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.limRatio ρ`

. Do *not* use this definition: it is only a temporary
device to show that `v.limRatio`

is almost everywhere equal to the Radon-Nikodym derivative.

## Equations

- VitaliFamily.limRatioMeas v hρ = AEMeasurable.mk (VitaliFamily.limRatio v ρ) ⋯

## Instances For

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.limRatioMeas hρ x`

, the same property holds for sets `s`

on which `v.limRatioMeas 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.limRatioMeas hρ x`

, the same property holds for sets `s`

on which `q < v.limRatioMeas hρ`

.

The points with `v.limRatioMeas hρ x = ∞`

have measure `0`

for `μ`

.

The points with `v.limRatioMeas hρ x = 0`

have measure `0`

for `ρ`

.

As an intermediate step to show that `μ.withDensity (v.limRatioMeas hρ) = ρ`

, we show here
that `μ.withDensity (v.limRatioMeas hρ) ≤ t^2 ρ`

for any `t > 1`

.

As an intermediate step to show that `μ.withDensity (v.limRatioMeas hρ) = ρ`

, we show here
that `ρ ≤ t μ.withDensity (v.limRatioMeas 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 `VitaliFamily.ae_tendsto_rnDeriv`

.

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_measurableSet`

.

### 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.