English
If f is Lipschitz on a set s around x0 with constant C, then the operator norm of its derivative is bounded by C.
Русский
Если f на множестве s окрестности x0 Lipschitz c, то нормa оператора производной не больше C.
LaTeX
$$$\text{If } \mathrm{LipschitzOnWith}(C,f,s) \text{ near } x_0, \|f'(x_0)\| \le C$$$
Lean4
/-- Converse to the mean value inequality: if `f` is `C`-lipschitz
on a neighborhood of `x₀` then its derivative at `x₀` has norm bounded by `C`.
Version using `fderiv`. -/
theorem norm_fderiv_le_of_lipschitzOn {f : E → F} {x₀ : E} {s : Set E} (hs : s ∈ 𝓝 x₀) {C : ℝ≥0}
(hlip : LipschitzOnWith C f s) : ‖fderiv 𝕜 f x₀‖ ≤ C :=
by
refine norm_fderiv_le_of_lip' 𝕜 C.coe_nonneg ?_
filter_upwards [hs] with x hx using hlip.norm_sub_le hx (mem_of_mem_nhds hs)
