Lax9.MergeWidth

Merge-Width

concepts/Lax9/MergeWidth.lean · lax-9

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Definition

A merge sequence of a finite simple graph consists of a coarsening sequence of partitions and a monotone sequence of graphs of resolved pairs. At each step, adjacency is uniform on the unresolved pairs between any two parts. The radius- $r$ width of a merge sequence is the maximum number of parts of the preceding partition met by a radius- $r$ ball in the graph of resolved pairs. The radius- $r$ merge-width of a graph is the minimum width of a merge sequence of that graph. A graph class has bounded merge-width if these parameters are bounded by a function of $r$ throughout the class.

Lean source view on GitHub

1	import Mathlib
2
3	/-!
4	---
5	title: Merge-Width
6	type: definition
7	---
8	A merge sequence of a finite simple graph consists of a coarsening sequence of
9	partitions and a monotone sequence of graphs of resolved pairs. At each step,
10	adjacency is uniform on the unresolved pairs between any two parts. The
11	radius- $r$ width of a merge sequence is the maximum number of parts of the
12	preceding partition met by a radius- $r$ ball in the graph of resolved pairs.
13	The radius- $r$ merge-width of a graph is the minimum width of a merge sequence
14	of that graph. A graph class has bounded merge-width if these parameters are
15	bounded by a function of $r$ throughout the class.
16	-/
17
18	namespace Lax9.MergeWidth
19
20	open scoped Classical
21
22	universe u
23
24	variable {V : Type u} [Fintype V]
25
26	/-- The resolved ball of radius $r$ around $v$ in a graph $H$ :
27	the set of vertices reachable from $v$ by a walk of length at most $r$ .
28	In the paper this is applied to the graph $(V, Rᵢ)$ of resolved pairs. -/
29	def resolvedBall (H : SimpleGraph V) (r : ℕ) (v : V) : Set V :=
30	{u \| ∃ w : H.Walk v u, w.length ≤ r}
31
32	/--
33	A merge sequence for a finite simple graph $G$ is a sequence
34	$(P₁, R₁), …, (P_length, R_length)$ where:
35
36	* each $part i$ is a partition of $V(G)$ (encoded as a $Setoid$ ), with $part 1$
37	the partition into singletons ( $⊥$ ) and $part length$ the trivial partition
38	with one part ( $⊤$ );
39	* the partitions are coarsening: $part i ≤ part j$ for $i ≤ j$
40	(recall that for setoids a coarser partition is a larger relation);
41	* each $resolved i$ is the graph $(V, Rᵢ)$ of resolved pairs, and these are
42	monotone: $resolved i ≤ resolved j$ for $i ≤ j$ ;
43	* (uniformity) for any two parts $A, B$ of $part i$ , the unresolved pairs
44	between $A$ and $B$ (pairs $xy ∉ Rᵢ$ ) are either all edges or all non-edges of
45	$G$ .
46	-/
47	structure MergeSeq (G : SimpleGraph V) where
48	/-- The number $m$ of steps of the sequence. -/
49	length : ℕ
50	/-- The sequence is nonempty. -/
51	one_le_length : 1 ≤ length
52	/-- The partition $Pᵢ$ at step $i$ (as a setoid on the vertices). -/
53	part : ℕ → Setoid V
54	/-- The graph $(V, Rᵢ)$ of resolved pairs at step $i$ . -/
55	resolved : ℕ → SimpleGraph V
56	/-- $P₁$ is the partition into singletons. -/
57	part_one : part 1 = ⊥
58	/-- $P_m$ is the trivial partition with a single part. -/
59	part_length : part length = ⊤
60	/-- The partitions get coarser. -/
61	part_mono : ∀ ⦃i j⦄, 1 ≤ i → i ≤ j → j ≤ length → part i ≤ part j
62	/-- The sets of resolved pairs are monotone. -/
63	resolved_mono : ∀ ⦃i j⦄, 1 ≤ i → i ≤ j → j ≤ length → resolved i ≤ resolved j
64	/-- Uniformity: unresolved pairs between two parts are all edges or all
65	non-edges. -/
66	uniform : ∀ ⦃i⦄, 1 ≤ i → i ≤ length → ∀ ⦃x x' y y' : V⦄,
67	(part i).r x x' → (part i).r y y' → x ≠ y → x' ≠ y' →
68	¬ (resolved i).Adj x y → ¬ (resolved i).Adj x' y' →
69	(G.Adj x y ↔ G.Adj x' y')
70
71	namespace MergeSeq
72
73	variable {G : SimpleGraph V}
74
75	/-- The number of parts of $part (i-1)$ that are accessible from $v$ by a
76	walk of length at most $r$ in the resolved graph $resolved i$ . (Note the
77	intentional mismatch of indices $Pᵢ₋₁$ versus $Rᵢ$ .) -/
78	noncomputable def numAccessible (S : MergeSeq G) (r i : ℕ) (v : V) : ℕ :=
79	Set.ncard ((fun u => Quotient.mk (S.part (i - 1)) u) '' resolvedBall (S.resolved i) r v)
80
81	/-- The radius- $r$ width of a merge sequence: the maximum over all steps
82	$i ≥ 2$ and vertices $v$ of the number of parts of $Pᵢ₋₁$ accessible from $v$
83	within distance $r$ in $(V, Rᵢ)$ . -/
84	noncomputable def width (S : MergeSeq G) (r : ℕ) : ℕ :=
85	(Finset.Icc 2 S.length).sup fun i => Finset.univ.sup fun v => S.numAccessible r i v
86
87	end MergeSeq
88
89	/-- The radius- $r$ merge-width $mwᵣ(G)$ of a graph $G$ : the minimum
90	radius- $r$ width over all merge sequences of $G$ . -/
91	noncomputable def mergeWidth (r : ℕ) (G : SimpleGraph V) : ℕ :=
92	sInf {w \| ∃ S : MergeSeq G, S.width r = w}
93
94	/-- A graph class: a property of finite simple graphs. -/
95	def GraphClass : Type 1 := ∀ ⦃V : Type⦄ [Fintype V], SimpleGraph V → Prop
96
97	/-- A class $C$ has bounded merge-width if there is a function $f$ such that
98	every $G ∈ C$ satisfies $mwᵣ(G) ≤ f(r)$ for all radii $r$ . -/
99	def BoundedMergeWidth (C : GraphClass) : Prop :=
100	∃ f : ℕ → ℕ, ∀ ⦃V : Type⦄ [Fintype V] (G : SimpleGraph V), C G → ∀ r, mergeWidth r G ≤ f r
101
102	end Lax9.MergeWidth
103

Builds on

none

Used by

From Mathlib

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

Merge-Width

Flags

Flag this concept