eventually_measure_le_scaling_constant_mul'

English

Same as Scaling-Constant for another formulation; the bound holds under the same hypotheses.

Русский

То же утверждение о константе масштабирования в другой формулировке; неравенство сохраняется при тех же предположениях.

LaTeX

$$$$ \\forall K,\\forall x,\\forall t\\in(0,K],\\forall r,\\ μ(\\overline{B}(x,t r)) \\le \\mathrm{scalingConstantOf}(\\mu,K)\\, μ(\\overline{B}(x,r)). $$$$

Lean4

theorem eventually_measure_le_scaling_constant_mul' (K : ℝ) (hK : 0 < K) :
    ∀ᶠ r in 𝓝[>] 0, ∀ x, μ (closedBall x r) ≤ scalingConstantOf μ K⁻¹ * μ (closedBall x (K * r)) :=
  by
  convert eventually_nhdsGT_zero_mul_left hK (eventually_measure_le_scaling_constant_mul μ K⁻¹)
  simp [inv_mul_cancel_left₀ hK.ne']

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