Edge expansion from the spectral bound

Dinur's degree-reduction step needs expansion in its combinatorial form: a vertex set with few outgoing edges must be almost everything or almost nothing. This module derives that from Mixing by feeding it indicator functions.

Specialising mixing_sq to 1_S and 1_T says that the number of darts from S to T is what independence predicts, deg · |S| · |T| / n, up to lam times the two variances. Taking T = Sᶜ, both variances equal |S| |Sᶜ| / n, so the error term's square root is rational in the data and no Real.sqrt is needed: the number of darts leaving S is at least (1 - lam) · deg · |S| |Sᶜ| / n.

That is exactly the statement degree reduction consumes: inside a cloud built on an expander, the vertices disagreeing with the cloud's plurality label send out proportionally many edges, each of which is an unsatisfied equality constraint.

Main definitions

• RegGraph.dartsBetween — the darts from one vertex set to another

Main results

• RegGraph.sum_indicator_mul_step — the dart count as an operator inner product
• RegGraph.mixing_sq_indicator — the mixing lemma for vertex sets
• RegGraph.card_dartsBetween_compl_ge — edge expansion: a set sends out at least (1 - lam) · deg · |S| |Sᶜ| / n darts

def Complexity.RegGraph.dartsBetween (G : RegGraph) (S T : Finset G.V) : Finset (G.V × G.D)

The darts whose tail lies in S and whose head lies in T.

Equations

• G.dartsBetween S T = {p : G.V × G.D | p.1 ∈ S ∧ G.nbr p.1 p.2 ∈ T}

def Complexity.RegGraph.indicator (G : RegGraph) (S : Finset G.V) : G.V → ℝ

The real-valued indicator of a vertex set.

Equations

• G.indicator S v = if v ∈ S then 1 else 0

@[simp]

theorem Complexity.RegGraph.sum_indicator (G : RegGraph) (S : Finset G.V) : ∑ v : G.V, G.indicator S v = ↑S.card

@[simp]

theorem Complexity.RegGraph.sum_sq_indicator (G : RegGraph) (S : Finset G.V) : ∑ v : G.V, G.indicator S v ^ 2 = ↑S.card

theorem Complexity.RegGraph.sum_indicator_mul_step (G : RegGraph) (S T : Finset G.V) : ∑ v : G.V, G.indicator S v * G.step (G.indicator T) v = ↑(G.dartsBetween S T).card / ↑G.deg

The dart count between two sets, as an inner product against the walk operator.

theorem Complexity.RegGraph.mixing_sq_indicator (G : RegGraph) {lam : ℝ} (h : G.SpectralBound lam) (hn : 0 < G.order) (S T : Finset G.V) : (↑(G.dartsBetween S T).card / ↑G.deg - ↑S.card * ↑T.card / ↑G.order) ^ 2 ≤ lam ^ 2 * (↑S.card - ↑S.card ^ 2 / ↑G.order) * (↑T.card - ↑T.card ^ 2 / ↑G.order)

The mixing lemma for vertex sets.

theorem Complexity.RegGraph.card_dartsBetween_compl_ge (G : RegGraph) {lam : ℝ} (hlam : 0 ≤ lam) (h : G.SpectralBound lam) (hn : 0 < G.order) (S : Finset G.V) : (1 - lam) * ↑G.deg * (↑S.card * ↑Sᶜ.card / ↑G.order) ≤ ↑(G.dartsBetween S Sᶜ).card

Edge expansion. A vertex set sends out at least (1 - lam) · deg · |S| · |Sᶜ| / n darts.