OAI/Analysis/KadisonKastler/MatrixCommutantDistance.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Commutant distance in the presence of countable full matrix units

Finite matrix averaging and Cuntz amplification reduce the estimate to the commutant-distance formula.

  1. theorem OAI.KadisonKastler.blockDiagonal_commutator line 29
  2. theorem OAI.KadisonKastler.exists_commutant_approximation_of_complete_bound line 37
  3. theorem OAI.KadisonKastler.FullMatrixCorner.exists_commutant_approximation line 86