maxGenEigenspaceIndex — Mathlib

English

The index maxGenEigenspaceIndex(f, μ) is the least k such that the kernel of (f − μ I)^k equals the maximal generalized eigenspace, if such k exists.

Русский

Индекс maxGenEigenspaceIndex(f, μ) — наименьшее k такое, что ядро (f − μ I)^k совпадает с максимальным обобщённым эйгенпространством, если такое k существует.

LaTeX

$$$\\text{maxGenEigenspaceIndex}(f, \\mu) = \\min\\{ k ∈ \\mathbb{N} : \\ker((f-\\mu I)^k) = \\maxGenEigenspace(f, \\mu) \\}. $$$

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 abbrev maxGenEigenspaceIndex (f : End R M) (μ : R) :=
  maxUnifEigenspaceIndex f μ

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