Graphs built from permutations

A tuple of D permutations of Fin n gives a 2 D-regular graph: at each vertex, every permutation contributes a forward dart to its image and a backward dart to its preimage. Reversal swaps the two, so the rotation map is an involution with no bookkeeping.

This is the shape in which the expander family is obtained: the permutations are chosen by counting (a random tuple works), and this module supplies the translation from a statement about permutations — some permutation moves a constant fraction of any small set out of itself — to the edge expansion the Cheeger bound consumes.

Main definitions

• Complexity.RegGraph.permsGraph — the 2 D-regular graph of a tuple
• Complexity.escape — how many points of a set a permutation moves out of it

Main results

• Complexity.RegGraph.edgeExpansion_permsGraph — a lower bound on escape for every small set gives edge expansion

def Complexity.RegGraph.permsRot {n D : ℕ} (σ : Fin D → Equiv.Perm (Fin n)) : Fin n × Fin D × Bool → Fin n × Fin D × Bool

The rotation map of a tuple of permutations: a forward dart becomes the matching backward dart at the image, and conversely.

Equations

• Complexity.RegGraph.permsRot σ p = if p.2.2 = true then ((Equiv.symm (σ p.2.1)) p.1, p.2.1, false) else ((σ p.2.1) p.1, p.2.1, true)

theorem Complexity.RegGraph.permsRot_involutive {n D : ℕ} (σ : Fin D → Equiv.Perm (Fin n)) : Function.Involutive (permsRot σ)

def Complexity.RegGraph.permsGraph {n D : ℕ} (hD : 0 < D) (σ : Fin D → Equiv.Perm (Fin n)) : RegGraph

The graph of a tuple of permutations, of degree 2 D.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Complexity.RegGraph.order_permsGraph {n D : ℕ} (hD : 0 < D) (σ : Fin D → Equiv.Perm (Fin n)) : (permsGraph hD σ).order = n

theorem Complexity.RegGraph.deg_permsGraph {n D : ℕ} (hD : 0 < D) (σ : Fin D → Equiv.Perm (Fin n)) : (permsGraph hD σ).deg = 2 * D

theorem Complexity.RegGraph.nbr_permsGraph_false {n D : ℕ} (hD : 0 < D) (σ : Fin D → Equiv.Perm (Fin n)) (v : Fin n) (i : Fin D) : (permsGraph hD σ).nbr v (i, false) = (σ i) v

theorem Complexity.RegGraph.sum_escape_le_dartsBetween {n D : ℕ} (hD : 0 < D) (σ : Fin D → Equiv.Perm (Fin n)) (S : Finset (Fin n)) : ∑ i : Fin D, escape (σ i) S ≤ ((permsGraph hD σ).dartsBetween S Sᶜ).card

Forward darts leave. The darts of the graph that leave S include, for every permutation, one for each point of S that permutation moves out.

theorem Complexity.RegGraph.edgeExpansion_permsGraph {n D : ℕ} (hD : 0 < D) (σ : Fin D → Equiv.Perm (Fin n)) (c : ℕ) (hc : 0 < c) (hesc : ∀ (S : Finset (Fin n)), 2 * S.card ≤ n → ∃ (i : Fin D), S.card ≤ c * escape (σ i) S) : (permsGraph hD σ).EdgeExpansion (1 / (2 * ↑c * ↑D))

From escape to expansion. If every nonempty set of at most half the vertices is moved out of itself by some permutation, in at least a 1 / c fraction, the graph has edge expansion 1 / (2 c D).