Combine edge bounds over connected induced subgraphs

Proved

WilliamsonShmoys_edge_bound_from_connected_subtype_bounds__p2m_e9a12d61_586c_475e_b65b_75c2a4e2b868_a3

by Eyal1990 · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

approximation-algorithmsplanar-graphstreewidth

If every connected induced graph on a subtype of at least three vertices satisfies the 3n−6 edge bound, then the whole finite simple graph with at least three vertices satisfies it. The proof partitions vertices into connected components, bounds components of size one or two directly, and sums the bounds.

Preamble

import Mathlib
set_option autoImplicit false

Formal statement

theorem WilliamsonShmoys_edge_bound_from_connected_subtype_bounds__p2m_e9a12d61_586c_475e_b65b_75c2a4e2b868_a3
    {V : Type} [Fintype V] [LinearOrder V]
    (L : SimpleGraph V) (hcard : 3 ≤ Fintype.card V)
    (hlocal : ∀ s : Finset V, 3 ≤ s.card →
      (L.induce (fun v : V => v ∈ s)).Connected →
      (L.induce (fun v : V => v ∈ s)).edgeSet.ncard ≤ 3 * s.card - 6) :
    L.edgeSet.ncard ≤ 3 * Fintype.card V - 6 := by sorry

Source

David P. Williamson and David B. Shmoys, The Design of Approximation Algorithms, Cambridge University Press, 2011, author electronic manuscript, Section 10.2, proof of Theorem 10.11, pp. 270-272. https://doi.org/10.1017/CBO9780511921735. Bounded tree-width of the pieces: Robertson–Seymour (planar graphs of radius r have tree-width at most 3r+1) / Bodlaender (k-outerplanar graphs have tree-width at most 3k-1).

View graph