Structures · Analysis

IsUnifLocDoublingMeasure

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 IsUnifLocDoublingMeasure 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(ε).

Defined in

Mathlib.MeasureTheory.Measure.Doubling

Shape

One type argument · adds exists_measure_closedBall_le_mul''