OAI/Analysis/BoundedHochschild/RepresentedAveragingOrbit.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The compact orbit of the original factorization operator under normalized right averages. Membership in the original algebra is preserved on its closure.

  1. def OAI.BoundedHochschild.KadisonRingrose.representedAveragingOrbit line 19
  2. def OAI.BoundedHochschild.KadisonRingrose.closedRepresentedAveragingOrbit line 24
  3. lemma OAI.BoundedHochschild.KadisonRingrose.weakRepresentedRightAverage_mem_orbit line 28
  4. lemma OAI.BoundedHochschild.KadisonRingrose.representedAveragingOrbit_self line 38
  5. lemma OAI.BoundedHochschild.KadisonRingrose.representedAveragingOrbit_invariant line 47
  6. theorem OAI.BoundedHochschild.KadisonRingrose.closedRepresentedAveragingOrbit_invariant line 61
  7. theorem OAI.BoundedHochschild.KadisonRingrose.closedRepresentedAveragingOrbit_isCompact line 69
  8. theorem OAI.BoundedHochschild.KadisonRingrose.closedRepresentedAveragingOrbit_subset_candidates line 77