Lemma 2: Edge-to-Vertex Expansion

Main Results

• edgeToVertexExpansion: For a finite, connected s-regular graph with second-largest eigenvalue lam2, if |E| <= alpha|X1| then |Gamma(E)| >= beta|E| where beta = (sqrt(lam2^2 + 4s(s-lam2)alpha) - lam2) / (s(s-lam2)alpha).

The quadratic inverse gamma(at)

noncomputable def EdgeToVertexExpansion.gammaOfAlpha (s lam2 a : ℝ) : ℝ

The quadratic inverse: given at, solve at = g^2 + (lam2/s)g(1-g) for g. Gives g(at) = (sqrt(lam2^2 + 4s(s-lam2)at) - lam2) / (2(s-lam2)).

Equations

• EdgeToVertexExpansion.gammaOfAlpha s lam2 a = (√(lam2 ^ 2 + 4 * s * (s - lam2) * a) - lam2) / (2 * (s - lam2))

noncomputable def EdgeToVertexExpansion.betaParam (s lam2 a : ℝ) : ℝ

The expansion parameter beta = 2*gamma(alpha)/(s*alpha).

Equations

• EdgeToVertexExpansion.betaParam s lam2 a = (√(lam2 ^ 2 + 4 * s * (s - lam2) * a) - lam2) / (s * (s - lam2) * a)

theorem EdgeToVertexExpansion.betaParam_eq (s lam2 a : ℝ) (hs : s ≠ 0) (ha : a ≠ 0) : betaParam s lam2 a = 2 * gammaOfAlpha s lam2 a / (s * a)

Discriminant positivity

theorem EdgeToVertexExpansion.discriminant_nonneg (s lam2 a : ℝ) (hs : 0 < s) (hsl : lam2 < s) (ha : 0 ≤ a) : 0 ≤ lam2 ^ 2 + 4 * s * (s - lam2) * a

sqrt >= lam2

theorem EdgeToVertexExpansion.sqrt_ge_lam2 (s lam2 a : ℝ) (hs : 0 < s) (hsl : lam2 < s) (ha : 0 ≤ a) : lam2 ≤ √(lam2 ^ 2 + 4 * s * (s - lam2) * a)

gammaOfAlpha is nonneg

theorem EdgeToVertexExpansion.gammaOfAlpha_nonneg (s lam2 a : ℝ) (hs : 0 < s) (hsl : lam2 < s) (ha : 0 ≤ a) : 0 ≤ gammaOfAlpha s lam2 a

gammaOfAlpha at zero

theorem EdgeToVertexExpansion.gammaOfAlpha_zero (s lam2 : ℝ) (_hs : 0 < s) (_hsl : lam2 < s) (hlam_nn : 0 ≤ lam2) : gammaOfAlpha s lam2 0 = 0

Concavity: gamma(at) * alpha >= gamma(alpha) * at for at <= alpha

theorem EdgeToVertexExpansion.gammaOfAlpha_concavity (s lam2 alpha at_ : ℝ) (hs : 0 < s) (hsl : lam2 < s) (halpha : 0 < alpha) (hat_nn : 0 ≤ at_) (hat_le : at_ ≤ alpha) : gammaOfAlpha s lam2 alpha * at_ ≤ gammaOfAlpha s lam2 at_ * alpha

Handshaking lemma

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

Step 2: Alon-Chung implies |Gamma(E)| >= gamma(at) * |V|

theorem EdgeToVertexExpansion.incidentVertices_ge_gamma {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) (lam2 : ℝ) (hlam2 : lam2 = GraphExpansion.secondLargestEigenvalue G hcard) (hlam2_lt_s : lam2 < ↑s) (E : Finset (Sym2 V)) (hE_sub : E ⊆ G.edgeFinset) (hE_ne : E.Nonempty) : ↑(AlonChungContrapositive.incidentVertices E).card ≥ gammaOfAlpha (↑s) lam2 (↑E.card / ↑G.edgeFinset.card) * ↑(Fintype.card V)

Main theorem

theorem EdgeToVertexExpansion.edgeToVertexExpansion {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) (lam2 : ℝ) (hlam2 : lam2 = GraphExpansion.secondLargestEigenvalue G hcard) (hlam2_lt_s : lam2 < ↑s) (alpha : ℝ) (halpha_pos : 0 < alpha) (_halpha_le : alpha ≤ 1) (E : Finset (Sym2 V)) (hE_sub : E ⊆ G.edgeFinset) (hE_le : ↑E.card ≤ alpha * ↑G.edgeFinset.card) : ↑(AlonChungContrapositive.incidentVertices E).card ≥ betaParam (↑s) lam2 alpha * ↑E.card