Erdős Problem 253

Reference: erdosproblems.com/253

@[inline]

def Erdos253.RepresentsAPs (a : ℕ → ℤ) : Prop

The predicate that a : ℕ → ℤ is a strictly monotone sequence such that every infinite arithmetic progression contains infinitely many integers that are the sum of distinct $a_i$s.

Equations

• Erdos253.RepresentsAPs a = (StrictMono a ∧ ∀ (l : Set ℤ), l.IsAPOfLength ⊤ → (subsetSums (Set.range a) ∩ l).Infinite)

theorem Erdos253.erdos_253 : ¬∀ (a : ℕ → ℤ), RepresentsAPs a → Filter.Tendsto (fun (n : ℕ) => ↑(a (n + 1)) / ↑(a n)) Filter.atTop (nhds 1) → subsetSums (Set.range a) ∈ Filter.cofinite

Let $a_1 < a_2 < \dotsc$ be an infinite sequence of integers such that $\frac{a_{i+1}}{a_i} \to 1$. If every arithmetic progression contains infinitely many integers which are the sum of distinct $a_i$ then every sufficiently large integer is the sum of distinct $a_i$.