Prove2Me

Variance of ∑i=1nf(Xi)\sum_{i=1}^n f(X_i) for a stationary reversible chain, stated through ⟨f,Hif⟩\langle f, H^i f\rangle

Proved
TierneyMH.Peskun.variance_identity

by mikedeng1 · Sep 29, 2026 · Mathlib 0df444a (Lean v4.33.1)

markov-chainsmcmcp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1probability

Let π\pi be a probability measure on a measurable space EE, let HH be a Markov kernel reversible with respect to π\pi, and let f∈L02(π)f \in L^2_0(\pi). Let X0,X1,…X_0, X_1, \dots be the Markov chain with initial distribution π\pi and transition kernel HH. Then for every n≥1n \ge 1,

1nVar⁡H(∑i=1nf(Xi))  =  ⟨f,f⟩+2∑i=1nn−in ⟨f,Hif⟩,\frac{1}{n}\operatorname{Var}_H\Bigl(\sum_{i=1}^{n} f(X_i)\Bigr) \;=\; \langle f, f\rangle + 2\sum_{i=1}^{n} \frac{n-i}{n}\,\langle f, H^{i} f\rangle ,

where ⟨f,Hif⟩=∫f(x)∫f(y) Hi(x,dy) π(dx)\langle f, H^i f\rangle = \int f(x)\int f(y)\,H^i(x,dy)\,\pi(dx).

The paper writes the right-hand side as ∫(1+2∑i=1nn−inxi) ef,H(dx)\int \bigl(1 + 2\sum_{i=1}^n \frac{n-i}{n} x^i\bigr)\, e_{f,H}(dx), where ef,He_{f,H} is the spectral measure of ff with ⟨f,Hif⟩=∫xi ef,H(dx)\langle f, H^i f\rangle = \int x^i\, e_{f,H}(dx); this is the finite-nn step from which the limit ∫1+x1−x ef,H(dx)\int \frac{1+x}{1-x}\,e_{f,H}(dx) is read off.

Formalization Note The right-hand side is stated through the moments ⟨f,Hif⟩\langle f, H^i f\rangle instead of the spectral measure ef,He_{f,H} (Mathlib has no spectral measure of a self-adjoint operator); substituting the moments into the paper's integrand gives exactly this expression. The variance is Mathlib's real variance (the real part of the extended variance, finite here), and the weights (n−i)/n(n-i)/n are computed in R\mathbb R.

Preamble
import Mathlib
import Definitions.Def_TierneyMH_Peskun_chainMeasure
import Definitions.Def_TierneyMH_Peskun_lagInner

open MeasureTheory ProbabilityTheory
Formal statement
namespace TierneyMH.Peskun

/-- **Proof of Theorem 4** (Tierney 1998, p. 5, the display), stated through `⟨f, Hⁱ f⟩`.
Let `H` be a reversible Markov kernel with invariant distribution `π`, let `f ∈ L²₀(π)`, and let
`X₀, X₁, …` be the Markov chain with initial distribution `π` and kernel `H`
(`chainMeasure π H`). For every `n ≥ 1`,
`(1/n) Var_H(∑_{i=1}^{n} f(X_i)) = ⟨f, f⟩ + 2 ∑_{i=1}^{n} ((n − i)/n) ⟨f, Hⁱ f⟩`.
The paper writes the right side as `∫ (1 + 2 ∑ ((n−i)/n) xⁱ) e_{f,H}(dx)` through the spectral
measure `e_{f,H}` with `⟨f, Hⁱ f⟩ = ∫ xⁱ e_{f,H}(dx)`; the moment form here is that right side
with the moments substituted (Mathlib has no spectral measure of a self-adjoint operator).
The weights are computed in `ℝ` (`((n : ℝ) − i) / n`), not with truncated `ℕ` subtraction. -/
theorem variance_identity {E : Type*} [MeasurableSpace E]
    (π : Measure E) [IsProbabilityMeasure π]
    (H : Kernel E E) [IsMarkovKernel H] (hH : Kernel.IsReversible H π)
    (f : E → ℝ) (hf_meas : Measurable f) (hf : MemLp f 2 π) (hf0 : ∫ x, f x ∂π = 0)
    (n : ℕ) (hn : 1 ≤ n) :
    variance (pathSum f n) (chainMeasure π H) / n =
      ∫ x, f x ^ 2 ∂π +
        2 * ∑ i ∈ Finset.Icc 1 n, (((n : ℝ) - i) / n) * lagInner π H f i := by sorry

end TierneyMH.Peskun
Source
L. Tierney, A Note on Metropolis–Hastings Kernels for General State Spaces, Ann. Appl. Probab. 8(1) (1998) 1–9, DOI 10.1214/aoap/1027961031, p. 5, proof of Theorem 4 (displayed identity for (1/n) Var_H)
Human review

  • Endorsed by Shuze Chen · Oct 1, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 1, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph