Følner sequences and filters - definitions and properties

This file defines Følner sequences and filters for measurable spaces acted on by a group.

Definitions

• IsFoelner G μ l F : Consider a group G acting on a measure space X. A sequence of sets F : ι → Set X is Følner with respect to the G-action, the measure μ, and a filter l on the indexing type ι, if:

  1. Eventually, as i tends to l, the set F i is measurable with finite non-zero measure,
  2. For all g : G, μ ((g • F i) ∆ F i) / μ (F i) tends to 0.

• IsFoelner.mean μ u F s : The limit along an ultrafilter u of the density of a set s with respect to a Følner sequence F in the measure space X.

• maxFoelner G μ : The maximal Følner filter with respect to some group G acting on a measure space X is the pullback of 𝓝 0 along the map s ↦ μ (g • s) / μ s over measurable sets of finite non-zero measure.

• IsAddFoelner G μ l F: the analog of IsFoelner G μ l F for an additive group action

Main results

• IsFoelner.amenable : If there exists a non-trivial Følner filter with respect to some group G acting on a measure space X, then there exists a G-invariant finitely additive probability measure on X.

• isFoelner_iff_tendsto : A sequence of sets is Følner if and only if it tends to the maximal Følner filter. The attribute "maximal" of the latter comes from the direct implication of this theorem : if IsFoelner G μ l F then the push-forward filter map F l ≤ maxFoelner G μ.

• amenable_of_maxFoelner_neBot : If the maximal Følner filter is non-trivial, then there exists a G-invariant finitely additive probability measure on X.

Temporary design adaptations

• In the current version, we refer to the amenability of the action of a group on a measure space (e.g. in IsFoelner.amenable and amenable_of_maxFoelner_neBot), even though a definition of amenability has not yet been given in Mathlib. This is because there are different notions of amenability for groups and for group actions, and a Mathlib definition should be provided at the greatest level of generality, on which there has not yet been a general consensus. At the present moment, amenable corresponds to the existence of a G-invariant finitely additive probability measure.

Tags

Foelner, Følner filter, amenability, amenable group

structure IsAddFoelner (G : Type u_4) {X : Type u_5} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [AddGroup G] [AddAction G X] {ι : Type u_6} (l : Filter ι) (F : ι → Set X) : Prop

Consider an additive group G acting on a measure space X. A sequence of sets F : ι → Set X is Følner with respect to the G-action, the measure μ, and a filter l on the indexing type ι, if:

1. Each s in l is eventually measurable with finite non-zero measure,
2. For all g : G, μ ((g +ᵥ F i) ∆ F i) / μ (F i) tends to 0.

• eventually_measurableSet : ∀ᶠ (i : ι) in l, MeasurableSet (F i)
• eventually_meas_ne_zero : ∀ᶠ (i : ι) in l, μ (F i) ≠ 0
• eventually_meas_ne_top : ∀ᶠ (i : ι) in l, μ (F i) ≠ ⊤
• tendsto_meas_vadd_symmDiff (g : G) : Filter.Tendsto (fun (i : ι) => μ (symmDiff (g +ᵥ F i) (F i)) / μ (F i)) l (nhds 0)

theorem isAddFoelner_iff (G : Type u_4) {X : Type u_5} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [AddGroup G] [AddAction G X] {ι : Type u_6} (l : Filter ι) (F : ι → Set X) : IsAddFoelner G μ l F ↔ (∀ᶠ (i : ι) in l, MeasurableSet (F i)) ∧ (∀ᶠ (i : ι) in l, μ (F i) ≠ 0) ∧ (∀ᶠ (i : ι) in l, μ (F i) ≠ ⊤) ∧ ∀ (g : G), Filter.Tendsto (fun (i : ι) => μ (symmDiff (g +ᵥ F i) (F i)) / μ (F i)) l (nhds 0)

structure IsFoelner (G : Type u_1) {X : Type u_2} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [Group G] [MulAction G X] {ι : Type u_3} (l : Filter ι) (F : ι → Set X) : Prop

Consider a group G acting on a measure space X. A sequence of sets F : ι → Set X is Følner with respect to the G-action, the measure μ, and a filter l on the indexing type ι, if:

1. Each s in l is eventually measurable with finite non-zero measure,
2. For all g : G, μ ((g • F i) ∆ F i) / μ (F i) tends to 0.

• eventually_measurableSet : ∀ᶠ (i : ι) in l, MeasurableSet (F i)
• eventually_meas_ne_zero : ∀ᶠ (i : ι) in l, μ (F i) ≠ 0
• eventually_meas_ne_top : ∀ᶠ (i : ι) in l, μ (F i) ≠ ⊤
• tendsto_meas_smul_symmDiff (g : G) : Filter.Tendsto (fun (i : ι) => μ (symmDiff (g • F i) (F i)) / μ (F i)) l (nhds 0)

theorem isFoelner_iff (G : Type u_1) {X : Type u_2} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [Group G] [MulAction G X] {ι : Type u_3} (l : Filter ι) (F : ι → Set X) : IsFoelner G μ l F ↔ (∀ᶠ (i : ι) in l, MeasurableSet (F i)) ∧ (∀ᶠ (i : ι) in l, μ (F i) ≠ 0) ∧ (∀ᶠ (i : ι) in l, μ (F i) ≠ ⊤) ∧ ∀ (g : G), Filter.Tendsto (fun (i : ι) => μ (symmDiff (g • F i) (F i)) / μ (F i)) l (nhds 0)

theorem IsFoelner.univ_of_isFiniteMeasure {G : Type u_1} {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [Group G] [MulAction G X] {ι : Type u_3} {l : Filter ι} [NeZero μ] [MeasureTheory.IsFiniteMeasure μ] : IsFoelner G μ l fun (x : ι) => Set.univ

The constant sequence X is Følner if X has finite measure.

theorem IsAddFoelner.univ_of_isFiniteMeasure {G : Type u_1} {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [AddGroup G] [AddAction G X] {ι : Type u_3} {l : Filter ι} [NeZero μ] [MeasureTheory.IsFiniteMeasure μ] : IsAddFoelner G μ l fun (x : ι) => Set.univ

The constant sequence X is Følner if X has finite measure.

theorem IsFoelner.mono {G : Type u_1} {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [Group G] [MulAction G X] {ι : Type u_3} {l : Filter ι} {F : ι → Set X} {l' : Filter ι} (hfoel : IsFoelner G μ l F) (hle : l' ≤ l) : IsFoelner G μ l' F

theorem IsAddFoelner.mono {G : Type u_1} {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [AddGroup G] [AddAction G X] {ι : Type u_3} {l : Filter ι} {F : ι → Set X} {l' : Filter ι} (hfoel : IsAddFoelner G μ l F) (hle : l' ≤ l) : IsAddFoelner G μ l' F

theorem IsFoelner.comp_tendsto {G : Type u_1} {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [Group G] [MulAction G X] {ι : Type u_3} {l : Filter ι} {F : ι → Set X} {ι' : Type u_4} {l' : Filter ι'} {φ : ι' → ι} (hfoel : IsFoelner G μ l F) (htendsto : Filter.Tendsto φ l' l) : IsFoelner G μ l' (F ∘ φ)

theorem IsAddFoelner.comp_tendsto {G : Type u_1} {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [AddGroup G] [AddAction G X] {ι : Type u_3} {l : Filter ι} {F : ι → Set X} {ι' : Type u_4} {l' : Filter ι'} {φ : ι' → ι} (hfoel : IsAddFoelner G μ l F) (htendsto : Filter.Tendsto φ l' l) : IsAddFoelner G μ l' (F ∘ φ)

noncomputable def IsFoelner.mean {X : Type u_2} [MeasurableSpace X] (μ : MeasureTheory.Measure X) {ι : Type u_3} (u : Ultrafilter ι) (F : ι → Set X) (s : Set X) : ENNReal

The limit along an ultrafilter of the density of a set with respect to a sequence in X.

Equations

• IsFoelner.mean μ u F s = limUnder ↑u fun (i : ι) => μ (s ∩ F i) / μ (F i)

noncomputable def IsAddFoelner.mean {X : Type u_2} [MeasurableSpace X] (μ : MeasureTheory.Measure X) {ι : Type u_3} (u : Ultrafilter ι) (F : ι → Set X) (s : Set X) : ENNReal

The limit along an ultrafilter of the density of a set with respect to a sequence in X.

Equations

• IsAddFoelner.mean μ u F s = limUnder ↑u fun (i : ι) => μ (s ∩ F i) / μ (F i)

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

theorem IsAddFoelner.tendsto_nhds_mean {G : Type u_1} {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [AddGroup G] [AddAction G X] {ι : Type u_3} {u : Ultrafilter ι} {F : ι → Set X} (hfoel : IsAddFoelner G μ (↑u) F) (s : Set X) : Filter.Tendsto (fun (i : ι) => μ (s ∩ F i) / μ (F i)) (↑u) (nhds (mean μ u F s))

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

theorem IsAddFoelner.mean_univ_eq_zero {G : Type u_1} {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [AddGroup G] [AddAction G X] {ι : Type u_3} {u : Ultrafilter ι} {F : ι → Set X} (hfoel : IsAddFoelner G μ (↑u) F) : mean μ u F Set.univ = 1

theorem IsFoelner.mean_union_eq_add_of_disjoint {G : Type u_1} {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [Group G] [MulAction G X] {ι : Type u_3} {u : Ultrafilter ι} {F : ι → Set X} (hfoel : IsFoelner G μ (↑u) F) (s t : Set X) (ht : MeasurableSet t) (hdisj : Disjoint s t) : mean μ u F (s ∪ t) = mean μ u F s + mean μ u F t

theorem IsAddFoelner.mean_union_eq_add_of_disjoint {G : Type u_1} {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [AddGroup G] [AddAction G X] {ι : Type u_3} {u : Ultrafilter ι} {F : ι → Set X} (hfoel : IsAddFoelner G μ (↑u) F) (s t : Set X) (ht : MeasurableSet t) (hdisj : Disjoint s t) : mean μ u F (s ∪ t) = mean μ u F s + mean μ u F t

theorem IsFoelner.tendsto_meas_smul_symmDiff_smul {G : Type u_1} {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [Group G] [MulAction G X] {ι : Type u_3} {u : Ultrafilter ι} {F : ι → Set X} [MeasureTheory.SMulInvariantMeasure G X μ] (hfoel : IsFoelner G μ (↑u) F) (g h : G) : Filter.Tendsto (fun (i : ι) => μ (symmDiff (g • F i) (h • F i)) / μ (F i)) (↑u) (nhds 0)

theorem IsAddFoelner.tendsto_meas_vadd_symmDiff_vadd {G : Type u_1} {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [AddGroup G] [AddAction G X] {ι : Type u_3} {u : Ultrafilter ι} {F : ι → Set X} [MeasureTheory.VAddInvariantMeasure G X μ] (hfoel : IsAddFoelner G μ (↑u) F) (g h : G) : Filter.Tendsto (fun (i : ι) => μ (symmDiff (g +ᵥ F i) (h +ᵥ F i)) / μ (F i)) (↑u) (nhds 0)

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

theorem IsAddFoelner.mean_vadd_eq_mean_vadd {G : Type u_1} {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [AddGroup G] [AddAction G X] {ι : Type u_3} {u : Ultrafilter ι} {F : ι → Set X} [MeasureTheory.VAddInvariantMeasure G X μ] (hfoel : IsAddFoelner G μ (↑u) F) (g h : G) (s : Set X) : mean μ u F (g +ᵥ s) = mean μ u F (h +ᵥ s)

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

theorem IsAddFoelner.mean_vadd_eq_mean {G : Type u_1} {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [AddGroup G] [AddAction G X] {ι : Type u_3} {u : Ultrafilter ι} {F : ι → Set X} [MeasureTheory.VAddInvariantMeasure G X μ] (hfoel : IsAddFoelner G μ (↑u) F) (g : G) (s : Set X) : mean μ u F (g +ᵥ s) = mean μ u F s

theorem IsFoelner.amenable {G : Type u_1} {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [Group G] [MulAction G X] {ι : Type u_3} {l : Filter ι} {F : ι → Set X} [MeasureTheory.SMulInvariantMeasure G X μ] [l.NeBot] (hfoel : IsFoelner G μ l F) : ∃ (m : Set X → ENNReal), m Set.univ = 1 ∧ (∀ (s t : Set X), MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t) ∧ ∀ (g : G) (s : Set X), m (g • s) = m s

If there exists a non-trivial Følner filter with respect to some group G acting on a measure space X, then there exists a G-invariant finitely additive probability measure on X.

theorem IsAddFoelner.amenable {G : Type u_1} {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [AddGroup G] [AddAction G X] {ι : Type u_3} {l : Filter ι} {F : ι → Set X} [MeasureTheory.VAddInvariantMeasure G X μ] [l.NeBot] (hfoel : IsAddFoelner G μ l F) : ∃ (m : Set X → ENNReal), m Set.univ = 1 ∧ (∀ (s t : Set X), MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t) ∧ ∀ (g : G) (s : Set X), m (g +ᵥ s) = m s

If there exists a non-trivial Følner filter with respect to some additive group G acting on a measure space X, then there exists a G-invariant finitely additive probability measure on X.

def maxFoelner (G : Type u_1) {X : Type u_2} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [Group G] [MulAction G X] : Filter (Set X)

The maximal Følner filter with respect to some group G acting on a measure space X is the pullback of 𝓝 0 along the map s ↦ μ (g • s) / μ s on measurable sets of finite non-zero measure.

Equations

• maxFoelner G μ = Filter.principal {s : Set X | MeasurableSet s ∧ μ s ≠ 0 ∧ μ s ≠ ⊤} ⊓ ⨅ (g : G), Filter.comap (fun (s : Set X) => μ (symmDiff (g • s) s) / μ s) (nhds 0)

def maxAddFoelner (G : Type u_1) {X : Type u_2} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [AddGroup G] [AddAction G X] : Filter (Set X)

The maximal Følner filter with respect to some additive group G acting on a measure space X is the pullback of 𝓝 0 along the map s ↦ μ (g +ᵥ s) / μ s on measurable sets of finite non-zero measure.

Equations

• maxAddFoelner G μ = Filter.principal {s : Set X | MeasurableSet s ∧ μ s ≠ 0 ∧ μ s ≠ ⊤} ⊓ ⨅ (g : G), Filter.comap (fun (s : Set X) => μ (symmDiff (g +ᵥ s) s) / μ s) (nhds 0)

theorem isFoelner_iff_tendsto {G : Type u_1} {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [Group G] [MulAction G X] {ι : Type u_3} (l : Filter ι) (F : ι → Set X) : IsFoelner G μ l F ↔ Filter.Tendsto F l (maxFoelner G μ)

theorem isAddFoelner_iff_tendsto {G : Type u_1} {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [AddGroup G] [AddAction G X] {ι : Type u_3} (l : Filter ι) (F : ι → Set X) : IsAddFoelner G μ l F ↔ Filter.Tendsto F l (maxAddFoelner G μ)

theorem isFoelner_maxFoelner (G : Type u_1) {X : Type u_2} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [Group G] [MulAction G X] : IsFoelner G μ (maxFoelner G μ) id

theorem isAddFoelner_maxAddFoelner (G : Type u_1) {X : Type u_2} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [AddGroup G] [AddAction G X] : IsAddFoelner G μ (maxAddFoelner G μ) id

theorem amenable_of_maxFoelner_neBot {G : Type u_1} {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [Group G] [MulAction G X] [MeasureTheory.SMulInvariantMeasure G X μ] [(maxFoelner G μ).NeBot] : ∃ (m : Set X → ENNReal), m Set.univ = 1 ∧ (∀ (s t : Set X), MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t) ∧ ∀ (g : G) (s : Set X), m (g • s) = m s

theorem amenable_of_maxAddFoelner_neBot {G : Type u_1} {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [AddGroup G] [AddAction G X] [MeasureTheory.VAddInvariantMeasure G X μ] [(maxAddFoelner G μ).NeBot] : ∃ (m : Set X → ENNReal), m Set.univ = 1 ∧ (∀ (s t : Set X), MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t) ∧ ∀ (g : G) (s : Set X), m (g +ᵥ s) = m s