MatrixSequences.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Finite matrices and bounded sequences

Entrywise evaluation identifies bounded sequences of finite matrices with finite matrices of bounded sequences. Applying a tracial quotient to the entries gives the normalized matrix trace formula.

def OAI.KadisonKastler.matrixEntrySequence line 32
Source documentation
A matrix entry of a bounded sequence is itself a bounded sequence.
```
def matrixEntrySequence (x : BoundedSequence (CStarMatrix ι ι B)) (i j : ι) :
    BoundedSequence B :=
…
```
Mentions: OAI.KadisonKastler.BoundedSequence
theorem OAI.KadisonKastler.matrixEntrySequence_apply line 39
def OAI.KadisonKastler.matrixSequenceOfEntries line 43
Source documentation
Assemble finitely many bounded entries into a bounded matrix sequence.
```
def matrixSequenceOfEntries (x : CStarMatrix ι ι (BoundedSequence B)) :
    BoundedSequence (CStarMatrix ι ι B) where
…
```
Mentions: OAI.KadisonKastler.BoundedSequence
theorem OAI.KadisonKastler.matrixSequenceOfEntries_apply line 58
theorem OAI.KadisonKastler.boundedSequence_sum_apply line 62
def OAI.KadisonKastler.sequenceMatrixHom line 67
Source documentation
Entrywise transposition of the sequence index and matrix indices.
```
def sequenceMatrixHom : BoundedSequence (CStarMatrix ι ι B) →⋆ₐ[ℂ]
    CStarMatrix ι ι (BoundedSequence B) where
…
```
Mentions: OAI.KadisonKastler.BoundedSequence
theorem OAI.KadisonKastler.sequenceMatrixHom_apply line 98
theorem OAI.KadisonKastler.sequenceMatrixHom_bijective line 101
def OAI.KadisonKastler.sequenceMatrixEquiv line 112
Source documentation
The actual star-algebra equivalence between the two bounded-sequence constructions.
```
def sequenceMatrixEquiv : BoundedSequence (CStarMatrix ι ι B) ≃⋆ₐ[ℂ]
    CStarMatrix ι ι (BoundedSequence B) :=
…
```
Mentions: OAI.KadisonKastler.BoundedSequence
theorem OAI.KadisonKastler.sequenceMatrixEquiv_apply line 117
theorem OAI.KadisonKastler.norm_sequenceMatrixEquiv line 120
def OAI.KadisonKastler.matrixSequenceQuotient line 128
Source documentation
Apply a tracial quotient to each finite matrix entry.
```
def matrixSequenceQuotient (Q : TraceQuotientMap τ σ ω) :
    BoundedSequence (CStarMatrix ι ι B) →⋆ₐ[ℂ] CStarMatrix ι ι C :=
…
```
Mentions: OAI.KadisonKastler.TraceQuotientMap, OAI.KadisonKastler.BoundedSequence
theorem OAI.KadisonKastler.matrixSequenceQuotient_apply line 134
theorem OAI.KadisonKastler.matrixSequenceQuotient_surjective line 139
theorem OAI.KadisonKastler.matrixSequenceQuotient_trace_limit line 153
def OAI.KadisonKastler.TraceQuotientMap.matrix line 164
Source documentation
The entrywise quotient is itself a tracial quotient of finite matrix algebras.
```
def TraceQuotientMap.matrix (Q : TraceQuotientMap τ σ ω) :
    TraceQuotientMap (matrixTrace (ι := ι) τ) (matrixTrace (ι := ι) σ) ω where
…
```
Mentions: OAI.KadisonKastler.TraceQuotientMap, OAI.KadisonKastler.matrixTrace