Exponential Lyapunov Moment Bound

This is an auxiliary Grönwall-type estimate for the cutoff Eldan process; the literature register relates it to 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 cutoff $\gamma$, and assume:

1. The filtration and null-set compatibility conditions hold.
2. $K\geq0$.
3. For every parameter $q=(c,Q)$ with $Q$ self-adjoint and positive semidefinite,

$$\operatorname{generator}(\mu,h_c,\mathcal V)(q)\leq K\mathcal V(q),$$

where $\mathcal V=\operatorname{lyapunov}(\mu,h_c)$. 4. $t\geq0$.

Then $\mathcal V(p_t)$ is $P$-integrable and

$$\int_\Omega \mathcal V(p_t(\omega))\,dP(\omega) \leq \mathcal V(0)e^{Kt}.$$

This estimate is the moment bound used to control the localization process and its tails.

Formalization Note. The generator inequality is assumed only on self-adjoint positive-semidefinite matrix components; no universal bound on $K$ is asserted.

Original Lean declaration header

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

theorem IsEldanCutoff.integral_lyapunov_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) :
    Integrable (fun ω => lyapunov μ hc (p t ω)) P ∧
      ∫ ω, lyapunov μ hc (p t ω) ∂P ≤ lyapunov μ hc 0 * Real.exp (K * t)

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.

Selected supporting theorems: le_mul_exp_of_le_add_integral, Covariance.inner_operator_self_pos_of_affineSupport_eq_top, IsEldanCutoff.ae_Q_posSemidef, IsEldanCutoff.continuous, IsEldanCutoff.dynkin.

Next: IsEldanCutoff.measure_norm_gt_le.

Source excerpt, lines 70–78 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Localization_Lyapunov_Moment

open MeasureTheory ProbabilityTheory Filter Topology
open scoped NNReal ENNReal RealInnerProductSpace
variable {n : ℕ} {μ : MeasureTheory.ProbabilityMeasure (EuclideanSpace ℝ (Fin n))}
  {hc : IsCompact (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))).support}
  {Ω : 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}

theorem FunctionalInequalities.KLS.BKL.Localization.IsEldanCutoff.integral_lyapunov_le_readable (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) :
    Integrable (fun ω => lyapunov μ hc (p t ω)) P ∧
      ∫ ω, lyapunov μ hc (p t ω) ∂P ≤ lyapunov μ hc 0 * Real.exp (K * t) := by sorry