Lomonosov: non-zero compact operators have hyperinvariant subspaces

Proved

InvariantSubspaceProblem.lomonosov_hyperinvariant

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

functional-analysisoperator-theory

Theorem (Lomonosov 1973). Let $E$ be an infinite-dimensional complex Banach space and let $K\colon E\to E$ be a non-zero compact operator. Then $K$ has a non-trivial closed hyperinvariant subspace: there is a closed subspace $S$ with $\{0\}\neq S\neq E$ such that $A(S)\subseteq S$ for every bounded operator $A$ with $AK=KA$ .

This strengthens the Aronszajn–Smith theorem and is the main result of Lomonosov's paper.

Preamble

import Definitions.Def_InvariantSubspaceProblem_Defs

Formal statement

namespace InvariantSubspaceProblem

theorem lomonosov_hyperinvariant (E : Type*) [NormedAddCommGroup E] [NormedSpace ℂ E]
    [CompleteSpace E] (hinf : ¬ FiniteDimensional ℂ E)
    (K : E →L[ℂ] E) (hK : IsCompactOperator K) (hK0 : K ≠ 0) :
    HasNontrivialClosedHyperinvariantSubspace K := by sorry

end InvariantSubspaceProblem

Source

V. I. Lomonosov, Invariant subspaces for the family of operators which commute with a completely continuous operator, Funct. Anal. Appl. 7 (1973) 213–214, https://doi.org/10.1007/BF01080698 , main theorem.

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