mathlib documentation

measure_theory.measure.doubling

Doubling measures #

A 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 files on doubling measures.

Main definitions #

@[class]

A measure μ is said to be a 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_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_doubling_measure
  • is_doubling_measure.has_sizeof_inst

A variant of is_doubling_measure.doubling_constant which allows for scaling the radius by values other than 2.

Equations

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