Finite Dyadic $S^2$ Bound for the Diffusion Component

Proved

LevyStochCalc.Ito.Picard.lintegral_sq_iSup_diffusion_lt_top_readable

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

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

This proves finiteness of the dyadic supremum second moment of one Brownian diffusion coordinate in the Picard step.

Let $W$ be a $d$ -dimensional Brownian motion with filtration $\mathcal F$ , let $X$ be a state process, and fix $i<n$ . Assume each diffusion coefficient $\sigma_{ij}$ is measurable and progressively measurable, and for every $j<d$ and every $T>0$ ,

\int_\Omega\int_0^T\|\sigma_{ij}(s,X_s(\omega))\|^2\,ds\,dP(\omega)<\top.

Then for every $T'>0$ ,

\int_\Omega\left(\sup_m\left\|\operatorname{dyadicRunMax}(\text{diffusion}_i,T',m)(\omega)\right\|\right)^2dP(\omega)<\top.

This is an ENNReal finiteness result used in the componentwise $S^2$ estimate.

Original Lean declaration header

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

theorem lintegral_sq_iSup_diffusion_lt_top
    (W : LevyStochCalc.Brownian.Multidim.MultidimBrownianMotion P d)
    (ℱ : MeasureTheory.Filtration ℝ ‹MeasurableSpace Ω›)
    (hℱW : ∀ j : Fin d, LevyStochCalc.Brownian.IsBrownianFiltration (W.W j) ℱ)
    (coeffs : LevyStochCalc.Ito.Setting.JumpDiffusionCoeffs n d E)
    (X : ℝ → Ω → (Fin n → ℝ))
    (h_meas : ∀ i : Fin n, ∀ j : Fin d,
      Measurable (Function.uncurry (fun ω s => coeffs.σ s (X s ω) i j)))
    (h_progMeas : ∀ i : Fin n, ∀ j : Fin d,
      Probability.ProgressivelyMeasurable ℱ (fun ω s => coeffs.σ s (X s ω) i j))
    (h_sq : ∀ i : Fin n, ∀ j : Fin d, ∀ T : ℝ, 0 < T →
      ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
        (‖coeffs.σ s (X s ω) i j‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
    (i : Fin n) {T' : ℝ} (hT' : 0 < T') :
    ∫⁻ ω, (⨆ m, (‖dyadicRunMax (fun t ω =>
        picardStep_diffusion W ℱ hℱW coeffs X h_meas h_progMeas h_sq t ω i)
        T' m ω‖₊ : ℝ≥0∞)) ^ 2 ∂P < ⊤

Module navigation

Module: LevyStochCalc/Ito/PicardSupL2.

Definition modules: LevyStochCalc/Brownian/Filtered, LevyStochCalc/Brownian/Multidim, LevyStochCalc/Ito/Setting, LevyStochCalc/Probability/Progressive, LevyStochCalc/Ito/PicardStepMap, LevyStochCalc/Probability/DoobContinuous.

Supporting theorems: enorm_dyadicRunMax, lintegral_sq_dyadicRunMax_le, sq_sum_le_card_sq_mul.

Previous: lintegral_sq_drift_bound_lt_top · Next: lintegral_sq_iSup_picardStep_lt_top.

Source excerpt, lines 205–221 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_LevyStochCalc_Ito_PicardSupL2

/-
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/Ito/PicardSupL2.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
open MeasureTheory ProbabilityTheory LevyStochCalc.Probability
open scoped NNReal ENNReal
universe u v
variable {Ω : Type u} [MeasurableSpace Ω] {E : Type v} [MeasurableSpace E]
variable {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {n d : ℕ}
omit [MeasurableSpace E]

Formal statement


theorem LevyStochCalc.Ito.Picard.lintegral_sq_iSup_diffusion_lt_top_readable
    (W : LevyStochCalc.Brownian.Multidim.MultidimBrownianMotion P d)
    (ℱ : MeasureTheory.Filtration ℝ ‹MeasurableSpace Ω›)
    (hℱW : ∀ j : Fin d, LevyStochCalc.Brownian.IsBrownianFiltration (W.W j) ℱ)
    (coeffs : LevyStochCalc.Ito.Setting.JumpDiffusionCoeffs n d E)
    (X : ℝ → Ω → (Fin n → ℝ))
    (h_meas : ∀ i : Fin n, ∀ j : Fin d,
      Measurable (Function.uncurry (fun ω s => coeffs.σ s (X s ω) i j)))
    (h_progMeas : ∀ i : Fin n, ∀ j : Fin d,
      Probability.ProgressivelyMeasurable ℱ (fun ω s => coeffs.σ s (X s ω) i j))
    (h_sq : ∀ i : Fin n, ∀ j : Fin d, ∀ T : ℝ, 0 < T →
      ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
        (‖coeffs.σ s (X s ω) i j‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
    (i : Fin n) {T' : ℝ} (hT' : 0 < T') :
    ∫⁻ ω, (⨆ m, (‖dyadicRunMax (fun t ω =>
        picardStep_diffusion W ℱ hℱW coeffs X h_meas h_progMeas h_sq t ω i)
        T' m ω‖₊ : ℝ≥0∞)) ^ 2 ∂P < ⊤ := by sorry

Source

Lean source: https://github.com/cgarryZA/LevyStochCalc/blob/984dbf0b790031eac05d56fe5a84b65e15e1e932/LevyStochCalc/Ito/PicardSupL2.lean#L203-L251 (repository human-ai-mathematics/kls-lean, commit 408915f, module `LevyStochCalc.Ito.PicardSupL2`, declaration `LevyStochCalc.Ito.Picard.lintegral_sq_iSup_diffusion_lt_top`; 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

Finite Dyadic S2S^2S2 Bound for the Diffusion Component

Finite Dyadic $S^2$ Bound for the Diffusion Component