Gaussian vertex layouts of multigraphs

Lay out a loopless multigraph G of maximum degree d by Gaussian vertex scores (Cslib.Circuits.Frontier.Gaussian.vertexScore), sorting the vertices by score (Cslib.Circuits.Frontier.Multigraph.exists_width_le_of_vertexScore). The kernel rows are those of the underlying simple graph, while the crossing events are indexed by the edges of G, so parallel edges count with multiplicity.

Fix the grid -T, -T + δ, ..., T of M windows of width δ = 2T / M. Four families of counts control the frontiers: the edges crossed at each grid threshold, the vertices scoring in each window, and the vertices scoring in each tail. Each is a count of local events, which concentrates by the second-moment bound, so for large |V| one sample keeps all of them within ε |V| of their means (Cslib.Circuits.Frontier.Gaussian.exists_multi_vertex_sample). An edge is crossed with probability at most arccos ρ / π, a vertex scores in a window with probability at most δ / √(2π) and in a tail with probability at most 1 / T ^ 2. As the parameters improve, the width is at most vertexCoefficient d · |E| + ξ |V| for every ξ > 0 (Cslib.Circuits.Frontier.Gaussian.exists_width_le_vertexCoefficient).

Main results

• Cslib.Circuits.Frontier.Gaussian.exists_multi_vertex_sample: a good sample.
• Cslib.Circuits.Frontier.Gaussian.exists_width_le_vertexCoefficient: Gaussian vertex layouts of large loopless multigraphs of maximum degree d.

theorem Cslib.Circuits.Frontier.Gaussian.exists_multi_vertex_sample {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {q : ℝ} [Finite V] [Finite E] (hloop : G.Loopless) {d : ℕ} (hd : 2 ≤ d) (hdeg : G.MaxDegreeLE d) (hq : 0 ≤ q) (R : ℕ) {ρ : ℝ} (hρ : ρ ≤ 2 * q / (1 + q ^ 2) - ↑d * ((↑d - 1) * q ^ 2) ^ R) {T ε : ℝ} (hT : 0 < T) (hε : 0 < ε) {M : ℕ} (hM : 0 < M) (large : (↑M * (↑d + 1) + 2) * ↑(vertexOverlap d R) / ε ^ 2 < ↑(Nat.card V)) : ∃ (σ : Layout V), ↑(G.width σ) ≤ Real.arccos ρ / Real.pi * ↑(Nat.card E) + ↑(Nat.card V) * (↑d / T ^ 2 + ↑d * (2 * T / ↑M) / √(2 * Real.pi) + (↑d + 1) * ε)

A good sample. Let G be a loopless multigraph of maximum degree d ≥ 2, and let ρ be at most the truncated kernel bound 2 q / (1 + q ^ 2) - d ((d - 1) q ^ 2) ^ R. If G has more than (M (d + 1) + 2) vertexOverlap d R / ε ^ 2 vertices, some sample of the Gaussian vertex scores gives a layout of width at most (arccos ρ / π) |E| + |V| (d / T ^ 2 + d (2T / M) / √(2π) + (d + 1) ε).

theorem Cslib.Circuits.Frontier.Gaussian.exists_width_le_vertexCoefficient {d : ℕ} (hd : 2 ≤ d) {ξ : ℝ} (hξ : 0 < ξ) : ∃ (N₀ : ℕ), ∀ (V : Type u_3) (E : Type u_4) [Finite V] [inst : Finite E] (G : Multigraph V E), G.Loopless → G.MaxDegreeLE d → N₀ < Nat.card V → ∃ (σ : Layout V), ↑(G.width σ) ≤ vertexCoefficient d * ↑(Nat.card E) + ξ * ↑(Nat.card V)

Gaussian vertex layouts of multigraphs. For every ξ > 0, every large enough loopless multigraph of maximum degree d ≥ 2 has a layout of width at most vertexCoefficient d · |E| + ξ |V|, parallel edges counted with multiplicity.