Noncomplete graphs and the two largest adjacency eigenvalues

A missing edge gives a vanishing 2x2 principal submatrix of the adjacency matrix. Courant-Fischer on that coordinate plane yields lambda2 G ≥ 0 when G is not complete, and therefore F(A_G) = lambda1 G ^ 2 + lambda2 G ^ 2. The largest eigenvalue is nonnegative for every finite graph, complete or not.

SP13 — A nonedge gives a zero principal 2x2

theorem BollobasNikiforov.adjMatrix_eq_zero_on_nonedge_pair {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {i j : V} (hij : i ≠ j) (hna : ¬G.Adj i j) {a b : V} (ha : a ∈ {i, j}) (hb : b ∈ {i, j}) : SimpleGraph.adjMatrix ℝ G a b = 0

The principal 2x2 submatrix of the adjacency matrix on a nonedge is identically zero.

theorem BollobasNikiforov.dotProduct_mulVec_adjMatrix_eq_zero_of_supported_on_nonedge {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {i j : V} (hij : i ≠ j) (hna : ¬G.Adj i j) {x : V → ℝ} (hx : ∀ v ∉ {i, j}, x v = 0) : x ⬝ᵥ (SimpleGraph.adjMatrix ℝ G).mulVec x = 0

The adjacency quadratic form vanishes on vectors supported on a nonedge.

SP14 — Rayleigh on a 2-dimensional coordinate subspace

noncomputable def BollobasNikiforov.euclInner {n : Type u_2} [Fintype n] (x y : EuclideanSpace ℝ n) : ℝ

Euclidean inner product on coordinate space. Avoids the BollobasNikiforov.inner name clash.

Equations

• BollobasNikiforov.euclInner x y = inner ℝ x y

theorem BollobasNikiforov.euclInner_smul_right {n : Type u_2} [Fintype n] (x y : EuclideanSpace ℝ n) (c : ℝ) : euclInner x (c • y) = c * euclInner x y

theorem BollobasNikiforov.dotProduct_mulVec_eq_sum_eigenvalues₀ {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsHermitian) (x : n → ℝ) : x ⬝ᵥ A.mulVec x = ∑ i : Fin (Fintype.card n), hA.eigenvalues₀ i * euclInner ((⋯.eigenvectorBasis ⋯) i) (WithLp.toLp 2 x) ^ 2

The Euclidean quadratic form expands in the ordered eigenbasis.

theorem BollobasNikiforov.dotProduct_mulVec_le_lambdaSecond_of_orthogonal {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsHermitian) [Nontrivial n] {x : n → ℝ} (hx : ∑ k : n, x k ^ 2 = 1) (horth : euclInner ((⋯.eigenvectorBasis ⋯) ⟨0, ⋯⟩) (WithLp.toLp 2 x) = 0) : x ⬝ᵥ A.mulVec x ≤ lambdaSecond hA

On the orthogonal complement of a top eigenvector, the Rayleigh form is at most lambdaSecond.

theorem BollobasNikiforov.exists_l2_mem_span_single_pair_orthogonal {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsHermitian) [Nontrivial n] {i j : n} (hij : i ≠ j) : ∃ x ∈ Submodule.span ℝ {Pi.single i 1, Pi.single j 1}, ∑ k : n, x k ^ 2 = 1 ∧ euclInner ((⋯.eigenvectorBasis ⋯) ⟨0, ⋯⟩) (WithLp.toLp 2 x) = 0

A unit vector in span {e i, e j} orthogonal to a top eigenvector.

def BollobasNikiforov.rayleighOnSpanPair {n : Type u_2} [Fintype n] [DecidableEq n] (A : Matrix n n ℝ) (i j : n) : Set ℝ

Rayleigh values of unit vectors in span {e i, e j}.

Equations

• BollobasNikiforov.rayleighOnSpanPair A i j = {t : ℝ | ∃ x ∈ Submodule.span ℝ {Pi.single i 1, Pi.single j 1}, ∑ k : n, x k ^ 2 = 1 ∧ t = x ⬝ᵥ A.mulVec x}

theorem BollobasNikiforov.nonempty_rayleighOnSpanPair {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} {i j : n} : (rayleighOnSpanPair A i j).Nonempty

theorem BollobasNikiforov.bddBelow_rayleighOnSpanPair {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} {i j : n} : BddBelow (rayleighOnSpanPair A i j)

theorem BollobasNikiforov.lambdaSecond_ge_sInf_span_single_pair {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsHermitian) [Nontrivial n] {i j : n} (hij : i ≠ j) : sInf (rayleighOnSpanPair A i j) ≤ lambdaSecond hA

SP14. Courant-Fischer comparison on a coordinate 2-plane: lambdaSecond is at least the infimum of the Rayleigh form on span {e i, e j}.

theorem BollobasNikiforov.lambdaSecond_nonneg_of_rayleighOnSpanPair_nonneg {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsHermitian) [Nontrivial n] {i j : n} (hij : i ≠ j) (hnn : ∀ t ∈ rayleighOnSpanPair A i j, 0 ≤ t) : 0 ≤ lambdaSecond hA

If the Rayleigh form is nonnegative on the coordinate 2-plane, then 0 ≤ lambdaSecond.

theorem BollobasNikiforov.lambdaSecond_nonneg_of_quadForm_eq_zero_on_span {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsHermitian) [Nontrivial n] {i j : n} (hij : i ≠ j) (h0 : ∀ x ∈ Submodule.span ℝ {Pi.single i 1, Pi.single j 1}, x ⬝ᵥ A.mulVec x = 0) : 0 ≤ lambdaSecond hA

If the quadratic form vanishes on span {e i, e j}, then 0 ≤ lambdaSecond.

theorem BollobasNikiforov.mem_span_single_pair_support {n : Type u_2} [DecidableEq n] {i j : n} {x : n → ℝ} (hx : x ∈ Submodule.span ℝ {Pi.single i 1, Pi.single j 1}) {v : n} (hvi : v ≠ i) (hvj : v ≠ j) : x v = 0

SP15 — lambda2 G ≥ 0 if G is not complete

theorem BollobasNikiforov.lambda2_eq_lambdaSecond {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Nontrivial V] : lambda2 G = lambdaSecond ⋯

theorem BollobasNikiforov.lambda1_eq_lambdaMax {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Nonempty V] : lambda1 G = lambdaMax ⋯

theorem BollobasNikiforov.lambda2_nonneg {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Nontrivial V] (hG : G ≠ ⊤) : 0 ≤ lambda2 G

SP15. A noncomplete graph on at least two vertices has lambda2 ≥ 0.

SP17 — lambda1 G ≥ 0

theorem BollobasNikiforov.lambda1_nonneg {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Nonempty V] : 0 ≤ lambda1 G

SP17. The largest adjacency eigenvalue is nonnegative.

SP16 — F(A_G) = lambda1^2 + lambda2^2 for noncomplete G

theorem BollobasNikiforov.lambdaSecond_le_lambdaMax {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsHermitian) [Nontrivial n] : lambdaSecond hA ≤ lambdaMax hA

theorem BollobasNikiforov.F_adjMatrix_eq {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Nontrivial V] (hG : G ≠ ⊤) : F ⋯ = lambda1 G ^ 2 + lambda2 G ^ 2

SP16. On a noncomplete graph the positive-part squares in F are lambda1 ^ 2 and lambda2 ^ 2.