feat(analysis/special_functions/trigonometric/angle): to_real lemmas (

#17395)

Add a series of lemmas mainly about `real.angle.to_real` and twice angles, concluding with conditions for an angle and twice that angle to have the same sign (which is of use for proving that the base angles of an isosceles triangle are acute).

src/analysis/special_functions/trigonometric/angle.lean

@@ -71,6 +71,18 @@ begin
   simp [two_mul, sub_eq_add_neg]
 end
 
+@[simp] lemma two_nsmul_coe_div_two (θ : ℝ) : (2 : ℕ) • (↑(θ / 2) : angle) = θ :=
+by rw [←coe_nsmul, two_nsmul, add_halves]
+
+@[simp] lemma two_zsmul_coe_div_two (θ : ℝ) : (2 : ℤ) • (↑(θ / 2) : angle) = θ :=
+by rw [←coe_zsmul, two_zsmul, add_halves]
+
+@[simp] lemma two_nsmul_neg_pi_div_two : (2 : ℕ) • (↑(-π / 2) : angle) = π :=
+by rw [two_nsmul_coe_div_two, coe_neg, neg_coe_pi]
+
+@[simp] lemma two_zsmul_neg_pi_div_two : (2 : ℤ) • (↑(-π / 2) : angle) = π :=
+by rw [two_zsmul, ←two_nsmul, two_nsmul_neg_pi_div_two]
+
 lemma sub_coe_pi_eq_add_coe_pi (θ : angle) : θ - π = θ + π :=
 by rw [sub_eq_add_neg, neg_coe_pi]
 
@@ -536,6 +548,65 @@ lemma abs_to_real_eq_pi_div_two_iff {θ : angle} :
 by rw [abs_eq (div_nonneg real.pi_pos.le two_pos.le), ←neg_div, to_real_eq_pi_div_two_iff,
        to_real_eq_neg_pi_div_two_iff]
 
+lemma nsmul_to_real_eq_mul {n : ℕ} (h : n ≠ 0) {θ : angle} :
+  (n • θ).to_real = n * θ.to_real ↔ θ.to_real ∈ set.Ioc (-π / n) (π / n) :=
+begin
+  nth_rewrite 0 ←coe_to_real θ,
+  have h' : 0 < (n : ℝ), { exact_mod_cast nat.pos_of_ne_zero h },
+  rw [←coe_nsmul, nsmul_eq_mul, to_real_coe_eq_self_iff, set.mem_Ioc, div_lt_iff' h',
+      le_div_iff' h']
+end
+
+lemma two_nsmul_to_real_eq_two_mul {θ : angle} :
+  ((2 : ℕ) • θ).to_real = 2 * θ.to_real ↔ θ.to_real ∈ set.Ioc (-π / 2) (π / 2) :=
+by exact_mod_cast nsmul_to_real_eq_mul two_ne_zero
+
+lemma two_zsmul_to_real_eq_two_mul {θ : angle} :
+  ((2 : ℤ) • θ).to_real = 2 * θ.to_real ↔ θ.to_real ∈ set.Ioc (-π / 2) (π / 2) :=
+by rw [two_zsmul, ←two_nsmul, two_nsmul_to_real_eq_two_mul]
+
+lemma to_real_coe_eq_self_sub_two_mul_int_mul_pi_iff {θ : ℝ} {k : ℤ} :
+  (θ : angle).to_real = θ - 2 * k * π ↔ θ ∈ set.Ioc ((2 * k - 1 : ℝ) * π) ((2 * k + 1) * π) :=
+begin
+  rw [←sub_zero (θ : angle), ←zsmul_zero k, ←coe_two_pi, ←coe_zsmul, ←coe_sub,
+      zsmul_eq_mul, ←mul_assoc, mul_comm (k : ℝ), to_real_coe_eq_self_iff, set.mem_Ioc],
+  exact ⟨λ h, ⟨by linarith, by linarith⟩, λ h, ⟨by linarith, by linarith⟩⟩
+end
+
+lemma to_real_coe_eq_self_sub_two_pi_iff {θ : ℝ} :
+  (θ : angle).to_real = θ - 2 * π ↔ θ ∈ set.Ioc π (3 * π) :=
+by { convert @to_real_coe_eq_self_sub_two_mul_int_mul_pi_iff θ 1; norm_num }
+
+lemma to_real_coe_eq_self_add_two_pi_iff {θ : ℝ} :
+  (θ : angle).to_real = θ + 2 * π ↔ θ ∈ set.Ioc (-3 * π) (-π) :=
+by { convert @to_real_coe_eq_self_sub_two_mul_int_mul_pi_iff θ (-1); norm_num }
+
+lemma two_nsmul_to_real_eq_two_mul_sub_two_pi {θ : angle} :
+  ((2 : ℕ) • θ).to_real = 2 * θ.to_real - 2 * π ↔ π / 2 < θ.to_real :=
+begin
+  nth_rewrite 0 ←coe_to_real θ,
+  rw [←coe_nsmul, two_nsmul, ←two_mul, to_real_coe_eq_self_sub_two_pi_iff, set.mem_Ioc],
+  exact ⟨λ h, by linarith,
+         λ h, ⟨(div_lt_iff' (zero_lt_two' ℝ)).1 h, by linarith [pi_pos, to_real_le_pi θ]⟩⟩
+end
+
+lemma two_zsmul_to_real_eq_two_mul_sub_two_pi {θ : angle} :
+  ((2 : ℤ) • θ).to_real = 2 * θ.to_real - 2 * π ↔ π / 2 < θ.to_real :=
+by rw [two_zsmul, ←two_nsmul, two_nsmul_to_real_eq_two_mul_sub_two_pi]
+
+lemma two_nsmul_to_real_eq_two_mul_add_two_pi {θ : angle} :
+  ((2 : ℕ) • θ).to_real = 2 * θ.to_real + 2 * π ↔ θ.to_real ≤ -π / 2 :=
+begin
+  nth_rewrite 0 ←coe_to_real θ,
+  rw [←coe_nsmul, two_nsmul, ←two_mul, to_real_coe_eq_self_add_two_pi_iff, set.mem_Ioc],
+  refine ⟨λ h, by linarith,
+          λ h, ⟨by linarith [pi_pos, neg_pi_lt_to_real θ], (le_div_iff' (zero_lt_two' ℝ)).1 h⟩⟩
+end
+
+lemma two_zsmul_to_real_eq_two_mul_add_two_pi {θ : angle} :
+  ((2 : ℤ) • θ).to_real = 2 * θ.to_real + 2 * π ↔ θ.to_real ≤ -π / 2 :=
+by rw [two_zsmul, ←two_nsmul, two_nsmul_to_real_eq_two_mul_add_two_pi]
+
 @[simp] lemma sin_to_real (θ : angle) : real.sin θ.to_real = sin θ :=
 by conv_rhs { rw [← coe_to_real θ, sin_coe] }
 
@@ -759,6 +830,47 @@ begin
   exact sin_nonneg_of_nonneg_of_le_pi h0 hpi
 end
 
+lemma sign_two_nsmul_eq_sign_iff {θ : angle} :
+  ((2 : ℕ) • θ).sign = θ.sign ↔ (θ = π ∨ |θ.to_real| < π / 2) :=
+begin
+  by_cases hpi : θ = π, { simp [hpi] },
+  rw or_iff_right hpi,
+  refine ⟨λ h, _, λ h, _⟩,
+  { by_contra hle,
+    rw [not_lt, le_abs, le_neg] at hle,
+    have hpi' : θ.to_real ≠ π, { simpa using hpi },
+    rcases hle with hle | hle; rcases hle.eq_or_lt with heq | hlt,
+    { rw [←coe_to_real θ, ←heq] at h, simpa using h },
+    { rw [←sign_to_real hpi, sign_pos (pi_div_two_pos.trans hlt),
+          ←sign_to_real, two_nsmul_to_real_eq_two_mul_sub_two_pi.2 hlt, _root_.sign_neg] at h,
+      { simpa using h },
+      { rw ←mul_sub,
+        exact mul_neg_of_pos_of_neg two_pos (sub_neg.2 ((to_real_le_pi _).lt_of_ne hpi')) },
+      { intro he, simpa [he] using h } },
+    { rw [←coe_to_real θ, heq] at h, simpa using h },
+    { rw [←sign_to_real hpi,
+          _root_.sign_neg (hlt.trans (left.neg_neg_iff.2 pi_div_two_pos)),
+          ←sign_to_real] at h, swap, { intro he, simpa [he] using h },
+      rw ←neg_div at hlt,
+      rw [two_nsmul_to_real_eq_two_mul_add_two_pi.2 hlt.le, sign_pos] at h,
+      { simpa using h },
+      { linarith [neg_pi_lt_to_real θ] } } },
+  { have hpi' : (2 : ℕ) • θ ≠ π,
+    { rw [ne.def, two_nsmul_eq_pi_iff, not_or_distrib],
+      split,
+      { rintro rfl, simpa [pi_pos, div_pos, abs_of_pos] using h },
+      { rintro rfl,
+        rw [to_real_neg_pi_div_two] at h,
+        simpa [pi_pos, div_pos, neg_div, abs_of_pos] using h } },
+    rw [abs_lt, ←neg_div] at h,
+    rw [←sign_to_real hpi, ←sign_to_real hpi', two_nsmul_to_real_eq_two_mul.2 ⟨h.1, h.2.le⟩,
+        sign_mul, sign_pos (zero_lt_two' ℝ), one_mul] }
+end
+
+lemma sign_two_zsmul_eq_sign_iff {θ : angle} :
+  ((2 : ℤ) • θ).sign = θ.sign ↔ (θ = π ∨ |θ.to_real| < π / 2) :=
+by rw [two_zsmul, ←two_nsmul, sign_two_nsmul_eq_sign_iff]
+
 lemma continuous_at_sign {θ : angle} (h0 : θ ≠ 0) (hpi : θ ≠ π) : continuous_at sign θ :=
 (continuous_at_sign_of_ne_zero (sin_ne_zero_iff.2 ⟨h0, hpi⟩)).comp continuous_sin.continuous_at