OAI/Analysis/KadisonKastler/IncreasingFiniteMean.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Invariant means from increasing finite subgroups

Normalized counting averages have a simultaneous scalar ultralimit. Every fixed group translation preserves all sufficiently late averages.

  1. theorem OAI.KadisonKastler.finiteAverage_positive line 21
  2. def OAI.KadisonKastler.subgroupRestriction line 37
  3. def OAI.KadisonKastler.finiteSubgroupFunctional line 40
  4. theorem OAI.KadisonKastler.finiteSubgroupFunctional_apply line 44
  5. theorem OAI.KadisonKastler.finiteSubgroupFunctional_norm line 49
  6. theorem OAI.KadisonKastler.finiteSubgroupFunctional_const line 56
  7. theorem OAI.KadisonKastler.finiteSubgroupFunctional_positive line 62
  8. theorem OAI.KadisonKastler.finiteSubgroupFunctional_invariant line 68
  9. def OAI.KadisonKastler.finiteChainUltrafilter line 83
  10. theorem OAI.KadisonKastler.finiteChainUltrafilter_le line 85
  11. theorem OAI.KadisonKastler.exists_finiteChainMeanValue line 88
  12. def OAI.KadisonKastler.finiteChainMeanValue line 101
  13. theorem OAI.KadisonKastler.finiteChainMeanValue_norm line 104
  14. theorem OAI.KadisonKastler.finiteChainMeanValue_tendsto line 108
  15. theorem OAI.KadisonKastler.finiteChainMeanValue_add line 113
  16. theorem OAI.KadisonKastler.finiteChainMeanValue_smul line 119
  17. theorem OAI.KadisonKastler.finiteChainMeanValue_const line 124
  18. theorem OAI.KadisonKastler.finiteChainMeanValue_positive line 130
  19. theorem OAI.KadisonKastler.finiteChainMeanValue_invariant line 146
  20. def OAI.KadisonKastler.increasingFiniteScalarInvariantMean line 158

    Source documentation

    The scalar invariant mean for a group exhausted by an increasing sequence of finite subgroups.

    def increasingFiniteScalarInvariantMean [DiscreteTopology G] (hmono : Monotone K)
    (hcover : ∀ g : G, ∃ n, g ∈ K n) : ScalarInvariantMean G where
…

    Mentions: OAI.KadisonKastler.ScalarInvariantMean