English
A linear map maps a generalized eigenrange into itself.
Русский
Линейное отображение отображает обобщённый диапазон эйгенсез в себя.
LaTeX
$$$\\mathrm{Submodule.map}\\ f(f.\\mathrm{genEigenrange}(μ,n)) \\le f.\\mathrm{genEigenrange}(μ,n)$$$
Lean4
/-- A linear map maps a generalized eigenrange into itself. -/
theorem map_genEigenrange_le {f : End K V} {μ : K} {n : ℕ} :
Submodule.map f (f.genEigenrange μ n) ≤ f.genEigenrange μ n :=
calc
Submodule.map f (f.genEigenrange μ n) = LinearMap.range (f * (f - algebraMap _ _ μ) ^ n) := by
rw [genEigenrange_nat]; exact (LinearMap.range_comp _ _).symm
_ = LinearMap.range ((f - algebraMap _ _ μ) ^ n * f) := by rw [Algebra.mul_sub_algebraMap_pow_commutes]
_ = Submodule.map ((f - algebraMap _ _ μ) ^ n) (LinearMap.range f) := (LinearMap.range_comp _ _)
_ ≤ f.genEigenrange μ n := by rw [genEigenrange_nat]; apply LinearMap.map_le_range
