English
Under convexity and differentiability hypotheses, the remainder of the Taylor expansion, scaled by (x−x0)^n, tends to zero as x approaches x0 within s.
Русский
При выпуклости и дифференцируемости остаток разложения Тейлора, делённый на (x−x0)^n, стремится к нулю при приближении x к x0 внутри s.
LaTeX
$$$\\text{If } hs: \\text{Convex } \\mathbb{R} \\, s, hx_0s: x_0 \\in s, hf: \\ ContDiffOn\\\\ On\\ Real n f s, \\\\ (isLittleO) : \\\\ isLittleO (f(x) - taylorWithinEval f n s x_0 x) (x - x_0)^n$, then \n$\\lim_{x\\to x_0, x\\in s} ( (x - x_0)^{-n} (f(x) - taylorWithinEval f n s x_0 x) ) = 0$$$
Lean4
/-- **Taylor's theorem** as a limit. -/
theorem taylor_tendsto {f : ℝ → E} {x₀ : ℝ} {n : ℕ} {s : Set ℝ} (hs : Convex ℝ s) (hx₀s : x₀ ∈ s)
(hf : ContDiffOn ℝ n f s) :
Filter.Tendsto (fun x ↦ ((x - x₀) ^ n)⁻¹ • (f x - taylorWithinEval f n s x₀ x)) (𝓝[s] x₀) (𝓝 0) :=
by
have h_isLittleO := (taylor_isLittleO hs hx₀s hf).norm_norm
rw [Asymptotics.isLittleO_iff_tendsto] at h_isLittleO
· rw [tendsto_zero_iff_norm_tendsto_zero]
simpa [norm_smul, div_eq_inv_mul] using h_isLittleO
· simp only [norm_pow, Real.norm_eq_abs, pow_eq_zero_iff', abs_eq_zero, ne_eq, norm_eq_zero, and_imp]
intro x hx
rw [sub_eq_zero] at hx
simp [hx]
