OAI/Analysis/BoundedHochschild/CochainAverages.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Cesaro averaging and fixed cocycles.

  1. def OAI.HochschildCesaro.avg line 26
  2. lemma OAI.HochschildCesaro.iterate_norm_le line 29
  3. lemma OAI.HochschildCesaro.norm_avg_le line 35
  4. lemma OAI.HochschildCesaro.sum_defect line 50
  5. lemma OAI.HochschildCesaro.avg_defect line 61
  6. lemma OAI.HochschildCesaro.avg_defect_tendsto line 65
  7. lemma OAI.BoundedHochschild.residual_cesaro line 82
  8. lemma OAI.BoundedHochschild.averageLast_apply line 106
  9. lemma OAI.BoundedHochschild.predual_tendsto_average line 112
  10. lemma OAI.BoundedHochschild.predual_tendsto_residual line 133
  11. theorem OAI.BoundedHochschild.exists_average_fixed_cocycle line 149