Theorems · Theorem · measure theory

IsUnifLocDoublingMeasure.eventually_measure_le_scaling_constant_mul

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

Defined in

Mathlib.MeasureTheory.Measure.Doubling

Cited by

1 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpaceMeasurableSpaceIsUnifLocDoublingMeasure