English
For a self-adjoint operator T, a maximum of the Rayleigh quotient on a sphere yields an eigenvector with eigenvalue equal to the global supremum of the Rayleigh quotient.
Русский
Для самосопряжённого оператора T максимум коэффициента Райли на сфере даёт собственный вектор с наибольшим собственным значением.
LaTeX
$$HasEigenvector T x0 with eigenvalue = ⨆ x≠0 ρ_T(x).$$
Lean4
/-- 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 hasEigenvector_of_isMaxOn (hT : IsSelfAdjoint T) {x₀ : E} (hx₀ : x₀ ≠ 0)
(hextr : IsMaxOn T.reApplyInnerSelf (sphere (0 : E) ‖x₀‖) x₀) :
HasEigenvector (T : E →ₗ[𝕜] E) (↑(⨆ x : { x : E // x ≠ 0 }, T.rayleighQuotient x)) x₀ :=
by
convert hT.hasEigenvector_of_isLocalExtrOn hx₀ (Or.inr hextr.localize)
have hx₀' : 0 < ‖x₀‖ := by simp [hx₀]
have hx₀'' : x₀ ∈ sphere (0 : E) ‖x₀‖ := by simp
rw [T.iSup_rayleigh_eq_iSup_rayleigh_sphere hx₀']
refine IsMaxOn.iSup_eq hx₀'' ?_
intro x hx
dsimp
have : ‖x‖ = ‖x₀‖ := by simpa using hx
simp only [ContinuousLinearMap.rayleighQuotient]
rw [this]
gcongr
exact hextr hx
