OAI/Analysis/BoundedHochschild/AveragingOrbitFactorization.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

All maps in a closed averaging orbit admit the same representation and left factor as its initial map. Only the bounded right factor changes.

  1. def OAI.BoundedHochschild.KadisonRingrose.weakNormalOperatorFamily line 20
  2. lemma OAI.BoundedHochschild.KadisonRingrose.weakNormalOperatorFamily_continuous line 24
  3. lemma OAI.BoundedHochschild.KadisonRingrose.weakNormalOperatorFamily_image line 30
  4. theorem OAI.BoundedHochschild.KadisonRingrose.weakRightAverageOrbit_fixed_factorization line 40