English
From a convex set and differentiability with HasFDerivWithinAt, there exists a LipschitzOnWith constant on some nhds around x.
Русский
При выпуклости и дифференцируемости существует окрестность вокруг x на которой функция липшицева по некоторой константе.
LaTeX
$$$\exists K, \exists t \in 𝓝[x] , LipschitzOnWith K f t$$$
Lean4
/-- Let `s` be a convex set in a real normed vector space `E`, let `f : E → G` be a function
differentiable within `s` in a neighborhood of `x : E` with derivative `f'`. Suppose that `f'` is
continuous within `s` at `x`. Then for any number `K : ℝ≥0` larger than `‖f' x‖₊`, `f` is Lipschitz
on some neighborhood of `x` within `s`. See also
`Convex.exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt_of_nnnorm_lt` for a version
with an explicit estimate on the Lipschitz constant. -/
theorem exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt (hs : Convex ℝ s) {f : E → G}
(hder : ∀ᶠ y in 𝓝[s] x, HasFDerivWithinAt f (f' y) s y) (hcont : ContinuousWithinAt f' s x) :
∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t :=
(exists_gt _).imp <| hs.exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt_of_nnnorm_lt hder hcont
