Erdős Problem 757

References:

• erdosproblems.com/757
• [GyLe95] Gyárfás, András and Lehel, Jenő, Linear sets with five distinct differences among any four elements. J. Combin. Theory Ser. B (1995), 108-118.

def Erdos757.IsAdmissible (c : ℝ) : Prop

We say that c is admissible if for any finit set A such that for any subset B of size 4, (B - B).card = 11, there exists a Sidon subset S of size at least c * A.ncard.

Equations

• Erdos757.IsAdmissible c = ∀ {A : Set ℝ}, A.Finite → (∀ B ⊆ A, B.ncard = 4 → (B - B).ncard = 11) → ∃ S ⊆ A, IsSidon S ∧ c * ↑A.ncard ≤ ↑S.ncard

theorem Erdos757.erdos_757 {A : Set ℝ} : sorry = sSup {c : ℝ | IsAdmissible c}

What is the supremum of the set of admissible numbers?

theorem Erdos757.erdos_757.lowerBound {A : Set ℝ} : 1 / 2 < sSup {c : ℝ | IsAdmissible c}

The supremum is strictly larger than 1 / 2, which is proved in [GyLe95].

theorem Erdos757.erdos_757.upperBound {A : Set ℝ} : sSup {c : ℝ | IsAdmissible c} < 3 / 5

In [GyLe95], the authors also prove that the supremum is smaller than 3 / 5.