OAI/GroupTheory/PolycyclicRecognition/Analysis/RightFolnerExpansion.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Right finite expansions and metric Følner sets in the source group

Left-invariant metrics use right expansions of finite sets. Inversion converts the left Følner sets supplied by an invariant mean into these sets.

  1. def OAI.PolycyclicRecognition.rightFiniteExpansion line 21
  2. theorem OAI.PolycyclicRecognition.exists_small_rightExpansion line 24
  3. def OAI.PolycyclicRecognition.finiteMetricNeighborhood line 73

    Source documentation

    A source metric neighborhood is a right expansion by the finite identity ball. This is the exact finite set used in the boundary estimate.

    def finiteMetricNeighborhood (hfinite : ∀ R : ℝ, (Metric.closedBall (1 : G) R).Finite)
    (E : Finset G) (R : ℝ) : Finset G :=
…
  4. theorem OAI.PolycyclicRecognition.mem_finiteMetricNeighborhood line 77
  5. theorem OAI.PolycyclicRecognition.exists_small_metricNeighborhood line 100