Theorems · Definition · measure theory

maxFoelner

(G : Type u_1) →
  {X : Type u_2} →
    [inst : MeasurableSpace X] → MeasureTheory.Measure X → [inst : 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.

Defined in

Mathlib.MeasureTheory.Group.FoelnerFilter

Cited by

3 results in Mathlib

Foundations

Depth 170 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceGroupMulAction