Disagreement across an expander

The counting fact that makes Dinur's clouds work. A cloud is wired by an expander and carries equality constraints, so an assignment that is not constant on the cloud must break many of them. Quantitatively: if f labels the vertices of an expander and S is the set of vertices whose label differs from some fixed value c, then at least (1 - lam) · deg · |S| · |Sᶜ| / n darts join two vertices with different labels — because every dart from S to Sᶜ does, and EdgeExpansion counts those.

Taking c to be a plurality value of f — which by pigeonhole is held by at least a 1 / |α| fraction of the vertices — turns this into

(1 - lam) · deg · |S| / |α| ≤ #disagreeing darts,

a bound linear in the number of deviant vertices, with a constant depending only on the expander and the alphabet. That is exactly the exchange rate degree reduction needs: each vertex that lies about its cloud's value pays for itself in broken equality constraints.

Main definitions

• RegGraph.disagreeDarts — the darts whose two ends carry different labels

Main results

• exists_plurality_value — pigeonhole: some value is held n / |α| often
• RegGraph.card_disagreeDarts_ge — disagreement is at least the edge boundary
• RegGraph.card_disagreeDarts_ge_of_plurality — the form used by clouds

theorem Complexity.exists_plurality_value {V α : Type} [Fintype V] [Fintype α] [Nonempty α] [DecidableEq α] (f : V → α) : ∃ (c : α), Fintype.card V ≤ Fintype.card α * {v : V | f v = c}.card

Pigeonhole. Some value is taken by at least a 1 / |α| fraction.

def Complexity.RegGraph.disagreeDarts {α : Type} [DecidableEq α] (G : RegGraph) (f : G.V → α) : Finset (G.V × G.D)

The darts whose two endpoints carry different labels.

Equations

• G.disagreeDarts f = {p : G.V × G.D | f p.1 ≠ f (G.nbr p.1 p.2)}

theorem Complexity.RegGraph.card_disagreeDarts_ge {α : Type} [DecidableEq α] (G : RegGraph) {lam : ℝ} (hlam : 0 ≤ lam) (h : G.SpectralBound lam) (hn : 0 < G.order) (f : G.V → α) (c : α) : (1 - lam) * ↑G.deg * (↑{v : G.V | f v ≠ c}.card * ↑{v : G.V | f v ≠ c}ᶜ.card / ↑G.order) ≤ ↑(G.disagreeDarts f).card

Disagreement is at least the edge boundary. Every dart leaving the set of vertices that differ from c joins two differently-labelled vertices.

theorem Complexity.RegGraph.card_disagreeDarts_ge_of_plurality {α : Type} [DecidableEq α] (G : RegGraph) [Fintype α] {lam : ℝ} (hlam : 0 ≤ lam) (hlam1 : lam ≤ 1) (h : G.SpectralBound lam) (hn : 0 < G.order) (f : G.V → α) (c : α) (hc : G.order ≤ Fintype.card α * {v : G.V | f v = c}.card) : (1 - lam) * ↑G.deg * (↑{v : G.V | f v ≠ c}.card / ↑(Fintype.card α)) ≤ ↑(G.disagreeDarts f).card

The form the cloud argument uses: with c a plurality value, the number of disagreeing darts is proportional to the number of deviant vertices.