The Rayleigh quotient

The Rayleigh quotient of a self-adjoint operator T on an inner product space E is the function fun x ↦ ⟪T x, x⟫ / ‖x‖ ^ 2.

The main results of this file are IsSelfAdjoint.hasEigenvector_of_isMaxOn and IsSelfAdjoint.hasEigenvector_of_isMinOn, 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 iSup/iInf of fun x ↦ ⟪T x, x⟫ / ‖x‖ ^ 2 is the corresponding eigenvalue.

The corollaries LinearMap.IsSymmetric.hasEigenvalue_iSup_of_finiteDimensional and LinearMap.IsSymmetric.hasEigenvalue_iSup_of_finiteDimensional state that if E is finite-dimensional and nontrivial, then T has some (nonzero) eigenvectors with eigenvalue the iSup/iInf of fun 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).

@[reducible, inline]

noncomputable abbrev ContinuousLinearMap.rayleighQuotient {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →L[𝕜] E) (x : E) : ℝ

The Rayleigh quotient of a continuous linear map T (over ℝ or ℂ) at a vector x is the quantity re ⟪T x, x⟫ / ‖x‖ ^ 2.

Equations

• T.rayleighQuotient x = T.reApplyInnerSelf x / ‖x‖ ^ 2

theorem ContinuousLinearMap.rayleigh_smul {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →L[𝕜] E) (x : E) {c : 𝕜} (hc : c ≠ 0) : T.rayleighQuotient (c • x) = T.rayleighQuotient x

theorem ContinuousLinearMap.image_rayleigh_eq_image_rayleigh_sphere {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →L[𝕜] E) {r : ℝ} (hr : 0 < r) : T.rayleighQuotient '' {0}ᶜ = T.rayleighQuotient '' Metric.sphere 0 r

theorem ContinuousLinearMap.iSup_rayleigh_eq_iSup_rayleigh_sphere {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →L[𝕜] E) {r : ℝ} (hr : 0 < r) : ⨆ (x : { x : E // x ≠ 0 }), T.rayleighQuotient ↑x = ⨆ (x : ↑(Metric.sphere 0 r)), T.rayleighQuotient ↑x

theorem ContinuousLinearMap.iInf_rayleigh_eq_iInf_rayleigh_sphere {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →L[𝕜] E) {r : ℝ} (hr : 0 < r) : ⨅ (x : { x : E // x ≠ 0 }), T.rayleighQuotient ↑x = ⨅ (x : ↑(Metric.sphere 0 r)), T.rayleighQuotient ↑x

theorem LinearMap.IsSymmetric.hasStrictFDerivAt_reApplyInnerSelf {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {T : F →L[ℝ] F} (hT : (↑T).IsSymmetric) (x₀ : F) : HasStrictFDerivAt T.reApplyInnerSelf (2 • (innerSL ℝ) (T x₀)) x₀

theorem IsSelfAdjoint.linearly_dependent_of_isLocalExtrOn {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] {T : F →L[ℝ] F} (hT : IsSelfAdjoint T) {x₀ : F} (hextr : IsLocalExtrOn T.reApplyInnerSelf (Metric.sphere 0 ‖x₀‖) x₀) : ∃ (a : ℝ) (b : ℝ), (a, b) ≠ 0 ∧ a • x₀ + b • T x₀ = 0

theorem IsSelfAdjoint.eq_smul_self_of_isLocalExtrOn_real {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] {T : F →L[ℝ] F} (hT : IsSelfAdjoint T) {x₀ : F} (hextr : IsLocalExtrOn T.reApplyInnerSelf (Metric.sphere 0 ‖x₀‖) x₀) : T x₀ = T.rayleighQuotient x₀ • x₀

theorem IsSelfAdjoint.eq_smul_self_of_isLocalExtrOn {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} (hT : IsSelfAdjoint T) {x₀ : E} (hextr : IsLocalExtrOn T.reApplyInnerSelf (Metric.sphere 0 ‖x₀‖) x₀) : T x₀ = ↑(T.rayleighQuotient x₀) • x₀

theorem IsSelfAdjoint.hasEigenvector_of_isLocalExtrOn {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} (hT : IsSelfAdjoint T) {x₀ : E} (hx₀ : x₀ ≠ 0) (hextr : 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.

theorem IsSelfAdjoint.hasEigenvector_of_isMaxOn {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} (hT : IsSelfAdjoint T) {x₀ : E} (hx₀ : x₀ ≠ 0) (hextr : IsMaxOn T.reApplyInnerSelf (Metric.sphere 0 ‖x₀‖) x₀) : Module.End.HasEigenvector (↑T) (↑(⨆ (x : { x : E // x ≠ 0 }), 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.

theorem IsSelfAdjoint.hasEigenvector_of_isMinOn {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} (hT : IsSelfAdjoint T) {x₀ : E} (hx₀ : x₀ ≠ 0) (hextr : IsMinOn T.reApplyInnerSelf (Metric.sphere 0 ‖x₀‖) x₀) : Module.End.HasEigenvector (↑T) (↑(⨅ (x : { x : E // x ≠ 0 }), T.rayleighQuotient ↑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 LinearMap.IsSymmetric.hasEigenvalue_iSup_of_finiteDimensional {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} [Nontrivial E] (hT : T.IsSymmetric) : Module.End.HasEigenvalue T ↑(⨆ (x : { x : E // x ≠ 0 }), RCLike.re (inner (T ↑x) ↑x) / ‖↑x‖ ^ 2)

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 LinearMap.IsSymmetric.hasEigenvalue_iInf_of_finiteDimensional {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} [Nontrivial E] (hT : T.IsSymmetric) : Module.End.HasEigenvalue T ↑(⨅ (x : { x : E // x ≠ 0 }), RCLike.re (inner (T ↑x) ↑x) / ‖↑x‖ ^ 2)

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 LinearMap.IsSymmetric.subsingleton_of_no_eigenvalue_finiteDimensional {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hT' : ∀ (μ : 𝕜), Module.End.eigenspace T μ = ⊥) : Subsingleton E