Tensorization (subadditivity) of entropy for product probability measures: $\mathrm{Ent}_{\otimes\mu_i}(h)\le\sum_i\int\mathrm{Ent}_{\mu_i}(h)\,d\mu$

Let $\iota$ be a finite index set, $(\Omega, \mathcal{F})$ a measurable space, and $\mu_i$ ($i\in\iota$) probability measures on $\Omega$. Let $\mu = \bigotimes_{i\in\iota}\mu_i$ be the product measure on $\Omega^\iota$. For $x \in \Omega^\iota$, $i \in \iota$ and $t \in \Omega$ write $x^{(i\leftarrow t)}$ for the point obtained from $x$ by replacing its $i$-th coordinate with $t$. For a positive function $\varphi$ on a probability space $(E,\nu)$ let $\mathrm{Ent}_\nu(\varphi) = \int \varphi\log\varphi\,d\nu - \big(\int\varphi\,d\nu\big)\log\big(\int\varphi\,d\nu\big)$.

Let $h : \Omega^\iota \to (0,\infty)$ be measurable, with $h$ and $h \log h$ both $\mu$-integrable. Then

that is,

The inner bracket depends only on the coordinates of $x$ other than $i$, so this is the usual statement that the entropy of a product measure is bounded by the sum of the expected conditional (one-coordinate) entropies. It reduces log-Sobolev inequalities on product spaces to one-dimensional ones; for the Gaussian measure it turns the one-dimensional log-Sobolev inequality into the dimension-free inequality on $\mathbb{R}^\iota$.

Formalization Note. The product measure is Measure.pi μ on ι → Ω and $x^{(i\leftarrow t)}$ is Function.update x i t (hence [DecidableEq ι]). The function is assumed strictly positive, which is all that the application ($h = g^2+\delta$) needs; the general nonnegative case follows by approximation but is not claimed here. For $\mu$-almost every $x$ the sections are integrable, and the outer integrands are genuinely integrable, so the Bochner conventions play no role. For $\iota = \emptyset$ both sides are $0$.