Weighted Cross-Variation Orthogonality for Itô Increments

Proved

LevyStochCalc.Brownian.Ito.integral_mul_cross_increment_eq_zero_readable

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

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

This is the cross-variation orthogonality identity for two Itô integrals driven by distinct Brownian coordinates.

Let $W$ be a multidimensional Brownian motion with distinct coordinates $i\ne j$ , and let $\mathcal F$ be a common Brownian filtration. Let $H$ and $K$ be measurable, progressively measurable integrands with finite integrated squared norms on every positive interval. Assume $0\le a<b$ . If $Z$ is measurable, strongly $\mathcal F_a$ -measurable, and bounded in absolute value, then

\int Z(\omega)\bigl(I^i_b-I^i_a\bigr)(\omega) \bigl(I^j_b-I^j_a\bigr)(\omega)\,dP=0,

where $I^i$ and $I^j$ are the corresponding stochasticIntegralBrownian processes.

This result states that the product of the two cross-coordinate Itô increments is orthogonal to every bounded coefficient known at the left endpoint of the interval.

Original Lean declaration header

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

theorem integral_mul_cross_increment_eq_zero {i j : Fin d} (hij : i ≠ j) {a b : ℝ} (ha : 0 ≤ a)
    (hab : a < b) {Z : Ω → ℝ} (hZm : Measurable Z) {M : ℝ} (hZb : ∀ ω, |Z ω| ≤ M)
    (hZa : StronglyMeasurable[ℱ a] Z) :
    ∫ ω, Z ω * ((stochasticIntegralBrownian (W.W i) ℱ (hcoord i) H hHm hHp hHs b ω
          - stochasticIntegralBrownian (W.W i) ℱ (hcoord i) H hHm hHp hHs a ω)
        * (stochasticIntegralBrownian (W.W j) ℱ (hcoord j) K hKm hKp hKs b ω
          - stochasticIntegralBrownian (W.W j) ℱ (hcoord j) K hKm hKp hKs a ω)) ∂P = 0

Module navigation

Module: LevyStochCalc/Brownian/CrossVariation.

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

Supporting theorems: stochasticIntegralBrownian_integralAgainst, integral_stochasticIntegral_mul_eq_zero.

Next: condExp_mul_cross_increment_eq_zero.

Source excerpt, lines 242–248 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_LevyStochCalc_Brownian_CrossVariation

/-
Copyright (c) 2026 Christian Garry. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Christian Garry
-/
-- Modified 2026-10-12 by the KLS formalization project: ported to Lean v4.33.0 and
-- Mathlib db584cd. The changes are listed in vendor/README.md and vendor/port.patch.
-- Vendored from https://github.com/cgarryZA/LevyStochCalc at commit 984dbf0b790031eac05d56fe5a84b65e15e1e932 (upstream path LevyStochCalc/Brownian/CrossVariation.lean; Apache-2.0; locally patched, see formalization/vendor/port.patch; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
open MeasureTheory ProbabilityTheory Filter
open scoped ENNReal NNReal
universe u
variable {Ω : Type u} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P]
  {ℱ : MeasureTheory.Filtration ℝ ‹MeasurableSpace Ω›}
variable {d : ℕ} (W : LevyStochCalc.Brownian.Multidim.MultidimBrownianMotion P d)
  (hcoord : ∀ k : Fin d, LevyStochCalc.Brownian.IsBrownianFiltration (W.W k) ℱ)
  {H K : Ω → ℝ → ℝ} (hHm : Measurable (Function.uncurry H))
  (hHp : LevyStochCalc.Probability.ProgressivelyMeasurable ℱ H)
  (hHs : ∀ T, 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
    (‖H ω s‖₊ : ℝ≥0∞) ^ 2 ∂MeasureTheory.MeasureSpace.volume ∂P < ⊤)
  (hKm : Measurable (Function.uncurry K))
  (hKp : LevyStochCalc.Probability.ProgressivelyMeasurable ℱ K)
  (hKs : ∀ T, 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
    (‖K ω s‖₊ : ℝ≥0∞) ^ 2 ∂MeasureTheory.MeasureSpace.volume ∂P < ⊤)

Formal statement


theorem LevyStochCalc.Brownian.Ito.integral_mul_cross_increment_eq_zero_readable {i j : Fin d} (hij : i ≠ j) {a b : ℝ} (ha : 0 ≤ a)
    (hab : a < b) {Z : Ω → ℝ} (hZm : Measurable Z) {M : ℝ} (hZb : ∀ ω, |Z ω| ≤ M)
    (hZa : StronglyMeasurable[ℱ a] Z) :
    ∫ ω, Z ω * ((stochasticIntegralBrownian (W.W i) ℱ (hcoord i) H hHm hHp hHs b ω
          - stochasticIntegralBrownian (W.W i) ℱ (hcoord i) H hHm hHp hHs a ω)
        * (stochasticIntegralBrownian (W.W j) ℱ (hcoord j) K hKm hKp hKs b ω
          - stochasticIntegralBrownian (W.W j) ℱ (hcoord j) K hKm hKp hKs a ω)) ∂P = 0 := by sorry

Source

Lean source: https://github.com/cgarryZA/LevyStochCalc/blob/984dbf0b790031eac05d56fe5a84b65e15e1e932/LevyStochCalc/Brownian/CrossVariation.lean (repository human-ai-mathematics/kls-lean, commit 408915f, module `LevyStochCalc.Brownian.CrossVariation`, declaration `LevyStochCalc.Brownian.Ito.integral_mul_cross_increment_eq_zero`; the repository is private at upload time); vendored copy patched by formalization/vendor/port.patch (project file formalization/vendor/LevyStochCalc/LevyStochCalc/Brownian/CrossVariation.lean, lines 239-264). Vendored from https://github.com/cgarryZA/LevyStochCalc at commit 984dbf0b790031eac05d56fe5a84b65e15e1e932 (Apache-2.0; upstream copyright notice retained in the Lean text).

View graph