Normed-Space Second-Order Taylor Remainder Bound

This is the normed-space version of the second-order Taylor remainder estimate. Let E be a normed additive commutative group and real normed space, let f : E → ℝ, let f′ : E → E →L[ℝ] ℝ, let f″ : E → E →L[ℝ] E →L[ℝ] ℝ, and let M ≥ 0. Assume f and f′ have the indicated Fréchet derivatives at every point. For x, y : E, assume that every z in the segment joining x and y satisfies ‖f″(z) − f″(x)‖ ≤ M. Then, using abs_sub_taylor_two_le_modulus_normed_readable,

The result is dimension-free at the level of arbitrary normed spaces and isolates the dependence on the second-derivative oscillation along one segment.

Original Lean declaration header

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

theorem abs_sub_taylor_two_le_modulus_normed {f : E → ℝ} {f' : E → E →L[ℝ] ℝ}
    {f'' : E → E →L[ℝ] E →L[ℝ] ℝ} {M : ℝ} (hM0 : 0 ≤ M)
    (hf : ∀ z, HasFDerivAt f (f' z) z) (hf' : ∀ z, HasFDerivAt f' (f'' z) z) {x y : E}
    (hM : ∀ z ∈ segment ℝ x y, ‖f'' z - f'' x‖ ≤ M) :
    |f y - f x - f' x (y - x) - f'' x (y - x) (y - x) / 2| ≤ M * ‖y - x‖ ^ 2

Module navigation

Module: LevyStochCalc/Brownian/TaylorTwoModulus.

Supporting theorems: abs_sub_taylor_two_le_modulus.

Previous: abs_sub_taylor_two_le_modulus · Next: abs_sub_taylor_two_le_affine.

Source excerpt, lines 100–104 · Frozen source 408915f.