Doubling measures and Lebesgue's density theorem #
Lebesgue's density theorem states that given a set S
in a sigma compact metric space with
locally-finite doubling measure μ
then for almost all points x
in S
, for any sequence of
closed balls B₀, B₁, B₂, ...
containing x
, the limit μ (S ∩ Bⱼ) / μ (Bⱼ) → 1
as j → ∞
.
In this file we combine general results about existence of Vitali families for doubling measures with results about differentiation along a Vitali family to obtain an explicit form of Lebesgue's density theorem.
Main results #
is_doubling_measure.ae_tendsto_measure_inter_div
: a version of Lebesgue's density theorem for sequences of balls converging on a point but whose centres are not required to be fixed.
A Vitali family in a space with a doubling measure, designed so that the sets at x
contain
all closed_ball y r
when dist x y ≤ K * r
.
Equations
- is_doubling_measure.vitali_family μ K = let R : ℝ := is_doubling_measure.scaling_scale_of μ (linear_order.max (4 * K + 3) 3) in (vitali.vitali_family μ (is_doubling_measure.scaling_constant_of μ (linear_order.max (4 * K + 3) 3)) _).enlarge (R / 4) _
In the Vitali family is_doubling_measure.vitali_family K
, the sets based at x
contain all
balls closed_ball y r
when dist x y ≤ K * r
.
A version of Lebesgue's density theorem for a sequence of closed balls whose centers are not required to be fixed.
See also besicovitch.ae_tendsto_measure_inter_div
.
A version of Lebesgue differentiation theorem for a sequence of closed balls whose centers are not required to be fixed.
A version of Lebesgue differentiation theorem for a sequence of closed balls whose centers are not required to be fixed.