OAI/Analysis/BoundedHochschild/FiniteGroupModuleAverages.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Finite group averaging on arbitrary bounded linear maps. Unlike the simultaneous infinite module projection, this elementary contraction does not require complete boundedness and preserves normality.

  1. def OAI.BoundedHochschild.KadisonRingrose.finiteGroupRightAverage line 17
  2. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupRightAverage_apply line 20
  3. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupRightAverage_norm line 25
  4. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupRightAverage_module line 43
  5. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupRightAverage_span_module line 58
  6. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupRightAverage_fixes line 67
  7. def OAI.BoundedHochschild.KadisonRingrose.finiteGroupRightAverageCLM line 77
  8. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupRightAverageCLM_apply line 90
  9. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupRightAverage_idempotent line 93
  10. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupRightAverage_covariance line 97
  11. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupRightAverage_normal line 106