lipschitzOnWith_of_abs_le — Mathlib

English

If f is concave on a ball and bounded in absolute value by M, then f is Lipschitz on a smaller ball with some finite constant.

Русский

Если f конкавна на шаре и ограничена сверху- снизу по модулю величины M, то на меньшем шаре f липшицево ограничена.

LaTeX

$$$\\exists K,\\; \\text{LipschitzOnWith}(K)\n f\\; (\\mathrm{ball}\\ x_0, r')$$$

Lean4

theorem lipschitzOnWith_of_abs_le (hf : ConcaveOn ℝ (ball x₀ r) f) (hε : 0 < ε) (hM : ∀ a, dist a x₀ < r → |f a| ≤ M) :
    LipschitzOnWith (2 * M / ε).toNNReal f (ball x₀ (r - ε)) := by
  simpa using hf.neg.lipschitzOnWith_of_abs_le hε <| by simpa using hM

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