The random-walk matrix and its symmetrization: entries and similarity

Helpers for the rate bound (Survey, Section 7.2, Theorem 33): the entries of P = D⁻¹A, the identification of Pᵗ with the t-step transition probabilities transW and of the averaging dynamics with Pᵗ x, and the similarity P = D^{-1/2} N D^{1/2} with N = D^{-1/2} A D^{-1/2} when every degree is positive.

theorem Averaging.walkMatrix_apply {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (u v : V) : walkMatrix G u v = if G.Adj u v then (↑(G.degree u))⁻¹ else 0

The entries of P = D⁻¹A: P u v = 1 / d(u) if u ~ v, 0 otherwise.

theorem Averaging.walkMatrix_pow_apply_eq_transW {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 t-step transition probability transW G t u v.

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

The averaging dynamics is x⁽ᵗ⁾ = Pᵗ x⁽⁰⁾.

theorem Averaging.normAdjMatrix_apply {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (u v : V) : normAdjMatrix G u v = if G.Adj u v then (√↑(G.degree u))⁻¹ * (√↑(G.degree v))⁻¹ else 0

The entries of N = D^{-1/2} A D^{-1/2}.

theorem Averaging.diagonal_sqrt_mul_inv {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hdeg : ∀ (v : V), 0 < G.degree v) : ((Matrix.diagonal fun (v : V) => √↑(G.degree v)) * Matrix.diagonal fun (v : V) => (√↑(G.degree v))⁻¹) = 1

D^{1/2} D^{-1/2} = I when every degree is positive.

theorem Averaging.walkMatrix_eq_conj {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hdeg : ∀ (v : V), 0 < G.degree v) : walkMatrix G = (Matrix.diagonal fun (v : V) => (√↑(G.degree v))⁻¹) * normAdjMatrix G * Matrix.diagonal fun (v : V) => √↑(G.degree v)

P = D^{-1/2} N D^{1/2} when every degree is positive.

theorem Averaging.walkMatrix_pow_eq {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hdeg : ∀ (v : V), 0 < G.degree v) (t : ℕ) : walkMatrix G ^ t = (Matrix.diagonal fun (v : V) => (√↑(G.degree v))⁻¹) * normAdjMatrix G ^ t * Matrix.diagonal fun (v : V) => √↑(G.degree v)

Pᵗ = D^{-1/2} Nᵗ D^{1/2} when every degree is positive.

theorem Averaging.walkMatrix_pow_apply_eq {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hdeg : ∀ (v : V), 0 < G.degree v) (t : ℕ) (u v : V) : (walkMatrix G ^ t) u v = (√↑(G.degree u))⁻¹ * (normAdjMatrix G ^ t) u v * √↑(G.degree v)

The entries of Pᵗ through Nᵗ: Pᵗ(u, v) = d(u)^{-1/2} Nᵗ(u, v) d(v)^{1/2}.

theorem Averaging.charpoly_walkMatrix_eq {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 and N have the same characteristic polynomial when every degree is positive.