Lyapunov-Based Tail Bound

This is a Markov-type tail estimate associated in the literature register with 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 with ball cutoff, and assume:

1. The filtration and null-set compatibility hypotheses hold.
2. $K\geq0$ and the generator satisfies $\mathcal L\mathcal V(q)\leq K\mathcal V(q)$ for every self-adjoint positive-semidefinite parameter matrix.
3. $t\geq0$ and $R>0$.

Then

The result converts the Lyapunov moment estimate into a probability tail bound for the parameter process.

Formalization Note. The probability is an ENNReal measure converted with toReal; the denominator is the ordinary real number $R^2$.

Original Lean declaration header

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

theorem IsEldanCutoff.measure_norm_gt_le (hiso : KLS.Isotropic μ) (hγ : IsCutoff γ)
    (hℱ0 : ∀ t : ℝ, t ≤ 0 → ℱ 0 ≤ ℱ t)
    (hnull : ∀ s : Set Ω, MeasurableSet s → P s = 0 → MeasurableSet[ℱ 0] s)
    (h : IsEldanCutoff μ hc W ℱ hW γ p) {K : ℝ} (hK0 : 0 ≤ K)
    (hK : ∀ q : Param n, IsSelfAdjoint q.2 → (∀ x, 0 ≤ ⟪q.2 x, x⟫) →
      generator μ hc (lyapunov μ hc) q ≤ K * lyapunov μ hc q)
    {t : ℝ} (ht : 0 ≤ t) {R : ℝ} (hR : 0 < R) :
    (P {ω | R < ‖p t ω‖}).toReal ≤ lyapunov μ hc 0 * Real.exp (K * t) / R ^ 2

Module navigation

Module: KLS/BKL/Localization/Lyapunov/Moment.

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

Supporting theorems: opNorm_sq_le_hsNormSq, IsEldanCutoff.integral_lyapunov_le.

Previous: IsEldanCutoff.integral_lyapunov_le.

Source excerpt, lines 309–316 · Frozen source 408915f.