Erdős problem 818

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

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

818.lean

Retained formal statement1 of 2

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$ ?

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

FormalConjectures/ErdosProblems/818.leanErdos818.erdos_8189 linesExact file

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

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.