The score function has zero mean: $\int p_\theta \, \partial_\theta \log p_\theta \, d\mu = 0$

Proved

ScoreFunction.score_zero_mean

by Cody Wang · Sep 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysiscalculusinformation-geometrymeasure-theorypolicy-gradientprobabilityreinforcement-learningstatistics

The score function has mean zero: the measure-theoretic analogue of score_zero_mean, which is already on the platform in the finite-sum setting.

Let $(\mathcal X,\mathcal A,\mu)$ be a measure space and let $p_\theta$ be a family of probability densities with respect to $\mu$ , so that

\int_{\mathcal X} p_t(x)\, d\mu(x) \;=\; 1 \qquad \text{for every } t \text{ in a neighbourhood of } \theta .

The score at $\theta$ is $\partial_\theta \log p_\theta$ . Then, under the standard conditions for differentiating under the integral sign,

\mathbb E_{p_\theta}\!\left[\partial_\theta \log p_\theta\right] \;=\; \int_{\mathcal X} p_\theta(x)\, \frac{\partial}{\partial\theta}\log p_\theta(x)\; d\mu(x) \;=\; 0 .

The identity is what makes the Fisher information the variance of the score rather than a second moment about an unknown mean, and it is the reason an arbitrary $\theta$ -independent baseline may be subtracted from the reward in a policy-gradient estimator without introducing bias.

Note that normalization is required on a whole neighbourhood of $\theta$ , not merely at $\theta$ itself: the proof differentiates the constant function $t \mapsto \int p_t \, d\mu$ , and a family normalized only at the single point $\theta$ carries no information about that derivative. The remaining hypotheses are the dominated-derivative conditions: almost-everywhere positivity of $p_\theta$ , measurability of $p_t$ near $\theta$ and integrability at $\theta$ , differentiability of $t \mapsto p_t(x)$ on a neighbourhood $s$ of $\theta$ with derivative $p'_t(x)$ , and an integrable bound on $|p'_t|$ uniform over $t \in s$ .

Formalization Note As in the general identity, the parameter derivative is supplied explicitly as p' through HasDerivAt, while the conclusion is stated with deriv (fun t => Real.log (p t x)) θ so that the score appears as a logarithmic derivative. This statement is the $f \equiv 1$ specialization of the measure-theoretic log-derivative trick combined with the normalization hypothesis.

Preamble

import Mathlib.Analysis.Calculus.ParametricIntegral
import Mathlib.Analysis.SpecialFunctions.Log.Deriv

open MeasureTheory Filter
open scoped Topology

Formal statement

namespace ScoreFunction
theorem score_zero_mean
    {X : Type*} [MeasurableSpace X] {μ : Measure X}
    {p p' : ℝ → X → ℝ} {bound : X → ℝ} {θ : ℝ} {s : Set ℝ}
    (hs : s ∈ 𝓝 θ)
    (hp_pos : ∀ᵐ x ∂μ, 0 < p θ x)
    (hp_meas : ∀ᶠ t in 𝓝 θ, AEStronglyMeasurable (p t) μ)
    (hp_int : Integrable (p θ) μ)
    (hp'_meas : AEStronglyMeasurable (p' θ) μ)
    (h_bound : ∀ᵐ x ∂μ, ∀ t ∈ s, |p' t x| ≤ bound x)
    (h_bound_int : Integrable bound μ)
    (h_diff : ∀ᵐ x ∂μ, ∀ t ∈ s, HasDerivAt (fun u => p u x) (p' t x) t)
    (h_norm : ∀ t ∈ s, ∫ x, p t x ∂μ = 1) :
    ∫ x, p θ x * deriv (fun t => Real.log (p t x)) θ ∂μ = 0 := by sorry
end ScoreFunction

Source

Measure-theoretic (continuous) form of the score-function / likelihood-ratio gradient identity, a.k.a. the log-derivative trick. Identity as stated in A. C. Jones, 'The log-derivative trick', https://andrewcharlesjones.github.io/journal/log-derivative.html : grad_theta E_{p(x;theta)}[f(x)] = E_{p(x;theta)}[grad_theta log p(x;theta) * f(x)]. Standard references: P. W. Glynn, 'Likelihood ratio gradient estimation for stochastic systems', Communications of the ACM 33(10):75-84, 1990, https://doi.org/10.1145/84537.84552 ; S. Mohamed, M. Rosca, M. Figurnov, A. Mnih, 'Monte Carlo Gradient Estimation in Machine Learning', JMLR 21(132):1-62, 2020, https://arxiv.org/abs/1906.10652 (score-function estimators). The interchange-of-derivative-and-integral hypotheses are the standard dominated-derivative conditions, matching Mathlib's hasDerivAt_integral_of_dominated_loc_of_deriv_le. Discrete counterparts already on Prove2Me: likelihood_ratio_gradient and score_zero_mean (R. J. Williams, Machine Learning 8, 1992, REINFORCE).

View graph

The score function has zero mean: ∫pθ ∂θlog⁡pθ dμ=0\int p_\theta \, \partial_\theta \log p_\theta \, d\mu = 0∫pθ​∂θ​logpθ​dμ=0

The score function has zero mean: $\int p_\theta \, \partial_\theta \log p_\theta \, d\mu = 0$