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
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 : ℝ)
WantedExt/Combinatorics/SubsetSumConcentrationErdosProblem362Wanted.lean:38
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
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
WantedExt/Combinatorics/SubsetSumConcentrationErdosProblem362Wanted.lean:45
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
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.