English
If T is a symmetric operator on a nontrivial finite-dimensional space, then the infimum of its Rayleigh quotients is an eigenvalue of T.
Русский
Если T симметричен на ненулевом пространстве конечной размерности, то нижняя грань коэффициентов Райли является собственным значением T.
LaTeX
$$HasEigenvalue T ↑(⨅ x≠0, ρ_T(x)).$$
Lean4
/-- 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 hasEigenvalue_iInf_of_finiteDimensional [Nontrivial E] (hT : T.IsSymmetric) :
HasEigenvalue T ↑(⨅ x : { x : E // x ≠ 0 }, RCLike.re ⟪T x, x⟫ / ‖(x : E)‖ ^ 2 : ℝ) :=
by
haveI := FiniteDimensional.proper_rclike 𝕜 E
let T' := hT.toSelfAdjoint
obtain ⟨x, hx⟩ : ∃ x : E, x ≠ 0 := exists_ne 0
have H₁ : IsCompact (sphere (0 : E) ‖x‖) := isCompact_sphere _ _
have H₂ : (sphere (0 : E) ‖x‖).Nonempty :=
⟨x, by simp⟩
-- key point: in finite dimension, a continuous function on the sphere has a min
obtain ⟨x₀, hx₀', hTx₀⟩ := H₁.exists_isMinOn H₂ T'.val.reApplyInnerSelf_continuous.continuousOn
have hx₀ : ‖x₀‖ = ‖x‖ := by simpa using hx₀'
have : IsMinOn T'.val.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀ := by simpa only [← hx₀] using hTx₀
have hx₀_ne : x₀ ≠ 0 :=
by
have : ‖x₀‖ ≠ 0 := by simp only [hx₀, norm_eq_zero, hx, Ne, not_false_iff]
simpa [← norm_eq_zero, Ne]
exact hasEigenvalue_of_hasEigenvector (T'.prop.hasEigenvector_of_isMinOn hx₀_ne this)
