feat(archive/imo): formalize IMO 1962 problem 4 (#4518)

The problem statement: Solve the equation `cos x ^ 2 + cos (2 * x) ^ 2 + cos (3 * x) ^ 2 = 1`.

There are a bunch of trig formulas I proved along the way; there are sort of an infinite number of trig formulas so I'm open to feedback on whether some should go in the core libraries. Also possibly some of them have a shorter proof that would render the lemma unnecessary.

For what it's worth, the actual method of solution is not how a human would do it; a more intuitive human method is to simplify in terms of `cos x` and then solve, but I think this is simpler in Lean because it doesn't rely on solving `cos x = y` for several different `y`.

Co-authored-by: Patrick Massot <patrickmassot@free.fr>

archive/imo/imo1962_q4.lean

@@ -0,0 +1,93 @@
+/-
+Copyright (c) 2020 Kevin Lacker. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kevin Lacker
+-/
+
+import analysis.special_functions.trigonometric
+
+/-!
+# 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.
+-/
+
+open real
+open_locale real
+noncomputable theory
+
+def problem_equation (x : ℝ) : Prop := cos x ^ 2 + cos (2 * x) ^ 2 + cos (3 * x) ^ 2 = 1
+
+def solution_set : set ℝ :=
+{ x : ℝ | ∃ k : ℤ, x = (2 * ↑k + 1) * π / 4 ∨ x = (2 * ↑k + 1) * π / 6 }
+
+/-
+The key to solving this problem simply is that we can rewrite the equation as
+a product of terms, shown in `alt_formula`, being equal to zero.
+-/
+
+def alt_formula (x : ℝ) : ℝ := cos x * (cos x ^ 2 - 1/2) * cos (3 * x)
+
+lemma cos_sum_equiv {x : ℝ} :
+(cos x ^ 2 + cos (2 * x) ^ 2 + cos (3 * x) ^ 2 - 1) / 4 = alt_formula x :=
+begin
+  simp only [real.cos_two_mul, cos_three_mul, alt_formula],
+  ring
+end
+
+lemma alt_equiv {x : ℝ} : problem_equation x ↔ alt_formula x = 0 :=
+begin
+  rw [ problem_equation, ← cos_sum_equiv, div_eq_zero_iff, sub_eq_zero],
+  norm_num,
+end
+
+lemma finding_zeros {x : ℝ} :
+alt_formula x = 0 ↔ cos x ^ 2 = 1/2 ∨ cos (3 * x) = 0 :=
+begin
+  simp only [alt_formula, mul_assoc, mul_eq_zero, sub_eq_zero],
+  split,
+  { rintro (h1|h2),
+    { right,
+      rw [cos_three_mul, h1],
+      ring },
+    { exact h2 } },
+  { exact or.inr }
+end
+
+/-
+Now we can solve for `x` using basic-ish trigonometry.
+-/
+
+lemma solve_cos2_half {x : ℝ} : cos x ^ 2 = 1/2 ↔ ∃ k : ℤ, x = (2 * ↑k + 1) * π / 4 :=
+begin
+  rw cos_square,
+  simp only [add_right_eq_self, div_eq_zero_iff],
+  norm_num,
+  rw cos_eq_zero_iff,
+  split;
+  { rintro ⟨k, h⟩,
+    use k,
+    linarith },
+end
+
+lemma solve_cos3x_0 {x : ℝ} : cos (3 * x) = 0 ↔ ∃ k : ℤ, x = (2 * ↑k + 1) * π / 6 :=
+begin
+  rw cos_eq_zero_iff,
+  apply exists_congr,
+  intro k,
+  split; intro; linarith
+end
+
+/-
+The final theorem is now just gluing together our lemmas.
+-/
+
+theorem imo1962_q4 {x : ℝ} : problem_equation x ↔ x ∈ solution_set :=
+begin
+  rw [alt_equiv, finding_zeros, solve_cos3x_0, solve_cos2_half],
+  exact exists_or_distrib.symm
+end
+

src/data/complex/exponential.lean

@@ -10,7 +10,7 @@ import data.complex.basic
 # Exponential, trigonometric and hyperbolic trigonometric functions
 
 This file contains the definitions of the real and complex exponential, sine, cosine, tangent,
-hyperbolic sine, hypebolic cosine, and hyperbolic tangent functions.
+hyperbolic sine, hyperbolic cosine, and hyperbolic tangent functions.
 
 -/
 local notation `abs'` := _root_.abs
@@ -609,6 +609,47 @@ by rw [← mul_right_inj' (@two_ne_zero' ℂ _ _ _), mul_sub,
 lemma cosh_sq_sub_sinh_sq : cosh x ^ 2 - sinh x ^ 2 = 1 :=
 by rw [sq_sub_sq, cosh_add_sinh, cosh_sub_sinh, ← exp_add, add_neg_self, exp_zero]
 
+lemma cosh_square : cosh x ^ 2 = sinh x ^ 2 + 1 :=
+begin
+  rw ← cosh_sq_sub_sinh_sq x,
+  ring
+end
+
+lemma sinh_square : sinh x ^ 2 = cosh x ^ 2 - 1 :=
+begin
+  rw ← cosh_sq_sub_sinh_sq x,
+  ring
+end
+
+lemma cosh_two_mul : cosh (2 * x) = cosh x ^ 2 + sinh x ^ 2 :=
+by rw [two_mul, cosh_add, pow_two, pow_two]
+
+lemma sinh_two_mul : sinh (2 * x) = 2 * sinh x * cosh x :=
+begin
+  rw [two_mul, sinh_add],
+  ring
+end
+
+lemma cosh_three_mul : cosh (3 * x) = 4 * cosh x ^ 3 - 3 * cosh x :=
+begin
+  have h1 : x + 2 * x = 3 * x, by ring,
+  rw [← h1, cosh_add x (2 * x)],
+  simp only [cosh_two_mul, sinh_two_mul],
+  have h2 : sinh x * (2 * sinh x * cosh x) = 2 * cosh x * sinh x ^ 2, by ring,
+  rw [h2, sinh_square],
+  ring
+end
+
+lemma sinh_three_mul : sinh (3 * x) = 4 * sinh x ^ 3 + 3 * sinh x :=
+begin
+  have h1 : x + 2 * x = 3 * x, by ring,
+  rw [← h1, sinh_add x (2 * x)],
+  simp only [cosh_two_mul, sinh_two_mul],
+  have h2 : cosh x * (2 * sinh x * cosh x) = 2 * sinh x * cosh x ^ 2, by ring,
+  rw [h2, cosh_square],
+  ring,
+end
+
 @[simp] lemma sin_zero : sin 0 = 0 := by simp [sin]
 
 @[simp] lemma sin_neg : sin (-x) = -sin x :=
@@ -729,9 +770,32 @@ by rw [two_mul, sin_add, two_mul, add_mul, mul_comm]
 lemma cos_square : cos x ^ 2 = 1 / 2 + cos (2 * x) / 2 :=
 by simp [cos_two_mul, div_add_div_same, mul_div_cancel_left, two_ne_zero', -one_div]
 
+lemma cos_square' : cos x ^ 2 = 1 - sin x ^ 2 :=
+by { rw [←sin_sq_add_cos_sq x], simp }
+
 lemma sin_square : sin x ^ 2 = 1 - cos x ^ 2 :=
 by { rw [←sin_sq_add_cos_sq x], simp }
 
+lemma cos_three_mul : cos (3 * x) = 4 * cos x ^ 3 - 3 * cos x :=
+begin
+  have h1 : x + 2 * x = 3 * x, by ring,
+  rw [← h1, cos_add x (2 * x)],
+  simp only [cos_two_mul, sin_two_mul, mul_add, mul_sub, mul_one, pow_two],
+  have h2 : 4 * cos x ^ 3 = 2 * cos x * cos x * cos x + 2 * cos x * cos x ^ 2, by ring,
+  rw [h2, cos_square'],
+  ring
+end
+
+lemma sin_three_mul : sin (3 * x) = 3 * sin x - 4 * sin x ^ 3 :=
+begin
+  have h1 : x + 2 * x = 3 * x, by ring,
+  rw [← h1, sin_add x (2 * x)],
+  simp only [cos_two_mul, sin_two_mul, cos_square'],
+  have h2 : cos x * (2 * sin x * cos x) = 2 * sin x * cos x ^ 2, by ring,
+  rw [h2, cos_square'],
+  ring
+end
+
 lemma exp_mul_I : exp (x * I) = cos x + sin x * I :=
 (cos_add_sin_I _).symm
 
@@ -853,15 +917,27 @@ lemma neg_one_le_cos : -1 ≤ cos x :=
 lemma cos_two_mul : cos (2 * x) = 2 * cos x ^ 2 - 1 :=
 by rw ← of_real_inj; simp [cos_two_mul]
 
+lemma cos_two_mul' : cos (2 * x) = cos x ^ 2 - sin x ^ 2 :=
+by rw ← of_real_inj; simp [cos_two_mul']
+
 lemma sin_two_mul : sin (2 * x) = 2 * sin x * cos x :=
 by rw ← of_real_inj; simp [sin_two_mul]
 
 lemma cos_square : cos x ^ 2 = 1 / 2 + cos (2 * x) / 2 :=
 of_real_inj.1 $ by simpa using cos_square x
 
+lemma cos_square' : cos x ^ 2 = 1 - sin x ^ 2 :=
+by { rw [←sin_sq_add_cos_sq x], simp }
+
 lemma sin_square : sin x ^ 2 = 1 - cos x ^ 2 :=
 eq_sub_iff_add_eq.2 $ sin_sq_add_cos_sq _
 
+lemma cos_three_mul : cos (3 * x) = 4 * cos x ^ 3 - 3 * cos x :=
+by rw ← of_real_inj; simp [cos_three_mul]
+
+lemma sin_three_mul : sin (3 * x) = 3 * sin x - 4 * sin x ^ 3 :=
+by rw ← of_real_inj; simp [sin_three_mul]
+
 /-- The definition of `sinh` in terms of `exp`. -/
 lemma sinh_eq (x : ℝ) : sinh x = (exp x - exp (-x)) / 2 :=
 eq_div_of_mul_eq two_ne_zero $ by rw [sinh, exp, exp, complex.of_real_neg, complex.sinh, mul_two,
@@ -894,23 +970,40 @@ by simp [sub_eq_add_neg, sinh_add, sinh_neg, cosh_neg]
 lemma cosh_sub : cosh (x - y) = cosh x * cosh y - sinh x * sinh y :=
 by simp [sub_eq_add_neg, cosh_add, sinh_neg, cosh_neg]
 
-lemma cosh_sq_sub_sinh_sq (x : ℝ) : cosh x ^ 2 - sinh x ^ 2 = 1 :=
-begin
-  rw [sinh, cosh],
-  have := congr_arg complex.re (complex.cosh_sq_sub_sinh_sq x),
-  rw [pow_two, pow_two] at this,
-  change (⟨_, _⟩ : ℂ).re - (⟨_, _⟩ : ℂ).re = 1 at this,
-  rw [complex.cosh_of_real_im x, complex.sinh_of_real_im x, mul_zero, sub_zero, sub_zero] at this,
-  rwa [pow_two, pow_two],
-end
-
 lemma tanh_eq_sinh_div_cosh : tanh x = sinh x / cosh x :=
 of_real_inj.1 $ by simp [tanh_eq_sinh_div_cosh]
 
 @[simp] lemma tanh_zero : tanh 0 = 0 := by simp [tanh]
 
 @[simp] lemma tanh_neg : tanh (-x) = -tanh x := by simp [tanh, neg_div]
 
+lemma cosh_add_sinh : cosh x + sinh x = exp x :=
+by rw ← of_real_inj; simp [cosh_add_sinh]
+
+lemma sinh_add_cosh : sinh x + cosh x = exp x :=
+by rw ← of_real_inj; simp [sinh_add_cosh]
+
+lemma cosh_sq_sub_sinh_sq (x : ℝ) : cosh x ^ 2 - sinh x ^ 2 = 1 :=
+by rw ← of_real_inj; simp [cosh_sq_sub_sinh_sq]
+
+lemma cosh_square : cosh x ^ 2 = sinh x ^ 2 + 1 :=
+by rw ← of_real_inj; simp [cosh_square]
+
+lemma sinh_square : sinh x ^ 2 = cosh x ^ 2 - 1 :=
+by rw ← of_real_inj; simp [sinh_square]
+
+lemma cosh_two_mul : cosh (2 * x) = cosh x ^ 2 + sinh x ^ 2 :=
+by rw ← of_real_inj; simp [cosh_two_mul]
+
+lemma sinh_two_mul : sinh (2 * x) = 2 * sinh x * cosh x :=
+by rw ← of_real_inj; simp [sinh_two_mul]
+
+lemma cosh_three_mul : cosh (3 * x) = 4 * cosh x ^ 3 - 3 * cosh x :=
+by rw ← of_real_inj; simp [cosh_three_mul]
+
+lemma sinh_three_mul : sinh (3 * x) = 4 * sinh x ^ 3 + 3 * sinh x :=
+by rw ← of_real_inj; simp [sinh_three_mul]
+
 open is_absolute_value
 
 /- TODO make this private and prove ∀ x -/