English
If f is Lipschitz with constant C on a neighborhood, then the norm of its line derivative is at most C times the norm of v.
Русский
Если f липшицова с константой C в окрестности, то норма линейной производной по направлению v не превышает C|v|.
LaTeX
$$$\\text{If } \\text{Lip}(f) \\le C, \\; \\|\\mathrm{lineDeriv}_{\\mathbb{K}}(f,x,v)\\| \\le C \\|v\\|$$$
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‖`. This version only assumes that `‖f x - f x₀‖ ≤ C * ‖x - x₀‖` in a
neighborhood of `x`.
Version using `lineDeriv`. -/
theorem norm_lineDeriv_le_of_lip' {f : E → F} {x₀ : E} {C : ℝ} (hC₀ : 0 ≤ C)
(hlip : ∀ᶠ x in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖) : ‖lineDeriv 𝕜 f x₀ v‖ ≤ C * ‖v‖ :=
by
apply norm_deriv_le_of_lip' (by positivity)
have A : Continuous (fun (t : 𝕜) ↦ x₀ + t • v) := by fun_prop
have : ∀ᶠ x in 𝓝 (x₀ + (0 : 𝕜) • v), ‖f x - f x₀‖ ≤ C * ‖x - x₀‖ := by simpa using hlip
filter_upwards [(A.continuousAt (x := 0)).preimage_mem_nhds this] with t ht
simp only [preimage_setOf_eq, add_sub_cancel_left, norm_smul, mem_setOf_eq, mul_comm (‖t‖)] at ht
simpa [mul_assoc] using ht
