OAI/Analysis/KadisonKastler/TracialMatrixVariance.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Uniform variance control for the finite matrix coordinates

  1. def OAI.KadisonKastler.standardAlgebraicMatrixUnits line 21
  2. theorem OAI.KadisonKastler.standardAlgebraicMatrixUnits_hom line 30
  3. def OAI.KadisonKastler.matrixUnitsOfEquiv line 36
  4. theorem OAI.KadisonKastler.matrixUnitsOfEquiv_hom line 39
  5. theorem OAI.KadisonKastler.matrixUnitsOfEquiv_surjective line 47
  6. def OAI.KadisonKastler.finiteMatrixFlatten line 52
  7. theorem OAI.KadisonKastler.finiteMatrixModel_variance_control line 61