OAI/Analysis/KadisonKastler/FiniteBlockExtension.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Finite blocks of a countable amplification

Finite operator matrices act on the first finitely many matrix summands. Their extension is an isometric nonunital star homomorphism. These are the bounded approximants used for the infinite-amplification gap estimate.

  1. def OAI.KadisonKastler.FullMatrixCorner.blockElement line 25
  2. theorem OAI.KadisonKastler.FullMatrixCorner.blockElement_mul line 28
  3. theorem OAI.KadisonKastler.FullMatrixCorner.blockElement_star line 43
  4. theorem OAI.KadisonKastler.FullMatrixCorner.matrixEntry_blockElement line 47
  5. theorem OAI.KadisonKastler.FullMatrixCorner.matrixEntry_sum line 65
  6. def OAI.KadisonKastler.FullMatrixCorner.finiteBlock line 71
  7. theorem OAI.KadisonKastler.FullMatrixCorner.matrixEntry_finiteBlock line 74
  8. theorem OAI.KadisonKastler.FullMatrixCorner.finiteBlock_mul line 89
  9. def OAI.KadisonKastler.FullMatrixCorner.finiteBlockHom line 115
  10. theorem OAI.KadisonKastler.FullMatrixCorner.finiteBlockHom_injective line 126
  11. theorem OAI.KadisonKastler.FullMatrixCorner.norm_finiteBlock line 141