Expansion of finite sets under a finite set of acting elements

Let a monoid α act on a type β, and let D ⊆ α be finite. We say that D expands finite sets by a factor c if

c · |F| ≤ |D • F|        for every finite F ⊆ β.

This file proves two consequences of such an expansion bound.

• Expansion iterates: if D expands by c ≥ 0, then the pointwise power D ^ n expands by c ^ n.
• Expansion by a natural number k gives, by Hall's marriage theorem for an infinite index type with finite neighbour sets, an injection j : β × Fin k → β moving each point by an element of D: j (x, i) = d • x for some d ∈ D. Each point of β is thus sent to k distinct points, in a way that is injective overall.

For a group without Følner sets these give the finite set and the injection used to construct a paradoxical decomposition, the hard direction of Tarski's alternative.

Main results

• Finset.pow_mul_card_le_card_pow_smul: if c · |F| ≤ |D • F| for all finite F and c ≥ 0, then c ^ n · |F| ≤ |D ^ n • F|.
• Finset.exists_injective_of_mul_card_le_card_smul: if k · |F| ≤ |D • F| for all finite F, there is an injective j : β × Fin k → β with j (x, i) = d • x for some d ∈ D.

References

• T. Ceccherini-Silberstein, R. Grigorchuk, P. de la Harpe, Amenability and paradoxical decompositions for pseudogroups and for discrete metric spaces, Theorem 35.
• A. Garrido, An introduction to amenable groups, proof of Theorem 1.11.

theorem Finset.pow_mul_card_le_card_pow_smul {α : Type u_1} {β : Type u_2} [Monoid α] [MulAction α β] [DecidableEq α] [DecidableEq β] {D : Finset α} {c : ℝ} (hc : 0 ≤ c) (h : ∀ (F : Finset β), c * ↑F.card ≤ ↑(D • F).card) (n : ℕ) (F : Finset β) : c ^ n * ↑F.card ≤ ↑(D ^ n • F).card

Iterated expansion. If a finite set D of a monoid expands every finite set by a factor c ≥ 0, then its n-th pointwise power expands every finite set by the factor c ^ n.

theorem Finset.exists_injective_of_mul_card_le_card_smul {α : Type u_1} {β : Type u_2} [SMul α β] [DecidableEq β] {D : Finset α} {k : ℕ} (h : ∀ (F : Finset β), k * F.card ≤ (D • F).card) : ∃ (j : β × Fin k → β), Function.Injective j ∧ ∀ (p : β × Fin k), ∃ d ∈ D, d • p.1 = j p

Hall's theorem for expanding sets. If a finite set D acting on β satisfies k · |F| ≤ |D • F| for every finite F ⊆ β, then there is an injective map j : β × Fin k → β moving each point by an element of D: j (x, i) = d • x for some d ∈ D.

This applies Hall's marriage theorem to the neighbour sets D • {x} indexed by β × Fin k.