Prove2Me

Gaussian log-Sobolev inequality for compactly supported C1C^1 functions: Entγ(g2)≤2∫(g′)2 dγ\mathrm{Ent}_\gamma(g^2)\le 2\int (g')^2\,d\gamma

Proved
GaussianMatrix.gaussian_logsobolev_one_dim_compact_support

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

entropyfunctional-inequalitygaussiangrosslog-sobolev

Let γ=N(0,1)\gamma = N(0,1) be the standard Gaussian measure on R\mathbb{R}, and let g:R→Rg:\mathbb{R}\to\mathbb{R} be continuously differentiable with compact support. Then

∫g2log⁡g2 dγ−(∫g2 dγ)log⁡(∫g2 dγ)  ≤  2∫(g′)2 dγ,\int g^2\log g^2\,d\gamma-\Big(\int g^2\,d\gamma\Big)\log\Big(\int g^2\,d\gamma\Big)\;\le\;2\int (g')^2\,d\gamma ,

with the convention 0log⁡0=00\log 0=0.

This is Gross's inequality restricted to compactly supported test functions. All integrals are finite, so no integrability hypotheses are needed. The general one-dimensional inequality gaussian_logsobolev_one_dim follows from this case by multiplying gg with smooth cutoffs χ(x/n)\chi(x/n) and applying dominated convergence. In turn, this case follows from gaussian_logsobolev_bounded_below applied to g2+εg^2+\varepsilon, letting ε↓0\varepsilon\downarrow 0.

Formalization Note. The derivative is deriv g and C1C^1 is ContDiff ℝ 1 g. Real.log 0 = 0 matches 0log⁡0=00\log 0 = 0, and g≡0g\equiv 0 gives 0≤00\le 0.

Preamble
import Definitions.Def_GaussianMatrix_basic

open MeasureTheory ProbabilityTheory
open scoped Matrix
Formal statement
namespace GaussianMatrix

theorem gaussian_logsobolev_one_dim_compact_support (g : ℝ → ℝ) (hg : ContDiff ℝ 1 g)
    (hgc : HasCompactSupport g) :
    ∫ t, g t ^ 2 * Real.log (g t ^ 2) ∂(gaussianReal 0 1)
      - (∫ t, g t ^ 2 ∂(gaussianReal 0 1)) * Real.log (∫ t, g t ^ 2 ∂(gaussianReal 0 1))
      ≤ 2 * ∫ t, deriv g t ^ 2 ∂(gaussianReal 0 1) := by
  sorry

end GaussianMatrix
Source
L. Gross, Logarithmic Sobolev inequalities, Amer. J. Math. 97 (1975), 1061–1083 (Gaussian case); M. Ledoux, The Concentration of Measure Phenomenon (AMS, 2001), Theorem 5.1 / inequality (5.3); D. Bakry, I. Gentil, M. Ledoux, Analysis and Geometry of Markov Diffusion Operators (Springer, 2014), Proposition 5.5.1. Theorem and equation numbers are cited from memory and should be checked.

View graph