Continuity of Cutoff Localization Paths

Proved

FunctionalInequalities.KLS.BKL.Localization.IsEldanCutoff.continuous_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement establishes path continuity for an IsEldanCutoff process. Let $p:ℝ→Ω→\operatorname{Param}(n)$ satisfy the cutoff Eldan-process assumptions, including the associated Brownian motion and filtration. Then every sample path is continuous:

\forall ω∈Ω,\qquad t\mapsto p_t(ω)\text{ is continuous on }ℝ.

The conclusion is everywhere in $ω$ , not merely almost surely. It provides the regularity needed for subsequent pathwise integral and localization arguments.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS.BKL.Localization. Shown in its original module context. Proof omitted.

theorem IsEldanCutoff.continuous (h : IsEldanCutoff μ hc W ℱ hW γ p) (ω : Ω) :
    Continuous fun t => p t ω

Module navigation

Module: KLS/BKL/Localization/Process/Basic.

Definition modules: KLS/BKL/Localization/Coefficients, LevyStochCalc/Brownian/Filtered, LevyStochCalc/Brownian/Multidim.

Previous: exists_isEldanCutoff · Next: IsEldanCutoff.dynkin.

Source excerpt, lines 146–147 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Localization_Process_Basic

variable {n : ℕ} (μ : MeasureTheory.ProbabilityMeasure (EuclideanSpace ℝ (Fin n)))
  (hc : IsCompact (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))).support)
variable {μ hc} {Ω : Type*} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P]
  {W : LevyStochCalc.Brownian.Multidim.MultidimBrownianMotion P n} {ℱ : MeasureTheory.Filtration ℝ ‹MeasurableSpace Ω›}
  {hW : ∀ k, LevyStochCalc.Brownian.IsBrownianFiltration (W.W k) ℱ} {γ : FunctionalInequalities.KLS.BKL.Localization.Param n → ℝ} {p : ℝ → Ω → FunctionalInequalities.KLS.BKL.Localization.Param n}

Formal statement


theorem FunctionalInequalities.KLS.BKL.Localization.IsEldanCutoff.continuous_readable (h : IsEldanCutoff μ hc W ℱ hW γ p) (ω : Ω) :
    Continuous fun t => p t ω := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/Localization/Process/Basic.lean#L145-L162 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.Localization.Process.Basic`, declaration `FunctionalInequalities.KLS.BKL.Localization.IsEldanCutoff.continuous`; the repository is private at upload time).

View graph