instIsUnifLocDoublingMeasureRealVolume

English

The volume measure on AddCircle Realized by the quotient is uniformly locally doubling with doubling constant 2: vol(B(x,2r)) ≤ 2 vol(B(x,r)) for all x and r.

Русский

Мера объёма на AddCircle является равномерно локально удваиваемой с постоянной удвоения 2: объём окружности вдвое большего радиуса не превышает вдвое объём меньшей окружности.

LaTeX

$$$\\mathrm{vol}(B(x,2r)) \\le 2\\,\\mathrm{vol}(B(x,r))$ for all $x,r \\ge 0$$$

Lean4

instance : IsUnifLocDoublingMeasure (volume : Measure (AddCircle T)) :=
  by
  refine ⟨⟨Real.toNNReal 2, Filter.Eventually.of_forall fun ε x => ?_⟩⟩
  simp only [volume_closedBall]
  erw [← ENNReal.ofReal_mul zero_le_two]
  apply ENNReal.ofReal_le_ofReal
  rw [mul_min_of_nonneg _ _ (zero_le_two : (0 : ℝ) ≤ 2)]
  exact min_le_min (by linarith [hT.out]) (le_refl _)

Похожие утверждения