Gaussian logarithmic Sobolev inequality on $\mathbb{R}^\iota$: $\mathrm{Ent}_{\gamma_\iota}(g^2)\le 2\int\|\nabla g\|_2^2\,d\gamma_\iota$ for $C^1$ functions $g$

Let $\iota$ be a finite index set and $\gamma_\iota = \bigotimes_{i\in\iota} N(0,1)$ the standard Gaussian measure on $\mathbb{R}^\iota$. Let $g : \mathbb{R}^\iota \to \mathbb{R}$ be continuously differentiable, with partial derivatives $\partial_i g(x) = Dg(x)\,e_i$, and assume that $g^2$, $g^2\log g^2$ and $\|\nabla g\|_2^2 = \sum_{i\in\iota}(\partial_i g)^2$ are $\gamma_\iota$-integrable. Then

This is Gross's dimension-free logarithmic Sobolev inequality for the standard Gaussian measure. Applied to $g = e^{sf/2}$ with $\|\nabla f\|_2 \le L$ it gives $\mathrm{Ent}(e^{sf}) \le \tfrac{s^2L^2}{2}\,\mathbb{E}e^{sf}$, the input of Herbst's argument for sharp Gaussian concentration.

Formalization Note. The partial derivative is fderiv ℝ g x (Pi.single i 1); the Euclidean norm of the gradient is written out as a sum of squares (the default norm on ι → ℝ is the sup norm, but fderiv does not depend on the choice of norm). $C^1$ is ContDiff ℝ 1 g. With the integrability hypotheses every Bochner integral in the statement is a true integral. For $\iota = \emptyset$, $g$ is constant and both sides are $0$.