OAI/Analysis/BoundedHochschild/StrongRowDefect.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The square-root defect of a strongly normalized row tends strongly to zero. Its extra averaging term therefore disappears even if the left representation is not normal.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.represented_norm_sq line 22
  2. lemma OAI.BoundedHochschild.KadisonRingrose.rowDefect_strong_zero line 28
  3. lemma OAI.BoundedHochschild.KadisonRingrose.rowDefect_average_strong_zero line 52