English
There exists a point x' between x0 and x such that f(x) − (P_n f)(x0,x) equals f^{(n+1)}(x') (x−x0)^{n+1}/(n+1)!, i.e., the standard Lagrange form of the remainder.
Русский
Существует точка x' между x0 и x такая, что остаток Тейлора имеет форму Лагранжа: f(x) − P_n f(x0,x) = f^{(n+1)}(x') (x−x0)^{n+1}/(n+1)!, где P_n — полином Тейлора.
LaTeX
$$$\\exists x' \\in Ioo(x_0,x), \\\\ f(x) - taylorWithinEval f n (Icc x_0 x) x_0 x = \\frac{f^{(n+1)}(x') (x - x_0)^{n+1}}{(n+1)!}$$$
Lean4
/-- **Taylor's theorem** with the general mean value 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`, and `g` is a differentiable function on
`Ioo x₀ x` and continuous on `Icc x₀ x`. Then there exists an `x' ∈ Ioo x₀ x` such that
$$f(x) - (P_n f)(x₀, x) = \frac{(x - x')^n}{n!} \frac{g(x) - g(x₀)}{g' x'},$$
where $P_n f$ denotes the Taylor polynomial of degree $n$. -/
theorem taylor_mean_remainder {f : ℝ → ℝ} {g g' : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ} (hx : x₀ < x)
(hf : ContDiffOn ℝ n f (Icc x₀ x)) (hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x))
(gcont : ContinuousOn g (Icc x₀ x)) (gdiff : ∀ x_1 : ℝ, x_1 ∈ Ioo x₀ x → HasDerivAt g (g' x_1) x_1)
(g'_ne : ∀ x_1 : ℝ, x_1 ∈ Ioo x₀ x → g' x_1 ≠ 0) :
∃ x' ∈ Ioo x₀ x,
f x - taylorWithinEval f n (Icc x₀ x) x₀ x =
((x - x') ^ n / n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (Icc x₀ x) x' :=
by
-- We apply the mean value theorem
rcases
exists_ratio_hasDerivAt_eq_ratio_slope (fun t => taylorWithinEval f n (Icc x₀ x) t x)
(fun t => ((n ! : ℝ)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc x₀ x) t) hx
(continuousOn_taylorWithinEval (uniqueDiffOn_Icc hx) hf)
(fun _ hy => taylorWithinEval_hasDerivAt_Ioo x hx hy hf hf') g g' gcont gdiff with
⟨y, hy, h⟩
use y, hy
simp only [taylorWithinEval_self] at h
rw [mul_comm, ← div_left_inj' (g'_ne y hy), mul_div_cancel_right₀ _ (g'_ne y hy)] at h
rw [← h]
simp [field]
-- see https://github.com/leanprover-community/mathlib4/issues/29041
