OAI/Analysis/KadisonKastler/OperatorCochainStar.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Involution symmetrization of operator-valued cochains

  1. def OAI.KadisonKastler.cochainSharp line 15
  2. theorem OAI.KadisonKastler.cochainSharp_apply line 20
  3. def OAI.KadisonKastler.bilinearSharp line 23
  4. theorem OAI.KadisonKastler.bilinearSharp_apply line 31
  5. theorem OAI.KadisonKastler.matrix_cochainSharp line 34
  6. theorem OAI.KadisonKastler.matrix_bilinearSharp line 41
  7. theorem OAI.KadisonKastler.bilinearSharp_coboundary line 48
  8. theorem OAI.KadisonKastler.bilinearSharp_sub line 55
  9. def OAI.KadisonKastler.cochainSymmetrize line 60
  10. theorem OAI.KadisonKastler.cochainSymmetrize_star line 63
  11. theorem OAI.KadisonKastler.cochainSymmetrize_residual line 67
  12. theorem OAI.KadisonKastler.operator_cochainSharp_bound line 88
  13. theorem OAI.KadisonKastler.operator_bilinearSharp_bound line 94
  14. theorem OAI.KadisonKastler.operator_cochainSymmetrize_bound line 102
  15. theorem OAI.KadisonKastler.operator_cochainSymmetrize_residual_bound line 119