Erdős Problem 340

Reference: erdosproblems.com/340

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

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

theorem Erdos340.greedySidon_zero : Finset.greedySidon 0 = 1

theorem Erdos340.greedySidon_one : Finset.greedySidon 1 = 2

theorem Erdos340.greedySidon_two : Finset.greedySidon 2 = 4

theorem Erdos340.greedySidon_three : Finset.greedySidon 3 = 8

theorem Erdos340.greedySidon_four : Finset.greedySidon 4 = 13

theorem Erdos340.greedySidon_five : Finset.greedySidon 5 = 21

theorem Erdos340.greedySidon_ten : Finset.greedySidon 10 = 97

theorem Erdos340.erdos_340 (ε : ℝ) (hε : ε > 0) : (fun (n : ℕ) => √↑n / ↑n ^ ε) =O[Filter.atTop] fun (n : ℕ) => ↑(Set.range Finset.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 Erdos340.erdos_340.variants.isTheta (ε : ℝ) (hε : ε > 0) : (fun (n : ℕ) => ↑(Set.range Finset.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 Erdos340.erdos_340.variants.third (ε : ℝ) (hε : ε > 0) : (fun (n : ℕ) => ↑n ^ (1 / 3)) =O[Filter.atTop] fun (n : ℕ) => ↑(Set.range Finset.greedySidon ∩ Set.Icc 1 n).ncard

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

theorem Erdos340.erdos_340.variants.sub_hasPosDensity : (Set.range Finset.greedySidon - Set.range Finset.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 Erdos340.erdos_340.variants.cofinite_sub : sorry ↔ ∀ᶠ (n : ℕ) in Filter.cofinite, n ∈ Set.range Finset.greedySidon - Set.range Finset.greedySidon

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

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

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