ConcreteClippedDrift.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Clipped drift in the concrete matrix representation

This connects the support estimate for operator-valued matrices to the bounded sequences in the represented tracial ultrapower. The norm bound holds at each coordinate before the discarded tails are restored.

def OAI.KadisonKastler.concreteMatrixEntries line 45
Source documentation
Recover the matrix of original-space operators from the concrete amplified algebra.
```
def concreteMatrixEntries : Algebra (matrixVonNeumann (ι := Fin n) M) →⋆ₐ[ℂ]
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann
theorem OAI.KadisonKastler.hilbertMatrix_concreteMatrixEntries line 50
theorem OAI.KadisonKastler.concreteMatrixEntries_mem line 55
theorem OAI.KadisonKastler.concrete_spectralClipped_drift_le line 62
Source documentation
The support and through-label estimates give the actual coordinate clipped drift in the represented amplified factor.
```
theorem concrete_spectralClipped_drift_le
    (hPublished : PublishedCyclicSimilarity.{u, u} (A := Algebra M))
…
```
Mentions: OAI.KadisonKastler.Algebra