feat(analysis/special_functions/trigonometric): some lemmas (#4638)

The following changes:
- `sin_sub_sin` and friends (sum-to-product lemmas) moved from `trigonometric` to the earlier file `exponential`.  (I think the distinction between the files is that `trigonometric` collects the facts that require either differentiation or the definition `pi`, whereas purely algebraic facts about trigonometry go in `exponential`?  For example the double-angle formula is in `exponential`).
- rewrite proof of `cos_lt_cos_of_nonneg_of_le_pi_div_two` to avoid dependence on `cos_eq_one_iff_of_lt_of_lt` (but not sure if the result is actually simpler, feel free to propose this be reverted)
- some new explicit values of trig functions, `cos (π / 3)` and similar
- correct a series of lemmas in the `complex` namespace that were stated for real arguments (presumably the author copy-pasted but forgot to rewrite)
- lemmas `sin_eq_zero_iff`, `cos_eq_cos_iff`, `sin_eq_sin_iff`

src/analysis/special_functions/trigonometric.lean

@@ -719,15 +719,6 @@ by rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq x,
     pow_two, pow_two, ← sub_eq_iff_eq_add, sub_self];
   exact ⟨λ h, by rw [h, mul_zero], eq_zero_of_mul_self_eq_zero ∘ eq.symm⟩
 
-theorem sin_sub_sin (θ ψ : ℝ) : sin θ - sin ψ = 2 * sin((θ - ψ)/2) * cos((θ + ψ)/2) :=
-begin
-  have s1 := sin_add ((θ + ψ) / 2) ((θ - ψ) / 2),
-  have s2 := sin_sub ((θ + ψ) / 2) ((θ - ψ) / 2),
-  rw [div_add_div_same, add_sub, add_right_comm, add_sub_cancel, add_self_div_two] at s1,
-  rw [div_sub_div_same, ←sub_add, add_sub_cancel', add_self_div_two] at s2,
-  rw [s1, s2, ←sub_add, add_sub_cancel', ← two_mul, ← mul_assoc, mul_right_comm]
-end
-
 lemma cos_eq_one_iff (x : ℝ) : cos x = 1 ↔ ∃ n : ℤ, (n : ℝ) * (2 * π) = x :=
 ⟨λ h, let ⟨n, hn⟩ := sin_eq_zero_iff.1 (sin_eq_zero_iff_cos_eq.2 (or.inl h)) in
     ⟨n / 2, (int.mod_two_eq_zero_or_one n).elim
@@ -751,25 +742,16 @@ lemma cos_eq_one_iff_of_lt_of_lt {x : ℝ} (hx₁ : -(2 * π) < x) (hx₂ : x <
     end,
   λ h, by simp [h]⟩
 
-theorem cos_sub_cos (θ ψ : ℝ) : cos θ - cos ψ = -2 * sin((θ + ψ)/2) * sin((θ - ψ)/2) :=
-by rw [← sin_pi_div_two_sub, ← sin_pi_div_two_sub, sin_sub_sin, sub_sub_sub_cancel_left,
-    add_sub, sub_add_eq_add_sub, add_halves, sub_sub, sub_div π, cos_pi_div_two_sub,
-    ← neg_sub, neg_div, sin_neg, ← neg_mul_eq_mul_neg, neg_mul_eq_neg_mul, mul_right_comm]
-
 lemma cos_lt_cos_of_nonneg_of_le_pi_div_two {x y : ℝ} (hx₁ : 0 ≤ x) (hy₂ : y ≤ π / 2) (hxy : x < y) :
   cos y < cos x :=
-calc cos y = cos x * cos (y - x) - sin x * sin (y - x) :
-  by rw [← cos_add, add_sub_cancel'_right]
-... < (cos x * 1) - sin x * sin (y - x) :
-  sub_lt_sub_right ((mul_lt_mul_left
-    (cos_pos_of_mem_Ioo (lt_of_lt_of_le (neg_neg_of_pos pi_div_two_pos) hx₁)
-      (lt_of_lt_of_le hxy hy₂))).2
-        (lt_of_le_of_ne (cos_le_one _) (mt (cos_eq_one_iff_of_lt_of_lt
-          (show -(2 * π) < y - x, by linarith) (show y - x < 2 * π, by linarith)).1
-            (sub_ne_zero.2 (ne_of_lt hxy).symm)))) _
-... ≤ _ : by rw mul_one;
-  exact sub_le_self _ (mul_nonneg (sin_nonneg_of_nonneg_of_le_pi hx₁ (by linarith))
-    (sin_nonneg_of_nonneg_of_le_pi (by linarith) (by linarith)))
+begin
+  rw [← sub_lt_zero, cos_sub_cos],
+  have : 0 < sin ((y + x) / 2),
+  { refine sin_pos_of_pos_of_lt_pi _ _; linarith },
+  have : 0 < sin ((y - x) / 2),
+  { refine sin_pos_of_pos_of_lt_pi _ _; linarith },
+  nlinarith,
+end
 
 lemma cos_lt_cos_of_nonneg_of_le_pi {x y : ℝ} (hx₁ : 0 ≤ x) (hy₂ : y ≤ π) (hxy : x < y) :
   cos y < cos x :=
@@ -999,6 +981,75 @@ by { transitivity cos (pi / 2 ^ 5), congr, norm_num, simp }
 lemma sin_pi_div_thirty_two : sin (pi / 32) = sqrt (2 - sqrt (2 + sqrt (2 + sqrt 2))) / 2 :=
 by { transitivity sin (pi / 2 ^ 5), congr, norm_num, simp }
 
+-- This section is also a convenient location for other explicit values of `sin` and `cos`.
+
+/-- The cosine of `π / 3` is `1 / 2`. -/
+lemma cos_pi_div_three : cos (π / 3) = 1 / 2 :=
+begin
+  have h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0,
+  { have : cos (3 * (π / 3)) = cos π := by { congr' 1, ring },
+    linarith [cos_pi, cos_three_mul (π / 3)] },
+  cases mul_eq_zero.mp h₁ with h h,
+  { linarith [pow_eq_zero h] },
+  { have : cos π < cos (π / 3),
+    { refine cos_lt_cos_of_nonneg_of_le_pi _ rfl.ge _;
+      linarith [pi_pos] },
+    linarith [cos_pi] }
+end
+
+/-- The square of the cosine of `π / 6` is `3 / 4` (this is sometimes more convenient than the
+result for cosine itself). -/
+lemma square_cos_pi_div_six : cos (π / 6) ^ 2 = 3 / 4 :=
+begin
+  have h1 : cos (π / 6) ^ 2 = 1 / 2 + 1 / 2 / 2,
+  { convert cos_square (π / 6),
+    have h2 : 2 * (π / 6) = π / 3 := by cancel_denoms,
+    rw [h2, cos_pi_div_three] },
+  rw ← sub_eq_zero at h1 ⊢,
+  convert h1 using 1,
+  ring
+end
+
+/-- The cosine of `π / 6` is `√3 / 2`. -/
+lemma cos_pi_div_six : cos (π / 6) = (sqrt 3) / 2 :=
+begin
+  suffices : sqrt 3 = cos (π / 6) * 2,
+  { field_simp [(by norm_num : 0 ≠ 2)], exact this.symm },
+  rw sqrt_eq_iff_sqr_eq,
+  { have h1 := (mul_right_inj' (by norm_num : (4:ℝ) ≠ 0)).mpr square_cos_pi_div_six,
+    rw ← sub_eq_zero at h1 ⊢,
+    convert h1 using 1,
+    ring },
+  { norm_num },
+  { have : 0 < cos (π / 6) := by { apply cos_pos_of_mem_Ioo; linarith [pi_pos] },
+    linarith },
+end
+
+/-- The sine of `π / 6` is `1 / 2`. -/
+lemma sin_pi_div_six : sin (π / 6) = 1 / 2 :=
+begin
+  rw [← cos_pi_div_two_sub, ← cos_pi_div_three],
+  congr,
+  ring
+end
+
+/-- The square of the sine of `π / 3` is `3 / 4` (this is sometimes more convenient than the
+result for cosine itself). -/
+lemma square_sin_pi_div_three : sin (π / 3) ^ 2 = 3 / 4 :=
+begin
+  rw [← cos_pi_div_two_sub, ← square_cos_pi_div_six],
+  congr,
+  ring
+end
+
+/-- The sine of `π / 3` is `√3 / 2`. -/
+lemma sin_pi_div_three : sin (π / 3) = (sqrt 3) / 2 :=
+begin
+  rw [← cos_pi_div_two_sub, ← cos_pi_div_six],
+  congr,
+  ring
+end
+
 end cos_div_pow_two
 
 /-- The type of angles -/
@@ -1659,40 +1710,40 @@ by simp [two_mul, sin_add]
 @[simp] lemma cos_two_pi : cos (2 * π) = 1 :=
 by simp [two_mul, cos_add]
 
-lemma sin_add_pi (x : ℝ) : sin (x + π) = -sin x :=
+lemma sin_add_pi (x : ℂ) : sin (x + π) = -sin x :=
 by simp [sin_add]
 
-lemma sin_add_two_pi (x : ℝ) : sin (x + 2 * π) = sin x :=
+lemma sin_add_two_pi (x : ℂ) : sin (x + 2 * π) = sin x :=
 by simp [sin_add_pi, sin_add, sin_two_pi, cos_two_pi]
 
-lemma cos_add_two_pi (x : ℝ) : cos (x + 2 * π) = cos x :=
+lemma cos_add_two_pi (x : ℂ) : cos (x + 2 * π) = cos x :=
 by simp [cos_add, cos_two_pi, sin_two_pi]
 
-lemma sin_pi_sub (x : ℝ) : sin (π - x) = sin x :=
+lemma sin_pi_sub (x : ℂ) : sin (π - x) = sin x :=
 by simp [sub_eq_add_neg, sin_add]
 
-lemma cos_add_pi (x : ℝ) : cos (x + π) = -cos x :=
+lemma cos_add_pi (x : ℂ) : cos (x + π) = -cos x :=
 by simp [cos_add]
 
-lemma cos_pi_sub (x : ℝ) : cos (π - x) = -cos x :=
+lemma cos_pi_sub (x : ℂ) : cos (π - x) = -cos x :=
 by simp [sub_eq_add_neg, cos_add]
 
-lemma sin_add_pi_div_two (x : ℝ) : sin (x + π / 2) = cos x :=
+lemma sin_add_pi_div_two (x : ℂ) : sin (x + π / 2) = cos x :=
 by simp [sin_add]
 
-lemma sin_sub_pi_div_two (x : ℝ) : sin (x - π / 2) = -cos x :=
+lemma sin_sub_pi_div_two (x : ℂ) : sin (x - π / 2) = -cos x :=
 by simp [sub_eq_add_neg, sin_add]
 
-lemma sin_pi_div_two_sub (x : ℝ) : sin (π / 2 - x) = cos x :=
+lemma sin_pi_div_two_sub (x : ℂ) : sin (π / 2 - x) = cos x :=
 by simp [sub_eq_add_neg, sin_add]
 
-lemma cos_add_pi_div_two (x : ℝ) : cos (x + π / 2) = -sin x :=
+lemma cos_add_pi_div_two (x : ℂ) : cos (x + π / 2) = -sin x :=
 by simp [cos_add]
 
-lemma cos_sub_pi_div_two (x : ℝ) : cos (x - π / 2) = sin x :=
+lemma cos_sub_pi_div_two (x : ℂ) : cos (x - π / 2) = sin x :=
 by simp [sub_eq_add_neg, cos_add]
 
-lemma cos_pi_div_two_sub (x : ℝ) : cos (π / 2 - x) = sin x :=
+lemma cos_pi_div_two_sub (x : ℂ) : cos (π / 2 - x) = sin x :=
 by rw [← cos_neg, neg_sub, cos_sub_pi_div_two]
 
 lemma sin_nat_mul_pi (n : ℕ) : sin (n * π) = 0 :=
@@ -1733,6 +1784,63 @@ end
 theorem cos_ne_zero_iff {θ : ℂ} : cos θ ≠ 0 ↔ ∀ k : ℤ, θ ≠ (2 * k + 1) * π / 2 :=
 by rw [← not_exists, not_iff_not, cos_eq_zero_iff]
 
+theorem sin_eq_zero_iff {θ : ℂ} : sin θ = 0 ↔ ∃ k : ℤ, θ = k * π :=
+begin
+  rw [← complex.cos_sub_pi_div_two, cos_eq_zero_iff],
+  split,
+  { rintros ⟨k, hk⟩,
+    use k + 1,
+    field_simp [eq_add_of_sub_eq hk],
+    ring },
+  { rintros ⟨k, rfl⟩,
+    use k - 1,
+    field_simp,
+    ring }
+end
+
+theorem sin_ne_zero_iff {θ : ℂ} : sin θ ≠ 0 ↔ ∀ k : ℤ, θ ≠ k * π :=
+by rw [← not_exists, not_iff_not, sin_eq_zero_iff]
+
+lemma cos_eq_cos_iff {x y : ℂ} :
+  cos x = cos y ↔ ∃ k : ℤ, y = 2 * k * π + x ∨ y = 2 * k * π - x :=
+calc cos x = cos y ↔ cos x - cos y = 0 : sub_eq_zero.symm
+... ↔ -2 * sin((x + y)/2) * sin((x - y)/2) = 0 : by rw cos_sub_cos
+... ↔ sin((x + y)/2) = 0 ∨ sin((x - y)/2) = 0 : by { field_simp [(by norm_num : -(2:ℂ) ≠ 0)] }
+... ↔ sin((x - y)/2) = 0 ∨ sin((x + y)/2) = 0 : or.comm
+... ↔ (∃ k : ℤ, y = 2 * k * π + x) ∨ (∃ k :ℤ, y = 2 * k * π - x) :
+begin
+  apply or_congr;
+  rw sin_eq_zero_iff;
+  field_simp [(by norm_num : -(2:ℂ) ≠ 0)],
+  work_on_goal 0 -- material specific to the left of the `or`, when x ≅ y mod 2π
+  { split,
+    all_goals
+    { rintros ⟨k, hk⟩,
+      refine ⟨-k, eq.symm _⟩ } },
+  work_on_goal 2 -- material specific to the right of the `or`, when x ≅ -y mod 2π
+  { refine exists_congr (λ k, ⟨λ hk, _, λ hk, _⟩) },
+  all_goals -- joint material for showing two equations differ by a constant
+  { rw ← sub_eq_zero at hk ⊢,
+    convert hk using 1,
+    try { push_cast },
+    ring }
+end
+... ↔ ∃ k : ℤ, y = 2 * k * π + x ∨ y = 2 * k * π - x : exists_or_distrib.symm
+
+lemma sin_eq_sin_iff {x y : ℂ} :
+  sin x = sin y ↔ ∃ k : ℤ, y = 2 * k * π + x ∨ y = (2 * k + 1) * π - x :=
+begin
+  rw [←complex.cos_sub_pi_div_two, ←complex.cos_sub_pi_div_two, cos_eq_cos_iff],
+  simp only [exists_or_distrib],
+  apply or_congr;
+  refine exists_congr (λ k, ⟨_, _⟩);
+  { intros h,
+    rw ← sub_eq_zero at ⊢ h,
+    convert h using 1,
+    field_simp,
+    ring },
+end
+
 lemma has_deriv_at_tan {x : ℂ} (h : ∀ k : ℤ, x ≠ (2 * k + 1) * π / 2) :
   has_deriv_at tan (1 / (cos x)^2) x :=
 begin
@@ -1770,6 +1878,24 @@ end
 theorem cos_ne_zero_iff {θ : ℝ} : cos θ ≠ 0 ↔ ∀ k : ℤ, θ ≠ (2 * k + 1) * π / 2 :=
 by rw [← not_exists, not_iff_not, cos_eq_zero_iff]
 
+lemma cos_eq_cos_iff {x y : ℝ} :
+  cos x = cos y ↔ ∃ k : ℤ, y = 2 * k * π + x ∨ y = 2 * k * π - x :=
+begin
+  have := @complex.cos_eq_cos_iff x y,
+  rw [← complex.of_real_cos, ← complex.of_real_cos] at this,
+  norm_cast at this,
+  simp [this],
+end
+
+lemma sin_eq_sin_iff {x y : ℝ} :
+  sin x = sin y ↔ ∃ k : ℤ, y = 2 * k * π + x ∨ y = (2 * k + 1) * π - x :=
+begin
+  have := @complex.sin_eq_sin_iff x y,
+  rw [← complex.of_real_sin, ← complex.of_real_sin] at this,
+  norm_cast at this,
+  simp [this],
+end
+
 lemma has_deriv_at_tan {x : ℝ} (h : ∀ k : ℤ, x ≠ (2 * k + 1) * π / 2) :
   has_deriv_at tan (1 / (cos x)^2) x :=
 begin

src/data/complex/exponential.lean

@@ -695,6 +695,38 @@ by simp [sub_eq_add_neg, sin_add, sin_neg, cos_neg]
 lemma cos_sub : cos (x - y) = cos x * cos y + sin x * sin y :=
 by simp [sub_eq_add_neg, cos_add, sin_neg, cos_neg]
 
+theorem sin_sub_sin : sin x - sin y = 2 * sin((x - y)/2) * cos((x + y)/2) :=
+begin
+  have s1 := sin_add ((x + y) / 2) ((x - y) / 2),
+  have s2 := sin_sub ((x + y) / 2) ((x - y) / 2),
+  rw [div_add_div_same, add_sub, add_right_comm, add_sub_cancel, half_add_self] at s1,
+  rw [div_sub_div_same, ←sub_add, add_sub_cancel', half_add_self] at s2,
+  rw [s1, s2],
+  ring
+end
+
+theorem cos_sub_cos : cos x - cos y = -2 * sin((x + y)/2) * sin((x - y)/2) :=
+begin
+  have s1 := cos_add ((x + y) / 2) ((x - y) / 2),
+  have s2 := cos_sub ((x + y) / 2) ((x - y) / 2),
+  rw [div_add_div_same, add_sub, add_right_comm, add_sub_cancel, half_add_self] at s1,
+  rw [div_sub_div_same, ←sub_add, add_sub_cancel', half_add_self] at s2,
+  rw [s1, s2],
+  ring,
+end
+
+lemma cos_add_cos : cos x + cos y = 2 * cos ((x + y) / 2)  * cos ((x - y) / 2) :=
+begin
+  have h2 : (2:ℂ) ≠ 0 := by norm_num,
+  calc cos x + cos y = cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) : _
+  ... = (cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2))
+          + (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)) : _
+  ... = 2 * cos ((x + y) / 2) * cos ((x - y) / 2) : _,
+  { congr; field_simp [h2]; ring },
+  { rw [cos_add, cos_sub] },
+  ring,
+end
+
 lemma sin_conj : sin (conj x) = conj (sin x) :=
 by rw [← mul_left_inj' I_ne_zero, ← sinh_mul_I,
        ← conj_neg_I, ← conj.map_mul, ← conj.map_mul, sinh_conj,
@@ -873,6 +905,33 @@ by simp [sub_eq_add_neg, sin_add, sin_neg, cos_neg]
 lemma cos_sub : cos (x - y) = cos x * cos y + sin x * sin y :=
 by simp [sub_eq_add_neg, cos_add, sin_neg, cos_neg]
 
+lemma sin_sub_sin : sin x - sin y = 2 * sin((x - y)/2) * cos((x + y)/2) :=
+begin
+  rw ← of_real_inj,
+  simp only [sin, cos, of_real_sin_of_real_re, of_real_sub, of_real_add, of_real_div, of_real_mul,
+    of_real_one, of_real_bit0],
+  convert sin_sub_sin _ _;
+  norm_cast
+end
+
+theorem cos_sub_cos : cos x - cos y = -2 * sin((x + y)/2) * sin((x - y)/2) :=
+begin
+  rw ← of_real_inj,
+  simp only [cos, neg_mul_eq_neg_mul_symm, of_real_sin, of_real_sub, of_real_add,
+    of_real_cos_of_real_re, of_real_div, of_real_mul, of_real_one, of_real_neg, of_real_bit0],
+  convert cos_sub_cos _ _,
+  ring,
+end
+
+lemma cos_add_cos : cos x + cos y = 2 * cos ((x + y) / 2)  * cos ((x - y) / 2) :=
+begin
+  rw ← of_real_inj,
+  simp only [cos, of_real_sub, of_real_add, of_real_cos_of_real_re, of_real_div, of_real_mul,
+    of_real_one, of_real_bit0],
+  convert cos_add_cos _ _;
+  norm_cast,
+end
+
 lemma tan_eq_sin_div_cos : tan x = sin x / cos x :=
 if h : complex.cos x = 0 then by simp [sin, cos, tan, *, complex.tan, div_eq_mul_inv] at *
 else