Erdős problem 178
Let be an infinite collection of infinite sets of integers, say . Does there exist some such that for all ?
Sources
FormalConjectures/ErdosProblems/
178.lean
Retained formal statement
Let be an infinite collection of infinite sets of integers, say . Does there exist some such that for all ?
Erdős remarks 'it seems certain that the answer is affirmative'. This was solved by Beck [Be81]. Recently Beck [Be17] proved that one can replace with for any .
True ↔ ∀ (a : ℕ → ℕ → ℕ), (∀ (i : ℕ), StrictMono (a i)) → ∃ f, (∀ (n : ℕ), f n = 1 ∨ f n = -1) ∧ ∀ (d : ℕ), ∃ C, ∀ (m i : ℕ), i < d → |∑ j ∈ Finset.range m, f (a i j)| ≤ ↑C