Nonnegative Perron vector for a symmetric nonnegative matrix

A real symmetric entrywise-nonnegative matrix has a nonnegative unit maximizer of the Rayleigh quotient, and that maximizer is an eigenvector for lambdaMax.

def BollobasNikiforov.l2Sphere {n : Type u_1} [Fintype n] : Set (n → ℝ)

The Euclidean unit sphere in coordinates {x | ∑ i, x i ^ 2 = 1}.

Equations

• BollobasNikiforov.l2Sphere = {x : n → ℝ | ∑ i : n, x i ^ 2 = 1}

theorem BollobasNikiforov.mem_l2Sphere {n : Type u_1} [Fintype n] {x : n → ℝ} : x ∈ l2Sphere ↔ ∑ i : n, x i ^ 2 = 1

theorem BollobasNikiforov.isCompact_l2Sphere {n : Type u_1} [Fintype n] : IsCompact l2Sphere

theorem BollobasNikiforov.l2Sphere_nonempty {n : Type u_1} [Fintype n] [Nonempty n] : l2Sphere.Nonempty

theorem BollobasNikiforov.continuous_dotProduct_mulVec {n : Type u_1} [Fintype n] {B : Matrix n n ℝ} : Continuous fun (x : n → ℝ) => x ⬝ᵥ B.mulVec x

theorem BollobasNikiforov.dotProduct_mulVec_le_abs {n : Type u_1} [Fintype n] {B : Matrix n n ℝ} (hnn : ∀ (i j : n), 0 ≤ B i j) (x : n → ℝ) : x ⬝ᵥ B.mulVec x ≤ |x| ⬝ᵥ B.mulVec |x|

SP01. Replacing a vector by its absolute value cannot decrease the Rayleigh form of an entrywise nonnegative matrix.

theorem BollobasNikiforov.exists_isMaxOn_dotProduct_mulVec {n : Type u_1} [Fintype n] {B : Matrix n n ℝ} (_hB : B.IsHermitian) [Nonempty n] : ∃ u ∈ l2Sphere, IsMaxOn (fun (x : n → ℝ) => x ⬝ᵥ B.mulVec x) l2Sphere u

SP02 (existence). The Rayleigh form of a symmetric matrix attains a maximum on the Euclidean unit sphere.

theorem BollobasNikiforov.exists_nonneg_isMaxOn_dotProduct_mulVec {n : Type u_1} [Fintype n] {B : Matrix n n ℝ} (hB : B.IsHermitian) (hnn : ∀ (i j : n), 0 ≤ B i j) [Nonempty n] : ∃ u ∈ l2Sphere, (∀ (i : n), 0 ≤ u i) ∧ IsMaxOn (fun (x : n → ℝ) => x ⬝ᵥ B.mulVec x) l2Sphere u

SP02. If B is also entrywise nonnegative, some maximizer is nonnegative.

theorem BollobasNikiforov.exists_nonneg_eigenvector_lambdaMax {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} (hB : B.IsHermitian) (hnn : ∀ (i j : n), 0 ≤ B i j) [Nonempty n] : ∃ (u : n → ℝ), (∀ (i : n), 0 ≤ u i) ∧ ∑ i : n, u i ^ 2 = 1 ∧ B.mulVec u = lambdaMax hB • u

SP03. A symmetric entrywise-nonnegative matrix has a nonnegative unit eigenvector for lambdaMax.