The Bollobás--Nikiforov inequality #
This file exposes the statement of Conjecture conj:BN in docs/sol.tex.
Adjacency eigenvalues are ordered nonincreasingly and counted with algebraic
multiplicity. Completeness is G = ⊤; the hypothesis G ≠ ⊤ is the paper's
noncomplete assumption. [Nontrivial V] is the paper's n ≥ 2.
theorem
BollobasNikiforov.lambda1_sq_add_lambda2_sq_le
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
[Nontrivial V]
(hG : G ≠ ⊤)
:
Every finite noncomplete simple undirected graph on at least two vertices
satisfies λ₁(G)² + λ₂(G)² ≤ 2 (1 - 1/ω(G)) |E(G)|.