# IMO 1962 Q4 #

Solve the equation cos x ^ 2 + cos (2 * x) ^ 2 + cos (3 * x) ^ 2 = 1.

Since Lean does not have a concept of "simplest form", we just express what is in fact the simplest form of the set of solutions, and then prove it equals the set of solutions.

Equations
• = (x.cos ^ 2 + (2 * x).cos ^ 2 + (3 * x).cos ^ 2 = 1)
Instances For
Equations
Instances For
Equations
• = x.cos * (x.cos ^ 2 - 1 / 2) * (3 * x).cos
Instances For
theorem Imo1962Q4.cos_sum_equiv {x : } :
(x.cos ^ 2 + (2 * x).cos ^ 2 + (3 * x).cos ^ 2 - 1) / 4 =
theorem Imo1962Q4.finding_zeros {x : } :
x.cos ^ 2 = 1 / 2 (3 * x).cos = 0
theorem Imo1962Q4.solve_cos2_half {x : } :
x.cos ^ 2 = 1 / 2 ∃ (k : ), x = (2 * k + 1) * Real.pi / 4
theorem Imo1962Q4.solve_cos3x_0 {x : } :
(3 * x).cos = 0 ∃ (k : ), x = (2 * k + 1) * Real.pi / 6
theorem imo1962_q4 {x : } :
theorem Imo1962Q4.formula {R : Type u_1} [] [] [] (a : R) :
a ^ 2 + (2 * a ^ 2 - 1) ^ 2 + (4 * a ^ 3 - 3 * a) ^ 2 = 1 (2 * a ^ 2 - 1) * (4 * a ^ 3 - 3 * a) = 0
theorem Imo1962Q4.solve_cos2x_0 {x : } :
(2 * x).cos = 0 ∃ (k : ), x = (2 * k + 1) * Real.pi / 4
theorem imo1962_q4' {x : } :