Compensated square increments of a Brownian Itô integral

Definition

KLSModular_LevyStochCalc_Brownian_ItoQuadVarSum

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

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

Vendored from the LevyStochCalc library at https://github.com/cgarryZA/LevyStochCalc, commit 984dbf0b790031eac05d56fe5a84b65e15e1e932. Given a Brownian motion $W$ under a probability measure $P$ , a filtration satisfying IsBrownianFiltration, and a progressively measurable integrand $H$ with finite $L^2$ energy on every positive window, quadVarIncrement W ℱ hℱ H ... a b ω is $(M_b-M_a)^2-\int_{[0,b]}H_s^2\,ds+\int_{[0,a]}H_s^2\,ds$ , where $M_t$ is the Brownian Itô integral of $H$ .

Original module imports

import LevyStochCalc.Brownian.ItoIncrementMoment
import LevyStochCalc.Probability.MartingaleDifference

Original declaration excerpt

Shown in the original module context.

noncomputable def quadVarIncrement (a b : ℝ) (ω : Ω) : ℝ :=
  (stochasticIntegralBrownian W ℱ hℱ H hm hp hq b ω
      - stochasticIntegralBrownian W ℱ hℱ H hm hp hq a ω) ^ 2
    - ((∫ u in Set.Icc (0 : ℝ) b, (H ω u) ^ 2 ∂volume)
        - ∫ u in Set.Icc (0 : ℝ) a, (H ω u) ^ 2 ∂volume)

Module navigation

Direct project imports: LevyStochCalc/Brownian/ItoIncrementMoment, LevyStochCalc/Probability/MartingaleDifference.

Theorems in source order:

Project result: The KLS conjecture.

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

Definition code

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/ItoQuadVarSum.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 Ω]
section QuadVarIncrement
variable {P : Measure Ω} [IsProbabilityMeasure P] (W : LevyStochCalc.Brownian.BrownianMotion P)
  (ℱ : Filtration ℝ ‹MeasurableSpace Ω›) (hℱ : IsBrownianFiltration W ℱ)
  (H : Ω → ℝ → ℝ) (hm : Measurable (Function.uncurry H))
  (hp : Probability.ProgressivelyMeasurable ℱ H)
  (hq : ∀ T, 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
    (‖H ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
/-- The compensated square increment `(M_b − M_a)² − ∫_a^b H_s² ds` of the Itô integral. -/
noncomputable def quadVarIncrement (a b : ℝ) (ω : Ω) : ℝ :=
  (stochasticIntegralBrownian W ℱ hℱ H hm hp hq b ω
      - stochasticIntegralBrownian W ℱ hℱ H hm hp hq a ω) ^ 2
    - ((∫ u in Set.Icc (0 : ℝ) b, (H ω u) ^ 2 ∂volume)
        - ∫ u in Set.Icc (0 : ℝ) a, (H ω u) ^ 2 ∂volume)
end QuadVarIncrement
end Ito
end Brownian
end LevyStochCalc

Source

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