Existence of a Lyapunov Generator Constant

This establishes a pointwise generator inequality for the localization Lyapunov function.

Let $\mu$ be a compactly supported isotropic log-concave probability measure on $\mathbb{R}^n$, assume CumulantBoundCompact 2 8, and suppose that for some $r\ge0$ the support of $\mu$ is contained in the closed ball $\overline B(0,r)$. Then there exists $K\ge0$ such that, for every localization parameter $p=(c,Q)$ with $Q$ self-adjoint and positive semidefinite,

The formal statement asserts existence of $K$ and does not require a dimension-free choice. It packages the generator estimates for the separate components of lyapunov.

Original Lean declaration header

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

set_option maxHeartbeats 1000000 in
theorem exists_generator_lyapunov_le (hiso : KLS.Isotropic μ) (hLC : KLS.LogConcave μ)
    (h8 : LogConcave.Suspension.CumulantBoundCompact 2 8) {r : ℝ} (hr : 0 ≤ r)
    (hsupp : (μ : Measure (EuclideanSpace ℝ (Fin n))).support ⊆ Metric.closedBall 0 r) :
    ∃ K : ℝ, 0 ≤ K ∧ ∀ p : Param n, IsSelfAdjoint p.2 → (∀ x, 0 ≤ ⟪p.2 x, x⟫) →
      generator μ hc (lyapunov μ hc) p ≤ K * lyapunov μ hc p

Module navigation

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

Definition modules: KLS/BKL/Localization/Coefficients, Probability/LogConcave, KLS/Isotropic, KLS/BKL/Localization/Lyapunov/Basic, KLS/BKL/CompactReduction.

Selected supporting theorems: inner_self_pos_of_comp_eq_id, opNorm_sq_le_hsNormSq, sum_inner_apply_le_sqrt_hsNormSq_mul, Covariance.inner_operator_self_pos_of_affineSupport_eq_top, generator_hsNormSq_snd.

Previous: sum_sq_fderiv_stdTrace_ringInverse_cov_noise_le.

Source excerpt, lines 379–384 · Frozen source 408915f.