Theorem 6: Alon–Chung Bound

Main Results

• inducedEdges: The edge set of the induced subgraph on S.
• alonChung: For a finite s-regular graph with second-largest eigenvalue λ₂, and S ⊆ V with |S| = γ|V|, we have |X(S)₁| ≤ α |X₁| where α = γ² + (λ₂/s) γ(1-γ).

The proof uses spectral decomposition of the quadratic form 1_S^T M 1_S where M is the adjacency matrix.

Induced edges

def AlonChung.inducedEdges {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : Finset (Sym2 V)

The induced edge set X(S)₁ = {e ∈ X₁ : both endpoints of e lie in S}.

Equations

• AlonChung.inducedEdges G S = G.edgeFinset ∩ S.sym2

theorem AlonChung.mem_inducedEdges {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) (e : Sym2 V) : e ∈ inducedEdges G S ↔ e ∈ G.edgeFinset ∧ ∀ v ∈ e, v ∈ S

theorem AlonChung.inducedEdges_nonempty {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) (h : ∃ e ∈ G.edgeFinset, ∀ v ∈ e, v ∈ S) : (inducedEdges G S).Nonempty

Indicator vector

def AlonChung.indicatorVec {V : Type u_1} [DecidableEq V] (S : Finset V) : V → ℝ

The indicator (characteristic) vector 1_S ∈ ℝ^V of a subset S ⊆ V.

Equations

• AlonChung.indicatorVec S v = if v ∈ S then 1 else 0

@[simp]

theorem AlonChung.indicatorVec_mem {V : Type u_1} [Fintype V] [DecidableEq V] {S : Finset V} {v : V} (hv : v ∈ S) : indicatorVec S v = 1

@[simp]

theorem AlonChung.indicatorVec_not_mem {V : Type u_1} [Fintype V] [DecidableEq V] {S : Finset V} {v : V} (hv : v ∉ S) : indicatorVec S v = 0

Quadratic form identity

theorem AlonChung.quadratic_form_eq_twice_inducedEdges {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : indicatorVec S ⬝ᵥ (SimpleGraph.adjMatrix ℝ G).mulVec (indicatorVec S) = 2 * ↑(inducedEdges G S).card

The quadratic form 1_S^T M 1_S counts twice the number of induced edges: ∑_{v,w} 1_S(v) M(v,w) 1_S(w) = 2 |X(S)₁|.

Edge count for regular graphs

theorem AlonChung.twice_card_edgeFinset_eq {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (s : ℕ) (hreg : G.IsRegularOfDegree s) : 2 * ↑G.edgeFinset.card = ↑s * ↑(Fintype.card V)

For an s-regular graph, |X₁| = s * |V| / 2. More precisely, 2 * |X₁| = s * |V|.

Spectral decomposition of the quadratic form

theorem AlonChung.spectral_decomp_quadratic {V : Type u_1} [Fintype V] [DecidableEq V] (A : Matrix V V ℝ) (hA : A.IsHermitian) (x : V → ℝ) : x ⬝ᵥ A.mulVec x = ∑ j : V, hA.eigenvalues j * (x ⬝ᵥ (hA.eigenvectorBasis j).ofLp) ^ 2

The spectral decomposition: x^T A x = ∑_j λ_j (x · v_j)² for Hermitian A, where v_j are orthonormal eigenvectors and λ_j are eigenvalues.

theorem AlonChung.parseval_eigenvector {V : Type u_1} [Fintype V] [DecidableEq V] (A : Matrix V V ℝ) (hA : A.IsHermitian) (x : V → ℝ) : x ⬝ᵥ x = ∑ j : V, (x ⬝ᵥ (hA.eigenvectorBasis j).ofLp) ^ 2

The Parseval identity for the eigenvector basis: ‖x‖² = ∑_j (x · v_j)².

theorem AlonChung.quadratic_le_bound {V : Type u_1} [Fintype V] [DecidableEq V] (A : Matrix V V ℝ) (hA : A.IsHermitian) (x : V → ℝ) (C : ℝ) (hC : ∀ (j : V), hA.eigenvalues j ≤ C) : x ⬝ᵥ A.mulVec x ≤ C * x ⬝ᵥ x

Quadratic form bounded by max eigenvalue times norm squared.

Eigenvalue bounds for regular graphs

theorem AlonChung.eigenvalue_le_degree {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (s : ℕ) (hreg : G.IsRegularOfDegree s) (j : V) : ⋯.eigenvalues j ≤ ↑s

All eigenvalues of an s-regular graph are at most s.

theorem AlonChung.degree_mem_eigenvalues {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Nonempty V] (s : ℕ) (hreg : G.IsRegularOfDegree s) : ↑s ∈ Set.range ⋯.eigenvalues

s is an eigenvalue of the adjacency matrix of an s-regular graph. This follows from M · 1 = s · 1.

theorem AlonChung.max_eigenvalue_eq_degree {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (s : ℕ) (hreg : G.IsRegularOfDegree s) (hcard : 2 ≤ Fintype.card V) : GraphExpansion.adjEigenvalues G ⟨0, ⋯⟩ = ↑s

The maximum eigenvalue of an s-regular graph is s.

Norm of indicator vector

@[simp]

theorem AlonChung.indicatorVec_dotProduct_self {V : Type u_1} [Fintype V] [DecidableEq V] (S : Finset V) : indicatorVec S ⬝ᵥ indicatorVec S = ↑S.card

Spectral bound on the quadratic form

theorem AlonChung.regular_mulVec_const {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (s : ℕ) (hreg : G.IsRegularOfDegree s) (c : ℝ) : (SimpleGraph.adjMatrix ℝ G).mulVec (Function.const V c) = Function.const V (↑s * c)

The all-ones vector is an eigenvector of the adjacency matrix with eigenvalue s.

theorem AlonChung.quadratic_decomp {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (s : ℕ) (hreg : G.IsRegularOfDegree s) (x z : V → ℝ) (γ : ℝ) (hx : x = fun (v : V) => γ + z v) (hz_sum : ∑ v : V, z v = 0) : x ⬝ᵥ (SimpleGraph.adjMatrix ℝ G).mulVec x = ↑s * γ ^ 2 * ↑(Fintype.card V) + z ⬝ᵥ (SimpleGraph.adjMatrix ℝ G).mulVec z

Decomposition of the quadratic form using the all-ones vector. If z = x - γ · 1, then x^T M x = s γ² n + z^T M z.

axiom AlonChung.regular_eigenvector_s_constant {V : Type u_1} [Fintype V] [DecidableEq V] {V✝ : Type u_2} [Fintype V✝] [DecidableEq V✝] (G : SimpleGraph V✝) [DecidableRel G.Adj] (s : ℕ) (hs : 1 ≤ s) (hreg : G.IsRegularOfDegree s) (hcard : 2 ≤ Fintype.card V✝) (hsimple : ⋯.eigenvalues₀ ⟨0, ⋯⟩ > ⋯.eigenvalues₀ ⟨1, ⋯⟩) (v : V✝ → ℝ) (hv : (SimpleGraph.adjMatrix ℝ G).mulVec v = ↑s • v) : ∃ (c : ℝ), v = Function.const V✝ c

For an s-regular graph with s ≥ 1 where the largest eigenvalue is simple (strictly greater than the second), any eigenvector of the adjacency matrix with eigenvalue s is globally constant. This combines two classical spectral graph theory results: (1) the discrete maximum principle shows eigenvectors for eigenvalue s are constant on connected components, and (2) simple top eigenvalue implies graph connectivity (otherwise each component contributes an independent eigenvector for eigenvalue s, giving multiplicity ≥ 2). Both require infrastructure (harmonic function theory on graphs, eigenspace dimension theory) not currently available in Mathlib.

theorem AlonChung.spectral_bound {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (s : ℕ) (hs : 1 ≤ s) (hreg : G.IsRegularOfDegree s) (hcard : 2 ≤ Fintype.card V) (S : Finset V) : have n := ↑(Fintype.card V); have γ := ↑S.card / n; have lam₂ := GraphExpansion.secondLargestEigenvalue G hcard; indicatorVec S ⬝ᵥ (SimpleGraph.adjMatrix ℝ G).mulVec (indicatorVec S) ≤ ↑s * γ ^ 2 * n + lam₂ * γ * (1 - γ) * n

The spectral bound: 1_S^T M 1_S ≤ s γ² n + λ₂ γ(1-γ) n.

Main Theorem

theorem AlonChung.alonChung {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (s : ℕ) (hs : 1 ≤ s) (hreg : G.IsRegularOfDegree s) (hcard : 2 ≤ Fintype.card V) (S : Finset V) (hS_ne : S.Nonempty) (hS_lt : S.card < Fintype.card V) : have n := ↑(Fintype.card V); have γ := ↑S.card / n; have lam₂ := GraphExpansion.secondLargestEigenvalue G hcard; have α := γ ^ 2 + lam₂ / ↑s * γ * (1 - γ); ↑(inducedEdges G S).card ≤ α * ↑G.edgeFinset.card

Alon–Chung Bound. For a finite s-regular graph with s ≥ 1 and |V| ≥ 2, with second-largest eigenvalue λ₂, and S ⊆ V with |S| = γ|V| for 0 < γ < 1, define α = γ² + (λ₂/s) γ(1-γ). Then |X(S)₁| ≤ α |X₁|.

The proof uses the spectral decomposition of the quadratic form 1_S^T M 1_S to bound the number of edges in the induced subgraph.