genEigenrange — Mathlib

English

The generalized eigenrange for f, μ, k is the infimum over ranges of (f − μI)^l for l such that l ≤ k.

Русский

Обобщённый диапазон собственных значений генерируется как пересечение рядов диапазонов (f − μI)^l при l ≤ k.

LaTeX

$$genEigenrange(f, μ, k) = ⨅ l:ℕ, ⨅ (l ≤ k), LinearMap.range((f - μ·1)^l)$$

Lean4

/-- The generalized eigenrange for a linear map `f`, a scalar `μ`, and an exponent `k ∈ ℕ∞`
is the range of `(f - μ • id) ^ k` if `k` is a natural number,
or the infimum of these ranges if `k = ∞`. -/
def genEigenrange (f : End R M) (μ : R) (k : ℕ∞) : Submodule R M :=
  ⨅ l : ℕ, ⨅ (_ : l ≤ k), LinearMap.range ((f - μ • 1) ^ l)

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