HilbertMatrixGeneration.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Finite or countable matrix coordinates on separable Hilbert spaces

theorem OAI.KadisonKastler.separable_hilbertBasis_dichotomy line 19

Source documentation

A separable Hilbert space has either finite or natural-number matrix coordinates.

theorem separable_hilbertBasis_dichotomy [TopologicalSpace.SeparableSpace H] :
    (∃ n : ℕ, Nonempty (OrthonormalBasis (Fin n) ℂ H)) ∨
      Nonempty (HilbertBasis ℕ ℂ H) := by
…

theorem OAI.KadisonKastler.mem_of_hilbertMatrixUnits line 56

Source documentation

Rank-one entries of a Hilbert basis generate all ambient operators.

theorem mem_of_hilbertMatrixUnits {ι : Type*} [Nonempty ι]
    (b : HilbertBasis ι ℂ H) (Q : VonNeumannAlgebra H)
    (hQ : ∀ i j, InnerProductSpace.rankOne ℂ (b i) (b j) ∈ Q)
    (T : H →L[ℂ] H) : T ∈ Q := by
…

def OAI.KadisonKastler.hilbertBasisInitialSpace line 87
Source documentation
The initial rank-one corner of a natural-number Hilbert basis.
```
def hilbertBasisInitialSpace (b : HilbertBasis ℕ ℂ H) : Submodule ℂ H :=
…
```
instance OAI.KadisonKastler.(instance at line 90) line 90
def OAI.KadisonKastler.hilbertBasisFullCorner line 95
Source documentation
Concrete full countable matrix units on the original Hilbert space.
```
def hilbertBasisFullCorner (b : HilbertBasis ℕ ℂ H) :
    FullMatrixCorner (hilbertBasisInitialSpace b) where
…
```
Mentions: OAI.KadisonKastler.FullMatrixCorner, OAI.KadisonKastler.hilbertBasisInitialSpace
theorem OAI.KadisonKastler.hilbertBasisFullCorner_mem_scalar line 113