exists_taylor_mean_remainder_bound

English

There exists x' ∈ Ioo x0 x such that f(x) − (P_n f)(x0, x) equals iteratedDerivWithin (n+1) f (Icc x0 x) x' times (x−x0)^{n+1}/(n+1)!, i.e., a Lagranian-type remainder for iterated derivatives.

Русский

Существует x' ∈ Ioo x0 x, такое что остаток Тейлора с использованием очередной производной имеет форму Лагранжа: остаток равен iteratedDerivWithin (n+1) f (Icc x0 x) x' умноженное на (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 a polynomial bound on the remainder

We assume that `f` is `n+1`-times continuously differentiable on the closed set `Icc a b`.
There exists a constant `C` such that for all `x ∈ Icc a b` the difference of `f` and its `n`-th
Taylor polynomial can be estimated by `C * (x - a)^(n+1)`. -/
theorem exists_taylor_mean_remainder_bound {f : ℝ → E} {a b : ℝ} {n : ℕ} (hab : a ≤ b)
    (hf : ContDiffOn ℝ (n + 1) f (Icc a b)) :
    ∃ C, ∀ x ∈ Icc a b, ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) :=
  by
  rcases eq_or_lt_of_le hab with (rfl | h)
  · refine ⟨0, fun x hx => ?_⟩
    have : x = a := by simpa [← le_antisymm_iff] using hx
    simp [← this]
      -- We estimate by the supremum of the norm of the iterated derivative

  let g : ℝ → ℝ := fun y => ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖
  use SupSet.sSup (g '' Icc a b) / (n !)
  intro x hx
  rw [div_mul_eq_mul_div₀]
  refine taylor_mean_remainder_bound hab hf hx fun y => ?_
  exact (hf.continuousOn_iteratedDerivWithin rfl.le <| uniqueDiffOn_Icc h).norm.le_sSup_image_Icc

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