# mathlib3documentation

analysis.inner_product_space.rayleigh

# 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).

theorem continuous_linear_map.rayleigh_smul {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [ E] (T : E →L[𝕜] E) (x : E) {c : 𝕜} (hc : c 0) :
(λ (x : E), / x ^ 2) (c x) = (λ (x : E), / x ^ 2) x
theorem continuous_linear_map.image_rayleigh_eq_image_rayleigh_sphere {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [ E] (T : E →L[𝕜] E) {r : } (hr : 0 < r) :
(λ (x : E), / x ^ 2) '' {0} = (λ (x : E), / x ^ 2) ''
theorem continuous_linear_map.supr_rayleigh_eq_supr_rayleigh_sphere {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [ E] (T : E →L[𝕜] E) {r : } (hr : 0 < r) :
( (x : {x // x 0}), (λ (x : E), / x ^ 2) x) = (x : r)), (λ (x : E), / x ^ 2) x
theorem continuous_linear_map.infi_rayleigh_eq_infi_rayleigh_sphere {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [ E] (T : E →L[𝕜] E) {r : } (hr : 0 < r) :
( (x : {x // x 0}), (λ (x : E), / x ^ 2) x) = (x : r)), (λ (x : E), / x ^ 2) x
theorem linear_map.is_symmetric.has_strict_fderiv_at_re_apply_inner_self {F : Type u_3} {T : F →L[] F} (hT : T.is_symmetric) (x₀ : F) :
(bit0 ((innerSL ) (T x₀))) x₀
theorem is_self_adjoint.linearly_dependent_of_is_local_extr_on {F : Type u_3} {T : F →L[] F} (hT : is_self_adjoint T) {x₀ : F} (hextr : x₀) :
(a b : ), (a, b) 0 a x₀ + b T x₀ = 0
theorem is_self_adjoint.eq_smul_self_of_is_local_extr_on_real {F : Type u_3} {T : F →L[] F} (hT : is_self_adjoint T) {x₀ : F} (hextr : x₀) :
T x₀ = (λ (x : F), / x ^ 2) x₀ x₀
theorem is_self_adjoint.eq_smul_self_of_is_local_extr_on {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [ E] {T : E →L[𝕜] E} (hT : is_self_adjoint T) {x₀ : E} (hextr : x₀) :
T x₀ = ((λ (x : E), / x ^ 2) x₀) x₀
theorem is_self_adjoint.has_eigenvector_of_is_local_extr_on {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [ E] {T : E →L[𝕜] E} (hT : is_self_adjoint T) {x₀ : E} (hx₀ : x₀ 0) (hextr : x₀) :
((λ (x : E), / x ^ 2) 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.

theorem is_self_adjoint.has_eigenvector_of_is_max_on {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [ E] {T : E →L[𝕜] E} (hT : is_self_adjoint T) {x₀ : E} (hx₀ : x₀ 0) (hextr : x₀) :
( (x : {x // x 0}), (λ (x : E), / x ^ 2) 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.

theorem is_self_adjoint.has_eigenvector_of_is_min_on {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [ E] {T : E →L[𝕜] E} (hT : is_self_adjoint T) {x₀ : E} (hx₀ : x₀ 0) (hextr : x₀) :
( (x : {x // x 0}), (λ (x : E), / x ^ 2) x) x₀

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.

theorem linear_map.is_symmetric.has_eigenvalue_supr_of_finite_dimensional {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [ E] [ E] [nontrivial E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) :

The supremum of the Rayleigh quotient of a symmetric operator T on a nontrivial finite-dimensional vector space is an eigenvalue for that operator.

theorem linear_map.is_symmetric.has_eigenvalue_infi_of_finite_dimensional {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [ E] [ E] [nontrivial E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) :

The infimum of the Rayleigh quotient of a symmetric operator T on a nontrivial finite-dimensional vector space is an eigenvalue for that operator.

theorem linear_map.is_symmetric.subsingleton_of_no_eigenvalue_finite_dimensional {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [ E] [ E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) (hT' : (μ : 𝕜), ) :