Flat Littlewood polynomials

DefinitionLittlewood polynomials#✓fully proved

A polynomial \(P\) over a ring \(F\), of degree \(n\) (with the zero polynomial taken to have degree \(0\)), is a Littlewood polynomial if each of its coefficients of \(X^0, X^1, \ldots, X^n\) is \(1\) or \(-1\).

def IsLittlewoodPolynomial {F : Type*} [Ring F] (P : F[X]) : Prop :=
  ∀ i ≤ P.natDegree, P.coeff i = 1 ∨ P.coeff i = -1

Used by 1

Used byFlat Littlewood polynomials exist

TheoremFlat Littlewood polynomials exist#●ready to prove

There exist real constants \(\Delta > \delta > 0\) such that for every natural number \(n \ge 2\) there is a Littlewood polynomial \(P\) with complex coefficients and of degree \(n\) such that \(\delta \sqrt{n} \le |P(z)| \le \Delta \sqrt{n}\) for all \(z \in \mathbb{C}\) with \(|z| = 1\).

public theorem_wanted theorem_1_1 :
    ∃ Δ δ : ℝ, Δ > δ ∧ δ > 0 ∧ ∀ n ≥ 2,
      ∃ P : ℂ[X], IsLittlewoodPolynomial P ∧ P.natDegree = n ∧
      ∀ z : ℂ, ‖z‖ = 1 → δ * √n ≤ ‖P.eval z‖ ∧
      ‖P.eval z‖ ≤ Δ * √n

Sources

• P. Balister, B. Bollobás, R. Morris, J. Sahasrabudhe, and M. Tiba, Flat Littlewood polynomials exist, Annals of Math, 192 (3) 2020. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_flat_littlewood_poly of the lean-eval benchmark.

Uses 1

Statement usesLittlewood polynomials

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.