English
A corollary of the Lagrange form: there exists x' ∈ Ioo(x0,x) with f(x) − (P_n f)(x0,x) = iteratedDerivWithin (n+1) f (Icc x0 x) x' · (x−x0)^{n+1}/(n+1)!.
Русский
Кориоллар Лагранжа: существует x' ∈ Ioo(x0,x), такое что остаток равен производной (n+1)-й итерации, умноженной на (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 = iteratedDerivWithin (n+1) f (Icc x_0 x) x' \\cdot \\frac{(x - x_0)^{n+1}}{(n+1)!}$$$
Lean4
/-- **Taylor's theorem** with the Lagrange form of the remainder.
We assume that `f` is `n+1`-times continuously differentiable in the closed set `Icc x₀ x` and
`n+1`-times differentiable on the open set `Ioo x₀ x`. Then there exists an `x' ∈ Ioo x₀ x` such
that $$f(x) - (P_n f)(x₀, x) = \frac{f^{(n+1)}(x') (x - x₀)^{n+1}}{(n+1)!},$$
where $P_n f$ denotes the Taylor polynomial of degree $n$ and $f^{(n+1)}$ is the $n+1$-th iterated
derivative. -/
theorem taylor_mean_remainder_lagrange {f : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ} (hx : x₀ < x) (hf : ContDiffOn ℝ n f (Icc x₀ x))
(hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)) :
∃ x' ∈ Ioo x₀ x,
f x - taylorWithinEval f n (Icc x₀ x) x₀ x =
iteratedDerivWithin (n + 1) f (Icc x₀ x) x' * (x - x₀) ^ (n + 1) / (n + 1)! :=
by
have gcont : ContinuousOn (fun t : ℝ => (x - t) ^ (n + 1)) (Icc x₀ x) := by fun_prop
have xy_ne : ∀ y : ℝ, y ∈ Ioo x₀ x → (x - y) ^ n ≠ 0 :=
by
intro y hy
refine pow_ne_zero _ ?_
rw [mem_Ioo] at hy
rw [sub_ne_zero]
exact hy.2.ne'
have hg' : ∀ y : ℝ, y ∈ Ioo x₀ x → -(↑n + 1) * (x - y) ^ n ≠ 0 := fun y hy =>
mul_ne_zero (neg_ne_zero.mpr (Nat.cast_add_one_ne_zero n))
(xy_ne y hy)
-- We apply the general theorem with g(t) = (x - t)^(n+1)
rcases taylor_mean_remainder hx hf hf' gcont (fun y _ => monomial_has_deriv_aux y x _) hg' with ⟨y, hy, h⟩
use y, hy
simp only [sub_self, zero_pow, Ne, Nat.succ_ne_zero, not_false_iff, zero_sub, mul_neg] at h
rw [h, neg_div, ← div_neg, neg_mul, neg_neg]
simp [field, xy_ne y hy, Nat.factorial]
