mathlib documentation

linear_algebra.eigenspace

Eigenvectors and eigenvalues

This file defines eigenspaces, eigenvalues, and eigenvalues, as well as their generalized counterparts. We follow Axler's approach [axler2015] because it allows us to derive many properties without choosing a basis and without using matrices.

An eigenspace of a linear map f for a scalar μ is the kernel of the map (f - μ • id). The nonzero elements of an eigenspace are eigenvectors x. They have the property f x = μ • x. If there are eigenvectors for a scalar μ, the scalar μ is called an eigenvalue.

There is no consensus in the literature whether 0 is an eigenvector. Our definition of has_eigenvector permits only nonzero vectors. For an eigenvector x that may also be 0, we write x ∈ f.eigenspace μ.

A generalized eigenspace of a linear map f for a natural number k and a scalar μ is the kernel of the map (f - μ • id) ^ k. The nonzero elements of a generalized eigenspace are generalized eigenvectors x. If there are generalized eigenvectors for a natural number k and a scalar μ, the scalar μ is called a generalized eigenvalue.

References

Tags

eigenspace, eigenvector, eigenvalue, eigen

def module.End.eigenspace {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] :
module.End R MR → submodule R M

The submodule eigenspace f μ for a linear map f and a scalar μ consists of all vectors x such that f x = μ • x. (Def 5.36 of [axler2015])

Equations
def module.End.has_eigenvector {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] :
module.End R MR → M → Prop

A nonzero element of an eigenspace is an eigenvector. (Def 5.7 of [axler2015])

Equations
def module.End.has_eigenvalue {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] :
module.End R MR → Prop

A scalar μ is an eigenvalue for a linear map f if there are nonzero vectors x such that f x = μ • x. (Def 5.5 of [axler2015])

Equations
theorem module.End.mem_eigenspace_iff {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] {f : module.End R M} {μ : R} {x : M} :
x f.eigenspace μ f x = μ x

theorem module.End.eigenspace_div {K : Type v} {V : Type w} [field K] [add_comm_group V] [vector_space K V] (f : module.End K V) (a b : K) :
b 0f.eigenspace (a / b) = linear_map.ker (b f - (algebra_map K (module.End K V)) a)

theorem module.End.aeval_apply_of_has_eigenvector {K : Type v} {V : Type w} [field K] [add_comm_group V] [vector_space K V] {f : module.End K V} {p : polynomial K} {μ : K} {x : V} :

theorem module.End.is_integral {K : Type v} {V : Type w} [field K] [add_comm_group V] [vector_space K V] [finite_dimensional K V] (f : module.End K V) :

theorem module.End.is_root_of_has_eigenvalue {K : Type v} {V : Type w} [field K] [add_comm_group V] [vector_space K V] [finite_dimensional K V] {f : module.End K V} {μ : K} :

theorem module.End.has_eigenvalue_of_is_root {K : Type v} {V : Type w} [field K] [add_comm_group V] [vector_space K V] [finite_dimensional K V] {f : module.End K V} {μ : K} :

theorem module.End.has_eigenvalue_iff_is_root {K : Type v} {V : Type w} [field K] [add_comm_group V] [vector_space K V] [finite_dimensional K V] {f : module.End K V} {μ : K} :

theorem module.End.exists_eigenvalue {K : Type v} {V : Type w} [field K] [add_comm_group V] [vector_space K V] [is_alg_closed K] [finite_dimensional K V] [nontrivial V] (f : module.End K V) :
∃ (c : K), f.has_eigenvalue c

Every linear operator on a vector space over an algebraically closed field has an eigenvalue. (Lemma 5.21 of [axler2015])

theorem module.End.eigenvectors_linear_independent {K : Type v} {V : Type w} [field K] [add_comm_group V] [vector_space K V] (f : module.End K V) (μs : set K) (xs : μs → V) :
(∀ (μ : μs), f.has_eigenvector μ (xs μ))linear_independent K xs

Eigenvectors corresponding to distinct eigenvalues of a linear operator are linearly independent. (Lemma 5.10 of [axler2015])

We use the eigenvalues as indexing set to ensure that there is only one eigenvector for each eigenvalue in the image of xs.

def module.End.generalized_eigenspace {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] :
module.End R MR → submodule R M

The generalized eigenspace for a linear map f, a scalar μ, and an exponent k ∈ ℕ is the kernel of (f - μ • id) ^ k. (Def 8.10 of [axler2015])

Equations
def module.End.has_generalized_eigenvector {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] :
module.End R MR → M → Prop

A nonzero element of a generalized eigenspace is a generalized eigenvector. (Def 8.9 of [axler2015])

Equations
def module.End.has_generalized_eigenvalue {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] :
module.End R MR → → Prop

A scalar μ is a generalized eigenvalue for a linear map f and an exponent k ∈ ℕ if there are generalized eigenvectors for f, k, and μ.

Equations
def module.End.generalized_eigenrange {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] :
module.End R MR → submodule R M

The generalized eigenrange for a linear map f, a scalar μ, and an exponent k ∈ ℕ is the range of (f - μ • id) ^ k.

Equations
theorem module.End.exp_ne_zero_of_has_generalized_eigenvalue {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] {f : module.End R M} {μ : R} {k : } :

The exponent of a generalized eigenvalue is never 0.

theorem module.End.generalized_eigenspace_mono {K : Type v} {V : Type w} [field K] [add_comm_group V] [vector_space K V] {f : module.End K V} {μ : K} {k m : } :

A generalized eigenspace for some exponent k is contained in the generalized eigenspace for exponents larger than k.

A generalized eigenvalue for some exponent k is also a generalized eigenvalue for exponents larger than k.

theorem module.End.eigenspace_le_generalized_eigenspace {K : Type v} {V : Type w} [field K] [add_comm_group V] [vector_space K V] {f : module.End K V} {μ : K} {k : } :

The eigenspace is a subspace of the generalized eigenspace.

theorem module.End.has_generalized_eigenvalue_of_has_eigenvalue {K : Type v} {V : Type w} [field K] [add_comm_group V] [vector_space K V] {f : module.End K V} {μ : K} {k : } :

All eigenvalues are generalized eigenvalues.

Every generalized eigenvector is a generalized eigenvector for exponent findim K V. (Lemma 8.11 of [axler2015])

Generalized eigenspaces for exponents at least findim K V are equal to each other.

theorem module.End.generalized_eigenspace_restrict {K : Type v} {V : Type w} [field K] [add_comm_group V] [vector_space K V] (f : module.End K V) (p : submodule K V) (k : ) (μ : K) (hfp : ∀ (x : V), x pf x p) :

If f maps a subspace p into itself, then the generalized eigenspace of the restriction of f to p is the part of the generalized eigenspace of f that lies in p.

Generalized eigenrange and generalized eigenspace for exponent findim K V are disjoint.

The generalized eigenspace of an eigenvalue has positive dimension for positive exponents.

theorem module.End.map_generalized_eigenrange_le {K : Type v} {V : Type w} [field K] [add_comm_group V] [vector_space K V] {f : module.End K V} {μ : K} {n : } :

A linear map maps a generalized eigenrange into itself.

theorem module.End.supr_generalized_eigenspace_eq_top {K : Type v} {V : Type w} [field K] [add_comm_group V] [vector_space K V] [is_alg_closed K] [finite_dimensional K V] (f : module.End K V) :
(⨆ (μ : K) (k : ), f.generalized_eigenspace μ k) =

The generalized eigenvectors span the entire vector space (Lemma 8.21 of [axler2015]).

theorem linear_map.is_integral {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [vector_space K V] [finite_dimensional K V] (f : V →ₗ[K] V) :