Layouts of disconnected graphs

The layout hypothesis Frontier.LayoutBound is stated for connected graphs. A disconnected graph is laid out one connected component after another, each component by the layout hypothesis. Every frontier of the result lies inside a single component, and is bounded in terms of the cycle rank of that component alone.

A set of vertices W is closed when no edge leaves it: G.cut W = ∅. The cycle rank of a closed set is |E(W)| + 1 - |W|, where E(W) are the edges with an endpoint in W (Frontier.Multigraph.cycleRankOn). Connected components are closed, and a closed set is the disjoint union of the components of its vertices. Adding a disjoint closed set to a set of vertices does not change its cut (Frontier.Multigraph.cut_union_of_cut_eq_empty), so the frontiers of the concatenated layout are those of the layouts of the components.

Main definitions

• Frontier.Multigraph.cycleRankOn: the cycle rank of a set of vertices.
• Frontier.Multigraph.component: the connected component of a vertex.
• Frontier.Multigraph.induce: the subgraph induced on a set of vertices.

Main results

• Frontier.Multigraph.cut_union_of_cut_eq_empty: closed sets do not change cuts.
• Frontier.Multigraph.connected_induce_component: components are connected.
• Frontier.LayoutBound.exists_layout_componentwise: under the layout hypothesis, every loopless graph of maximum degree d has a layout in which the vertex processed at each step lies in a closed set W with at least |W| - 1 edges that contains both frontiers of the step, and both frontiers are at most (A + η) β₁(W) + η |V| + C.

noncomputable def Complexity.Frontier.Multigraph.cycleRankOn {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (W : Set V) : ℕ

The truncated expression |E(W)| + 1 - |W|, where E(W) are the edges with an endpoint in W. For a nonempty closed, connected set it is the number of independent cycles of the subgraph spanned by W; it need not be additive over components.

Equations

• G.cycleRankOn W = (G.touching W).ncard + 1 - W.ncard

Closed sets

theorem Complexity.Frontier.Multigraph.cut_eq_empty_iff {V : Type u_1} {E : Type u_2} (G : Multigraph V E) {W : Set V} : G.cut W = ∅ ↔ ∀ (e : E), G.src e ∈ W ↔ G.tgt e ∈ W

A set of vertices is closed when every edge has either both endpoints in it or none.

theorem Complexity.Frontier.Multigraph.cut_subset_touching {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (L : Set V) : G.cut L ⊆ G.touching L

Every edge of the cut of L has an endpoint in L.

theorem Complexity.Frontier.Multigraph.touching_mono {V : Type u_1} {E : Type u_2} (G : Multigraph V E) {L M : Set V} (h : L ⊆ M) : G.touching L ⊆ G.touching M

A larger set of vertices touches more edges.

theorem Complexity.Frontier.Multigraph.mem_of_reflTransGen {V : Type u_1} {E : Type u_2} (G : Multigraph V E) {W : Set V} (hW : G.cut W = ∅) {u v : V} (huv : Relation.ReflTransGen G.Adj u v) (hu : u ∈ W) : v ∈ W

Walks do not leave closed sets.

theorem Complexity.Frontier.Multigraph.cut_union_of_cut_eq_empty {V : Type u_1} {E : Type u_2} (G : Multigraph V E) {K L : Set V} (hK : G.cut K = ∅) (h : Disjoint K L) : G.cut (K ∪ L) = G.cut L

Closed sets do not change cuts. Adding a closed set K to a set L disjoint from it does not change the cut of L.

theorem Complexity.Frontier.Multigraph.cut_diff_eq_empty {V : Type u_1} {E : Type u_2} (G : Multigraph V E) {K W : Set V} (hK : G.cut K = ∅) (hW : G.cut W = ∅) : G.cut (K \ W) = ∅

The difference of two closed sets is closed.

Connected components

def Complexity.Frontier.Multigraph.component {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (v : V) : Set V

The connected component of a vertex v: the vertices joined to v by a walk.

Equations

• G.component v = {u : V | Relation.ReflTransGen G.Adj v u}

theorem Complexity.Frontier.Multigraph.mem_component_self {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (v : V) : v ∈ G.component v

Every vertex lies in its own component.

theorem Complexity.Frontier.Multigraph.cut_component {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (v : V) : G.cut (G.component v) = ∅

Connected components are closed.

theorem Complexity.Frontier.Multigraph.component_subset {V : Type u_1} {E : Type u_2} (G : Multigraph V E) {W : Set V} (hW : G.cut W = ∅) {v : V} (hv : v ∈ W) : G.component v ⊆ W

A closed set contains the connected component of each of its vertices.

Induced subgraphs

def Complexity.Frontier.Multigraph.induce {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (W : Set V) : Multigraph ↑W { e : E // G.src e ∈ W ∧ G.tgt e ∈ W }

The subgraph induced on a set of vertices W: the edges with both endpoints in W.

Equations

• G.induce W = { src := fun (e : { e : E // G.src e ∈ W ∧ G.tgt e ∈ W }) => ⟨G.src ↑e, ⋯⟩, tgt := fun (e : { e : E // G.src e ∈ W ∧ G.tgt e ∈ W }) => ⟨G.tgt ↑e, ⋯⟩ }

theorem Complexity.Frontier.Multigraph.Loopless.induce {V : Type u_1} {E : Type u_2} {G : Multigraph V E} (hG : G.Loopless) (W : Set V) : (G.induce W).Loopless

Induced subgraphs of loopless graphs are loopless.

theorem Complexity.Frontier.Multigraph.MaxDegreeLE.induce {V : Type u_1} {E : Type u_2} {G : Multigraph V E} [Finite E] {d : ℕ} (hG : G.MaxDegreeLE d) (W : Set V) : (G.induce W).MaxDegreeLE d

Induced subgraphs have no larger degrees.

theorem Complexity.Frontier.Multigraph.connected_induce_component {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (v : V) : (G.induce (G.component v)).Connected

Components are connected.

theorem Complexity.Frontier.Multigraph.touching_eq_of_cut_eq_empty {V : Type u_1} {E : Type u_2} (G : Multigraph V E) {W : Set V} (hW : G.cut W = ∅) : G.touching W = {e : E | G.src e ∈ W ∧ G.tgt e ∈ W}

The edges touching a closed set W are the edges of the subgraph induced on W.

theorem Complexity.Frontier.Multigraph.cycleRank_induce {V : Type u_1} {E : Type u_2} (G : Multigraph V E) {W : Set V} (hW : G.cut W = ∅) : (G.induce W).cycleRank = G.cycleRankOn W

The subgraph induced on a closed set W has the cycle rank of W.

theorem Complexity.Frontier.Multigraph.ncard_le_ncard_touching_add_one {V : Type u_1} {E : Type u_2} (G : Multigraph V E) [Finite E] {W : Set V} (hW : G.cut W = ∅) (hc : (G.induce W).Connected) : W.ncard ≤ (G.touching W).ncard + 1

A closed set W spanning a connected subgraph has at least |W| - 1 edges, so its cycle rank |E(W)| + 1 - |W| involves no truncation.

theorem Complexity.Frontier.Multigraph.cut_image_val {V : Type u_1} {E : Type u_2} (G : Multigraph V E) {W : Set V} (hW : G.cut W = ∅) (S : Set ↑W) : G.cut (Subtype.val '' S) = Subtype.val '' (G.induce W).cut S

On a closed set W, the cuts of the induced subgraph are the cuts of G.

Laying out components one after another

theorem Complexity.Frontier.LayoutBound.exists_layout_componentwise {d : ℕ} {A : ℝ} (h : LayoutBound d A) {η : ℝ} (hη : 0 < η) : ∃ (C : ℝ), ∀ (V E : Type) [Finite V] [Finite E] (G : Multigraph V E), G.Loopless → G.MaxDegreeLE d → ∃ (π : Layout V), ∀ (t : ℕ) (ht : t < Nat.card V), ∃ (W : Set V), (Equiv.symm π) ⟨t, ht⟩ ∈ W ∧ G.cut W = ∅ ∧ W.ncard ≤ (G.touching W).ncard + 1 ∧ G.cut (π.initial t) ⊆ G.touching W ∧ G.cut (π.initial (t + 1)) ⊆ G.touching W ∧ ↑(G.cut (π.initial t)).ncard ≤ (A + η) * ↑(G.cycleRankOn W) + η * ↑(Nat.card V) + C ∧ ↑(G.cut (π.initial (t + 1))).ncard ≤ (A + η) * ↑(G.cycleRankOn W) + η * ↑(Nat.card V) + C

Layouts of disconnected graphs. Under the layout hypothesis for maximum degree d, every loopless graph of maximum degree d, connected or not, has a layout such that at every step t the vertex processed lies in a closed set W with at least |W| - 1 edges (a connected component), both frontiers of the step lie among the edges of W, and both are at most (A + η) β₁(W) + η |V| + C.