Normal operators have closed invariant subspaces

Proved

InvariantSubspaceProblem.normal_exists_invariant

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

functional-analysisoperator-theory

Let $H$ be a complex Hilbert space of dimension at least $2$ and let $T\colon H\to H$ be a bounded normal operator, i.e. $T^*T=TT^*$ . Then $T$ has a non-trivial closed invariant subspace.

This is a classical consequence of the spectral theorem for normal operators and is one of the standard positive partial results on the invariant subspace problem.

Formalization Note Normality is Mathlib's IsStarNormal for the C*-algebra of bounded operators on $H$ ; the dimension hypothesis is $\operatorname{rank}_{\mathbb{C}} H>1$ (cardinal-valued, so infinite dimension is included). Separability is not assumed.

Preamble

import Definitions.Def_InvariantSubspaceProblem_Defs

Formal statement

namespace InvariantSubspaceProblem

theorem normal_exists_invariant (H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℂ H]
    [CompleteSpace H] (hdim : 1 < Module.rank ℂ H) (T : H →L[ℂ] H) [IsStarNormal T] :
    HasNontrivialClosedInvariantSubspace T := by sorry

end InvariantSubspaceProblem

Source

Radjavi & Rosenthal, Invariant Subspaces, Springer 1973 (normal operators); Open Problem Garden, 'Invariant subspace problem' (posted by tchow, 9 Feb 2009), http://www.openproblemgarden.org/op/invariant_subspace_problem, overview references [2],[3],[5].

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