nothing to prove
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- width of a merge sequence is the maximum number of parts of the preceding partition met by a radius- ball in the graph of resolved pairs. The radius- 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 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 |