English
If f has a formal Taylor series up to order 1 around x, and the domain set is convex, then there exists a neighborhood of x on which f is Lipschitz with some constant K.
Русский
Если у функции есть формальная Taylor-полином порядка 1 около точки x и область выпукла, существует окрестность x, на которой f Lipschitz с некоторой константой K.
LaTeX
$$$HasFTaylorSeriesUpToOn\\ 1\\ f\\ p\\ (insert x s)\\land Convex\\ ℝ\\ s\\Rightarrow ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t$$$
Lean4
/-- If `f` has a formal Taylor series `p` up to order `1` on `{x} ∪ s`, where `s` is a convex set,
then `f` is Lipschitz in a neighborhood of `x` within `s`. -/
theorem exists_lipschitzOnWith {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F]
[NormedSpace ℝ F] {f : E → F} {p : E → FormalMultilinearSeries ℝ E F} {s : Set E} {x : E}
(hf : HasFTaylorSeriesUpToOn 1 f p (insert x s)) (hs : Convex ℝ s) : ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t :=
(exists_gt _).imp <| hf.exists_lipschitzOnWith_of_nnnorm_lt hs
