From 538373cedd8622b6438d0c66eea176e19fa20d3c Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sat, 20 Jan 2024 17:20:12 -0600 Subject: [PATCH] =?UTF-8?q?feat(Trigonometric):=20add=20lemmas=20about=20`?= =?UTF-8?q?cos=20x=20=3D=20-1=20=E2=86=94=20=5F`=20etc?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../Trigonometric/Complex.lean | 29 +++++++++++++++++-- 1 file changed, 27 insertions(+), 2 deletions(-) diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean index 2ba8d14e5d27d..92711caa50931 100644 --- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean +++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean @@ -98,6 +98,22 @@ theorem sin_eq_sin_iff {x y : ℂ} : refine' exists_congr fun k => or_congr _ _ <;> refine' Eq.congr rfl _ <;> field_simp <;> ring #align complex.sin_eq_sin_iff Complex.sin_eq_sin_iff +theorem cos_eq_one_iff {x : ℂ} : cos x = 1 ↔ ∃ k : ℤ, k * (2 * π) = x := by + rw [← cos_zero, eq_comm, cos_eq_cos_iff] + simp [mul_assoc, mul_left_comm, eq_comm] + +theorem cos_eq_neg_one_iff {x : ℂ} : cos x = -1 ↔ ∃ k : ℤ, π + k * (2 * π) = x := by + rw [← neg_eq_iff_eq_neg, ← cos_sub_pi, cos_eq_one_iff] + simp only [eq_sub_iff_add_eq'] + +theorem sin_eq_one_iff {x : ℂ} : sin x = 1 ↔ ∃ k : ℤ, π / 2 + k * (2 * π) = x := by + rw [← cos_sub_pi_div_two, cos_eq_one_iff] + simp only [eq_sub_iff_add_eq'] + +theorem sin_eq_neg_one_iff {x : ℂ} : sin x = -1 ↔ ∃ k : ℤ, -(π / 2) + k * (2 * π) = x := by + rw [← neg_eq_iff_eq_neg, ← cos_add_pi_div_two, cos_eq_one_iff] + simp only [← sub_eq_neg_add, sub_eq_iff_eq_add] + theorem tan_add {x y : ℂ} (h : ((∀ k : ℤ, x ≠ (2 * k + 1) * π / 2) ∧ ∀ l : ℤ, y ≠ (2 * l + 1) * π / 2) ∨ (∃ k : ℤ, x = (2 * k + 1) * π / 2) ∧ ∃ l : ℤ, y = (2 * l + 1) * π / 2) : @@ -208,8 +224,8 @@ theorem cos_eq_zero_iff {θ : ℝ} : cos θ = 0 ↔ ∃ k : ℤ, θ = (2 * k + 1 mod_cast @Complex.cos_eq_zero_iff θ #align real.cos_eq_zero_iff Real.cos_eq_zero_iff -theorem cos_ne_zero_iff {θ : ℝ} : cos θ ≠ 0 ↔ ∀ k : ℤ, θ ≠ (2 * k + 1) * π / 2 := by - rw [← not_exists, not_iff_not, cos_eq_zero_iff] +theorem cos_ne_zero_iff {θ : ℝ} : cos θ ≠ 0 ↔ ∀ k : ℤ, θ ≠ (2 * k + 1) * π / 2 := + mod_cast @Complex.cos_ne_zero_iff θ #align real.cos_ne_zero_iff Real.cos_ne_zero_iff theorem cos_eq_cos_iff {x y : ℝ} : cos x = cos y ↔ ∃ k : ℤ, y = 2 * k * π + x ∨ y = 2 * k * π - x := @@ -221,6 +237,15 @@ theorem sin_eq_sin_iff {x y : ℝ} : mod_cast @Complex.sin_eq_sin_iff x y #align real.sin_eq_sin_iff Real.sin_eq_sin_iff +theorem cos_eq_neg_one_iff {x : ℝ} : cos x = -1 ↔ ∃ k : ℤ, π + k * (2 * π) = x := + mod_cast @Complex.cos_eq_neg_one_iff x + +theorem sin_eq_one_iff {x : ℝ} : sin x = 1 ↔ ∃ k : ℤ, π / 2 + k * (2 * π) = x := + mod_cast @Complex.sin_eq_one_iff x + +theorem sin_eq_neg_one_iff {x : ℝ} : sin x = -1 ↔ ∃ k : ℤ, -(π / 2) + k * (2 * π) = x := + mod_cast @Complex.sin_eq_neg_one_iff x + theorem lt_sin_mul {x : ℝ} (hx : 0 < x) (hx' : x < 1) : x < sin (π / 2 * x) := by simpa [mul_comm x] using strictConcaveOn_sin_Icc.2 ⟨le_rfl, pi_pos.le⟩ ⟨pi_div_two_pos.le, half_le_self pi_pos.le⟩