Existence Of The Cutoff Eldan Localization Process

This formalizes the existence assertion associated with Equation (67) of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), locator Equation (67), p. 19. Let $\mu$ be a probability measure on $\operatorname{EuclideanSpace}(\mathbb R,\operatorname{Fin}(n))$ with compact support and assume that $\mu$ is isotropic. Let $W$ be an $n$-dimensional Brownian motion on a probability space $(\Omega,P)$, and let $\mathcal F$ be a right-continuous filtration satisfying the stated ordering and null-set hypotheses. For a cutoff function $\gamma$ satisfying IsCutoff γ, there exists a parameter process $p:\mathbb R\to\Omega\to\operatorname{Param}(n)$ satisfying IsEldanCutoff μ hc W ℱ hW γ p:

The predicate records the cutoff localization dynamics, including the initial parameter and the associated process properties. The theorem is the existence component of the cutoff-stage construction.

Original Lean declaration header

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

theorem exists_isEldanCutoff (hiso : KLS.Isotropic μ)
    {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
    (W : MultidimBrownianMotion P n) (ℱ : Filtration ℝ ‹MeasurableSpace Ω›)
    [ℱ.IsRightContinuous] (hW : ∀ k, IsBrownianFiltration (W.W k) ℱ)
    (hℱ0 : ∀ t : ℝ, t ≤ 0 → ℱ 0 ≤ ℱ t)
    (hnull : ∀ s : Set Ω, MeasurableSet s → P s = 0 → MeasurableSet[ℱ 0] s)
    {γ : Param n → ℝ} (hγ : IsCutoff γ) :
    ∃ p : ℝ → Ω → Param n, IsEldanCutoff μ hc W ℱ hW γ p

Module navigation

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

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

Supporting theorems: cutoffCoefficients_admissible, exists_isDiffusion.

Next: IsEldanCutoff.continuous.

Source excerpt, lines 44–51 · Frozen source 408915f.