Prove2Me

Herbst's argument: an entropy bound Ent(esf)≤cs2 Eesf\mathrm{Ent}(e^{sf})\le c s^2\,\mathbb{E}e^{sf} for all s>0s>0 implies Eesf≤esEf+cs2\mathbb{E}e^{sf}\le e^{s\mathbb{E}f+cs^2}

Proved
GaussianMatrix.herbst_argument

by tc · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

entropyherbst-argumentlog-sobolevmoment-generating-functionsub-gaussian

Let (Ω,μ)(\Omega, \mu) be a probability space, c∈Rc \in \mathbb{R}, and f:Ω→Rf : \Omega \to \mathbb{R} a function such that esfe^{sf} is μ\mu-integrable for every s∈Rs \in \mathbb{R}. Write M(s)=∫esf dμM(s) = \int e^{sf}\,d\mu and

Entμ(esf)=∫sf esf dμ−M(s)log⁡M(s)\mathrm{Ent}_\mu(e^{sf}) = \int s f\, e^{sf}\, d\mu - M(s)\log M(s)

for the entropy of esfe^{sf}. Suppose that

Entμ(esf)≤c s2 M(s)for every s>0.\mathrm{Ent}_\mu(e^{sf}) \le c\, s^2\, M(s) \qquad \text{for every } s > 0 .

Then for every s≥0s \ge 0,

∫esf dμ  ≤  exp⁡(s∫f dμ+c s2).\int e^{sf}\, d\mu \;\le\; \exp\Big(s \int f\, d\mu + c\, s^2\Big).

This is Herbst's argument, which turns a logarithmic Sobolev type inequality into a sub-Gaussian bound on the moment generating function. With c=L2/2c = L^2/2 and the Gaussian entropy bound for LL-Lipschitz functions, it gives E es(f−Ef)≤es2L2/2\mathbb{E}\,e^{s(f - \mathbb{E}f)} \le e^{s^2L^2/2}; the Chernoff bound then yields sharp Gaussian concentration.

Formalization Note. The integrability hypothesis for all real ss implies that ff itself is integrable, so ∫f dμ\int f\,d\mu is the true mean. No sign condition on cc is assumed. Entropy is nonnegative and M(s)>0M(s) > 0, so the hypothesis already forces c≥0c \ge 0.

Preamble
import Definitions.Def_GaussianMatrix_basic

open MeasureTheory ProbabilityTheory
open scoped Matrix
Formal statement
namespace GaussianMatrix

theorem herbst_argument {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ]
    (f : Ω → ℝ) (c : ℝ) (hint : ∀ s : ℝ, Integrable (fun ω => Real.exp (s * f ω)) μ)
    (hent : ∀ s : ℝ, 0 < s →
      ∫ ω, s * f ω * Real.exp (s * f ω) ∂μ
        - (∫ ω, Real.exp (s * f ω) ∂μ) * Real.log (∫ ω, Real.exp (s * f ω) ∂μ)
        ≤ c * s ^ 2 * ∫ ω, Real.exp (s * f ω) ∂μ)
    (s : ℝ) (hs : 0 ≤ s) :
    ∫ ω, Real.exp (s * f ω) ∂μ ≤ Real.exp (s * ∫ ω, f ω ∂μ + c * s ^ 2) := by sorry

end GaussianMatrix
Source
S. Boucheron, G. Lugosi, P. Massart, Concentration Inequalities (Oxford Univ. Press, 2013), Proposition 6.1 (Herbst's argument), stated there with v=2cv = 2c; M. Ledoux, The Concentration of Measure Phenomenon (AMS, 2001), §5.1, Theorem 5.3. Numbering is cited from memory.

View graph