Rank-at-most-two spectral slice of a symmetric nonnegative matrix

A symmetric entrywise-nonnegative matrix B has a rank-at-most-two PSD slice X = a uuᵀ + b vvᵀ built from a nonnegative Perron vector for λ_max and, when λ₂ > 0, a unit eigenvector for λ₂ orthogonal to it. This slice satisfies ⟨B, X⟩ = ⟨X, X⟩ = F B and is a Gram matrix of planar vectors in the closed right half-plane. If B is zero-diagonal and supported on E(G), the Motzkin–Straus bound on M X yields F B ≤ turanFactor G * ⟨B, B⟩.

theorem BollobasNikiforov.sum_sq_eq_dotProduct {n : Type u_1} [Fintype n] (x : n → ℝ) : ∑ i : n, x i ^ 2 = x ⬝ᵥ x

theorem BollobasNikiforov.isHermitian_dotProduct_mulVec {n : Type u_1} [Fintype n] {B : Matrix n n ℝ} (hB : B.IsHermitian) (x y : n → ℝ) : x ⬝ᵥ B.mulVec y = B.mulVec x ⬝ᵥ y

theorem BollobasNikiforov.inner_smul_vecMulVec {n : Type u_1} [Fintype n] (r : ℝ) (C : Matrix n n ℝ) (u : n → ℝ) : inner C (r • Matrix.vecMulVec u u) = r * u ⬝ᵥ C.mulVec u

theorem BollobasNikiforov.vecMulVec_mulVec {n : Type u_1} [Fintype n] (u v x : n → ℝ) : (Matrix.vecMulVec u v).mulVec x = (v ⬝ᵥ x) • u

theorem BollobasNikiforov.inner_vecMulVec_vecMulVec {n : Type u_1} [Fintype n] (u v : n → ℝ) : inner (Matrix.vecMulVec u u) (Matrix.vecMulVec v v) = (u ⬝ᵥ v) ^ 2

noncomputable def BollobasNikiforov.lambdaMaxIndex {n : Type u_1} [Fintype n] [Nontrivial n] : n

Index of λ_max among eigenvalues.

Equations

• BollobasNikiforov.lambdaMaxIndex = (Fintype.equivOfCardEq ⋯) ⟨0, ⋯⟩

noncomputable def BollobasNikiforov.lambdaSecondIndex {n : Type u_1} [Fintype n] [Nontrivial n] : n

Index of λ₂ among eigenvalues.

Equations

• BollobasNikiforov.lambdaSecondIndex = (Fintype.equivOfCardEq ⋯) ⟨1, ⋯⟩

theorem BollobasNikiforov.lambdaMaxIndex_ne_lambdaSecondIndex {n : Type u_1} [Fintype n] [Nontrivial n] : lambdaMaxIndex ≠ lambdaSecondIndex

theorem BollobasNikiforov.eigenvalues_lambdaMaxIndex {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} [Nontrivial n] (hB : B.IsHermitian) : hB.eigenvalues lambdaMaxIndex = lambdaMax hB

theorem BollobasNikiforov.eigenvalues_lambdaSecondIndex {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} [Nontrivial n] (hB : B.IsHermitian) : hB.eigenvalues lambdaSecondIndex = lambdaSecond hB

theorem BollobasNikiforov.eigenvectorBasis_sum_sq {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} (hB : B.IsHermitian) (i : n) : ∑ k : n, (hB.eigenvectorBasis i).ofLp k ^ 2 = 1

theorem BollobasNikiforov.eigenvectorBasis_dotProduct {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} (hB : B.IsHermitian) {i j : n} (hij : i ≠ j) : (hB.eigenvectorBasis i).ofLp ⬝ᵥ (hB.eigenvectorBasis j).ofLp = 0

theorem BollobasNikiforov.exists_second_eigenvec {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} [Nontrivial n] (hB : B.IsHermitian) {u : n → ℝ} (hu : B.mulVec u = lambdaMax hB • u) (hu1 : ∑ i : n, u i ^ 2 = 1) (_hb : 0 < lambdaSecond hB) : ∃ (v : n → ℝ), ∑ i : n, v i ^ 2 = 1 ∧ u ⬝ᵥ v = 0 ∧ B.mulVec v = lambdaSecond hB • v

A unit eigenvector for λ₂ orthogonal to a unit λ_max-eigenvector, when λ₂ > 0.

structure BollobasNikiforov.SpectralSlice {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} [Nontrivial n] (hB : B.IsHermitian) (hnn : ∀ (i j : n), 0 ≤ B i j) : Type u_1

Data of the rank-at-most-two spectral slice of a symmetric nonnegative matrix.

• a : ℝ

  The largest eigenvalue λ₁(B).

• b : ℝ

  The positive part max (λ₂(B)) 0 of the second eigenvalue.

• u : n → ℝ

  A nonnegative unit eigenvector for a.

• v : n → ℝ

  An eigenvector for b, orthogonal to u, of unit mass when 0 < b and zero otherwise.

• X : Matrix n n ℝ

  The rank-at-most-two matrix a • u uᵀ + b • v vᵀ.

• ha : self.a = lambdaMax hB
• hb : self.b = max (lambdaSecond hB) 0
• hu_nonneg (i : n) : 0 ≤ self.u i
• hu_unit : ∑ i : n, self.u i ^ 2 = 1
• hu_eigen : B.mulVec self.u = self.a • self.u
• hv_sq : ∑ i : n, self.v i ^ 2 = if 0 < self.b then 1 else 0
• hv_ortho : self.u ⬝ᵥ self.v = 0
• hv_eigen : B.mulVec self.v = self.b • self.v
• hX : self.X = self.a • Matrix.vecMulVec self.u self.u + self.b • Matrix.vecMulVec self.v self.v

noncomputable def BollobasNikiforov.spectralSlice {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} [Nontrivial n] (hB : B.IsHermitian) (hnn : ∀ (i j : n), 0 ≤ B i j) : SpectralSlice hB hnn

SP04. Existence of the spectral slice.

Equations

• One or more equations did not get rendered due to their size.

theorem BollobasNikiforov.SpectralSlice.a_nonneg {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} [Nontrivial n] {hB : B.IsHermitian} {hnn : ∀ (i j : n), 0 ≤ B i j} (s : SpectralSlice hB hnn) : 0 ≤ s.a

theorem BollobasNikiforov.SpectralSlice.b_nonneg {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} [Nontrivial n] {hB : B.IsHermitian} {hnn : ∀ (i j : n), 0 ≤ B i j} (s : SpectralSlice hB hnn) : 0 ≤ s.b

theorem BollobasNikiforov.SpectralSlice.hv_dot {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} [Nontrivial n] {hB : B.IsHermitian} {hnn : ∀ (i j : n), 0 ≤ B i j} (s : SpectralSlice hB hnn) : s.v ⬝ᵥ s.v = if 0 < s.b then 1 else 0

theorem BollobasNikiforov.SpectralSlice.posSemidef {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} [Nontrivial n] {hB : B.IsHermitian} {hnn : ∀ (i j : n), 0 ≤ B i j} (s : SpectralSlice hB hnn) : s.X.PosSemidef

SP04. The spectral slice is positive semidefinite.

theorem BollobasNikiforov.SpectralSlice.col_eq {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} [Nontrivial n] {hB : B.IsHermitian} {hnn : ∀ (i j : n), 0 ≤ B i j} (s : SpectralSlice hB hnn) (j : n) : s.X.col j = (s.a * s.u j) • s.u + (s.b * s.v j) • s.v

theorem BollobasNikiforov.SpectralSlice.rank_le_two {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} [Nontrivial n] {hB : B.IsHermitian} {hnn : ∀ (i j : n), 0 ≤ B i j} (s : SpectralSlice hB hnn) : s.X.rank ≤ 2

SP04. The spectral slice has rank at most two.

theorem BollobasNikiforov.SpectralSlice.inner_B_X_eq_sq {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} [Nontrivial n] {hB : B.IsHermitian} {hnn : ∀ (i j : n), 0 ≤ B i j} (s : SpectralSlice hB hnn) : inner B s.X = s.a ^ 2 + s.b ^ 2

theorem BollobasNikiforov.SpectralSlice.inner_X_X_eq_sq {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} [Nontrivial n] {hB : B.IsHermitian} {hnn : ∀ (i j : n), 0 ≤ B i j} (s : SpectralSlice hB hnn) : inner s.X s.X = s.a ^ 2 + s.b ^ 2

theorem BollobasNikiforov.SpectralSlice.inner_B_X {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} [Nontrivial n] {hB : B.IsHermitian} {hnn : ∀ (i j : n), 0 ≤ B i j} (s : SpectralSlice hB hnn) : inner B s.X = F hB

SP05. ⟨B, X⟩ = ⟨X, X⟩ = F B.

theorem BollobasNikiforov.SpectralSlice.inner_X_X {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} [Nontrivial n] {hB : B.IsHermitian} {hnn : ∀ (i j : n), 0 ≤ B i j} (s : SpectralSlice hB hnn) : inner s.X s.X = F hB

theorem BollobasNikiforov.SpectralSlice.inner_B_X_eq_inner_X_X {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} [Nontrivial n] {hB : B.IsHermitian} {hnn : ∀ (i j : n), 0 ≤ B i j} (s : SpectralSlice hB hnn) : inner B s.X = inner s.X s.X

theorem BollobasNikiforov.SpectralSlice.lambdaMax_pos_of_ne_zero {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} [Nontrivial n] {hB : B.IsHermitian} {hnn : ∀ (i j : n), 0 ≤ B i j} (s : SpectralSlice hB hnn) (hB0 : B ≠ 0) : 0 < s.a

theorem BollobasNikiforov.SpectralSlice.inner_pos {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} [Nontrivial n] {hB : B.IsHermitian} {hnn : ∀ (i j : n), 0 ≤ B i j} (s : SpectralSlice hB hnn) (hB0 : B ≠ 0) : 0 < inner s.X s.X

SP05. If B ≠ 0 then the common Frobenius mass is positive.

noncomputable def BollobasNikiforov.SpectralSlice.embed {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} [Nontrivial n] {hB : B.IsHermitian} {hnn : ∀ (i j : n), 0 ≤ B i j} (s : SpectralSlice hB hnn) (i : n) : Fin 2 → ℝ

Planar Gram embedding of the spectral slice.

Equations

• s.embed i = ![√s.a * s.u i, √s.b * s.v i]

theorem BollobasNikiforov.SpectralSlice.embed_nonneg_fst {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} [Nontrivial n] {hB : B.IsHermitian} {hnn : ∀ (i j : n), 0 ≤ B i j} (s : SpectralSlice hB hnn) (i : n) : 0 ≤ s.embed i 0

SP06. The first coordinate is nonnegative.

theorem BollobasNikiforov.SpectralSlice.gram {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} [Nontrivial n] {hB : B.IsHermitian} {hnn : ∀ (i j : n), 0 ≤ B i j} (s : SpectralSlice hB hnn) (i j : n) : s.X i j = s.embed i ⬝ᵥ s.embed j

SP06. X is the Gram matrix of the planar embedding.

theorem BollobasNikiforov.SpectralSlice.isCompletelyPositive_M {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} [Nontrivial n] {hB : B.IsHermitian} {hnn : ∀ (i j : n), 0 ≤ B i j} (s : SpectralSlice hB hnn) [LinearOrder n] : IsCompletelyPositive (M s.X)

SP07. M of the spectral slice is completely positive.

theorem BollobasNikiforov.SpectralSlice.sum_adjMatrix_posPart_sq_le_turanFactor {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} [Nontrivial n] {hB : B.IsHermitian} {hnn : ∀ (i j : n), 0 ≤ B i j} (s : SpectralSlice hB hnn) {G : SimpleGraph n} [DecidableRel G.Adj] : ∑ i : n, ∑ j : n, SimpleGraph.adjMatrix ℝ G i j * posPart s.X i j ^ 2 ≤ turanFactor G * F hB

SP08. Completely positive Motzkin–Straus on M s.X.

SP09–SP10 — support bound and Frobenius Cauchy–Schwarz

theorem BollobasNikiforov.inner_le_inner_hadamard_posPart {n : Type u_1} [Fintype n] {B : Matrix n n ℝ} {G : SimpleGraph n} [DecidableRel G.Adj] {X : Matrix n n ℝ} (hnn : ∀ (i j : n), 0 ≤ B i j) (hdiag : ∀ (i : n), B i i = 0) (hsupp : ∀ (i j : n), ¬G.Adj i j → B i j = 0) : inner B X ≤ inner B ((SimpleGraph.adjMatrix ℝ G).hadamard (posPart X))

SP09. If B is supported on the edges of G and entrywise nonnegative, then pairing against X is dominated by pairing against A_G ⊙ X₊.

theorem BollobasNikiforov.inner_hadamard_posPart_le_sqrt {n : Type u_1} [Fintype n] {B : Matrix n n ℝ} {G : SimpleGraph n} [DecidableRel G.Adj] (X : Matrix n n ℝ) : inner B ((SimpleGraph.adjMatrix ℝ G).hadamard (posPart X)) ≤ √(inner B B) * √(∑ i : n, ∑ j : n, SimpleGraph.adjMatrix ℝ G i j * posPart X i j ^ 2)

SP10. Cauchy–Schwarz for the Frobenius pairing against A_G ⊙ X₊.

SP11–SP12 — algebra of the weighted inequality

theorem BollobasNikiforov.SpectralSlice.F_le_turanFactor_mul_inner {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} [Nontrivial n] {hB : B.IsHermitian} {hnn : ∀ (i j : n), 0 ≤ B i j} (s : SpectralSlice hB hnn) {G : SimpleGraph n} (hdiag : ∀ (i : n), B i i = 0) (hsupp : ∀ (i j : n), ¬G.Adj i j → B i j = 0) : F hB ≤ turanFactor G * inner B B

SP11. Combining the support bound, Cauchy–Schwarz, and SP08.

theorem BollobasNikiforov.weighted {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} [Nontrivial n] {G : SimpleGraph n} (hB : B.IsHermitian) (hnn : ∀ (i j : n), 0 ≤ B i j) (hdiag : ∀ (i : n), B i i = 0) (hsupp : ∀ (i j : n), ¬G.Adj i j → B i j = 0) : F hB ≤ turanFactor G * inner B B

SP12. Theorem thm:weighted.