HilbertMatrix.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

This identifies the abstract C⋆-matrix norm with the operator norm on the finite Hilbert direct sum, through a faithful star representation.

def OAI.KadisonKastler.hilbertMatrix line 27
Source documentation
The action of an operator-valued matrix on a finite Hilbert direct sum.
```
def hilbertMatrix (M : CStarMatrix n n (H →L[ℂ] H)) :
    Generator.FiniteHilbert n H →L[ℂ] Generator.FiniteHilbert n H :=
…
```
Mentions: OAI.Generator.FiniteHilbert
theorem OAI.KadisonKastler.hilbertMatrix_apply line 35
theorem OAI.KadisonKastler.hilbertMatrix_mul line 41
theorem OAI.KadisonKastler.hilbertMatrix_star line 49

def OAI.KadisonKastler.hilbertMatrixHom line 60

Source documentation

The usual matrix action is a star representation.

def hilbertMatrixHom : CStarMatrix n n (H →L[ℂ] H) →⋆ₐ[ℂ]
    (Generator.FiniteHilbert n H →L[ℂ] Generator.FiniteHilbert n H) where
…

theorem OAI.KadisonKastler.hilbertMatrixHom_injective line 86
theorem OAI.KadisonKastler.norm_hilbertMatrix line 94
Source documentation
Abstract C⋆-matrix norms are the concrete direct-sum operator norms.
```
theorem norm_hilbertMatrix (M : CStarMatrix n n (H →L[ℂ] H)) : ‖hilbertMatrix M‖ = ‖M‖ :=
…
```
Mentions: OAI.KadisonKastler.hilbertMatrix