Adjacency eigenvalues

This file records the spectral conventions used in docs/sol.tex. The unordered family is indexed by the vertex type, so algebraic multiplicity is counted automatically. The ordered family is Mathlib's antitone eigenvalues₀, which is the paper's λ₁ ≥ ⋯ ≥ λₙ with λ₁ at index 0.

noncomputable def BollobasNikiforov.adjacencyEigenvalues {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : V → ℝ

The adjacency eigenvalues of a finite simple graph, indexed with algebraic multiplicity by its vertex type.

Equations

• BollobasNikiforov.adjacencyEigenvalues G = ⋯.eigenvalues

noncomputable def BollobasNikiforov.adjacencyEigenvalues₀ {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : Fin (Fintype.card V) → ℝ

The adjacency eigenvalues in nonincreasing order. The value at i is the paper's λ_{i+1}(G).

Equations

• BollobasNikiforov.adjacencyEigenvalues₀ G = ⋯.eigenvalues₀

theorem BollobasNikiforov.adjacencyEigenvalues₀_antitone {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : Antitone (adjacencyEigenvalues₀ G)

noncomputable def BollobasNikiforov.lambda1 {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Nonempty V] : ℝ

The largest adjacency eigenvalue λ₁(G).

Equations

• BollobasNikiforov.lambda1 G = BollobasNikiforov.adjacencyEigenvalues₀ G ⟨0, ⋯⟩

noncomputable def BollobasNikiforov.lambda2 {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Nontrivial V] : ℝ

The second-largest adjacency eigenvalue λ₂(G).

Equations

• BollobasNikiforov.lambda2 G = BollobasNikiforov.adjacencyEigenvalues₀ G ⟨1, ⋯⟩