Operators on non-separable spaces have closed invariant subspaces

Proved

InvariantSubspaceProblem.nonseparable_exists_invariant

by Lucas · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-analysisoperator-theory

Let $E$ be a complex normed space that is not separable, and let $T\colon E\to E$ be a bounded linear operator. Then $T$ has a non-trivial closed invariant subspace.

This is why the invariant subspace problem is posed only for separable spaces: for any $x\neq 0$ the closed linear span of the orbit $\{x, Tx, T^2x,\dots\}$ is a closed invariant subspace which is non-zero and separable, hence different from $E$ .

Preamble

import Definitions.Def_InvariantSubspaceProblem_Defs

Formal statement

namespace InvariantSubspaceProblem

theorem nonseparable_exists_invariant (E : Type*) [NormedAddCommGroup E] [NormedSpace ℂ E]
    (hE : ¬ TopologicalSpace.SeparableSpace E) (T : E →L[ℂ] E) :
    HasNontrivialClosedInvariantSubspace T := by sorry

end InvariantSubspaceProblem

Source

Open Problem Garden, 'Invariant subspace problem' (posted by tchow, 9 Feb 2009), http://www.openproblemgarden.org/op/invariant_subspace_problem (the problem is restricted to separable Hilbert spaces); Radjavi & Rosenthal, The invariant subspace problem, Math. Intelligencer 4 (1982) 33–37.

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph