Erdős Problem 1

Reference: erdosproblems.com/1

@[reducible, inline]

abbrev IsSumDistinctSet (A : Finset ℕ) (N : ℕ) : Prop

A finite set of naturals $A$ is said to be a sum-distinct set for $N \in \mathbb{N}$ if $A\subseteq\{1, ..., N\}$ and the sums $\sum_{a\in S}a$ are distinct for all $S\subseteq A$

Equations

• IsSumDistinctSet A N = (A ⊆ Finset.Icc 1 N ∧ Function.Injective fun (x : { x : Finset ℕ // x ∈ A.powerset }) => match x with | ⟨S, property⟩ => S.sum id)

theorem erdos_1 : ∃ C > 0, ∀ (N : ℕ) (A : Finset ℕ), IsSumDistinctSet A N → N ≠ 0 → C * 2 ^ A.card < ↑N

If $A\subseteq\{1, ..., N\}$ with $|A| = n$ is such that the subset sums $\sum_{a\in S}a$ are distinct for all $S\subseteq A$ then $$ N \gg 2 ^ n. $$

theorem erdos_1.variants.weaker : ∃ C > 0, ∀ (N : ℕ) (A : Finset ℕ), IsSumDistinctSet A N → N ≠ 0 → C * 2 ^ A.card / ↑A.card < ↑N

The trivial lower bound is $N \gg 2^n / n$.

theorem erdos_1.variants.lb : ∃ (o : ℕ → ℝ) (_ : Filter.Tendsto o Filter.atTop (nhds 0)), ∀ (N : ℕ) (A : Finset ℕ), IsSumDistinctSet A N → (1 / 4 - o A.card) * 2 ^ A.card / √↑A.card ≤ ↑N

Erdős and Moser [Er56] proved $$ N \geq (\tfrac{1}{4} - o(1)) \frac{2^n}{\sqrt{n}}. $$

[Er56] Erdős, P., Problems and results in additive number theory. Colloque sur la Th'{E}orie des Nombres, Bruxelles, 1955 (1956), 127-137.

theorem erdos_1.variants.lb_strong : ∃ (o : ℕ → ℝ) (_ : Filter.Tendsto o Filter.atTop (nhds 0)), ∀ (N : ℕ) (A : Finset ℕ), IsSumDistinctSet A N → (√(2 / Real.pi) - o A.card) * 2 ^ A.card / √↑A.card ≤ ↑N

A number of improvements of the constant $\frac{1}{4}$ have been given, with the current record $\sqrt{2 / \pi}$ first provied in unpublished work of Elkies and Gleason.

@[reducible, inline]

abbrev IsSumDistinctRealSet (A : Finset ℝ) (N : ℕ) : Prop

A finite set of real numbers is said to be sum-distinct if all the subset sums differ by at least $1$.

Equations

• IsSumDistinctRealSet A N = (↑A ⊆ Set.Ioc 0 ↑N ∧ (↑A.powerset).Pairwise fun (S₁ S₂ : Finset ℝ) => 1 ≤ dist (S₁.sum id) (S₂.sum id))

theorem erdos_1.variants.real : ∃ C > 0, ∀ (N : ℕ) (A : Finset ℝ), IsSumDistinctRealSet A N → N ≠ 0 → C * 2 ^ A.card < ↑N

A generalisation of the problem to sets $A \subseteq (0, N]$ of real numbers, such that the subset sums all differ by at least $1$ is proposed in [Er73] and [ErGr80].

[Er73] Erdős, P., Problems and results on combinatorial number theory. A survey of combinatorial theory (Proc. Internat. Sympos., Colorado State Univ., Fort Collins, Colo., 1971) (1973), 117-138.

[ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).

theorem erdos_1.variants.least_N_3 : IsLeast {N : ℕ | ∃ (A : Finset ℕ), IsSumDistinctSet A N ∧ A.card = 3} 4

The minimal value of $N$ such that there exists a sum-distinct set with three elements is $4$.

https://oeis.org/A276661

theorem erdos_1.variants.least_N_5 : IsLeast {N : ℕ | ∃ (A : Finset ℕ), IsSumDistinctSet A N ∧ A.card = 5} 13

The minimal value of $N$ such that there exists a sum-distinct set with five elements is $13$.

https://oeis.org/A276661

theorem erdos_1.variants.least_N_9 : IsLeast {N : ℕ | ∃ (A : Finset ℕ), IsSumDistinctSet A N ∧ A.card = 9} 161

The minimal value of $N$ such that there exists a sum-distinct set with nine elements is $161$.

https://oeis.org/A276661