OAI/Analysis/BoundedHochschild/WeakRepresentationAverages.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Continuity of the lifted averaging operators and of the map back to coefficients of the original algebra.

  1. def OAI.BoundedHochschild.KadisonRingrose.weakRepresentedRightAverage line 20
  2. lemma OAI.BoundedHochschild.KadisonRingrose.weakRepresentedRightAverage_continuous line 24
  3. def OAI.BoundedHochschild.KadisonRingrose.weakFactorValue line 43
  4. lemma OAI.BoundedHochschild.KadisonRingrose.weakFactorValue_continuous line 47
  5. lemma OAI.BoundedHochschild.KadisonRingrose.weakRepresentedRightAverage_mem_ball line 59