Theorems · Inductive type · measure theory

IsUnifLocDoublingMeasure

{α : Type u_1} → [PseudoMetricSpace α] → [inst : MeasurableSpace α] → MeasureTheory.Measure α → Prop

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

Cited by

26 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

PseudoMetricSpaceMeasurableSpace