L² Distance Between Vector Itô Processes
ProvedLevyStochCalc.Brownian.Ito.lintegral_sq_norm_vectorItoProcess_sub_le_readablefunctional-inequalitieskls-conjecturekls-modularkls-readablelog-concavevendored-levystochcalc
Let (Ω, P) be a probability space with a d-dimensional Brownian motion W and filtration ℱ. Consider two vector Itô processes driven by the same measurable, progressively measurable diffusion framework H₁ and H₂ and the same measurable initial value X₀, but with drifts b₁ and b₂. Assume all four coefficient families satisfy the stated finite ENNReal square-energy conditions, and assume t > 0. Then
Here the left-hand integral is the ENNReal integral of the squared extended norm, and the displayed notation ∫^∞ denotes the corresponding lintegral. This estimate separates drift and diffusion errors and is used for stability of vector Itô processes.
Original Lean declaration header
Within namespace LevyStochCalc.Brownian.Ito. Shown in its original module context. Proof omitted.
theorem lintegral_sq_norm_vectorItoProcess_sub_le
{H₁ H₂ : Fin n → Fin d → Ω → ℝ → ℝ}
(hm₁ : ∀ p k, Measurable (Function.uncurry (H₁ p k)))
(hp₁ : ∀ p k, Probability.ProgressivelyMeasurable ℱ (H₁ p k))
(hq₁ : ∀ (p : Fin n) (k : Fin d) (T : ℝ), 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
(‖H₁ p k ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
(hm₂ : ∀ p k, Measurable (Function.uncurry (H₂ p k)))
(hp₂ : ∀ p k, Probability.ProgressivelyMeasurable ℱ (H₂ p k))
(hq₂ : ∀ (p : Fin n) (k : Fin d) (T : ℝ), 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
(‖H₂ p k ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
{X₀ : Ω → Fin n → ℝ} (hX₀ : ∀ p : Fin n, Measurable fun ω => X₀ ω p)
{b₁ b₂ : Fin n → Ω → ℝ → ℝ}
(hbm₁ : ∀ p, Measurable (Function.uncurry (b₁ p)))
(hbm₂ : ∀ p, Measurable (Function.uncurry (b₂ p)))
{t : ℝ} (ht : 0 < t)
(hbq₁ : ∀ (p : Fin n) (T : ℝ), 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
(‖b₁ p ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
(hbq₂ : ∀ (p : Fin n) (T : ℝ), 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
(‖b₂ p ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤) :
∫⁻ ω, (‖vectorItoProcess W ℱ hcoord H₂ hm₂ hp₂ hq₂ X₀ b₂ t ω
- vectorItoProcess W ℱ hcoord H₁ hm₁ hp₁ hq₁ X₀ b₁ t ω‖₊ : ℝ≥0∞) ^ 2 ∂P
≤ ∑ p : Fin n, (2 * (ENNReal.ofReal t * ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) t,
(‖b₂ p ω s - b₁ p ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P)
+ 2 * ((d : ℝ≥0∞) * ∑ k : Fin d, ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) t,
(‖H₂ p k ω s - H₁ p k ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P))
Module navigation
Module: LevyStochCalc/Ito/VectorItoProcessDiff.
Definition modules: LevyStochCalc/Brownian/Filtered, LevyStochCalc/Brownian/Multidim, LevyStochCalc/Probability/Progressive, LevyStochCalc/Brownian/VectorItoProcess.
Supporting theorems: lintegral_energy_lt_top_of_bound, sq_enorm_finsetSum_le.
Source excerpt, lines 54–78 · Frozen source 408915f.
Preamble
import Definitions.Def_KLSModular_LevyStochCalc_Ito_VectorItoProcessDiff
/-
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/Ito/VectorItoProcessDiff.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
open MeasureTheory ProbabilityTheory LevyStochCalc.Brownian.Multidim
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) ℱ)
Formal statement
theorem LevyStochCalc.Brownian.Ito.lintegral_sq_norm_vectorItoProcess_sub_le_readable
{H₁ H₂ : Fin n → Fin d → Ω → ℝ → ℝ}
(hm₁ : ∀ p k, Measurable (Function.uncurry (H₁ p k)))
(hp₁ : ∀ p k, Probability.ProgressivelyMeasurable ℱ (H₁ p k))
(hq₁ : ∀ (p : Fin n) (k : Fin d) (T : ℝ), 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
(‖H₁ p k ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
(hm₂ : ∀ p k, Measurable (Function.uncurry (H₂ p k)))
(hp₂ : ∀ p k, Probability.ProgressivelyMeasurable ℱ (H₂ p k))
(hq₂ : ∀ (p : Fin n) (k : Fin d) (T : ℝ), 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
(‖H₂ p k ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
{X₀ : Ω → Fin n → ℝ} (hX₀ : ∀ p : Fin n, Measurable fun ω => X₀ ω p)
{b₁ b₂ : Fin n → Ω → ℝ → ℝ}
(hbm₁ : ∀ p, Measurable (Function.uncurry (b₁ p)))
(hbm₂ : ∀ p, Measurable (Function.uncurry (b₂ p)))
{t : ℝ} (ht : 0 < t)
(hbq₁ : ∀ (p : Fin n) (T : ℝ), 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
(‖b₁ p ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
(hbq₂ : ∀ (p : Fin n) (T : ℝ), 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
(‖b₂ p ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤) :
∫⁻ ω, (‖vectorItoProcess W ℱ hcoord H₂ hm₂ hp₂ hq₂ X₀ b₂ t ω
- vectorItoProcess W ℱ hcoord H₁ hm₁ hp₁ hq₁ X₀ b₁ t ω‖₊ : ℝ≥0∞) ^ 2 ∂P
≤ ∑ p : Fin n, (2 * (ENNReal.ofReal t * ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) t,
(‖b₂ p ω s - b₁ p ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P)
+ 2 * ((d : ℝ≥0∞) * ∑ k : Fin d, ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) t,
(‖H₂ p k ω s - H₁ p k ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P)) := by sorry
Source
Lean source: https://github.com/cgarryZA/LevyStochCalc/blob/984dbf0b790031eac05d56fe5a84b65e15e1e932/LevyStochCalc/Ito/VectorItoProcessDiff.lean#L53-L190 (repository human-ai-mathematics/kls-lean, commit 408915f, module `LevyStochCalc.Ito.VectorItoProcessDiff`, declaration `LevyStochCalc.Brownian.Ito.lintegral_sq_norm_vectorItoProcess_sub_le`; 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).