Theorems · Theorem · measure theory

IsUnifLocDoublingMeasure.eventually_measure_le_doublingConstant_mul

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

Defined in

Mathlib.MeasureTheory.Measure.Doubling

Cited by

1 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpaceMeasurableSpaceIsUnifLocDoublingMeasure