Compact Log-Concave Quadratic Bound

For every $n>0$, every compactly supported isotropic log-concave probability law $\mu$ on $\mathrm{EuclideanSpace}\,\mathbb R\,(\mathrm{Fin}\,n)$, and every self-adjoint real continuous linear operator $A$, the associated quadratic form satisfies

Equivalently, in the matrix formulation, the right side is $8\operatorname{tr}(A^2)$. The statement includes singular and indefinite self-adjoint operators and is restricted to compactly supported laws.

Original Lean source

Within namespace FunctionalInequalities.KLS.LogConcave.Suspension. Shown in its original module context.

theorem letwinCompactBound : LetwinCompactBound := by
  apply letwinCompactBound_of_regularClass
  intro n hn K W κ hκ hK hKc hKint hW hstrong μ hμ hiso
  exact regularClass_letwinQuadraticBound hn hκ hK hKc hKint hW hstrong μ hμ hiso

Module navigation

Module: KLS/Letwin/CompactBound.

Definition modules: KLS/BKL/CompactReduction.

Supporting theorems: letwinCompactBound_of_regularClass, regularClass_matrix_variance_le_eight.

Source excerpt, lines 26–29 · Frozen source 408915f.

Literature

This formalizes Theorem 1.2 of Letwin (arXiv:2607.24164v1), cited as “Quadratic-form Poincaré inequality,” and is the compact counterpart used in Lemma 4.2 of Bizeul–Klartag–Lehec (arXiv:2610.05474v1).