English
For End R M, μ ∈ R and k ∈ N, x ∈ M lies in the generalized eigenspace of exponent k iff x is in the kernel of (f − μ·id)^k.
Русский
Для отображения f конечной размерности, μ ∈ R, натуральное k: x ∈ genEigenspace f μ k ⇔ x ∈ ker((f − μ·id)^k).
LaTeX
$$$$ x \\in f.genEigenspace\\, μ\\, k \\quad\\Leftrightarrow\\quad x \\in \\ker\\left((f - μ \\cdot 1)^k\\right). $$$$
Lean4
theorem mem_genEigenspace {f : End R M} {μ : R} {k : ℕ∞} {x : M} :
x ∈ f.genEigenspace μ k ↔ ∃ l : ℕ, l ≤ k ∧ x ∈ LinearMap.ker ((f - μ • 1) ^ l) :=
by
have : Nonempty { l : ℕ // l ≤ k } := ⟨⟨0, zero_le _⟩⟩
have : Directed (ι := { i : ℕ // i ≤ k }) (· ≤ ·) fun i ↦ LinearMap.ker ((f - μ • 1) ^ (i : ℕ)) :=
Monotone.directed_le fun m n h ↦ by simpa using (f - μ • 1).iterateKer.monotone h
simp_rw [genEigenspace, OrderHom.coe_mk, LinearMap.mem_ker, iSup_subtype', Submodule.mem_iSup_of_directed _ this,
LinearMap.mem_ker, Subtype.exists, exists_prop]
