Invariant contents and paradoxical sets

Let a group G act on X, and let m be a finitely additive set function on all subsets of X, m : MeasureTheory.AddContent M (Set.univ : Set (Set X)), which is invariant under the action: m (g • s) = m s. Cutting a set into finitely many pieces and moving each piece by an element of G preserves the total content, so equidecomposable sets have the same content (TauCeti.Equidecomposable.addContent_eq).

Consequently a paradoxical set S, which splits into two disjoint sets each equidecomposable with S, satisfies m S + m S = m S. For an ℝ≥0∞-valued content this forces m S to be zero or infinite. In particular a group action admitting an invariant finitely additive probability on all subsets of X is not paradoxical on all of X. This is the easy half of Tarski's characterization of amenability by the absence of paradoxical decompositions.

Main results

• TauCeti.Equidecomposable.addContent_eq: an invariant content takes equal values on equidecomposable sets.
• TauCeti.Paradoxical.addContent_add_self: an invariant content of a paradoxical set S satisfies m S + m S = m S.
• TauCeti.Paradoxical.addContent_eq_zero: a finite invariant ℝ≥0∞-valued content vanishes on paradoxical sets.
• TauCeti.not_paradoxical_univ_of_addContent: if X carries an invariant finitely additive probability on all subsets, then X is not paradoxical.

References

• A. Garrido, An introduction to amenable groups, §1.

theorem TauCeti.Equidecomposable.addContent_eq {X : Type u_1} {G : Type u_2} {M : Type u_3} [Group G] [MulAction G X] [AddCommMonoid M] {m : MeasureTheory.AddContent M Set.univ} {A B : Set X} (hm : ∀ (g : G) (s : Set X), m (g • s) = m s) (h : Equidecomposable G A B) : m A = m B

A content on all subsets which is invariant under the action of G takes equal values on sets which are equidecomposable using G.

theorem TauCeti.Paradoxical.addContent_add_self {X : Type u_1} {G : Type u_2} {M : Type u_3} [Group G] [MulAction G X] [AddCommMonoid M] {m : MeasureTheory.AddContent M Set.univ} {S : Set X} (hm : ∀ (g : G) (s : Set X), m (g • s) = m s) (hS : Paradoxical G S) : m S + m S = m S

An invariant content of a paradoxical set S satisfies m S + m S = m S: the set splits into two disjoint sets, each with the same content as S.

theorem TauCeti.Paradoxical.addContent_eq_zero {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] {m : MeasureTheory.AddContent ENNReal Set.univ} {S : Set X} (hm : ∀ (g : G) (s : Set X), m (g • s) = m s) (hS : Paradoxical G S) (hfin : m S ≠ ⊤) : m S = 0

A finite invariant ℝ≥0∞-valued content on all subsets vanishes on every paradoxical set.

theorem TauCeti.not_paradoxical_univ_of_addContent {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] {m : MeasureTheory.AddContent ENNReal Set.univ} (hm : ∀ (g : G) (s : Set X), m (g • s) = m s) (h1 : m Set.univ = 1) : ¬Paradoxical G Set.univ

If X carries a finitely additive probability on all subsets which is invariant under the action of G, then X is not paradoxical for this action.