exists_measure_closedBall_le_mul'

English

There is a fixed constant that bounds the growth of measure from ε to 2ε near zero, uniformly for all centers x.

Русский

Существуют фиксированная константа и равномерность по всем центрам x, задающие верхнюю границу роста меры при переходе от ε к 2ε при стремлении ε к 0.

LaTeX

$$$$ \\forall^*\\varepsilon>0,\\ \\forall x,\\ \\mu(B(x,2\\varepsilon)) \\le \\mathrm{doublingConstant}\\,\\mu(B(x,\\varepsilon)). $$$$

Lean4

theorem exists_measure_closedBall_le_mul' :
    ∀ᶠ ε in 𝓝[>] 0, ∀ x, μ (closedBall x (2 * ε)) ≤ doublingConstant μ * μ (closedBall x ε) :=
  Classical.choose_spec <| exists_measure_closedBall_le_mul μ

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