Ordering the vertices of a multigraph by scores

Sort the vertices of a multigraph of maximum degree d by a real score (Cslib.Circuits.Frontier.Layout.exists_threshold). Fix a grid a, a + δ, ..., a + M δ. The cuts below the grid thresholds and the numbers of vertices scoring in the windows between them bound every frontier of the layout, parallel edges counted separately (Cslib.Circuits.Frontier.Multigraph.ncard_edgeCut_le_grid).

Indeed, let the vertices of P score at most m and the others at least m. If a + i δ ≤ m < a + (i + 1) δ, an edge leaving P either leaves the threshold set {v | score v < a + i δ} too, or has its end in P scoring in the window [a + i δ, a + (i + 1) δ); at most d edges are at each vertex of the window. If m lies below the grid, every edge leaving P is at a vertex scoring below a, and if m lies above it, every such edge is at a vertex scoring at least a + M δ.

Main results

• Cslib.Circuits.Frontier.Multigraph.ncard_edgeCut_le_grid: the cut of a threshold set.
• Cslib.Circuits.Frontier.Multigraph.exists_width_le_of_vertexScore: the layout by a vertex score.

theorem Cslib.Circuits.Frontier.Multigraph.ncard_edgeCut_le_grid {V : Type u_1} {E : Type u_2} (G : Multigraph V E) [Finite V] [Finite E] {d : ℕ} (hd : G.MaxDegreeLE d) (score : V → ℝ) {P : Set V} {m a δ : ℝ} (hP : ∀ v ∈ P, score v ≤ m) (hPc : ∀ v ∉ P, m ≤ score v) (hδ : 0 < δ) (M : ℕ) {B : ℝ} (low : ↑d * ↑{v : V | score v < a}.ncard ≤ B) (high : ↑d * ↑{v : V | a + ↑M * δ ≤ score v}.ncard ≤ B) (mid : ∀ i < M, ↑(G.edgeCut {v : V | score v < a + ↑i * δ}).ncard + ↑d * ↑{v : V | a + ↑i * δ ≤ score v ∧ score v < a + (↑i + 1) * δ}.ncard ≤ B) : ↑(G.edgeCut P).ncard ≤ B

Grid control. Let the vertices of P score at most m and the others at least m. If d times the number of vertices scoring in each tail, and the cut below each grid threshold plus d times the number of vertices scoring in the following window, are at most B, then at most B edges leave P.

theorem Cslib.Circuits.Frontier.Multigraph.exists_width_le_of_vertexScore {V : Type u_1} {E : Type u_2} (G : Multigraph V E) [Finite V] [Finite E] {d : ℕ} (hd : G.MaxDegreeLE d) (score : V → ℝ) {a δ : ℝ} (hδ : 0 < δ) (M : ℕ) {B : ℝ} (low : ↑d * ↑{v : V | score v < a}.ncard ≤ B) (high : ↑d * ↑{v : V | a + ↑M * δ ≤ score v}.ncard ≤ B) (mid : ∀ i < M, ↑(G.edgeCut {v : V | score v < a + ↑i * δ}).ncard + ↑d * ↑{v : V | a + ↑i * δ ≤ score v ∧ score v < a + (↑i + 1) * δ}.ncard ≤ B) : ∃ (π : Layout V), ↑(G.width π) ≤ B

The layout by a vertex score. Under the grid hypotheses of ncard_edgeCut_le_grid, listing the vertices by score gives a layout of width at most B.