OAI/Analysis/KadisonKastler/PointedBlockMoments.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Product moments for disjoint finite matrix blocks

  1. def OAI.KadisonKastler.matrixSiteBlockWord line 15
  2. theorem OAI.KadisonKastler.matrixSiteBlockWord_indices line 20
  3. theorem OAI.KadisonKastler.matrixSiteBlockWord_weight line 26
  4. theorem OAI.KadisonKastler.PointedMatrixSites.wordWeight_append line 43
  5. theorem OAI.KadisonKastler.PointedMatrixSites.blockWord_eval line 48
  6. theorem OAI.KadisonKastler.PointedMatrixSites.disjoint_blockEntry_moment line 58
  7. theorem OAI.KadisonKastler.PointedMatrixSites.disjoint_block_algebra_independent line 77
  8. theorem OAI.KadisonKastler.PointedMatrixSites.disjoint_three_blockEntry_moment line 104