Erdős Problem 41

Reference: erdosproblems.com/41

def Erdos41.NtupleCondition {α : Type} [AddCommMonoid α] (A : Set α) (n : ℕ) : Prop

For a given set A, the n-tuple sums a₁ + ... + aₙ are all distinct for a₁, ..., aₙ in A (aside from the trivial coincidences).

Equations

• Erdos41.NtupleCondition A n = ∀ (I J : Finset α), ↑I ⊆ A ∧ ↑J ⊆ A ∧ I.card = n ∧ J.card = n ∧ ∑ i ∈ I, i = ∑ j ∈ J, j → I = J

theorem Erdos41.erdos_41 (A : Set ℕ) (h_triple : NtupleCondition A 3) (h_infinite : A.Infinite) : Filter.liminf (fun (N : ℕ) => ↑(A.interIcc 1 N).ncard / ↑N ^ (1 / 3)) Filter.atTop = 0

Let A ⊆ ℕ be an infinite set such that the triple sums a + b + c are all distinct for a, b, c in A (aside from the trivial coincidences). Is it true that liminf n → ∞ |A ∩ {1, …, N}| / N^(1/3) = 0?

theorem Erdos41.erdos_41_i (A : Set ℕ) (h_pair : NtupleCondition A 2) (h_infinite : A.Infinite) : Filter.liminf (fun (N : ℕ) => ↑(A.interIcc 1 N).ncard / √↑N) Filter.atTop = 0

Erdős proved the following pairwise version. Let A ⊆ ℕ be an infinite set such that the pairwise sums a + b are all distinct for a, b in A (aside from the trivial coincidences). Is it true that liminf n → ∞ |A ∩ {1, …, N}| / N^(1/2) = 0?