Følner sequences and amenability

[YaelDillies]

Følner sequences are an important tool to study amenability of group actions and almost periodic functions, and can be thought of as a generalisation of the sequence n ↦ B(n 0) of balls centered around the origin.

The main result about Følner sequences is that an action is amenable iff it admits a Følner sequence(/filter). Here is the forward direction of this claim as a Lean statement. The proof can be found on the Wikipedia page: https://en.wikipedia.org/wiki/F%C3%B8lner_sequence.

import Mathlib.MeasureTheory.Group.Defs
import Mathlib.MeasureTheory.Measure.Typeclasses.Finite

open MeasureTheory
open scoped ENNReal Pointwise symmDiff Topology

variable {G ι X : Type*} [MeasurableSpace X] [Group G] [MulAction G X] {l : Filter ι}
  {F : ι → Set X} {μ : Measure X}

variable (G) in
/-- A Følner sequence with respect to some group `G` acting on a measure space `X`
is a sequence of sets `F` such that:
1. Each `F i` has finite non-zero measure,
2. For all `g : G`, `μ (g • F i ∆ F i) / μ (F i)` tends to `0`. -/
structure IsFoelner (l : Filter ι) (F : ι → Set X) (μ : Measure X := by volume_tac) : Prop where
  /-- Each `F i` has non-zero measure -/
  meas_ne_zero i : μ (F i) ≠ 0
  /-- Each `F i` has finite measure. -/
  meas_ne_top i : μ (F i) ≠ ∞
  /-- For all `g : G`, `μ (g • F i ∆ F i) / μ (F i)` tends to `0`. -/
  tendsto_meas_symmDiff (g : G) : l.Tendsto (fun i ↦ μ (g • F i ∆ F i) / μ (F i)) (𝓝 0)

/-- The constant sequence `X` is Følner if `X` has finite measure. -/
lemma IsFoelner.of_isFiniteMeasure [NeZero μ] [IsFiniteMeasure μ] :
    IsFoelner G l (fun _ ↦ .univ) μ where
  meas_ne_zero := by simp [NeZero.ne]
  meas_ne_top := by simp
  tendsto_meas_symmDiff := by simp [tendsto_const_nhds]

/-- If an action of a group on a measure space admits a non-trivial Følner sequence,
then the action is amenable. -/
lemma IsFoelner.amenable [SMulInvariantMeasure G X μ] [l.NeBot] (h : IsFoelner G l F μ) :
    ∃ m : Set X → ℝ≥0∞,
      m .univ = 1 ∧
      (∀ s t, Disjoint s t → m (s ∪ t) = m s + m t) ∧
      ∀ (g : G) s, μ (g • s) = μ s := sorry

[ADedecker]

I'd like to add that there is a maximal Følner filter, let's call it Filter.foelner G X, namely the filter on sets of finite non-zero measure obtained by pulling back 𝓝 0 under the map fun S g ↦ μ (g • S ∆ S) / μ (S). Then IsFoelner l F is the same as Tendsto F l (Filter.foelner G X), and a locally compact group is amenable iff (Filter.foelner G G).NeBot.

[ster99]

@YaelDillies I would like to work on this one, if that’s okay with you!

[YaelDillies]

Sure, it's yours!