Skip to content

Erdős problem 1150

Is there some constant c>0c > 0 such that, for all large enough nn and all polynomials PP of degree nn with coefficients in {−1,1}\{-1, 1\}, max⁡∣z∣=1∣P(z)∣>(1+c)n?\max_{|z|=1} |P(z)| > (1 + c) \sqrt{n}?

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1150.lean

Retained formal statement2 of 2

The trivial lower bound from Parseval's identity: for any polynomial PP of degree nn with coefficients in {−1,1}\{-1, 1\}, we have max⁡∣z∣=1∣P(z)∣≥n+1\max_{|z|=1} |P(z)| \geq \sqrt{n+1}.

This follows from Parseval's identity: 12π∫02π∣P(eiθ)∣2dθ=∑k=0n∣ak∣2=n+1\frac{1}{2\pi} \int_0^{2\pi} |P(e^{i\theta})|^2 d\theta = \sum_{k=0}^{n} |a_k|^2 = n+1 since each ∣ak∣2=1|a_k|^2 = 1.

FormalConjectures/ErdosProblems/1150.leanErdos1150.erdos_1150.variants.parseval_lower_bound2 linesExact file
∀ (P : Polynomial ℂ) (n : ℕ),  (∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1) → P.natDegree = n → ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)
TextbookStatement only, no proof