English
For a self-adjoint operator T on a complete space, if a local extremum exists on a sphere, then x0 is an eigenvector with eigenvalue equal to the Rayleigh quotient.
Русский
Для самосопряжённого оператора T на полной пространстве, если существует локальный экстремум на сфере, то x0 — собственный вектор с eigenvalue = коэффициент Райли.
LaTeX
$$HasEigenvector T x0 with eigenvalue = RayleighQuotient(x0).$$
Lean4
/-- 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 hasEigenvector_of_isLocalExtrOn (hT : IsSelfAdjoint T) {x₀ : E} (hx₀ : x₀ ≠ 0)
(hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere (0 : E) ‖x₀‖) x₀) :
HasEigenvector (T : E →ₗ[𝕜] E) (↑(T.rayleighQuotient x₀)) x₀ :=
by
refine ⟨?_, hx₀⟩
rw [Module.End.mem_eigenspace_iff]
exact hT.eq_smul_self_of_isLocalExtrOn hextr
