Skip to content

Erdős problem 512

Is it true that, if A⊂ZA\subset \mathbb{Z} is a finite set of size NN, then ∫01∣∑n∈Ae(nθ)∣dθ≫log⁡N,\int_0^1 \left\lvert \sum_{n\in A}e(n\theta)\right\rvert \mathrm{d}\theta \gg \log N, where e(x)=e2πixe(x)=e^{2\pi ix }?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

512.lean

Retained formal statement1 of 1

Is it true that, if A⊂ZA\subset \mathbb{Z} is a finite set of size NN, then ∫01∣∑n∈Ae(nθ)∣dθ≫log⁡N,\int_0^1 \left\lvert \sum_{n\in A}e(n\theta)\right\rvert \mathrm{d}\theta \gg \log N, where e(x)=e2πixe(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
True ↔  ∃ 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.