Gaussian vertex layouts with parallel edges #
The radial kernels use a simple support graph. Events are indexed by multigraph edges, so their expectations and variances retain multiplicity. Bounded multigraph degree bounds both dependence overlap and the cost of moving a vertex across a threshold.
theorem
Complexity.Frontier.Gaussian.multi_edge_overlap_le
{W E : Type}
[Fintype W]
[Fintype E]
(H : SimpleGraph W)
[DecidableRel H.Adj]
(G : Multigraph W E)
{d : ℕ}
(hd : 2 ≤ d)
(degree : ∀ (v : W), H.degree v ≤ d)
(multiDegree : G.MaxDegreeLE d)
(adj : ∀ (e : E), H.Adj (G.src e) (G.tgt e))
(R : ℕ)
(e : E)
:
Edge-event overlap is bounded even with repeated endpoint pairs.
theorem
Complexity.Frontier.Gaussian.exists_multi_vertex_sample
{W E : Type}
[Fintype W]
[Fintype E]
(H : SimpleGraph W)
[DecidableRel H.Adj]
(G : Multigraph W E)
{d : ℕ}
(hd : 2 ≤ d)
(degree : ∀ (v : W), H.degree v ≤ d)
(multiDegree : G.MaxDegreeLE d)
(adj : ∀ (e : E), H.Adj (G.src e) (G.tgt e))
{q : ℝ}
(hq : 0 ≤ q)
(R : ℕ)
{ρ : ℝ}
(hρ0 : -1 < ρ)
(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 < ↑(Fintype.card W))
:
Simultaneous control of all grid cuts, vertex windows, and tails. The sample determines an actual vertex ordering, with no distinct-score assumption.
theorem
Complexity.Frontier.Gaussian.multigraph_vertexLayout_bound
{d : ℕ}
(hd : 2 ≤ d)
{ξ : ℝ}
(hξ : 0 < ξ)
:
∃ (N₀ : ℕ),
∀ (W E : Type) [inst : Fintype W] [inst_1 : Fintype E] (G : Multigraph W E),
G.Loopless →
G.MaxDegreeLE d →
N₀ < Fintype.card W →
∃ (key : W → ℕ),
Function.Injective key ∧ ∀ (t : ℕ),
↑(G.crossingFinset {v : W | key v < t}).card ≤ vertexCoefficient d * ↑(Fintype.card E) + ξ * ↑(Fintype.card W)
The Gaussian per-edge layout coefficient holds for loopless multigraphs as well.