Theorems · Theorem · measure theory

IsUnifLocDoublingMeasure.exists_measure_closedBall_le_mul

∀ {α : Type u_1} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] (μ : MeasureTheory.Measure α)
  [IsUnifLocDoublingMeasure μ],
  ∃ C,
    ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (x : α), μ (Metric.closedBall x (2 * ε)) ≤ ↑C * μ (Metric.closedBall x ε)

Defined in

Mathlib.MeasureTheory.Measure.Doubling

Cited by

1 results in Mathlib

Foundations

Depth 171 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoMetricSpaceMeasurableSpaceIsUnifLocDoublingMeasure