Integrated Vector Itô Taylor Remainder Bound
ProvedLevyStochCalc.Brownian.Ito.integral_abs_vectorTaylorRemainder_le_affine_readableThis theorem bounds the integrated absolute second-order Taylor remainder of a vector Itô process on a uniform grid. Let (Ω, P) be a probability space, let W be a d-dimensional Brownian motion with filtration ℱ, and let H, X₀, and bdrift satisfy the stated measurability, progressive measurability, and finite ENNReal energy hypotheses. Assume C ≥ 0 and |H(m,k,ω,s)| ≤ C. Assume X₀ is coordinatewise measurable. Let the drift be measurable, let B ≥ 0, and assume |bdrift(p,ω,s)| ≤ B. Let f : (Fin n → ℝ) → ℝ have everywhere-defined first and second Fréchet derivatives f′ and f″, with A ≥ 0, K ≥ 0, continuous f″, and ‖f″(z) − f″(w)‖ ≤ A + K‖z − w‖. For T > 0 and m ≠ 0, the function taylorRemainderNormed along the process vectorItoProcess sampled at unifGrid T m is integrable and its absolute integral is at most
The declaration integral_abs_vectorTaylorRemainder_le_affine_readable supplies an L¹ grid-error estimate for later Itô-formula arguments.
Original Lean declaration header
Within namespace LevyStochCalc.Brownian.Ito. Shown in its original module context. Proof omitted.
theorem integral_abs_vectorTaylorRemainder_le_affine (X₀ : Ω → Fin n → ℝ)
(hX₀ : ∀ p : Fin n, Measurable fun ω => X₀ ω p)
(bdrift : Fin n → Ω → ℝ → ℝ) (hbm : ∀ p, Measurable (Function.uncurry (bdrift p)))
{B : ℝ} (hB0 : 0 ≤ B) (hB : ∀ (p : Fin n) (ω : Ω) (s : ℝ), |bdrift p ω s| ≤ B)
{f : (Fin n → ℝ) → ℝ} {f' : (Fin n → ℝ) → (Fin n → ℝ) →L[ℝ] ℝ}
{f'' : (Fin n → ℝ) → (Fin n → ℝ) →L[ℝ] (Fin n → ℝ) →L[ℝ] ℝ} {A K : ℝ} (hA0 : 0 ≤ A)
(hK0 : 0 ≤ K) (hf : ∀ z, HasFDerivAt f (f' z) z) (hf' : ∀ z, HasFDerivAt f' (f'' z) z)
(hf''c : Continuous f'') (hf'' : ∀ z w, ‖f'' z - f'' w‖ ≤ A + K * ‖z - w‖)
{T : ℝ} (hT : 0 < T) {m : ℕ} (hm0 : m ≠ 0) :
Integrable (fun ω : Ω => taylorRemainderNormed f f' f''
(fun i => vectorItoProcess W ℱ hcoord H hHm hHp hHs X₀ bdrift (unifGrid T m i) ω) m) P
∧ ∫ ω, |taylorRemainderNormed f f' f''
(fun i => vectorItoProcess W ℱ hcoord H hHm hHp hHs X₀ bdrift (unifGrid T m i) ω) m| ∂P
≤ A * ((n : ℝ) * (2 * (B ^ 2 * (T * (T / (m : ℝ)))) + 2 * ((d : ℝ) ^ 2 * (C ^ 2 * T))))
+ K * ((n : ℝ) ^ 2 * ((n : ℝ) * (4 * ((m : ℝ) * (B * (T / (m : ℝ))) ^ 3
+ (d : ℝ) ^ 2 * ((d : ℝ) * ((C ^ 2 + (6 + gaussianFourthMoment) * C ^ 4) / 2
* (T * Real.sqrt (T / (m : ℝ)))))))))
Module navigation
Module: LevyStochCalc/Brownian/VectorItoTaylor.
Definition modules: LevyStochCalc/Brownian/Filtered, LevyStochCalc/Brownian/Multidim, LevyStochCalc/Brownian/ItoFormulaGrid, LevyStochCalc/Brownian/ItoFourthMomentIncrements, LevyStochCalc/Probability/Progressive, LevyStochCalc/Brownian/TaylorTwoVector, LevyStochCalc/Brownian/VectorItoProcess.
Selected supporting theorems: integrable_norm_vectorItoProcess_sub_pow_three, integral_sq_norm_vectorItoProcess_sub_le, measurable_taylorRemainderNormed, sum_integral_norm_vectorItoIncrement_pow_three_le, sum_integral_sq_norm_vectorItoIncrement_le.
Previous: sum_integral_sq_norm_vectorItoIncrement_le.
Source excerpt, lines 113–129 · Frozen source 408915f.
import Definitions.Def_KLSModular_LevyStochCalc_Brownian_VectorItoTaylor
/-
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/VectorItoTaylor.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
open MeasureTheory ProbabilityTheory
open scoped NNReal ENNReal
universe u
variable {Ω : Type u} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P]
{n d : ℕ} (W : LevyStochCalc.Brownian.Multidim.MultidimBrownianMotion P d)
(ℱ : MeasureTheory.Filtration ℝ ‹MeasurableSpace Ω›)
(hcoord : ∀ k : Fin d, LevyStochCalc.Brownian.IsBrownianFiltration (W.W k) ℱ)
(H : Fin n → Fin d → Ω → ℝ → ℝ)
(hHm : ∀ m k, Measurable (Function.uncurry (H m k)))
(hHp : ∀ m k, LevyStochCalc.Probability.ProgressivelyMeasurable ℱ (H m k))
(hHs : ∀ (m : Fin n) (k : Fin d) (T : ℝ), 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
(‖H m k ω s‖₊ : ℝ≥0∞) ^ 2 ∂MeasureTheory.MeasureSpace.volume ∂P < ⊤)
{C : ℝ} (hC0 : 0 ≤ C)
(hCH : ∀ (m : Fin n) (k : Fin d) (ω : Ω) (s : ℝ), |H m k ω s| ≤ C)
include hC0 hCH
theorem LevyStochCalc.Brownian.Ito.integral_abs_vectorTaylorRemainder_le_affine_readable (X₀ : Ω → Fin n → ℝ)
(hX₀ : ∀ p : Fin n, Measurable fun ω => X₀ ω p)
(bdrift : Fin n → Ω → ℝ → ℝ) (hbm : ∀ p, Measurable (Function.uncurry (bdrift p)))
{B : ℝ} (hB0 : 0 ≤ B) (hB : ∀ (p : Fin n) (ω : Ω) (s : ℝ), |bdrift p ω s| ≤ B)
{f : (Fin n → ℝ) → ℝ} {f' : (Fin n → ℝ) → (Fin n → ℝ) →L[ℝ] ℝ}
{f'' : (Fin n → ℝ) → (Fin n → ℝ) →L[ℝ] (Fin n → ℝ) →L[ℝ] ℝ} {A K : ℝ} (hA0 : 0 ≤ A)
(hK0 : 0 ≤ K) (hf : ∀ z, HasFDerivAt f (f' z) z) (hf' : ∀ z, HasFDerivAt f' (f'' z) z)
(hf''c : Continuous f'') (hf'' : ∀ z w, ‖f'' z - f'' w‖ ≤ A + K * ‖z - w‖)
{T : ℝ} (hT : 0 < T) {m : ℕ} (hm0 : m ≠ 0) :
Integrable (fun ω : Ω => taylorRemainderNormed f f' f''
(fun i => vectorItoProcess W ℱ hcoord H hHm hHp hHs X₀ bdrift (unifGrid T m i) ω) m) P
∧ ∫ ω, |taylorRemainderNormed f f' f''
(fun i => vectorItoProcess W ℱ hcoord H hHm hHp hHs X₀ bdrift (unifGrid T m i) ω) m| ∂P
≤ A * ((n : ℝ) * (2 * (B ^ 2 * (T * (T / (m : ℝ)))) + 2 * ((d : ℝ) ^ 2 * (C ^ 2 * T))))
+ K * ((n : ℝ) ^ 2 * ((n : ℝ) * (4 * ((m : ℝ) * (B * (T / (m : ℝ))) ^ 3
+ (d : ℝ) ^ 2 * ((d : ℝ) * ((C ^ 2 + (6 + gaussianFourthMoment) * C ^ 4) / 2
* (T * Real.sqrt (T / (m : ℝ))))))))) := by sorry