The Rayleigh quotient #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
The Rayleigh quotient of a self-adjoint operator T on an inner product space E is the function
λ x, ⟪T x, x⟫ / ‖x‖ ^ 2.
The main results of this file are is_self_adjoint.has_eigenvector_of_is_max_on and
is_self_adjoint.has_eigenvector_of_is_min_on, which state that if E is complete, and if the
Rayleigh quotient attains its global maximum/minimum over some sphere at the point x₀, then x₀
is an eigenvector of T, and the supr/infi of λ x, ⟪T x, x⟫ / ‖x‖ ^ 2 is the corresponding
eigenvalue.
The corollaries is_self_adjoint.has_eigenvalue_supr_of_finite_dimensional and
is_self_adjoint.has_eigenvalue_supr_of_finite_dimensional state that if E is finite-dimensional
and nontrivial, then T has some (nonzero) eigenvectors with eigenvalue the supr/infi of
λ x, ⟪T x, x⟫ / ‖x‖ ^ 2.
TODO #
A slightly more elaborate corollary is that if E is complete and T is a compact operator, then
T has some (nonzero) eigenvector with eigenvalue either ⨆ x, ⟪T x, x⟫ / ‖x‖ ^ 2 or
⨅ x, ⟪T x, x⟫ / ‖x‖ ^ 2 (not necessarily both).
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.
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.
For a self-adjoint operator T, a minimum of the Rayleigh quotient of T on a sphere centred
at the origin is an eigenvector of T, with eigenvalue the global infimum of the Rayleigh
quotient.
The supremum of the Rayleigh quotient of a symmetric operator T on a nontrivial
finite-dimensional vector space is an eigenvalue for that operator.
The infimum of the Rayleigh quotient of a symmetric operator T on a nontrivial
finite-dimensional vector space is an eigenvalue for that operator.