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

• IsUnifLocDoublingMeasure: the definition of a uniformly locally doubling measure (as a typeclass).
• IsUnifLocDoublingMeasure.doublingConstant: a function yielding the doubling constant C appearing in the definition of a uniformly locally doubling measure.

class IsUnifLocDoublingMeasure {α : Type u_1} [MetricSpace α] [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(ε).

• exists_measure_closedBall_le_mul'' : ∃ (C : NNReal), ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (x : α), ↑↑μ (Metric.closedBall x (2 * ε)) ≤ ↑C * ↑↑μ (Metric.closedBall x ε)

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

def IsUnifLocDoublingMeasure.doublingConstant {α : Type u_1} [MetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [IsUnifLocDoublingMeasure μ] : NNReal

A doubling constant for a uniformly locally doubling measure.

See also IsUnifLocDoublingMeasure.scalingConstantOf.

Equations

• IsUnifLocDoublingMeasure.doublingConstant μ = Classical.choose ⋯

theorem IsUnifLocDoublingMeasure.exists_measure_closedBall_le_mul' {α : Type u_1} [MetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [IsUnifLocDoublingMeasure μ] : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (x : α), ↑↑μ (Metric.closedBall x (2 * ε)) ≤ ↑(IsUnifLocDoublingMeasure.doublingConstant μ) * ↑↑μ (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 : α), ∀ t ≤ K, ↑↑μ (Metric.closedBall x (t * ε)) ≤ ↑C * ↑↑μ (Metric.closedBall x ε)

def IsUnifLocDoublingMeasure.scalingConstantOf {α : Type u_1} [MetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [IsUnifLocDoublingMeasure μ] (K : ℝ) : NNReal

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

Equations

• IsUnifLocDoublingMeasure.scalingConstantOf μ K = max (Classical.choose ⋯) 1

@[simp]

theorem IsUnifLocDoublingMeasure.one_le_scalingConstantOf {α : Type u_1} [MetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [IsUnifLocDoublingMeasure μ] (K : ℝ) : 1 ≤ IsUnifLocDoublingMeasure.scalingConstantOf μ K

theorem IsUnifLocDoublingMeasure.eventually_measure_mul_le_scalingConstantOf_mul {α : Type u_1} [MetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [IsUnifLocDoublingMeasure μ] (K : ℝ) : ∃ (R : ℝ), 0 < R ∧ ∀ (x : α) (t r : ℝ), t ∈ Set.Ioc 0 K → r ≤ R → ↑↑μ (Metric.closedBall x (t * r)) ≤ ↑(IsUnifLocDoublingMeasure.scalingConstantOf μ K) * ↑↑μ (Metric.closedBall x r)

theorem IsUnifLocDoublingMeasure.eventually_measure_le_scaling_constant_mul {α : Type u_1} [MetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [IsUnifLocDoublingMeasure μ] (K : ℝ) : ∀ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (x : α), ↑↑μ (Metric.closedBall x (K * r)) ≤ ↑(IsUnifLocDoublingMeasure.scalingConstantOf μ K) * ↑↑μ (Metric.closedBall x r)

theorem IsUnifLocDoublingMeasure.eventually_measure_le_scaling_constant_mul' {α : Type u_1} [MetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [IsUnifLocDoublingMeasure μ] (K : ℝ) (hK : 0 < K) : ∀ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (x : α), ↑↑μ (Metric.closedBall x r) ≤ ↑(IsUnifLocDoublingMeasure.scalingConstantOf μ K⁻¹) * ↑↑μ (Metric.closedBall x (K * r))

def IsUnifLocDoublingMeasure.scalingScaleOf {α : Type u_1} [MetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [IsUnifLocDoublingMeasure μ] (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 IsUnifLocDoublingMeasure.measure_mul_le_scalingConstantOf_mul.

Equations

• IsUnifLocDoublingMeasure.scalingScaleOf μ K = Exists.choose ⋯

theorem IsUnifLocDoublingMeasure.scalingScaleOf_pos {α : Type u_1} [MetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [IsUnifLocDoublingMeasure μ] (K : ℝ) : 0 < IsUnifLocDoublingMeasure.scalingScaleOf μ K

theorem IsUnifLocDoublingMeasure.measure_mul_le_scalingConstantOf_mul {α : Type u_1} [MetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [IsUnifLocDoublingMeasure μ] {K : ℝ} {x : α} {t : ℝ} {r : ℝ} (ht : t ∈ Set.Ioc 0 K) (hr : r ≤ IsUnifLocDoublingMeasure.scalingScaleOf μ K) : ↑↑μ (Metric.closedBall x (t * r)) ≤ ↑(IsUnifLocDoublingMeasure.scalingConstantOf μ K) * ↑↑μ (Metric.closedBall x r)