/-
Copyright 2025 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtilErdős Problem 340
Reference: erdosproblems.com/340
open Filter Finsetopen scoped Real Pointwisenamespace Erdos340@[category test, AMS 5]
theorem greedySidon_go_singleton_two : (greedySidon.go {1} (⊢ IsSidon ↑{1} All goals completed! 🐙) 2).val = 2 := ⊢ ↑(greedySidon.go {1} ⋯ 2) = 2
All goals completed! 🐙@[category test, AMS 5]
theorem greedySidon_go_pair_three : (greedySidon.go {1, 2} (⊢ IsSidon ↑{1, 2} All goals completed! 🐙) 3).val = 4 := ⊢ ↑(greedySidon.go {1, 2} ⋯ 3) = 4
All goals completed! 🐙@[category test, AMS 5]
theorem greedySidon_zero : greedySidon 0 = 1 := rfl@[category test, AMS 5]
theorem greedySidon_one : greedySidon 1 = 2 := ⊢ greedySidon 1 = 2
All goals completed! 🐙@[category test, AMS 5]
theorem greedySidon_two : greedySidon 2 = 4 := ⊢ greedySidon 2 = 4
All goals completed! 🐙@[category test, AMS 5]
theorem greedySidon_three : greedySidon 3 = 8 := ⊢ greedySidon 3 = 8
All goals completed! 🐙@[category test, AMS 5]
theorem greedySidon_four : greedySidon 4 = 13 := ⊢ greedySidon 4 = 13
All goals completed! 🐙@[category test, AMS 5]
theorem greedySidon_five : greedySidon 5 = 21 := ⊢ greedySidon 5 = 21
All goals completed! 🐙@[category test, AMS 5]
theorem greedySidon_ten : greedySidon 10 = 97 := ⊢ greedySidon 10 = 97
All goals completed! 🐙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$?
@[category research open, AMS 5]
theorem erdos_340 (ε : ℝ) (hε : ε > 0) :
(fun n : ℕ ↦ √n / n ^ ε) =O[atTop]
fun n : ℕ ↦ ((Set.range greedySidon ∩ Set.Icc 1 n).ncard : ℝ) := ε:ℝhε:ε > 0⊢ (fun n ↦ √↑n / ↑n ^ ε) =O[atTop] fun n ↦ ↑(Set.range greedySidon ∩ Set.Icc 1 n).ncard
All goals completed! 🐙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$?
@[category research open, AMS 5]
theorem erdos_340.variants.isTheta (ε : ℝ) (hε : ε > 0) :
(fun n : ℕ ↦ ((Set.range greedySidon ∩ Set.Icc 1 n).ncard : ℝ)) =Θ[atTop]
(answer(sorry) : ℕ → ℝ) := ε:ℝhε:ε > 0⊢ (fun n ↦ ↑(Set.range greedySidon ∩ Set.Icc 1 n).ncard) =Θ[atTop] sorry
All goals completed! 🐙It is trivial that this sequence grows at least like $\gg N^{1/3}$.
@[category textbook, AMS 5]
theorem erdos_340.variants.third (ε : ℝ) (hε : ε > 0) :
(fun n : ℕ ↦ (n : ℝ) ^ ((1 : ℝ) / 3)) =O[atTop]
fun n : ℕ ↦ ((Set.range greedySidon ∩ Set.Icc 1 n).ncard : ℝ) := ε:ℝhε:ε > 0⊢ (fun n ↦ ↑n ^ (1 / 3)) =O[atTop] fun n ↦ ↑(Set.range greedySidon ∩ Set.Icc 1 n).ncard
All goals completed! 🐙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).
@[category research open, AMS 5]
theorem erdos_340.variants.sub_hasPosDensity :
Set.HasPosDensity (Set.range greedySidon - Set.range greedySidon) := ⊢ (Set.range greedySidon - Set.range greedySidon).HasPosDensity
All goals completed! 🐙Erdős and Graham [ErGr80] also asked about the difference set $A - A$ and whether this contains $22$, which it does.
[ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).
h:22 = greedySidon 14 - greedySidon 13⊢ greedySidon 14 - greedySidon 13 ∈ Set.range greedySidon - Set.range greedySidon
All goals completed! 🐙The smallest integer which is unknown to be in $A - A$ is $33$.
@[category research open, AMS 5]
theorem erdos_340.variants._33_mem_sub : answer(sorry) ↔
33 ∈ Set.range greedySidon - Set.range greedySidon := ⊢ True ↔ 33 ∈ Set.range greedySidon - Set.range greedySidon
All goals completed! 🐙It may be true that all or almost all integers are in $A - A$.
@[category research open, AMS 5]
theorem erdos_340.variants.cofinite_sub : answer(sorry) ↔
∀ᶠ n in cofinite, n ∈ Set.range greedySidon - Set.range greedySidon := ⊢ True ↔ ∀ᶠ (n : ℕ) in cofinite, n ∈ Set.range greedySidon - Set.range greedySidon
All goals completed! 🐙It may be true that all or almost all integers are in $A - A$.
@[category research open, AMS 5]
theorem erdos_340.variants.co_density_zero_sub : answer(sorry) ↔
∃ S : Set ℕ, S.HasDensity 0 ∧ ∀ n ∈ Sᶜ, n ∈ Set.range greedySidon - Set.range greedySidon := ⊢ True ↔ ∃ S, S.HasDensity 0 ∧ ∀ n ∈ Sᶜ, n ∈ Set.range greedySidon - Set.range greedySidon
All goals completed! 🐙end Erdos340