The density-limit content of a Følner family

Let a group G act on a measure space X in which every subset is measurable, and let F : ι → Set X be a Følner family along an ultrafilter u. Mathlib's IsFoelner.mean μ u F s is the limit along u of the densities μ (s ∩ F i) / μ (F i). It is the finitely additive probability behind IsFoelner.amenable, which only records its properties in an existential statement. This file bundles it as a content on all subsets of X (IsFoelner.addContent), so that it can be compared with other finitely additive probabilities, such as the content of a mean on a discrete group. The content has total mass one and is invariant under G when μ is.

Main definitions

• IsFoelner.addContent: the density-limit content s ↦ lim_u μ (s ∩ F i) / μ (F i) of a Følner family along an ultrafilter.

Main results

• IsFoelner.tendsto_addContent: the densities of s tend to the content of s along u.
• IsFoelner.addContent_univ: the content has total mass one.
• IsFoelner.addContent_smul: the content is invariant under the action of G.

References

• A. Garrido, An introduction to amenable groups, Definition 3.1 and Theorem 3.6.

noncomputable def IsFoelner.addContent {G : Type u_1} {X : Type u_2} {ι : Type u_3} [Group G] [MulAction G X] [MeasurableSpace X] [DiscreteMeasurableSpace X] {μ : MeasureTheory.Measure X} {u : Ultrafilter ι} {F : ι → Set X} (hF : IsFoelner G μ (↑u) F) : MeasureTheory.AddContent ENNReal Set.univ

The density-limit content of a Følner family F along an ultrafilter u: the content of s is the limit along u of the densities μ (s ∩ F i) / μ (F i). Every subset of X is measurable, so this is a finitely additive set function on all subsets.

theorem IsFoelner.addContent_apply {G : Type u_1} {X : Type u_2} {ι : Type u_3} [Group G] [MulAction G X] [MeasurableSpace X] [DiscreteMeasurableSpace X] {μ : MeasureTheory.Measure X} {u : Ultrafilter ι} {F : ι → Set X} (hF : IsFoelner G μ (↑u) F) (s : Set X) : hF.addContent s = mean μ u F s

theorem IsFoelner.tendsto_addContent {G : Type u_1} {X : Type u_2} {ι : Type u_3} [Group G] [MulAction G X] [MeasurableSpace X] [DiscreteMeasurableSpace X] {μ : MeasureTheory.Measure X} {u : Ultrafilter ι} {F : ι → Set X} (hF : IsFoelner G μ (↑u) F) (s : Set X) : Filter.Tendsto (fun (i : ι) => μ (s ∩ F i) / μ (F i)) (↑u) (nhds (hF.addContent s))

The densities μ (s ∩ F i) / μ (F i) tend to the content of s along the ultrafilter.

@[simp]

theorem IsFoelner.addContent_univ {G : Type u_1} {X : Type u_2} {ι : Type u_3} [Group G] [MulAction G X] [MeasurableSpace X] [DiscreteMeasurableSpace X] {μ : MeasureTheory.Measure X} {u : Ultrafilter ι} {F : ι → Set X} (hF : IsFoelner G μ (↑u) F) : hF.addContent Set.univ = 1

The density-limit content has total mass one.

theorem IsFoelner.addContent_smul {G : Type u_1} {X : Type u_2} {ι : Type u_3} [Group G] [MulAction G X] [MeasurableSpace X] [DiscreteMeasurableSpace X] {μ : MeasureTheory.Measure X} {u : Ultrafilter ι} {F : ι → Set X} [MeasureTheory.SMulInvariantMeasure G X μ] (hF : IsFoelner G μ (↑u) F) (g : G) (s : Set X) : hF.addContent (g • s) = hF.addContent s

The density-limit content of a Følner family for a G-invariant measure is G-invariant.