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 #
is_doubling_measure
: the definition of a doubling measure (as a typeclass).is_doubling_measure.doubling_constant
: a function yielding the doubling constantC
appearing in the definition of a doubling measure.
- exists_measure_closed_ball_le_mul : ∃ (C : nnreal), ∀ᶠ (ε : ℝ) in nhds_within 0 (set.Ioi 0), ∀ (x : α), ⇑μ (metric.closed_ball x (2 * ε)) ≤ ↑C * ⇑μ (metric.closed_ball x ε)
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 doubling constant for a doubling measure.
See also is_doubling_measure.scaling_constant_of
.
Equations
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
.