OAI/GroupTheory/PolycyclicRecognition/Analysis/FiniteFolnerMean.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

From finite Følner witnesses to an invariant mean

  1. def OAI.PolycyclicRecognition.HasFiniteFolnerSets line 21

    Source documentation

    Finite Følner witnesses, in the symmetric-difference convention used by the actual finite-average translation estimate.

    def HasFiniteFolnerSets (G : Type*) [Group G] [DecidableEq G] : Prop :=
…
  2. theorem OAI.PolycyclicRecognition.invariantMean_of_finiteFolnerSets line 27

    Source documentation

    The directed family ranges over every finite set of translations and every positive reciprocal scale. No countability of the group is required.

    theorem invariantMean_of_finiteFolnerSets (h : HasFiniteFolnerSets G) :
    Nonempty (InvariantMean G) := by
…

    Mentions: OAI.PolycyclicRecognition.HasFiniteFolnerSets