HilbertClassification.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Hyperinvariant.orthonormal_subtype_countable line 13

Source documentation

An orthonormal subset of a separable Hilbert space is countable.

theorem orthonormal_subtype_countable [CompleteSpace H] [SeparableSpace H] (w : Set H)
    (hw : Orthonormal ℂ (Subtype.val : w → H)) : Countable w := by
…

theorem OAI.Hyperinvariant.exists_nat_hilbertBasis line 31
Source documentation
Every infinite-dimensional separable complex Hilbert space has a Hilbert basis indexed by the natural numbers.
```
theorem exists_nat_hilbertBasis (hInf : ¬FiniteDimensional ℂ H) :
    Nonempty (HilbertBasis ℕ ℂ H) := by
…
```

theorem OAI.Hyperinvariant.nonempty_linearIsometryEquiv line 56

Source documentation

This handles arbitrary ambient Hilbert spaces, not just a canonical model.

theorem nonempty_linearIsometryEquiv
    {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K]
    [CompleteSpace K] [SeparableSpace K]
    (hH : ¬FiniteDimensional ℂ H) (hK : ¬FiniteDimensional ℂ K) :
    Nonempty (H ≃ₗᵢ[ℂ] K) := by
…