Erdős problem 818 · problems.science

Let $A$ be a finite set of integers such that $\lvert A+A\rvert \ll \lvert A\rvert$ . Is it true that $\lvert AA\rvert \gg \frac{\lvert A\rvert^2}{(\log \lvert A\rvert)^C}$ for some constant $C>0$ ?

Sources

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

2 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

818.lean

Retained formal statement2 of 2

This was proved by Solymosi [So09d], in the strong form $\lvert AA\rvert \gg \frac{\lvert A\rvert^2}{\log \lvert A\rvert}.$

FormalConjectures/ErdosProblems/818.leanErdos818.erdos_818.variants.solymosi5 linesExact file

1∀ (K : ℝ),2  0 < K →3    ∃ c,4      0 < c ∧5        ∀ (A : Finset ℤ), 2 ≤ A.card → ↑(A + A).card ≤ K * ↑A.card → c * ↑A.card ^ 2 / Real.log ↑A.card ≤ ↑(A * A).card

SolvedStatement only, no proof

Sources

Search problems.science