Erdős problem 52 · problems.science

Let $A$ be a finite set of integers. Is it true that for every $\epsilon>0$ $\max( \lvert A+A\rvert,\lvert AA\rvert)\gg_\epsilon \lvert A\rvert^{2-\epsilon}?$

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

52.lean

Retained formal statement1 of 1

Let $A$ be a finite set of integers. Is it true that for every $\epsilon>0$ $\max( \lvert A+A\rvert,\lvert AA\rvert)\gg_\epsilon \lvert A\rvert^{2-\epsilon}?$

FormalConjectures/ErdosProblems/52.leanErdos52.erdos_521 lineExact file

1True ↔ ∀ (ε : ℝ), 0 < ε → ε < 1 → ∃ C, 0 < C ∧ ∀ (A : Finset ℤ), max ↑(A + A).card ↑(A * A).card ≥ C * ↑A.card ^ (2 - ε)

OpenStatement only, no proof

Sources

Search problems.science