Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1988P2

module

public import Mathlib.Algebra.Order.Star.Real
public import Mathlib.Algebra.Polynomial.Derivative

public section


/-!
# USA Mathematical Olympiad 1988, Problem 2

The cubic x^3 + ax^2 + bx + c has real coefficients and three real roots
r ≥ s ≥ t. Show that k = a^2 - 3b ≥ 0 and that √k ≤ r - t.
-/

namespace Usa1988P2

open Polynomial

theorem usa1988_p2 (a b c r s t : ℝ) (hrs : s ≤ r) (hst : t ≤ s)
    (hroots : (X - C r) * (X - C s) * (X - C t)
      = X ^ 3 + C a * X ^ 2 + C b * X + C c) :
    0 ≤ a ^ 2 - 3 * b ∧ Real.sqrt (a ^ 2 - 3 * b) ≤ r - t := sorry

end Usa1988P2

File author(s): Kimi K3

This problem has a complete formalized solution.