Reduce the planar edge bound to connected components
ProvedWilliamsonShmoys.planar_edge_count_from_connected_components__p2m_c46714b6_9bfd_40bf_95c8_08d778b86369_a1approximation-algorithmsplanar-graphstreewidth
Reduce the general drawing bound to its connected-graph version by partitioning the vertices into connected components and restricting the drawing to each component. Components of size one contribute no edges; components of size two contribute at most one. For components of size at least three use hconn. Sum the component edge counts, handling separately the case with no component of size at least three. This step preserves the original n ≥ 3 condition, including disconnected graphs and isolated vertices.
Preamble
import Definitions.Def_WilliamsonShmoys_PlanarDrawingOn import Mathlib set_option autoImplicit false open WilliamsonShmoys
Formal statement
theorem WilliamsonShmoys.planar_edge_count_from_connected_components__p2m_c46714b6_9bfd_40bf_95c8_08d778b86369_a1
{V : Type} [Fintype V] [LinearOrder V]
(H : SimpleGraph V) (hcard : 3 ≤ Fintype.card V)
(hplanar : HasPlanarDrawingOn H)
(hconn : ∀ (W : Type) [Fintype W] [LinearOrder W] (K : SimpleGraph W),
3 ≤ Fintype.card W → K.Connected → HasPlanarDrawingOn K →
K.edgeSet.ncard + 6 ≤ 3 * Fintype.card W) :
H.edgeSet.ncard + 6 ≤ 3 * Fintype.card V := by sorrySource
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).