Documentation

FormalConjectures.GreensOpenProblems.«31»

Ben Green's Open Problem 31 #

Write $F(N)$ for the largest Sidon subset of $[N]$. Improve, at least for infinitely many $N$, the bounds $N^{1/2} + O(1) \le F(N) \le N^{1/2} + N^{1/4} + O(1)$.

Note: the upper bound was improved to $N^{1/2} + 0.98183 N^{1/4} + O(1)$ in [CHO25].

Related to Erdős Problem 30.

References:

source
noncomputable def Green31.F (N : ℕ) :
ℝ

Let $F(N)$ be the largest Sidon subset of $[N]$.

Equations
Instances For
    source
    theorem Green31.green_31.lower :
    have ans := sorry; Filter.Tendsto (fun (N : ℕ) => ans N - √↑N) Filter.atTop Filter.atTop ∧ ∃ᶠ (N : ℕ) in Filter.atTop, ans N ≤ F N

    Can we improve the lower bound $N^{1/2} + O(1)$, at least for infinitely many $N$?

    source
    theorem Green31.green_31.variants.lower_eventually :
    have ans := sorry; Filter.Tendsto (fun (N : ℕ) => ans N - √↑N) Filter.atTop Filter.atTop ∧ ∀ᶠ (N : ℕ) in Filter.atTop, ans N ≤ F N

    Can we improve the lower bound $N^{1/2} + O(1)$, for all sufficiently large $N$?

    source
    theorem Green31.green_31.upper :
    have ans := sorry; (∃ᶠ (N : ℕ) in Filter.atTop, F N ≤ ans N) ∧ ∃ c < 0.98183, ∃ (C : ℝ), ∀ᶠ (N : ℕ) in Filter.atTop, ans N - √↑N ≤ c * ↑N ^ 4⁻¹ + C

    Can we improve the upper bound $N^{1/2} + 0.98183 N^{1/4} + O(1)$ [CHO25], at least for infinitely many $N$?

    source
    theorem Green31.green_31.variants.upper_eventually :
    have ans := sorry; (∀ᶠ (N : ℕ) in Filter.atTop, F N ≤ ans N) ∧ ∃ c < 0.98183, ∃ (C : ℝ), ∀ᶠ (N : ℕ) in Filter.atTop, ans N - √↑N ≤ c * ↑N ^ 4⁻¹ + C

    Can we improve the upper bound $N^{1/2} + 0.98183 N^{1/4} + O(1)$ [CHO25], for all sufficiently large $N$?

    source
    theorem Green31.green_31.variants.upper_li69 :
    ∃ (C : ℝ), ∀ᶠ (N : ℕ) in Filter.atTop, F N ≤ √↑N + ↑N ^ 4⁻¹ + C

    [Li69] proved $F(n) \le n^{1/2} + n^{1/4} + O(1)$.

    source
    theorem Green31.green_31.variants.upper_bfr23 :
    ∀ᶠ (N : ℕ) in Filter.atTop, F N ≤ √↑N + 0.998 * ↑N ^ 4⁻¹

    [BFR23] obtained a small improvement, getting an upper bound of $F(N) \le N^{1/2} + 0.998 N^{1/4}$ for large $N$.

    source
    theorem Green31.green_31.variants.upper_cho25 :
    ∃ (C : ℝ), ∀ᶠ (N : ℕ) in Filter.atTop, F N ≤ √↑N + 0.98183 * ↑N ^ 4⁻¹ + C

    The upper bound was further improved to $N^{1/2} + 0.98183 N^{1/4} + O(1)$ [CHO25].

    source
    theorem Green31.green_31.variants.zmod_p :
    True ↔ ∃ (S : (n : ℕ) → Finset (ZMod n)) (o : ℕ → ℝ), (o =o[Filter.atTop] fun (x : ℕ) => 1) ∧ (∀ (p : ℕ), Nat.Prime p → IsSidon ↑(S p)) ∧ ∀ (p : ℕ), Nat.Prime p → ↑(S p).card = (1 + o p) * √↑p

    It is not known whether or not there exists a Sidon subset of $\mathbb{Z}/p\mathbb{Z}$ of size $(1 + o(1))\sqrt{p}$, for all $p$ [Gr24].

    source
    theorem Green31.green_31.variants.abelian :
    True ↔ ∀ (G : Type) [inst : AddCommGroup G] [inst_1 : Fintype G], ∃ (S : Finset G), IsSidon ↑S ∧ 1e-2 * √↑(Fintype.card G) ≤ ↑S.card

    It is not known whether, if $G$ is an abelian group of size $n$, there always exists a Sidon subset of $G$ of size $0.01\sqrt{n}$ [Gr24].

    source
    theorem Green31.green_31.variants.sidon_01n :
    True ↔ ∃ (S : (n : ℕ) → Finset (Fin n → ZMod 2)), (∀ (n : ℕ), IsSidon ↑(S n)) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, (2 ^ n) ^ 0.51 ≤ ↑(S n).card

    Another very nice old problem is whether there is a Sidon subset of $\{0, 1\}^n$ of size $N^{0.51}$, where $N = 2^n$ [Gr24].

    source
    theorem Green31.green_31.variants.sidon_01n_clz01 :
    ∃ (C : ℝ), ∀ (n : ℕ) (S : Finset (Fin n → ZMod 2)), IsSidon ↑S → ↑S.card ≤ C * (2 ^ n) ^ 0.5753

    The best-known upper bound for a Sidon subset of $\{0, 1\}^n$ ($N = 2^n$) is $N^{0.5753}$ [CLZ01].