Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2002P3

module

public import Mathlib.Analysis.Polynomial.Basic
public import Mathlib.LinearAlgebra.Lagrange
public import Mathlib.Topology.Algebra.Polynomial

public section


/-!
# USA Mathematical Olympiad 2002, Problem 3

Prove that any monic polynomial (a polynomial with leading coefficient 1)
of degree n with real coefficients is the average of two monic polynomials
of degree n with n real roots.
-/

namespace Usa2002P3

open Polynomial Filter Asymptotics

theorem usa2002_p3 (n : ℕ) (p : ℝ[X]) (hpm : p.Monic) (hpn : p.natDegree = n) :
    ∃ q r : ℝ[X], q.Monic ∧ r.Monic ∧ q.natDegree = n ∧ r.natDegree = n ∧
      q.roots.card = n ∧ r.roots.card = n ∧
      q.Splits ∧ r.Splits ∧ p = (q + r) / 2 := sorry

end Usa2002P3

File author(s): Kimi K3

This problem has a complete formalized solution.