Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

α(n)≤γ(n) EπM\alpha(n) \le \gamma(n)\, E_\pi Mα(n)≤γ(n)Eπ​M from a total-variation rate (Jones Thm 2(ii))

Proved
MarkovChainCLT.alpha_mixing_le_tv_rate

by Shuze Chen · 1 vote · Aug 15, 2026 · Mathlib 0df444a (Lean v4.33.1)

markov-chainsmcmcmixing-processesprobability

Let XXX be a Markov chain with transition kernel PPP, Harris ergodic with invariant probability π\piπ, and suppose the total-variation rate bound ∥Pn(x,⋅)−π∥≤M(x) γ(n)\|P^n(x, \cdot) - \pi\| \le M(x)\, \gamma(n)∥Pn(x,⋅)−π∥≤M(x)γ(n) holds for all xxx and all n≥1n \ge 1n≥1, where M≥0M \ge 0M≥0 is integrable with respect to π\piπ and γ≥0\gamma \ge 0γ≥0. Then the strong mixing coefficients of the stationary chain satisfy

α(n)  ≤  γ(n)∫M dπ(n≥1).\alpha(n) \;\le\; \gamma(n) \int M \, d\pi \qquad (n \ge 1).α(n)≤γ(n)∫Mdπ(n≥1).

This quantitative bound turns any total-variation convergence rate (geometric, polynomial, …) into a mixing rate, and is the step through which the corollaries of the mission consume the classical sequence CLTs. The source records the consequence α(n)=O(γ(n))\alpha(n) = O(\gamma(n))α(n)=O(γ(n)); the sharp inequality stated here is what its derivation gives.

Formalization Note "Harris ergodic" is encoded by its total-variation characterization: π\piπ is invariant for PPP and ∥Pn(x,⋅)−π∥→0\|P^n(x, \cdot) - \pi\| \to 0∥Pn(x,⋅)−π∥→0 for every starting point xxx (equivalent to the classical aperiodic, ψ\psiψ-irreducible, positive Harris recurrent definition; the "every xxx" quantifier is exactly the Harris property). Convergence in distribution is weak convergence of laws, and N(0,0)N(0, 0)N(0,0) is read as the point mass at 000, which absorbs the source's "σf2>0\sigma_f^2 > 0σf2​>0" caveat.

Preamble
import Definitions.Def_MarkovErgodicity
import Definitions.Def_MarkovChainPathMeasure
import Definitions.Def_MixingCoefficients

open MeasureTheory ProbabilityTheory Filter
open scoped ENNReal NNReal Topology ProbabilityTheory

/-- **Theorem 2, part 2**: if the chain has total-variation rate `γ` with constant
`M` and `E_π M < ∞`, then the strong mixing coefficients of the stationary chain
satisfy `α(n) ≤ γ(n) E_π M` for all `n ≥ 1` (Jones 2004, §3; the paper states the
consequence `α(n) = O(γ(n))`). -/
Formal statement
theorem MarkovChainCLT.alpha_mixing_le_tv_rate {X : Type*} [MeasurableSpace X]
    (P : Kernel X X) [IsMarkovKernel P] (π : Measure X) [IsProbabilityMeasure π]
    (hP : HarrisErgodic P π)
    (M : X → ℝ) (hM0 : ∀ x, 0 ≤ M x) (hM : Integrable M π)
    (γ : ℕ → ℝ) (hγ0 : ∀ n, 0 ≤ γ n) (hrate : ErgodicWithRate P π M γ) :
    ∀ n : ℕ, 1 ≤ n →
      alphaMixingCoef (chainMeasure P π) (fun i ω => ω i) n ≤ γ n * ∫ x, M x ∂π := by sorry
Source
G. L. Jones, "On the Markov Chain Central Limit Theorem", Probability Surveys 1 (2004) 299-320, arXiv math/0409112v2, Theorem 2, part 2 (arXiv v2 p. 8; Section 3 derivation via the coupling inequality, eq. (7))

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me