bourgain_exponential_sum
Disprovedadditivecombinatoricscombinatoricsnumbertheoryopenproblemproved
Bourgain's exponential sum theorem: For subsets A of ℤ/pℤ with |A| > p^{1/2+ε}, the exponential sum has nontrivial cancellation. Proved by Bourgain using sum-product methods. Optimal bounds for all sizes remain open.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem bourgain_exponential_sum (p : ℕ) (hp : Nat.Prime p) (delta : ℝ)
(hdelta : 0 < delta ∧ delta < 1/2) :
∀ (A : Finset (ZMod p)),
(p : ℝ) ^ (1/2 + delta) ≤ A.card →
‖∑ a ∈ A, Complex.exp (2 * Real.pi * Complex.I * a.val / p)‖ ≤
(A.card : ℝ) * (p : ℝ) ^ (-delta / 2) := by
sorrySource