Theorems · Theorem · operator theory

IsSelfAdjoint.hasEigenvector_of_isLocalExtrOn

∀ {𝕜 : 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 →
        IsLocalExtrOn T.reApplyInnerSelf (Metric.sphere 0 ‖x₀‖) x₀ →
          Module.End.HasEigenvector (↑T) (↑(T.rayleighQuotient x₀)) x₀

For a self-adjoint operator T, a local extremum of the Rayleigh quotient of T on a sphere centred at the origin is an eigenvector of T.

Defined in

Mathlib.Analysis.InnerProductSpace.Rayleigh

Cited by

2 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceCompleteSpace