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

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/512.lean

Formal Conjectures

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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:512

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page