Polarised compensated quadratic increment

Definition

KLSModular_LevyStochCalc_Brownian_PolarisedQuadVar

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 two progressively measurable square-integrable integrands $H_1,H_2$ for the same Brownian motion, polarQuadVarIncrement is the product of their Itô-integral increments across $(a,b]$ minus the Lebesgue integral of $H_1H_2$ over the corresponding interval difference $[0,b]-[0,a]$ .

Original module imports

import LevyStochCalc.Brownian.ItoQuadVarSum
import LevyStochCalc.Brownian.ItoLinear
import LevyStochCalc.Brownian.DriftIncrement

Original declaration excerpt

Shown in the original module context.

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

Module navigation

Direct project imports: LevyStochCalc/Brownian/ItoQuadVarSum, LevyStochCalc/Brownian/ItoLinear, LevyStochCalc/Brownian/DriftIncrement.

Theorems in source order:

Project result: The KLS conjecture.

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

Definition code

import Definitions.Def_KLSModular_LevyStochCalc_Brownian_ItoQuadVarSum
import Definitions.Def_KLSModular_LevyStochCalc_Brownian_ItoLinear
import Definitions.Def_KLSModular_LevyStochCalc_Brownian_DriftIncrement

/-
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/PolarisedQuadVar.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 Polarised
variable {P : Measure Ω} [IsProbabilityMeasure P] (W : LevyStochCalc.Brownian.BrownianMotion P)
  (ℱ : Filtration ℝ ‹MeasurableSpace Ω›) (hℱ : IsBrownianFiltration W ℱ)
  (H₁ H₂ : Ω → ℝ → ℝ)
  (hm₁ : Measurable (Function.uncurry H₁)) (hm₂ : Measurable (Function.uncurry H₂))
  (hp₁ : Probability.ProgressivelyMeasurable ℱ H₁)
  (hp₂ : Probability.ProgressivelyMeasurable ℱ H₂)
  (hq₁ : ∀ T, 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
    (‖H₁ ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
  (hq₂ : ∀ T, 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
    (‖H₂ ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
  (hma : Measurable (Function.uncurry fun ω s => H₁ ω s + H₂ ω s))
  (hpa : Probability.ProgressivelyMeasurable ℱ fun ω s => H₁ ω s + H₂ ω s)
  (hqa : ∀ T, 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
    (‖H₁ ω s + H₂ ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
/-- The product of the increments of the Itô integrals of `H₁` and `H₂` against the same Brownian
motion, compensated by the window integral of `H₁·H₂`. -/
noncomputable def polarQuadVarIncrement (a b : ℝ) (ω : Ω) : ℝ :=
  (stochasticIntegralBrownian W ℱ hℱ H₁ hm₁ hp₁ hq₁ b ω
      - stochasticIntegralBrownian W ℱ hℱ H₁ hm₁ hp₁ hq₁ a ω)
    * (stochasticIntegralBrownian W ℱ hℱ H₂ hm₂ hp₂ hq₂ b ω
      - stochasticIntegralBrownian W ℱ hℱ H₂ hm₂ hp₂ hq₂ a ω)
    - ((∫ u in Set.Icc (0 : ℝ) b, H₁ ω u * H₂ ω u ∂volume)
      - ∫ u in Set.Icc (0 : ℝ) a, H₁ ω u * H₂ ω u ∂volume)
end Polarised
end Ito
end Brownian
end LevyStochCalc

Source

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