Integrability of Bounded-Coefficient Brownian Cross Terms

Proved

LevyStochCalc.Brownian.Multidim.MultidimBrownianMotion.integrable_cross_term_readable

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

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

This is an integrability estimate for a product of two Brownian increments with bounded coefficients.

Let $P$ be a probability measure, let $V_1,V_2$ be Brownian motions, and let $0\le p\le q$ and $0\le r\le v$ . Let $\xi,\eta:\Omega\to\mathbb R$ be measurable and assume $|\xi(\omega)|\le M_\xi$ and $|\eta(\omega)|\le M_\eta$ . Then

\omega\mapsto \bigl(\xi(\omega)(V_1(q,\omega)-V_1(p,\omega))\bigr) \bigl(\eta(\omega)(V_2(v,\omega)-V_2(r,\omega))\bigr)

is integrable.

The result is a technical domination lemma for cross terms; it asserts integrability but no vanishing or orthogonality conclusion.

Original Lean declaration header

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

lemma integrable_cross_term (V₁ V₂ : BrownianMotion P) {p q r v : ℝ} (hp : 0 ≤ p) (hpq : p ≤ q)
    (hr : 0 ≤ r) (hrv : r ≤ v) {ξ η : Ω → ℝ} (hξm : Measurable ξ) (hηm : Measurable η)
    {Mξ Mη : ℝ} (hξb : ∀ ω, |ξ ω| ≤ Mξ) (hηb : ∀ ω, |η ω| ≤ Mη) :
    Integrable (fun ω => (ξ ω * (V₁.W q ω - V₁.W p ω))
      * (η ω * (V₂.W v ω - V₂.W r ω))) P

Module navigation

Module: LevyStochCalc/Brownian/CrossOrthogonalityLimit.

Definition modules: LevyStochCalc/Brownian/Construction.

Next: integral_cross_increment_eq_zero_of_le.

Source excerpt, lines 55–59 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_LevyStochCalc_Brownian_CrossOrthogonalityLimit

/-
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/CrossOrthogonalityLimit.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
open MeasureTheory ProbabilityTheory
universe u
variable {Ω : Type u} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {d : ℕ}

Formal statement


lemma LevyStochCalc.Brownian.Multidim.MultidimBrownianMotion.integrable_cross_term_readable (V₁ V₂ : BrownianMotion P) {p q r v : ℝ} (hp : 0 ≤ p) (hpq : p ≤ q)
    (hr : 0 ≤ r) (hrv : r ≤ v) {ξ η : Ω → ℝ} (hξm : Measurable ξ) (hηm : Measurable η)
    {Mξ Mη : ℝ} (hξb : ∀ ω, |ξ ω| ≤ Mξ) (hηb : ∀ ω, |η ω| ≤ Mη) :
    Integrable (fun ω => (ξ ω * (V₁.W q ω - V₁.W p ω))
      * (η ω * (V₂.W v ω - V₂.W r ω))) P := by sorry

Source

Lean source: https://github.com/cgarryZA/LevyStochCalc/blob/984dbf0b790031eac05d56fe5a84b65e15e1e932/LevyStochCalc/Brownian/CrossOrthogonalityLimit.lean#L54-L82 (repository human-ai-mathematics/kls-lean, commit 408915f, module `LevyStochCalc.Brownian.CrossOrthogonalityLimit`, declaration `LevyStochCalc.Brownian.Multidim.MultidimBrownianMotion.integrable_cross_term`; 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