Erdős Problem 254

References:

• erdosproblems.com/254
• [Ca60] Cassels, J. W. S., On the representation of integers as the sums of distinct summands taken from a fixed set. Acta Sci. Math. (Szeged) (1960), 111-124.

def Erdos254.IsSumOfDistinct (A : Set ℕ) (n : ℕ) : Prop

An integer n can be written as a sum of distinct elements of A.

Equations

• Erdos254.IsSumOfDistinct A n = ∃ (S : Finset ℕ), ↑S ⊆ A ∧ ∑ x ∈ S, x = n

theorem Erdos254.erdos_254 (A : Set ℕ) : (Filter.Tendsto (fun (x : ℕ) => (A ∩ Set.Icc 1 (2 * x)).ncard - (A ∩ Set.Icc 1 x).ncard) Filter.atTop Filter.atTop ∧ ∀ (θ : ℝ), 0 < θ → θ < 1 → ¬Summable fun (n : ↑A) => distToNearestInt (θ * ↑↑n)) → ∀ᶠ (m : ℕ) in Filter.atTop, IsSumOfDistinct A m

Let $A\subseteq \mathbb{N}$ be such that $\lvert A\cap [1,2x]\rvert -\lvert A\cap [1,x]\rvert \to \infty\textrm{ as }x\to \infty$ and $\sum_{n\in A} \{ \theta n\}=\infty$ for every $\theta\in (0,1)$, where $\{x\}$ is the distance of $x$ from the nearest integer. Then every sufficiently large integer is the sum of distinct elements of $A$.

theorem Erdos254.erdos_254.variants.cassels (A : Set ℕ) : (Filter.Tendsto (fun (x : ℕ) => (↑(A ∩ Set.Icc 1 (2 * x)).ncard - ↑(A ∩ Set.Icc 1 x).ncard) / Real.log (Real.log ↑x)) Filter.atTop Filter.atTop ∧ ∀ (θ : ℝ), 0 < θ → θ < 1 → ¬Summable fun (n : ↑A) => distToNearestInt (θ * ↑↑n) ^ 2) → ∀ᶠ (m : ℕ) in Filter.atTop, IsSumOfDistinct A m

Cassels [Ca60] proved this under the alternative hypotheses $\lim \frac{\lvert A\cap [1,2x]\rvert -\lvert A\cap [1,x]\rvert}{\log\log x}=\infty$ and $\sum_{n\in A} \{ \theta n\}^2=\infty$ for every $\theta\in (0,1)$.