mathlib3documentation

measure_theory.measure.doubling

Uniformly locally doubling measures #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• is_unif_loc_doubling_measure: the definition of a uniformly locally doubling measure (as a typeclass).
• is_unif_loc_doubling_measure.doubling_constant: a function yielding the doubling constant C appearing in the definition of a uniformly locally doubling measure.
@[class]

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 is_unif_loc_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_unif_loc_doubling_measure
• is_unif_loc_doubling_measure.has_sizeof_inst

A doubling constant for a uniformly locally doubling measure.

See also is_unif_loc_doubling_measure.scaling_constant_of.

Equations

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

Equations
theorem is_unif_loc_doubling_measure.eventually_measure_mul_le_scaling_constant_of_mul {α : Type u_1} [metric_space α] (μ : measure_theory.measure α) (K : ) :
(R : ), 0 < R (x : α) (t r : ), t K r R μ (t * r))
theorem is_unif_loc_doubling_measure.eventually_measure_le_scaling_constant_mul' {α : Type u_1} [metric_space α] (μ : measure_theory.measure α) (K : ) (hK : 0 < K) :
∀ᶠ (r : ) in (set.Ioi 0), (x : α), μ r) * μ (K * r))
noncomputable def is_unif_loc_doubling_measure.scaling_scale_of {α : Type u_1} [metric_space α] (μ : measure_theory.measure α) (K : ) :

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
theorem is_unif_loc_doubling_measure.measure_mul_le_scaling_constant_of_mul {α : Type u_1} [metric_space α] (μ : measure_theory.measure α) {K : } {x : α} {t r : } (ht : t K) (hr : r ) :
μ (t * r))