Second-order Taylor remainder along a sequence

Vendored from the LevyStochCalc library at https://github.com/cgarryZA/LevyStochCalc, commit 984dbf0b790031eac05d56fe5a84b65e15e1e932. For a real-valued function $f$ on a real normed space $E$, first derivative $f':E\to E\toL[\mathbb R]\mathbb R$, second derivative $f'':E\to E\toL[\mathbb R]E\toL[\mathbb R]\mathbb R$, sequence $x_i$, and $m\in\mathbb N$, taylorRemainderNormed is $f(x_m)-f(x_0)$ minus the sum of the first-order increments and the quadratic terms divided by $2$.

Original module imports

import LevyStochCalc.Brownian.TaylorTwo
import Mathlib.Analysis.Calculus.FDeriv.Comp
import Mathlib.Analysis.Calculus.Deriv.Comp

Original declaration excerpt

Shown in the original module context.

noncomputable def taylorRemainderNormed (f : E → ℝ) (f' : E → E →L[ℝ] ℝ)
    (f'' : E → E →L[ℝ] E →L[ℝ] ℝ) (x : ℕ → E) (m : ℕ) : ℝ :=
  f (x m) - f (x 0)
    - ((∑ i ∈ Finset.range m, f' (x i) (x (i + 1) - x i))
      + ∑ i ∈ Finset.range m, f'' (x i) (x (i + 1) - x i) (x (i + 1) - x i) / 2)

Module navigation

Direct project imports: LevyStochCalc/Brownian/TaylorTwo.

Project result: The KLS conjecture.

Original module · LevyStochCalc.Brownian.TaylorTwoVector · Frozen source 408915f.