Sets determined by their k-sums

DefinitionMultiset of \(k\)-sums#✓fully proved

For a finite set \(A \subseteq \mathbb{C}\) and a natural number \(k\), \(A_k\) is the multiset of the sums \(\sum_{z \in S} z\) over the \(k\)-element subsets \(S\) of \(A\), that is, of the sums of \(k\) distinct elements of \(A\), each subset counted once.

noncomputable def kSumMultiset (A : Finset ℂ) (k : ℕ) : Multiset ℂ :=
  (A.powersetCard k).val.map fun s => ∑ z ∈ s, z

Used by 1

Used byErdős Problem 494 for large sets

DefinitionErdős Problem 494 for large sets#✓fully proved

For a finite set \(A \subseteq \mathbb{C}\) and a natural number \(k\), let \(A_k\) be the multiset of the sums of the \(k\)-element subsets of \(A\). This is the statement that for every natural number \(k \ge 3\) there is a natural number \(n_0\) such that any two finite sets \(A, B \subseteq \mathbb{C}\) with \(|A| = |B| \ge n_0\) and \(A_k = B_k\) are equal.

This is the question of Selfridge and Straus with \(|A|\) large in terms of \(k\).

def kSumMultisetDeterminesLargeSet : Prop :=
  ∀ k : ℕ, 3 ≤ k → ∃ n₀ : ℕ, ∀ A B : Finset ℂ, A.card = B.card → n₀ ≤ A.card →
    kSumMultiset A k = kSumMultiset B k → A = B

Uses 1 · Used by 1

Statement usesMultiset of \(k\)-sums

Used byLarge sets of complex numbers are determined by their \(k\)-sums

TheoremLarge sets of complex numbers are determined by their \(k\)-sums#●ready to prove

For a finite set \(A \subseteq \mathbb{C}\) and a natural number \(k\), let \(A_k\) be the multiset of the sums \(\sum_{z \in S} z\) over the \(k\)-element subsets \(S\) of \(A\). For every natural number \(k \ge 3\) there is a natural number \(n_0\) such that any two finite sets \(A, B \subseteq \mathbb{C}\) with \(|A| = |B| \ge n_0\) and \(A_k = B_k\) are equal.

Gordon, Fraenkel and Straus proved (Section 4) that for \(s > 2\) two \(n\)-element multisets in a torsion-free abelian group with the same multiset of \(s\)-sums are equal for all but finitely many \(n\); \(\mathbb{C}\) is torsion-free and sets are multisets.

public theorem_wanted kSumMultisetDeterminesLargeSet_holds : kSumMultisetDeterminesLargeSet

Sources

• T. F. Bloom, Erdős Problems, Problem #494, https://www.erdosproblems.com/494 (status PROVED); resolution: B. Gordon, A. S. Fraenkel and E. G. Straus, On the determination of sets by the sets of sums of a certain order, Pacific J. Math. 12 (1962), 187-196, Section 4: for s > 2, F_s(n) = 1 for all but finitely many n, for finite multisets in any torsion-free abelian group, https://doi.org/10.2140/pjm.1962.12.187.

Uses 1

Statement usesErdős Problem 494 for large sets

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.