Theorems · Theorem · measure theory

IsUnifLocDoublingMeasure.exists_eventually_forall_measure_closedBall_le_mul

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

Defined in

Mathlib.MeasureTheory.Measure.Doubling

Cited by

3 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpaceMeasurableSpaceIsUnifLocDoublingMeasure