Cross increments of two Brownian Itô integrals
DefinitionKLSModular_LevyStochCalc_Brownian_CrossVariationSumVendored from the LevyStochCalc library at https://github.com/cgarryZA/LevyStochCalc, commit 984dbf0b790031eac05d56fe5a84b65e15e1e932. Under the stated probability, Brownian-filtration, measurability, progressive-measurability, and finite-energy assumptions for and , crossIncrement W ℱ hcoord H K i j a b ω is the product of the increment of the Itô integral of against coordinate and the increment of the Itô integral of against coordinate across .
Original module imports
import LevyStochCalc.Brownian.CrossVariation
import LevyStochCalc.Brownian.ItoIncrementMoment
import LevyStochCalc.Probability.MartingaleDifference
Original declaration excerpt
Shown in the original module context.
noncomputable def crossIncrement (i j : Fin d) (a b : ℝ) (ω : Ω) : ℝ :=
(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 ω)
Module navigation
Direct project imports: LevyStochCalc/Brownian/CrossVariation, LevyStochCalc/Brownian/ItoIncrementMoment, LevyStochCalc/Probability/MartingaleDifference.
Theorems in source order:
Project result: The KLS conjecture.
Original module · LevyStochCalc.Brownian.CrossVariationSum · Frozen source 408915f.
import Definitions.Def_KLSModular_LevyStochCalc_Brownian_CrossVariation
import Definitions.Def_KLSModular_LevyStochCalc_Brownian_ItoIncrementMoment
import Definitions.Def_KLSModular_LevyStochCalc_Probability_MartingaleDifference
/-
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/CrossVariationSum.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
namespace LevyStochCalc
namespace Brownian
namespace Ito
open MeasureTheory ProbabilityTheory
open scoped NNReal ENNReal
universe u
variable {Ω : Type u} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
{ℱ : Filtration ℝ ‹MeasurableSpace Ω›}
section CrossSum
open LevyStochCalc.Brownian.Multidim
variable {d : ℕ} (W : Multidim.MultidimBrownianMotion P d)
(hcoord : ∀ k : Fin d, IsBrownianFiltration (W.W k) ℱ)
{H K : Ω → ℝ → ℝ} (hHm : Measurable (Function.uncurry H))
(hHp : Probability.ProgressivelyMeasurable ℱ H)
(hHs : ∀ T, 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
(‖H ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
(hKm : Measurable (Function.uncurry K))
(hKp : Probability.ProgressivelyMeasurable ℱ K)
(hKs : ∀ T, 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
(‖K ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
/-- The product of the increments of the Itô integrals against the coordinates `i` and `j`
across `(a, b]`. -/
noncomputable def crossIncrement (i j : Fin d) (a b : ℝ) (ω : Ω) : ℝ :=
(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 ω)
variable {CH CK : ℝ} (hCH0 : 0 ≤ CH) (hCH : ∀ ω s, |H ω s| ≤ CH)
(hCK0 : 0 ≤ CK) (hCK : ∀ ω s, |K ω s| ≤ CK)
end CrossSum
end Ito
end Brownian
end LevyStochCalc