∀ {α : 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 ε)