Catalog/Sparsity/UniformQuasiWideness/Contract.lean

1	import Mathlib.Combinatorics.SimpleGraph.Walk.Basic
2	import Catalog.Sparsity.Preliminaries.Contract
3
4	open Catalog.Sparsity.Preliminaries
5
6	namespace Catalog.Sparsity.UniformQuasiWideness
7
8	/-- A set `A` of vertices is distance-`r` independent in `G` when every two
9	distinct vertices in `A` have no walk of length ≤ `r` between them. -/
10	def DistIndependent {V : Type} (G : SimpleGraph V) (r : ℕ) (A : Set V) : Prop :=
11	A.Pairwise (fun u v => ∀ (p : G.Walk u v), r < p.length)
12
13	/-- `deleteVerts G S` removes all edges incident to vertices in `S`, keeping
14	the vertex type `V` unchanged. This models `G - S`. -/
15	def deleteVerts {V : Type} (G : SimpleGraph V) (S : Set V) : SimpleGraph V where
16	Adj u v := G.Adj u v ∧ u ∉ S ∧ v ∉ S
17	symm _ _ h := ⟨h.1.symm, h.2.2, h.2.1⟩
18	loopless := ⟨fun v h => G.loopless.irrefl v h.1⟩
19
20	/-- A class `C` of graphs is uniformly quasi-wide if for every radius `r`
21	there exist a threshold function `N` and a separator size bound `s` such
22	that in every graph `G ∈ C`, every vertex set `A` of size at least `N(m)`
23	contains a subset `B` of size at least `m` that is distance-`r` independent
24	after removing at most `s` vertices. (Def 3.1) -/
25	def UniformlyQuasiWide (C : GraphClass) : Prop :=
26	∀ r : ℕ, ∃ (N : ℕ → ℕ) (s : ℕ),
27	∀ (m : ℕ) {V : Type} [DecidableEq V] [Fintype V] (G : SimpleGraph V),
28	C G → ∀ (A : Finset V), N m ≤ A.card →
29	∃ (S : Finset V) (B : Finset V),
30	S.card ≤ s ∧
31	↑B ⊆ ↑A \ ↑S ∧
32	m ≤ B.card ∧
33	DistIndependent (deleteVerts G ↑S) r ↑B
34
35	end Catalog.Sparsity.UniformQuasiWideness
36