Tools for layout bounds

This file collects the facts shared by the proofs of instances of the layout hypothesis Cslib.Circuits.Frontier.LayoutBound: the subadditivity of edge cuts, the cut-counting identity for disjoint sets, the handshake lemma for multigraphs, layouts that follow an injective key, and the absorption of logarithmic error terms into the layout hypothesis.

Main results

• Cslib.Circuits.Frontier.Multigraph.ncard_edgeCut_union_add: the cut of a disjoint union S ∪ T together with twice the edges between S and T makes up the cuts of S and of T.
• Cslib.Circuits.Frontier.Multigraph.edgeCut_nonempty: in a connected multigraph, some edge leaves every set of vertices other than the empty set and the whole vertex set.
• Cslib.Circuits.Frontier.Multigraph.sum_ncard_incidenceSet: the handshake lemma.
• Cslib.Circuits.Frontier.Layout.exists_lt_iff: a layout ordered by an injective key.
• Cslib.Circuits.Frontier.LayoutBound.mono: a larger coefficient gives a weaker layout bound.
• Cslib.Circuits.Frontier.LayoutBound.of_natLog: error terms D log₂ |V| are absorbed into the layout hypothesis.

theorem Cslib.Circuits.Frontier.exists_natLog_le_mul_add {ε : ℝ} (hε : 0 < ε) : ∃ (K : ℝ), ∀ (N : ℕ), ↑(Nat.log 2 N) ≤ ε * ↑N + K

log₂ N is at most ε N plus a constant, for every ε > 0.

Edge cuts

theorem Cslib.Circuits.Frontier.Multigraph.edgeCut_union_subset {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (S T : Set V) : G.edgeCut (S ∪ T) ⊆ G.edgeCut S ∪ G.edgeCut T

Edge cuts are subadditive.

theorem Cslib.Circuits.Frontier.Multigraph.ncard_edgeCut_union_le {V : Type u_1} {E : Type u_2} (G : Multigraph V E) [Finite E] (S T : Set V) : (G.edgeCut (S ∪ T)).ncard ≤ (G.edgeCut S).ncard + (G.edgeCut T).ncard

theorem Cslib.Circuits.Frontier.Multigraph.ncard_edgeCut_union_add {V : Type u_1} {E : Type u_2} (G : Multigraph V E) [Finite E] {S T : Set V} (h : Disjoint S T) : (G.edgeCut (S ∪ T)).ncard + 2 * (G.edgeCut S ∩ G.edgeCut T).ncard = (G.edgeCut S).ncard + (G.edgeCut T).ncard

The cut of a disjoint union. The edges between S and T lie in the cuts of both S and T, but not in the cut of S ∪ T.

theorem Cslib.Circuits.Frontier.Multigraph.edgeCut_singleton {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (hG : G.Loopless) (v : V) : G.edgeCut {v} = G.incidenceSet v

In a loopless multigraph, the edges leaving a single vertex are the edges at it.

theorem Cslib.Circuits.Frontier.Multigraph.edgeCut_nonempty {V : Type u_1} {E : Type u_2} {G : Multigraph V E} (hG : G.toSimpleGraph.Connected) {S : Set V} {u v : V} (hu : u ∈ S) (hv : v ∉ S) : (G.edgeCut S).Nonempty

In a connected multigraph, some edge leaves every set of vertices other than the empty set and the whole vertex set.

theorem Cslib.Circuits.Frontier.Multigraph.sum_ncard_incidenceSet {V : Type u_1} {E : Type u_2} (G : Multigraph V E) [Fintype V] [Finite E] (hG : G.Loopless) : ∑ v : V, (G.incidenceSet v).ncard = 2 * Nat.card E

The handshake lemma. In a finite loopless multigraph, the numbers of edges at the vertices add up to twice the number of edges.

theorem Cslib.Circuits.Frontier.Multigraph.width_le_card {V : Type u_1} {E : Type u_2} (G : Multigraph V E) [Finite E] (π : Layout V) : G.width π ≤ Nat.card E

No layout is wider than the number of edges.

Layouts following a key

theorem Cslib.Circuits.Frontier.Layout.exists_lt_iff {V : Type u_1} [Finite V] {α : Type u_2} [LinearOrder α] {f : V → α} (hf : Function.Injective f) : ∃ (π : Layout V), ∀ (v w : V), π v < π w ↔ f v < f w

Layouts following a key. Listing the vertices in increasing order of an injective key gives a layout ordered by the key.

theorem Cslib.Circuits.Frontier.Layout.initial_eq_of_lt_iff {V : Type u_1} {α : Type u_2} [LinearOrder α] {f : V → α} {π : Layout V} (hπ : ∀ (v w : V), π v < π w ↔ f v < f w) {t : ℕ} (ht : t < Nat.card V) : π.initial t = {v : V | f v < f ((Equiv.symm π) ⟨t, ht⟩)}

The first t vertices of a layout ordered by a key are those whose key is less than that of the vertex numbered t.

The layout hypothesis

theorem Cslib.Circuits.Frontier.LayoutBound.mono {d : ℕ} {A A' : ℝ} (h : LayoutBound d A) (hAA' : A ≤ A') : LayoutBound d A'

A larger coefficient gives a weaker layout bound.

theorem Cslib.Circuits.Frontier.LayoutBound.of_natLog {d D : ℕ} {A : ℝ} (h : ∀ η > 0, ∃ (C : ℝ), ∀ (V E : Type) [Finite V] [inst : Finite E] (G : Multigraph V E), G.toSimpleGraph.Connected → G.Loopless → G.MaxDegreeLE d → ∃ (π : Layout V), ↑(G.width π) ≤ (A + η) * ↑G.cycleRank + ↑D * ↑(Nat.log 2 (Nat.card V)) + C) : LayoutBound d A

Logarithmic error terms. To prove the layout hypothesis it suffices to find, for every η > 0, layouts of width at most (A + η) β₁ + D log₂ |V| + C, for a constant C: the term D log₂ |V| is at most η |V| plus a constant.