OAI/Analysis/KadisonKastler/AbelianCesaro.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Finite Cesaro averages in an abelian group

Iterating the one-generator averages over a finite list gives positive contractions. A translation by any generator in the list changes the average by at most twice the reciprocal averaging length.

  1. def OAI.KadisonKastler.scalarTranslation line 21
  2. theorem OAI.KadisonKastler.scalarTranslation_apply line 31
  3. theorem OAI.KadisonKastler.scalarTranslation_norm_le line 34
  4. theorem OAI.KadisonKastler.scalarTranslation_one line 39
  5. theorem OAI.KadisonKastler.scalarTranslation_mul line 43
  6. theorem OAI.KadisonKastler.scalarTranslation_comm line 48
  7. theorem OAI.KadisonKastler.scalarTranslation_const line 52
  8. def OAI.KadisonKastler.cesaroTranslation line 56
  9. theorem OAI.KadisonKastler.cesaroTranslation_apply line 60
  10. theorem OAI.KadisonKastler.cesaroTranslation_norm_le line 65
  11. theorem OAI.KadisonKastler.cesaroTranslation_const line 79
  12. theorem OAI.KadisonKastler.scalarTranslation_cesaro line 89
  13. theorem OAI.KadisonKastler.cesaroTranslation_difference line 98
  14. theorem OAI.KadisonKastler.norm_inv_nat_smul_sub_le line 116
  15. theorem OAI.KadisonKastler.cesaroTranslation_difference_norm_le line 130
  16. def OAI.KadisonKastler.abelianBoxAverage line 137
  17. theorem OAI.KadisonKastler.abelianBoxAverage_nil line 141
  18. theorem OAI.KadisonKastler.abelianBoxAverage_cons line 144
  19. theorem OAI.KadisonKastler.abelianBoxAverage_norm_le line 147
  20. theorem OAI.KadisonKastler.abelianBoxAverage_const line 153
  21. theorem OAI.KadisonKastler.scalarTranslation_box line 160
  22. theorem OAI.KadisonKastler.abelianBoxAverage_difference_norm_le line 168