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 Imo1962Q4.ProblemEquation (x : ℝ) : Prop

Equations

• Imo1962Q4.ProblemEquation x = (Real.cos x ^ 2 + Real.cos (2 * x) ^ 2 + Real.cos (3 * x) ^ 2 = 1)

def Imo1962Q4.solutionSet : Set ℝ

Equations

• Imo1962Q4.solutionSet = {x : ℝ | ∃ (k : ℤ), x = (2 * ↑k + 1) * Real.pi / 4 ∨ x = (2 * ↑k + 1) * Real.pi / 6}

def Imo1962Q4.altFormula (x : ℝ) : ℝ

Equations

• Imo1962Q4.altFormula x = Real.cos x * (Real.cos x ^ 2 - 1 / 2) * Real.cos (3 * x)

theorem Imo1962Q4.cos_sum_equiv {x : ℝ} : (Real.cos x ^ 2 + Real.cos (2 * x) ^ 2 + Real.cos (3 * x) ^ 2 - 1) / 4 = Imo1962Q4.altFormula x

theorem Imo1962Q4.alt_equiv {x : ℝ} : Imo1962Q4.ProblemEquation x ↔ Imo1962Q4.altFormula x = 0

theorem Imo1962Q4.finding_zeros {x : ℝ} : Imo1962Q4.altFormula x = 0 ↔ Real.cos x ^ 2 = 1 / 2 ∨ Real.cos (3 * x) = 0

theorem Imo1962Q4.solve_cos2_half {x : ℝ} : Real.cos 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 : ℝ} : Imo1962Q4.ProblemEquation x ↔ x ∈ Imo1962Q4.solutionSet

theorem Imo1962Q4.formula {R : Type u_1} [CommRing R] [IsDomain R] [CharZero 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

theorem Imo1962Q4.solve_cos2x_0 {x : ℝ} : Real.cos (2 * x) = 0 ↔ ∃ (k : ℤ), x = (2 * ↑k + 1) * Real.pi / 4

theorem imo1962_q4' {x : ℝ} : Imo1962Q4.ProblemEquation x ↔ x ∈ Imo1962Q4.solutionSet