English
Near a, HasStrictFDerivAt f f' a yields existence of neighborhood s with ApproximatesLinearOn f f' s c for some c > 0.
Русский
Рядом с a существует окрестность s такая, что f аппроксимируется линейно на s с константой c > 0.
LaTeX
$$$\exists s \in 𝓝 a, ApproximatesLinearOn f f' s c$$$
Lean4
/-- If `f` has derivative `f'` at `a` in the strict sense and `c > 0`, then `f` approximates `f'`
with constant `c` on some neighborhood of `a`. -/
theorem approximates_deriv_on_nhds {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f f' a) {c : ℝ≥0}
(hc : Subsingleton E ∨ 0 < c) : ∃ s ∈ 𝓝 a, ApproximatesLinearOn f f' s c :=
by
rcases hc with hE | hc
· refine ⟨univ, IsOpen.mem_nhds isOpen_univ trivial, fun x _ y _ => ?_⟩
simp [@Subsingleton.elim E hE x y]
have := hf.isLittleO.def hc
rw [nhds_prod_eq, Filter.Eventually, mem_prod_same_iff] at this
rcases this with ⟨s, has, hs⟩
exact ⟨s, has, fun x hx y hy => hs (mk_mem_prod hx hy)⟩
