Lax12.UniformQuasiWideness

Uniform quasi-wideness

concepts/Lax12/UniformQuasiWideness.lean · lax-12

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Definition

A set A of vertices is distance-r independent in G if any two distinct vertices of A are at distance more than r. A graph class is uniformly quasi-wide if for every radius r there are a threshold function N and a separator bound s such that in every member G, every vertex set A of size at least N(m) contains a distance-r independent subset of size at least m of G − S, for some set S of at most s vertices.

This is Definition 3.1 of Chapter 4 of the source lecture notes (2019/20 edition), where the constants s are called the margins and the functions N the wideness functions.

Lean source view on GitHub

1	import Lax12.GraphClasses
2	import Mathlib.Combinatorics.SimpleGraph.Walk.Basic
3	import Mathlib.Data.Set.Card
4
5	/-!
6	---
7	title: Uniform quasi-wideness
8	type: definition
9	---
10	A set A of vertices is distance-r independent in G if any two
11	distinct vertices of A are at distance more than r. A graph class is
12	uniformly quasi-wide if for every radius r there are a threshold
13	function N and a separator bound s such that in every member G,
14	every vertex set A of size at least N(m) contains a distance-r
15	independent subset of size at least m of G − S, for some set S
16	of at most s vertices.
17
18	This is Definition 3.1 of Chapter 4 of the source lecture notes (2019/20
19	edition), where the constants s are called the margins and the
20	functions N the wideness functions.
21
22	# Formalization notes
23
24	Distance is stated with walks: two vertices are at distance more than
25	`r` exactly when every walk between them is longer than `r`, which needs
26	no metric, connectivity or decidability instance. Deleting a vertex set
27	is modelled by isolating it — `deleteVerts G S` keeps the carrier and
28	drops every edge incident to `S` — so every set in the statement lives
29	in the same vertex type and no subtype plumbing enters the surface.
30	Since the witness satisfies `B ⊆ A \ S`, the isolated vertices are not
31	in `B` and distance-`r` independence in the isolated graph is the same
32	as in the induced subgraph on the complement of `S`.
33
34	Sets and `Set.ncard` are used throughout, as in the other concepts of
35	this submission. The threshold `N` may depend on the requested size `m`,
36	while the separator bound `s` may not: that uniformity in `s` is the
37	"uniform" of uniform quasi-wideness and is the whole strength of the
38	notion. `DistIndependent` and `deleteVerts` are stated for an arbitrary
39	vertex type, since both are pointwise notions and the proofs consuming
40	them work over intermediate carriers.
41	-/
42
43	namespace Lax12.UniformQuasiWideness
44
45	open Lax12.GraphClasses
46
47	/-- A set of vertices is distance-`r` independent in `G` when every walk
48	between two distinct members is longer than `r`. -/
49	def DistIndependent {V : Type*} (G : SimpleGraph V) (r : ℕ) (A : Set V) : Prop :=
50	A.Pairwise fun u v => ∀ p : G.Walk u v, r < p.length
51
52	/-- `G` with the vertices of `S` isolated: every edge incident to `S` is
53	removed and the vertex type is unchanged. This models `G − S`. -/
54	def deleteVerts {V : Type*} (G : SimpleGraph V) (S : Set V) : SimpleGraph V where
55	Adj u v := G.Adj u v ∧ u ∉ S ∧ v ∉ S
56	symm _ _ h := ⟨h.1.symm, h.2.2, h.2.1⟩
57	loopless := ⟨fun v h => G.loopless.irrefl v h.1⟩
58
59	/-- A graph class is uniformly quasi-wide if for every radius `r` there
60	are a threshold function `N` and a separator bound `s` such that in
61	every member, every vertex set of size at least `N m` contains a
62	distance-`r` independent subset of size at least `m` after deleting at
63	most `s` vertices. -/
64	def UniformlyQuasiWide (C : GraphClass) : Prop :=
65	∀ r : ℕ, ∃ (N : ℕ → ℕ) (s : ℕ),
66	∀ (m n : ℕ) (G : SimpleGraph (Fin n)), C n G →
67	∀ A : Set (Fin n), N m ≤ A.ncard →
68	∃ S B : Set (Fin n),
69	S.ncard ≤ s ∧ B ⊆ A \ S ∧ m ≤ B.ncard ∧
70	DistIndependent (deleteVerts G S) r B
71
72	end Lax12.UniformQuasiWideness
73

Formalization notes

Distance is stated with walks: two vertices are at distance more than $r$ exactly when every walk between them is longer than $r$ , which needs no metric, connectivity or decidability instance. Deleting a vertex set is modelled by isolating it — $deleteVerts G S$ keeps the carrier and drops every edge incident to $S$ — so every set in the statement lives in the same vertex type and no subtype plumbing enters the surface. Since the witness satisfies $B ⊆ A \ S$ , the isolated vertices are not in $B$ and distance- $r$ independence in the isolated graph is the same as in the induced subgraph on the complement of $S$ .

Sets and $Set.ncard$ are used throughout, as in the other concepts of this submission. The threshold $N$ may depend on the requested size $m$ , while the separator bound $s$ may not: that uniformity in $s$ is the "uniform" of uniform quasi-wideness and is the whole strength of the notion. $DistIndependent$ and $deleteVerts$ are stated for an arbitrary vertex type, since both are pointwise notions and the proofs consuming them work over intermediate carriers.

Builds on

Lax12.GraphClasses

Used by

From Mathlib

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

Uniform quasi-wideness

Flags

Flag this concept