OAI/Analysis/KadisonSimilarity/Representation/CenteredBaseDensity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Trace-zero algebra elements are dense in the actual centered base space. This extends elementary reduced-word identities to completed tensor letters.

  1. def OAI.KadisonSimilarity.TracialCornerGeometry.centeredBaseAlgebraVector line 20

    Source documentation

    The trace-zero algebra elements, with their actual centered Hilbert vectors.

    def centeredBaseAlgebraVector (a : {a : A // G.trace (a : P) = 0}) :
    centeredSubspace (G.baseVector A 1) := G.baseSymmetryLetter A a.val a.property

    Mentions: OAI.KadisonSimilarity.centeredSubspace

  2. theorem OAI.KadisonSimilarity.TracialCornerGeometry.centeredBaseAlgebraVector_dense line 23