Rate of convergence of the averaging dynamics

Theorem 33 of Becchetti, Clementi, Natale, Consensus Dynamics: An Overview, SIGACT News 51(1), 2020 (the Survey), Section 7.2, which is Theorem 5.1 of Lovász, Random walks on graphs: a survey, 1993. For the random walk P = D⁻¹A with stationary distribution π(v) = d(v) / 2m and λ = max {|λ₂(P)|, |λₙ(P)|}, |Pᵗ(u, v) - π(v)| ≤ √(d(v) / d(u)) λᵗ for all nodes u, v and times t (the Survey prints √(d(v) / d(v)), a typo). Unless G is bipartite, λ < 1, so the averaging dynamics x⁽ᵗ⁾ = Pᵗ x⁽⁰⁾ converges exponentially fast to ∑ π(v) x⁽⁰⁾(v) at every node.

The bridges walkMatrix_pow_apply and avgIter_eq_walkMatrix_pow_mulVec identify Pᵗ with the t-step transition probabilities transW and the averaging dynamics avgIter of Averaging.Basic; charpoly_walkMatrix shows that walkLambda is computed from the spectrum of P.

theorem Averaging.walkMatrix_pow_apply {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (t : ℕ) (u v : V) : (walkMatrix G ^ t) u v = transW G t u v

Pᵗ(u, v) is the probability that the random walk started at u is at v after t steps (Survey, Section 7.2, before Theorem 33).

theorem Averaging.avgIter_eq_walkMatrix_pow_mulVec {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (t : ℕ) (x : V → ℝ) : avgIter G t x = (walkMatrix G ^ t).mulVec x

A round of the averaging dynamics applies P (Survey, Section 7.2): x⁽ᵗ⁾ = P x⁽ᵗ⁻¹⁾ = ⋯ = Pᵗ x⁽⁰⁾.

theorem Averaging.charpoly_walkMatrix {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hdeg : ∀ (v : V), 0 < G.degree v) : (walkMatrix G).charpoly = (normAdjMatrix G).charpoly

P = D⁻¹A and N = D^{-1/2} A D^{-1/2} have the same characteristic polynomial when every degree is positive. Hence the eigenvalues of P with multiplicity, sorted decreasingly, are eigenvalues₀ of N (Matrix.IsHermitian.sort_roots_charpoly_eq_eigenvalues₀), and walkLambda is the λ of Theorem 33.

theorem Averaging.abs_walkMatrix_pow_sub_walkStationary_le {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hdeg : ∀ (v : V), 0 < G.degree v) (u v : V) (t : ℕ) : |(walkMatrix G ^ t) u v - walkStationary G v| ≤ √(↑(G.degree v) / ↑(G.degree u)) * walkLambda G ^ t

Theorem 33 (Survey; Lovász 1993, Theorem 5.1). Let λ = max {|λ₂(P)|, |λₙ(P)|}. For every u, v ∈ V and every t ≥ 0, |Pᵗ(u, v) - π(v)| ≤ √(d(v) / d(u)) λᵗ.

theorem Averaging.walkLambda_lt_one {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hc : G.Connected) (hodd : ∃ (u : V) (p : G.Walk u u), Odd p.length) : walkLambda G < 1

Unless G is bipartite, λ < 1 (Survey, after Theorem 33): on a connected graph with a closed walk of odd length, λ < 1.

theorem Averaging.abs_avgIter_sub_walkStationary_le {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hdeg : ∀ (v : V), 0 < G.degree v) (x : V → ℝ) (u : V) (t : ℕ) : |avgIter G t x u - ∑ v : V, walkStationary G v * x v| ≤ walkLambda G ^ t * ∑ v : V, √(↑(G.degree v) / ↑(G.degree u)) * |x v|

Theorem 33 for the averaging dynamics: the value of node u after t rounds is within λᵗ ∑ᵥ √(d(v) / d(u)) |x(v)| of the stationary average ∑ᵥ π(v) x(v) of the initial values (Survey, Section 7.2: Pᵗx → (∑ᵥ π(v) x(v)) 𝟙).