Erdős Problem 494

References:

• erdosproblems.com/494
• [SeSt58] Selfridge, J. L. and Straus, E., On the determination of numbers by their sums of a fixed order. Pacific Journal of Math. (1958), 847-856.
• [Er61] Erdős, Paul, Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. (1961), 221-254.
• [GFS62] Gordon, B. and Fraenkel, A. S. and Straus, E. G., On the determination of sets by the sets of sums of a certain order. Pacific J. Math. (1962), 187--196.

noncomputable def Erdos494.sumMultiset (A : Finset ℂ) (k : ℕ) : Multiset ℂ

For a finite set $A \subset \mathbb{C}$ and $k \ge 1$, define $A_k$ as the multiset consisting of all sums of $k$ distinct elements of $A$.

Equations

• Erdos494.sumMultiset A k = Multiset.map (fun (s : Finset ℂ) => s.sum id) (Finset.powersetCard k A).val

def Erdos494.Erdos494Unique (k card : ℕ) : Prop

Equations

• Erdos494.Erdos494Unique k card = ∀ (A B : Finset ℂ), A.card = card → B.card = card → Erdos494.sumMultiset A k = Erdos494.sumMultiset B k → A = B

theorem Erdos494.erdos_494.variant.k_eq_2_card_not_pow_two (card : ℕ) : (∀ (l : ℕ), card ≠ 2 ^ l) → Erdos494Unique 2 card

Selfridge and Straus [SeSt58] showed that the conjecture is true when $k = 2$ and $|A| \ne 2^l$ for $l \ge 0$. They also gave counterexamples when $k = 2$ and $|A| = 2^l$.

theorem Erdos494.erdos_494.variant.k_eq_2_card_pow_two (card : ℕ) : (∃ (l : ℕ), card = 2 ^ l) → ¬Erdos494Unique 2 card

theorem Erdos494.erdos_494.variant.k_eq_3_card_gt_6 (card : ℕ) : card > 6 → Erdos494Unique 3 card

Selfridge and Straus [SeSt58] also showed that the conjecture is true when

1. $k = 3$ and $|A| > 6$ or
2. $k = 4$ and $|A| > 12$. More generally, they proved that $A$ is determined by $A_k$ (and $|A|$) if $|A|$ is divisible by a prime greater than $k$.

theorem Erdos494.erdos_494.variant.k_eq_4_card_gt_12 (card : ℕ) : card > 12 → Erdos494Unique 4 card

theorem Erdos494.erdos_494.variant.card_divisible_by_prime_gt_k (k card p : ℕ) : Nat.Prime p ∧ k < p ∧ p ∣ card → Erdos494Unique k card

theorem Erdos494.erdos_494.variant.k_eq_card (k : ℕ) : k > 2 → ¬Erdos494Unique k k

Kruyt noted that the conjecture fails when $|A| = k$, by rotating $A$ around an appropriate point.

theorem Erdos494.erdos_494.variant.card_eq_2k (k : ℕ) : k > 2 → ¬Erdos494Unique k (2 * k)

Similarly, Tao noted that the conjecture fails when $|A| = 2k$, by taking $A$ to be a set of the total sum 0 and considering $-A$.

theorem Erdos494.erdos_494.variant.gordon_fraenkel_straus (k : ℕ) : k > 2 → ∀ᶠ (card : ℕ) in Filter.atTop, Erdos494Unique k card

Gordon, Fraenkel, and Straus [GRS62] proved that the claim is true for all $k > 2$ when $|A|$ is sufficiently large.

noncomputable def Erdos494.prodMultiset (A : Finset ℂ) (k : ℕ) : Multiset ℂ

A version in [Er61] by Erdős is product instead of sum, which is false. Counterexample (by Steinerberger): consider $k = 3$ and let $A = \{1, \zeta_6, \zeta_6^2, \zeta_6^4\}$ and $B = \{1, \zeta_6^2, \zeta_6^3, \zeta_6^4\}$.

Equations

• Erdos494.prodMultiset A k = Multiset.map (fun (s : Finset ℂ) => s.prod id) (Finset.powersetCard k A).val

theorem Erdos494.erdos_494.variant.product : ∃ (A : Finset ℂ) (B : Finset ℂ), A.card = B.card ∧ prodMultiset A 3 = prodMultiset B 3 ∧ A ≠ B