from a total-variation rate (Jones Thm 2(ii))
ProvedMarkovChainCLT.alpha_mixing_le_tv_rateLet be a Markov chain with transition kernel , Harris ergodic with invariant probability , and suppose the total-variation rate bound holds for all and all , where is integrable with respect to and . Then the strong mixing coefficients of the stationary chain satisfy
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 ; the sharp inequality stated here is what its derivation gives.
Formalization Note "Harris ergodic" is encoded by its total-variation characterization: is invariant for and for every starting point (equivalent to the classical aperiodic, -irreducible, positive Harris recurrent definition; the "every " quantifier is exactly the Harris property). Convergence in distribution is weak convergence of laws, and is read as the point mass at , which absorbs the source's "" caveat.
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))`). -/
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