English
If L and R are semilinear maps whose composite is linear, and f has derivative f' at Rz, then L ◦ f ◦ R has derivative L ◦ f' ◦ R at z.
Русский
Если L и R — полуправые линейные отображения, композиция линейна, и f имеет производную f' в Rz, то L ∘ f ∘ R имеет производную L ∘ f' ∘ R в z.
LaTeX
$$$\text{HasFDerivAt}(f,f',Rz) \Rightarrow \text{HasFDerivAt}(L \circ f \circ R, L \circ f' \circ R, z)$$$
Lean4
/-- Converse to the mean value inequality: if `f` is differentiable at `x₀` and `C`-lipschitz
on a neighborhood of `x₀` then its derivative at `x₀` has norm bounded by `C`. 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' : E →L[𝕜] F} {x₀ : E} (hf : HasFDerivAt f f' x₀) {C : ℝ} (hC₀ : 0 ≤ C)
(hlip : ∀ᶠ x in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖) : ‖f'‖ ≤ C :=
by
refine le_of_forall_pos_le_add fun ε ε0 => opNorm_le_of_nhds_zero ?_ ?_
· exact add_nonneg hC₀ ε0.le
rw [← map_add_left_nhds_zero x₀, eventually_map] at hlip
filter_upwards [isLittleO_iff.1 (hasFDerivAt_iff_isLittleO_nhds_zero.1 hf) ε0, hlip] with y hy hyC
rw [add_sub_cancel_left] at hyC
calc
‖f' y‖ ≤ ‖f (x₀ + y) - f x₀‖ + ‖f (x₀ + y) - f x₀ - f' y‖ := norm_le_insert _ _
_ ≤ C * ‖y‖ + ε * ‖y‖ := (add_le_add hyC hy)
_ = (C + ε) * ‖y‖ := (add_mul _ _ _).symm
