OAI/Analysis/BoundedHochschild/CountableMatrixAverage.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

A fixed contractive map of the cochain complex into the matrix-unit multimodular cochains, obtained from the actual finite-group averages. Its action on cohomology is not asserted here.

  1. def OAI.BoundedHochschild.KadisonRingrose.matrixAverageUltrafilter line 23
  2. lemma OAI.BoundedHochschild.KadisonRingrose.matrix_average_limit_exists line 25
  3. def OAI.BoundedHochschild.KadisonRingrose.countableMatrixAverage line 33
  4. lemma OAI.BoundedHochschild.KadisonRingrose.countableMatrixAverage_norm line 38
  5. lemma OAI.BoundedHochschild.KadisonRingrose.countableMatrixAverage_tendsto line 44
  6. lemma OAI.BoundedHochschild.KadisonRingrose.countableMatrixAverage_add line 51
  7. lemma OAI.BoundedHochschild.KadisonRingrose.countableMatrixAverage_smul line 60
  8. def OAI.BoundedHochschild.KadisonRingrose.countableMatrixAverageCLM line 69
  9. lemma OAI.BoundedHochschild.KadisonRingrose.countableMatrixAverage_multimodular line 83
  10. lemma OAI.BoundedHochschild.KadisonRingrose.countableMatrixAverage_differential line 96
  11. lemma OAI.BoundedHochschild.KadisonRingrose.countableMatrixAverage_cocycle line 105
  12. theorem OAI.BoundedHochschild.KadisonRingrose.primitive_of_countableMatrixAverage line 122