OAI/Analysis/BoundedHochschild/RepresentedAveragingConvexity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Convexity of the lifted averaging orbit.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.representedRightAverage_real_smul line 17
  2. lemma OAI.BoundedHochschild.KadisonRingrose.representedRightAverage_sum line 34
  3. lemma OAI.BoundedHochschild.KadisonRingrose.representedRightAverage_convex line 43
  4. theorem OAI.BoundedHochschild.KadisonRingrose.representedAveragingOrbit_convex line 52
  5. theorem OAI.BoundedHochschild.KadisonRingrose.closedRepresentedAveragingOrbit_convex line 65