Real Second-Order Taylor Remainder Bound

This is a second-order Taylor remainder estimate for a twice differentiable function on ℝ. Let f, f′, f″ : ℝ → ℝ and M : ℝ satisfy M ≥ 0. Assume f′ is the derivative of f everywhere and f″ is the derivative of f′ everywhere. For x, y : ℝ, assume that every w in the interval between x and y satisfies |f″(w) − f″(x)| ≤ M. Then, with abs_sub_taylor_two_le_modulus_readable, the Taylor remainder obeys

This is the one-dimensional form of the oscillation-controlled Taylor estimate and can be reused when only a bound on the second derivative’s oscillation along the relevant segment is available.

Original Lean declaration header

Within namespace LevyStochCalc. Shown in its original module context. Proof omitted.

theorem abs_sub_taylor_two_le_modulus {f f' f'' : ℝ → ℝ} {M : ℝ} (hM0 : 0 ≤ M)
    (hf : ∀ x, HasDerivAt f (f' x) x) (hf' : ∀ x, HasDerivAt f' (f'' x) x)
    {x y : ℝ} (hM : ∀ w ∈ Set.uIcc x y, |f'' w - f'' x| ≤ M) :
    |f y - f x - f' x * (y - x) - f'' x * (y - x) ^ 2 / 2| ≤ M * |y - x| ^ 2

Module navigation

Module: LevyStochCalc/Brownian/TaylorTwoModulus.

Supporting theorems: abs_sub_taylor_one_le_modulus.

Previous: abs_sub_taylor_one_le_modulus · Next: abs_sub_taylor_two_le_modulus_normed.

Source excerpt, lines 53–56 · Frozen source 408915f.