Zero-jump Poisson measure and diffusion coefficient packaging

Definition

KLSModular_FunctionalInequalities_Probability_Diffusion_Existence

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

The private auxiliary definition zeroPoisson constructs a Poisson random measure with zero intensity on Unit: its counting process is identically zero, with the corresponding measurability, integer-valuedness, Poisson-law, independence, and past/future independence fields. The private definition diffusionCoeffs packages autonomous drift $b$ , diffusion coefficients $\sigma$ , and zero jump coefficients into JumpDiffusionCoeffs N d Unit. These are technical data structures used by the surrounding existence construction; this bundle itself exposes no public existence theorem.

Original module imports

import FunctionalInequalities.Probability.Diffusion.Setup
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.Probability.DoobContinuous

Original declaration excerpt

Shown in the original module context. Body omitted.

private def zeroPoisson {Ω : Type u} [MeasurableSpace Ω]
    (P : Measure Ω) [IsProbabilityMeasure P] :
    Poisson.PoissonRandomMeasure.{u, 0, 0} P (0 : Measure Unit)

Module navigation

Direct project imports: Probability/Diffusion/Setup, LevyStochCalc/Ito/PicardGlobal, LevyStochCalc/Ito/VectorItoVersionLimit, LevyStochCalc/Ito/ItoFormulaUnbounded, LevyStochCalc/Brownian/AugmentedFiltration, LevyStochCalc/Brownian/MultidimFiltered, LevyStochCalc/Brownian/ItoL2CompletionMaster, LevyStochCalc/Probability/DoobContinuous.

Theorems in source order:

Project result: The KLS conjecture.

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

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Diffusion_Setup
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_Probability_DoobContinuous

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
universe u
 def zeroPoisson {Ω : Type u} [MeasurableSpace Ω]
    (P : Measure Ω) [IsProbabilityMeasure P] :
    Poisson.PoissonRandomMeasure.{u, 0, 0} P (0 : Measure Unit) where
  N := fun _ => 0
  measurable_eval := fun _ => measurable_const
  integer_valued := fun _ _ =>
    Filter.Eventually.of_forall fun _ => ⟨0, by simp⟩
  infinite_at_infinite_intensity := by
    intro B _ h
    simp [Poisson.referenceIntensity] at h
  poisson_law := by
    intro B _ _
    have hz : poissonMeasure 0 = Measure.dirac 0 := by
      apply Measure.ext_of_singleton
      intro n
      cases n <;> simp [poissonMeasure_singleton]
    change P.map (fun _ => (0 : ℝ≥0∞)) = _
    rw [Measure.map_const]
    simp [Poisson.referenceIntensity, Poisson.poissonMeasureENN, hz]
  independent_disjoint := by
    classical
    intro ι _ _ _ _
    apply iIndepFun_iff_measure_inter_preimage_eq_mul.mpr
    intro S sets hs
    clear hs
    induction S using Finset.induction_on with
    | empty => simp
    | @insert i S hi ih =>
      by_cases hz : (0 : ℝ≥0∞) ∈ sets i <;> simp_all [Set.preimage_const]
  joint_past_future_independent := by
    intro s t _ _ A _ _
    simp only [Measure.coe_zero, Pi.zero_apply, MeasurableSpace.comap_const]
    exact indep_bot_right _
 def diffusionCoeffs {N d : ℕ}
    (b : (Fin N → ℝ) → Fin N → ℝ)
    (σ : (Fin N → ℝ) → Fin d → Fin N → ℝ) :
    LevyStochCalc.Ito.Setting.JumpDiffusionCoeffs N d Unit :=
  ⟨fun _ => b, fun _ x i k => σ x k i, fun _ _ _ => 0⟩
end Diffusion
end Probability
end FunctionalInequalities

Source

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

View graph