OAI/Analysis/BoundedHochschild/FiniteModuleAverages.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A finite family of completely bounded maps admits a simultaneous right-module average, with each original complete bound retained.

  1. def OAI.BoundedHochschild.KadisonRingrose.finiteFamilyAverageOrbit line 21
  2. def OAI.BoundedHochschild.KadisonRingrose.weakFamilyAverageOrbit line 26
  3. theorem OAI.BoundedHochschild.KadisonRingrose.exists_finite_right_module_average line 30