Discrete invariant means

On a discrete group, means on TauCeti.UCB G correspond bijectively to positive real linear functionals on all bounded functions which take the value one at the constant one. The correspondence preserves left invariance. This gives a bounded-function characterization of amenability suitable for constructing finitely additive probabilities from indicator functions. Amenability with the discrete topology also implies amenability with any group topology.

A mean on a discrete group G also pushes forward along an arbitrary map r : G → H, by f ↦ m (f ∘ r) (TauCeti.Mean.mapOfDiscrete). When r (φ h * x) = h * r x for a homomorphism φ : H →* G, the pushforward of a left-invariant mean is left invariant.

The function-space identification is TauCeti.UCB.discreteAlgEquiv; the normalization and positivity use Mathlib's PositiveLinearMap, without an additional continuity assumption.

References

• A. Garrido, An introduction to amenable groups, Definitions 1.12–1.13 and Theorem 1.15 (for discrete groups).
• B. Bekka, P. de la Harpe, A. Valette, Kazhdan's Property (T), Appendix G.1.

noncomputable def TauCeti.Mean.boundedContinuousFunctionEquiv (G : Type u_1) [Group G] [TopologicalSpace G] [DiscreteTopology G] : Mean G ≃ { m : BoundedContinuousFunction G ℝ →ₚ[ℝ] ℝ // m 1 = 1 }

Means on a discrete group correspond to normalized positive linear functionals on all bounded functions.

@[simp]

theorem TauCeti.Mean.boundedContinuousFunctionEquiv_apply {G : Type u_1} [Group G] [TopologicalSpace G] [DiscreteTopology G] (m : Mean G) (f : BoundedContinuousFunction G ℝ) : ↑((boundedContinuousFunctionEquiv G) m) f = m ((UCB.discreteAlgEquiv G).symm f)

@[simp]

theorem TauCeti.Mean.boundedContinuousFunctionEquiv_symm_apply {G : Type u_1} [Group G] [TopologicalSpace G] [DiscreteTopology G] (m : { m : BoundedContinuousFunction G ℝ →ₚ[ℝ] ℝ // m 1 = 1 }) (f : UCB G) : ((boundedContinuousFunctionEquiv G).symm m) f = ↑m ↑f

theorem TauCeti.Mean.isLeftInvariant_iff_boundedContinuousFunction {G : Type u_1} [Group G] [TopologicalSpace G] [DiscreteTopology G] (m : Mean G) : m.IsLeftInvariant ↔ ∀ (g : G) (f : BoundedContinuousFunction G ℝ), ↑((boundedContinuousFunctionEquiv G) m) (f.compContinuous (ContinuousMap.mulLeft g⁻¹)) = ↑((boundedContinuousFunctionEquiv G) m) f

The correspondence of means preserves and reflects left invariance.

noncomputable def TauCeti.Mean.mapOfDiscrete {G : Type u_1} [Group G] [TopologicalSpace G] [DiscreteTopology G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (r : G → H) (m : Mean G) : Mean H

The pushforward f ↦ m (f ∘ r) of a mean m on a discrete group G along an arbitrary map r : G → H into a topological group, as a mean on UCB H.

@[simp]

theorem TauCeti.Mean.mapOfDiscrete_apply {G : Type u_1} [Group G] [TopologicalSpace G] [DiscreteTopology G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (r : G → H) (m : Mean G) (f : UCB H) : (mapOfDiscrete r m) f = m ((UCB.compRightAlgHomOfDiscrete r) f)

theorem TauCeti.Mean.mapOfDiscrete_coe {G : Type u_1} [Group G] [TopologicalSpace G] [DiscreteTopology G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : G →ₜ* H) (m : Mean G) : mapOfDiscrete (⇑φ) m = map φ m

Along a continuous homomorphism, the pushforward out of a discrete group is the pushforward TauCeti.Mean.map.

theorem TauCeti.Mean.IsLeftInvariant.mapOfDiscrete {G : Type u_1} [Group G] [TopologicalSpace G] [DiscreteTopology G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {m : Mean G} (hm : m.IsLeftInvariant) (φ : H →* G) {r : G → H} (hr : ∀ (h : H) (x : G), r (φ h * x) = h * r x) : (Mean.mapOfDiscrete r m).IsLeftInvariant

If r (φ h * x) = h * r x for a homomorphism φ : H →* G, then the pushforward of a left-invariant mean along r is left invariant.

theorem TauCeti.amenable_iff_exists_boundedContinuousFunction_mean (G : Type u_1) [Group G] [TopologicalSpace G] [DiscreteTopology G] : Amenable G ↔ ∃ (m : BoundedContinuousFunction G ℝ →ₚ[ℝ] ℝ), m 1 = 1 ∧ ∀ (g : G) (f : BoundedContinuousFunction G ℝ), m (f.compContinuous (ContinuousMap.mulLeft g⁻¹)) = m f

A discrete group is amenable exactly when all bounded functions admit a normalized positive left-invariant real linear functional.

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

An abstract group which is amenable with the discrete topology is amenable with any group topology.