L² Error Between Itô Versions Under Clamping
ProvedLevyStochCalc.Brownian.Ito.lintegral_sq_norm_version_clamp_sub_le_readableLet X be an IsVectorItoVersion for coefficients H and b, and let Xj be an IsVectorItoVersion for the clamped coefficients clampCoeff H j and clampDrift b j. Under the stated measurability and finite ENNReal energy assumptions, for 0 < s ≤ T,
The theorem lintegral_sq_norm_version_clamp_sub_le_readable transfers the process-level estimate to arbitrary versions, using their almost-everywhere agreement with the canonical vectorItoProcess.
Original Lean declaration header
Within namespace LevyStochCalc.Brownian.Ito. Shown in its original module context. Proof omitted.
theorem lintegral_sq_norm_version_clamp_sub_le
{H : Fin n → Fin d → Ω → ℝ → ℝ}
{hm : ∀ p k, Measurable (Function.uncurry (H p k))}
{hpg : ∀ 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 : Fin n → Ω → ℝ → ℝ} (hbm : ∀ p, Measurable (Function.uncurry (b p)))
(hbq : ∀ (p : Fin n) (T' : ℝ), 0 < T' → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T',
(‖b p ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
{j : ℕ} {X Xj : ℝ → Ω → Fin n → ℝ}
(hX : IsVectorItoVersion W ℱ' hcoord H hm hpg hq X₀ b X)
(hXj : IsVectorItoVersion W ℱ' hcoord (clampCoeff H j)
(fun p k => measurable_clampCoeff hm j p k)
(fun p k => progressivelyMeasurable_clampCoeff hpg j p k)
(fun p k T' hT' => energy_clampCoeff_lt_top j p k T' hT')
X₀ (clampDrift b j) Xj)
{T s : ℝ} (hs : 0 < s) (hsT : s ≤ T) :
∫⁻ ω, (‖Xj s ω - X s ω‖₊ : ℝ≥0∞) ^ 2 ∂P ≤ clampMesh P H b T j
Module navigation
Module: LevyStochCalc/Ito/ItoFormulaUnboundedClamp.
Definition modules: LevyStochCalc/Brownian/Filtered, LevyStochCalc/Brownian/Multidim, LevyStochCalc/Probability/Progressive, LevyStochCalc/Brownian/VectorItoProcessVersion.
Supporting theorems: lintegral_sq_norm_clampProcess_sub_le.
Previous: lintegral_sq_norm_clampProcess_sub_le · Next: lintegral_window_sq_norm_version_clamp_sub_le.
Source excerpt, lines 250–268 · Frozen source 408915f.
import Definitions.Def_KLSModular_LevyStochCalc_Ito_ItoFormulaUnboundedClamp
/-
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/ItoFormulaUnboundedClamp.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 : ℕ} {ℱ : MeasureTheory.Filtration ℝ ‹MeasurableSpace Ω›}
variable (W : LevyStochCalc.Brownian.Multidim.MultidimBrownianMotion P d)
(ℱ' : MeasureTheory.Filtration ℝ ‹MeasurableSpace Ω›)
(hcoord : ∀ k : Fin d, LevyStochCalc.Brownian.IsBrownianFiltration (W.W k) ℱ')
theorem LevyStochCalc.Brownian.Ito.lintegral_sq_norm_version_clamp_sub_le_readable
{H : Fin n → Fin d → Ω → ℝ → ℝ}
{hm : ∀ p k, Measurable (Function.uncurry (H p k))}
{hpg : ∀ 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 : Fin n → Ω → ℝ → ℝ} (hbm : ∀ p, Measurable (Function.uncurry (b p)))
(hbq : ∀ (p : Fin n) (T' : ℝ), 0 < T' → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T',
(‖b p ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
{j : ℕ} {X Xj : ℝ → Ω → Fin n → ℝ}
(hX : IsVectorItoVersion W ℱ' hcoord H hm hpg hq X₀ b X)
(hXj : IsVectorItoVersion W ℱ' hcoord (clampCoeff H j)
(fun p k => measurable_clampCoeff hm j p k)
(fun p k => progressivelyMeasurable_clampCoeff hpg j p k)
(fun p k T' hT' => energy_clampCoeff_lt_top j p k T' hT')
X₀ (clampDrift b j) Xj)
{T s : ℝ} (hs : 0 < s) (hsT : s ≤ T) :
∫⁻ ω, (‖Xj s ω - X s ω‖₊ : ℝ≥0∞) ^ 2 ∂P ≤ clampMesh P H b T j := by sorry