Theorems · Definition · measure theory

IsUnifLocDoublingMeasure.doublingConstant

{α : Type u_1} →
  [inst : PseudoMetricSpace α] →
    [inst_1 : MeasurableSpace α] → (μ : MeasureTheory.Measure α) → [IsUnifLocDoublingMeasure μ] → NNReal

A doubling constant for a uniformly locally doubling measure. See also IsUnifLocDoublingMeasure.scalingConstantOf.

Defined in: Mathlib.MeasureTheory.Measure.Doubling
Cited by: 3 results in Mathlib
Foundations: Depth 172 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: PseudoMetricSpace MeasurableSpace IsUnifLocDoublingMeasure

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
NNRealstatement · cited by 4,310
PseudoMetricSpacestatement and proof · cited by 1,550
IsUnifLocDoublingMeasurestatement and proof · cited by 26
IsUnifLocDoublingMeasure.exists_measure_closedBall_le_mulproof · cited by 1

Cited by3

Results whose statement or proof uses this declaration.

IsUnifLocDoublingMeasure.exists_eventually_forall_measure_closedBall_le_mulproof · cited by 3
IsUnifLocDoublingMeasure.eventually_measure_le_doublingConstant_mulstatement · cited by 1
IsUnifLocDoublingMeasure.doublingConstant.congr_simpstatement and proof · cited by 0