English
If line derivative exists and a Lipschitz bound holds, then the norm of line derivative is bounded by the Lipschitz bound times the direction norm.
Русский
Если существует линейная производная вдоль направления и есть липшицевское ограничение, то норма линейной производной ограничена липшицевской константой умноженной на норму направления.
LaTeX
$$$\\|\\mathrm{lineDeriv}_{\\mathbb{K}}(f,x,v)\\| \\le C \\|v\\|$ при Lip(f) ≤ C$$
Lean4
/-- Converse to the mean value inequality: if `f` is `C`-lipschitz on a neighborhood of `x₀`
then its line derivative at `x₀` in the direction `v` has norm bounded by `C * ‖v‖`.
Version using `lineDeriv`. -/
theorem norm_lineDeriv_le_of_lipschitzOn {f : E → F} {x₀ : E} {s : Set E} (hs : s ∈ 𝓝 x₀) {C : ℝ≥0}
(hlip : LipschitzOnWith C f s) : ‖lineDeriv 𝕜 f x₀ v‖ ≤ C * ‖v‖ :=
by
refine norm_lineDeriv_le_of_lip' 𝕜 C.coe_nonneg ?_
filter_upwards [hs] with x hx using hlip.norm_sub_le hx (mem_of_mem_nhds hs)
