Lax17.Expansion

Edge expansion and cut-matching transcripts

concepts/Lax17/Expansion.lean · lax-17

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Definition

The edge boundary of a vertex set consists of the graph edges with exactly one endpoint in the set. A finite graph is an $(a/b)$ -edge-expander when every set containing at most half of the vertices has boundary at least $(a/b)$ times its size.

A cut-matching transcript is a finite list of perfect matchings across bisections. Its boundary count retains the round of each matching edge, so parallel copies contributed in different rounds are counted separately.

Lean source view on GitHub

1	import Mathlib.Combinatorics.SimpleGraph.DeleteEdges
2	import Lax17.Degree
3
4	/-!
5	---
6	title: Edge expansion and cut-matching transcripts
7	type: definition
8	---
9	The edge boundary of a vertex set consists of the graph edges with exactly one
10	endpoint in the set. A finite graph is an $(a/b)$-edge-expander when every
11	set containing at most half of the vertices has boundary at least
12	$(a/b)$ times its size.
13
14	A cut-matching transcript is a finite list of perfect matchings across
15	bisections. Its boundary count retains the round of each matching edge, so
16	parallel copies contributed in different rounds are counted separately.
17	-/
18
19	namespace Lax17.Expansion
20
21	universe u
22
23	open Lax17.Degree
24
25	/-- An unordered pair crosses the vertex set `S`. -/
26	def Crosses {V : Type u} [DecidableEq V]
27	(S : Finset V) (e : Sym2 V) : Prop :=
28	∃ x y : V, e = s(x, y) ∧
29	((x ∈ S ∧ y ∉ S) ∨ (y ∈ S ∧ x ∉ S))
30
31	/-- The finite edge boundary of `S`. -/
32	noncomputable def edgeBoundary {V : Type u} [Fintype V] [DecidableEq V]
33	(G : SimpleGraph V) (S : Finset V) : Finset (Sym2 V) :=
34	@Finset.filter (Sym2 V)
35	(fun e => e ∈ G.edgeSet ∧ Crosses S e)
36	(Classical.decPred _)
37	Finset.univ
38
39	/-- Every set of at most half the vertices expands by a factor of `a / b`. -/
40	def IsEdgeExpander {V : Type u} [Fintype V] [DecidableEq V]
41	(G : SimpleGraph V) (a b : ℕ) : Prop :=
42	0 < a ∧ 0 < b ∧
43	∀ S : Finset V, 0 < S.card → 2 * S.card ≤ Fintype.card V →
44	b * (edgeBoundary G S).card ≥ a * S.card
45
46	/-- A balanced vertex separator `A ∪ B ∪ S = V`, oriented so that `A` is
47	the smaller side and both large sides have size at most two thirds of the
48	graph. -/
49	structure BalancedSeparator {V : Type u} [Fintype V] [DecidableEq V]
50	(G : SimpleGraph V) (A B S : Finset V) : Prop where
51	cover : A ∪ B ∪ S = Finset.univ
52	left_right_disjoint : Disjoint A B
53	left_separator_disjoint : Disjoint A S
54	right_separator_disjoint : Disjoint B S
55	left_card_le_right_card : A.card ≤ B.card
56	right_balanced : 3 * B.card ≤ 2 * Fintype.card V
57	no_edge_left_right :
58	∀ ⦃a b : V⦄, a ∈ A → b ∈ B → ¬ G.Adj a b
59
60	/-- Every balanced separator has size at least `\|V\| / d`, expressed without
61	division. -/
62	def NoSmallBalancedSeparator
63	{V : Type u} [Fintype V] [DecidableEq V]
64	(G : SimpleGraph V) (d : ℕ) : Prop :=
65	∀ ⦃A B S : Finset V⦄, BalancedSeparator G A B S →
66	Fintype.card V ≤ d * S.card
67
68	/-- One cut-matching round: a bisection and a perfect matching from its left
69	half to its right half. -/
70	structure MatchingRound (V : Type u) [Fintype V] [DecidableEq V] where
71	left : Finset V
72	right : Finset V
73	sides_disjoint : Disjoint left right
74	sides_equipotent : left.card = right.card
75	sides_cover : left ∪ right = Finset.univ
76	partner : {x : V // x ∈ left} ≃ {x : V // x ∈ right}
77
78	namespace MatchingRound
79
80	/-- Whether the matching edge starting at `x` crosses `S`. -/
81	def Crosses {V : Type u} [Fintype V] [DecidableEq V]
82	(R : MatchingRound V) (S : Finset V)
83	(x : {x : V // x ∈ R.left}) : Prop :=
84	(x.1 ∈ S ∧ (R.partner x).1 ∉ S) ∨
85	((R.partner x).1 ∈ S ∧ x.1 ∉ S)
86
87	/-- Matching edges of one round that cross `S`, indexed by their endpoint on
88	the left side of the bisection. -/
89	noncomputable def boundary {V : Type u} [Fintype V] [DecidableEq V]
90	(R : MatchingRound V) (S : Finset V) :
91	Finset {x : V // x ∈ R.left} :=
92	@Finset.filter {x : V // x ∈ R.left}
93	(R.Crosses S) (Classical.decPred _) Finset.univ
94
95	end MatchingRound
96
97	/-- A finite cut-matching transcript. -/
98	abbrev CutMatchingTranscript (V : Type u) [Fintype V] [DecidableEq V] :=
99	List (MatchingRound V)
100
101	namespace CutMatchingTranscript
102
103	/-- Number of matching-edge instances crossing `S`; edges from different
104	rounds are counted with multiplicity. -/
105	noncomputable def edgeBoundaryCount {V : Type u} [Fintype V] [DecidableEq V]
106	(T : CutMatchingTranscript V) (S : Finset V) : ℕ :=
107	(T.map fun R => (R.boundary S).card).sum
108
109	/-- Every nonempty set of at most half the vertices has at least half as many
110	crossing matching-edge instances as vertices. -/
111	def IsHalfEdgeExpander {V : Type u} [Fintype V] [DecidableEq V]
112	(T : CutMatchingTranscript V) : Prop :=
113	∀ S : Finset V, 0 < S.card → 2 * S.card ≤ Fintype.card V →
114	S.card ≤ 2 * T.edgeBoundaryCount S
115
116	end CutMatchingTranscript
117
118	end Lax17.Expansion
119

Builds on

Lax17.Degree

Used by

From Mathlib

Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Community review

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

0 comments

Loading discussion…

Lax Lean Archive

Edge expansion and cut-matching transcripts

Flags

Flag this concept