OAI/Analysis/BoundedHochschild/CompletelyBoundedLastSlices.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Uniformly completely bounded last slices and their module-averaged primitive. Only the last variable needs a complete bound for this step.

  1. def OAI.BoundedHochschild.KadisonRingrose.LastSliceEstimate line 15
  2. def OAI.BoundedHochschild.KadisonRingrose.cbCurryRight line 19
  3. lemma OAI.BoundedHochschild.KadisonRingrose.cbCurryRight_val line 25
  4. lemma OAI.BoundedHochschild.KadisonRingrose.cbCurryRight_apply line 29
  5. lemma OAI.BoundedHochschild.KadisonRingrose.cbLeftSandwich_apply line 33
  6. def OAI.BoundedHochschild.KadisonRingrose.averagedLastMultilinear line 36
  7. lemma OAI.BoundedHochschild.KadisonRingrose.averagedLastMultilinear_apply line 42
  8. lemma OAI.BoundedHochschild.KadisonRingrose.averagedLastMultilinear_bound line 47
  9. def OAI.BoundedHochschild.KadisonRingrose.averagedLastCochain line 57
  10. lemma OAI.BoundedHochschild.KadisonRingrose.averagedLastCochain_apply line 62
  11. lemma OAI.BoundedHochschild.KadisonRingrose.averagedLastCochain_norm line 67
  12. lemma OAI.BoundedHochschild.KadisonRingrose.completelyBounded_id line 73
  13. def OAI.BoundedHochschild.KadisonRingrose.cbIdentity line 79
  14. def OAI.BoundedHochschild.KadisonRingrose.cbLeftMul line 82
  15. lemma OAI.BoundedHochschild.KadisonRingrose.cbLeftMul_apply line 84
  16. lemma OAI.BoundedHochschild.KadisonRingrose.moduleProjection_leftMul line 87