mathlib documentation

mathlib-archive / imo.imo1962_q4

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.

def imo.problem_equation (x : ) :
Prop
Equations
Equations
noncomputable def imo.alt_formula (x : ) :
Equations
theorem imo.cos_sum_equiv {x : } :
(real.cos x ^ 2 + real.cos (2 * x) ^ 2 + real.cos (3 * x) ^ 2 - 1) / 4 = imo.alt_formula x
theorem imo.finding_zeros {x : } :
imo.alt_formula x = 0 real.cos x ^ 2 = 1 / 2 real.cos (3 * x) = 0
theorem imo.solve_cos2_half {x : } :
real.cos x ^ 2 = 1 / 2 (k : ), x = (2 * k + 1) * real.pi / 4
theorem imo.solve_cos3x_0 {x : } :
real.cos (3 * x) = 0 (k : ), x = (2 * k + 1) * real.pi / 6
theorem imo.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 imo.solve_cos2x_0 {x : } :
real.cos (2 * x) = 0 (k : ), x = (2 * k + 1) * real.pi / 4