VaryingSequence.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Bounded products for the finite-matrix model

The matrix sizes in the preliminary free model vary with the coordinate. The existing lp space at infinity supplies its ordinary bounded-product C*-algebra, without identifying the operator norm with a tracial norm.

abbrev OAI.KadisonKastler.VaryingBoundedSequence line 21
instance OAI.KadisonKastler.varyingSequenceCStarAlgebra line 23
def OAI.KadisonKastler.varyingSequenceEval line 32
Source documentation
Evaluation in the j-th finite factor.
```
def varyingSequenceEval (j : ℕ) : VaryingBoundedSequence B →⋆ₐ[ℂ] B j where
…
```
Mentions: OAI.KadisonKastler.VaryingBoundedSequence
theorem OAI.KadisonKastler.varyingSequence_norm_apply_le line 44
def OAI.KadisonKastler.varyingSequenceMap line 51
Source documentation
Coordinate star embeddings into a fixed factor induce the map on bounded products used for the finite-matrix model.
```
def varyingSequenceMap (φ : ∀ j, B j →⋆ₐ[ℂ] C) :
    VaryingBoundedSequence B →⋆ₐ[ℂ] BoundedSequence C where
…
```
Mentions: OAI.KadisonKastler.VaryingBoundedSequence, OAI.KadisonKastler.BoundedSequence
theorem OAI.KadisonKastler.varyingSequenceMap_apply line 68