Argyros–Haydon: a scalar-plus-compact Banach space

Open

InvariantSubspaceProblem.argyros_haydon_scalar_plus_compact

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

functional-analysisoperator-theory

Theorem (Argyros–Haydon 2011). There exists a separable, infinite-dimensional real Banach space $E$ on which every bounded linear operator $T\colon E\to E$ has the form

T=\lambda I+K,\qquad \lambda\in\mathbb{R},\ K \text{ compact}.

This solves the scalar-plus-compact problem; it is cited as reference [4] of the source.

Formalization Note The space is existentially quantified (in Type). Separability records that the constructed space has a Schauder basis.

Preamble

import Definitions.Def_InvariantSubspaceProblem_Defs

Formal statement

namespace InvariantSubspaceProblem

theorem argyros_haydon_scalar_plus_compact :
    ∃ (E : Type) (_ : NormedAddCommGroup E) (_ : NormedSpace ℝ E) (_ : CompleteSpace E),
      TopologicalSpace.SeparableSpace E ∧ ¬ FiniteDimensional ℝ E ∧
      ∀ T : E →L[ℝ] E, ∃ (c : ℝ) (K : E →L[ℝ] E), IsCompactOperator K ∧ T = c • 1 + K := by sorry

end InvariantSubspaceProblem

Source

S. A. Argyros & R. G. Haydon, A hereditarily indecomposable L∞-space that solves the scalar-plus-compact problem, Acta Math. 206 (2011) 1–54, arXiv:0903.3921 , main theorem; cited as [4] in Open Problem Garden, 'Invariant subspace problem' (posted by tchow, 9 Feb 2009), http://www.openproblemgarden.org/op/invariant_subspace_problem.

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