Affine Second-Derivative Taylor Remainder Bound

This theorem gives a second-order Taylor estimate under an affine oscillation bound. Let E be a real normed space, f : E → ℝ, f′ and f″ the first and second Fréchet derivative fields, and A, K : ℝ with A ≥ 0 and K ≥ 0. Assume f and f′ have the stated Fréchet derivatives everywhere, and assume

for all z, w : E. Then, for all x, y : E,

The declaration abs_sub_taylor_two_le_affine_readable is useful when a uniform additive oscillation term and a Lipschitz term are available simultaneously.

Original Lean declaration header

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

theorem abs_sub_taylor_two_le_affine {f : E → ℝ} {f' : E → E →L[ℝ] ℝ}
    {f'' : E → E →L[ℝ] E →L[ℝ] ℝ} {A K : ℝ} (hA0 : 0 ≤ A) (hK0 : 0 ≤ K)
    (hf : ∀ z, HasFDerivAt f (f' z) z) (hf' : ∀ z, HasFDerivAt f' (f'' z) z)
    (hf'' : ∀ z w, ‖f'' z - f'' w‖ ≤ A + K * ‖z - w‖) (x y : E) :
    |f y - f x - f' x (y - x) - f'' x (y - x) (y - x) / 2|
      ≤ A * ‖y - x‖ ^ 2 + K * ‖y - x‖ ^ 3

Module navigation

Module: LevyStochCalc/Brownian/TaylorTwoModulus.

Supporting theorems: abs_sub_taylor_two_le_modulus_normed.

Previous: abs_sub_taylor_two_le_modulus_normed · Next: abs_taylorRemainderNormed_le_affine.

Source excerpt, lines 142–147 · Frozen source 408915f.