English
Generalized eigenspace at μ and k equals the supremum of those for l ≤ k; i.e., f.genEigenspace μ k = ⨆ l: {l ≤ k}, f.genEigenspace μ l.
Русский
Обобщённое собственное пространство при μ и k равно наивысшей верхней границе между всеми l ≤ k: f.genEigenspace μ k = ⨆ l ≤ k f.genEigenspace μ l.
LaTeX
$$$$ f.genEigenspace\\, μ\\, k = \\big\\langle f.genEigenspace\\, μ\\, l \\big\\rangle_{l \\le k} = \\Sup_{l: \\{l: \\mathbb{N} \\;|\\; l \\le k\\}} f.genEigenspace\\, μ\\, l. $$$$
Lean4
theorem mem_genEigenspace_nat {f : End R M} {μ : R} {k : ℕ} {x : M} :
x ∈ f.genEigenspace μ k ↔ x ∈ LinearMap.ker ((f - μ • 1) ^ k) :=
by
rw [mem_genEigenspace]
constructor
· rintro ⟨l, hl, hx⟩
simp only [Nat.cast_le] at hl
exact (f - μ • 1).iterateKer.monotone hl hx
· intro hx
exact ⟨k, le_rfl, hx⟩
