mathlib3 documentation

linear_algebra.eigenspace.basic

Eigenvectors and eigenvalues #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines eigenspaces, eigenvalues, and eigenvalues, as well as their generalized counterparts. We follow Axler's approach [Axl15] 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.

The fact that the eigenvalues are the roots of the minimal polynomial is proved in linear_algebra.eigenspace.minpoly.

The existence of eigenvalues over an algebraically closed field (and the fact that the generalized eigenspaces then span) is deferred to linear_algebra.eigenspace.is_alg_closed.

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] (f : module.End R M) (μ : R) :

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 [Axl15])

Equations

f.eigenspace μ = linear_map.ker (f - ⇑(algebra_map R (module.End R M)) μ)

Instances for module.End.eigenspace

linear_map.is_symmetric.direct_sum_decomposition

@[simp]

theorem module.End.eigenspace_zero {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] (f : module.End R M) :

f.eigenspace 0 = linear_map.ker f

def module.End.has_eigenvector {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] (f : module.End R M) (μ : R) (x : M) :

Prop

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

Equations

f.has_eigenvector μ x = (x ∈ f.eigenspace μ ∧ x ≠ 0)

def module.End.has_eigenvalue {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] (f : module.End R M) (a : R) :

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 [Axl15])

Equations

f.has_eigenvalue a = (f.eigenspace a ≠ ⊥)

def module.End.eigenvalues {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] (f : module.End R M) :

The eigenvalues of the endomorphism f, as a subtype of R.

Equations

f.eigenvalues = {μ // f.has_eigenvalue μ}

Instances for module.End.eigenvalues

@[protected, instance]

def module.End.has_coe {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] (f : module.End R M) :

has_coe f.eigenvalues R

Equations

f.has_coe = coe_subtype

theorem module.End.has_eigenvalue_of_has_eigenvector {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] {f : module.End R M} {μ : R} {x : M} (h : f.has_eigenvector μ x) :

f.has_eigenvalue μ

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.has_eigenvector.apply_eq_smul {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] {f : module.End R M} {μ : R} {x : M} (hx : f.has_eigenvector μ x) :

⇑f x = μ • x

theorem module.End.has_eigenvalue.exists_has_eigenvector {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] {f : module.End R M} {μ : R} (hμ : f.has_eigenvalue μ) :

∃ (v : M), f.has_eigenvector μ v

theorem module.End.mem_spectrum_of_has_eigenvalue {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] {f : module.End R M} {μ : R} (hμ : f.has_eigenvalue μ) :

μ ∈ spectrum R f

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

f.has_eigenvalue μ ↔ μ ∈ spectrum K f

theorem module.End.eigenspace_div {K : Type v} {V : Type w} [field K] [add_comm_group V] [module K V] (f : module.End K V) (a b : K) (hb : b ≠ 0) :

f.eigenspace (a / b) = linear_map.ker (b • f - ⇑(algebra_map K (module.End K V)) a)

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

complete_lattice.independent f.eigenspace

The eigenspaces of a linear operator form an independent family of subspaces of V. That is, any eigenspace has trivial intersection with the span of all the other eigenspaces.

theorem module.End.eigenvectors_linear_independent {K : Type v} {V : Type w} [field K] [add_comm_group V] [module K V] (f : module.End K V) (μs : set K) (xs : ↥μs → V) (h_eigenvec : ∀ (μ : ↥μ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 [Axl15])

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] (f : module.End R M) (μ : R) :

ℕ →o 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 [Axl15]). Furthermore, a generalized eigenspace for some exponent k is contained in the generalized eigenspace for exponents larger than k.

Equations

f.generalized_eigenspace μ = {to_fun := λ (k : ℕ), linear_map.ker ((f - ⇑(algebra_map R (module.End R M)) μ) ^ k), monotone' := _}

@[simp]

theorem module.End.mem_generalized_eigenspace {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] (f : module.End R M) (μ : R) (k : ℕ) (m : M) :

m ∈ ⇑(f.generalized_eigenspace μ) k ↔ ⇑((f - μ • 1) ^ k) m = 0

@[simp]

theorem module.End.generalized_eigenspace_zero {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] (f : module.End R M) (k : ℕ) :

⇑(f.generalized_eigenspace 0) k = linear_map.ker (f ^ k)

def module.End.has_generalized_eigenvector {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] (f : module.End R M) (μ : R) (k : ℕ) (x : M) :

Prop

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

Equations

f.has_generalized_eigenvector μ k x = (x ≠ 0 ∧ x ∈ ⇑(f.generalized_eigenspace μ) k)

def module.End.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 : ℕ) :

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

f.has_generalized_eigenvalue μ k = (⇑(f.generalized_eigenspace μ) k ≠ ⊥)

def module.End.generalized_eigenrange {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] (f : module.End R M) (μ : R) (k : ℕ) :

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

Equations

f.generalized_eigenrange μ k = linear_map.range ((f - ⇑(algebra_map R (module.End R M)) μ) ^ k)

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 : ℕ} (h : f.has_generalized_eigenvalue μ k) :

k ≠ 0

The exponent of a generalized eigenvalue is never 0.

def module.End.maximal_generalized_eigenspace {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] (f : module.End R M) (μ : R) :

The union of the kernels of (f - μ • id) ^ k over all k.

Equations

f.maximal_generalized_eigenspace μ = ⨆ (k : ℕ), ⇑(f.generalized_eigenspace μ) k

theorem module.End.generalized_eigenspace_le_maximal {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] (f : module.End R M) (μ : R) (k : ℕ) :

⇑(f.generalized_eigenspace μ) k ≤ f.maximal_generalized_eigenspace μ

@[simp]

theorem module.End.mem_maximal_generalized_eigenspace {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] (f : module.End R M) (μ : R) (m : M) :

m ∈ f.maximal_generalized_eigenspace μ ↔ ∃ (k : ℕ), ⇑((f - μ • 1) ^ k) m = 0

noncomputable def module.End.maximal_generalized_eigenspace_index {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] (f : module.End R M) (μ : R) :

If there exists a natural number k such that the kernel of (f - μ • id) ^ k is the maximal generalized eigenspace, then this value is the least such k. If not, this value is not meaningful.

Equations

f.maximal_generalized_eigenspace_index μ = monotonic_sequence_limit_index (f.generalized_eigenspace μ)

theorem module.End.maximal_generalized_eigenspace_eq {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] [h : is_noetherian R M] (f : module.End R M) (μ : R) :

f.maximal_generalized_eigenspace μ = ⇑(f.generalized_eigenspace μ) (f.maximal_generalized_eigenspace_index μ)

For an endomorphism of a Noetherian module, the maximal eigenspace is always of the form kernel (f - μ • id) ^ k for some k.

theorem module.End.has_generalized_eigenvalue_of_has_generalized_eigenvalue_of_le {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] {f : module.End R M} {μ : R} {k m : ℕ} (hm : k ≤ m) (hk : f.has_generalized_eigenvalue μ k) :

f.has_generalized_eigenvalue μ m

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

theorem module.End.eigenspace_le_generalized_eigenspace {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] {f : module.End R M} {μ : R} {k : ℕ} (hk : 0 < k) :

f.eigenspace μ ≤ ⇑(f.generalized_eigenspace μ) k

The eigenspace is a subspace of the generalized eigenspace.

theorem module.End.has_generalized_eigenvalue_of_has_eigenvalue {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] {f : module.End R M} {μ : R} {k : ℕ} (hk : 0 < k) (hμ : f.has_eigenvalue μ) :

f.has_generalized_eigenvalue μ k

All eigenvalues are generalized eigenvalues.

theorem module.End.has_eigenvalue_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 : ℕ} (hμ : f.has_generalized_eigenvalue μ k) :

f.has_eigenvalue μ

All generalized eigenvalues are eigenvalues.

@[simp]

theorem module.End.has_generalized_eigenvalue_iff_has_eigenvalue {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] {f : module.End R M} {μ : R} {k : ℕ} (hk : 0 < k) :

f.has_generalized_eigenvalue μ k ↔ f.has_eigenvalue μ

Generalized eigenvalues are actually just eigenvalues.

theorem module.End.generalized_eigenspace_le_generalized_eigenspace_finrank {K : Type v} {V : Type w} [field K] [add_comm_group V] [module K V] [finite_dimensional K V] (f : module.End K V) (μ : K) (k : ℕ) :

⇑(f.generalized_eigenspace μ) k ≤ ⇑(f.generalized_eigenspace μ) (finite_dimensional.finrank K V)

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

theorem module.End.generalized_eigenspace_eq_generalized_eigenspace_finrank_of_le {K : Type v} {V : Type w} [field K] [add_comm_group V] [module K V] [finite_dimensional K V] (f : module.End K V) (μ : K) {k : ℕ} (hk : finite_dimensional.finrank K V ≤ k) :

⇑(f.generalized_eigenspace μ) k = ⇑(f.generalized_eigenspace μ) (finite_dimensional.finrank K V)

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

theorem module.End.generalized_eigenspace_restrict {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] (f : module.End R M) (p : submodule R M) (k : ℕ) (μ : R) (hfp : ∀ (x : M), x ∈ p → ⇑f x ∈ p) :

⇑(module.End.generalized_eigenspace (linear_map.restrict f hfp) μ) k = submodule.comap p.subtype (⇑(f.generalized_eigenspace μ) k)

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.

theorem module.End.eigenspace_restrict_le_eigenspace {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] (f : module.End R M) {p : submodule R M} (hfp : ∀ (x : M), x ∈ p → ⇑f x ∈ p) (μ : R) :

submodule.map p.subtype (module.End.eigenspace (linear_map.restrict f hfp) μ) ≤ f.eigenspace μ

If p is an invariant submodule of an endomorphism f, then the μ-eigenspace of the restriction of f to p is a submodule of the μ-eigenspace of f.

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

disjoint (f.generalized_eigenrange μ (finite_dimensional.finrank K V)) (⇑(f.generalized_eigenspace μ) (finite_dimensional.finrank K V))

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

theorem module.End.eigenspace_restrict_eq_bot {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] {f : module.End R M} {p : submodule R M} (hfp : ∀ (x : M), x ∈ p → ⇑f x ∈ p) {μ : R} (hμp : disjoint (f.eigenspace μ) p) :

module.End.eigenspace (linear_map.restrict f hfp) μ = ⊥

If an invariant subspace p of an endomorphism f is disjoint from the μ-eigenspace of f, then the restriction of f to p has trivial μ-eigenspace.

theorem module.End.pos_finrank_generalized_eigenspace_of_has_eigenvalue {K : Type v} {V : Type w} [field K] [add_comm_group V] [module K V] [finite_dimensional K V] {f : module.End K V} {k : ℕ} {μ : K} (hx : f.has_eigenvalue μ) (hk : 0 < k) :

0 < finite_dimensional.finrank K ↥(⇑(f.generalized_eigenspace μ) k)

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] [module K V] {f : module.End K V} {μ : K} {n : ℕ} :

submodule.map f (f.generalized_eigenrange μ n) ≤ f.generalized_eigenrange μ n

A linear map maps a generalized eigenrange into itself.