OAI/Analysis/KadisonKastler/PointedFiniteBlock.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Full matrix blocks on finitely many product sites

The index type records one binary matrix index at each site. Distinct sites commute, so their ordered products form a full matrix system. This is the finite algebraic construction needed for the product stages.

  1. abbrev OAI.KadisonKastler.MatrixSiteBlockIndex line 21
  2. instance OAI.KadisonKastler.matrixSiteBlockIndexFintype line 25
  3. instance OAI.KadisonKastler.matrixSiteBlockIndexDecidableEq line 31
  4. def OAI.KadisonKastler.matrixSiteBlockZero line 38
  5. instance OAI.KadisonKastler.(instance at line 42) line 42
  6. def OAI.KadisonKastler.matrixSiteBlockMapEquiv line 44
  7. def OAI.KadisonKastler.matrixSiteBlockIndexOfFunction line 49
  8. theorem OAI.KadisonKastler.matrixSiteBlockIndexOfFunction_congr line 53
  9. theorem OAI.KadisonKastler.matrixSiteBlockIndexOfFunction_surjective line 61
  10. def OAI.KadisonKastler.matrixSiteBlockWeight line 76
  11. theorem OAI.KadisonKastler.matrixSiteBlockWeight_ofFunction line 83
  12. theorem OAI.KadisonKastler.matrixSiteBlockWeight_map line 94
  13. def OAI.KadisonKastler.PointedMatrixSites.blockEntry line 115
  14. theorem OAI.KadisonKastler.PointedMatrixSites.blockEntry_ofFunction line 120
  15. theorem OAI.KadisonKastler.PointedMatrixSites.blockEntry_moment line 129
  16. theorem OAI.KadisonKastler.PointedMatrixSites.site_commutes_blockEntry line 136
  17. theorem OAI.KadisonKastler.PointedMatrixSites.blockEntry_star line 145
  18. theorem OAI.KadisonKastler.PointedMatrixSites.blockEntry_mul line 154
  19. theorem OAI.KadisonKastler.PointedMatrixSites.blockEntry_total line 168
  20. def OAI.KadisonKastler.PointedMatrixSites.finiteBlock line 178
  21. theorem OAI.KadisonKastler.PointedMatrixSites.finiteBlock_cons line 185
  22. theorem OAI.KadisonKastler.PointedMatrixSites.finiteBlock_le line 191
  23. theorem OAI.KadisonKastler.PointedMatrixSites.finiteBlock_le_of_sites_le line 206
  24. theorem OAI.KadisonKastler.PointedMatrixSites.site_le_finiteBlock line 218
  25. theorem OAI.KadisonKastler.PointedMatrixSites.finiteBlock_mono line 247
  26. theorem OAI.KadisonKastler.PointedMatrixSites.finiteBlock_commuting line 252