eq_smul_self_of_isLocalExtrOn — Mathlib

English

In the self-adjoint setting, the same eigenvector relation holds with the Rayleigh quotient interpreted in the base field.

Русский

В контексте самосопряжённости аналогичен равенству собственный вектор и собственное значение, где коэффициент Райли берётся в базовом поле.

LaTeX

$$$T x_0 = (\\text{RayleighQuotient}_T(x_0))\\, x_0$$$

Lean4

theorem eq_smul_self_of_isLocalExtrOn (hT : IsSelfAdjoint T) {x₀ : E}
    (hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere (0 : E) ‖x₀‖) x₀) : T x₀ = (↑(T.rayleighQuotient x₀) : 𝕜) • x₀ :=
  by
  letI := InnerProductSpace.rclikeToReal 𝕜 E
  let hSA := hT.isSymmetric.restrictScalars.toSelfAdjoint.prop
  exact hSA.eq_smul_self_of_isLocalExtrOn_real hextr

Похожие утверждения