Documentation

Mathlib.MeasureTheory.Measure.Doubling

Uniformly locally doubling measures #

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 #

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

Instances
    theorem IsUnifLocDoublingMeasure.exists_measure_closedBall_le_mul {α : Type u_1} [MetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [IsUnifLocDoublingMeasure μ] :
    ∃ (C : NNReal), ∀ᶠ (ε : ) in nhdsWithin 0 (Set.Ioi 0), ∀ (x : α), μ (Metric.closedBall x (2 * ε)) C * μ (Metric.closedBall x ε)
    theorem IsUnifLocDoublingMeasure.exists_eventually_forall_measure_closedBall_le_mul {α : Type u_1} [MetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [IsUnifLocDoublingMeasure μ] (K : ) :
    ∃ (C : NNReal), ∀ᶠ (ε : ) in nhdsWithin 0 (Set.Ioi 0), ∀ (x : α), tK, μ (Metric.closedBall x (t * ε)) C * μ (Metric.closedBall x ε)

    A variant of IsUnifLocDoublingMeasure.doublingConstant which allows for scaling the radius by values other than 2.

    Equations
    Instances For

      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 IsUnifLocDoublingMeasure.measure_mul_le_scalingConstantOf_mul.

      Equations
      Instances For