Erdős problem 481
Let such that . For any finite sequence of (not necessarily distinct) integers let denote the sequence of length given by Prove that, if and , then there must be some with repeated elements.
Sources
FormalConjectures/ErdosProblems/
481.lean
Retained formal statement
Let such that . For any finite sequence of (not necessarily distinct) integers let denote the sequence of length given by Prove that, if and , then there must be some with repeated elements.
This is true. This appears to have first been shown by Klarner [Kl82], with a generalisation given by Kolpakov and Talambutsa [KoTa22]. Essentially the same proof was found independently by Barreto in the comment section.
∀ {r : ℕ} (a b : Fin r → ℕ), (∀ (i : Fin r), 0 < a i) → 1 < ∑ i, 1 / ↑(a i) → ∃ k, ¬((Erdos481.T a b)^[k] [1]).NodupSolvedStatement only, no proof