Rayleigh quotient for compact self-adjoint operators

Mathlib’s file Mathlib.Analysis.InnerProductSpace.Rayleigh contains the core calculus lemma: if the quadratic form x ↦ re ⟪T x, x⟫ attains its maximum/minimum on a sphere, then the extremiser is an eigenvector and the corresponding eigenvalue is the global iSup/iInf of the Rayleigh quotient.

This file supplies the (slightly more elaborate) compact-operator corollary suggested as a TODO in Mathlib:

If T is compact and self-adjoint on a (real or complex) Hilbert space, then T has a nonzero eigenvector with eigenvalue either ⨆ x, rayleighQuotient T x or ⨅ x, rayleighQuotient T x.

The key technical step is to work on the unit weak closed ball, which is compact by Banach–Alaoglu + Riesz (CompactSelfAdjoint.Topology.WeakHilbertCompact), and show that for a compact operator the quadratic form is continuous on that weakly compact set.

Main results

• CompactSelfAdjoint.continuousOn_weakClosedBall_reApplyInnerSelf_of_isCompactOperator
• CompactSelfAdjoint.exists_hasEigenvector_iSup_or_iInf_of_isCompactOperator

noncomputable def CompactSelfAdjoint.strongToWeakDual {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] : E → WeakDual 𝕜 E

The inclusion E → WeakDual 𝕜 E obtained by composing the weak-topology inclusion E → WeakSpace 𝕜 E with the Riesz map into the dual. This is a convenient bridge for uniqueness arguments that need a Hausdorff target (since WeakDual 𝕜 E is T2).

Equations

• CompactSelfAdjoint.strongToWeakDual x = CompactSpectral.weakToWeakDual ((toWeakSpaceCLM 𝕜 E) x)

theorem CompactSelfAdjoint.tendsto_apply_of_isCompactOperator {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) (hTc : IsCompactOperator ⇑T) {α : Type u_3} {l : Filter α} {x : α → WeakSpace 𝕜 E} {x0 : WeakSpace 𝕜 E} {r : ℝ} (hx : ∀ᶠ (a : α) in l, x a ∈ CompactSpectral.weakClosedBall r) (hweak : Filter.Tendsto x l (nhds x0)) : Filter.Tendsto (fun (a : α) => T (x a)) l (nhds (T x0))

If T is compact, then it sends weak convergence on a weakly-closed ball to norm convergence.

theorem CompactSelfAdjoint.continuousOn_weakClosedBall_reApplyInnerSelf_of_isCompactOperator {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) (hTc : IsCompactOperator ⇑T) (r : ℝ) : ContinuousOn (fun (x : WeakSpace 𝕜 E) => T.reApplyInnerSelf x) (CompactSpectral.weakClosedBall r)

For a compact operator T, the quadratic form x ↦ re ⟪T x, x⟫ is continuous on weakly-compact closed balls (i.e. weakClosedBall).

theorem CompactSelfAdjoint.exists_reApplyInnerSelf_ne_zero_of_isSelfAdjoint {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) (hT : IsSelfAdjoint T) (h0 : T ≠ 0) : ∃ (x : E), T.reApplyInnerSelf x ≠ 0

If a self-adjoint operator is nonzero, then its quadratic form x ↦ re ⟪T x, x⟫ is not identically zero.

theorem CompactSelfAdjoint.exists_hasEigenvector_iSup_or_iInf_of_isCompactOperator {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [Nontrivial E] (T : E →L[𝕜] E) (hT : IsSelfAdjoint T) (hTc : IsCompactOperator ⇑T) : (∃ (x : E), Module.End.HasEigenvector (↑T) (↑(⨆ (x : { x : E // x ≠ 0 }), T.rayleighQuotient ↑x)) x) ∨ ∃ (x : E), Module.End.HasEigenvector (↑T) (↑(⨅ (x : { x : E // x ≠ 0 }), T.rayleighQuotient ↑x)) x

Compact self-adjoint operators attain an extremum of the Rayleigh quotient, yielding a nonzero eigenvector for either the global supremum or the global infimum.