Erdős problem 512 · problems.science

Is it true that, if $A\subset \mathbb{Z}$ is a finite set of size $N$ , then $\int_0^1 \left\lvert \sum_{n\in A}e(n\theta)\right\rvert \mathrm{d}\theta \gg \log N,$ where $e(x)=e^{2\pi ix }$ ?

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

512.lean

Retained formal statement1 of 1

Is it true that, if $A\subset \mathbb{Z}$ is a finite set of size $N$ , then $\int_0^1 \left\lvert \sum_{n\in A}e(n\theta)\right\rvert \mathrm{d}\theta \gg \log N,$ where $e(x)=e^{2\pi ix }$ ?

Littlewood's conjecture, proved independently by Konyagin [Ko81] and McGehee, Pigno, and Smith [MPS81].

FormalConjectures/ErdosProblems/512.leanErdos512.erdos_5122 linesExact file

1True ↔2  ∃ c > 0, ∀ (N : ℕ) (A : Finset ℤ), A.card = N → c * Real.log ↑N ≤ ∫ (θ : ℝ) in 0..1, ‖∑ n ∈ A, additiveChar (↑n * θ)‖

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.

Sources

Search problems.science