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