Gaussian integration by parts: $\mathbb E[U\,G(V)]=\sum_j \mathrm{Cov}(U,V_j)\,\mathbb E[\partial_j G(V)]$ for jointly Gaussian $(U,V)$, $U$ centered, $G\in C^1_b$

Let $\iota$ be a finite index set and let $(\Omega,P)$ be a probability space. Let $U:\Omega\to\mathbb R$ and $V=(V_j)_{j\in\iota}:\Omega\to\mathbb R^\iota$ be random variables such that the pair $(U,V)$ has a Gaussian law on $\mathbb R\times\mathbb R^\iota$, and suppose $U$ is centered: $\mathbb E\,U=0$. Let $G:\mathbb R^\iota\to\mathbb R$ be differentiable everywhere, with partial derivatives $G'_j=\partial_jG$. Assume each $G'_j$ is continuous, and that for some constant $C$ we have $|G|\le C$ and $|G'_j|\le C$ for all $j$. Then

This is the Gaussian integration-by-parts (Stein) identity. It drives Gaussian interpolation arguments: the Sudakov–Fernique and Slepian comparison inequalities, Gordon's inequality, and Chatterjee's error bounds. In those arguments one differentiates $\theta\mapsto\mathbb E\,F(Z(\theta))$ along an interpolating Gaussian path $Z(\theta)$ and turns $\mathbb E[Z'_i\,\partial_iF(Z)]$ into covariances times second derivatives. Here the identity is proved by regressing $V$ on $U$. The residual $V-cU$ is uncorrelated with $U$, hence independent of it, which reduces the claim to the one-dimensional identity $\mathbb E[\xi h(\xi)]=v\,\mathbb E[h'(\xi)]$ for $\xi\sim N(0,v)$.

Formalization Note. Joint Gaussianity is HasGaussianLaw (fun ω => (U ω, fun j => V j ω)) P; this also forces $P$ to be a probability measure. The gradient is supplied explicitly: HasFDerivAt G (∑ j, G' j x • proj j) x, i.e. $DG(x)v=\sum_j G'_j(x)v_j$. The covariance is Mathlib's cov[U, V j; P]. Edge cases: if $\operatorname{Var}U=0$, both sides are $0$; if $\iota=\emptyset$, $G$ is constant and both sides are $0$ because $\mathbb E\,U=0$. The boundedness of $G$ and $\nabla G$ is a convenient sufficient regularity class ($C^1_b$); it makes every integral finite, so the Bochner convention for non-integrable functions plays no role.