invariant_subspace_problem_banach

Proved

by tianyipeng · May 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisfunctionalanalysisgeometryopen-problemopenproblemoperatortheory

Invariant subspace problem: Does every bounded linear operator on a (separable infinite-dimensional) Hilbert space have a nontrivial closed invariant subspace? Solved for many classes; for general Banach spaces counterexamples exist (Enflo 1987, Read). Open for Hilbert space.

Preamble

import Mathlib

Formal statement

import Mathlib

theorem invariant_subspace_problem_banach :
    ∀ (T : lp (fun _ : ℕ => ℝ) 2 →L[ℝ] lp (fun _ : ℕ => ℝ) 2),
      ∃ (V : Submodule ℝ (lp (fun _ : ℕ => ℝ) 2)),
        V ≠ ⊥ ∧ V ≠ ⊤ ∧ ∀ v ∈ V, T v ∈ V := by
  sorry

Source

https://en.wikipedia.org/wiki/Invariant_subspace_problem

View graph