mathlib3 documentation

measure_theory.measure.doubling

Uniformly locally doubling measures #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A uniformly locally doubling measure μ on a metric space is a measure for which there exists a constant C such that for all sufficiently small radii ε, and for any centre, the measure of a ball of radius 2 * ε is bounded by C times the measure of the concentric ball of radius ε.

This file records basic facts about uniformly locally doubling measures.

Main definitions #

@[class]

A measure μ is said to be a uniformly locally doubling measure if there exists a constant C such that for all sufficiently small radii ε, and for any centre, the measure of a ball of radius 2 * ε is bounded by C times the measure of the concentric ball of radius ε.

Note: it is important that this definition makes a demand only for sufficiently small ε. For example we want hyperbolic space to carry the instance is_unif_loc_doubling_measure volume but volumes grow exponentially in hyperbolic space. To be really explicit, consider the hyperbolic plane of curvature -1, the area of a disc of radius ε is A(ε) = 2π(cosh(ε) - 1) so A(2ε)/A(ε) ~ exp(ε).

Instances of this typeclass
Instances of other typeclasses for is_unif_loc_doubling_measure
  • is_unif_loc_doubling_measure.has_sizeof_inst

A scale below which the doubling measure μ satisfies good rescaling properties when one multiplies the radius of balls by at most K, as stated in measure_mul_le_scaling_constant_of_mul.

Equations