English
If f is strictly differentiable at x with derivative f' and K > ‖f'‖₊, then there exists a neighborhood s of x on which f is Lipschitz with constant K.
Русский
Если f строго дифференцируема в x с производной f' и K больше нормы ‖f'‖₊, то существует окрестность s(x) такой, что f Lipschitz на s с константой K.
LaTeX
$$$ \\text{HasStrictFDerivAt } f\\ f'\\ x \\Rightarrow \\forall K \\,( ‖f'‖_+ < K ) \\Rightarrow ∃ s ∈ 𝓝 x,\\ LipschitzOnWith K\\ f\\ s. $$$
Lean4
/-- If `f` is strictly differentiable at `x` with derivative `f'` and `K > ‖f'‖₊`, then `f` is
`K`-Lipschitz in a neighborhood of `x`. -/
theorem exists_lipschitzOnWith_of_nnnorm_lt (hf : HasStrictFDerivAt f f' x) (K : ℝ≥0) (hK : ‖f'‖₊ < K) :
∃ s ∈ 𝓝 x, LipschitzOnWith K f s :=
by
have := hf.isLittleO.add_isBigOWith (f'.isBigOWith_comp _ _) hK
simp only [sub_add_cancel, IsBigOWith] at this
rcases exists_nhds_square this with ⟨U, Uo, xU, hU⟩
exact ⟨U, Uo.mem_nhds xU, lipschitzOnWith_iff_norm_sub_le.2 fun x hx y hy => hU (mk_mem_prod hx hy)⟩
