Cutoff Eldan localization process predicate

Definition

KLSModular_FunctionalInequalities_KLS_BKL_Localization_Process_Basic

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

IsEldanCutoff μ hc W ℱ hW γ p defines the cutoff Eldan process for a probability measure $\mu$ on $\mathrm{EuclideanSpace}\,\mathbb{R}\,(\mathrm{Fin}\,n)$ with compact support and parameter process $p_t$ . It requires that the coordinate representation of $p_t$ under stateEquiv (Param n) is an IsDiffusion with transported cutoff drift transportDrift ... (cutoffDrift μ hc γ), transported cutoff noise transportNoise ... (cutoffNoise μ hc γ), and initial state corresponding to zero. The predicate is conditional on a Brownian motion, filtration, Brownian-filtration hypotheses, and cutoff function $\gamma$ ; it does not itself assert existence.

Original module imports

import FunctionalInequalities.KLS.BKL.Localization.Coefficients
import FunctionalInequalities.Probability.Diffusion.Transport
import FunctionalInequalities.Probability.Diffusion.Setup
import FunctionalInequalities.Probability.Diffusion.Existence
import FunctionalInequalities.Probability.Diffusion.Dynkin
import FunctionalInequalities.KLS.BKL.Posterior.Covariance
import FunctionalInequalities.KLS.BKL.Posterior.Regularity
import FunctionalInequalities.Probability.Diffusion.Generator

Original declaration excerpt

Shown in the original module context.

def IsEldanCutoff {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
    (W : MultidimBrownianMotion P n) (ℱ : Filtration ℝ ‹MeasurableSpace Ω›)
    (hW : ∀ k, IsBrownianFiltration (W.W k) ℱ) (γ : Param n → ℝ)
    (p : ℝ → Ω → Param n) : Prop :=
  IsDiffusion W ℱ hW (transportDrift (stateEquiv (Param n)) (cutoffDrift μ hc γ))
    (transportNoise (stateEquiv (Param n)) (cutoffNoise μ hc γ)) (stateEquiv (Param n) 0)
    (fun t ω => stateEquiv (Param n) (p t ω))

Module navigation

Direct project imports: KLS/BKL/Localization/Coefficients, Probability/Diffusion/Transport, Probability/Diffusion/Setup, Probability/Diffusion/Existence, Probability/Diffusion/Dynkin, KLS/BKL/Posterior/Covariance, KLS/BKL/Posterior/Regularity, Probability/Diffusion/Generator.

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.KLS.BKL.Localization.Process.Basic · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Localization_Coefficients
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Diffusion_Transport
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Diffusion_Setup
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Diffusion_Existence
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Diffusion_Dynkin
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Posterior_Covariance
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Posterior_Regularity
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Diffusion_Generator

noncomputable section
open MeasureTheory ProbabilityTheory Filter Topology
open scoped NNReal ENNReal RealInnerProductSpace
open FunctionalInequalities.Probability.Posterior FunctionalInequalities.Analysis
  FunctionalInequalities.Probability.Diffusion
namespace FunctionalInequalities
namespace KLS
namespace BKL
namespace Localization
open LevyStochCalc LevyStochCalc.Brownian LevyStochCalc.Brownian.Multidim LevyStochCalc.Brownian.Ito
variable {n : ℕ} (μ : ProbabilityMeasure (EuclideanSpace ℝ (Fin n)))
  (hc : IsCompact (μ : Measure (EuclideanSpace ℝ (Fin n))).support)
/-- **The cutoff Eldan process** (BKL arXiv:2610.05474v1, (67), with cutoff coefficients `γ² · drift`, `γ · noise`)
in parameter-space form: its coordinates under `stateEquiv (Param n)` form an `IsDiffusion` with the transported cutoff coefficients, started at `p₀ = (0, 0)`. -/
def IsEldanCutoff {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
    (W : MultidimBrownianMotion P n) (ℱ : Filtration ℝ ‹MeasurableSpace Ω›)
    (hW : ∀ k, IsBrownianFiltration (W.W k) ℱ) (γ : Param n → ℝ)
    (p : ℝ → Ω → Param n) : Prop :=
  IsDiffusion W ℱ hW (transportDrift (stateEquiv (Param n)) (cutoffDrift μ hc γ))
    (transportNoise (stateEquiv (Param n)) (cutoffNoise μ hc γ)) (stateEquiv (Param n) 0)
    (fun t ω => stateEquiv (Param n) (p t ω))
end Localization
end BKL
end KLS
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/Localization/Process/Basic.lean#L32-L40 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.Localization.Process.Basic`, definition bundle `KLSModular_FunctionalInequalities_KLS_BKL_Localization_Process_Basic`; the repository is private at upload time).

View graph