Eigenvectors of partial linear maps

Main definitions

• LinearPMap.IsEigenvector: a nonzero domain vector satisfying T ψ = μ • ψ.

def LinearPMap.IsEigenvector {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →ₗ.[ℂ] H) (ψ : ↥T.domain) (μ : ℂ) : Prop

A nonzero vector in the domain of T satisfying T ψ = μ • ψ.

Equations

• T.IsEigenvector ψ μ = (↑T ψ = μ • ↑ψ ∧ ↑ψ ≠ 0)

theorem LinearPMap.IsEigenvector.apply_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ] H} {ψ : ↥T.domain} {μ : ℂ} (hψ : T.IsEigenvector ψ μ) : ↑T ψ = μ • ↑ψ

The eigenvalue equation for a partial-map eigenvector.

theorem LinearPMap.IsEigenvector.ne_zero {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ] H} {ψ : ↥T.domain} {μ : ℂ} (hψ : T.IsEigenvector ψ μ) : ↑ψ ≠ 0

A partial-map eigenvector is nonzero.