InvariantSubspaceProblem.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

7 declarations, 3 contain sorry, 0 declared as axioms

Invariant Subspace Problem

Reference: Wikipedia, Chalendar-Partington

Imports (1)

FormalConjecturesUtil

structure InvariantSubspaceProblem.ClosedInvariantSubspace Documented declaration: ClosedInvariantSubspace line 35 source
Source documentation
ClosedInvariantSubspace T is the type of non-trivial (different from H and {0}) closed subspaces of a complex vector space H that are invariant under the action of linear map T.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, Module, Complex, ContinuousLinearMap, RingHom.id
8 instances, coercions and auxiliary constants left out.
```
structure ClosedInvariantSubspace [Module ℂ H] (T : H →L[ℂ] H) where
…
```
theorem InvariantSubspaceProblem.Invariant_subspace_problem Documented declaration: Invariant_subspace_problem sorry line 48 source
Source documentation
Show that every bounded linear operator T : H → H on a separable Hilbert space H of dimension at least 2 has a non-trivial closed T-invariant subspace: a closed linear subspace W of H, which is different from H and from {0}, such that T ( W ) ⊂ W. One needs the assumption that the dimension of H is at least 2 because otherwise any subspace would be either H or {0}.

depends on sorry what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Complex, TopologicalSpace.SeparableSpace, CompleteSpace, LE.le, Cardinal, OfNat.ofNat, Nat, Module.rank, ContinuousLinearMap, RingHom.id, Nonempty, InvariantSubspaceProblem.ClosedInvariantSubspace
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
36 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem Invariant_subspace_problem [InnerProductSpace ℂ H] [TopologicalSpace.SeparableSpace H]
    [CompleteSpace H] (hdim : 2 ≤ Module.rank ℂ H) (T : H →L[ℂ] H) :
    Nonempty (ClosedInvariantSubspace T) := by
…
```
Mentions: InvariantSubspaceProblem.ClosedInvariantSubspace
theorem InvariantSubspaceProblem.Invariant_subspace_problem_finite_dimensional Every (bounded) linear operator T : H → H on a finite-dimensional normed space H of dimension at least 2 has a non-trivial (closed) T-invariant subspace line 61 source
Source documentation
Every (bounded) linear operator T : H → H on a finite-dimensional normed space H of dimension at least 2 has a non-trivial (closed) T-invariant subspace. Since ℂ is algebraically closed, T has an eigenvector v ≠ 0, and the line ℂ ∙ v is such a subspace.
H is a complex normed space: with a bare Module ℂ H unrelated to the norm, finite-dimensional subspaces need not be closed, and the statement fails already in complex dimension 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, NormedSpace, Complex, FiniteDimensional, LE.le, Cardinal, OfNat.ofNat, Nat, Module.rank, ContinuousLinearMap, RingHom.id, Nonempty, InvariantSubspaceProblem.ClosedInvariantSubspace
Proof uses: Nontrivial, Eq.mpr, LT.lt, id, Eq, congrArg, Eq.symm, propext, rank_pos_iff_nontrivial, lt_of_lt_of_le, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.false, Module.End.HasEigenvalue, Exists, Module.End.exists_eigenvalue and 36 more
136 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
```
theorem Invariant_subspace_problem_finite_dimensional [NormedSpace ℂ H] (h : FiniteDimensional ℂ H)
    (hdim : 2 ≤ Module.rank ℂ H) (T : H →L[ℂ] H) : Nonempty (ClosedInvariantSubspace T) := by
…
```
Mentions: InvariantSubspaceProblem.ClosedInvariantSubspace
lemma InvariantSubspaceProblem.TopologicalSpace.nontrivial_of_not_separableSpace line 89 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Not, TopologicalSpace.SeparableSpace, Nontrivial
Proof uses: Eq.mpr, Subsingleton, id, Eq, congrArg, Eq.symm, propext, not_subsingleton_iff_nontrivial, Mathlib.Tactic.Contrapose.contrapose₄, inferInstance
8 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem InvariantSubspaceProblem.Invariant_subspace_problem_non_separable Every bounded linear operator T : H → H on a non-separable Hilbert space H has a non-trivial closed T-invariant subspace line 100 source
Source documentation
Every bounded linear operator T : H → H on a non-separable Hilbert space H has a non-trivial closed T-invariant subspace. Such an invariant space is given by considering the closure of the linear span of the orbit of any single non-zero vector.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Complex, CompleteSpace, Not, TopologicalSpace.SeparableSpace, ContinuousLinearMap, RingHom.id, Nonempty, InvariantSubspaceProblem.ClosedInvariantSubspace
Proof uses: Nontrivial, InvariantSubspaceProblem.TopologicalSpace.nontrivial_of_not_separableSpace, Ne, OfNat.ofNat, Exists, exists_ne, Set, Set.range, Nat, HPow.hPow, Eq, rfl, Submodule, Submodule.topologicalClosure, Submodule.span, Nonempty.intro, InvariantSubspaceProblem.ClosedInvariantSubspace.mk, Membership.mem, Submodule.le_topologicalClosure, Submodule.subset_span and 40 more
91 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
theorem Invariant_subspace_problem_non_separable [InnerProductSpace ℂ H] [CompleteSpace H]
    (h : ¬TopologicalSpace.SeparableSpace H) (T : H →L[ℂ] H) :
    Nonempty (ClosedInvariantSubspace T) := by
…
```
Mentions: InvariantSubspaceProblem.ClosedInvariantSubspace
theorem InvariantSubspaceProblem.Invariant_subspace_problem_normal_operator Every normal linear operator T : H → H on a Hilbert space H of dimension at least 2 has a non-trivial closed T-invariant subspace sorry line 134 source
Source documentation
Every normal linear operator T : H → H on a Hilbert space H of dimension at least 2 has a non-trivial closed T-invariant subspace. If T is a multiple of the identity, one can tafrake any non-trivial subspace . If not, one can take any nontrivial spectral subspace of T.

depends on sorry what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Complex, CompleteSpace, LE.le, Cardinal, OfNat.ofNat, Nat, Module.rank, ContinuousLinearMap, RingHom.id, IsStarNormal, Nonempty, InvariantSubspaceProblem.ClosedInvariantSubspace
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
40 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem Invariant_subspace_problem_normal_operator [InnerProductSpace ℂ H] [CompleteSpace H]
    (hdim : 2 ≤ Module.rank ℂ H) (T : H →L[ℂ] H) [IsStarNormal T]:
    Nonempty (ClosedInvariantSubspace T) := by
…
```
Mentions: InvariantSubspaceProblem.ClosedInvariantSubspace
theorem InvariantSubspaceProblem.Invariant_subspace_problem_l1 Documented declaration: Invariant_subspace_problem_l1 sorry line 145 source
Source documentation
There exists a bounded linear operator T on the l1 space (lp (fun (_ : ℕ) => ℂ) 1)) without non-trivial closed T-invariant subspace Read 1985, see also the first counterexample by Enflo Enflo 1987, submitted in 1981.

L4DEL explanation
There exists a bounded linear operator T on the l1 space (lp (fun (_ : ℕ) => ℂ) 1)) without non-trivial closed T-invariant subspace Read 1985, see also the first counterexample by Enflo Enflo 1987, submitted in 1981.
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: Exists, ContinuousLinearMap, Complex, RingHom.id, Subtype, PreLp, Nat, Membership.mem, AddSubgroup, lp, OfNat.ofNat, ENNReal, IsEmpty, InvariantSubspaceProblem.ClosedInvariantSubspace
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
69 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem Invariant_subspace_problem_l1 :
    ∃ (T : (lp (fun (_ : ℕ) => ℂ) 1) →L[ℂ] (lp (fun (_ : ℕ) => ℂ) 1)),
    IsEmpty (ClosedInvariantSubspace T) := by
…
```
Mentions: InvariantSubspaceProblem.ClosedInvariantSubspace