Measurability of the Normed Taylor Remainder

This is a measurability lemma for a second-order Taylor remainder.

Let $E$ be a second-countable normed real vector space with its Borel measurable structure. Let $f:E\to\mathbb R$, $f':E\to(E\to\mathbb R)$, and $f'':E\to(E\to(E\to\mathbb R))$ be continuous, with the derivative-valued maps interpreted as continuous linear maps. Let $x_i:\Omega\to E$ be measurable for every $i\in\mathbb N$. Then, for every $m\in\mathbb N$,

is measurable.

This technical result supplies measurability of the grid Taylor remainder used in vector Itô-formula estimates.

Formalization Note The exact derivative objects are Lean ContinuousLinearMaps, and the remainder is the definition taylorRemainderNormed.

Original Lean declaration header

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

theorem measurable_taylorRemainderNormed {f : E → ℝ} {f' : E → E →L[ℝ] ℝ}
    {f'' : E → E →L[ℝ] E →L[ℝ] ℝ} (hfc : Continuous f) (hf'c : Continuous f')
    (hf''c : Continuous f'') {x : ℕ → Ω → E} (hx : ∀ i, Measurable (x i)) (m : ℕ) :
    Measurable fun ω => taylorRemainderNormed f f' f'' (fun i => x i ω) m

Module navigation

Module: LevyStochCalc/Brownian/VectorItoTaylor.

Definition modules: LevyStochCalc/Brownian/TaylorTwoVector.

Next: sum_integral_sq_norm_vectorItoIncrement_le.

Source excerpt, lines 41–44 · Frozen source 408915f.