Prove2Me

Gaussian log-Sobolev inequality Entγ(f)≤12∫(f′)2/f dγ\mathrm{Ent}_\gamma(f)\le\frac12\int (f')^2/f\,d\gamma for C1C^1 functions ff bounded away from 00 with bounded derivative

Proved
GaussianMatrix.gaussian_logsobolev_bounded_below

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

bakry-emeryentropygaussianlog-sobolevornstein-uhlenbeck

Let γ=N(0,1)\gamma=N(0,1) be the standard Gaussian measure on R\mathbb{R}. Let δ>0\delta>0 and C∈RC\in\mathbb{R}, and let f:R→Rf:\mathbb{R}\to\mathbb{R} be continuously differentiable with δ≤f(x)≤C\delta\le f(x)\le C and ∣f′(x)∣≤C|f'(x)|\le C for all xx. Then

∫flog⁡f dγ−(∫f dγ)log⁡(∫f dγ)  ≤  12∫(f′)2f dγ.\int f\log f\,d\gamma-\Big(\int f\,d\gamma\Big)\log\Big(\int f\,d\gamma\Big)\;\le\;\frac12\int\frac{(f')^2}{f}\,d\gamma .

This is the entropy form of Gross's inequality; substituting f=g2f=g^2 gives the usual form. It is proved with the Bakry–Émery argument along the Ornstein–Uhlenbeck semigroup PtP_t. The entropy decreases with rate equal to the Fisher information (ou_entropy_hasDerivAt). By commutation and Cauchy–Schwarz, the Fisher information of PtfP_tf is at most e−2t∫(f′)2/f dγe^{-2t}\int (f')^2/f\,d\gamma, and invariance of γ\gamma handles the integral. Hence t↦Ent(Ptf)−12e−2t∫(f′)2/f dγt\mapsto\mathrm{Ent}(P_tf)-\frac12e^{-2t}\int (f')^2/f\,d\gamma is nondecreasing on [0,∞)[0,\infty); it equals the difference of the two sides at t=0t=0 and tends to 00 as t→∞t\to\infty.

Formalization Note. The hypotheses force C≥δ>0C\ge\delta>0. All integrands are bounded and measurable, so every Bochner integral is a true integral.

Preamble
import Definitions.Def_GaussianMatrix_basic

open MeasureTheory ProbabilityTheory
open scoped Matrix
Formal statement
namespace GaussianMatrix

theorem gaussian_logsobolev_bounded_below (f : ℝ → ℝ) (hf : ContDiff ℝ 1 f) (δ C : ℝ)
    (hδ : 0 < δ) (hlow : ∀ x, δ ≤ f x) (hup : ∀ x, f x ≤ C) (hdf : ∀ x, |deriv f x| ≤ C) :
    ∫ x, f x * Real.log (f x) ∂(gaussianReal 0 1)
      - (∫ x, f x ∂(gaussianReal 0 1)) * Real.log (∫ x, f x ∂(gaussianReal 0 1))
      ≤ (1 / 2) * ∫ x, deriv f x ^ 2 / f x ∂(gaussianReal 0 1) := by
  sorry

end GaussianMatrix
Source
D. Bakry, M. Émery, Diffusions hypercontractives, Séminaire de Probabilités XIX, Lecture Notes in Math. 1123 (1985), 177–206; D. Bakry, I. Gentil, M. Ledoux, Analysis and Geometry of Markov Diffusion Operators (Springer, 2014), Proposition 5.5.1 and §5.7 (semigroup proof); M. Ledoux, The Concentration of Measure Phenomenon (AMS, 2001), Theorem 5.1 / (5.3). Numbering is cited from memory.

View graph