Complementary polynomial on the unit circle | Lean AI formalization leaderboard

Problem statement

Notes: If a complex polynomial has modulus at most 1 on the unit circle, then there is a same-degree complementary polynomial whose squared moduli add to 1 on the circle.

Source: https://link.springer.com/article/10.1007/s00220-025-05302-9

Informal solution: Construct a polynomial Q so that |P(z)|^2 + |Q(z)|^2 = 1 for all z on the unit circle.

theorem declaration uses `sorry`exists_complementary_polynomial_on_unit_circle (P : ℂ[X])
    (hP : ∀ z : Circle, ‖P.eval (z : ℂ)‖ ≤ 1) :
    ∃ Q : ℂ[X],
      Q.natDegree ≤ P.natDegree ∧
        ∀ z : Circle, ‖P.eval (z : ℂ)‖ ^ 2 + ‖Q.eval (z : ℂ)‖ ^ 2 = 1 := byP:ℂ[X]hP:∀ (z : Circle), ‖eval (↑z) P‖ ≤ 1⊢ ∃ Q, Q.natDegree ≤ P.natDegree ∧ ∀ (z : Circle), ‖eval (↑z) P‖ ^ 2 + ‖eval (↑z) Q‖ ^ 2 = 1
  sorryAll goals completed! 🐙