ENNReal Window Bound for Vector-Process Increments
ProvedLevyStochCalc.Brownian.Ito.IsVectorItoVersion.lintegral_window_norm_sub_le_readableThis is the window estimate for a version of a vector Itô process.
Let be a probability measure and let be a version of the vector Itô process driven by a -dimensional Brownian motion, with state coordinates. Assume the diffusion integrands are measurable, progressively measurable, square-integrable on every positive interval, and bounded by ; assume the drift coordinates are measurable and bounded in absolute value by . For , the joint integral over the time window satisfies
\int^\!*_{\Omega}\int^\!*_{(u,v]} \operatorname{ofReal}\!\left(\|X_s-X_u\|\right)\,ds\,dP \le \operatorname{ofReal}\!\left((v-u)n\left(B(v-u)+dC\sqrt{v-u}\right)\right).Here IsVectorItoVersion supplies the version properties required by the estimate. The result is suited to time-window integrations in Riemann-sum arguments.
Formalization Note The displayed integrals are lower integrals, and ENNReal.ofReal is applied to the real-valued norm and to the final real bound.
Original Lean declaration header
Within namespace LevyStochCalc.Brownian.Ito. Shown in its original module context. Proof omitted.
theorem IsVectorItoVersion.lintegral_window_norm_sub_le
(h : IsVectorItoVersion W ℱ hcoord H hHm hHp hHs X₀ bdrift X)
(hbm : ∀ m, Measurable (Function.uncurry (bdrift m))) {B : ℝ} (hB0 : 0 ≤ B)
(hB : ∀ (m : Fin n) (ω : Ω) (s : ℝ), |bdrift m ω s| ≤ B) {u v : ℝ} (hu : 0 ≤ u)
(huv : u ≤ v) :
∫⁻ ω, ∫⁻ s in Set.Ioc u v, ENNReal.ofReal ‖X s ω - X u ω‖ ∂volume ∂P
≤ ENNReal.ofReal ((v - u)
* ((n : ℝ) * (B * (v - u) + (d : ℝ) * (C * Real.sqrt (v - u)))))
Module navigation
Module: LevyStochCalc/Brownian/VectorItoProcessWindow.
Definition modules: LevyStochCalc/Brownian/Filtered, LevyStochCalc/Brownian/Multidim, LevyStochCalc/Probability/Progressive, LevyStochCalc/Brownian/VectorItoProcessVersion.
Supporting theorems: integral_norm_vectorItoProcess_sub_le.
Next: IsVectorItoVersion.lintegral_window_sq_norm_sub_le.
Source excerpt, lines 49–56 · Frozen source 408915f.
import Definitions.Def_KLSModular_LevyStochCalc_Brownian_VectorItoProcessWindow
/-
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/VectorItoProcessWindow.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 < ⊤}
{X₀ : Ω → Fin n → ℝ} {bdrift : Fin n → Ω → ℝ → ℝ} {X : ℝ → Ω → Fin n → ℝ}
{C : ℝ} (hC0 : 0 ≤ C)
(hCH : ∀ (m : Fin n) (k : Fin d) (ω : Ω) (s : ℝ), |H m k ω s| ≤ C)
include hC0 hCH
theorem LevyStochCalc.Brownian.Ito.IsVectorItoVersion.lintegral_window_norm_sub_le_readable
(h : IsVectorItoVersion W ℱ hcoord H hHm hHp hHs X₀ bdrift X)
(hbm : ∀ m, Measurable (Function.uncurry (bdrift m))) {B : ℝ} (hB0 : 0 ≤ B)
(hB : ∀ (m : Fin n) (ω : Ω) (s : ℝ), |bdrift m ω s| ≤ B) {u v : ℝ} (hu : 0 ≤ u)
(huv : u ≤ v) :
∫⁻ ω, ∫⁻ s in Set.Ioc u v, ENNReal.ofReal ‖X s ω - X u ω‖ ∂volume ∂P
≤ ENNReal.ofReal ((v - u)
* ((n : ℝ) * (B * (v - u) + (d : ℝ) * (C * Real.sqrt (v - u))))) := by sorry