exists_lipschitzOnWith_of_isBounded

English

Let hf be a concave function on a ball. If the image hf(B(x0,r)) is bounded, then there exists K such that hf is Lipschitz on B(x0,r') with r'<r.

Русский

Пусть hf является выпукло-ограниченной на шаре; тогда существует K, так что hf липшицево ограничена на меньшем шаре.

LaTeX

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

Lean4

theorem exists_lipschitzOnWith_of_isBounded (hf : ConcaveOn ℝ (ball x₀ r) f) (hr : r' < r)
    (hf' : IsBounded (f '' ball x₀ r)) : ∃ K, LipschitzOnWith K f (ball x₀ r') :=
  by
  replace hf' : IsBounded ((-f) '' ball x₀ r) := by convert hf'.neg; ext; simp [neg_eq_iff_eq_neg]
  simpa using hf.neg.exists_lipschitzOnWith_of_isBounded hr hf'

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