eventually_measure_le_scaling_constant_mul

English

For K, x, t, r with t ∈ (0,K] and r ≤ scalingScaleOf μ K, we have μ(B(x, t r)) ≤ scalingConstantOf μ K μ(B(x,r)).

Русский

Для K, x, t, r с t∈(0,K] и r ≤ scalingScaleOf μ K выполняется μ(B(x,t r)) ≤ scalingConstantOf μ K μ(B(x,r)).

LaTeX

$$$$ \\forall K\\in\\mathbb{R},\\forall x\\in\\alpha,\\forall t\\in(0,K],\\forall r\\leqslant scalingScaleOf(\\mu,K),\\ \\mu(\\overline{B}(x,t r)) \\le \\mathrm{scalingConstantOf}(\\mu,K)\\, \\mu(\\overline{B}(x,r)). $$$$

Lean4

theorem eventually_measure_le_scaling_constant_mul (K : ℝ) :
    ∀ᶠ r in 𝓝[>] 0, ∀ x, μ (closedBall x (K * r)) ≤ scalingConstantOf μ K * μ (closedBall x r) :=
  by
  filter_upwards [Classical.choose_spec (exists_eventually_forall_measure_closedBall_le_mul μ K)] with r hr x
  exact (hr x K le_rfl).trans (mul_le_mul_right' (ENNReal.coe_le_coe.2 (le_max_left _ _)) _)

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