Ben Green's Open Problem 41

References

• [Gr24] Ben Green's Open Problem 41
• [Ma15] Manners, Freddie. "A solution to the pyjama problem." Inventiones mathematicae 202.1 (2015): 239-270.
• [KrLe25] Kravitz, Noah, and James Leng. "Quantitative pyjama." arXiv preprint arXiv:2510.17744 (2025).

def Green41.pyjamaSet (ε : ℝ) : Set ℂ

The pyjama set is the set of points in the complex plane whose real part is within $\varepsilon$ of an integer.

Equations

• Green41.pyjamaSet ε = {z : ℂ | ∃ (k : ℤ), |z.re - ↑k| ≤ ε}

def Green41.coveringCopies (ε : ℝ) : Set ℕ

The set of valid numbers of rotated copies of the pyjama set of width ε that cover the plane.

Equations

• Green41.coveringCopies ε = {n : ℕ | ∃ (Θ : Finset ℝ), Θ.card = n ∧ ⋃ θ ∈ Θ, Complex.exp (↑θ * Complex.I) • Green41.pyjamaSet ε = Set.univ}

noncomputable def Green41.minCopies (ε : ℝ) : ℕ

The minimal number of rotated copies of the pyjama set of width ε needed to cover the plane.

Equations

• Green41.minCopies ε = sInf (Green41.coveringCopies ε)

theorem Green41.minCopies_set_nonempty (ε : ℝ) (hε : 0 < ε) : (coveringCopies ε).Nonempty

[Ma15] proved that for any $\varepsilon > 0$, finitely many rotations of the pyjama set of width $\varepsilon$ cover the plane. This implies that the set we are taking the infimum over in minCopies is non-empty.

theorem Green41.green_41 : ∃ C > 0, ∃ ε₀ > 0, ∀ ε ∈ Set.Ioc 0 ε₀, have ans := sorry; ↑(minCopies ε) ≤ ans ∧ ans < Real.exp (Real.exp (Real.exp (ε ^ (-C))))

How many rotated (about the origin) copies of the 'pyjama set' $\\{(x, y) \in \mathbb{R}^2 : \text{dist}(x, \mathbb{Z}) \leq \varepsilon\\}$ are needed to cover $\mathbb{R}^2$?

In particular, can one find a better bound than the best-known bound from [KrLe25]?

theorem Green41.green_41.variants.exists_better_bound : True ↔ ∃ C > 0, ∃ ε₀ > 0, ∀ ε ∈ Set.Ioc 0 ε₀, ∃ (ans : ℝ), ↑(minCopies ε) ≤ ans ∧ ans < Real.exp (Real.exp (Real.exp (ε ^ (-C))))

Is there a better bound than the best-known bound from [KrLe25]? This is an existential version of the main problem that does not require providing the bound explicitly.

theorem Green41.green_41.variants.polynomial_bound : True ↔ ∃ (C : ℝ), ∃ ε₀ > 0, ∀ ε ∈ Set.Ioc 0 ε₀, ↑(minCopies ε) ≤ ε ^ (-C)

Is $\varepsilon^{-C}$ rotations enough?

theorem Green41.green_41.variants.kravitz_leng : ∃ (C : ℝ), ∃ ε₀ > 0, ∀ ε ∈ Set.Ioc 0 ε₀, ↑(minCopies ε) ≤ Real.exp (Real.exp (Real.exp (ε ^ (-C))))

[KrLe25] have established the first quantitative bound, showing via an analysis of [Ma15]'s method that $\exp\exp\exp(\varepsilon^{-C})$ rotations suffice.