Theorems · Inductive type · measure theory

IsFoelner

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

Defined in

Mathlib.MeasureTheory.Group.FoelnerFilter

Cited by

17 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

MeasurableSpaceGroupMulAction