Erdős problem 1193
Let and let be a non-decreasing function of which is always .
Sources
FormalConjectures/ErdosProblems/
1193.lean
Retained formal statement
Let and let be a non-decreasing function of which is always .
Is the upper density of always for some constant ?
The answer is trivially no to both questions: indeed if (assuming ) then for all . Presumably Erdős had some additional restrictions on either or in mind, but these are not recorded in [Er80].
False ↔ ∃ c < 1, ∀ (A : Set ℕ) (g : ℕ → ℕ), Monotone g → (∀ (n : ℕ), 0 < g n) → {n | AdditiveCombinatorics.sumRep A n = g n}.upperDensity < cSolvedStatement only, no proof