OAI/Analysis/KadisonKastler/PeriodicMatrixAveraging.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Averaging over the countable matrix factor

Weak limits of finite signed-permutation averages commute with the countable matrix units, preserving both the displacement and the scalar commutator estimate.

  1. theorem OAI.KadisonKastler.isSelfAdjoint_of_weak_limit line 23
  2. theorem OAI.KadisonKastler.FullMatrixCorner.weak_limit_commutes_matrixUnits line 43
  3. theorem OAI.KadisonKastler.FullMatrixCorner.exists_matrixUnit_commuting_average line 86
  4. theorem OAI.KadisonKastler.FullMatrixCorner.commute_finiteCuntz_of_commute_matrixUnits line 121