CenteredLabels.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The centered label map

The covariance matrix of the centered diagonal projections in a normalized matrix trace is d⁻¹ I - d⁻² 11*. It is the scalar multiple of the projection off the constant vectors constructed below.

def OAI.KadisonKastler.constantLabelProjection line 24
theorem OAI.KadisonKastler.constantLabelProjection_apply line 29
theorem OAI.KadisonKastler.constantLabelProjection_isStarProjection line 33
def OAI.KadisonKastler.centeredLabelProjection line 48
theorem OAI.KadisonKastler.centeredLabelProjection_isStarProjection line 50
def OAI.KadisonKastler.centeredLabelMatrix line 55
Source documentation
The label map has the d⁻¹/² scale used at every free-word cut.
```
def centeredLabelMatrix : CStarMatrix ι ι ℂ :=
…
```
theorem OAI.KadisonKastler.norm_centeredLabelMatrix_le line 58
theorem OAI.KadisonKastler.centeredLabelProjection_apply line 70
theorem OAI.KadisonKastler.centeredLabelProjection_mul_self line 74