feat(*): polar co-ordinates, de moivre, trig identities, quotient group for angles (#745)

* feat(algebra/group_power): re-PRing polar co-ords

* Update group_power.lean

* feat(analysis/exponential): re-PRing polar stuff

* feat(data.complex.exponential): re-PR polar stuff

* fix(analysis.exponential): stylistic

* fix(data.complex.exponential): stylistic

* fix(analysis/exponential.lean): angle_eq_iff_two_pi_dvd_sub

* fix(analysis/exponential): angle_eq_iff_two_pi_dvd_sub

Author: abhimanyupallavisudhir

src/algebra/group_power.lean

@@ -521,6 +521,24 @@ theorem pow_nonneg {a : α} (H : 0 ≤ a) : ∀ (n : ℕ), 0 ≤ a ^ n
 | 0     := zero_le_one
 | (n+1) := mul_nonneg H (pow_nonneg _)
 
+theorem pow_lt_pow_of_lt_left {x y : α} {n : ℕ} (Hxy : x < y) (Hxpos : 0 ≤ x) (Hnpos : 0 < n) : x ^ n < y ^ n :=
+begin
+  cases lt_or_eq_of_le Hxpos,
+  { rw ←nat.sub_add_cancel Hnpos,
+    induction (n - 1), { simpa only [pow_one] },
+    rw [pow_add, pow_add, nat.succ_eq_add_one, pow_one, pow_one],
+    apply mul_lt_mul ih (le_of_lt Hxy) h (le_of_lt (pow_pos (lt_trans h Hxy) _)) },
+  { rw [←h, zero_pow Hnpos], apply pow_pos (by rwa ←h at Hxy : 0 < y),}
+end
+
+theorem pow_right_inj {x y : α} {n : ℕ} (Hxpos : 0 ≤ x) (Hypos : 0 ≤ y) (Hnpos : 0 < n) (Hxyn : x ^ n = y ^ n) : x = y :=
+begin
+  rcases lt_trichotomy x y with hxy | rfl | hyx,
+  { exact absurd Hxyn (ne_of_lt (pow_lt_pow_of_lt_left hxy Hxpos Hnpos)) },
+  { refl },
+  { exact absurd Hxyn (ne_of_gt (pow_lt_pow_of_lt_left hyx Hypos Hnpos)) },
+end
+
 theorem one_le_pow_of_one_le {a : α} (H : 1 ≤ a) : ∀ (n : ℕ), 1 ≤ a ^ n
 | 0     := le_refl _
 | (n+1) := by simpa only [mul_one] using mul_le_mul H (one_le_pow_of_one_le n)

src/analysis/exponential.lean

@@ -1,9 +1,9 @@
 /-
 Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Chris Hughes
+Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo
 -/
-import topology.instances.complex tactic.linarith data.complex.exponential
+import topology.instances.complex tactic.linarith data.complex.exponential group_theory.quotient_group
 
 open finset filter metric
 
@@ -309,6 +309,15 @@ by rw [← mul_self_eq_one_iff (cos x), ← sin_pow_two_add_cos_pow_two 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
@@ -320,6 +329,18 @@ lemma cos_eq_one_iff (x : ℝ) : cos x = 1 ↔ ∃ n : ℤ, (n : ℝ) * (2 * π)
         exact absurd h (by norm_num))⟩,
   λ ⟨n, hn⟩, hn ▸ cos_int_mul_two_pi _⟩
 
+theorem cos_eq_zero_iff {θ : ℝ} : cos θ = 0 ↔ ∃ k : ℤ, θ = (2 * k + 1) * pi / 2 :=
+begin
+  rw [←real.sin_pi_div_two_sub, sin_eq_zero_iff],
+  split,
+  { rintro ⟨n, hn⟩, existsi -n,
+    rw [int.cast_neg, add_mul, add_div, mul_assoc, mul_div_cancel_left _ two_ne_zero,
+        one_mul, ←neg_mul_eq_neg_mul, hn, neg_sub, sub_add_cancel] },
+  { rintro ⟨n, hn⟩, existsi -n,
+    rw [hn, add_mul, one_mul, add_div, mul_assoc, mul_div_cancel_left _ two_ne_zero,
+        sub_add_eq_sub_sub_swap, sub_self, zero_sub, neg_mul_eq_neg_mul, int.cast_neg] }
+end
+
 lemma cos_eq_one_iff_of_lt_of_lt {x : ℝ} (hx₁ : -(2 * π) < x) (hx₂ : x < 2 * π) : cos x = 1 ↔ x = 0 :=
 ⟨λ h, let ⟨n, hn⟩ := (cos_eq_one_iff x).1 h in
     begin
@@ -332,6 +353,11 @@ 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) (hx₂ : x ≤ π / 2)
   (hy₁ : 0 ≤ y) (hy₂ : y ≤ π / 2) (hxy : x < y) : cos y < cos x :=
 calc cos y = cos x * cos (y - x) - sin x * sin (y - x) :
@@ -400,6 +426,90 @@ lemma exists_sin_eq {x : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) : ∃ y, -(π
   (by rwa [sin_neg, sin_pi_div_two]) (by rwa sin_pi_div_two)
   (le_trans (neg_nonpos.2 (le_of_lt pi_div_two_pos)) (le_of_lt pi_div_two_pos))
 
+namespace angle
+
+/-- The type of angles -/
+def angle : Type :=
+quotient_add_group.quotient (gmultiples (2 * π))
+
+instance angle.add_comm_group : add_comm_group angle :=
+quotient_add_group.add_comm_group _
+
+instance angle.has_coe : has_coe ℝ angle :=
+⟨quotient.mk'⟩
+
+instance angle.is_add_group_hom : is_add_group_hom (coe : ℝ → angle) :=
+@quotient_add_group.is_add_group_hom _ _ _ (normal_add_subgroup_of_add_comm_group _)
+
+@[simp] lemma coe_zero : ↑(0 : ℝ) = (0 : angle) := rfl
+@[simp] lemma coe_add (x y : ℝ) : ↑(x + y : ℝ) = (↑x + ↑y : angle) := rfl
+@[simp] lemma coe_neg (x : ℝ) : ↑(-x : ℝ) = -(↑x : angle) := rfl
+@[simp] lemma coe_sub (x y : ℝ) : ↑(x - y : ℝ) = (↑x - ↑y : angle) := rfl
+@[simp] lemma coe_gsmul (x : ℝ) (n : ℤ) : ↑(gsmul n x : ℝ) = gsmul n (↑x : angle) := is_add_group_hom.gsmul _ _ _
+@[simp] lemma coe_two_pi : ↑(2 * π : ℝ) = (0 : angle) :=
+quotient.sound' ⟨-1, by dsimp only; rw [neg_one_gsmul, add_zero]⟩
+
+lemma angle_eq_iff_two_pi_dvd_sub {ψ θ : ℝ} : (θ : angle) = ψ ↔ ∃ k : ℤ, θ - ψ = 2 * π * k :=
+by simp only [quotient_add_group.eq, gmultiples, set.mem_range, gsmul_eq_mul', (sub_eq_neg_add _ _).symm, eq_comm]
+
+theorem cos_eq_iff_eq_or_eq_neg {θ ψ : ℝ} : cos θ = cos ψ ↔ (θ : angle) = ψ ∨ (θ : angle) = -ψ :=
+begin
+  split,
+  { intro Hcos,
+    rw [←sub_eq_zero, cos_sub_cos, mul_eq_zero, mul_eq_zero, neg_eq_zero, eq_false_intro two_ne_zero,
+        false_or, sin_eq_zero_iff, sin_eq_zero_iff] at Hcos,
+    rcases Hcos with ⟨n, hn⟩ | ⟨n, hn⟩,
+    { right,
+      rw [eq_div_iff_mul_eq _ _ two_ne_zero, ← sub_eq_iff_eq_add] at hn,
+      rw [← hn, coe_sub, eq_neg_iff_add_eq_zero, sub_add_cancel, mul_assoc,
+          ← gsmul_eq_mul, coe_gsmul, mul_comm, coe_two_pi, gsmul_zero] },
+    { left,
+      rw [eq_div_iff_mul_eq _ _ two_ne_zero, eq_sub_iff_add_eq] at hn,
+      rw [← hn, coe_add, mul_assoc,
+          ← gsmul_eq_mul, coe_gsmul, mul_comm, coe_two_pi, gsmul_zero, zero_add] } },
+  { rw [angle_eq_iff_two_pi_dvd_sub, ← coe_neg, angle_eq_iff_two_pi_dvd_sub], 
+    rintro (⟨k, H⟩ | ⟨k, H⟩),
+    rw [← sub_eq_zero_iff_eq, cos_sub_cos, H, mul_assoc 2 π k, mul_div_cancel_left _ two_ne_zero, 
+      mul_comm π _, sin_int_mul_pi, mul_zero],
+    rw [←sub_eq_zero_iff_eq, cos_sub_cos, ← sub_neg_eq_add, H, mul_assoc 2 π k, 
+      mul_div_cancel_left _ two_ne_zero, mul_comm π _, sin_int_mul_pi, mul_zero, zero_mul] }
+end
+
+theorem sin_eq_iff_eq_or_add_eq_pi {θ ψ : ℝ} : sin θ = sin ψ ↔ (θ : angle) = ψ ∨ (θ : angle) + ψ = π :=
+begin
+  split,
+  { intro Hsin, rw [← cos_pi_div_two_sub, ← cos_pi_div_two_sub] at Hsin,
+    cases cos_eq_iff_eq_or_eq_neg.mp Hsin with h h,
+    { left, rw coe_sub at h, exact sub_left_inj.1 h },
+      right, rw [coe_sub, coe_sub, eq_neg_iff_add_eq_zero, add_sub,
+      sub_add_eq_add_sub, ← coe_add, add_halves, sub_sub, sub_eq_zero] at h,
+    exact h.symm },
+  { rw [angle_eq_iff_two_pi_dvd_sub, ←eq_sub_iff_add_eq, ←coe_sub, angle_eq_iff_two_pi_dvd_sub], 
+    rintro (⟨k, H⟩ | ⟨k, H⟩),
+    rw [← sub_eq_zero_iff_eq, sin_sub_sin, H, mul_assoc 2 π k, mul_div_cancel_left _ two_ne_zero,
+      mul_comm π _, sin_int_mul_pi, mul_zero, zero_mul],
+    have H' : θ + ψ = (2 * k) * π + π := by rwa [←sub_add, sub_add_eq_add_sub, sub_eq_iff_eq_add, 
+      mul_assoc, mul_comm π _, ←mul_assoc] at H,
+    rw [← sub_eq_zero_iff_eq, sin_sub_sin, H', add_div, mul_assoc 2 _ π, mul_div_cancel_left _ two_ne_zero, 
+      cos_add_pi_div_two, sin_int_mul_pi, neg_zero, mul_zero] }
+end
+
+theorem cos_sin_inj {θ ψ : ℝ} (Hcos : cos θ = cos ψ) (Hsin : sin θ = sin ψ) : (θ : angle) = ψ :=
+begin
+  cases cos_eq_iff_eq_or_eq_neg.mp Hcos with hc hc, { exact hc },
+  cases sin_eq_iff_eq_or_add_eq_pi.mp Hsin with hs hs, { exact hs },
+  rw [eq_neg_iff_add_eq_zero, hs] at hc,
+  cases quotient.exact' hc with n hn, dsimp only at hn,
+  rw [← neg_one_mul, add_zero, ← sub_eq_zero_iff_eq, gsmul_eq_mul, ← mul_assoc, ← sub_mul,
+      mul_eq_zero, eq_false_intro (ne_of_gt pi_pos), or_false, sub_neg_eq_add,
+      ← int.cast_zero, ← int.cast_one, ← int.cast_bit0, ← int.cast_mul, ← int.cast_add, int.cast_inj] at hn,
+  have : (n * 2 + 1) % (2:ℤ) = 0 % (2:ℤ) := congr_arg (%(2:ℤ)) hn,
+  rw [add_comm, int.add_mul_mod_self] at this,
+  exact absurd this one_ne_zero
+end
+
+end angle
+
 /-- Inverse of the `sin` function, returns values in the range `-π / 2 ≤ arcsin x` and `arcsin x ≤ π / 2`.
   If the argument is not between `-1` and `1` it defaults to `0` -/
 noncomputable def arcsin (x : ℝ) : ℝ :=

src/data/complex/exponential.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Chris Hughes
+Authors: Chris Hughes, Abhimanyu Pallavi Sudhir
 -/
 import algebra.archimedean
 import data.nat.choose data.complex.basic
@@ -394,6 +394,10 @@ by rw lim_mul_lim;
   exact eq.symm (lim_eq_lim_of_equiv (by dsimp; simp only [hj];
     exact cauchy_product (is_cau_abs_exp x) (is_cau_exp y)))
 
+lemma exp_nat_mul (x : ℂ) : ∀ n : ℕ, exp(n*x) = (exp x)^n
+| 0 := by rw [nat.cast_zero, zero_mul, exp_zero, pow_zero]
+| (nat.succ n) := by rw [pow_succ', nat.cast_add_one, add_mul, exp_add, ←exp_nat_mul, one_mul]
+
 lemma exp_ne_zero : exp x ≠ 0 :=
 λ h, @zero_ne_one ℂ _ $
   by rw [← exp_zero, ← add_neg_self x, exp_add, h]; simp
@@ -556,6 +560,14 @@ by rw [exp_add, exp_mul_I]
 lemma exp_eq_exp_re_mul_sin_add_cos : exp x = exp x.re * (cos x.im + sin x.im * I) :=
 by rw [← exp_add_mul_I, re_add_im]
 
+theorem cos_add_sin_mul_I_pow (n : ℕ) (z : ℂ) : (cos z + sin z * I) ^ n = cos (↑n * z) + sin (↑n * z) * I :=
+begin
+  rw [← exp_mul_I, ← exp_mul_I],
+  induction n with n ih,
+  { rw [pow_zero, nat.cast_zero, zero_mul, zero_mul, exp_zero] },
+  { rw [pow_succ', ih, nat.cast_succ, add_mul, add_mul, one_mul, exp_add] }
+end
+
 @[simp] lemma sinh_zero : sinh 0 = 0 := by simp [sinh]
 
 @[simp] lemma sinh_neg : sinh (-x) = -sinh x :=
@@ -658,6 +670,10 @@ by simp [real.exp]
 lemma exp_add : exp (x + y) = exp x * exp y :=
 by simp [exp_add, exp]
 
+lemma exp_nat_mul (x : ℝ) : ∀ n : ℕ, exp(n*x) = (exp x)^n
+| 0 := by rw [nat.cast_zero, zero_mul, exp_zero, pow_zero]
+| (nat.succ n) := by rw [pow_succ', nat.cast_add_one, add_mul, exp_add, ←exp_nat_mul, one_mul]
+
 lemma exp_ne_zero : exp x ≠ 0 :=
 λ h, exp_ne_zero x $ by rw [exp, ← of_real_inj] at h; simp * at *