# Documentation

Archive.Imo.Imo1962Q4

# 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.

Instances For
Instances For
Instances For
theorem Imo1962Q4.cos_sum_equiv {x : } :
( ^ 2 + Real.cos (2 * x) ^ 2 + Real.cos (3 * x) ^ 2 - 1) / 4 =
theorem Imo1962Q4.finding_zeros {x : } :
^ 2 = 1 / 2 Real.cos (3 * x) = 0
theorem Imo1962Q4.solve_cos2_half {x : } :
^ 2 = 1 / 2 k, x = (2 * k + 1) * Real.pi / 4
theorem Imo1962Q4.solve_cos3x_0 {x : } :
Real.cos (3 * x) = 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 : } :
Real.cos (2 * x) = 0 k, x = (2 * k + 1) * Real.pi / 4
theorem imo1962_q4' {x : } :