# mathlib3documentation

measure_theory.covering.differentiation

# 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_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.
• vitali_family.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 (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 #

noncomputable def vitali_family.lim_ratio {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) (ρ : measure_theory.measure α) (x : α) :

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
theorem vitali_family.ae_eventually_measure_pos {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ)  :
∀ᵐ (x : α) μ, ∀ᶠ (a : set α) in v.filter_at x, 0 < μ a

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

theorem vitali_family.eventually_measure_lt_top {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) (x : α) :
∀ᶠ (a : set α) in v.filter_at x, μ a <

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

theorem vitali_family.measure_le_of_frequently_le {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) [borel_space α] {ρ : measure_theory.measure α} (ν : measure_theory.measure α) (hρ : ρ.absolutely_continuous μ) (s : set α) (hs : (x : α), x s (∃ᶠ (a : set α) in v.filter_at x, ρ a ν a)) :
ρ s ν s

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

theorem vitali_family.ae_eventually_measure_zero_of_singular {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) [borel_space α] {ρ : measure_theory.measure α} (hρ : ρ.mutually_singular μ) :
∀ᵐ (x : α) μ, filter.tendsto (λ (a : set α), ρ a / μ a) (v.filter_at x) (nhds 0)

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.

theorem vitali_family.null_of_frequently_le_of_frequently_ge {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) [borel_space α] {ρ : measure_theory.measure α} (hρ : ρ.absolutely_continuous μ) {c d : nnreal} (hcd : c < d) (s : set α) (hc : (x : α), x s (∃ᶠ (a : set α) in v.filter_at x, ρ a c * μ a)) (hd : (x : α), x s (∃ᶠ (a : set α) in v.filter_at x, d * μ a ρ a)) :
μ s = 0

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.

theorem vitali_family.ae_tendsto_div {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) [borel_space α] {ρ : measure_theory.measure α} (hρ : ρ.absolutely_continuous μ) :
∀ᵐ (x : α) μ, (c : ennreal), filter.tendsto (λ (a : set α), ρ a / μ a) (v.filter_at x) (nhds c)

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

theorem vitali_family.ae_tendsto_lim_ratio {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) [borel_space α] {ρ : measure_theory.measure α} (hρ : ρ.absolutely_continuous μ) :
∀ᵐ (x : α) μ, filter.tendsto (λ (a : set α), ρ a / μ a) (v.filter_at x) (nhds (v.lim_ratio ρ x))
theorem vitali_family.exists_measurable_supersets_lim_ratio {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) [borel_space α] {ρ : measure_theory.measure α} (hρ : ρ.absolutely_continuous μ) {p q : nnreal} (hpq : p < q) :
(a b : set α), {x : α | v.lim_ratio ρ x < p} a {x : α | q < v.lim_ratio ρ x} b μ (a b) = 0

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.

noncomputable def vitali_family.lim_ratio_meas {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) [borel_space α] {ρ : measure_theory.measure α} (hρ : ρ.absolutely_continuous μ) :

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
theorem vitali_family.ae_tendsto_lim_ratio_meas {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) [borel_space α] {ρ : measure_theory.measure α} (hρ : ρ.absolutely_continuous μ) :
∀ᵐ (x : α) μ, filter.tendsto (λ (a : set α), ρ a / μ a) (v.filter_at x) (nhds (v.lim_ratio_meas x))
theorem vitali_family.measure_le_mul_of_subset_lim_ratio_meas_lt {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) [borel_space α] {ρ : measure_theory.measure α} (hρ : ρ.absolutely_continuous μ) {p : nnreal} {s : set α} (h : s {x : α | v.lim_ratio_meas x < p}) :
ρ s p * μ s

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.

theorem vitali_family.mul_measure_le_of_subset_lt_lim_ratio_meas {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) [borel_space α] {ρ : measure_theory.measure α} (hρ : ρ.absolutely_continuous μ) {q : nnreal} {s : set α} (h : s {x : α | q < v.lim_ratio_meas x}) :
q * μ s ρ s

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

theorem vitali_family.measure_lim_ratio_meas_top {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) [borel_space α] {ρ : measure_theory.measure α} (hρ : ρ.absolutely_continuous μ) :
μ {x : α | v.lim_ratio_meas x = } = 0

The points with v.lim_ratio_meas hρ x = ∞ have measure 0 for μ.

theorem vitali_family.measure_lim_ratio_meas_zero {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) [borel_space α] {ρ : measure_theory.measure α} (hρ : ρ.absolutely_continuous μ) :
ρ {x : α | v.lim_ratio_meas x = 0} = 0

The points with v.lim_ratio_meas hρ x = 0 have measure 0 for ρ.

theorem vitali_family.with_density_le_mul {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) [borel_space α] {ρ : measure_theory.measure α} (hρ : ρ.absolutely_continuous μ) {s : set α} (hs : measurable_set s) {t : nnreal} (ht : 1 < t) :
(μ.with_density (v.lim_ratio_meas hρ)) s t ^ 2 * ρ s

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.

theorem vitali_family.le_mul_with_density {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) [borel_space α] {ρ : measure_theory.measure α} (hρ : ρ.absolutely_continuous μ) {s : set α} (hs : measurable_set s) {t : nnreal} (ht : 1 < t) :

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.

theorem vitali_family.ae_tendsto_rn_deriv_of_absolutely_continuous {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) [borel_space α] {ρ : measure_theory.measure α} (hρ : ρ.absolutely_continuous μ) :
∀ᵐ (x : α) μ, filter.tendsto (λ (a : set α), ρ a / μ a) (v.filter_at x) (nhds (ρ.rn_deriv μ x))

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.

theorem vitali_family.ae_tendsto_rn_deriv {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) [borel_space α] (ρ : measure_theory.measure α)  :
∀ᵐ (x : α) μ, filter.tendsto (λ (a : set α), ρ a / μ a) (v.filter_at x) (nhds (ρ.rn_deriv μ x))

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 #

theorem vitali_family.ae_tendsto_measure_inter_div_of_measurable_set {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) [borel_space α] {s : set α} (hs : measurable_set s) :
∀ᵐ (x : α) μ, filter.tendsto (λ (a : set α), μ (s a) / μ a) (v.filter_at x) (nhds (s.indicator 1 x))

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.

theorem vitali_family.ae_tendsto_measure_inter_div {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) [borel_space α] (s : set α) :
∀ᵐ (x : α) μ.restrict s, filter.tendsto (λ (a : set α), μ (s a) / μ a) (v.filter_at x) (nhds 1)

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 #

theorem vitali_family.ae_tendsto_lintegral_div' {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) [borel_space α] {f : α ennreal} (hf : measurable f) (h'f : ∫⁻ (y : α), f y μ ) :
∀ᵐ (x : α) μ, filter.tendsto (λ (a : set α), ∫⁻ (y : α) in a, f y μ / μ a) (v.filter_at x) (nhds (f x))
theorem vitali_family.ae_tendsto_lintegral_div {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) [borel_space α] {f : α ennreal} (hf : μ) (h'f : ∫⁻ (y : α), f y μ ) :
∀ᵐ (x : α) μ, filter.tendsto (λ (a : set α), ∫⁻ (y : α) in a, f y μ / μ a) (v.filter_at x) (nhds (f x))
theorem vitali_family.ae_tendsto_lintegral_nnnorm_sub_div' {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) {E : Type u_2} [borel_space α] {f : α E} (hf : μ)  :
∀ᵐ (x : α) μ, filter.tendsto (λ (a : set α), ∫⁻ (y : α) in a, f y - f x‖₊ μ / μ a) (v.filter_at x) (nhds 0)
theorem vitali_family.ae_tendsto_lintegral_nnnorm_sub_div {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) {E : Type u_2} [borel_space α] {f : α E} (hf : μ) :
∀ᵐ (x : α) μ, filter.tendsto (λ (a : set α), ∫⁻ (y : α) in a, f y - f x‖₊ μ / μ a) (v.filter_at x) (nhds 0)
theorem vitali_family.ae_tendsto_average_norm_sub {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) {E : Type u_2} [borel_space α] {f : α E} (hf : μ) :
∀ᵐ (x : α) μ, filter.tendsto (λ (a : set α), (y : α) in a, f y - f x μ) (v.filter_at x) (nhds 0)

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.

theorem vitali_family.ae_tendsto_average {α : Type u_1} [metric_space α] {m0 : measurable_space α} {μ : measure_theory.measure α} (v : vitali_family μ) {E : Type u_2} [borel_space α] [ E] {f : α E} (hf : μ) :
∀ᵐ (x : α) μ, filter.tendsto (λ (a : set α), (y : α) in a, f y μ) (v.filter_at x) (nhds (f x))

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.