Documentation

LeanPool.BollobasNikiforov.Basic.Spectrum

Ordered spectrum of a Hermitian matrix #

This file records the ordered real spectrum of a Hermitian matrix, matching the conventions in docs/sol.tex. The ordered family is Mathlib's antitone eigenvalues₀, which is the paper's λ₁ ≥ ⋯ ≥ λₙ with λ₁ at index 0. F is the sum of squares of the two largest positive eigenvalues, with missing terms replaced by zero.

source
noncomputable def BollobasNikiforov.eigs₀ {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsHermitian) :
Fin (Fintype.card n) → ℝ

The eigenvalues of a Hermitian matrix in nonincreasing order. The value at i is the paper's λ_{i+1}.

Equations
Instances For
    source
    theorem BollobasNikiforov.eigs₀_antitone {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsHermitian) :
    Antitone (eigs₀ hA)
    source
    noncomputable def BollobasNikiforov.lambdaMax {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsHermitian) [Nonempty n] :
    ℝ

    The largest eigenvalue λ₁(A).

    Equations
    Instances For
      source
      noncomputable def BollobasNikiforov.lambdaSecond {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsHermitian) [Nontrivial n] :
      ℝ

      The second-largest eigenvalue λ₂(A).

      Equations
      Instances For
        source
        noncomputable def BollobasNikiforov.F {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsHermitian) :
        ℝ

        The sum of squares of the two largest positive eigenvalues of a Hermitian matrix, with missing terms replaced by zero.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem BollobasNikiforov.F_eq {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsHermitian) [Nontrivial n] :
          F hA = max (lambdaMax hA) 0 ^ 2 + max (lambdaSecond hA) 0 ^ 2
          source
          theorem BollobasNikiforov.F_nonneg {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsHermitian) :
          0 ≤ F hA
          source
          theorem BollobasNikiforov.F_zero {n : Type u_1} [Fintype n] [DecidableEq n] :
          F ⋯ = 0

          N11 — Adjacency Frobenius mass #

          source
          theorem BollobasNikiforov.inner_adjMatrix_eq_trace_mul {V : Type u_2} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] :
          inner (SimpleGraph.adjMatrix ℝ G) (SimpleGraph.adjMatrix ℝ G) = (SimpleGraph.adjMatrix ℝ G * SimpleGraph.adjMatrix ℝ G).trace

          The adjacency matrix is symmetric, so the Frobenius pairing with itself is the trace of the square.

          source
          theorem BollobasNikiforov.trace_adjMatrix_mul_self {V : Type u_2} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] :
          (SimpleGraph.adjMatrix ℝ G * SimpleGraph.adjMatrix ℝ G).trace = ∑ v : V, ↑(G.degree v)

          The diagonal of A_G² records vertex degrees.

          source
          theorem BollobasNikiforov.inner_adjMatrix_self {V : Type u_2} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] :
          inner (SimpleGraph.adjMatrix ℝ G) (SimpleGraph.adjMatrix ℝ G) = 2 * ↑G.edgeFinset.card

          The Frobenius mass of the adjacency matrix is twice the number of edges.