Menger's theorem between vertex sets in multigraphs

Let G : Graph α β be a multigraph with finitely many actual vertices, and let A and B be finite sets of actual vertices. An A–B path runs from a vertex of A to a vertex of B, with no other vertex in either terminal set. A vertex-capacitated packing is a finite indexed family of such paths, repetitions allowed, in which each vertex v, including the endpoints, occurs in at most c v members. A separator may meet A and B; its weight is the sum of the capacities of its vertices.

This file proves that some vertex-capacitated packing and some separator have equal size and weight. At unit capacity it gives pairwise vertex-disjoint paths and a separator of the same cardinality. The terminal sets may be empty or overlap. In particular, a vertex of A ∩ B may give a zero-length path, and every separator contains it. No finiteness assumption is made on the edge set, so loops and arbitrary parallel edges are allowed.

Main results

• Graph.card_le_sum_of_forall_not_reachable_deleteVerts: weak duality for vertex-capacitated packings between vertex sets.
• Graph.exists_paths_setSeparator_sum_eq: vertex-capacitated set-to-set Menger in witness form.
• Graph.exists_paths_setSeparator_card_eq: set-to-set Menger for vertex-disjoint paths.
• Graph.forall_exists_reachable_deleteVerts_iff_exists_paths: the corresponding predicate form.

Attainment is transported from the directed theorem for the bidirected arrow family on V(G). The walk equivalence preserves vertex sequences, paths, and disjointness.

References

• K. Menger, Zur allgemeinen Kurventheorie, Fund. Math. 10 (1927).
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer, 2003, Section 9.1.

Vertex-capacitated packings

theorem Graph.card_le_sum_of_forall_not_reachable_deleteVerts {α : Type u} {β : Type v} {G : Graph α β} [DecidableEq α] {A B : Finset α} (hA : ↑A ⊆ G.vertexSet) {ι : Type u_1} [Fintype ι] {a b : ι → α} {P : (i : ι) → G.Walk (a i) (b i)} (ha : ∀ (i : ι), a i ∈ A) (hb : ∀ (i : ι), b i ∈ B) {c : α → ℕ} (hP : ∀ (x : α), {i : ι | x ∈ (P i).support}.card ≤ c x) {X : Finset α} (hX : ∀ a ∈ A, ∀ b ∈ B, ¬(G.deleteVerts ↑X).Reachable a b) : Fintype.card ι ≤ ∑ x ∈ X, c x

Weak duality for vertex-capacitated set-to-set packings. A family of walks, each from a vertex of A to a vertex of B, in which every vertex v lies on at most c v members, has at most ∑ v ∈ X, c v members whenever deleting X destroys reachability from every vertex of A to every vertex of B.

theorem Graph.exists_paths_setSeparator_sum_eq {α : Type u} {β : Type v} {G : Graph α β} [Finite ↑G.vertexSet] [DecidableEq α] (c : α → ℕ) (A B : Finset α) (hA : ↑A ⊆ G.vertexSet) (hB : ↑B ⊆ G.vertexSet) : ∃ (k : ℕ) (a : Fin k → α) (b : Fin k → α) (P : (i : Fin k) → G.Walk (a i) (b i)) (X : Finset α), (∀ (i : Fin k), a i ∈ A) ∧ (∀ (i : Fin k), b i ∈ B) ∧ (∀ (i : Fin k), (P i).IsPath) ∧ (∀ (i : Fin k), ∀ x ∈ (P i).support, x ≠ a i → x ≠ b i → x ∉ A ∧ x ∉ B) ∧ (∀ (x : α), {i : Fin k | x ∈ (P i).support}.card ≤ c x) ∧ ↑X ⊆ G.vertexSet ∧ (∀ a ∈ A, ∀ b ∈ B, ¬(G.deleteVerts ↑X).Reachable a b) ∧ ∑ x ∈ X, c x = k

Vertex-capacitated Menger's theorem between vertex sets in a multigraph. Let A and B be finite sets of actual vertices of a multigraph with finitely many actual vertices. Some family of k paths, the i-th from a i ∈ A to b i ∈ B with its other vertices in neither terminal set, and some set X of actual vertices satisfy the following: every vertex v lies on at most c v members, deleting X destroys all A–B reachability, and ∑ v ∈ X, c v = k.

Vertex-disjoint paths

theorem Graph.card_le_card_of_forall_not_reachable_deleteVerts {α : Type u} {β : Type v} {G : Graph α β} {A B : Finset α} (hA : ↑A ⊆ G.vertexSet) {ι : Type u_1} [Fintype ι] {a b : ι → α} {P : (i : ι) → G.Walk (a i) (b i)} (ha : ∀ (i : ι), a i ∈ A) (hb : ∀ (i : ι), b i ∈ B) (hP : Pairwise fun (i j : ι) => (P i).support.Disjoint (P j).support) {X : Finset α} (hX : ∀ a ∈ A, ∀ b ∈ B, ¬(G.deleteVerts ↑X).Reachable a b) : Fintype.card ι ≤ X.card

Weak duality for vertex-disjoint set-to-set walks. A family of pairwise vertex-disjoint walks, each from a vertex of A to a vertex of B, has at most #X members whenever deleting X destroys reachability from every vertex of A to every vertex of B.

theorem Graph.exists_paths_setSeparator_card_eq {α : Type u} {β : Type v} {G : Graph α β} [Finite ↑G.vertexSet] (A B : Finset α) (hA : ↑A ⊆ G.vertexSet) (hB : ↑B ⊆ G.vertexSet) : ∃ (k : ℕ) (a : Fin k → α) (b : Fin k → α) (P : (i : Fin k) → G.Walk (a i) (b i)) (X : Finset α), (∀ (i : Fin k), a i ∈ A) ∧ (∀ (i : Fin k), b i ∈ B) ∧ (∀ (i : Fin k), (P i).IsPath) ∧ (∀ (i : Fin k), ∀ x ∈ (P i).support, x ≠ a i → x ≠ b i → x ∉ A ∧ x ∉ B) ∧ (Pairwise fun (i j : Fin k) => (P i).support.Disjoint (P j).support) ∧ ↑X ⊆ G.vertexSet ∧ (∀ a ∈ A, ∀ b ∈ B, ¬(G.deleteVerts ↑X).Reachable a b) ∧ X.card = k

Menger's theorem for vertex-disjoint paths between vertex sets in a multigraph. Let A and B be finite sets of actual vertices of a multigraph with finitely many actual vertices. Some family of k pairwise vertex-disjoint paths, the i-th from a i ∈ A to b i ∈ B with its other vertices in neither terminal set, and some set X of k actual vertices whose deletion destroys all A–B reachability exist.

theorem Graph.forall_exists_reachable_deleteVerts_iff_exists_paths {α : Type u} {β : Type v} {G : Graph α β} [Finite ↑G.vertexSet] (A B : Finset α) (hA : ↑A ⊆ G.vertexSet) (hB : ↑B ⊆ G.vertexSet) (k : ℕ) : (∀ (X : Finset α), X.card < k → ∃ a ∈ A, ∃ b ∈ B, (G.deleteVerts ↑X).Reachable a b) ↔ ∃ (a : Fin k → α) (b : Fin k → α) (P : (i : Fin k) → G.Walk (a i) (b i)), (∀ (i : Fin k), a i ∈ A) ∧ (∀ (i : Fin k), b i ∈ B) ∧ (∀ (i : Fin k), (P i).IsPath) ∧ (∀ (i : Fin k), ∀ x ∈ (P i).support, x ≠ a i → x ≠ b i → x ∉ A ∧ x ∉ B) ∧ Pairwise fun (i j : Fin k) => (P i).support.Disjoint (P j).support

Menger's theorem for vertex-disjoint paths between vertex sets in a multigraph, predicate form. Let A and B be finite sets of actual vertices of a multigraph with finitely many actual vertices. Deleting any set of fewer than k vertices leaves some vertex of B reachable from some vertex of A exactly when there are k pairwise vertex-disjoint A–B paths whose interiors avoid both terminal sets.