Almost-Everywhere Window Convergence of Clamped Versions
ProvedLevyStochCalc.Brownian.Ito.ae_ae_tendsto_version_clamp_readableUnder the stated probability-space, Brownian-motion, measurability, progressive measurability, finite-energy, and Itô-version assumptions, let X be the original version and Xj the version with coefficients clamped at levels j. Let ns : ℕ → ℕ satisfy
for every i. Then, for P-almost every ω and Lebesgue-almost every s in [0,T],
The two a.e. qualifiers are explicit: the outer one is with respect to P and the inner one with respect to restricted Lebesgue measure on the time window. This provides pathwise window convergence along a sufficiently fast subsequence of truncation levels.
Original Lean declaration header
Within namespace LevyStochCalc.Brownian.Ito. Shown in its original module context. Proof omitted.
theorem ae_ae_tendsto_version_clamp
{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 < ⊤)
{X : ℝ → Ω → Fin n → ℝ} {Xj : ℕ → ℝ → Ω → Fin n → ℝ}
(hX : IsVectorItoVersion W ℱ' hcoord H hm hpg hq X₀ b X)
(hXj : ∀ j : ℕ, 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 j))
{T : ℝ} {ns : ℕ → ℕ}
(hns : ∀ i : ℕ, clampMesh P H b T (ns i) < ((2 : ℝ≥0∞)⁻¹) ^ i) :
∀ᵐ ω ∂P, ∀ᵐ s ∂(volume.restrict (Set.Icc (0 : ℝ) T)),
Filter.Tendsto (fun i => Xj (ns i) s ω) Filter.atTop (𝓝 (X s ω))
Module navigation
Module: LevyStochCalc/Ito/ItoFormulaUnboundedClamp.
Definition modules: LevyStochCalc/Brownian/Filtered, LevyStochCalc/Brownian/Multidim, LevyStochCalc/Probability/Progressive, LevyStochCalc/Brownian/VectorItoProcessVersion.
Supporting theorems: lintegral_window_sq_norm_version_clamp_sub_le, tendsto_of_tendsto_sq_enorm.
Previous: exists_seq_ae_tendsto_of_tendsto_lintegral · Next: ae_tendsto_version_clamp_at.
Source excerpt, lines 430–450 · 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.ae_ae_tendsto_version_clamp_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 < ⊤)
{X : ℝ → Ω → Fin n → ℝ} {Xj : ℕ → ℝ → Ω → Fin n → ℝ}
(hX : IsVectorItoVersion W ℱ' hcoord H hm hpg hq X₀ b X)
(hXj : ∀ j : ℕ, 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 j))
{T : ℝ} {ns : ℕ → ℕ}
(hns : ∀ i : ℕ, clampMesh P H b T (ns i) < ((2 : ℝ≥0∞)⁻¹) ^ i) :
∀ᵐ ω ∂P, ∀ᵐ s ∂(volume.restrict (Set.Icc (0 : ℝ) T)),
Filter.Tendsto (fun i => Xj (ns i) s ω) Filter.atTop (𝓝 (X s ω)) := by sorry