# mathlib3documentation

mathlib-archive / imo.imo1962_q4

# IMO 1962 Q4 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

def imo1962_q4.problem_equation (x : ) :
Prop
Equations
Equations
noncomputable def imo1962_q4.alt_formula (x : ) :
Equations
theorem imo1962_q4.cos_sum_equiv {x : } :
(real.cos x ^ 2 + real.cos (2 * x) ^ 2 + real.cos (3 * x) ^ 2 - 1) / 4 =
theorem imo1962_q4.alt_equiv {x : } :
theorem imo1962_q4.finding_zeros {x : } :
^ 2 = 1 / 2 real.cos (3 * x) = 0
theorem imo1962_q4.solve_cos2_half {x : } :
^ 2 = 1 / 2 (k : ), x = (2 * k + 1) * real.pi / 4
theorem imo1962_q4.solve_cos3x_0 {x : } :
real.cos (3 * x) = 0 (k : ), x = (2 * k + 1) * real.pi / 6
theorem imo1962_q4 {x : } :
theorem imo1962_q4.formula {R : Type u_1} [comm_ring R] [is_domain R] [char_zero R] (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

Someday, when there is a Grobner basis tactic, try to automate this proof. (A little tricky -- the ideals are not the same but their Jacobson radicals are.)

theorem imo1962_q4.solve_cos2x_0 {x : } :
real.cos (2 * x) = 0 (k : ), x = (2 * k + 1) * real.pi / 4
theorem imo1962_q4' {x : } :