Skip to content

Erdős problem 1193

Let ANA\subset \mathbb{N} and let g(n)g(n) be a non-decreasing function of nn which is always >0>0.

Sources

Browse retained paths and inspect the exact material available for this Problem.

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1193.lean

Retained formal statement1 of 4

Let ANA\subset \mathbb{N} and let g(n)g(n) be a non-decreasing function of nn which is always >0>0.

Is the lower density of {n:1A1A(n)=g(n)}\{ n : 1_A\ast 1_A(n)=g(n)\} always 00?

The answer is trivially no to both questions: indeed if A=NA=\mathbb{N} (assuming 0N0\in\mathbb{N}) then 1A1A(n)=n+11_A\ast 1_A(n)=n+1 for all nn. Presumably Erdős had some additional restrictions on either gg or AA in mind, but these are not recorded in [Er80].

FormalConjectures/ErdosProblems/1193.leanErdos1193.erdos_1193.parts.i3 linesExact file
False  ∀ (A : Set ℕ) (g : ℕ → ℕ),    Monotone g → (∀ (n : ℕ), 0 < g n) → {n | AdditiveCombinatorics.sumRep A n = g n}.lowerDensity = 0
SolvedStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page