OAI/Analysis/BoundedHochschild/ProjectionNormGap.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A positive lower bound on the off-diagonal part of an operator prevents its diagonal compression from retaining the full norm.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.projection_norm_sq_split line 19
  2. lemma OAI.BoundedHochschild.KadisonRingrose.projection_compression_norm_of_le line 37
  3. lemma OAI.BoundedHochschild.KadisonRingrose.opNorm_sq_le_of_apply_sq_le line 50
  4. lemma OAI.BoundedHochschild.KadisonRingrose.no_positive_offDiagonal_gap line 60