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.

source

def imo.problem_equation (x : ℝ) :

Prop

Equations

imo.problem_equation x = (real.cos x ^ 2 + real.cos (2 * x) ^ 2 + real.cos (3 * x) ^ 2 = 1)

source

def imo.solution_set :

set ℝ

Equations

imo.solution_set = {x : ℝ | ∃ (k : ℤ), x = (2 * ↑k + 1) * real.pi / 4 ∨ x = (2 * ↑k + 1) * real.pi / 6}

source

noncomputable def imo.alt_formula (x : ℝ) :

ℝ

Equations

imo.alt_formula x = real.cos x * (real.cos x ^ 2 - 1 / 2) * real.cos (3 * x)

source

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

source

theorem imo.alt_equiv {x : ℝ} :

imo.problem_equation x ↔ imo.alt_formula x = 0

source

theorem imo.finding_zeros {x : ℝ} :

imo.alt_formula x = 0 ↔ real.cos x ^ 2 = 1 / 2 ∨ real.cos (3 * x) = 0

source

theorem imo.solve_cos2_half {x : ℝ} :

real.cos x ^ 2 = 1 / 2 ↔ ∃ (k : ℤ), x = (2 * ↑k + 1) * real.pi / 4

source

theorem imo.solve_cos3x_0 {x : ℝ} :

real.cos (3 * x) = 0 ↔ ∃ (k : ℤ), x = (2 * ↑k + 1) * real.pi / 6

source

theorem imo.imo1962_q4 {x : ℝ} :

imo.problem_equation x ↔ x ∈ imo.solution_set

source

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

source

theorem imo.solve_cos2x_0 {x : ℝ} :

real.cos (2 * x) = 0 ↔ ∃ (k : ℤ), x = (2 * ↑k + 1) * real.pi / 4

source

theorem imo.imo1962_q4' {x : ℝ} :

imo.problem_equation x ↔ x ∈ imo.solution_set