mathlib documentation

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

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 μ) [topological_space.second_countable_topology α] :
∀ᵐ (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 μ) [measure_theory.is_locally_finite_measure μ] (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 μ) [sigma_compact_space α] [borel_space α] {ρ : measure_theory.measure α} (ν : measure_theory.measure α) [measure_theory.is_locally_finite_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 ρ ≪ μ.

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 μ) [sigma_compact_space α] [borel_space α] [measure_theory.is_locally_finite_measure μ] {ρ : measure_theory.measure α} [measure_theory.is_locally_finite_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 μ) [sigma_compact_space α] [borel_space α] [measure_theory.is_locally_finite_measure μ] {ρ : measure_theory.measure α} [measure_theory.is_locally_finite_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 μ.

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

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

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 μ) [sigma_compact_space α] [borel_space α] [measure_theory.is_locally_finite_measure μ] {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 μ) [sigma_compact_space α] [borel_space α] [measure_theory.is_locally_finite_measure μ] (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.