OAI/Analysis/KadisonSimilarity/Tracial/MatrixDiffuseSource.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Projection comparison and small diagonal matrix corners show that each finite matrix amplification of the prescribed source is diffuse.

  1. theorem OAI.KadisonSimilarity.TracialCornerGeometry.proper_subprojection_of_small_trace line 18
  2. theorem OAI.KadisonSimilarity.matrix_diffuse_of_tower line 68