Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2014P1

import Mathlib.Tactic

/-!
# USA Mathematical Olympiad 2014, Problem 1

Let a, b, c, d be real numbers such that b-d ≥ 5 and all zeros
x₁, x₂, x₃, x₄ of x⁴+ax³+bx²+cx+d are real.
Find the smallest value the product $(x₁²+1)(x₂²+1)(x₃²+1)(x₄²+1)$ can take.
-/

namespace Usa2014P1

open Polynomial

noncomputable def Objective (x : Fin 4 → ℝ) : ℝ := ∏ i, ((x i)^2 + 1)

def Conditions (x : Fin 4 → ℝ) : Prop := ∃ a b c d : ℝ, (5 ≤ b - d) ∧
    ((X - C (x 0)) * (X - C (x 1)) * (X - C (x 2)) * (X - C (x 3))
    = X^4 + C a * X^3 + C b * X^2 + C c * X + C d)

noncomputable /- determine -/ abbrev solution : ℝ := sorry

theorem usa2014_p1 : IsLeast (Objective '' { x | Conditions x }) solution := sorry
end Usa2014P1

File author(s): Evan Chen

This problem has a complete formalized solution.