English
For real-valued f, the same Taylor remainder limit holds, i.e., the quotient by (x−x0)^n tends to zero as x approaches x0 from s.
Русский
Для вещественно-значной функции выполняется та же граница остатка Тейлора: частное на (x−x0)^n стремится к нулю при приближении x к x0.
LaTeX
$$$\\text{Under the Real setting } \\lim_{x\\to x_0, x\\in s} \\frac{f(x) - taylorWithinEval f n s x_0 x}{(x-x_0)^n} = 0$$$
Lean4
/-- **Taylor's theorem** as a limit. -/
theorem taylor_tendsto {f : ℝ → ℝ} {x₀ : ℝ} {n : ℕ} {s : Set ℝ} (hs : Convex ℝ s) (hx₀s : x₀ ∈ s)
(hf : ContDiffOn ℝ n f s) :
Filter.Tendsto (fun x ↦ (f x - taylorWithinEval f n s x₀ x) / (x - x₀) ^ n) (𝓝[s] x₀) (𝓝 0) :=
by
convert _root_.taylor_tendsto hs hx₀s hf using 2 with x
simp [div_eq_inv_mul]
