OAI/Analysis/BoundedHochschild/Cochains.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Bounded Hochschild cochains, last-input translation and averaging.

  1. abbrev OAI.BoundedHochschild.Cochain line 12

    Also declared: ComparatorChallenges/KadisonRingrose.lean:12 (same declaration text).

  2. def OAI.BoundedHochschild.mergeInputs line 16

    Also declared: ComparatorChallenges/KadisonRingrose.lean:15 (same declaration text).

  3. def OAI.BoundedHochschild.differentialValue line 23

    Also declared: ComparatorChallenges/KadisonRingrose.lean:20 (same declaration text).

  4. theorem OAI.BoundedHochschild.differentialValue_add line 32
  5. theorem OAI.BoundedHochschild.differentialValue_smul line 39
  6. def OAI.BoundedHochschild.insertLast line 51
  7. theorem OAI.BoundedHochschild.insertLast_apply line 54
  8. theorem OAI.BoundedHochschild.norm_insertLast_le line 57
  9. theorem OAI.BoundedHochschild.snoc_succ_tuple line 68
  10. theorem OAI.BoundedHochschild.snoc_castSucc_tuple line 76
  11. theorem OAI.BoundedHochschild.mergeInputs_snoc_castSucc line 81
  12. theorem OAI.BoundedHochschild.mergeInputs_snoc_last line 97
  13. theorem OAI.BoundedHochschild.differentialValue_snoc line 111
  14. def OAI.BoundedHochschild.rightMultiply line 128
  15. theorem OAI.BoundedHochschild.rightMultiply_apply line 131
  16. def OAI.BoundedHochschild.lastHomotopy line 135
  17. theorem OAI.BoundedHochschild.lastHomotopy_apply line 138
  18. theorem OAI.BoundedHochschild.norm_rightMultiply_le line 141
  19. theorem OAI.BoundedHochschild.norm_lastHomotopy_le line 151
  20. theorem OAI.BoundedHochschild.lastHomotopy_cocycle line 158
  21. def OAI.BoundedHochschild.translateLast line 185
  22. theorem OAI.BoundedHochschild.translateLast_apply line 192
  23. theorem OAI.BoundedHochschild.norm_translateLast_le line 202
  24. theorem OAI.BoundedHochschild.translateLast_add line 216
  25. theorem OAI.BoundedHochschild.translateLast_smul line 221
  26. def OAI.BoundedHochschild.averageLast line 227
  27. theorem OAI.BoundedHochschild.summable_averageLast line 231
  28. theorem OAI.BoundedHochschild.norm_averageLast_le line 238