The weak-* compact space of means

Every mean m on TauCeti.UCB G is a continuous linear functional of norm one, so the means sit inside the closed unit ball of the dual of UCB G. Positivity and normalization are conditions on finitely many values at a time, hence closed for the weak-* topology, and by the Banach–Alaoglu theorem the means form a weak-* compact set. We give TauCeti.Mean G the weak-* topology, induced from WeakDual ℝ (UCB G), so that it becomes a compact Hausdorff space in which a net of means converges exactly when it converges at every function.

Each invariance equation m (L_g f) = m f also defines a closed set of means, so the left-invariant means form a compact set. Compactness yields the two standard criteria for amenability:

• a finite-intersection criterion: G is amenable as soon as every finite family of invariance equations is satisfied by some mean;
• a cluster-point criterion: if means m_i are approximately left invariant along a nontrivial filter, in the sense that m_i (L_g f) - m_i f → 0 for all g and f, then every weak-* cluster point of m_i is a left-invariant mean, and such a cluster point exists.

These criteria are how amenability is proved for directed unions of subgroups and for groups with Følner sets.

Main definitions

• TauCeti.Mean.toWeakDual: a mean as an element of the weak-* dual of UCB G.
• TauCeti.Mean.instTopologicalSpace: the weak-* topology on means.

Main results

• TauCeti.Mean.mem_range_toWeakDual_iff: the weak-* functionals coming from means are the positive ones taking the value 1 at 1.
• TauCeti.Mean.isCompact_range_toWeakDual: the means form a weak-* compact subset of the dual unit ball; hence Mean G is a compact Hausdorff space.
• TauCeti.Mean.tendsto_iff_forall_apply_tendsto: weak-* convergence of means is convergence at every function.
• TauCeti.Mean.isCompact_setOf_isLeftInvariant: the left-invariant means form a compact set.
• TauCeti.amenable_iff_forall_finset_exists: the finite-intersection criterion for amenability.
• TauCeti.Mean.IsLeftInvariant.of_mapClusterPt, TauCeti.Amenable.of_tendsto: the cluster-point criterion for amenability.

References

• B. Bekka, P. de la Harpe, A. Valette, Kazhdan's Property (T), Appendix G.1 and the proof of Proposition G.2.2.

Means in the weak-* dual

noncomputable def TauCeti.Mean.toWeakDual {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (m : Mean G) : WeakDual ℝ (UCB G)

A mean on UCB G, as an element of the weak-* dual of UCB G.

@[simp]

theorem TauCeti.Mean.toWeakDual_apply {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (m : Mean G) (f : UCB G) : m.toWeakDual f = m f

@[simp]

theorem TauCeti.Mean.toStrongDual_toWeakDual {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (m : Mean G) : WeakDual.toStrongDual m.toWeakDual = m.toContinuousLinearMap

theorem TauCeti.Mean.toWeakDual_injective {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Function.Injective toWeakDual

theorem TauCeti.Mean.mem_range_toWeakDual_iff {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {φ : WeakDual ℝ (UCB G)} : φ ∈ Set.range toWeakDual ↔ (∀ (f : UCB G), 0 ≤ f → 0 ≤ φ f) ∧ φ 1 = 1

An element of the weak-* dual of UCB G comes from a mean exactly when it is nonnegative on nonnegative functions and takes the value 1 at 1.

theorem TauCeti.Mean.range_toWeakDual_subset_closedBall {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Set.range toWeakDual ⊆ ⇑WeakDual.toStrongDual ⁻¹' Metric.closedBall 0 1

The means lie in the closed unit ball of the dual of UCB G.

theorem TauCeti.Mean.isClosed_range_toWeakDual {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : IsClosed (Set.range toWeakDual)

The means form a weak-* closed set: positivity and normalization are closed conditions.

theorem TauCeti.Mean.isCompact_range_toWeakDual {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : IsCompact (Set.range toWeakDual)

The means form a weak-* compact set, by the Banach–Alaoglu theorem.

The weak-* topology on means

@[instance_reducible]

noncomputable instance TauCeti.Mean.instTopologicalSpace {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : TopologicalSpace (Mean G)

The weak-* topology on means, induced from the weak-* dual of UCB G. A net of means converges exactly when it converges at every function, see tendsto_iff_forall_apply_tendsto.

theorem TauCeti.Mean.isEmbedding_toWeakDual {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Topology.IsEmbedding toWeakDual

theorem TauCeti.Mean.continuous_toWeakDual {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Continuous toWeakDual

instance TauCeti.Mean.instContinuousEvalConstUCBReal {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : ContinuousEvalConst (Mean G) (UCB G) ℝ

Evaluation of means at a fixed function is weak-* continuous.

instance TauCeti.Mean.instT2Space {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : T2Space (Mean G)

instance TauCeti.Mean.instCompactSpace {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : CompactSpace (Mean G)

The space of means is weak-* compact.

theorem TauCeti.Mean.tendsto_iff_forall_apply_tendsto {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {ι : Type u_2} {l : Filter ι} {ms : ι → Mean G} {m : Mean G} : Filter.Tendsto ms l (nhds m) ↔ ∀ (f : UCB G), Filter.Tendsto (fun (i : ι) => (ms i) f) l (nhds (m f))

A family of means converges weak-* exactly when it converges at every function.

Invariant means

theorem TauCeti.Mean.isClosed_setOf_apply_leftTranslation_eq {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g : G) (f : UCB G) : IsClosed {m : Mean G | m ((UCB.leftTranslation g) f) = m f}

Each invariance equation m (L_g f) = m f defines a weak-* closed set of means.

theorem TauCeti.Mean.isClosed_setOf_isLeftInvariant {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : IsClosed {m : Mean G | m.IsLeftInvariant}

The left-invariant means form a weak-* closed set.

theorem TauCeti.Mean.isCompact_setOf_isLeftInvariant {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : IsCompact {m : Mean G | m.IsLeftInvariant}

The left-invariant means form a weak-* compact set.

theorem TauCeti.Mean.IsLeftInvariant.of_mapClusterPt {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {ι : Type u_2} {l : Filter ι} {ms : ι → Mean G} {m : Mean G} (hm : MapClusterPt m l ms) (h : ∀ (g : G) (f : UCB G), Filter.Tendsto (fun (i : ι) => (ms i) ((UCB.leftTranslation g) f) - (ms i) f) l (nhds 0)) : m.IsLeftInvariant

A weak-* cluster point of means ms i which are approximately left invariant along l, in the sense that ms i (L_g f) - ms i f → 0 for every g and f, is a left-invariant mean.

theorem TauCeti.Mean.exists_mapClusterPt_isLeftInvariant {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {ι : Type u_2} {l : Filter ι} [l.NeBot] {ms : ι → Mean G} (h : ∀ (g : G) (f : UCB G), Filter.Tendsto (fun (i : ι) => (ms i) ((UCB.leftTranslation g) f) - (ms i) f) l (nhds 0)) : ∃ (m : Mean G), MapClusterPt m l ms ∧ m.IsLeftInvariant

Means which are approximately left invariant along a nontrivial filter have a weak-* cluster point, and every such cluster point is a left-invariant mean.

theorem TauCeti.Amenable.of_tendsto {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {ι : Type u_2} {l : Filter ι} [l.NeBot] {ms : ι → Mean G} (h : ∀ (g : G) (f : UCB G), Filter.Tendsto (fun (i : ι) => (ms i) ((UCB.leftTranslation g) f) - (ms i) f) l (nhds 0)) : Amenable G

Cluster-point criterion: a topological group is amenable when it carries means ms i which are approximately left invariant along a nontrivial filter, that is, ms i (L_g f) - ms i f → 0 for every g and f.

theorem TauCeti.amenable_iff_forall_finset_exists {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Amenable G ↔ ∀ (s : Finset (G × UCB G)), ∃ (m : Mean G), ∀ p ∈ s, m ((UCB.leftTranslation p.1) p.2) = m p.2

Finite-intersection criterion: a topological group is amenable exactly when every finite family of invariance equations m (L_g f) = m f is satisfied by some mean.