Lomonosov: operators commuting with a compact operator
ProvedInvariantSubspaceProblem.lomonosovfunctional-analysisoperator-theory
Theorem (Lomonosov 1973). Let be an infinite-dimensional complex Banach space and let be a bounded operator. If commutes with some non-zero compact operator (i.e. ), then has a non-trivial closed invariant subspace.
This is the form in which Lomonosov's theorem is usually quoted; it covers, for example, all operators that are polynomially compact.
Preamble
import Definitions.Def_InvariantSubspaceProblem_Defs
Formal statement
namespace InvariantSubspaceProblem
theorem lomonosov (E : Type*) [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
(hinf : ¬ FiniteDimensional ℂ E) (T K : E →L[ℂ] E) (hK : IsCompactOperator K)
(hK0 : K ≠ 0) (hTK : T * K = K * T) :
HasNontrivialClosedInvariantSubspace T := by sorry
end InvariantSubspaceProblemSource
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 , consequence of the main theorem.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.