Admissibility of Cutoff Localization Coefficients

This statement formalizes the regularity and support properties of cutoff coefficients from Equation (67), p. 19, of Bizeul–Klartag–Lehec (arXiv:2610.05474v1).

Let $n\in\mathbb N$, let $\mu$ be a probability measure on EuclideanSpace ℝ (Fin n), assume that its support is compact and that $\mu$ is isotropic, and let $\gamma$ be an admissible cutoff, expressed by IsCutoff γ. Then the cutoff drift and every cutoff noise column satisfy:

1. There is one $K\in[0,\infty)$ such that the cutoff drift and every cutoff noise column are globally $K$-Lipschitz.
2. There is one $B\in\mathbb R$ uniformly bounding the norms of the cutoff drift and all cutoff noise columns at every parameter.
3. The cutoff drift has compact support.
4. Every cutoff noise column has compact support.

Equivalently, the conclusion is the conjunction of the corresponding global Lipschitz, boundedness, and compact-support assertions. This is an admissibility result for the cutoff coefficients, not a statement about a stochastic process.

Original Lean declaration header

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

theorem cutoffCoefficients_admissible (hiso : KLS.Isotropic μ) {γ : Param n → ℝ} (hγ : IsCutoff γ) :
    (∃ K : ℝ≥0, LipschitzWith K (cutoffDrift μ hc γ) ∧
        ∀ k, LipschitzWith K fun p => cutoffNoise μ hc γ p k) ∧
      (∃ B : ℝ, ∀ p, ‖cutoffDrift μ hc γ p‖ ≤ B ∧ ∀ k, ‖cutoffNoise μ hc γ p k‖ ≤ B) ∧
      HasCompactSupport (cutoffDrift μ hc γ) ∧
      ∀ k, HasCompactSupport fun p => cutoffNoise μ hc γ p k

Module navigation

Module: KLS/BKL/Localization/Coefficients.

Definition modules: KLS/Isotropic.

Selected supporting theorems: Covariance.inner_operator_self_pos_of_affineSupport_eq_top, locallyLipschitz_noise, Isotropic.locallyLipschitz_inverseSqrt_covariance_joint, exists_lipschitzWith_smul_of_locallyLipschitz, contDiff_posteriorCovariance_joint.

Previous: locallyLipschitz_noise.

Source excerpt, lines 153–158 · Frozen source 408915f.