taylor_mean_remainder_bound — Mathlib

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

Похожие утверждения