The edges of a rotation map

A D-regular multigraph presented by a rotation map G (Cslib.RotationMap) has an edge for each unordered pair {p, G.rot p} of a dart and its reversal (Cslib.RotationMap.edges), joining the vertices of the two darts (Cslib.RotationMap.edgeEnds); a dart fixed by G.rot is a self-loop. This presents G as a multigraph given by its ends (Cslib.Multigraph), with the same underlying simple graph (Cslib.RotationMap.toSimpleGraph_edgeEnds). The edges between a set S of vertices and its complement are the darts from S to its complement (Cslib.RotationMap.card_edgeCut_edgeEnds), so the edge expansion h(G) bounds the expansion e(G) of Ben-Sasson and Wigderson: h(G) |V| / 3 ≤ e(G) (Cslib.RotationMap.edgeExpansion_mul_card_div_three_le_minBalancedCut), and a rotation map of positive edge expansion is connected (Cslib.RotationMap.connected_toSimpleGraph_of_edgeExpansion_pos).

Main definitions

• Cslib.RotationMap.edges, Cslib.RotationMap.edgeEnds: the edges of a rotation map and their ends.

Main results

• Cslib.RotationMap.toSimpleGraph_edgeEnds: the multigraph of the edges has the simple graph of the rotation map.
• Cslib.RotationMap.card_edgeCut_edgeEnds: the edges leaving a set are the darts leaving it.
• Cslib.RotationMap.card_incidence_edgeEnds_le: a vertex has at most |D| edges other than self-loops.
• Cslib.RotationMap.edgeExpansion_mul_card_div_three_le_minBalancedCut: h(G) |V| / 3 ≤ e(G).
• Cslib.RotationMap.connected_toSimpleGraph_of_edgeExpansion_pos: positive edge expansion makes a rotation map connected.

References

• E. Ben-Sasson, A. Wigderson, Short proofs are narrow—resolution made simple
• S. Hoory, N. Linial, A. Wigderson, Expander graphs and their applications

def Cslib.RotationMap.edges {V : Type u_1} {D : Type u_2} [Fintype V] [DecidableEq V] [Fintype D] [DecidableEq D] (G : RotationMap V D) : Finset (Sym2 (V × D))

The edges of G: the unordered pairs {p, G.rot p} of a dart and its reversal. A dart fixed by G.rot is a self-loop.

def Cslib.RotationMap.edgeEnds {V : Type u_1} {D : Type u_2} [Fintype V] [DecidableEq V] [Fintype D] [DecidableEq D] (G : RotationMap V D) (e : ↥G.edges) : Sym2 V

The ends of an edge of G: the vertices of its two darts.

theorem Cslib.RotationMap.mk_mem_edges {V : Type u_1} {D : Type u_2} [Fintype V] [DecidableEq V] [Fintype D] [DecidableEq D] (G : RotationMap V D) (p : V × D) : s(p, G.rot p) ∈ G.edges

Every dart p gives the edge {p, G.rot p} of G.

theorem Cslib.RotationMap.exists_eq_of_mem_edges {V : Type u_1} {D : Type u_2} [Fintype V] [DecidableEq V] [Fintype D] [DecidableEq D] {G : RotationMap V D} {e : Sym2 (V × D)} (he : e ∈ G.edges) : ∃ (p : V × D), s(p, G.rot p) = e

Every edge of G is {p, G.rot p} for some dart p.

theorem Cslib.RotationMap.card_edges_le {V : Type u_1} {D : Type u_2} [Fintype V] [DecidableEq V] [Fintype D] [DecidableEq D] (G : RotationMap V D) : G.edges.card ≤ Fintype.card V * Fintype.card D

G has at most |V| |D| edges.

theorem Cslib.RotationMap.toSimpleGraph_edgeEnds {V : Type u_1} {D : Type u_2} [Fintype V] [DecidableEq V] [Fintype D] [DecidableEq D] (G : RotationMap V D) : Multigraph.toSimpleGraph G.edgeEnds = G.toSimpleGraph

The multigraph of the edges of G has the simple graph of G.

theorem Cslib.RotationMap.card_edgeCut_edgeEnds {V : Type u_1} {D : Type u_2} [Fintype V] [DecidableEq V] [Fintype D] [DecidableEq D] (G : RotationMap V D) (S : Finset V) : (Multigraph.edgeCut G.edgeEnds S).card = (G.interedges S Sᶜ).card

The edges between S and its complement are the darts from S to its complement.

theorem Cslib.RotationMap.card_incidence_edgeEnds_le {V : Type u_1} {D : Type u_2} [Fintype V] [DecidableEq V] [Fintype D] [DecidableEq D] (G : RotationMap V D) (v : V) : (Multigraph.incidence G.edgeEnds v).card ≤ Fintype.card D

A vertex of G has at most |D| edges other than self-loops.

theorem Cslib.RotationMap.edgeExpansion_mul_card_div_three_le_minBalancedCut {V : Type u_1} {D : Type u_2} [Fintype V] [DecidableEq V] [Fintype D] [DecidableEq D] (G : RotationMap V D) : G.edgeExpansion * ↑(Fintype.card V) / 3 ≤ ↑(Multigraph.minBalancedCut G.edgeEnds)

Edge expansion bounds the expansion of Ben-Sasson and Wigderson: h(G) |V| / 3 ≤ e(G).

theorem Cslib.RotationMap.connected_toSimpleGraph_of_edgeExpansion_pos {V : Type u_1} {D : Type u_2} [Fintype V] [DecidableEq V] [Fintype D] (G : RotationMap V D) (hG : 0 < G.edgeExpansion) : G.toSimpleGraph.Connected

A rotation map of positive edge expansion is connected.