English
If HasLineDerivAt holds for f and f1 is eventually equal to f near x, then it holds for f1 as well.
Русский
Если линейная производная существует для f, и f1 близка к f, то она существует и для f1.
LaTeX
$$HasLineDerivAt_{\\mathbb{K}}(f,f',x,v) \\Rightarrow (nhds x).EventuallyEq f_{1} f \\,\\Rightarrow \\HasLineDerivAt_{\\mathbb{K}}(f_{1},f',x,v)$$
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_lip' {f : E → F} {f' : F} {x₀ : E} (hf : HasLineDerivAt 𝕜 f f' x₀ v) {C : ℝ} (hC₀ : 0 ≤ C)
(hlip : ∀ᶠ x in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖) : ‖f'‖ ≤ C * ‖v‖ :=
by
apply HasDerivAt.le_of_lip' hf (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
