Vector Itô Formula Almost Everywhere
ProvedLevyStochCalc.Brownian.Ito.IsVectorItoVersion.itoFormula_readableThis theorem formalizes the vector Itô formula. Let (Ω, P) be a probability space, W a d-dimensional Brownian motion with filtration ℱ, H a measurable and progressively measurable diffusion coefficient satisfying the stated finite ENNReal square-energy conditions, and X an IsVectorItoVersion with measurable initial value X₀ and measurable bounded drift bdrift. Assume H is bounded by C ≥ 0, the drift is bounded by B ≥ 0, and the required measurability, progressive measurability, and finite-energy conditions hold for H(p,k)+H(q,k). Let f : (Fin n → ℝ) → ℝ have everywhere-defined first and second Fréchet derivatives f′ and f″, with ‖f′(z)‖ ≤ K₁, 0 ≤ K₂, ‖f″(z)‖ ≤ K₂, continuous f″, and the explicit uniform-continuity condition
Assume also the products coordDeriv f′ p (X s ω) * H p k ω s are measurable, progressively measurable, and have finite ENNReal square energy. For T > 0, outside a P-null set,
The result is the qualitative vector Itô formula obtained from the quantitative grid-error estimate.
Original Lean conclusion excerpt
Within namespace LevyStochCalc.Brownian.Ito. Shown in its original module context. Earlier hypotheses and the proof are omitted from this excerpt; the complete verified statement remains below.
fun ω s => coordDeriv f' p (X s ω) * H p k ω s)
(hqg : ∀ (p : Fin n) (k : Fin d) (T' : ℝ), 0 < T' → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T',
(‖coordDeriv f' p (X s ω) * H p k ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
{T : ℝ} (hT : 0 < T) :
(fun ω : Ω => f (X T ω) - f (X 0 ω)) =ᵐ[P] fun ω : Ω =>
(∑ p : Fin n, ∫ s in Set.Ioc (0 : ℝ) T,
coordDeriv f' p (X s ω) * bdrift p ω s ∂volume)
+ (∑ p : Fin n, ∑ k : Fin d, stochasticIntegralBrownian (W.W k) ℱ (hcoord k)
(fun ω s => coordDeriv f' p (X s ω) * H p k ω s)
(hmg p k) (hpg p k) (hqg p k) T ω)
+ 1 / 2 * ∑ p : Fin n, ∑ q : Fin n, ∫ s in Set.Ioc (0 : ℝ) T,
coordDeriv₂ f'' p q (X s ω) * ∑ k : Fin d, H p k ω s * H q k ω s ∂volume
Module navigation
Module: LevyStochCalc/Brownian/VectorItoFormula.
Definition modules: LevyStochCalc/Brownian/ItoL2CompletionMaster, LevyStochCalc/Brownian/Filtered, LevyStochCalc/Brownian/Multidim, LevyStochCalc/Brownian/CoordDerivative, LevyStochCalc/Probability/Progressive, LevyStochCalc/Brownian/VectorItoProcessVersion.
Supporting theorems: IsVectorItoVersion.integral_abs_vectorItoFormula_le.
Previous: IsVectorItoVersion.integral_abs_vectorItoFormula_le.
Source excerpt, lines 387–398 · Frozen source 408915f.
import Definitions.Def_KLSModular_LevyStochCalc_Brownian_VectorItoFormula
/-
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/VectorItoFormula.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
open MeasureTheory ProbabilityTheory
open scoped NNReal ENNReal Topology
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 : ∀ p k, Measurable (Function.uncurry (H p k))}
{hHp : ∀ p k, LevyStochCalc.Probability.ProgressivelyMeasurable ℱ (H p k)}
{hHs : ∀ (p : Fin n) (k : Fin d) (T : ℝ), 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
(‖H p k ω s‖₊ : ℝ≥0∞) ^ 2 ∂MeasureTheory.MeasureSpace.volume ∂P < ⊤}
{X₀ : Ω → Fin n → ℝ} {bdrift : Fin n → Ω → ℝ → ℝ} {X : ℝ → Ω → Fin n → ℝ}
{C : ℝ} (hC0 : 0 ≤ C)
(hCH : ∀ (p : Fin n) (k : Fin d) (ω : Ω) (s : ℝ), |H p k ω s| ≤ C)
include hC0 hCH
theorem LevyStochCalc.Brownian.Ito.IsVectorItoVersion.itoFormula_readable
(h : IsVectorItoVersion W ℱ hcoord H hHm hHp hHs X₀ bdrift X)
(hX₀ : ∀ p : Fin n, Measurable fun ω => X₀ ω p)
(hbm : ∀ p, Measurable (Function.uncurry (bdrift p))) {B : ℝ} (hB0 : 0 ≤ B)
(hB : ∀ (p : Fin n) (ω : Ω) (s : ℝ), |bdrift p ω s| ≤ B)
(hma : ∀ (p q : Fin n) (k : Fin d),
Measurable (Function.uncurry fun ω s => H p k ω s + H q k ω s))
(hpa : ∀ (p q : Fin n) (k : Fin d),
Probability.ProgressivelyMeasurable ℱ fun ω s => H p k ω s + H q k ω s)
(hqa : ∀ (p q : Fin n) (k : Fin d) (T' : ℝ), 0 < T' → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T',
(‖H p k ω s + H q k ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
{f : (Fin n → ℝ) → ℝ} {f' : (Fin n → ℝ) → (Fin n → ℝ) →L[ℝ] ℝ}
{f'' : (Fin n → ℝ) → (Fin n → ℝ) →L[ℝ] (Fin n → ℝ) →L[ℝ] ℝ}
(hf : ∀ z, HasFDerivAt f (f' z) z) (hf' : ∀ z, HasFDerivAt f' (f'' z) z)
{K₁ : ℝ} (hf'bd : ∀ z, ‖f' z‖ ≤ K₁)
{K₂ : ℝ} (hK₂0 : 0 ≤ K₂) (hf''bd : ∀ z, ‖f'' z‖ ≤ K₂)
(hf''c : Continuous f'')
(hf''unif : ∀ ε : ℝ, 0 < ε → ∃ δ : ℝ, 0 < δ ∧
∀ z w : Fin n → ℝ, ‖z - w‖ < δ → ‖f'' z - f'' w‖ ≤ ε)
(hmg : ∀ (p : Fin n) (k : Fin d),
Measurable (Function.uncurry fun ω s => coordDeriv f' p (X s ω) * H p k ω s))
(hpg : ∀ (p : Fin n) (k : Fin d), Probability.ProgressivelyMeasurable ℱ
fun ω s => coordDeriv f' p (X s ω) * H p k ω s)
(hqg : ∀ (p : Fin n) (k : Fin d) (T' : ℝ), 0 < T' → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T',
(‖coordDeriv f' p (X s ω) * H p k ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
{T : ℝ} (hT : 0 < T) :
(fun ω : Ω => f (X T ω) - f (X 0 ω)) =ᵐ[P] fun ω : Ω =>
(∑ p : Fin n, ∫ s in Set.Ioc (0 : ℝ) T,
coordDeriv f' p (X s ω) * bdrift p ω s ∂volume)
+ (∑ p : Fin n, ∑ k : Fin d, stochasticIntegralBrownian (W.W k) ℱ (hcoord k)
(fun ω s => coordDeriv f' p (X s ω) * H p k ω s)
(hmg p k) (hpg p k) (hqg p k) T ω)
+ 1 / 2 * ∑ p : Fin n, ∑ q : Fin n, ∫ s in Set.Ioc (0 : ℝ) T,
coordDeriv₂ f'' p q (X s ω) * ∑ k : Fin d, H p k ω s * H q k ω s ∂volume := by sorry
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.