Log-derivative trick: $\frac{d}{d\theta}\int f p_\theta \, d\mu = \int f p_\theta \, \partial_\theta \log p_\theta \, d\mu$

Proved

ScoreFunction.likelihood_ratio_gradient

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

analysiscalculusinformation-geometrymachine-learningmeasure-theorypolicy-gradientprobabilityreinforcement-learning

This is the log-derivative trick (also called the score-function or likelihood-ratio gradient identity) in its measure-theoretic form: the continuous analogue of the finite-sum identity likelihood_ratio_gradient already on the platform.

Let $(\mathcal X,\mathcal A,\mu)$ be a measure space and let $p_\theta : \mathcal X \to \mathbb R$ be a family of densities with respect to $\mu$ , indexed by a real parameter $\theta$ . For an observable $f : \mathcal X \to \mathbb R$ , write

\mathbb E_{p_\theta}[f] \;=\; \int_{\mathcal X} f(x)\, p_\theta(x)\, d\mu(x).

Then, under the interchange conditions listed below,

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

The right-hand side is again an expectation under $p_\theta$ itself, which is what makes the derivative estimable by Monte Carlo from samples of $p_\theta$ ; the intermediate quantity $\partial_\theta p_\theta$ is in general not a density, so it cannot be sampled directly. This is the identity behind the REINFORCE and policy-gradient estimators in reinforcement learning, the score-function gradient estimator for variational objectives, and likelihood-ratio sensitivity analysis in stochastic simulation.

The hypotheses are the standard dominated-derivative conditions for differentiating under the integral sign, stated on a neighbourhood $s$ of the base point $\theta$ :

$p_\theta > 0$ $\mu$ -almost everywhere, so that $\log p_\theta$ is defined a.e.;
$x \mapsto f(x)\,p_t(x)$ is almost-everywhere strongly measurable for every $t$ near $\theta$ , and integrable at $t=\theta$ , so that $\mathbb E_{p_\theta}[f]$ exists;
for almost every $x$ , the map $t \mapsto p_t(x)$ is differentiable at every $t \in s$ with derivative $p'_t(x)$ ;
the family of derivatives is dominated: $|f(x)\,p'_t(x)| \le \mathrm{bound}(x)$ for almost every $x$ and all $t \in s$ , with $\mathrm{bound}$ integrable.

Normalization of $p_\theta$ is deliberately not assumed: the identity is a statement about differentiating a weighted integral and holds for any positive weight family. The normalized case, in which the score has mean zero, is a separate statement.

Formalization Note The derivative family is supplied explicitly as p' via HasDerivAt (fun u => p u x) (p' t x) t rather than through deriv, which avoids the junk value deriv takes at points of non-differentiability. The conclusion is nevertheless phrased with deriv (fun t => Real.log (p t x)) θ, so the score appears literally as a logarithmic derivative. bound and the neighbourhood s are explicit parameters; taking s ∈ 𝓝 θ rather than a ball keeps the statement independent of the metric. The hypotheses line up one-for-one with Mathlib's hasDerivAt_integral_of_dominated_loc_of_deriv_le.

Preamble

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

open MeasureTheory Filter
open scoped Topology

Formal statement

namespace ScoreFunction
theorem likelihood_ratio_gradient
    {X : Type*} [MeasurableSpace X] {μ : Measure X}
    {p p' : ℝ → X → ℝ} {f bound : X → ℝ} {θ : ℝ} {s : Set ℝ}
    (hs : s ∈ 𝓝 θ)
    (hp_pos : ∀ᵐ x ∂μ, 0 < p θ x)
    (hF_meas : ∀ᶠ t in 𝓝 θ, AEStronglyMeasurable (fun x => f x * p t x) μ)
    (hF_int : Integrable (fun x => f x * p θ x) μ)
    (hF'_meas : AEStronglyMeasurable (fun x => f x * p' θ x) μ)
    (h_bound : ∀ᵐ x ∂μ, ∀ t ∈ s, |f x * 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) :
    deriv (fun t => ∫ x, f x * p t x ∂μ) θ
      = ∫ x, f x * p θ x * deriv (fun t => Real.log (p t x)) θ ∂μ := 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

Log-derivative trick: ddθ∫fpθ dμ=∫fpθ ∂θlog⁡pθ dμ\frac{d}{d\theta}\int f p_\theta \, d\mu = \int f p_\theta \, \partial_\theta \log p_\theta \, d\mudθd​∫fpθ​dμ=∫fpθ​∂θ​logpθ​dμ

Log-derivative trick: $\frac{d}{d\theta}\int f p_\theta \, d\mu = \int f p_\theta \, \partial_\theta \log p_\theta \, d\mu$