module
public import Mathlib.Tactic
public section
/-!
# International Mathematical Olympiad 1959, Problem 3
Let `a`, `b`, `c` be real numbers. Given the equation for `cos x`:
a cos²x + b cos x + c = 0,
form a quadratic equation in `cos 2x` whose roots are the same values of `x`.
Compare the equations in `cos x` and `cos 2x` for `a = 4`, `b = 2`, `c = -1`.
-/
open Real
namespace Imo1959P3
/-- The coefficients of the quadratic equation in `cos (2 * x)` formed from
`a * cos x ^ 2 + b * cos x + c = 0`: writing `cos (2 * x) = 2 * cos x ^ 2 - 1`
and eliminating the odd power of `cos x` by squaring. -/
/- determine -/ abbrev formedQuadratic (a b c : ℝ) : ℝ × ℝ × ℝ := sorry
/-- The formed quadratic evaluated at `t`, i.e. the quadratic with coefficients
`formedQuadratic a b c` applied to `t`. -/
def formedQuadraticEval (a b c : ℝ) (t : ℝ) : ℝ :=
(formedQuadratic a b c).1 * t ^ 2 + (formedQuadratic a b c).2.1 * t +
(formedQuadratic a b c).2.2
theorem imo1959_p3 (a b c x : ℝ) (h : a * cos x ^ 2 + b * cos x + c = 0) :
formedQuadraticEval a b c (cos (2 * x)) = 0 := sorry
/-- For `a = 4`, `b = 2`, `c = -1` the formed equation in `cos 2x` is four
times the original equation in `cos x`: the two equations are the same. -/
theorem imo1959_p3_comparison (t : ℝ) :
formedQuadraticEval 4 2 (-1) t = 4 * (4 * t ^ 2 + 2 * t - 1) := sorry
end Imo1959P3
This problem has a complete formalized solution.