Rate of convergence of the averaging dynamics: definitions

Definitions for the rate bound of roadmap AVG-1: Becchetti, Clementi, Natale, Consensus Dynamics: An Overview, SIGACT News 51(1), 2020 (the Survey), Section 7.2, Theorem 33, which cites Lovász, Random walks on graphs: a survey, 1993, Theorem 5.1.

• walkMatrix: the transition matrix P = D⁻¹A of the random walk (Survey, footnote 24);
• normAdjMatrix: the symmetric matrix N = D^{-1/2} A D^{-1/2}, similar to P (charpoly_walkMatrix), so that P and N have the same eigenvalues;
• walkLambda: λ = max {|λ₂(P)|, |λₙ(P)|} (Theorem 33), read off Mathlib's decreasingly sorted spectrum Matrix.IsHermitian.eigenvalues₀ of N;
• walkStationary: the stationary distribution π(v) = d(v) / 2m (Theorem 32).

The values after t rounds are avgIter G t x (Averaging.Basic) and the t-step transition probabilities transW G t u v.

noncomputable def Averaging.walkMatrix {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : Matrix V V ℝ

The transition matrix P = D⁻¹A of the random walk on G (Survey, footnote 24): P u v = 1 / d(u) if u ~ v and 0 otherwise (the row of an isolated node is zero).

Equations

• Averaging.walkMatrix G = (Matrix.diagonal fun (v : V) => (↑(G.degree v))⁻¹) * SimpleGraph.adjMatrix ℝ G

noncomputable def Averaging.normAdjMatrix {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : Matrix V V ℝ

The normalized adjacency matrix N = D^{-1/2} A D^{-1/2}. When every degree is positive, P = D^{-1/2} N D^{1/2}, so P and N have the same eigenvalues (charpoly_walkMatrix).

Equations

• Averaging.normAdjMatrix G = (Matrix.diagonal fun (v : V) => (√↑(G.degree v))⁻¹) * SimpleGraph.adjMatrix ℝ G * Matrix.diagonal fun (v : V) => (√↑(G.degree v))⁻¹

theorem Averaging.normAdjMatrix_isHermitian {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : (normAdjMatrix G).IsHermitian

N = D^{-1/2} A D^{-1/2} is real symmetric.

noncomputable def Averaging.walkLambda {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : ℝ

λ of Theorem 33: λ = max {|λ₂(P)|, |λₙ(P)|}, where λ₁ ≥ λ₂ ≥ ⋯ ≥ λₙ are the eigenvalues of P = D⁻¹A, listed in decreasing order with multiplicity. They are computed as the eigenvalues of the similar symmetric matrix N = D^{-1/2} A D^{-1/2} (charpoly_walkMatrix), with Mathlib's Matrix.IsHermitian.eigenvalues₀, which is indexed from 0 (so λ₂ has index 1 and λₙ index n - 1). By convention λ = 0 when n < 2.

Equations

• Averaging.walkLambda G = if h : 2 ≤ Fintype.card V then max |⋯.eigenvalues₀ ⟨1, ⋯⟩| |⋯.eigenvalues₀ ⟨Fintype.card V - 1, ⋯⟩| else 0

noncomputable def Averaging.walkStationary {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) : ℝ

The stationary distribution π(v) = d(v) / 2m of the random walk on G, where m is the number of edges (Survey, Theorem 32).

Equations

• Averaging.walkStationary G v = ↑(G.degree v) / (2 * ↑G.edgeFinset.card)