turan_power_sum_conjecture
Disprovedanalyticnumbertheorycombinatoricsharmonicanalysisopenproblemproved
Turán's first main theorem: Power sums ∑bₙzₙᵏ with |zₙ| ≥ 1 can't all be small. Proved by Turán (1953). Extensions to more general exponential sums and the exact constants in Turán's lemma are open.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem turan_power_sum_conjecture (n m : ℕ) (hn : 1 ≤ n) (hm : 1 ≤ m) :
∃ k : Fin m, ∀ (z : Fin n → ℂ) (b : Fin n → ℂ),
(∀ i, ‖z i‖ ≥ 1) →
∃ k' : Fin m,
(n : ℝ) ^ (-(n : ℝ)) * ∑ i : Fin n, ‖b i‖ ≤
‖∑ j : Fin n, b j * z j ^ (k'.val + 1)‖ := by
sorrySource