OAI/GroupTheory/PolycyclicRecognition/Analysis/PolycyclicInvariantMean.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Concrete invariant means for virtually polycyclic groups

The finite cyclic subnormal series gives the mean by successive kernel and quotient averages. Thus amenability in the model reduction is proved from polycyclicity, rather than retained as an extra premise.

  1. theorem OAI.PolycyclicRecognition.invariantMean_of_cyclicStep line 24
  2. theorem OAI.PolycyclicRecognition.invariantMean_of_cyclicSeries line 32
  3. theorem OAI.PolycyclicRecognition.invariantMean_of_isPolycyclic line 45
  4. theorem OAI.PolycyclicRecognition.invariantMean_of_isVirtuallyPolycyclic line 52
  5. theorem OAI.PolycyclicRecognition.finiteFolnerSets_of_invariantMean line 60

    Source documentation

    The existing finite coarea argument converts the constructed mean to the finite Følner sets used in the metric comparison.

    theorem finiteFolnerSets_of_invariantMean [DecidableEq G] (M : InvariantMean G) :
    HasFiniteFolnerSets G := by
…

    Mentions: OAI.PolycyclicRecognition.HasFiniteFolnerSets

  6. theorem OAI.PolycyclicRecognition.finiteFolnerSets_of_isVirtuallyPolycyclic line 68