Erdős problem 328
Suppose and is such that for all . Can be partitioned into many subsets (where depends only on ) such that for all and ?
Sources
FormalConjectures/ErdosProblems/
328.lean
Suppose and is such that for all . Can be partitioned into many subsets (where depends only on ) such that for all and ?
The answer is no. Asked by Erdős and Newman. Nešetřil and Rödl [NeRo85] have shown the answer is no for all (even if is also allowed to depend on ).
Erdős [Er80e] had previously shown the answer is no for and infinitely many other values of .
See also [774].
The linked proof writes the representation function as Set.ncard {p : ℕ × ℕ | p.1 ∈ A ∧ p.2 ∈ A ∧ p.1 + p.2 = n}, which counts the same ordered pairs as sumRep, and states the partition condition as a named definition with the same two conjuncts used below. Its ∃ t additionally carries 1 ≤ t, which costs nothing: t = 0 forces A = ∅, and A = {1} has all representation counts at most C for C ≥ 1.
False ↔ ∀ (C : ℕ), 0 < C → ∃ t, ∀ (A : Set ℕ), (∀ (n : ℕ), AdditiveCombinatorics.sumRep A n ≤ C) → ∃ P, ⋃ i, P i = A ∧ Set.univ.PairwiseDisjoint P ∧ ∀ (i : Fin t) (n : ℕ), AdditiveCombinatorics.sumRep (P i) n < C