OAI/Analysis/KadisonKastler/AbelianInvariantMean.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

A scalar invariant mean for every discrete abelian group

Finite iterated Cesaro averages give a positive, unital, contractive family of scalar functionals. An ultrafilter extending the directed finite-set/length filter gives a simultaneous scalar limit. The explicit telescoping bound proves invariance. This constructs the mean used for the real modular and character groups without an amenability premise.

  1. theorem OAI.KadisonKastler.cesaroTranslation_positive line 23
  2. theorem OAI.KadisonKastler.abelianBoxAverage_positive line 53
  3. def OAI.KadisonKastler.abelianBoxFunctional line 60
  4. theorem OAI.KadisonKastler.abelianBoxFunctional_apply line 64
  5. theorem OAI.KadisonKastler.abelianBoxFunctional_norm_le line 67
  6. theorem OAI.KadisonKastler.abelianBoxFunctional_const line 72
  7. theorem OAI.KadisonKastler.abelianBoxFunctional_positive line 77
  8. theorem OAI.KadisonKastler.abelianBoxFunctional_translation_bound line 82
  9. def OAI.KadisonKastler.abelianMeanFilter line 97
  10. theorem OAI.KadisonKastler.abelianMeanFilter_le line 102
  11. theorem OAI.KadisonKastler.exists_abelianMeanValue line 107
  12. def OAI.KadisonKastler.abelianMeanValue line 119
  13. theorem OAI.KadisonKastler.norm_abelianMeanValue line 122
  14. theorem OAI.KadisonKastler.tendsto_abelianMeanValue line 125
  15. theorem OAI.KadisonKastler.abelianMeanValue_add line 130
  16. theorem OAI.KadisonKastler.abelianMeanValue_smul line 135
  17. theorem OAI.KadisonKastler.abelianMeanValue_const line 140
  18. theorem OAI.KadisonKastler.abelianMeanValue_positive line 147
  19. theorem OAI.KadisonKastler.abelianBoxFunctional_translation_tendsto_zero line 161
  20. theorem OAI.KadisonKastler.abelianMeanValue_invariant line 177
  21. def OAI.KadisonKastler.abelianScalarInvariantMean line 186

    Source documentation

    An actual invariant scalar mean on every discrete abelian group.

    def abelianScalarInvariantMean (G : Type*) [CommGroup G]
    [TopologicalSpace G] [DiscreteTopology G] : ScalarInvariantMean G where
…

    Mentions: OAI.KadisonKastler.ScalarInvariantMean