Usual Brownian filtration and diffusion predicate

Definition

KLSModular_FunctionalInequalities_Probability_Diffusion_Setup

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For a multidimensional Brownian motion W under a probability measure $P$ , usualFiltration W is the augmentation of the right-continuous natural filtration of W; the included instance asserts that this filtration is right-continuous. IsDiffusion W ℱ hW b σ x₀ Y means that $Y : \mathbb{R}\to\Omega\to(\mathrm{Fin}\,N\to\mathbb{R})$ has an Itô representation with initial value $x₀$ , drift $b(Y_s)$ , and diffusion coefficients $\sigma(Y_s)$ driven by the Brownian coordinates of W. The predicate additionally requires measurability, progressive measurability, and finite ENNReal squared energy on every interval $[0,T]$ with $T>0$ for each diffusion coefficient, together with the IsVectorItoVersion relation.

Original module imports

import LevyStochCalc.Ito.PicardGlobal
import LevyStochCalc.Ito.VectorItoVersionLimit
import LevyStochCalc.Ito.ItoFormulaUnbounded
import LevyStochCalc.Brownian.AugmentedFiltration
import LevyStochCalc.Brownian.MultidimFiltered
import LevyStochCalc.Brownian.ItoL2CompletionMaster
import LevyStochCalc.Brownian.ItoFinsetSum
import LevyStochCalc.Probability.DoobContinuous
import LevyStochCalc.Poisson.Filtered

Original declaration excerpt

Shown in the original module context.

noncomputable def usualFiltration (W : MultidimBrownianMotion P d) :
    Filtration ℝ ‹MeasurableSpace Ω› :=
  augFiltration W.naturalFiltration.rightCont P

Module navigation

Direct project imports: LevyStochCalc/Ito/PicardGlobal, LevyStochCalc/Ito/VectorItoVersionLimit, LevyStochCalc/Ito/ItoFormulaUnbounded, LevyStochCalc/Brownian/AugmentedFiltration, LevyStochCalc/Brownian/MultidimFiltered, LevyStochCalc/Brownian/ItoL2CompletionMaster, LevyStochCalc/Brownian/ItoFinsetSum, LevyStochCalc/Probability/DoobContinuous, LevyStochCalc/Poisson/Filtered.

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Probability.Diffusion.Setup · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_LevyStochCalc_Ito_PicardGlobal
import Definitions.Def_KLSModular_LevyStochCalc_Ito_VectorItoVersionLimit
import Definitions.Def_KLSModular_LevyStochCalc_Ito_ItoFormulaUnbounded
import Definitions.Def_KLSModular_LevyStochCalc_Brownian_AugmentedFiltration
import Definitions.Def_KLSModular_LevyStochCalc_Brownian_MultidimFiltered
import Definitions.Def_KLSModular_LevyStochCalc_Brownian_ItoL2CompletionMaster
import Definitions.Def_KLSModular_LevyStochCalc_Brownian_ItoFinsetSum
import Definitions.Def_KLSModular_LevyStochCalc_Probability_DoobContinuous
import Definitions.Def_KLSModular_LevyStochCalc_Poisson_Filtered

open MeasureTheory ProbabilityTheory Filter Topology
open scoped NNReal ENNReal
namespace FunctionalInequalities
namespace Probability
namespace Diffusion
open LevyStochCalc LevyStochCalc.Brownian LevyStochCalc.Brownian.Multidim
  LevyStochCalc.Brownian.Ito
section Usual
variable {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P] {d : ℕ}
noncomputable def usualFiltration (W : MultidimBrownianMotion P d) :
    Filtration ℝ ‹MeasurableSpace Ω› :=
  augFiltration W.naturalFiltration.rightCont P
instance (W : MultidimBrownianMotion P d) : (usualFiltration W).IsRightContinuous :=
  isRightContinuous_augFiltration W.naturalFiltration P
end Usual
section Diffusion
variable {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω}
  [IsProbabilityMeasure P] {N d : ℕ}
/-- `Y` is an everywhere-continuous adapted version of
`x₀ + ∫₀ᵗ b(Y_s) ds + Σ_k ∫₀ᵗ σ_k(Y_s) dW^k_s`, coefficients evaluated along `Y` itself. -/
def IsDiffusion (W : MultidimBrownianMotion P d) (ℱ : Filtration ℝ ‹MeasurableSpace Ω›)
    (hW : ∀ k, IsBrownianFiltration (W.W k) ℱ)
    (b : (Fin N → ℝ) → Fin N → ℝ) (σ : (Fin N → ℝ) → Fin d → Fin N → ℝ) (x₀ : Fin N → ℝ)
    (Y : ℝ → Ω → Fin N → ℝ) : Prop :=
  ∃ (hm : ∀ i k, Measurable (Function.uncurry fun ω s => σ (Y s ω) k i))
    (hp : ∀ i k, Probability.ProgressivelyMeasurable ℱ fun ω s => σ (Y s ω) k i)
    (hq : ∀ i k (T : ℝ), 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
      (‖σ (Y s ω) k i‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤),
    IsVectorItoVersion W ℱ hW (fun i k ω s => σ (Y s ω) k i) hm hp hq
      (fun _ => x₀) (fun i ω s => b (Y s ω) i) Y
end Diffusion
end Diffusion
end Probability
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Probability/Diffusion/Setup.lean#L33-L70 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.Diffusion.Setup`, definition bundle `KLSModular_FunctionalInequalities_Probability_Diffusion_Setup`; the repository is private at upload time).

View graph