OAI/Analysis/BoundedHochschild/CompactFamilyAverages.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Compactness and restriction of joint averaging orbits.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.weakFamilyAverageOrbit_component line 19
  2. lemma OAI.BoundedHochschild.KadisonRingrose.weakFamilyAverageOrbit_nonempty line 29
  3. theorem OAI.BoundedHochschild.KadisonRingrose.weakFamilyAverageOrbit_isCompact line 33
  4. theorem OAI.BoundedHochschild.KadisonRingrose.weakFamilyAverageOrbit_restriction_lift line 40