Banach Tarski Paradox in Lean

Stream: mathlib4

[Christian K]

Hello there, I'm a high school student from germany and I'm working together with another student to formalize the Banach-Tarski Paradox in lean.(A ball is equidecomposable with two copies of itself). (I already made a post in #new members > Introduction some time ago). We've realized that the Formalization of the Banach-Tarski Paradox is a quite substantial task (especially for beginners). So, if you are interested (and perhaps even want to contribute), this thread can be used for discussion. The blueprint and a link to the github repo can be found at https://bergschaf.github.io/banach-tarski/ (PRs are very welcome :) )

[Christian K]

We've already completed a definition of equidecomposability and we've proven that a circle is equidecomposable with a copy of itself without a certain point. Where would this fit in the mathlib?

[Kim Morrison]

(https://github.com/Bergschaf/banach-tarski/blob/master/banach_tarski/Equidecomposable/Def.lean#L151 for reference.)

[Kim Morrison]

I think this would need to be rewritten and made quite a bit more general to go in Mathlib. (i.e. neither R^3, or even GL, should be baked into the definition; can you just use Mathlib's affine maps isometries, if such exist?) It looks like you're also developing a lot of non-canonical List api that it would be good to unify first.

[Mitchell Lee]

Looking at the blueprint, it seems there are a few things you use that could fit into mathlib on their own.

For example, I searched around the docs and I don't think the orbits of a monoid action (or group action) appear in mathlib.

You also use the fact that $\pi^2$ is irrational (although I don't actually believe this is really necessary), which, as far as I can tell, doesn't appear in mathlib either. In fact, even the irrationality of $\pi$ doesn't appear.

Finally, you of course use the multiplicative action of the linear group $GL_3$ on Euclidean space $\mathbb{R}^3$. You also use the multiplicative action of the affine group $\mathbb{R}^3 \rtimes GL_3$ on $\mathbb{R}^3$. These aren't defined in mathlib (at least not as MulActions, although there is the vecMul notation ᵥ*). In fact, the affine group isn't even defined in mathlib as far as I can see.

I wonder if someone could weigh in on whether it might be better to try to get these individual pieces into mathlib first.

[Kim Morrison]

There are lots of subsidiary definitions for equidecomposable which you're not using (e.g. just API for writing a set as a disjoint union, which I don't think should be in terms of List).

[Mitchell Lee]

Also, I might be wrong, but shouldn't you be using the special orthogonal group $SO_3$ (https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/UnitaryGroup.html#Matrix.orthogonalGroup) instead of $GL_3$?

[Eric Wieser]

In fact, the affine group isn't even defined in mathlib as far as I can see.

docs#AffineEquiv.group ? (found with loogle by searching for "affine", Group)

[Ruben Van de Velde]

Transcendentality of pi is in #6718

[Christian K]

Mitchell Lee said:

You also use the fact that $\pi^2$ is irrational (although I don't actually believe this is really necessary), which, as far as I can tell, doesn't appear in mathlib either. In fact, even the irrationality of $\pi$ doesn't appear.

Yeah, but I think there is a PR that contains the irrationality of PI (ohh, Ruben van de velde was already faster ;) ). For my proof, someone on zulip suggested that I use the irrationality of sqrt 2 . (But I haven't prooved this lemma yet). I think it might be a good idea to wait for the irrationality of PI before putting the equidecomposability of the circle in the Mathlib.

[Christian K]

Scott Morrison said:

There are lots of subsidiary definitions for equidecomposable which you're not using (e.g. just API for writing a set as a disjoint union, which I don't think should be in terms of List).

What do you mean by this, should the parts and the rotations not be represented by lists?

[Mitchell Lee]

In your proof of Lemma 2.20 in the blueprint, instead of using $(\cos n, \sin n)$, use $(\cos (\sqrt{2} \pi n), \sin (\sqrt{2} \pi n))$. You can prove that these points are distinct without knowing anything about the irrationality of $\pi$.

[Christian K]

I'm already using this, the blueprint is not up to date (and in german, I'm sorry :rolling_on_the_floor_laughing: ).
(def A : Set r_3 := {w : r_3 | ∃ n : {x : ℕ | x > 0}, w = ![Real.cos (n * sq_2),Real.sin (n * sq_2),0]} -- TODO)

[Christian K]

I tried to prove here that the points are distinct, but the proof is incomplete.

[Mitchell Lee]

That's $(\cos (\sqrt{2} n), \sin (\sqrt{2} n))$. In order to know that those points are distinct, you need to know that $\pi / \sqrt{2}$ is irrational. If you use $(\cos (\sqrt{2} \pi n), \sin (\sqrt{2} \pi n))$ instead, it should be easier.

[Mitchell Lee]

You can use this: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.html#Real.Angle.cos_sin_inj

[Christian K]

Ok, I overlooked the difference. How long do you think will the irrationality of Pi take to get into the mathlib? Does it make sense to change this or should I just wait?

[Ruben Van de Velde]

At the rate it's going, months

[Yaël Dillies]

I don't think there's any point in waiting

[Mitchell Lee]

And this: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.html#Real.Angle.angle_eq_iff_two_pi_dvd_sub

I recommend writing the proof down on paper before trying to put it in Lean.

[Christian K]

Ok, I'll try to do it this way. But I'll have to do this together with my team mate, she is much better with mathematics than I am. In the meantime, I'll look into generalizing the equidecomposability. Apart from being not general enough, is the definition of equidecomposablility correct?

[Mitchell Lee]

As it is, the definition is not correct. One problem is that you are using the general linear group $GL$ instead of the orthogonal group.

One solution is to package the translation and rotation into a single affine isometry: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/NormedSpace/AffineIsometry.html#AffineIsometry. This should also make everything easier and cleaner to state.

It would also be nice if the definition of equidecomposability could be generalized to any normed affine space, rather than just $\mathbb{R}^3$.

[Mitchell Lee]

Finally, as Scott Morrison said, it is probably preferable not to use a List of sets to define equidecomposability. Lists are annoying to work with. Instead, you can use a term parts_X : Finset (Set r_3), which satisfies the hypotheses Pairwise (Disjoint on parts_X) (which means the parts are disjoint) and ⋃₀ parts_X = X (which means the union of the parts is X).

[Eric Wieser]

Or docs#Finpartition

[Kim Morrison]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Partition/Finpartition.html#Finpartition

[Mitchell Lee]

Ah, yes, that is better. Thanks.

[Mitchell Lee]

By the way, I said earlier that orbits are not in mathlib. I was wrong. They actually are: docs#MulAction.orbit. You should use this definition rather than your own.

In order to use this definition of orbits, you need to tell Lean that the group you are working with (in this case, the group $G$) acts on $\mathbb{R}^3$. You can do this by creating a local instance of MulAction. Doing so will also allow you to use the notation M • v for applying a transformation to a vector.

[Mitchell Lee]

One more thing.

I suggested using docs#Matrix.orthogonalGroup for your more specific computations. However, what you really want is the special orthogonal group $SO_3$. You are going to run into trouble at Lemma 2.10 if you try to use $GL_3$ or $O_3$.

I would recommend defining $SO_n$ before proceeding with your blueprint. This would be a nice thing to have in mathlib to begin with. Ideally, you could also define $O(V)$ and $SO(V)$ for any finite-dimensional inner product space $V$, but it'd also be fine to leave that for another time (in my opinion).

[Felix Weilacher]

A few comments are suggesting that equidecomposable should be defined for more general vector spaces than Euclidean space. Shouldn't it be defined for general group actions?

[Christian K]

abbrev specialOrthogonalGroup := {w : orthogonalGroup n β // Matrix.det (w : Matrix n n β) = 1}

Could I define SO as a subtype of the O, with the determinant 1? (inspired by https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.html#Matrix.SpecialLinearGroup)

[Christian K]

PR -> https://github.com/leanprover-community/mathlib4/pull/11708

[Eric Wieser]

I think it might be better to define it as the intersection with the special linear group, rather than nesting the subtypes.

[Christian K]

That doesn't seem to work out of the box, because the special linear group is defined as a subtype of Matrix.

[Mitchell Lee]

At the very least, I think it is important that you put a group structure on it. This will be done automatically if you define the special orthogonal group as the kernel of docs#Matrix.detMonoidHom.

While you're at it, you can define the special unitary group as well (which has the same definition).

[Scott Carnahan]

The special orthogonal group is a bit thorny to define in general. It is okay to use the kernel of determinant, when in odd rank, or if you are willing to assume 2 is invertible. Otherwise, it is better to define it as the kernel of the Dickson invariant when rank is even. A scheme-theoretic summary is on the middle-to-bottom of page 3 of B. Conrad's notes on orthogonal groups. Since you will be working in rank 3, it wouldn't hurt to limit the definition to odd rank.

[Mitchell Lee]

Thanks for the remark.

[Christian K]

abbrev specialUnitaryGroup :=  @MonoidHom.ker (Matrix.unitaryGroup n α) _ α _ ↑(@Matrix.detMonoidHom n _ _ α _)

What is the problem with this Definition? here on Github

Lean says:

type mismatch
  detMonoidHom
has type
  Matrix n n α →* α : Type (max (max v u) v)
but is expected to have type
  ↥(unitaryGroup n α) →* α : Type (max (max u v) v)

But earlier in the file, this is defined:

instance coeMatrix : Coe (unitaryGroup n α) (Matrix n n α) :=
  ⟨Subtype.val⟩

To me this looks like that ↥(unitaryGroup n α) should be the same as (Matrix n n α) . But why isn't this the case?

[Kevin Buzzard]

A general matrix isn't unitary so these two types aren't the same in any reasonable sense

[Richard Osborn]

As far as I know, lean doesn't coerce types in the contravariant position i.e. if A coerces to B, then a function B → C doesn't coerce to a function from A → C.

[Mitchell Lee]

You have (unitaryGroup n α).subtype (docs#Submonoid.subtype), which has type ↥(unitaryGroup n α) →* Matrix n n α.

You can compose this with the determinant homomorphism Matrix.detMonoidHom, which has type Matrix n n α →* α.

This will get you the term of type ↥(unitaryGroup n α) →* α that you need.

[Mitchell Lee]

So, I was oversimplifying a little when I said to just take the kernel of the determinant homomorphism. You need to restrict that homomorphism to the unitary group first.

[Mitchell Lee]

Actually, the easier way to do that is docs#MonoidHom.restrict.

[Christian K]

Ok thank you very much, i defined the special unitary group like this:

abbrev specialUnitaryGroup := MonoidHom.ker (MonoidHom.restrict Matrix.detMonoidHom
                                                (Matrix.unitaryGroup n α))

The special unitary group is now a subgroup of the unitary group.
But now, lean complains:

failed to synthesize instance
  Membership (Matrix n n α) (Subgroup ↥(unitaryGroup n α))

in this lemma

theorem mem_specialUnitaryGroup_iff :
    A ∈ Matrix.specialUnitaryGroup n α ↔ A * star A = 1 ∧ A.det = 1 := by sorry

why?

[Kevin Buzzard]

By default, if H : Subgroup G then it only makes sense to ask $x\in H$ if $x$ has type G. In type theory each term has a unique type, you can't just be flexible and say that the type of x is a matrix ring and a unitary group and lots of other things as well.

[Kevin Buzzard]

There are basic techniques which you use to move between these things, but they need to be applied.

[Richard Osborn]

I understand the confusion as A ∈ Matrix.unitaryGroup n α works due to the fact that unitaryGroup n α is a Submonoid of Matrix n n α.

[Richard Osborn]

Also your coeMatrix implementation is nonsense as aesop is pulling in the matrix A.

[Christian K]

Kevin Buzzard said:

There are basic techniques which you use to move between these things, but they need to be applied.

As you probably have noticed, I'm not very familiar with these techniques. Where can i learn more about rhis?

[Kevin Buzzard]

You might want to read the first few chapters of #tpil and learn about subtypes

[Christian K]

With this definition of the special unitary group, the theorem mem_specialUnitaryGroup_iff looks like this:

abbrev specialUnitaryGroup := (MonoidHom.restrict Matrix.detMonoidHom (Matrix.unitaryGroup n α)).ker

theorem mem_specialUnitaryGroup_iff  (h : A ∈ Matrix.unitaryGroup n α):
    {val:=A,property:=h} ∈ Matrix.specialUnitaryGroup n α ↔ A.det = 1 := by
  exact Eq.to_iff rfl

Is this acceptable?

[Kevin Buzzard]

Probably you can use \<A,h\> for the LHS and the proof is probably just by rfl.

In general I'm very unclear about how we're going to manage all these classical groups like special linear, orthogonal and unitary groups.

[Christian K]

I simplified the proofs and I created this theorem which makes creating an instance of SO way easier:

theorem specialOrthogonalGroup.mkOfDetEqOne (h1 : star A * A = 1) (h2 : A.det = 1) :
    specialOrthogonalGroup n β := ⟨⟨A,(by exact (mem_orthogonalGroup_iff' n β).mpr h1)⟩,h2⟩

(Inspired by GL.mkOfDetNeZero)

[Mitchell Lee]

This is nice. I have just a few comments.

• This should be a def rather than a theorem. Something should only be a theorem if its type is a proposition. The reason is that Lean does not unfold theorems, only defs. See here: https://leanprover.github.io/theorem_proving_in_lean4/propositions_and_proofs.html#working-with-propositions-as-types
• There's no need to write the words by and exact right next to each other. by enters tactic mode, and exact is the way to insert a proof term into a tactic block. So in a way, they are inverses of each other, and you can get rid of both of them. See here: https://leanprover.github.io/theorem_proving_in_lean4/tactics.html

[Christian K]

Ok thank you, CI already told me about the first one and I fixed the second one. Would be nice if you could review the PR

[Mitchell Lee]

I think this definition unfortunately conflicts with the remark @Scott Carnahan made, which might cause problems later.

[Mitchell Lee]

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Banach.20Tarski.20Paradox.20in.20Lean/near/429961018

[Mitchell Lee]

I do not know the best way to get around this problem.

[Christian K]

I'm not sure if this would work, but what about a Typeclass like OddFintype. It could look something like this:

class OddFintype (α : Type*) extends Fintype α where
  odd : Odd (Fintype.card α)

variable (n) (α) [Fintype n] [OddFintype n]

/--`Matrix.specialUnitaryGroup` is the group of unitary `n` by `n` matrices where the determinant
is 1-/
abbrev specialUnitaryGroup [OddFintype n] := (MonoidHom.restrict detMonoidHom (unitaryGroup n α)).ker

[Christian K]

But it seems like this would require an OddFin structure that only allows odd ranks.... Is there a smarter, easier way?

[Scott Carnahan]

I regret the direction this conversation went after my comment, which I wrote without thinking enough about the context.

You are working with the group of rigid rotations of a real 3-space, which is a group of independent interest. While it is possible to formulate it as a special case of a special orthogonal group, it might be better to define groups like rigidRotation n as a group of real rank n matrices satisfying your requirements. Then you can avoid the mess of arbitrary commutative rings, arbitrary quadratic forms, Dickson invariants, odd numbers, and so on, that are completely disconnected from your goals. Someone with more specialized expertise can make the connection with special orthogonal groups in the future (say, after we figure out how to formalize linear algebraic groups).

[Kalle Kytölä]

I think there is independent interest also in the group of linear isometries of a real inner product space $V$, otherwise known as "the orthogonal group of $V$". It moreover looks to me that this is not strictly a special case of the linear algebraic group, since infinite-dimensional $V$ make sense. (The special orthogonal group is then the subgroup of orientation preserving linear isometries, which makes sense in finite dimensions, at least.)

In other words, maybe two independent definitions are in place anyway, and then for $V=\R^n$ with the standard inner product we can later show that the (special) orthogonal group in the above sense coincides with the (special) orthogonal group in the linear algebraic group sense (distinct definitions).

[Kalle Kytölä]

Hmmm... The Mathlib-appropriate definition of orthogonal group in the "linear isometries" -sense should probably be a special case of groups of linear maps preserving an arbitrary bilinear form, though... This would include groups of interest to physicists such as the Lorentz group $O(1,3)$. And maybe bi-semilinear forms for the good measure, since linear isometries of complex inner product spaces (a.k.a. unitary transformations) are also interesting. :thinking:

I believe these would not be terrible to define, but let me try to avoid derailing the original interesting conversation another time...

[Mitchell Lee]

@Scott Carnahan I am glad that you made that comment. I certainly learned something from it.

I should take some responsibility for the direction that this conversation headed. I got stuck on "more generality is good" and didn't consider the trade-offs.

[Joseph Myers]

docs#LinearIsometryEquiv.instGroup already exists.

[Johan Commelin]

It might still pay off to define rigidRotation n in terms of existing API, because then the specialized API doesn't have to be built 100% by hand, but can be (partially) obtained by specializing the general API.

[Michael Rothgang]

I just remembered that the sphere-eversion project also formalised a construction of three-dimensional rotations here. Basically, given an axis of rotation and angle, they construct the corresponding rotation (as a smooth map), using the cross product.

@Christian K What kind of results do you need about rotations; is the above useful?
(I think the code is mostly good style; one proof broke over the last six month, but should be easy to fix. Ping me if you need help with that. I'm not sure if this would need to be generalised before going into mathlib.)

[Christian K]

@Michael Rothgang To be honest, I don't really understand the return type of the rotFunction, what does this Syntax mean? E →L[ℝ] E

[Richard Copley]

That's a docs#ContinuousLinearMap .

[Kevin Buzzard]

You should hopefully be able to hover over an instance of notation in Lean code and see what it represents. If the documentation doesn't pop up, this means that someone forgot something and a PR would be welcome :-)

[Christian K]

The special Orthogonal Group and the special unitary group are in the mathlib now :tada: :tada: :tada:
https://github.com/leanprover-community/mathlib4/pull/11708#issuecomment-2073873279

[Jireh Loreaux]

yep, now they just need some API.

[Christian K]

What is your opinion on this definition of equidecomposability? It uses an affine Isometry in a pseudometric space. (Pull Request):

variable (𝕜 : Type*) {V: Type*}(P: Type*)
  [NormedField 𝕜]
  [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P]

/--
Two subsets B₁ B₂ of a pseudometric space P are equidecomposable if B₁ and B₂ can be divided into
finitely many affinely isometric parts.
-/
def equidecomposable (B₁ B₂ : Set P) : Prop :=
  ∃ (P_B₁ : Finpartition B₁), ∃ (P_B₂ : Finpartition B₂), ∃ (f : P_B₁.parts → P_B₂.parts),
    P_B₂.parts.val.sizeOf = P_B₁.parts.val.sizeOf ∧
  Bijective f ∧ (∀ p_b₁ : P_B₁.parts, ∃ (a : AffineIsometry 𝕜 P P),
    ∀ x ∈ p_b₁.val, ∃ y ∈ (f p_b₁).val, a.toFun x = y ∧
    ∀ y ∈ (f p_b₁).val, ∃ x ∈ p_b₁.val, a.toFun x = y)

[Felix Weilacher]

Felix Weilacher said:

A few comments are suggesting that equidecomposable should be defined for more general vector spaces than Euclidean space. Shouldn't it be defined for general group actions?

.

[Felix Weilacher]

I am almost certain that we are going to want a equidecomposability and paradoxicality to be defined for group actions in general.

I think doing that, and then maybe having another definition in the MetricSpace namespace or something which uses the action of the isometry group is the way to go.

[Felix Weilacher]

The general definition is very standard, but here are some specific reasons I think we'll definitely want it in mathlib.

• When considering the action of a group on itself by left multiplication, it gives a nice definition of amenability (for countable groups, say)
• Even in nice metric spaces, it is often of interest to restrict the isometries one uses. For example, Laczkovich's famous circle squaring result uses only translations, and subsequent developments have gotten a lot of mileage out of the fact that the resulting group is abelian.
• Conversely, there are also interesting results in Euclidean space involving maps that are not isometries. E.g. https://en.wikipedia.org/wiki/Von_Neumann_paradox#:~:text=In%20mathematics%2C%20the%20von%20Neumann,same%20size%20as%20the%20original.

[Felix Weilacher]

I would do something like this

import Mathlib.Algebra.Group.Action.Defs
import Mathlib.Data.Setoid.Partition

variable (G : Type*) {X : Type*} [Group G] [SMul G X]

open Set

structure Equidecomposition (A B : Set X) extends A ≃ B where
    S : Finset G
    moves_by : ∀ a : A, ∃ g ∈ S, toEquiv a = g • (a : X)

def Equidecomposable (A B : Set X) : Prop := Nonempty (Equidecomposition G A B)

def Paradoxical (X : Type*) [SMul G X] : Prop :=
    ∃ A B : Set X, Disjoint A B ∧ Equidecomposable G A univ ∧ Equidecomposable G B univ

[Felix Weilacher]

G Probably only needs to be a monoid for these definitions, although the Equidecomposition structure will be better behaved when it is a group

[Felix Weilacher]

Here's some basic infrastructure to show how to use this definition

import Mathlib.Algebra.Group.Action.Basic
import Mathlib.Data.Finset.NAry

variable {X : Type*} (G : Type*)

variable [Group G] [MulAction G X]

open Set

structure Equidecomposition (A B : Set X) extends A ≃ B where
    elements : Finset G
    moves_by : ∀ a : A, ∃ g ∈ elements, toEquiv a = g • (a : X)

notation:50 A " ≃ₑ[" G:50 "] " B:50 => Equidecomposition G A B

def Equidecomposable (A B : Set X) : Prop := Nonempty (A ≃ₑ[G] B)

def Paradoxical (X : Type*) [MulAction G X] : Prop :=
    ∃ A B : Set X, Disjoint A B ∧ Equidecomposable G A univ ∧ Equidecomposable G B univ

instance equidecompositionEquivLike {A B : Set X} : EquivLike (A ≃ₑ[G] B) A B where
  coe e := e.toEquiv
  inv e := e.toEquiv.symm
  left_inv e := e.toEquiv.left_inv
  right_inv e := e.toEquiv.right_inv
  coe_injective' _ _ he _ := sorry

example (x : X) (p : X → Prop) : (∃ y ∈ ({x} : Set X), p y) ↔ p x := by exact exists_eq_left

def Equidecomposition.refl (A : Set X) : A ≃ₑ[G] A where
    toEquiv := Equiv.refl A
    elements := {1}
    moves_by := by simp

def Equidecomposition.symm [DecidableEq G] {A B : Set X} (f : A ≃ₑ[G] B): B ≃ₑ[G] A where
  toEquiv := f.toEquiv.symm
  elements := f.elements.image (·)⁻¹
  moves_by := by
    rintro b
    rcases f.moves_by (f.toEquiv.symm b) with ⟨g, g_mem, hg⟩
    use g⁻¹
    simp only [Finset.mem_image, Pi.inv_apply, inv_inj, exists_eq_right]
    refine ⟨g_mem, smul_left_cancel g ?_⟩
    simp[← hg]

def Equidecomposition.trans [DecidableEq G] {A B C : Set X} (f : A ≃ₑ[G] B) (i : B ≃ₑ[G] C)
    : A ≃ₑ[G] C where
  toEquiv := f.toEquiv.trans i.toEquiv
  elements := Finset.image₂ (· * ·) i.elements f.elements
  moves_by := by
    rintro a
    rcases f.moves_by a with ⟨g, g_mem, hg⟩
    rcases i.moves_by (f.toEquiv a) with ⟨k, k_mem, hk⟩
    simp only [Finset.mem_image₂, Equiv.trans_apply, exists_exists_and_exists_and_eq_and]
    use k, k_mem, g, g_mem
    rw [mul_smul, ← hg, ← hk]

[Christian K]

Thank you for your response, I'll integrate it into my PR as soon as possible

[Felix Weilacher]

For anyone interested, after talking with Christian I've prepared a PR #16936 with basic definitions about equidecompositions.

I used the docs#PartialEquiv API for this, and overall based my code heavily on the code in docs#PartialHomeomorph. This is my first time doing something like this and I'd appreciate any feedback

[Tristan Figueroa-Reid]

The new equidecomposition definition feels great to use! Here is a playground link to the proof of an equidecomposition of a deleted circle and the circle.

[Felix Weilacher]

cool! I'm working on a PR proving that if two sets equidecompose into subsets of eachother, they are equidecomposable (think Schroder-Bernstein). That should make this sort of thing, where one of the sets is already a subset of the other, even easier.

[Christian K]

Tristan Figueroa-Reid said:

The new equidecomposition definition feels great to use! Here is a playground link to the proof of an equidecomposition of a deleted circle and the circle.

I wasn't aware of the new API, it looks very nice indeed. This is a nice step towards the formalisation of Banach-Tarski :smile:

[Tristan Figueroa-Reid]

I can update the existing Banach-Tarski paradox repository to use the new definition :+1:

[Tristan Figueroa-Reid]

Tristan Figueroa-Reid said:

The new equidecomposition definition feels great to use! Here is a playground link to the proof of an equidecomposition of a deleted circle and the circle.

(I'm unaware of anything that depends on the equidecomposition of AddCircle - a countable set in literature, which is why I've avoided adding this to mathlib4).

[Tristan Figueroa-Reid]

Actually, looking deeper at this, is the main result from this repository right now that that the ℝ³ unit sphere is equidecomposable with the unit sphere - the origin?

[Tristan Figueroa-Reid]

Tristan Figueroa-Reid said:

The new equidecomposition definition feels great to use! Here is a playground link to the proof of an equidecomposition of a deleted circle and the circle.

Actually, is there any generalization of this? Some generic theorem for removing a countable set of elements from an uncountable space (with some restrictions that I can't think of) would be very useful for showing that the ball is equidecomposable with the ball minus the center.

[Felix Weilacher]

If the big set has empty interior I'm not sure how general you can be. For example it doesn't seem like an ellipse in R^2 is equidecomposable with an ellipse minus a point.

[Felix Weilacher]

For a bounded set S in R^n with nonempty interior, I think you can equidecompose S with S minus a countable set of n-1 dimensional hyperplanes, which may be the sort of generalization you're asking about.

[Felix Weilacher]

(using translations, even, for the latter)

[Tristan Figueroa-Reid]

Felix Weilacher said:

If the big set has empty interior I'm not sure how general you can be. For example it doesn't seem like an ellipse in R^2 is equidecomposable with an ellipse minus a point.

It feels like an ellipse in R^2 is equidecomposable with an ellipse minus a point would be true if a circle in R^2 is equidecomposable with a circle minus a point (which I believe to also be true, but I could be mistaken, as I don't remember the source of this proof).

Nonetheless, that generalization seems like a good idea.

[Tristan Figueroa-Reid]

While I'm not sure how to show that S minus a countable set of n-1 dimensional hyperplanes is equidecomposable with S, something we can do is generalize the earlier playground example I sent to a generic AddCircle instance (thus showing that any one of these wrapped lines is equidecomposable with a point removed), that way for any bounded set S in R^n,

• If the point lies on the boundary, we use our AddCircle equidecomposability instance on the boundary of the set
• If the point lies inside the set, we draw an arbitrary line that intersects that point: it should intersect two other points such that we can use our equidecomposability instance on the line turned into an AddCircle instance.

[Tristan Figueroa-Reid]

This generalization is mainly useful for the specific instance where we want to show that the unit ball is equidecomposable with the unit ball minus the center point, which I believe is an important lemma for the Banach-Tarski Paradox.

(Though, your generalization absolutely seems more powerful: however, I'm having trouble figure out a construction that would make that equidecomposition possible)

[Felix Weilacher]

Tristan Figueroa-Reid said:

It feels like an ellipse in R^2 is equidecomposable with an ellipse minus a point would be true if a circle in R^2 is equidecomposable with a circle minus a point (which I believe to also be true, but I could be mistaken, as I don't remember the source of this proof).

Isn't the equidecomposition of a circle with a circle minus a point the subject of the code you linked to above? That equidecomposition uses rotations centered at the center of the circle. The number of isometries that take an ellipse onto itself is just too small though.

[Felix Weilacher]

to be clear when I say ellipse I mean only the boundary of an ellipse

[Tristan Figueroa-Reid]

Felix Weilacher said:

Tristan Figueroa-Reid said:

It feels like an ellipse in R^2 is equidecomposable with an ellipse minus a point would be true if a circle in R^2 is equidecomposable with a circle minus a point (which I believe to also be true, but I could be mistaken, as I don't remember the source of this proof).

Isn't the equidecomposition of a circle with a circle minus a point the subject of the code you linked to above? That equidecomposition uses rotations centered at the center of the circle. The number of isometries that take an ellipse onto itself is just too small though.

(The equidecomposition I made I did not use the R^2 circle for, I used the general Real.Angle instance, so it's not the 'real' circle as the object: this was to simplify addition. That is why I believe this would hold for the ellipse, since you can always transform the point on the ellipses border by moving it across the border instead of rotating it at the center of the ellipse.)

[Felix Weilacher]

But then not every point is moving by the same isometry

[Felix Weilacher]

Put another way, the function which moves every point on the ellipse a fixed "angle" around the ellipse is not an isometry (unless the angle is 180 i guess)

[Tristan Figueroa-Reid]

By the way, do you have some proof (formal or otherwise) for

Felix Weilacher said:

For a bounded set S in R^n with nonempty interior, I think you can equidecompose S with S minus a countable set of n-1 dimensional hyperplanes, which may be the sort of generalization you're asking about.

I can't seem to convince myself of this (I can't even convince myself of the case where S is equidecomposable with S - one n-1 dimensional hyperplane)

[Felix Weilacher]

You could look at this: https://www.math.cmu.edu/~clintonc/s2024par/375spring2024.pdf

pages 102-105

[Tristan Figueroa-Reid]

Tristan Figueroa-Reid said:

To map AddCircle to Circle, it might be a good idea to have a theorem that if there exists an equidecomposition from A to B and a homeomorphism from B to C that there exists an equidecomposition from A to C (equidecomposition transivity by homeomorphism)

[Tristan Figueroa-Reid]

(By the way, the new banach-tarski theorem formalization is here)

[Tristan Figueroa-Reid]

Tristan Figueroa-Reid said:

To map AddCircle to Circle, it might be a good idea to have a theorem that if there exists an equidecomposition from A to B and a homeomorphism from B to C that there exists an equidecomposition from A to C (equidecomposition transivity by homeomorphism)

This is not true.

[Tristan Figueroa-Reid]

Made a PR to upstream the small theorem for coe_zero on an arbitrary AddCircle: https://github.com/leanprover-community/mathlib4/pull/22021

[Tristan Figueroa-Reid]

Actually, should we formalize the notion of order-preserving isometry actions in relation to equidecompositions? The formalization of Equidecomp deviates from the literature in that regard.

[Christian K]

Yeah, I think that this TODO in the Equidecomp file refers to that:
"TODO Prove the definition of equidecomposition used here is equivalent to the more familiar one using partitions. "

[Jz Pan]

Tristan Figueroa-Reid said:

To map AddCircle to Circle, it might be a good idea to have a theorem that if there exists an equidecomposition from A to B and a homeomorphism from B to C that there exists an equidecomposition from A to C (equidecomposition transivity by homeomorphism)

Simple counterexample: A = B and C is arbitrary space homeomorphic to B, then it implies that any homeomorphic spaces are equidecomposable.

[Felix Weilacher]

Christian K said:

Yeah, I think that this TODO in the Equidecomp file refers to that:
"TODO Prove the definition of equidecomposition used here is equivalent to the more familiar one using partitions. "

Not exactly. The TODO refers to the usual formulation being "split A into finitely many pieces, act on each by a single group element, and end up with a partition of B".

Partitions in mathlib are not that well supported, so this is hard to work with right now. I would also argue that even in pen and paper mathematics, the partial bijection formulation is closer to how most mathematicians think when working with equidecompositions.

It seems like you are referring the discrepancy between isometries of euclidean space and arbitrary group actions. The latter is a very standard generalization of the former in equidecomposition literature.

[Felix Weilacher]

If you want to deduce things about the circle in R^2 from your example with AddCircle, a good general thing to formalize would be that if two G-spaces (G a group) have a G-equivariant bijection between them, you can transfer equidecompositions in one to equidecompositions in the other.

More generally, if G and H are groups, X and Y are G and H-spaces resp, h: G \to H is any function, and f : X \to Y is an injection "commuting" with h, then any equidecompositions of sets in X transfer to equidecompositions of their images in Y.

[Tristan Figueroa-Reid]

By the way, I slightly discussed this with @Christian K , but is there a paper for the formal proof of the strong Banach-Tarski theorem for general n-dimensions? I opened a MSE post to some avail, where a user describes proving the weak Banach-Tarski theorem for any dimension 3 <= n, though that's the only information I've been able to gather on this so far.

[Tristan Figueroa-Reid]

https://www.cambridge.org/core/books/banachtarski-paradox/9C1FEAACF5EF6EB51C99F67136C8FCCB it can be proved by induction :+1: (see chapter 6)

[Tristan Figueroa-Reid]

It's not a trivial proof, but we can definitely establish stronger results from this than the existing Coq formalization of the Banach-Tarski theorem :+1:

[Tristan Figueroa-Reid]

@Felix Weilacher are you working on a definition of paradoxical subsets/actions?

[Felix Weilacher]

You could do the following: (here G is a group with a MulAction instance on X)

def Equidecomposable (A B : Set X) : Prop := ∃ f : Equidecomp X G, f.source = A ∧ f.target = B

def paradoxical (A : Set X) : Prop := ∃ B : Set X,
    B ⊆ A ∧ Equidecomposable G B A ∧ Equidecomposable G (A \ B) A

[Tristan Figueroa-Reid]

Alright (for extra context, @Christian K and I were thinking of following the proof of the Banach-Tarski theorem from Amenability of Discrete Groups by Examples, which would offer us a more general result than the earlier mentioned proof by induction)