Means and finitely additive probabilities on discrete groups

A mean on a discrete group gives a finitely additive probability on all subsets by evaluating characteristic functions. TauCeti.Mean.toContent bundles this probability as an AddContent, not as a countably additive measure. Its values are finite, and their real parts recover the mean on characteristic functions. More generally, the mean of a finite linear combination of characteristic functions is the corresponding linear combination of content values.

Every finitely additive probability on all subsets arises from exactly one mean (TauCeti.Mean.contentEquiv), by integrating bounded functions against it. The construction commutes with pushforward along arbitrary maps between discrete groups, and a mean is left invariant exactly when its probability is. Hence a discrete group is amenable exactly when it admits a left-invariant finitely additive probability on all subsets (TauCeti.amenable_iff_exists_invariantContent).

Point evaluation gives the Dirac probability (TauCeti.Mean.toContent_eval). On a finite group the uniform mean gives normalized counting, ν s = |s| / |G| (TauCeti.Mean.toContent_uniform), stated with Nat.card so that no Fintype instance is involved. This is the only left-invariant finitely additive probability on all subsets of a finite group (MeasureTheory.addContent_eq_natCard_div_natCard). On a group with one element the uniform mean is point evaluation, and its content is the Dirac probability.

References

• A. Garrido, An introduction to amenable groups, Theorem 1.15, in discrete scope.

noncomputable def TauCeti.Mean.toContent {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] (m : Mean G) : MeasureTheory.AddContent ENNReal Set.univ

The finitely additive probability on all subsets associated to a discrete mean.

theorem TauCeti.Mean.toContent_apply {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] (m : Mean G) (s : Set G) : m.toContent s = ENNReal.ofReal (m ((UCB.discreteAlgEquiv G).symm (BoundedContinuousFunction.indicator s ⋯)))

A content value is the mean of the characteristic function, converted to ℝ≥0∞.

@[simp]

theorem TauCeti.Mean.toContent_univ {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] (m : Mean G) : m.toContent Set.univ = 1

The content associated to a mean has total mass one.

theorem TauCeti.Mean.toContent_le_one {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] (m : Mean G) (s : Set G) : m.toContent s ≤ 1

Every value of the content associated to a mean is at most one.

theorem TauCeti.Mean.toContent_ne_top {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] (m : Mean G) (s : Set G) : m.toContent s ≠ ⊤

The content associated to a mean is finite on every subset.

@[simp]

theorem TauCeti.Mean.toReal_toContent {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] (m : Mean G) (s : Set G) : (m.toContent s).toReal = m ((UCB.discreteAlgEquiv G).symm (BoundedContinuousFunction.indicator s ⋯))

Taking real values recovers the mean on characteristic functions.

theorem TauCeti.Mean.toContent_toReal {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] (m : Mean G) : m.toContent.toReal ⋯ = (↑((boundedContinuousFunctionEquiv G) m)).toAddContent

The original real content is recovered by taking real values of toContent.

theorem TauCeti.Mean.apply_sum_smul_indicator {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] (m : Mean G) {ι : Type u_3} (I : Finset ι) (c : ι → ℝ) (A : ι → Set G) : m ((UCB.discreteAlgEquiv G).symm (∑ i ∈ I, c i • BoundedContinuousFunction.indicator (A i) ⋯)) = ∑ i ∈ I, c i * (m.toContent (A i)).toReal

A mean evaluates finite linear combinations of characteristic functions by its content. The sets need not be disjoint.

theorem TauCeti.Mean.toContent_mapOfDiscrete {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [DiscreteTopology H] (m : Mean G) (r : G → H) : (mapOfDiscrete r m).toContent = m.toContent.map r ⋯

Contents commute with pushforward along arbitrary maps between discrete groups.

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

In particular, contents commute with pushforward by continuous homomorphisms.

theorem TauCeti.Mean.IsLeftInvariant.toContent_smul {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] {m : Mean G} (hm : m.IsLeftInvariant) (g : G) (s : Set G) : m.toContent (g • s) = m.toContent s

A left-invariant mean assigns equal content to a set and each of its left translates.

@[simp]

theorem TauCeti.Mean.toContent_eval {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] (x : G) (s : Set G) : (eval G x).toContent s = s.indicator 1 x

The content of evaluation at x is the Dirac probability at x.

@[simp]

theorem TauCeti.Mean.toContent_uniform {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] [Finite G] (s : Set G) : (uniform G).toContent s = ↑(Nat.card ↑s) / ↑(Nat.card G)

On a finite group, the content of the uniform mean is normalized counting, ν s = |s| / |G|.

noncomputable def TauCeti.Mean.contentEquiv (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] : Mean G ≃ { ν : MeasureTheory.AddContent ENNReal Set.univ // ν Set.univ = 1 }

Means on a discrete group correspond to finitely additive probabilities on all subsets, by evaluating at characteristic functions. The inverse integrates a bounded function against the probability.

@[simp]

theorem TauCeti.Mean.coe_contentEquiv_apply {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] (m : Mean G) : ↑((contentEquiv G) m) = m.toContent

@[simp]

theorem TauCeti.Mean.toContent_contentEquiv_symm {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] (ν : { ν : MeasureTheory.AddContent ENNReal Set.univ // ν Set.univ = 1 }) : ((contentEquiv G).symm ν).toContent = ↑ν

The mean associated to a finitely additive probability has that probability as its content.

theorem TauCeti.Mean.toContent_injective {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] : Function.Injective toContent

A mean on a discrete group is determined by its content.

theorem TauCeti.Mean.isLeftInvariant_iff_toContent_smul {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] (m : Mean G) : m.IsLeftInvariant ↔ ∀ (g : G) (s : Set G), m.toContent (g • s) = m.toContent s

A mean on a discrete group is left invariant exactly when its content is invariant under left translation of sets.

theorem TauCeti.Amenable.exists_invariantContent {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] [Amenable G] : ∃ (ν : MeasureTheory.AddContent ENNReal Set.univ), ν Set.univ = 1 ∧ ∀ (g : G) (s : Set G), ν (g • s) = ν s

An amenable discrete group admits an invariant finitely additive probability on all subsets.

theorem TauCeti.amenable_iff_exists_invariantContent (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] : Amenable G ↔ ∃ (ν : MeasureTheory.AddContent ENNReal Set.univ), ν Set.univ = 1 ∧ ∀ (g : G) (s : Set G), ν (g • s) = ν s

Discrete amenability by finitely additive probabilities. A discrete group is amenable exactly when it admits a left-invariant finitely additive probability on all subsets.