mathlib3 documentation

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.

source
def imo1962_q4.problem_equation (x : ℝ) :
Prop
Equations
source
def imo1962_q4.solution_set  :
set ℝ
Equations
source
noncomputable def imo1962_q4.alt_formula (x : ℝ) :
ℝ
Equations
source
theorem imo1962_q4.cos_sum_equiv {x : ℝ} :
(real.cos x ^ 2 + real.cos (2 * x) ^ 2 + real.cos (3 * x) ^ 2 - 1) / 4 = imo1962_q4.alt_formula x
source
theorem imo1962_q4.alt_equiv {x : ℝ} :
imo1962_q4.problem_equation x ↔ imo1962_q4.alt_formula x = 0
source
theorem imo1962_q4.finding_zeros {x : ℝ} :
imo1962_q4.alt_formula x = 0 ↔ real.cos x ^ 2 = 1 / 2 ∨ real.cos (3 * x) = 0
source
theorem imo1962_q4.solve_cos2_half {x : ℝ} :
real.cos x ^ 2 = 1 / 2 ↔ ∃ (k : ℤ), x = (2 * ↑k + 1) * real.pi / 4
source
theorem imo1962_q4.solve_cos3x_0 {x : ℝ} :
real.cos (3 * x) = 0 ↔ ∃ (k : ℤ), x = (2 * ↑k + 1) * real.pi / 6
source
theorem imo1962_q4 {x : ℝ} :
imo1962_q4.problem_equation x ↔ x ∈ imo1962_q4.solution_set
source
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.)

source
theorem imo1962_q4.solve_cos2x_0 {x : ℝ} :
real.cos (2 * x) = 0 ↔ ∃ (k : ℤ), x = (2 * ↑k + 1) * real.pi / 4
source
theorem imo1962_q4' {x : ℝ} :
imo1962_q4.problem_equation x ↔ x ∈ imo1962_q4.solution_set