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.

Equations
Instances For
    Equations
    Instances For
      Equations
      Instances For
        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.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 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