English
If f1 =ᶠ[𝓝 x] f, then the norm of the line derivative is bounded by the Lipschitz bound.
Русский
Если f1 эквивалентно f близко к x то норма линейной производной ограничена липшицевой константой.
LaTeX
$$$(nhds x).EventuallyEq f_{1} f \\Rightarrow \\|\\mathrm{lineDeriv}_{\\mathbb{K}}(f_{1},x,v)\\| \\le C \\|v\\|$ для некоторого C$$
Lean4
/-- Converse to the mean value inequality: if `f` is line differentiable at `x₀` and `C`-lipschitz
on a neighborhood of `x₀` then its line derivative at `x₀` in the direction `v` has norm
bounded by `C * ‖v‖`. This version only assumes that `‖f x - f x₀‖ ≤ C * ‖x - x₀‖` in a
neighborhood of `x`. -/
theorem le_of_lipschitzOn {f : E → F} {f' : F} {x₀ : E} (hf : HasLineDerivAt 𝕜 f f' x₀ v) {s : Set E} (hs : s ∈ 𝓝 x₀)
{C : ℝ≥0} (hlip : LipschitzOnWith C f s) : ‖f'‖ ≤ C * ‖v‖ :=
by
refine hf.le_of_lip' C.coe_nonneg ?_
filter_upwards [hs] with x hx using hlip.norm_sub_le hx (mem_of_mem_nhds hs)
