Documentation

Complexity.Foundations.Combinatorics.Expander.LowerBound

A lower bound on the spectral expansion #

A D-regular multigraph on N ≥ 2 vertices has spectral expansion (N - D) / (D (N - 1)) ≤ λ(G) ^ 2 (div_le_sq_spectralExpansion). So no graph of degree below its number of vertices has λ(G) = 0 (spectralExpansion_pos), and λ(G) ≥ 1 / √(2 D) once N ≥ 2 D (one_div_sqrt_two_mul_le_spectralExpansion): bounded-degree expanders cannot be arbitrarily good. The bound is tight for D = N: the complete graph with a self-loop at every vertex, whose walk operator maps every function to its expectation, has λ = 0 (spectralExpansion_complete).

The proof is the trace argument, phrased without spectral theory. Let a v u be the number of edges from v to u and test the characterization of λ(G) on the functions f_u = δ_u - 1 / N of expectation zero, which have ∑ v, f_u v ^ 2 = 1 - 1 / N. Summing ∑ v, (G.walk f_u) v ^ 2 ≤ λ ^ 2 (1 - 1 / N) over u bounds ∑ v u, (a v u / D - 1 / N) ^ 2 by λ ^ 2 (N - 1), while a v u ≤ a v u ^ 2 (edge multiplicities are natural numbers) and ∑ u, a v u = D bound it below by N (1 / D - 1 / N). Compare the discussion of lower bounds on the second eigenvalue in Hoory, Linial and Wigderson, Section 5.

Main definitions #

Main results #

References #

The complete graph with self-loops #

source
def Cslib.RotationMap.complete (V : Type u_3) :
RotationMap V V

The complete graph on V with a self-loop at every vertex, as a |V|-regular multigraph: the u-th edge at v leads to u and is the v-th edge there.

Instances For
    source
    @[simp]
    theorem Cslib.RotationMap.rot_complete {V : Type u_1} (p : V × V) :
    (complete V).rot p = p.swap

    The rotation map of the complete graph swaps the vertex and the label.

    source
    @[simp]
    theorem Cslib.RotationMap.neighbor_complete {V : Type u_1} (v u : V) :
    (complete V).neighbor v u = u

    The u-th neighbor of every vertex in the complete graph is u.

    source
    theorem Cslib.RotationMap.spectralExpansion_complete {V : Type u_1} [Fintype V] :
    (complete V).spectralExpansion = 0

    The complete graph with self-loops has spectral expansion 0: one step of its walk replaces a function by its expectation.

    The trace bound #

    source
    theorem Cslib.RotationMap.div_le_sq_spectralExpansion {V : Type u_1} {D : Type u_2} [Fintype V] [Fintype D] [Nonempty D] (G : RotationMap V D) (hV : 2 ≤ Fintype.card V) :
    (↑(Fintype.card V) - ↑(Fintype.card D)) / (↑(Fintype.card D) * (↑(Fintype.card V) - 1)) ≤ G.spectralExpansion ^ 2

    Trace bound. A D-regular multigraph on N ≥ 2 vertices has (N - D) / (D (N - 1)) ≤ λ(G) ^ 2.

    source
    theorem Cslib.RotationMap.sqrt_le_spectralExpansion {V : Type u_1} {D : Type u_2} [Fintype V] [Fintype D] [Nonempty D] (G : RotationMap V D) (hV : 2 ≤ Fintype.card V) :
    √((↑(Fintype.card V) - ↑(Fintype.card D)) / (↑(Fintype.card D) * (↑(Fintype.card V) - 1))) ≤ G.spectralExpansion

    Trace bound, square-root form: a D-regular multigraph on N ≥ 2 vertices has √((N - D) / (D (N - 1))) ≤ λ(G).

    source
    theorem Cslib.RotationMap.spectralExpansion_pos {V : Type u_1} {D : Type u_2} [Fintype V] [Fintype D] [Nonempty D] (G : RotationMap V D) (hDV : Fintype.card D < Fintype.card V) :
    0 < G.spectralExpansion

    A regular multigraph whose degree is below its number of vertices has positive spectral expansion.

    source
    theorem Cslib.RotationMap.one_div_sqrt_two_mul_le_spectralExpansion {V : Type u_1} {D : Type u_2} [Fintype V] [Fintype D] [Nonempty D] (G : RotationMap V D) (hDV : 2 * Fintype.card D ≤ Fintype.card V) :
    1 / √(2 * ↑(Fintype.card D)) ≤ G.spectralExpansion

    A D-regular multigraph on at least 2 D vertices has 1 / √(2 D) ≤ λ(G).