Energy Bound by Weighted Energy and Cutoff Tail

This formalizes the boundary-term splitting associated with the cumulant bounds cited as Theorem 4.1, p. 18, of Bizeul–Klartag–Lehec (arXiv:2610.05474v1).

Let $\mu$ be isotropic with compact support, let $p_t$ be an IsEldanCutoff process using the ball cutoff $\gamma_R$, and fix $d\in\mathbb N$, $u\in\operatorname{EuclideanSpace}(\mathbb R,\operatorname{Fin}(n))$, and $t\geq0$. Assume:

1. $C\geq0$.
2. For every parameter $q=(c,Q)$ with $Q$ self-adjoint and positive semidefinite, the cumulant energy $E_d(q)$ is at most $C$.
3. The map $q\mapsto E_d(q)$ is continuous.

Then

This inequality separates the cutoff-weighted contribution from the tail outside the cutoff ball.

Formalization Note. The probability term is the toReal coercion of an ENNReal measure, and $\gamma_R$ is ballCutoff R.

Original Lean declaration header

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

theorem IsEldanCutoff.integral_energy_le_weighted_add (hiso : KLS.Isotropic μ) {R : ℝ}
    (h : IsEldanCutoff μ hc W ℱ hW (ballCutoff R) p) (d : ℕ) (u : EuclideanSpace ℝ (Fin n))
    {C : ℝ} (hC0 : 0 ≤ C)
    (hC : ∀ q : Param n, IsSelfAdjoint q.2 → (∀ x, 0 ≤ ⟪q.2 x, x⟫) →
      cumulantEnergy (compactPosterior μ hc q.1 q.2 : Measure (EuclideanSpace ℝ (Fin n))) d u ≤ C)
    (hcont : Continuous fun q : Param n =>
      cumulantEnergy (compactPosterior μ hc q.1 q.2 : Measure (EuclideanSpace ℝ (Fin n))) d u)
    {t : ℝ} (ht : 0 ≤ t) :
    ∫ w, cumulantEnergy (compactPosterior μ hc (p t w).1 (p t w).2 : Measure (EuclideanSpace ℝ (Fin n))) d u ∂P ≤
      (∫ w, ballCutoff R (p t w) ^ 2 *
        cumulantEnergy (compactPosterior μ hc (p t w).1 (p t w).2 : Measure (EuclideanSpace ℝ (Fin n))) d u ∂P) +
        C * (P {w | R < ‖p t w‖}).toReal

Module navigation

Module: KLS/BKL/Localization/CutoffEnergy/Boundary.

Definition modules: KLS/BKL/CumulantEnergy/Basic, KLS/BKL/Localization/Process/Basic, KLS/BKL/Localization/Coefficients, LevyStochCalc/Brownian/Filtered, KLS/Isotropic, LevyStochCalc/Brownian/Multidim, Probability/Posterior/CompactDomain, Analysis/Cutoff/LipschitzBall.

Supporting theorems: IsEldanCutoff.ae_Q_posSemidef.

Previous: exists_le_setIntegral_div · Next: IsEldanCutoff.exists_weighted_energy_le.

Source excerpt, lines 127–138 · Frozen source 408915f.