One-dimensional Gaussian logarithmic Sobolev inequality: $\mathrm{Ent}_\gamma(g^2)\le 2\int (g')^2\,d\gamma$ for $C^1$ functions $g:\mathbb{R}\to\mathbb{R}$

Let $\gamma = N(0,1)$ be the standard Gaussian measure on $\mathbb{R}$. Let $g : \mathbb{R} \to \mathbb{R}$ be continuously differentiable, and assume that $g^2$, $g^2 \log g^2$ and $(g')^2$ are $\gamma$-integrable (with the convention $0 \log 0 = 0$). Then

The left-hand side is the entropy $\mathrm{Ent}_\gamma(g^2)$ of the nonnegative function $g^2$.

This is Gross's logarithmic Sobolev inequality for the Gaussian measure in dimension one, with the sharp constant $2$. Together with the tensorization of entropy it yields the inequality on $\mathbb{R}^\iota$ (gaussian_logsobolev), which in turn gives the entropy bound $\mathrm{Ent}(e^{sf}) \le \tfrac{s^2L^2}{2}\mathbb{E}e^{sf}$ for Lipschitz $f$ used in Herbst's argument. It is the only analytic input of the whole chain that is not elementary.

Formalization Note. The derivative is deriv g, and $C^1$ is ContDiff ℝ 1 g. The integrability hypotheses guarantee that all Bochner integrals in the statement are the true (finite) integrals; Real.log 0 = 0 matches the convention $0\log 0 = 0$. The hypotheses on $g^2$ and $g^2\log g^2$ are in fact consequences of the others (Gaussian Poincaré inequality and the inequality itself) but are included to keep the statement transparent. Constant $g$ gives $0 \le 0$.