English
There exists x' ∈ Ioo(x0,x) such that f(x) − (P_n f)(x0,x) = f^{(n+1)}(x') (x−x')^n (x−x0)/n!.
Русский
Существует x' между x0 и x, такое что остаток равен f^{(n+1)}(x') (x−x')^n (x−x0)/n!.
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')^{n} (x - x_0)}{n!}$$$
Lean4
/-- **Taylor's theorem** with the Cauchy form of the remainder.
We assume that `f` is `n+1`-times continuously differentiable on 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 (x-x₀)}{n!},$$
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_cauchy {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 / n ! * (x - x₀) :=
by
have gcont : ContinuousOn id (Icc x₀ x) := by fun_prop
have gdiff : ∀ x_1 : ℝ, x_1 ∈ Ioo x₀ x → HasDerivAt id ((fun _ : ℝ => (1 : ℝ)) x_1) x_1 := fun _ _ =>
hasDerivAt_id
_
-- We apply the general theorem with g = id
rcases taylor_mean_remainder hx hf hf' gcont gdiff fun _ _ => by simp with ⟨y, hy, h⟩
use y, hy
rw [h]
simp [field]
