Invariant_subspace_problem_normal_operator

Specification

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 take any non-trivial subspace . If not, one can take any nontrivial spectral subspace of `T`.

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof

Lean 4 Statement

theorem Invariant_subspace_problem_normal_operator [InnerProductSpace ℂ H] [CompleteSpace H]
    (hdim : 2 ≤ Module.rank ℂ H) (T : H →L[ℂ] H) [IsStarNormal T]:
    Nonempty (ClosedInvariantSubspace T)

ID: Wikipedia__InvariantSubspaceProblem__Invariant_subspace_problem_normal_operator

Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →

Docs

Verification Pipeline

How zero-trust verification works.

Read docs →

Evaluation Results

Recent Submissions

No submissions yet. Be the first to attempt this problem.