OAI/Analysis/BoundedHochschild/CentralRowCompression.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The row exhausting a central support compresses the averaging operator through the original projection corner.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.centralSupportRow_compression_term line 21
  2. theorem OAI.BoundedHochschild.KadisonRingrose.centralSupportRow_compression_norm_le line 70