Erdős Problem 340

Reference: erdosproblems.com/340

theorem greedySidon_go_singleton_two : ↑(greedySidon.go✝ {1} ⋯ 2) = 2

theorem greedySidon_go_pair_three : ↑(greedySidon.go✝ {1, 2} ⋯ 3) = 4

def greedySidon (n : ℕ) : ℕ

greedySidon is the sequence obtained by the initial set $\{1\}$ and iteratively obtaining then next smallest integer that preserves the Sidon property of the set. This gives the sequence 1, 2, 4, 8, 13, 21, 31, ....

Equations

• greedySidon n = (greedySidon.aux✝ n).2

theorem greedySidon_zero : greedySidon 0 = 1

theorem greedySidon_one : greedySidon 1 = 2

theorem greedySidon_two : greedySidon 2 = 4

theorem greedySidon_three : greedySidon 3 = 8

theorem greedySidon_four : greedySidon 4 = 13

theorem greedySidon_five : greedySidon 5 = 21

theorem greedySidon_ten : greedySidon 10 = 97

theorem erdos_340 (ε : ℝ) (hε : ε > 0) : (fun (n : ℕ) => √↑n / ↑n ^ ε) =O[Filter.atTop] fun (n : ℕ) => ↑(Set.range greedySidon ∩ Set.Icc 1 n).ncard

Let $A = \{1, 2, 4, 8, 13, 21, 31, 45, 66, 81, 97, \ldots\}$ be the greedy Sidon sequence: we begin with $1$ and iteratively include the next smallest integer that preserves the Sidon property (i.e. there are no non-trivial solutions to $a + b = c + d$). What is the order of growth of $A$? Is it true that $| A \cap\{1, \ldots, N\}| \gg N^{1/2−\varepsilon}$ for all $\varepsilon > 0$ and large $N$?

theorem erdos_340.variants.isTheta (ε : ℝ) (hε : ε > 0) : (fun (n : ℕ) => ↑(Set.range greedySidon ∩ Set.Icc 1 n).ncard) =Θ[Filter.atTop] sorry

Let $A = \{1, 2, 4, 8, 13, 21, 31, 45, 66, 81, 97, \ldots\}$ be the greedy Sidon sequence: we begin with $1$ and iteratively include the next smallest integer that preserves the Sidon property (i.e. there are no non-trivial solutions to $a + b = c + d$). What is the order of growth of $A$? Is it true that $| A \cap\{1, \ldots, N\}| \gg N^{1/2−\varepsilon}$ for all $\varepsilon > 0$ and large $N$?

theorem erdos_340.variants.third (ε : ℝ) (hε : ε > 0) : (fun (n : ℕ) => ↑n ^ (1 / 3)) =O[Filter.atTop] fun (n : ℕ) => ↑(Set.range greedySidon ∩ Set.Icc 1 n).ncard

It is trivial that this sequence grows at least like $\gg N^{1/3}$.

theorem erdos_340.variants.sub_hasPosDensity : (Set.range greedySidon - Set.range greedySidon).HasPosDensity

Erdős and Graham [ErGr80] also asked about the difference set $A - A$ and whether this has positive density.

[ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).

theorem erdos_340.variants.cofinite_sub : (∀ᶠ (n : ℕ) in Filter.cofinite, n ∈ Set.range greedySidon - Set.range greedySidon) ↔ sorry

It may be true that all or almost all integers are in $A - A$.

theorem erdos_340.variants.co_density_zero_sub : (∃ (S : Set ℕ), S.HasDensity 0 ∧ ∀ n ∈ Sᶜ, n ∈ Set.range greedySidon - Set.range greedySidon) ↔ sorry

It may be true that all or almost all integers are in $A - A$.