OAI/Analysis/KadisonKastler/CochainStarBounds.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Involution symmetrization preserves cochain bounds in the represented algebra.

  1. theorem OAI.KadisonKastler.cochainSharp_bound line 14
  2. theorem OAI.KadisonKastler.bilinearSharp_bound line 20
  3. theorem OAI.KadisonKastler.cochainSymmetrize_bound line 28
  4. theorem OAI.KadisonKastler.cochainSymmetrize_residual_bound line 45