Spectral radius of a self-adjoint operator

Stream: Is there code for X?

[Thomas Browning]

Can this (or some generalization) be proven easily from mathlib? The issue is that docs#IsSelfAdjoint.spectralRadius_eq_nnnorm requires a CStarAlgebra which is false here (maybe you can tensor up to ℂ, but that sounds a little painful?)

theorem IsSelfAdjoint.spectralRadius_eq_nnnorm' {𝕜 X : Type*} [RCLike 𝕜] [NormedAddCommGroup X]
    [InnerProductSpace 𝕜 X] [CompleteSpace X] {T : X →L[𝕜] X} (hT : IsSelfAdjoint T) :
    spectralRadius 𝕜 T = ‖T‖₊ := by
  sorry

[Jireh Loreaux]

I was recently having a private discussion with Bhavik about very similar questions. There are essentially two ways to do this mathematically, and neither of them is trivial. If there are others, I am unaware of them.

1. You can show this directly using Rayleigh quotients. This I believe is the approach that Heather Macbeth and Frédéric Dupuis took when they formalized the spectral theorem for compact selfadjoint operators in Lean 3, but it's been a long time since I looked at things there.
2. This is essentially what you hinted at: embed H →L[𝕜] H into its complexification, which is a C⋆-algebra (over ℂ, importantly), get it for the ℂ- (or ℝ-) spectrum and because the operator is selfadjoint, it's spectrum is in fact real. (Note: in this approach we are likely still missing a great many of the necessary tools)

[Thomas Browning]

Is it possible to make the Rayleigh quotient argument work without using compactness of T to get a maximum Rayleigh quotient?

[Jireh Loreaux]

Well, you can't get a maximum Rayleigh quotient because in general the supremum will not be attained. In order for it to be attained, it must be the case that ‖T‖ is an eigenvalue, but T may have no eigenvalues at all if it is not compact.

However, you can still show that the supremum of (absolute values of) the Rayleigh quotients is the operator norm. This uses the polarization identity and the parallelogram identity to bound ‖⟪x, T y⟫‖ by the supremum of the Rayleigh quotients (for unit vectors x and y), which then implies that ‖T‖ is bounded by this quantity too. The other inequality is trivial.

To tie this back to the spectral radius, you then show not that ‖T‖ is an eigenvalue, but that it (or -‖T‖) is an approximate eigenvalue, and hence in the spectrum. In other words, suppose that ‖T‖ = ⨆ x, ⟪x, T x⟫ (we can do this WLOG because the other option is that -‖T‖ is the infimum). Then (‖T‖ • 1 - T) is not bounded below, hence not invertible and so ‖T‖ is in the spectrum (or, respectively, -‖T‖ is)

There's all kinds of formalization annoyances here related to the fact that you would be doing this for RCLike 𝕜 instead of ℝ directly.

[Thomas Browning]

Ah, thanks!