Almost-Sure Vanishing of the Zero Itô Integral

Proved

LevyStochCalc.Brownian.Ito.stochasticIntegralBrownian_ae_zero_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concavevendored-levystochcalc

This statement shows that the Brownian Itô integral of the zero integrand vanishes almost surely. Let $(Ω,P)$ be a probability space, let $W$ be a Brownian motion, and let $ℱ$ be a Brownian filtration. Assume that the zero process is measurable and progressively measurable and that its squared ENNReal energy is finite on every interval $[0,T]$ with $T>0$ .

For every $t∈ℝ$ ,

\texttt{stochasticIntegralBrownian}(0,t)=0\quad P\text{-almost everywhere}.

The conclusion holds for arbitrary real times, including nonpositive times. This is the zero element property needed for the additive and finite-sum algebra of the integral.

Original Lean declaration header

Within namespace LevyStochCalc.Brownian.Ito. Shown in its original module context. Proof omitted.

theorem stochasticIntegralBrownian_ae_zero
    (hm : Measurable (Function.uncurry fun (_ : Ω) (_ : ℝ) => (0 : ℝ)))
    (hp : Probability.ProgressivelyMeasurable ℱ fun (_ : Ω) (_ : ℝ) => (0 : ℝ))
    (hq : ∀ T, 0 < T → ∫⁻ _ω, ∫⁻ _s in Set.Icc (0 : ℝ) T,
      (‖(0 : ℝ)‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤) (t : ℝ) :
    stochasticIntegralBrownian W ℱ hℱ (fun _ _ => (0 : ℝ)) hm hp hq t =ᵐ[P] 0

Module navigation

Module: LevyStochCalc/Brownian/ItoZero.

Definition modules: LevyStochCalc/Brownian/ItoL2CompletionMaster, LevyStochCalc/Brownian/Filtered, LevyStochCalc/Brownian/Construction, LevyStochCalc/Probability/Progressive.

Source excerpt, lines 50–55 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_LevyStochCalc_Brownian_ItoZero

/-
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/ItoZero.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]
  (W : LevyStochCalc.Brownian.BrownianMotion P)
  (ℱ : MeasureTheory.Filtration ℝ ‹MeasurableSpace Ω›) (hℱ : LevyStochCalc.Brownian.IsBrownianFiltration W ℱ)
include hℱ

Formal statement


theorem LevyStochCalc.Brownian.Ito.stochasticIntegralBrownian_ae_zero_readable
    (hm : Measurable (Function.uncurry fun (_ : Ω) (_ : ℝ) => (0 : ℝ)))
    (hp : Probability.ProgressivelyMeasurable ℱ fun (_ : Ω) (_ : ℝ) => (0 : ℝ))
    (hq : ∀ T, 0 < T → ∫⁻ _ω, ∫⁻ _s in Set.Icc (0 : ℝ) T,
      (‖(0 : ℝ)‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤) (t : ℝ) :
    stochasticIntegralBrownian W ℱ hℱ (fun _ _ => (0 : ℝ)) hm hp hq t =ᵐ[P] 0 := by sorry

Source

Lean source: https://github.com/cgarryZA/LevyStochCalc/blob/984dbf0b790031eac05d56fe5a84b65e15e1e932/LevyStochCalc/Brownian/ItoZero.lean#L48-L71 (repository human-ai-mathematics/kls-lean, commit 408915f, module `LevyStochCalc.Brownian.ItoZero`, declaration `LevyStochCalc.Brownian.Ito.stochasticIntegralBrownian_ae_zero`; 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).

View graph