English
If f is (n+1)-times continuously differentiable on [a,b] and the (n+1)-th derivative is uniformly bounded by C on [a,b], then the remainder of the Taylor polynomial is bounded by C |x−a|^{n+1}/n! for x in [a,b].
Русский
Если функция $f$ имеет непрерывную $(n+1)$-ю производную на отрезке $[a,b]$ и эта производная ограничена на всём отрезке величиной $C$, то остаток разложения Тейлора удовлетворяет неравенству $\\|f(x)-P_n(f)(x)\\| ≤ C |x-a|^{n+1}/n!$ для $x∈[a,b]$.
LaTeX
$$$a \\le b \\Rightarrow \\text{ContDiffOn}(\\mathbb{R}, n+1, f,[a,b]) \\Rightarrow \\forall x\\in[a,b], \\, \\|f(x) - taylorWithinEval f n (Icc a b) a x\\| \\le C \\frac{|x-a|^{n+1}}{n!}$$$
Lean4
/-- **Taylor's theorem** with a polynomial bound on the remainder
We assume that `f` is `n+1`-times continuously differentiable on the closed set `Icc a b`.
The difference of `f` and its `n`-th Taylor polynomial can be estimated by
`C * (x - a)^(n+1) / n!` where `C` is a bound for the `n+1`-th iterated derivative of `f`. -/
theorem taylor_mean_remainder_bound {f : ℝ → E} {a b C x : ℝ} {n : ℕ} (hab : a ≤ b)
(hf : ContDiffOn ℝ (n + 1) f (Icc a b)) (hx : x ∈ Icc a b)
(hC : ∀ y ∈ Icc a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C) :
‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / n ! :=
by
rcases eq_or_lt_of_le hab with (rfl | h)
· rw [Icc_self, mem_singleton_iff] at hx
simp [hx]
-- The nth iterated derivative is differentiable
have hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b) :=
hf.differentiableOn_iteratedDerivWithin (mod_cast n.lt_succ_self)
(uniqueDiffOn_Icc h)
-- We can uniformly bound the derivative of the Taylor polynomial
have h' :
∀ y ∈ Ico a x,
‖((n ! : ℝ)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (n ! : ℝ)⁻¹ * |x - a| ^ n * C :=
by
rintro y ⟨hay, hyx⟩
rw [norm_smul, Real.norm_eq_abs]
gcongr
· rw [abs_mul, abs_pow, abs_inv, Nat.abs_cast]
gcongr
exact sub_nonneg.2 hyx.le
·
exact
hC y
⟨hay, hyx.le.trans hx.2⟩
-- Apply the mean value theorem for vector-valued functions:
have A :
∀ t ∈ Icc a x,
HasDerivWithinAt (fun y => taylorWithinEval f n (Icc a b) y x)
(((↑n !)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t :=
by
intro t ht
have I : Icc a x ⊆ Icc a b := Icc_subset_Icc_right hx.2
exact (hasDerivWithinAt_taylorWithinEval_at_Icc x h (I ht) hf.of_succ hf').mono I
have := norm_image_sub_le_of_norm_deriv_le_segment' A h' x (right_mem_Icc.2 hx.1)
simp only [taylorWithinEval_self] at this
refine
this.trans_eq
?_
-- The rest is a trivial calculation
rw [abs_of_nonneg (sub_nonneg.mpr hx.1)]
ring