Multidimensional Brownian Itô integral

Definition

KLSModular_LevyStochCalc_Brownian_MultidimIto

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-contextvendored-levystochcalc

Vendored from the LevyStochCalc library (https://github.com/cgarryZA/LevyStochCalc), commit 984dbf0b790031eac05d56fe5a84b65e15e1e932. For a $d$ -dimensional Brownian motion $W$ on a probability space, a filtration $\mathcal F$ for which every coordinate is Brownian, and a vector-valued integrand $Z:\mathbb R\to\Omega\to(\mathrm{Fin}\,d\to\mathbb R)$ , MultidimBrownianMotion.stochasticIntegral is defined by

\sum_{i\in\mathrm{Fin}\,d}\int_0^T Z_s^i\,dW_s^i.

Each component is required to be jointly measurable, progressively measurable, and square-integrable on every positive finite horizon. The definition is a finite sum of the one-dimensional stochasticIntegral constructions.

Original module imports

import LevyStochCalc.Brownian.MultidimFiltered
import LevyStochCalc.Brownian.ItoL2Completion

Original declaration excerpt

Shown in the original module context. Body omitted.

noncomputable def stochasticIntegral
    (W : MultidimBrownianMotion P d)
    (ℱ : Filtration ℝ ‹MeasurableSpace Ω›) (hℱ : ∀ i, IsBrownianFiltration (W.W i) ℱ)
    (Z : ℝ → Ω → (Fin d → ℝ))
    (h_meas : ∀ i : Fin d, Measurable (Function.uncurry (fun ω s => Z s ω i)))
    (h_progMeas : ∀ i : Fin d, Probability.ProgressivelyMeasurable ℱ (fun ω s => Z s ω i))
    (h_sq_int_global : ∀ i : Fin d, ∀ T : ℝ, 0 < T →
      ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
        (‖Z s ω i‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
    (T : ℝ) : Ω → ℝ

Module navigation

Direct project imports: LevyStochCalc/Brownian/MultidimFiltered, LevyStochCalc/Brownian/ItoL2Completion.

Project result: The KLS conjecture.

Original module · LevyStochCalc.Brownian.MultidimIto · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_LevyStochCalc_Brownian_MultidimFiltered
import Definitions.Def_KLSModular_LevyStochCalc_Brownian_ItoL2Completion

/-
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/MultidimIto.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
open MeasureTheory ProbabilityTheory
open scoped NNReal ENNReal
namespace LevyStochCalc
namespace Brownian
namespace Multidim
namespace MultidimBrownianMotion
universe u
variable {Ω : Type u} [MeasurableSpace Ω]
variable {P : Measure Ω} [IsProbabilityMeasure P]
variable {d : ℕ}
/-- The multidim Brownian Itô integral
`(∫_0^T Z_s · dW_s)(ω) = ∑_i ∫_0^T Z_s^i dW_s^i (ω)`.

`Z s ω i` is the `i`-th component of the integrand at `(s, ω)`. The result
at time `T` is the sum (over components) of the 1D Itô integrals against
the component Brownian motions `W.W i`.

Each component's 1D integral is `LevyStochCalc.Brownian.Ito.stochasticIntegral`
(`Brownian/ItoL2Completion.lean`), the coherent `L²`-limit of simple integrals
whose martingale, quadratic-variation and isometry properties are packaged in
`itoIsometry_brownian_unified_existence`. -/
noncomputable def stochasticIntegral
    (W : MultidimBrownianMotion P d)
    (ℱ : Filtration ℝ ‹MeasurableSpace Ω›) (hℱ : ∀ i, IsBrownianFiltration (W.W i) ℱ)
    (Z : ℝ → Ω → (Fin d → ℝ))
    (h_meas : ∀ i : Fin d, Measurable (Function.uncurry (fun ω s => Z s ω i)))
    (h_progMeas : ∀ i : Fin d, Probability.ProgressivelyMeasurable ℱ (fun ω s => Z s ω i))
    (h_sq_int_global : ∀ i : Fin d, ∀ T : ℝ, 0 < T →
      ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
        (‖Z s ω i‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
    (T : ℝ) : Ω → ℝ :=
  fun ω => ∑ i : Fin d,
    LevyStochCalc.Brownian.Ito.stochasticIntegral
      (W.W i) ℱ (hℱ i) (fun ω' s => Z s ω' i)
      (h_meas i) (h_progMeas i) (h_sq_int_global i) T ω
end MultidimBrownianMotion
end Multidim
end Brownian
end LevyStochCalc

Source

Lean source: https://github.com/cgarryZA/LevyStochCalc/blob/984dbf0b790031eac05d56fe5a84b65e15e1e932/LevyStochCalc/Brownian/MultidimIto.lean#L50-L74 (repository human-ai-mathematics/kls-lean, commit 408915f, module `LevyStochCalc.Brownian.MultidimIto`, definition bundle `KLSModular_LevyStochCalc_Brownian_MultidimIto`; 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