Concentration of subset sums

DefinitionErdős Problem 362: subsets with a given sum#✓fully proved

There is a real constant \(C\) such that for every nonempty finite set \(A \subseteq \mathbb{N}\) with \(N\) elements and every \(t \in \mathbb{N}\), the number of subsets \(S \subseteq A\) with \(\sum_{n \in S} n = t\) is at most \(C \cdot 2^N / N^{3/2}\).

def subsetSumCountBound : Prop :=
  ∃ C : ℝ, ∀ (A : Finset ℕ) (t : ℕ), A.Nonempty →
    ((A.powerset.filter fun S => ∑ n ∈ S, n = t).card : ℝ) ≤
      C * 2 ^ A.card / (A.card : ℝ) ^ (3 / 2 : ℝ)
Used by 1

DefinitionErdős Problem 362: subsets of a given size with a given sum#✓fully proved

There is a real constant \(C\) such that for every nonempty finite set \(A \subseteq \mathbb{N}\) with \(N\) elements and all \(l, t \in \mathbb{N}\), the number of \(l\)-element subsets \(S \subseteq A\) with \(\sum_{n \in S} n = t\) is at most \(C \cdot 2^N / N^2\).

def fixedSizeSubsetSumCountBound : Prop :=
  ∃ C : ℝ, ∀ (A : Finset ℕ) (l t : ℕ), A.Nonempty →
    (((A.powersetCard l).filter fun S => ∑ n ∈ S, n = t).card : ℝ) ≤
      C * 2 ^ A.card / (A.card : ℝ) ^ 2
Used by 1

TheoremSárközy–Szemerédi bound on subsets with a given sum#●ready to prove

There is a real constant \(C\) such that for every nonempty finite set \(A \subseteq \mathbb{N}\) with \(N\) elements and every \(t \in \mathbb{N}\), the number of subsets \(S \subseteq A\) with \(\sum_{n \in S} n = t\) is at most \(C \cdot 2^N / N^{3/2}\).

Sárközy and Szemerédi removed the factor \((\log N)^{3/2}\) from the Erdős–Moser bound; Stanley later found the extremal sets.

public theorem_wanted subsetSumCountBound_holds : subsetSumCountBound
Sources
  • T. F. Bloom, Erdős Problems, Problem #362, https://www.erdosproblems.com/362 (status PROVED (LEAN)); resolution: A. Sárközy and E. Szemerédi, Über ein Problem von Erdős und Moser, Acta Arith. (1965), 205-208; G. Halász, Estimates for the concentration function of combinatorial number theory and probability, Period. Math. Hungar. (1977), 197-211, erdosproblems.com/362: the first question answered by Sárközy and Szemerédi, the second by Halász as a consequence of a multi-dimensional result.
Uses 1

TheoremHalász's bound on subsets of a given size with a given sum#●ready to prove

There is a real constant \(C\) such that for every nonempty finite set \(A \subseteq \mathbb{N}\) with \(N\) elements and all \(l, t \in \mathbb{N}\), the number of \(l\)-element subsets \(S \subseteq A\) with \(\sum_{n \in S} n = t\) is at most \(C \cdot 2^N / N^2\).

Halász proved this as a consequence of a multi-dimensional concentration estimate.

public theorem_wanted fixedSizeSubsetSumCountBound_holds : fixedSizeSubsetSumCountBound
Sources
  • T. F. Bloom, Erdős Problems, Problem #362, https://www.erdosproblems.com/362 (status PROVED (LEAN)); resolution: A. Sárközy and E. Szemerédi, Über ein Problem von Erdős und Moser, Acta Arith. (1965), 205-208; G. Halász, Estimates for the concentration function of combinatorial number theory and probability, Period. Math. Hungar. (1977), 197-211, erdosproblems.com/362: the first question answered by Sárközy and Szemerédi, the second by Halász as a consequence of a multi-dimensional result.
Uses 1
2 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.