Finite averages; finite groups are amenable

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. On a finite group, the average over the whole group,

m f = 𝔼 x, f x = (∑ x, f x) / |G|,

is the uniform mean. It is left invariant because x ↦ g⁻¹ * x permutes G, so every finite topological group is amenable, whatever its topology.

Conversely, the uniform mean is the only left-invariant mean on a finite group: the sum ∑ g, L_g f of the left translates of f is the constant function ∑ x, f x (TauCeti.UCB.sum_leftTranslation), so a left-invariant mean m satisfies |G| * m f = ∑ x, f x. In particular, on a group with one element the uniform mean is evaluation at that element.

Main definitions

• TauCeti.Mean.average F hF: the average over a finite nonempty set F, as a mean.
• TauCeti.Mean.uniform G: the normalized counting mean f ↦ 𝔼 x, f x on a finite group.

Main results

• TauCeti.Mean.average_singleton: the average over a singleton is point evaluation.
• TauCeti.Mean.average_univ: the average over the whole of a finite group is the uniform mean.
• TauCeti.Mean.uniform_apply, TauCeti.Mean.uniform_apply_eq_sum_div_card: the value of the uniform mean, for any choice of Fintype instance.
• TauCeti.Mean.isLeftInvariant_uniform: the uniform mean is left invariant.
• TauCeti.Mean.isLeftInvariant_iff_eq_uniform: it is the unique left-invariant mean.
• TauCeti.Amenable.of_finite: finite topological groups are amenable.

References

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

noncomputable def TauCeti.Mean.average {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (F : Finset G) (hF : F.Nonempty) : Mean G

The average f ↦ 𝔼 x ∈ F, f x over a finite nonempty set F ⊆ G, as a mean on UCB G.

@[simp]

theorem TauCeti.Mean.average_apply {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F : Finset G} (hF : F.Nonempty) (f : UCB G) : (average F hF) f = F.expect fun (x : G) => ↑f x

theorem TauCeti.Mean.average_apply_eq_sum_div_card {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F : Finset G} (hF : F.Nonempty) (f : UCB G) : (average F hF) f = (∑ x ∈ F, ↑f x) / ↑F.card

The average over F is the sum over F divided by the cardinality of F.

@[simp]

theorem TauCeti.Mean.average_singleton {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (x : G) : average {x} ⋯ = eval G x

The average over a singleton {x} is evaluation at x.

noncomputable def TauCeti.Mean.uniform (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Finite G] : Mean G

The normalized counting mean f ↦ 𝔼 x, f x on a finite topological group G.

@[simp]

theorem TauCeti.Mean.uniform_apply {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Finite G] [Fintype G] (f : UCB G) : (uniform G) f = Finset.univ.expect fun (x : G) => ↑f x

The uniform mean is the average over the group. The Fintype instance is arbitrary.

@[simp]

theorem TauCeti.Mean.average_univ {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Finite G] [Fintype G] : average Finset.univ ⋯ = uniform G

On a finite group, the average over the whole group is the uniform mean.

theorem TauCeti.Mean.uniform_apply_eq_sum_div_card {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Finite G] [Fintype G] (f : UCB G) : (uniform G) f = (∑ x : G, ↑f x) / ↑(Fintype.card G)

The uniform mean is the sum over the group divided by its cardinality. The Fintype instance is arbitrary.

theorem TauCeti.Mean.isLeftInvariant_uniform {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Finite G] : (uniform G).IsLeftInvariant

The uniform mean is left invariant, since left multiplication permutes the group.

theorem TauCeti.Mean.IsLeftInvariant.eq_uniform {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Finite G] {m : Mean G} (hm : m.IsLeftInvariant) : m = uniform G

A left-invariant mean on a finite group is the uniform mean.

theorem TauCeti.Mean.isLeftInvariant_iff_eq_uniform {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Finite G] {m : Mean G} : m.IsLeftInvariant ↔ m = uniform G

On a finite group, the uniform mean is the unique left-invariant mean.

theorem TauCeti.Mean.uniform_eq_eval {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Subsingleton G] (x : G) : uniform G = eval G x

On a group with one element, the uniform mean is evaluation at that element.

@[instance 100]

instance TauCeti.Amenable.of_finite {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Finite G] : Amenable G

A finite topological group is amenable, for any group topology.