Flat Littlewood polynomials exist | Lean AI formalization leaderboard

Problem statement

Notes: Unavailable.

Source: 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 (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2020-192-3-FlatLittlewoodPoly.lean

Informal solution: Unavailable.

theorem declaration uses `sorry`theorem_1_1 :
    ∃ Δ δ : ℝ, Δ > δ ∧ δ > 0 ∧ ∀ n ≥ 2,
      ∃ P : ℂ[X], FlatLittlewoodPoly.IsLittlewoodPolynomial P ∧ P.natDegree = n ∧
      ∀ z : ℂ, ‖z‖ = 1 → δ * √n ≤ ‖P.eval z‖ ∧
      ‖P.eval z‖ ≤ Δ * √n := by⊢ ∃ Δ δ,
  Δ > δ ∧
    δ > 0 ∧
      ∀ n ≥ 2,
        ∃ P,
          IsLittlewoodPolynomial P ∧
            P.natDegree = n ∧ ∀ (z : ℂ), ‖z‖ = 1 → δ * √↑n ≤ ‖Polynomial.eval z P‖ ∧ ‖Polynomial.eval z P‖ ≤ Δ * √↑n
  sorryAll goals completed! 🐙