maxUnifEigenspaceIndex — Mathlib

English

There is a noncomputable invariant maxUnifEigenspaceIndex f μ ∈ ℕ that captures the index where the maximal generalized eigenspace occurs.

Русский

Существуют макcимальный индекс максимального обобщённого собственного пространства для f и μ.

LaTeX

$$maxUnifEigenspaceIndex (f) (μ) ∈ ℕ$$

Lean4

/-- If there exists a natural number `k` such that the kernel of `(f - μ • id) ^ k` is the
maximal generalized eigenspace, then this value is the least such `k`. If not, this value is not
meaningful. -/
noncomputable def maxUnifEigenspaceIndex (f : End R M) (μ : R) :=
  monotonicSequenceLimitIndex <| (f.genEigenspace μ).comp <| WithTop.coeOrderHom.toOrderHom

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