English
An iterated-derivative version of the Taylor mean remainder: there exists x' ∈ Ioo(x0,x) such that f(x) − (P_n f)(x0,x) = iteratedDeriv (n+1) f (Icc x0 x) x' · (x−x0)^{n+1}/(n+1)!.
Русский
Версия остатка Тейлора через итеративную производную: существует x' между x0 и x, такое что остаток равен iteratedDeriv(n+1) f в точке x' умноженный на (x−x0)^{n+1}/(n+1)!.
LaTeX
$$$\\exists x' \\in Ioo(x_0,x), \\\\ f(x) - taylorWithinEval f n (Icc x_0 x) x_0 x = iteratedDeriv (n+1) f (Icc x_0 x) x' \\cdot \\frac{(x - x_0)^{n+1}}{(n+1)!}$$$
Lean4
/-- A corollary of Taylor's theorem with the Lagrange form of the remainder. -/
theorem taylor_mean_remainder_lagrange_iteratedDeriv {f : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ} (hx : x₀ < x)
(hf : ContDiffOn ℝ (n + 1) f (Icc x₀ x)) :
∃ x' ∈ Ioo x₀ x,
f x - taylorWithinEval f n (Icc x₀ x) x₀ x = iteratedDeriv (n + 1) f x' * (x - x₀) ^ (n + 1) / (n + 1)! :=
by
have hu : UniqueDiffOn ℝ (Icc x₀ x) := uniqueDiffOn_Icc hx
have hd : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Icc x₀ x) :=
by
refine hf.differentiableOn_iteratedDerivWithin ?_ hu
norm_cast
simp
obtain ⟨x', h1, h2⟩ := taylor_mean_remainder_lagrange hx hf.of_succ (hd.mono Ioo_subset_Icc_self)
use x', h1
rw [h2, iteratedDeriv_eq_iteratedFDeriv, iteratedDerivWithin_eq_iteratedFDerivWithin,
iteratedFDerivWithin_eq_iteratedFDeriv hu _ ⟨le_of_lt h1.1, le_of_lt h1.2⟩]
exact hf.contDiffAt (Icc_mem_nhds_iff.2 h1)
