Theorem 33: the rate bound

Proof of Theorem 33 of the Survey (Lovász 1993, Theorem 5.1) for a graph without isolated nodes. The vector s = √π is a unit eigenvector of N = D^{-1/2} A D^{-1/2} for the eigenvalue 1; the quadratic form of N is bounded by the squared norm (|ab| ≤ (a² + b²)/2 on every edge), so every eigenvalue has |μ| ≤ 1; by the sorting of eigenvalues₀, at most one eigenvalue (the largest) has |μ| > λ. The spectral lemmas of Averaging.RateSpectral then give |Nᵗ(u, v) - s(u) s(v)| ≤ λᵗ, and Pᵗ = D^{-1/2} Nᵗ D^{1/2} turns this into |Pᵗ(u, v) - π(v)| ≤ √(d(v)/d(u)) λᵗ.

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

The vector s = √π, a unit eigenvector of N for the eigenvalue 1.

Equations

• Averaging.sqrtStationary G v = √(Averaging.walkStationary G v)

theorem Averaging.card_edgeFinset_pos {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hdeg : ∀ (v : V), 0 < G.degree v) [Nonempty V] : 0 < G.edgeFinset.card

A graph without isolated nodes on a nonempty vertex type has an edge.

theorem Averaging.two_le_card {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hdeg : ∀ (v : V), 0 < G.degree v) [Nonempty V] : 2 ≤ Fintype.card V

A graph without isolated nodes on a nonempty vertex type has at least two nodes.

theorem Averaging.sum_walkStationary {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hdeg : ∀ (v : V), 0 < G.degree v) [Nonempty V] : ∑ v : V, walkStationary G v = 1

π is a probability vector.

theorem Averaging.walkStationary_nonneg {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) : 0 ≤ walkStationary G v

theorem Averaging.sqrtStationary_dotProduct_self {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hdeg : ∀ (v : V), 0 < G.degree v) [Nonempty V] : sqrtStationary G ⬝ᵥ sqrtStationary G = 1

s = √π is a unit vector.

theorem Averaging.sqrtStationary_eq {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) : sqrtStationary G v = √↑(G.degree v) / √(2 * ↑G.edgeFinset.card)

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

N s = s.

theorem Averaging.abs_mul_normAdj_le {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hdeg : ∀ (v : V), 0 < G.degree v) (w : V → ℝ) (u v : V) : |w u * normAdjMatrix G u v * w v| ≤ if G.Adj u v then (w u ^ 2 / ↑(G.degree u) + w v ^ 2 / ↑(G.degree v)) / 2 else 0

On one edge: |w(u) w(v)| / √(d(u) d(v)) ≤ (w(u)²/d(u) + w(v)²/d(v)) / 2.

theorem Averaging.abs_dotProduct_normAdjMatrix_mulVec_le {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hdeg : ∀ (v : V), 0 < G.degree v) (w : V → ℝ) : |w ⬝ᵥ (normAdjMatrix G).mulVec w| ≤ w ⬝ᵥ w

The quadratic form of N is bounded by the squared norm: |w ⬝ N w| ≤ w ⬝ w.

theorem Averaging.walkLambda_nonneg {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : 0 ≤ walkLambda G

λ ≥ 0.

theorem Averaging.abs_eigenvalues₀_le_walkLambda {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (h2 : 2 ≤ Fintype.card V) (i : Fin (Fintype.card V)) (hi : i ≠ ⟨0, ⋯⟩) : |⋯.eigenvalues₀ i| ≤ walkLambda G

Every sorted eigenvalue but the largest is at most λ in absolute value.

theorem Averaging.eq_of_walkLambda_lt_abs {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hdeg : ∀ (v : V), 0 < G.degree v) [Nonempty V] (k l : V) (hk : walkLambda G < |⋯.eigenvalues k|) (hl : walkLambda G < |⋯.eigenvalues l|) : k = l

At most one eigenvalue of N exceeds λ in absolute value.

theorem Averaging.walkStationary_eq_sqrt {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hdeg : ∀ (v : V), 0 < G.degree v) (u v : V) : walkStationary G v = (√↑(G.degree u))⁻¹ * (sqrtStationary G u * sqrtStationary G v) * √↑(G.degree v)

π(v) through s = √π: π(v) = d(u)^{-1/2} s(u) s(v) d(v)^{1/2}.

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), for a graph without isolated nodes.