Invariant Subspace Problem
Exact formalization occurrence from the upstream source collection.
- Source category
- research open
- Formal proof
- Not retained
- Vela current state
- No Repository Result attached
Question
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}.Lean declaration
Open source viewtheorem Invariant_subspace_problem [InnerProductSpace ℂ H] [TopologicalSpace.SeparableSpace H]
[CompleteSpace H] (hdim : 2 ≤ Module.rank ℂ H) (T : H →L[ℂ] H) :
Nonempty (ClosedInvariantSubspace T)