Read: an operator on ℓ¹ without closed invariant subspaces

Open

InvariantSubspaceProblem.read_counterexample_l1

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

functional-analysisoperator-theory

Theorem (Read 1985). There is a bounded linear operator $T$ on the complex sequence space

\ell^1(\mathbb{N})=\Big\{(a_n)_{n\ge 0}\subseteq\mathbb{C} : \sum_n |a_n|<\infty\Big\}

that has no non-trivial closed invariant subspace.

This gives a counterexample on a classical Banach space, in contrast with Enflo's specially constructed space.

Formalization Note $\ell^1$ is Mathlib's lp (fun _ : ℕ => ℂ) 1 with its usual norm.

Preamble

import Definitions.Def_InvariantSubspaceProblem_Defs

Formal statement

namespace InvariantSubspaceProblem

theorem read_counterexample_l1 :
    ∃ T : lp (fun _ : ℕ => ℂ) 1 →L[ℂ] lp (fun _ : ℕ => ℂ) 1,
      ¬ HasNontrivialClosedInvariantSubspace T := by sorry

end InvariantSubspaceProblem

Source

C. J. Read, A solution to the invariant subspace problem on the space l1, Bull. London Math. Soc. 17 (1985) 305–317, https://doi.org/10.1112/blms/17.4.305 , 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