Mixing bounds from path coupling
ProvedMarkovMixing.path_coupling_mixingmarkov-chainsmixing-timesprobability
Let be a Markov chain on a finite state space with stationary distribution , and suppose the path coupling hypotheses of Theorem 14.6 hold: a connected graph on with symmetric edge lengths , a rate , and for every edge of a coupling of contracting the path metric (least total -length of a connecting walk) in expectation by . Write for the path-metric diameter, for the total variation distance, , and .
The theorem (Corollary 14.7 of Levin–Peres–Wilmer) asserts:
- the distance to stationarity decays geometrically: for every ;
- consequently, for every , .
The proof is one line from path coupling: iterating the one-step contraction bounds by , and the transportation distance dominates total variation because the path metric is at least between distinct states.
Preamble
import Definitions.Def_mm_transport import Mathlib.Analysis.SpecialFunctions.Log.Basic
Formal statement
namespace MarkovMixing
/-- **Corollary 14.7** (LPW): under the path coupling hypotheses,
`d(t) ≤ e^{-αt} diam(Ω)` and
`t_mix(ε) ≤ ⌈(−log ε + log diam(Ω))/α⌉`. -/
theorem path_coupling_mixing {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V]
(P : Matrix V V ℝ) (hP : IsStochastic P)
(π : V → ℝ) (hπ : IsStationary P π)
(G : SimpleGraph V) (hconn : G.Connected)
(ℓ : V → V → ℝ) (hℓ1 : ∀ x y : V, G.Adj x y → 1 ≤ ℓ x y)
(hℓsymm : ∀ x y : V, ℓ x y = ℓ y x)
(α : ℝ) (hα : 0 < α)
(hedge : ∀ x y : V, G.Adj x y →
∃ q : V × V → ℝ, IsCoupling (rowDist P 1 x) (rowDist P 1 y) q ∧
∑ p : V × V, q p * pathMetric G ℓ p.1 p.2 ≤ Real.exp (-α) * ℓ x y) :
(∀ t : ℕ, distStationary P π t ≤
Real.exp (-α * t) * ⨆ p : V × V, pathMetric G ℓ p.1 p.2) ∧
∀ ε : ℝ, 0 < ε → ε < 1 →
(mixingTime P π ε : ℝ) ≤
⌈(-Real.log ε + Real.log (⨆ p : V × V, pathMetric G ℓ p.1 p.2)) / α⌉₊ := by
sorry
end MarkovMixingSource
D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, AMS 2009, https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf, Section 14.2, Corollary 14.7, p. 192