English
If f has a formal Taylor series up to order 1 on a set around x, and the 1st coefficient p x 1 is bounded by K, then f is K-Lipschitz in a neighborhood of x within the set.
Русский
Если у функции есть формальная полиномиальная часть порядка 1 на окружении x внутри множества, и первая коэфф. p x 1 ограничена на K, то функция Lipschitz с константой K в окрестности x внутри множества.
LaTeX
$$$HasFTaylorSeriesUpToOn\\ 1\\ f\\ p\\ (insert x s) \\land Convex\\ ℝ\\ s \\land ‖p x 1‖₊ < K\\Rightarrow ∃ 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,
and `‖p x 1‖₊ < K`, then `f` is `K`-Lipschitz in a neighborhood of `x` within `s`. -/
theorem exists_lipschitzOnWith_of_nnnorm_lt {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 : ℝ≥0) (hK : ‖p x 1‖₊ < K) :
∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t :=
by
set f' := fun y => continuousMultilinearCurryFin1 ℝ E F (p y 1)
have hder : ∀ y ∈ s, HasFDerivWithinAt f (f' y) s y := fun y hy =>
(hf.hasFDerivWithinAt le_rfl (subset_insert x s hy)).mono (subset_insert x s)
have hcont : ContinuousWithinAt f' s x :=
(continuousMultilinearCurryFin1 ℝ E F).continuousAt.comp_continuousWithinAt
((hf.cont _ le_rfl _ (mem_insert _ _)).mono (subset_insert x s))
replace hK : ‖f' x‖₊ < K := by simpa only [f', LinearIsometryEquiv.nnnorm_map]
exact
hs.exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt_of_nnnorm_lt
(eventually_nhdsWithin_iff.2 <| Eventually.of_forall hder) hcont K hK
