def Equidecomposible {X : Type u_1} (G : Type u_2) [Group G] [MulAction G X] (E F : Set X) : Prop

In this top-level module we prove the main theorems specific Equidecompsibility and Paridoxicality. In particular we prove the main theorem that theorem banach_tarski_paradox_B3 : Paradoxical G3 B3

Equations

• One or more equations did not get rendered due to their size.

theorem equidecomposibility_trans {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] {L M N : Set X} : Equidecomposible G L M → Equidecomposible G M N → Equidecomposible G L N

Equidecomposibility is a transitive relation.

theorem equidecomposibility_symm {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] {M N : Set X} : Equidecomposible G M N → Equidecomposible G N M

Equidecomposibility is a symmetric relation.

def Paradoxical {X : Type u_1} (G : Type u_2) [Group G] [MulAction G X] (E : Set X) : Prop

Equations

• Paradoxical G E = (E.Nonempty ∧ ∃ (C : Set X) (D : Set X), C ⊆ E ∧ D ⊆ E ∧ Disjoint C D ∧ Equidecomposible G C E ∧ Equidecomposible G D E)

theorem paradoxical_of_equidecomposible_of_paradoxical {X : Type u_1} (G : Type u_2) [Group G] [MulAction G X] (E F : Set X) : Paradoxical G E → Equidecomposible G E F → Paradoxical G F

Equidecomposibility preserves Paradoxicallity.

theorem equidecomposible_of_supergroup_of_equidecomposible {X : Type u_1} (G : Type u_2) [Group G] [MulAction G X] (E F : Set X) (H : Subgroup G) : Equidecomposible (↥H) E F → Equidecomposible G E F

theorem paradoxical_of_supergroup_of_paradoxical {X : Type u_1} (G : Type u_2) [Group G] [MulAction G X] (H : Subgroup G) (E : Set X) : Paradoxical (↥H) E → Paradoxical G E

def SelfParadoxical (G : Type u_1) [Group G] : Prop

Equations

• SelfParadoxical G = Paradoxical G Set.univ

theorem paradoxical_preserved_by_iso {X : Type u_1} {Y : Type u_2} {G : Type u_3} {H : Type u_4} [Group G] [Group H] [MulAction G X] [MulAction H Y] (E : Set X) (iso : G ≃* H) (f : X ≃ Y) : (∀ (x : X) (g : G), iso g • f x = f (g • x)) → Paradoxical G E → Paradoxical H (⇑f '' E)

theorem self_paradoxical_preserved_by_iso {G : Type u_1} {H : Type u_2} [Group G] [Group H] : SelfParadoxical G → ∀ (a✝ : G ≃* H), SelfParadoxical H

theorem free_group_of_rank_two_is_self_paradoxical : SelfParadoxical FG2

Our first proof that something is Paradoxical. All other results will derive from this.

def FixedPoints {X : Type u_1} (G : Type u_2) [Group G] [MulAction G X] (E : Set X) : Set X

Set of points in X fixed by some non-identity element of G.

Equations

• FixedPoints G E = ⋃ g ∈ Set.univ \ {1}, {x : X | x ∈ E ∧ g • x = x}

theorem paradoxical_of_action_of_self_paradoxical {X : Type u_1} (G : Type u_2) [Group G] [MulAction G G] [MulAction G X] (Dom : Set X) : (∀ (g : G), f g '' Dom ⊆ Dom) → SelfParadoxical G → (¬∃ (fp : X), fp ∈ FixedPoints G Dom) → Dom.Nonempty → Paradoxical G Dom

If G is SelfParadoxical and acts on X without any nontrivial fixed points, then X is G-Paradoxical.

theorem hausdorff_paradox : ∃ D ⊆ S2, Countable ↑D ∧ Paradoxical (↥SO3) (S2 \ D)

We can find a countable subset of the 2-sphere such that removing it results in a set that is paradoxical under SO(3).

theorem absorption_lemma_1 {X : Type u_1} (G : Type u_2) [Group G] [MulAction G X] (E S : Set X) : (∃ D ⊆ E, S ⊆ D ∧ ∃ (ρ : G), f ρ '' D = D \ S) → Equidecomposible G E (E \ S)

A series of lemmas showing that when considering the paradoxicality of a set E certain subsets S ⊆ E can be "absorbed" into E, specifically that E is equidcomposible with E \ S.

theorem absorption_lemma_2 {X : Type u_1} (G : Type u_2) [Group G] [MulAction G X] (E S : Set X) : (∃ (ρ : G), (∀ (i : ℕ), (f ρ)^[i] '' S ⊆ E) ∧ ∀ (i : ℕ), Disjoint S ((f ρ)^[i + 1] '' S)) → Equidecomposible G E (E \ S)

theorem absorption_lemma_3 {X : Type u_1} (G : Type u_2) [Group G] [MulAction G X] (E S : Set X) : (∃ (F : ℝ → G), Countable ↑(Bad F S) ∧ ∀ (r : ℝ), orbit (F r) S ⊆ E) → Equidecomposible G E (E \ S)

theorem S2_equidecomposible_of_S2_minus_countable (S : Set R3) : S ⊆ S2 ∧ Countable ↑S → Equidecomposible (↥SO3) (S2 \ S) S2

Our first application of absorption: We can absorb any countable subset of the 2-sphere.

theorem banach_tarski_paradox_s2 : Paradoxical (↥SO3) S2

First we prove a simpler version of the main theorem on just the 2-sphere.

theorem banach_tarski_paradox_B3_minus_origin : Paradoxical (↥SO3) B3min

Next we extend the claim to the solid ball minus the origin.

theorem banach_tarski_paradox_B3 : Paradoxical G3 B3

Finally we show that we can absorb the origin.