Regular multigraphs of permutations

A family σ : K → Equiv.Perm V of permutations of the vertices gives a regular multigraph of degree 2 |K| (ofPerms): at every vertex v, each permutation σ k contributes an edge to σ k v and, as the other end of the edge from (σ k)⁻¹ v, an edge to (σ k)⁻¹ v. Following an edge forwards along σ k and then backwards along (σ k)⁻¹ returns to its start, so the rotation map is an involution. When the permutations are the actions of the generators of a group, this is the Schreier graph of the action with respect to the generators and their inverses Hoory, Linial and Wigderson, Section 11.1.2.

The edges leaving a set S of vertices are counted exactly by how many points of S each permutation moves out of S: σ k moves as many points of S out of S as its inverse does, and each such point is the start of an edge leaving S (card_interedges_compl_ofPerms). So if every set of at most half of the vertices has a constant fraction of its points moved out of it by the permutations, the multigraph is an edge expander (le_edgeExpansion_ofPerms). Random permutations have this property (Cslib.exists_perms_card_le_mul_card_filter_notMem): their multigraph is the permutation model of random regular graphs Hoory, Linial and Wigderson, Section 7.2.1, and random regular graphs are expanders Hoory, Linial and Wigderson, Theorem 4.16 Arora and Barak, Chapter 21.

Main definitions

• Cslib.RotationMap.ofPerms: the regular multigraph of a family of permutations.

Main results

• Cslib.RotationMap.card_interedges_compl_ofPerms: the edges leaving a set count the points the permutations move out of it, twice.
• Cslib.RotationMap.le_edgeExpansion_ofPerms: a lower bound on these counts for every set of at most half of the vertices bounds the edge expansion.

References

• S. Hoory, N. Linial, A. Wigderson, Expander graphs and their applications
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

def Cslib.RotationMap.ofPerms {V : Type u_1} {K : Type u_2} (σ : K → Equiv.Perm V) : RotationMap V (K × Bool)

The regular multigraph of a family σ : K → Equiv.Perm V of permutations, of degree 2 |K|, as in the permutation model of random regular graphs Hoory, Linial and Wigderson, Section 7.2.1: the edge (k, false) at v leads to σ k v, where it is the edge (k, true), which leads back along the inverse permutation.

@[simp]

theorem Cslib.RotationMap.rot_ofPerms_false {V : Type u_1} {K : Type u_2} (σ : K → Equiv.Perm V) (v : V) (k : K) : (ofPerms σ).rot (v, k, false) = ((σ k) v, k, true)

The rotation map of ofPerms σ on a forward edge.

@[simp]

theorem Cslib.RotationMap.rot_ofPerms_true {V : Type u_1} {K : Type u_2} (σ : K → Equiv.Perm V) (v : V) (k : K) : (ofPerms σ).rot (v, k, true) = ((Equiv.symm (σ k)) v, k, false)

The rotation map of ofPerms σ on a backward edge.

@[simp]

theorem Cslib.RotationMap.neighbor_ofPerms_false {V : Type u_1} {K : Type u_2} (σ : K → Equiv.Perm V) (v : V) (k : K) : (ofPerms σ).neighbor v (k, false) = (σ k) v

The forward edge labelled k at v leads to σ k v.

@[simp]

theorem Cslib.RotationMap.neighbor_ofPerms_true {V : Type u_1} {K : Type u_2} (σ : K → Equiv.Perm V) (v : V) (k : K) : (ofPerms σ).neighbor v (k, true) = (Equiv.symm (σ k)) v

The backward edge labelled k at v leads to (σ k)⁻¹ v.

theorem Cslib.RotationMap.card_interedges_compl_ofPerms {V : Type u_1} {K : Type u_2} (σ : K → Equiv.Perm V) [Fintype V] [DecidableEq V] [Fintype K] (S : Finset V) : ((ofPerms σ).interedges S Sᶜ).card = 2 * ∑ k : K, {v ∈ S | (σ k) v ∉ S}.card

The edges leaving a set in the multigraph of σ: each permutation σ k contributes twice the number of points of S it moves out of S, once along σ k and once along its inverse.

theorem Cslib.RotationMap.le_edgeExpansion_ofPerms {V : Type u_1} {K : Type u_2} (σ : K → Equiv.Perm V) [Fintype V] [DecidableEq V] [Fintype K] [Nontrivial V] {c : ℝ} (h : ∀ (S : Finset V), 2 * S.card ≤ Fintype.card V → c * ↑S.card ≤ ↑(∑ k : K, {v ∈ S | (σ k) v ∉ S}.card)) : 2 * c ≤ (ofPerms σ).edgeExpansion

Edge expansion from moved points: on at least two vertices, if the permutations together move at least c |S| points of every set S of at most half of the vertices out of S, then the edge expansion of their multigraph is at least 2 c.