Itô Integral Equals Elementary Integral for Simple Integrands

Proved

LevyStochCalc.Brownian.Ito.stochasticIntegralBrownian_eval_simple_readable

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

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

Let $W$ be a Brownian motion with Brownian filtration, let $G$ be a simple predictable integrand, and assume all coefficients of $G$ are strongly measurable at their preceding partition times. Suppose the evaluation of $G$ is jointly measurable, progressively measurable, and has finite squared ENNReal energy on every positive time interval. Then, for every $t≥0$ ,

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

The conclusion is equality of random variables modulo $P$ -null sets. This identifies the abstract L² Itô integral with the elementary finite-sum construction on simple predictable inputs.

Original Lean declaration header

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

theorem stochasticIntegralBrownian_eval_simple {t : ℝ} (ht : 0 ≤ t) :
    stochasticIntegralBrownian W ℱ hℱ (fun ω s => G.eval s ω) hm hp hq t
      =ᵐ[P] simpleIntegral W G t

Module navigation

Module: LevyStochCalc/Brownian/ItoAlgebraSimpleIntegrand.

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

Supporting theorems: simpleIntegral_diff_isometry_of_adapted.

Previous: simpleIntegral_diff_isometry_of_adapted.

Source excerpt, lines 238–240 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_LevyStochCalc_Brownian_ItoAlgebraSimpleIntegrand

/-
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/ItoAlgebraSimpleIntegrand.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
open scoped NNReal ENNReal
universe u
variable {Ω : Type u} [MeasurableSpace Ω]
variable {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] (W : LevyStochCalc.Brownian.BrownianMotion P)
  (ℱ : MeasureTheory.Filtration ℝ ‹MeasurableSpace Ω›) (hℱ : LevyStochCalc.Brownian.IsBrownianFiltration W ℱ)
  {T₀ : ℝ} (G : LevyStochCalc.Brownian.Ito.SimplePredictable Ω T₀)
  (h_adapt : ∀ i : Fin G.N, @MeasureTheory.StronglyMeasurable Ω ℝ _
    (ℱ (G.partition i.castSucc)) (G.ξ i))
  (hm : Measurable (Function.uncurry fun ω s => G.eval s ω))
  (hp : LevyStochCalc.Probability.ProgressivelyMeasurable ℱ fun ω s => G.eval s ω)
  (hq : ∀ T, 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
    (‖G.eval s ω‖₊ : ℝ≥0∞) ^ 2 ∂MeasureTheory.MeasureSpace.volume ∂P < ⊤)
include hℱ h_adapt

Formal statement


theorem LevyStochCalc.Brownian.Ito.stochasticIntegralBrownian_eval_simple_readable {t : ℝ} (ht : 0 ≤ t) :
    stochasticIntegralBrownian W ℱ hℱ (fun ω s => G.eval s ω) hm hp hq t
      =ᵐ[P] simpleIntegral W G t := by sorry

Source

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