2607.19268v1 / BootsRoyle/Spectral.lean

all files

import Mathlib.Analysis.InnerProductSpace.Rayleigh
import Mathlib.Analysis.Matrix.Spectrum
import Mathlib.Combinatorics.SimpleGraph.LapMatrix

/-!
# Spectral preliminaries for the Boots--Royle/Cao--Vince problem

This file defines the adjacency spectral radius as the maximum Rayleigh
quotient of the real adjacency operator.  This is a convenient definition for
the edge-switching arguments in the paper and is definitionally independent of
any ordering chosen for the eigenvalues.
-/

open scoped InnerProductSpace

namespace BootsRoyle

open Matrix

variable {V : Type*} [Fintype V] [DecidableEq V]

/-- The real adjacency matrix, with its finite decidability instance hidden
behind a noncomputable definition. -/
noncomputable def adjacencyMatrix (G : SimpleGraph V) : Matrix V V ℝ :=
  by
    classical
    exact G.adjMatrix ℝ

/-- The real adjacency operator of a finite simple graph. -/
noncomputable def adjacencyOperator (G : SimpleGraph V) :
    EuclideanSpace ℝ V →ₗ[ℝ] EuclideanSpace ℝ V :=
  (adjacencyMatrix G).toEuclideanLin

/-- The continuous version of `adjacencyOperator`. -/
noncomputable def adjacencyContinuousOperator (G : SimpleGraph V) :
    EuclideanSpace ℝ V →L[ℝ] EuclideanSpace ℝ V :=
  (adjacencyOperator G).toContinuousLinearMap

/-- The adjacency spectral radius, expressed as the maximum Rayleigh quotient.

For a real symmetric adjacency matrix this is its largest (algebraic)
eigenvalue.  The name follows the graph-theory convention; for a nonnegative
matrix Perron--Frobenius identifies this with the usual matrix spectral radius.
-/
noncomputable def adjacencySpectralRadius (G : SimpleGraph V) : ℝ :=
  ⨆ x : {x : EuclideanSpace ℝ V // x ≠ 0},
    ⟪adjacencyOperator G x, x⟫_ℝ / ‖(x : EuclideanSpace ℝ V)‖ ^ 2

lemma adjacencyOperator_isSymmetric (G : SimpleGraph V) :
    (adjacencyOperator G).IsSymmetric := by
  classical
  exact Matrix.isSymmetric_toEuclideanLin_iff.mpr (G.isHermitian_adjMatrix (R := ℝ))

lemma adjacencyOperator_apply (G : SimpleGraph V) (x : EuclideanSpace ℝ V) :
    adjacencyOperator G x = adjacencyMatrix G *ᵥ x := rfl

/-- The variationally defined adjacency spectral radius is an eigenvalue. -/
theorem hasEigenvalue_adjacencySpectralRadius [Nonempty V] (G : SimpleGraph V) :
    Module.End.HasEigenvalue (adjacencyOperator G) (adjacencySpectralRadius G) := by
  exact (adjacencyOperator_isSymmetric G).hasEigenvalue_iSup_of_finiteDimensional

/-- Coordinatewise absolute value on a real Euclidean space. -/
def vectorAbs (x : EuclideanSpace ℝ V) : EuclideanSpace ℝ V :=
  WithLp.toLp 2 fun i ↦ |x i|

omit [Fintype V] [DecidableEq V] in
@[simp] lemma vectorAbs_apply (x : EuclideanSpace ℝ V) (i : V) :
    vectorAbs x i = |x i| := rfl

omit [DecidableEq V] in
@[simp] lemma norm_vectorAbs (x : EuclideanSpace ℝ V) :
    ‖vectorAbs x‖ = ‖x‖ := by
  simp only [EuclideanSpace.norm_eq, vectorAbs_apply, Real.norm_eq_abs, abs_abs]

lemma adjacency_quadraticForm_le_abs (G : SimpleGraph V) (x : EuclideanSpace ℝ V) :
    ⟪adjacencyOperator G x, x⟫_ℝ ≤
      ⟪adjacencyOperator G (vectorAbs x), vectorAbs x⟫_ℝ := by
  classical
  simp only [adjacencyOperator_apply, EuclideanSpace.inner_eq_star_dotProduct, star_trivial,
    dotProduct, mulVec, vectorAbs_apply, Finset.mul_sum, adjacencyMatrix,
    SimpleGraph.adjMatrix_apply]
  apply Finset.sum_le_sum
  intro i _
  apply Finset.sum_le_sum
  intro j _
  split_ifs
  · rw [one_mul, one_mul]
    calc
      x i * x j ≤ |x i * x j| := le_abs_self _
      _ = |x i| * |x j| := abs_mul _ _
  · simp

/-- Perron--Frobenius in the precise form used in the paper: the largest
adjacency eigenvalue has a nonzero coordinatewise nonnegative eigenvector.

For adjacency matrices this elementary form follows by maximizing the
Rayleigh quotient on the unit sphere and replacing a maximizer by its
coordinatewise absolute value.  Irreducibility is not needed for
nonnegativity (it is needed only for strict positivity).
-/
theorem exists_nonnegative_perronVector [Nonempty V] (G : SimpleGraph V) :
    ∃ x : EuclideanSpace ℝ V,
      x ≠ 0 ∧
      (∀ i, 0 ≤ x i) ∧
      adjacencyOperator G x = adjacencySpectralRadius G • x := by
  classical
  let T := adjacencyContinuousOperator G
  let e : EuclideanSpace ℝ V := EuclideanSpace.basisFun V ℝ (Classical.choice inferInstance)
  have he : e ∈ Metric.sphere (0 : EuclideanSpace ℝ V) 1 := by
    simp [e]
  have hsphere : (Metric.sphere (0 : EuclideanSpace ℝ V) 1).Nonempty := ⟨e, he⟩
  obtain ⟨x, hx_sphere, hx_max⟩ :=
    (isCompact_sphere (0 : EuclideanSpace ℝ V) 1).exists_isMaxOn hsphere
      T.reApplyInnerSelf_continuous.continuousOn
  let y := vectorAbs x
  have hxnorm : ‖x‖ = 1 := by
    simpa [mem_sphere_zero_iff_norm] using hx_sphere
  have hynorm : ‖y‖ = 1 := by
    simpa [y, norm_vectorAbs] using hxnorm
  have hy_sphere : y ∈ Metric.sphere (0 : EuclideanSpace ℝ V) 1 := by
    simpa [mem_sphere_zero_iff_norm] using hynorm
  have hxy :
      T.reApplyInnerSelf x ≤ T.reApplyInnerSelf y := by
    simpa [T, adjacencyContinuousOperator, ContinuousLinearMap.reApplyInnerSelf_apply, y]
      using adjacency_quadraticForm_le_abs G x
  have hyx : T.reApplyInnerSelf y ≤ T.reApplyInnerSelf x :=
    hx_max hy_sphere
  have heq : T.reApplyInnerSelf y = T.reApplyInnerSelf x :=
    le_antisymm hyx hxy
  have hy_max : IsMaxOn T.reApplyInnerSelf (Metric.sphere 0 ‖y‖) y := by
    intro z hz
    have hz' : z ∈ Metric.sphere (0 : EuclideanSpace ℝ V) 1 := by
      simpa [hynorm] using hz
    exact (hx_max hz').trans_eq heq.symm
  have hyne : y ≠ 0 := by
    intro hy
    simp [hy] at hynorm
  have hT : IsSelfAdjoint T :=
    (adjacencyOperator_isSymmetric G).isSelfAdjoint
  have hev := hT.hasEigenvector_of_isMaxOn hyne hy_max
  refine ⟨y, hyne, fun i ↦ ?_, ?_⟩
  · exact abs_nonneg _
  · rw [← Module.End.mem_eigenspace_iff]
    simpa [adjacencySpectralRadius, T, adjacencyContinuousOperator,
      ContinuousLinearMap.rayleighQuotient, ContinuousLinearMap.reApplyInnerSelf_apply]
      using hev.1

lemma eigenvector_zero_propagates (G : SimpleGraph V) {x : EuclideanSpace ℝ V} {μ : ℝ}
    (hx_nonneg : ∀ i, 0 ≤ x i)
    (hx_eigen : adjacencyOperator G x = μ • x)
    {v w : V} (hvw : G.Adj v w) (hv : x v = 0) :
    x w = 0 := by
  classical
  have hsum : ∑ u ∈ G.neighborFinset v, x u = 0 := by
    calc
      ∑ u ∈ G.neighborFinset v, x u =
          (adjacencyOperator G x) v := by
            simp [adjacencyOperator_apply, adjacencyMatrix,
              SimpleGraph.adjMatrix_mulVec_apply]
      _ = (μ • x) v :=
        congrArg (fun y : EuclideanSpace ℝ V ↦ y v) hx_eigen
      _ = 0 := by simp [hv]
  exact (Finset.sum_eq_zero_iff_of_nonneg fun i _ ↦ hx_nonneg i).mp hsum w
    (by simpa using hvw)

/-- On a connected graph the nonnegative Perron vector is strictly positive. -/
lemma eigenvector_pos_of_connected (G : SimpleGraph V) (hG : G.Connected)
    {x : EuclideanSpace ℝ V} {μ : ℝ}
    (hx_ne : x ≠ 0)
    (hx_nonneg : ∀ i, 0 ≤ x i)
    (hx_eigen : adjacencyOperator G x = μ • x) :
    ∀ i, 0 < x i := by
  classical
  intro v
  refine lt_of_le_of_ne (hx_nonneg v) ?_
  intro hv_eq
  have hv : x v = 0 := hv_eq.symm
  have hall : ∀ w, x w = 0 := by
    intro w
    obtain ⟨p⟩ := hG v w
    have along {a b : V} (q : G.Walk a b) : x a = 0 → x b = 0 := by
      induction q with
      | nil => exact fun ha ↦ ha
      | @cons u z w huz q ih =>
          intro hu
          exact ih (eigenvector_zero_propagates G hx_nonneg hx_eigen huz hu)
    exact along p hv
  apply hx_ne
  ext i
  exact hall i

/-- Connected graphs have a strictly positive Perron vector for the
variational adjacency spectral radius. -/
theorem exists_positive_perronVector (G : SimpleGraph V) (hG : G.Connected) :
    ∃ x : EuclideanSpace ℝ V,
      (∀ i, 0 < x i) ∧
      adjacencyOperator G x = adjacencySpectralRadius G • x := by
  letI := hG.nonempty
  obtain ⟨x, hx_ne, hx_nonneg, hx_eigen⟩ := exists_nonnegative_perronVector G
  exact ⟨x, eigenvector_pos_of_connected G hG hx_ne hx_nonneg hx_eigen, hx_eigen⟩

/-- The `ℓ¹`-normalization used throughout the paper. -/
theorem exists_l1_normalized_perronVector (G : SimpleGraph V) (hG : G.Connected) :
    ∃ x : EuclideanSpace ℝ V,
      (∀ i, 0 < x i) ∧
      (∑ i, x i) = 1 ∧
      adjacencyOperator G x = adjacencySpectralRadius G • x := by
  classical
  letI := hG.nonempty
  obtain ⟨x, hx_pos, hx_eigen⟩ := exists_positive_perronVector G hG
  let s : ℝ := ∑ i, x i
  have hs_nonneg : 0 ≤ s := Finset.sum_nonneg fun i _ ↦ (hx_pos i).le
  have hs_ne : s ≠ 0 := by
    intro hs
    have hall := (Finset.sum_eq_zero_iff_of_nonneg fun i _ ↦ (hx_pos i).le).mp hs
    exact (hx_pos (Classical.choice inferInstance)).ne' (hall _ (Finset.mem_univ _))
  have hs_pos : 0 < s := lt_of_le_of_ne hs_nonneg (Ne.symm hs_ne)
  let y : EuclideanSpace ℝ V := s⁻¹ • x
  refine ⟨y, fun i ↦ ?_, ?_, ?_⟩
  · simp only [y, PiLp.smul_apply, smul_eq_mul]
    exact mul_pos (inv_pos.mpr hs_pos) (hx_pos i)
  · simp only [y, PiLp.smul_apply, smul_eq_mul, ← Finset.mul_sum, s]
    exact inv_mul_cancel₀ hs_ne
  · simp only [y, map_smul, hx_eigen, smul_smul]
    rw [mul_comm]

/-- Every Rayleigh quotient is bounded by the adjacency spectral radius. -/
lemma rayleighQuotient_le (G : SimpleGraph V) {x : EuclideanSpace ℝ V} (hx : x ≠ 0) :
    ⟪adjacencyOperator G x, x⟫_ℝ / ‖x‖ ^ 2 ≤ adjacencySpectralRadius G := by
  let T := adjacencyContinuousOperator G
  have hb : BddAbove
      (Set.range fun z : {z : EuclideanSpace ℝ V // z ≠ 0} ↦ T.rayleighQuotient z) := by
    refine ⟨‖T‖, ?_⟩
    rintro _ ⟨z, rfl⟩
    exact (le_abs_self _).trans (T.rayleighQuotient_le_norm z)
  have h := le_ciSup hb (⟨x, hx⟩ : {z : EuclideanSpace ℝ V // z ≠ 0})
  simpa [adjacencySpectralRadius, T, adjacencyContinuousOperator,
    ContinuousLinearMap.rayleighQuotient, ContinuousLinearMap.reApplyInnerSelf_apply] using h

lemma rayleighQuotient_eq_of_eigenvector (G : SimpleGraph V)
    {x : EuclideanSpace ℝ V} {μ : ℝ} (hx : x ≠ 0)
    (heigen : adjacencyOperator G x = μ • x) :
    ⟪adjacencyOperator G x, x⟫_ℝ / ‖x‖ ^ 2 = μ := by
  have hnorm : ‖x‖ ^ 2 ≠ 0 := pow_ne_zero 2 (norm_ne_zero_iff.mpr hx)
  rw [heigen, real_inner_smul_left]
  rw [real_inner_self_eq_norm_sq]
  field_simp

lemma quadraticForm_mono_of_nonnegative {G H : SimpleGraph V} (hGH : G ≤ H)
    (x : EuclideanSpace ℝ V) (hx : ∀ i, 0 ≤ x i) :
    ⟪adjacencyOperator G x, x⟫_ℝ ≤ ⟪adjacencyOperator H x, x⟫_ℝ := by
  classical
  simp only [adjacencyOperator_apply, EuclideanSpace.inner_eq_star_dotProduct, star_trivial,
    dotProduct, mulVec, Finset.mul_sum, adjacencyMatrix, SimpleGraph.adjMatrix_apply]
  apply Finset.sum_le_sum
  intro i _
  apply Finset.sum_le_sum
  intro j _
  by_cases hG : G.Adj i j
  · have hH := hGH hG
    simp [hG, hH]
  · simp only [hG, if_false, zero_mul]
    split_ifs
    · simpa using mul_nonneg (hx i) (hx j)
    · simp

theorem adjacencySpectralRadius_mono [Nonempty V] {G H : SimpleGraph V} (hGH : G ≤ H) :
    adjacencySpectralRadius G ≤ adjacencySpectralRadius H := by
  obtain ⟨x, hx_ne, hx_nonneg, hx_eigen⟩ := exists_nonnegative_perronVector G
  have hnorm : 0 < ‖x‖ ^ 2 := sq_pos_of_pos (norm_pos_iff.mpr hx_ne)
  calc
    adjacencySpectralRadius G =
        ⟪adjacencyOperator G x, x⟫_ℝ / ‖x‖ ^ 2 :=
      (rayleighQuotient_eq_of_eigenvector G hx_ne hx_eigen).symm
    _ ≤ ⟪adjacencyOperator H x, x⟫_ℝ / ‖x‖ ^ 2 := by
      exact (div_le_div_iff_of_pos_right hnorm).mpr
        (quadraticForm_mono_of_nonnegative hGH x hx_nonneg)
    _ ≤ adjacencySpectralRadius H := rayleighQuotient_le H hx_ne

lemma quadraticForm_strictMono_of_positive {G H : SimpleGraph V} (hGH : G < H)
    (x : EuclideanSpace ℝ V) (hx : ∀ i, 0 < x i) :
    ⟪adjacencyOperator G x, x⟫_ℝ < ⟪adjacencyOperator H x, x⟫_ℝ := by
  classical
  have hnle : ¬H ≤ G := hGH.2
  simp only [SimpleGraph.le_iff_adj] at hnle
  push Not at hnle
  obtain ⟨v, w, hH, hG⟩ := hnle
  simp only [adjacencyOperator_apply, EuclideanSpace.inner_eq_star_dotProduct, star_trivial,
    dotProduct, mulVec, Finset.mul_sum, adjacencyMatrix, SimpleGraph.adjMatrix_apply]
  apply Finset.sum_lt_sum
  · intro i _
    apply Finset.sum_le_sum
    intro j _
    by_cases hGi : G.Adj i j
    · have hHi := hGH.le hGi
      simp [hGi, hHi]
    · simp only [hGi, if_false, zero_mul]
      split_ifs
      · simpa using mul_nonneg (hx i).le (hx j).le
      · simp
  · refine ⟨v, Finset.mem_univ _, ?_⟩
    apply Finset.sum_lt_sum
    · intro j _
      by_cases hGj : G.Adj v j
      · have hHj := hGH.le hGj
        simp [hGj, hHj]
      · simp only [hGj, if_false, zero_mul]
        split_ifs
        · simpa using mul_nonneg (hx v).le (hx j).le
        · simp
    · refine ⟨w, Finset.mem_univ _, ?_⟩
      simp [hG, hH, mul_pos (hx v) (hx w)]

theorem adjacencySpectralRadius_strictMono_of_connected
    {G H : SimpleGraph V} (hG : G.Connected) (hGH : G < H) :
    adjacencySpectralRadius G < adjacencySpectralRadius H := by
  letI := hG.nonempty
  obtain ⟨x, hx_pos, hx_eigen⟩ := exists_positive_perronVector G hG
  have hx_ne : x ≠ 0 := by
    intro hx
    have := hx_pos (Classical.choice inferInstance)
    simp [hx] at this
  have hnorm : 0 < ‖x‖ ^ 2 := sq_pos_of_pos (norm_pos_iff.mpr hx_ne)
  calc
    adjacencySpectralRadius G =
        ⟪adjacencyOperator G x, x⟫_ℝ / ‖x‖ ^ 2 :=
      (rayleighQuotient_eq_of_eigenvector G hx_ne hx_eigen).symm
    _ < ⟪adjacencyOperator H x, x⟫_ℝ / ‖x‖ ^ 2 := by
      exact (div_lt_div_iff_of_pos_right hnorm).mpr
        (quadraticForm_strictMono_of_positive hGH x hx_pos)
    _ ≤ adjacencySpectralRadius H := rayleighQuotient_le H hx_ne

end BootsRoyle