Theorems · Theorem · operator theory

IsSelfAdjoint.hasEigenvector_of_isMaxOn

∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] {T : E →L[𝕜] E},
  IsSelfAdjoint T →
    ∀ {x₀ : E},
      x₀ ≠ 0 →
        IsMaxOn T.reApplyInnerSelf (Metric.sphere 0 ‖x₀‖) x₀ →
          Module.End.HasEigenvector (↑T) (↑(⨆ x, T.rayleighQuotient ↑x)) x₀

For a self-adjoint operator T, a maximum of the Rayleigh quotient of T on a sphere centred at the origin is an eigenvector of T, with eigenvalue the global supremum of the Rayleigh quotient.

Defined in

Mathlib.Analysis.InnerProductSpace.Rayleigh

Cited by

1 results in Mathlib

Foundations

Depth 200 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceCompleteSpace