Tree separators and path decompositions

A vertex minimizing the sum of distances is a centroid: every component left after deleting it contains at most half the vertices. This supplies the balanced recursion used for logarithmic-width tree decompositions.

theorem Algebraic.Cutwidth.PathDecomposition.Internal.exists_tree_centroid {W : Type} {H : SimpleGraph W} [Fintype W] (tree : H.IsTree) : ∃ (r : W), ∀ (C : (SimpleGraph.induce {w : W | w ≠ r} H).ConnectedComponent), 2 * Fintype.card ↥C ≤ Fintype.card W

theorem Algebraic.Cutwidth.PathDecomposition.Internal.exists_tree_decomposition_of_card_le_pow (k : ℕ) (W : Type) [Fintype W] (H : SimpleGraph W) : H.IsTree → Fintype.card W ≤ 2 ^ k → ∃ (D : PathDecomposition H), ∀ (i : Fin D.length), (D.bag i).card ≤ k + 1

theorem Algebraic.Cutwidth.PathDecomposition.Internal.exists_tree_decomposition {W : Type} {H : SimpleGraph W} [Fintype W] (tree : H.IsTree) : ∃ (D : PathDecomposition H), ∀ (i : Fin D.length), (D.bag i).card ≤ Nat.clog 2 (Fintype.card W) + 1

theorem Algebraic.Cutwidth.PathDecomposition.Internal.exists_forest_decomposition {W : Type} {H : SimpleGraph W} [Fintype W] (forest : H.IsAcyclic) : ∃ (D : PathDecomposition H), ∀ (i : Fin D.length), (D.bag i).card ≤ Nat.clog 2 (Fintype.card W) + 1