Invariant Subspace Problem

Reference: Wikipedia, Chalendar-Partington

structure ClosedInvariantSubspace {H : Type u_1} [NormedAddCommGroup H] [Module ℂ H] (T : H →L[ℂ] H) : Type u_1

ClosedInvariantSubspace T is the type of non-trivial (different from H and {0}) closed subspaces of a complex vector space H that are invariant under the action of linear map T.

• toSubspace : Submodule ℂ H
• ne_bot : self.toSubspace ≠ ⊥
• ne_top : self.toSubspace ≠ ⊤
• is_closed : IsClosed ↑self.toSubspace
• is_fixed : Submodule.map T self.toSubspace ≤ self.toSubspace

theorem Invariant_subspace_problem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [TopologicalSpace.SeparableSpace H] [CompleteSpace H] (hdim : 2 ≤ Module.rank ℂ H) (T : H →L[ℂ] H) : Nonempty (ClosedInvariantSubspace T)

Show that every bounded linear operator T : H → H on a separable Hilbert space H of dimension at least 2 has a non-trivial closed T-invariant subspace: a closed linear subspace W of H, which is different from H and from {0}, such that T ( W ) ⊂ W. One needs the assumption that the dimension of H is at least 2 because otherwise any subspace would be either H or {0}.

theorem Invariant_subspace_problem_finite_dimensional {H : Type u_1} [NormedAddCommGroup H] [Module ℂ H] (h : FiniteDimensional ℂ H) (hdim : 2 ≤ Module.rank ℂ H) (T : H →L[ℂ] H) : Nonempty (ClosedInvariantSubspace T)

Every (bounded) linear operator T : H → H on a finite-dimensional linear space H of dimension at least 2 has a non-trivial (closed) T-invariant subspace. This can be solved using the Jordan normal form, which is not yet in mathlib.

theorem Invariant_subspace_problem_non_separable {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (h : ¬TopologicalSpace.SeparableSpace H) (T : H →L[ℂ] H) : Nonempty (ClosedInvariantSubspace T)

Every bounded linear operator T : H → H on a non-separable Hilbert space H has a non-trivial closed T-invariant subspace. Such an invariant space is given by considering the closure of the linear span of the orbit of any single non-zero vector.

theorem Invariant_subspace_problem_normal_operator {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (hdim : 2 ≤ Module.rank ℂ H) (T : H →L[ℂ] H) [IsStarNormal T] : Nonempty (ClosedInvariantSubspace T)

Every normal linear operator T : H → H on a Hilbert space H of dimension at least 2 has a non-trivial closed T-invariant subspace. If T is a multiple of the identity, one can take any non-trivial subspace . If not, one can take any nontrivial spectral subspace of T.

theorem Invariant_subspace_problem_l1 : ∃ (T : ↥(lp (fun (x : ℕ) => ℂ) 1) →L[ℂ] ↥(lp (fun (x : ℕ) => ℂ) 1)), IsEmpty (ClosedInvariantSubspace T)

There exists a bounded linear operator T on the l1 space (lp (fun (_ : ℕ) => ℂ) 1)) without non-trivial closed T-invariant subspace Read 1985, see also the first counterexample by Enflo Enflo 1987, submitted in 1981.