Prove2Me

Telescoped Taylor Remainder Along A Sequence

Proved
LevyStochCalc.abs_taylorRemainderNormed_le_affine_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concavevendored-levystochcalc

This theorem bounds the accumulated second-order Taylor remainder along a finite sequence. Let E, f, f′, f″, A, and K satisfy the same normed-space differentiability and nonnegativity assumptions as in abs_sub_taylor_two_le_affine_readable, including ‖f″(z) − f″(w)‖ ≤ A + K‖z − w‖. For a sequence x : ℕ → E and m : ℕ, the definition taylorRemainderNormed satisfies

∣taylorRemainderNormed⁡(f,f′,f′′,x,m)∣≤A∑i<m∥xi+1−xi∥2+K∑i<m∥xi+1−xi∥3.|\operatorname{taylorRemainderNormed}(f,f',f'',x,m)|\le A\sum_{i<m}\|x_{i+1}-x_i\|^2+K\sum_{i<m}\|x_{i+1}-x_i\|^3.

This is the telescoped form of the pointwise affine-modulus estimate and is suited to discretized paths and finite partitions.

Original Lean declaration header

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

theorem abs_taylorRemainderNormed_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 : ℕ → E) (m : ℕ) :
    |taylorRemainderNormed f f' f'' x m|
      ≤ A * ∑ i ∈ Finset.range m, ‖x (i + 1) - x i‖ ^ 2
        + K * ∑ i ∈ Finset.range m, ‖x (i + 1) - x i‖ ^ 3

Module navigation

Module: LevyStochCalc/Brownian/TaylorTwoModulus.

Definition modules: LevyStochCalc/Brownian/TaylorTwoVector.

Supporting theorems: abs_sub_taylor_two_le_affine.

Previous: abs_sub_taylor_two_le_affine.

Source excerpt, lines 167–173 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_LevyStochCalc_Brownian_TaylorTwoModulus

/-
Copyright (c) 2026 Christian Garry. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Christian Garry
-/
-- Vendored from https://github.com/cgarryZA/LevyStochCalc at commit 984dbf0b790031eac05d56fe5a84b65e15e1e932 (upstream path LevyStochCalc/Brownian/TaylorTwoModulus.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
Formal statement

theorem LevyStochCalc.abs_taylorRemainderNormed_le_affine_readable {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 : ℕ → E) (m : ℕ) :
    |taylorRemainderNormed f f' f'' x m|
      ≤ A * ∑ i ∈ Finset.range m, ‖x (i + 1) - x i‖ ^ 2
        + K * ∑ i ∈ Finset.range m, ‖x (i + 1) - x i‖ ^ 3 := by sorry
Source
Lean source: https://github.com/cgarryZA/LevyStochCalc/blob/984dbf0b790031eac05d56fe5a84b65e15e1e932/LevyStochCalc/Brownian/TaylorTwoModulus.lean#L166-L185 (repository human-ai-mathematics/kls-lean, commit 408915f, module `LevyStochCalc.Brownian.TaylorTwoModulus`, declaration `LevyStochCalc.abs_taylorRemainderNormed_le_affine`; the repository is private at upload time). Vendored from https://github.com/cgarryZA/LevyStochCalc at commit 984dbf0b790031eac05d56fe5a84b65e15e1e932 (Apache-2.0; upstream copyright notice retained in the Lean text).

View graph