Averages over finite sets and amenability from Følner sets

For a finite nonempty subset F of a topological group G, averaging over F,

m_F f = 𝔼 x ∈ F, f x = |F|⁻¹ ∑_{x ∈ F} f x,

is a mean on TauCeti.UCB G (TauCeti.Mean.average). Left translation moves the set being averaged over: m_F (L_g f) = m_{g⁻¹F} f. Since g⁻¹F and F have the same cardinality, the two sums differ only on g⁻¹F △ F, which gives the estimate

|m_F (L_g f) - m_F f| ≤ ‖f‖ · |g⁻¹F △ F| / |F|.

Hence, along a Følner family of finite nonempty sets, the averages are approximately left invariant means, and the cluster-point criterion TauCeti.Amenable.of_tendsto produces a left-invariant mean. In particular a group with Følner sets is amenable for every group topology: the averages only evaluate functions at finitely many points, so no compatibility between the topology and the Følner sets is needed.

On a discrete group, a mean is determined by its finitely additive probability on all subsets. Along an ultrafilter u, the averages over a counting-measure Følner family F of finite nonempty sets converge weak-* to the mean TauCeti.Mean.ofIsFoelner whose probability is the density-limit content s ↦ lim_u |s ∩ F i| / |F i| (IsFoelner.addContent). That content is left invariant, so this limit is a left-invariant mean, described explicitly by limits of densities rather than as an unspecified weak-* cluster point.

Main definitions

• TauCeti.Mean.ofIsFoelner: the mean on a discrete group whose finitely additive probability is the density-limit content of a counting-measure Følner family along an ultrafilter.

Main results

• TauCeti.Mean.average_leftTranslation: m_F (L_g f) = m_{g⁻¹F} f.
• TauCeti.Mean.abs_average_leftTranslation_sub_le: the estimate |m_F (L_g f) - m_F f| ≤ ‖f‖ · |g⁻¹F △ F| / |F|.
• TauCeti.Amenable.of_tendsto_card_smul_symmDiff_div_card: a topological group with finite nonempty sets F i such that |g F i △ F i| / |F i| → 0 for every g, along a nontrivial filter, is amenable.
• TauCeti.Amenable.of_isFoelner: the same for a counting-measure Følner family.
• TauCeti.Amenable.of_hasFoelnerSets: a group with Følner sets is amenable for every group topology.
• TauCeti.Mean.isLeftInvariant_ofIsFoelner: the density-limit mean is left invariant.
• TauCeti.Mean.tendsto_average_ofIsFoelner: along an ultrafilter, the averages over a Følner family converge weak-* to its density-limit mean.

References

• A. Garrido, An introduction to amenable groups, Theorem 3.6.
• B. Bekka, P. de la Harpe, A. Valette, Kazhdan's Property (T), Theorem G.5.1.

theorem TauCeti.Mean.average_leftTranslation {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F : Finset G} (hF : F.Nonempty) [DecidableEq G] (g : G) (f : UCB G) : (average F hF) ((UCB.leftTranslation g) f) = (average (g⁻¹ • F) ⋯) f

Averaging a left translate L_g f over F is averaging f over g⁻¹F.

theorem TauCeti.Mean.abs_average_leftTranslation_sub_le {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F : Finset G} (hF : F.Nonempty) [DecidableEq G] (g : G) (f : UCB G) : |(average F hF) ((UCB.leftTranslation g) f) - (average F hF) f| ≤ ‖f‖ * ↑(symmDiff (g⁻¹ • F) F).card / ↑F.card

The averages of a left translate L_g f and of f over F differ by at most ‖f‖ · |g⁻¹F △ F| / |F|.

Limits of averages along an ultrafilter

noncomputable def TauCeti.Mean.ofIsFoelner {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] [MeasurableSpace G] [DiscreteMeasurableSpace G] {ι : Type u_2} {u : Ultrafilter ι} {F : ι → Set G} (hF : IsFoelner G MeasureTheory.Measure.count (↑u) F) : Mean G

The mean on a discrete group whose finitely additive probability is the density-limit content s ↦ lim_u |s ∩ F i| / |F i| of a counting-measure Følner family F along an ultrafilter u.

@[simp]

theorem TauCeti.Mean.toContent_ofIsFoelner {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] [MeasurableSpace G] [DiscreteMeasurableSpace G] {ι : Type u_2} {u : Ultrafilter ι} {F : ι → Set G} (hF : IsFoelner G MeasureTheory.Measure.count (↑u) F) : (ofIsFoelner hF).toContent = hF.addContent

theorem TauCeti.Mean.isLeftInvariant_ofIsFoelner {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] [MeasurableSpace G] [DiscreteMeasurableSpace G] {ι : Type u_2} {u : Ultrafilter ι} {F : ι → Set G} (hF : IsFoelner G MeasureTheory.Measure.count (↑u) F) : (ofIsFoelner hF).IsLeftInvariant

The mean of the density-limit content of a Følner family is left invariant.

theorem TauCeti.Mean.tendsto_average_ofIsFoelner {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] [MeasurableSpace G] [DiscreteMeasurableSpace G] {ι : Type u_2} {u : Ultrafilter ι} {F : ι → Finset G} (hne : ∀ (i : ι), (F i).Nonempty) (hF : IsFoelner G MeasureTheory.Measure.count ↑u fun (i : ι) => ↑(F i)) : Filter.Tendsto (fun (i : ι) => average (F i) ⋯) (↑u) (nhds (ofIsFoelner hF))

Averages over Følner sets converge to the density-limit mean. Along an ultrafilter u, the averages over a counting-measure Følner family of finite nonempty sets converge weak-* to the mean whose finitely additive probability is the density-limit content of the family along u.

theorem TauCeti.Amenable.of_tendsto_card_smul_symmDiff_div_card {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DecidableEq G] {ι : Type u_2} {l : Filter ι} [l.NeBot] {F : ι → Finset G} (hne : ∀ (i : ι), (F i).Nonempty) (h : ∀ (g : G), Filter.Tendsto (fun (i : ι) => ↑(symmDiff (g • F i) (F i)).card / ↑(F i).card) l (nhds 0)) : Amenable G

A topological group is amenable when it has finite nonempty sets F i with |g F i △ F i| / |F i| → 0 for every g, along a nontrivial filter. The averages over F i are then approximately left-invariant means.

theorem TauCeti.Amenable.of_isFoelner {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [MeasurableSpace G] [MeasurableSingletonClass G] {ι : Type u_2} {l : Filter ι} [l.NeBot] {F : ι → Set G} (hF : IsFoelner G MeasureTheory.Measure.count l F) : Amenable G

A topological group is amenable when it has a Følner family for counting measure, along a nontrivial filter.

theorem TauCeti.Amenable.of_hasFoelnerSets {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (h : HasFoelnerSets G) : Amenable G

A group with Følner sets is amenable, for every group topology.