Witness.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Hyperinvariant.source_basis_orthonormal line 15
Source documentation
The fiber indicators form an orthonormal family in the complex Hilbert space.
```
theorem source_basis_orthonormal : Orthonormal ℂ sourceBasis := by
…
```
theorem OAI.Hyperinvariant.source_infiniteDimensional line 34
theorem OAI.Hyperinvariant.source_mainClaim line 42
Source documentation
The finite-factor construction yields a nonzero norm-quasinilpotent operator whose ordinary commutant has no nontrivial closed invariant subspace.
```
theorem source_mainClaim : MainClaim (H := SourceHilbert SourceCoordinate) := by
…
```
Mentions: OAI.Hyperinvariant.MainClaim