OAI/Analysis/KadisonSimilarity/Tracial/ConcreteMatrixTower.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Coordinate maps for the actual increasing matrix stages. These maps retain the concrete operators and their normalized traces.

  1. def OAI.KadisonSimilarity.concreteStageEquiv line 20
  2. theorem OAI.KadisonSimilarity.concreteStageEquiv_apply line 26
  3. def OAI.KadisonSimilarity.generatedStageEmbedding line 33
  4. theorem OAI.KadisonSimilarity.generatedStageEmbedding_apply line 39
  5. def OAI.KadisonSimilarity.generatedMatrixTrace line 45
  6. def OAI.KadisonSimilarity.generatedMatrixVector line 49
  7. theorem OAI.KadisonSimilarity.generatedMatrixVector_apply line 53
  8. theorem OAI.KadisonSimilarity.generatedMatrixVector_inner line 57
  9. theorem OAI.KadisonSimilarity.generatedMatrixTrace_dist line 63
  10. theorem OAI.KadisonSimilarity.generatedMatrixTrace_one line 71
  11. theorem OAI.KadisonSimilarity.generatedMatrixTrace_tracial line 75
  12. theorem OAI.KadisonSimilarity.generatedMatrixTrace_faithful line 80
  13. theorem OAI.KadisonSimilarity.generatedMatrixTrace_normal line 87
  14. def OAI.KadisonSimilarity.generatedStageTransition line 96
  15. theorem OAI.KadisonSimilarity.generatedStageTransition_compatible line 102
  16. theorem OAI.KadisonSimilarity.generatedStageEmbedding_trace line 116
  17. theorem OAI.KadisonSimilarity.generatedStage_concrete_approximation line 125
  18. theorem OAI.KadisonSimilarity.generatedStage_vector_approximation line 143
  19. theorem OAI.KadisonSimilarity.generatedStage_vectors_dense line 153
  20. def OAI.KadisonSimilarity.concreteNestedTracialMatrices line 162

    Source documentation

    The matrix presentation required by the commutator argument comes from the actual increasing matrix subalgebras and their weak closure.

    def concreteNestedTracialMatrices (υ : TracialRepresentation N) :
    NestedTracialMatrices (A := fun n => Fin (F n).size)
…

    Mentions: OAI.KadisonSimilarity.NestedTracialMatrices