Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1989P3

module

public import Mathlib.Algebra.Order.Star.Real
public import Mathlib.Analysis.CStarAlgebra.Classes
public import Mathlib.Analysis.Complex.Polynomial.Basic
public import Mathlib.RingTheory.SimpleRing.Principal

public section


/-!
# USA Mathematical Olympiad 1989, Problem 3

Let P(z) = zⁿ + c₁zⁿ⁻¹ + ⋯ + cₙ be a polynomial in the complex variable z,
with real coefficients cₖ. Suppose that |P(i)| < 1. Prove that there exist
real numbers a and b such that P(a + bi) = 0 and (a² + b² + 1)² < 4b² + 1.
-/

namespace Usa1989P3

open Polynomial

theorem usa1989_p3
    (P : ℂ[X]) (hmonic : P.Monic)
    (hreal : ∀ n : ℕ, (P.coeff n).im = 0)
    (hP : ‖P.eval Complex.I‖ < 1) :
    ∃ a b : ℝ, P.eval (a + b * Complex.I) = 0 ∧
      (a ^ 2 + b ^ 2 + 1) ^ 2 < 4 * b ^ 2 + 1 := sorry

end Usa1989P3

File author(s): David Renshaw, Kimi K3

This problem has a complete formalized solution.