Mixing times of Markov chains

AbbreviationDiscrete torus#✓fully proved

For natural numbers \(d\) and \(n\), the vertices of the discrete torus \(\mathbb{Z}_n^d\) are the functions from \(\{0, \dots, d-1\}\) to \(\{0, \dots, n-1\}\), that is, the \(d\)-tuples of residues modulo \(n\).

abbrev Torus (d n : ℕ) := Fin d → Fin n

Used by 1

Used byCoordinate step on the discrete torus

DefinitionCoordinate step on the discrete torus#✓fully proved

For a vertex \(x\) of the discrete torus \(\mathbb{Z}_n^d\) and a coordinate \(k \in \{0, \dots, d-1\}\), the neighbour \(x + e_k\) is obtained from \(x\) by replacing its \(k\)-th coordinate \(x_k\) by \((x_k + 1) \bmod n\) and leaving the other coordinates unchanged.

def stepUp {d n : ℕ} (k : Fin d) (x : Torus d n) : Torus d n :=
  Function.update x k ⟨((x k).val + 1) % n, Nat.mod_lt _ (Nat.zero_lt_of_lt (x k).2)⟩

Uses 1

Statement usesDiscrete torus

DefinitionSign of a Boolean spin#✓fully proved

The sign of a Boolean spin is the real number \(+1\) if the spin is true and \(-1\) if it is false.

noncomputable def sgn (b : Bool) : ℝ := if b then 1 else -1

DefinitionTotal variation distance of functions on a finite set#✓fully proved

For real-valued functions \(\mu\) and \(\nu\) on a finite set \(S\), their total variation distance is \(\frac{1}{2} \sum_{y \in S} |\mu(y) - \nu(y)|\).

noncomputable def tvDist {S : Type*} [Fintype S] (μ ν : S → ℝ) : ℝ :=
  (1 / 2) * ∑ y, |μ y - ν y|

Used by 6

Used byThe systematic-scan Gibbs sampler converges to its target · The Metropolis–Hastings chain converges to its target · The convergence theorem · Convergence of matrix powers to the stationary distribution · Doeblin's argument · Being \(1/4\)-mixed at a given time

DefinitionTotal variation distance of a matrix row from a function#✓fully proved

For a real \(S \times S\) matrix \(Q\) indexed by a finite set \(S\), a function \(\pi : S \to \mathbb{R}\) and \(x \in S\), this is the total variation distance \(\frac{1}{2} \sum_{y \in S} |Q(x, y) - \pi(y)|\) of the row \(x\) of \(Q\) from \(\pi\).

noncomputable def tvRow {S : Type*} [Fintype S] (Q : Matrix S S ℝ) (π : S → ℝ) (x : S) : ℝ :=
  (1 / 2) * ∑ y, |Q x y - π y|

DefinitionBeing \(1/4\)-mixed at a given time#✓fully proved

Let \(S\) be a finite set, \(P\) a real \(S \times S\) matrix and \(\pi : S \to \mathbb{R}\). Then \(P\) is mixed at time \(t \in \mathbb{N}\) with respect to \(\pi\) if for every \(x \in S\) the total variation distance \(\frac{1}{2} \sum_{y \in S} |P^t(x, y) - \pi(y)|\) between the row \(x\) of the matrix power \(P^t\) and \(\pi\) is at most \(1/4\).

The mixing time is the least \(t\) at which \(P\) is mixed.

def IsMixedAt {S : Type*} [Fintype S] [DecidableEq S] (P : Matrix S S ℝ) (π : S → ℝ)
    (t : ℕ) : Prop :=
  ∀ x, tvDist (fun y => (P ^ t) x y) π ≤ 1 / 4

Uses 1

Statement usesTotal variation distance of functions on a finite set

DefinitionNumber of monochromatic edges#✓fully proved

For a simple graph \(G\) on the vertex set \(\{0, \dots, n-1\}\) and a colouring \(\sigma\) of its vertices with colours in \(\{0, \dots, q-1\}\), this is the number of edges \(uv\) of \(G\) with \(\sigma_u = \sigma_v\), as a real number, each edge counted once.

noncomputable def monoEdges {n q : ℕ} (G : SimpleGraph (Fin n)) (σ : Fin n → Fin q) : ℝ :=
  (1 / 2) * ∑ u, ∑ v, if G.Adj u v ∧ σ u = σ v then 1 else 0

DefinitionCutoff for a family of distance profiles#✓fully proved

A family of real numbers \(d_n(t)\), indexed by \(n \in \mathbb{N}\) and times \(t \in \mathbb{N}\), exhibits cutoff if there are real numbers \(t_n\) with \(t_n \to \infty\) such that for every \(\eta\) with \(0 < \eta < 1\), as \(n \to \infty\), \(d_n(\lceil (1+\eta) t_n \rceil) \to 0\) and \(d_n(\lfloor (1-\eta) t_n \rfloor) \to 1\). Here the ceiling and floor are taken in \(\mathbb{N}\), so a negative argument gives \(0\).

def HasCutoff (d : ℕ → ℕ → ℝ) : Prop :=
  ∃ t : ℕ → ℝ, Filter.Tendsto t Filter.atTop Filter.atTop ∧ ∀ η : ℝ, 0 < η → η < 1 →
    Filter.Tendsto (fun n => d n ⌈(1 + η) * t n⌉₊) Filter.atTop (nhds 0) ∧
      Filter.Tendsto (fun n => d n ⌊(1 - η) * t n⌋₊) Filter.atTop (nhds 1)

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.