Spectral theory of the walk operator on regular graphs

The walk operator G.walk of a regular multigraph G is self-adjoint for the uniform inner product 𝔼 v, f v * g v, and therefore defines a symmetric linear endomorphism G.walkEuclidean on EuclideanSpace ℝ V (isSymmetric_walkEuclidean). It preserves the subspace orthogonalSubmodule V of functions orthogonal to the constants—equivalently, of expectation zero (mem_orthogonalSubmodule_iff)—and restricts to a symmetric endomorphism G.orthogonalWalk on that subspace (isSymmetric_orthogonalWalk).

By the finite-dimensional spectral theorem (LinearMap.IsSymmetric.eigenvectorBasis), the spectral expansion λ(G) (spectralExpansion) and the second eigenvalue λ₂(G) (secondEigenvalue), which are defined in Expander.Basic and Expander.Cheeger without spectral theory, agree with the eigenvalue quantities they name:

• λ(G) is the operator norm of G.orthogonalWalk (spectralExpansion_eq_norm_orthogonalWalk) and the maximum absolute value of its eigenvalues (spectralExpansion_eq_ciSup_abs_eigenvalues).
• When V has at least two vertices, λ₂(G) is the maximum eigenvalue of G.orthogonalWalk (secondEigenvalue_eq_ciSup_eigenvalues, secondEigenvalue_eq_orthogonalWalk_eigenvalues_zero).
• On the full space EuclideanSpace ℝ V, every eigenvalue of G.walkEuclidean lies in [-1, 1] (abs_walkEuclidean_eigenvalues_le_one); for a graph of positive degree, the largest eigenvalue is 1 (walkEuclidean_eigenvalues_zero) and the second largest eigenvalue counted with multiplicity is λ₂(G) (secondEigenvalue_eq_walkEuclidean_eigenvalues_one).

Main definitions

• Cslib.RotationMap.walkEuclidean: the walk operator on EuclideanSpace ℝ V.
• Cslib.RotationMap.orthogonalSubmodule: the subspace of EuclideanSpace ℝ V orthogonal to the constant functions.
• Cslib.RotationMap.orthogonalWalk: the restriction of G.walkEuclidean to orthogonalSubmodule V.

Main results

• Cslib.RotationMap.isSymmetric_walkEuclidean, Cslib.RotationMap.isSymmetric_orthogonalWalk: G.walkEuclidean and G.orthogonalWalk are symmetric.
• Cslib.RotationMap.mem_orthogonalSubmodule_iff: WithLp.toLp 2 f ∈ orthogonalSubmodule V iff 𝔼 v, f v = 0.
• Cslib.RotationMap.spectralExpansion_eq_norm_orthogonalWalk: λ(G) is the operator norm of G.orthogonalWalk.
• Cslib.RotationMap.abs_orthogonalWalk_eigenvalues_le, Cslib.RotationMap.orthogonalWalk_eigenvalues_le_secondEigenvalue: every eigenvalue of G.orthogonalWalk has absolute value at most λ(G) and is at most λ₂(G).
• Cslib.RotationMap.spectralExpansion_eq_ciSup_abs_eigenvalues: λ(G) is the supremum of the absolute values of the eigenvalues of G.orthogonalWalk.
• Cslib.RotationMap.secondEigenvalue_eq_ciSup_eigenvalues, Cslib.RotationMap.secondEigenvalue_eq_orthogonalWalk_eigenvalues_zero: on at least two vertices, λ₂(G) is the largest eigenvalue of G.orthogonalWalk.
• Cslib.RotationMap.abs_walkEuclidean_eigenvalues_le_one, Cslib.RotationMap.walkEuclidean_eigenvalues_zero, Cslib.RotationMap.secondEigenvalue_eq_walkEuclidean_eigenvalues_one: the eigenvalues of G.walkEuclidean lie in [-1, 1], with top eigenvalue 1 and second eigenvalue λ₂(G).

References

• S. Hoory, N. Linial, A. Wigderson, Expander graphs and their applications
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

noncomputable def Cslib.RotationMap.walkEuclidean {V : Type u_1} {D : Type u_2} [Fintype D] (G : RotationMap V D) : Module.End ℝ (EuclideanSpace ℝ V)

The walk operator of G transported to EuclideanSpace ℝ V.

@[simp]

theorem Cslib.RotationMap.walkEuclidean_toLp {V : Type u_1} {D : Type u_2} [Fintype D] (G : RotationMap V D) (f : V → ℝ) : G.walkEuclidean (WithLp.toLp 2 f) = WithLp.toLp 2 (G.walk f)

Applying G.walkEuclidean to WithLp.toLp 2 f applies G.walk to f.

@[simp]

theorem Cslib.RotationMap.ofLp_walkEuclidean {V : Type u_1} {D : Type u_2} [Fintype D] (G : RotationMap V D) (x : EuclideanSpace ℝ V) : (G.walkEuclidean x).ofLp = G.walk x.ofLp

Applying G.walkEuclidean and projecting from EuclideanSpace ℝ V applies G.walk.

theorem Cslib.RotationMap.isSymmetric_walkEuclidean {V : Type u_1} {D : Type u_2} [Fintype D] (G : RotationMap V D) [Fintype V] : LinearMap.IsSymmetric G.walkEuclidean

The walk operator on EuclideanSpace ℝ V is symmetric.

noncomputable def Cslib.RotationMap.orthogonalSubmodule (V : Type u_3) [Fintype V] : Submodule ℝ (EuclideanSpace ℝ V)

The subspace of EuclideanSpace ℝ V orthogonal to the constant functions.

theorem Cslib.RotationMap.mem_orthogonalSubmodule_iff {V : Type u_1} [Fintype V] (f : V → ℝ) : WithLp.toLp 2 f ∈ orthogonalSubmodule V ↔ (Finset.univ.expect fun (v : V) => f v) = 0

A vector in EuclideanSpace ℝ V is orthogonal to the constants iff its coordinates have expectation zero.

theorem Cslib.RotationMap.walkEuclidean_mem_orthogonalSubmodule {V : Type u_1} {D : Type u_2} [Fintype D] (G : RotationMap V D) [Fintype V] {x : EuclideanSpace ℝ V} (hx : x ∈ orthogonalSubmodule V) : G.walkEuclidean x ∈ orthogonalSubmodule V

The walk operator preserves orthogonalSubmodule V.

noncomputable def Cslib.RotationMap.orthogonalWalk {V : Type u_1} {D : Type u_2} [Fintype D] (G : RotationMap V D) [Fintype V] : ↥(orthogonalSubmodule V) →ₗ[ℝ] ↥(orthogonalSubmodule V)

The restriction of G.walkEuclidean to the subspace orthogonalSubmodule V of functions of expectation zero.

@[simp]

theorem Cslib.RotationMap.coe_orthogonalWalk {V : Type u_1} {D : Type u_2} [Fintype D] (G : RotationMap V D) [Fintype V] (u : ↥(orthogonalSubmodule V)) : ↑(G.orthogonalWalk u) = G.walkEuclidean ↑u

Coercing G.orthogonalWalk u to EuclideanSpace ℝ V applies G.walkEuclidean to u.

theorem Cslib.RotationMap.isSymmetric_orthogonalWalk {V : Type u_1} {D : Type u_2} [Fintype D] (G : RotationMap V D) [Fintype V] : G.orthogonalWalk.IsSymmetric

The restricted walk operator G.orthogonalWalk is symmetric.

theorem Cslib.RotationMap.spectralExpansion_eq_norm_orthogonalWalk {V : Type u_1} {D : Type u_2} [Fintype D] (G : RotationMap V D) [Fintype V] : G.spectralExpansion = ‖LinearMap.toContinuousLinearMap G.orthogonalWalk‖

The spectral expansion λ(G) is the operator norm of the restricted walk operator G.orthogonalWalk on orthogonalSubmodule V.

theorem Cslib.RotationMap.abs_orthogonalWalk_eigenvalues_le {V : Type u_1} {D : Type u_2} [Fintype D] (G : RotationMap V D) [Fintype V] {n : ℕ} (hn : Module.finrank ℝ ↥(orthogonalSubmodule V) = n) (i : Fin n) : |⋯.eigenvalues hn i| ≤ G.spectralExpansion

Every eigenvalue of G.orthogonalWalk has absolute value at most λ(G).

theorem Cslib.RotationMap.orthogonalWalk_eigenvalues_le_secondEigenvalue {V : Type u_1} {D : Type u_2} [Fintype D] (G : RotationMap V D) [Fintype V] {n : ℕ} (hn : Module.finrank ℝ ↥(orthogonalSubmodule V) = n) (i : Fin n) : ⋯.eigenvalues hn i ≤ G.secondEigenvalue

Every eigenvalue of G.orthogonalWalk is at most λ₂(G).

theorem Cslib.RotationMap.spectralExpansion_eq_ciSup_abs_eigenvalues {V : Type u_1} {D : Type u_2} [Fintype D] (G : RotationMap V D) [Fintype V] {n : ℕ} (hn : Module.finrank ℝ ↥(orthogonalSubmodule V) = n) : G.spectralExpansion = ⨆ (i : Fin n), |⋯.eigenvalues hn i|

The spectral expansion λ(G) is the supremum of the absolute values of the eigenvalues of G.orthogonalWalk.

theorem Cslib.RotationMap.secondEigenvalue_eq_orthogonalWalk_eigenvalues_zero {V : Type u_1} {D : Type u_2} [Fintype D] (G : RotationMap V D) [Fintype V] {n : ℕ} (hn : Module.finrank ℝ ↥(orthogonalSubmodule V) = n) (h0 : 0 < n) : G.secondEigenvalue = ⋯.eigenvalues hn ⟨0, h0⟩

When orthogonalSubmodule V has positive dimension n, the second eigenvalue λ₂(G) is the largest eigenvalue of G.orthogonalWalk.

theorem Cslib.RotationMap.secondEigenvalue_eq_ciSup_eigenvalues {V : Type u_1} {D : Type u_2} [Fintype D] (G : RotationMap V D) [Fintype V] {n : ℕ} (hn : Module.finrank ℝ ↥(orthogonalSubmodule V) = n) [Nontrivial V] : G.secondEigenvalue = ⨆ (i : Fin n), ⋯.eigenvalues hn i

On at least two vertices, the second eigenvalue λ₂(G) is the supremum of the eigenvalues of G.orthogonalWalk.

theorem Cslib.RotationMap.abs_walkEuclidean_eigenvalues_le_one {V : Type u_1} {D : Type u_2} [Fintype D] (G : RotationMap V D) [Fintype V] {m : ℕ} (hm : Module.finrank ℝ (EuclideanSpace ℝ V) = m) (i : Fin m) : |⋯.eigenvalues hm i| ≤ 1

Every eigenvalue of G.walkEuclidean on EuclideanSpace ℝ V has absolute value at most 1.

theorem Cslib.RotationMap.walkEuclidean_eigenvalues_zero {V : Type u_1} {D : Type u_2} [Fintype D] (G : RotationMap V D) [Fintype V] {m : ℕ} (hm : Module.finrank ℝ (EuclideanSpace ℝ V) = m) [Nonempty D] (hm0 : 0 < m) : ⋯.eigenvalues hm ⟨0, hm0⟩ = 1

On a nonempty vertex set and positive degree, the largest eigenvalue of G.walkEuclidean is 1.

theorem Cslib.RotationMap.secondEigenvalue_eq_walkEuclidean_eigenvalues_one {V : Type u_1} {D : Type u_2} [Fintype D] (G : RotationMap V D) [Fintype V] {m : ℕ} (hm : Module.finrank ℝ (EuclideanSpace ℝ V) = m) [Nonempty D] (hm1 : 1 < m) : G.secondEigenvalue = ⋯.eigenvalues hm ⟨1, hm1⟩

On at least two vertices and positive degree, the second largest eigenvalue of G.walkEuclidean counted with multiplicity is G.secondEigenvalue.