chore(analysis/special_functions): moved trig vals out of real.pi, ad…

…ded new trig vals (#3497)

Moved trigonometric lemmas from real.pi to analysis.special_functions.trigonometric. Also added two new trig lemmas, tan_pi_div_four and arctan_one, to analysis.special_functions.trigonometric.

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Trig.20function.20values

src/analysis/special_functions/trigonometric.lean

@@ -832,6 +832,126 @@ begin
   norm_num, norm_num, apply pow_pos h
 end
 
+section cos_div_pow_two
+
+variable (x : ℝ)
+
+/-- the series `sqrt_two_add_series x n` is `sqrt(2 + sqrt(2 + ... ))` with `n` square roots,
+  starting with `x`. We define it here because `cos (pi / 2 ^ (n+1)) = sqrt_two_add_series 0 n / 2`
+-/
+@[simp] noncomputable def sqrt_two_add_series (x : ℝ) : ℕ → ℝ
+| 0     := x
+| (n+1) := sqrt (2 + sqrt_two_add_series n)
+
+lemma sqrt_two_add_series_zero : sqrt_two_add_series x 0 = x := by simp
+lemma sqrt_two_add_series_one : sqrt_two_add_series 0 1 = sqrt 2 := by simp
+lemma sqrt_two_add_series_two : sqrt_two_add_series 0 2 = sqrt (2 + sqrt 2) := by simp
+
+lemma sqrt_two_add_series_zero_nonneg : ∀(n : ℕ), 0 ≤ sqrt_two_add_series 0 n
+| 0     := le_refl 0
+| (n+1) := sqrt_nonneg _
+
+lemma sqrt_two_add_series_nonneg {x : ℝ} (h : 0 ≤ x) : ∀(n : ℕ), 0 ≤ sqrt_two_add_series x n
+| 0     := h
+| (n+1) := sqrt_nonneg _
+
+lemma sqrt_two_add_series_lt_two : ∀(n : ℕ), sqrt_two_add_series 0 n < 2
+| 0     := by norm_num
+| (n+1) :=
+  begin
+    refine lt_of_lt_of_le _ (le_of_eq $ sqrt_sqr $ le_of_lt two_pos),
+    rw [sqrt_two_add_series, sqrt_lt],
+    apply add_lt_of_lt_sub_left,
+    apply lt_of_lt_of_le (sqrt_two_add_series_lt_two n),
+    norm_num, apply add_nonneg, norm_num, apply sqrt_two_add_series_zero_nonneg, norm_num
+  end
+
+lemma sqrt_two_add_series_succ (x : ℝ) :
+  ∀(n : ℕ), sqrt_two_add_series x (n+1) = sqrt_two_add_series (sqrt (2 + x)) n
+| 0     := rfl
+| (n+1) := by rw [sqrt_two_add_series, sqrt_two_add_series_succ, sqrt_two_add_series]
+
+lemma sqrt_two_add_series_monotone_left {x y : ℝ} (h : x ≤ y) :
+  ∀(n : ℕ), sqrt_two_add_series x n ≤ sqrt_two_add_series y n
+| 0     := h
+| (n+1) :=
+  begin
+    rw [sqrt_two_add_series, sqrt_two_add_series],
+    apply sqrt_le_sqrt, apply add_le_add_left, apply sqrt_two_add_series_monotone_left
+  end
+
+@[simp] lemma cos_pi_over_two_pow : ∀(n : ℕ), cos (pi / 2 ^ (n+1)) = sqrt_two_add_series 0 n / 2
+| 0     := by simp
+| (n+1) :=
+  begin
+    symmetry, rw [div_eq_iff_mul_eq], symmetry,
+    rw [sqrt_two_add_series, sqrt_eq_iff_sqr_eq, mul_pow, cos_square, ←mul_div_assoc,
+      nat.add_succ, pow_succ, mul_div_mul_left, cos_pi_over_two_pow, add_mul],
+    congr, norm_num,
+    rw [mul_comm, pow_two, mul_assoc, ←mul_div_assoc, mul_div_cancel_left, ←mul_div_assoc,
+        mul_div_cancel_left],
+    norm_num, norm_num, norm_num,
+    apply add_nonneg, norm_num, apply sqrt_two_add_series_zero_nonneg, norm_num,
+    apply le_of_lt, apply cos_pos_of_neg_pi_div_two_lt_of_lt_pi_div_two,
+    { transitivity (0 : ℝ), rw neg_lt_zero, apply pi_div_two_pos,
+      apply div_pos pi_pos, apply pow_pos, norm_num },
+    apply div_lt_div' (le_refl pi) _ pi_pos _,
+    refine lt_of_le_of_lt (le_of_eq (pow_one _).symm) _,
+    apply pow_lt_pow, norm_num, apply nat.succ_lt_succ, apply nat.succ_pos, all_goals {norm_num}
+  end
+
+lemma sin_square_pi_over_two_pow (n : ℕ) :
+  sin (pi / 2 ^ (n+1)) ^ 2 = 1 - (sqrt_two_add_series 0 n / 2) ^ 2 :=
+by rw [sin_square, cos_pi_over_two_pow]
+
+lemma sin_square_pi_over_two_pow_succ (n : ℕ) :
+  sin (pi / 2 ^ (n+2)) ^ 2 = 1 / 2 - sqrt_two_add_series 0 n / 4 :=
+begin
+  rw [sin_square_pi_over_two_pow, sqrt_two_add_series, div_pow, sqr_sqrt, add_div, ←sub_sub],
+  congr, norm_num, norm_num, apply add_nonneg, norm_num, apply sqrt_two_add_series_zero_nonneg,
+end
+
+@[simp] lemma sin_pi_over_two_pow_succ (n : ℕ) :
+  sin (pi / 2 ^ (n+2)) = sqrt (2 - sqrt_two_add_series 0 n) / 2 :=
+begin
+  symmetry, rw [div_eq_iff_mul_eq], symmetry,
+  rw [sqrt_eq_iff_sqr_eq, mul_pow, sin_square_pi_over_two_pow_succ, sub_mul],
+  { congr, norm_num, rw [mul_comm], convert mul_div_cancel' _ _, norm_num, norm_num },
+  { rw [sub_nonneg], apply le_of_lt, apply sqrt_two_add_series_lt_two },
+  apply le_of_lt, apply mul_pos, apply sin_pos_of_pos_of_lt_pi,
+  { apply div_pos pi_pos, apply pow_pos, norm_num },
+  refine lt_of_lt_of_le _ (le_of_eq (div_one _)), rw [div_lt_div_left],
+  refine lt_of_le_of_lt (le_of_eq (pow_zero 2).symm) _,
+  apply pow_lt_pow, norm_num, apply nat.succ_pos, apply pi_pos,
+  apply pow_pos, all_goals {norm_num}
+end
+
+lemma cos_pi_div_four : cos (pi / 4) = sqrt 2 / 2 :=
+by { transitivity cos (pi / 2 ^ 2), congr, norm_num, simp }
+
+lemma sin_pi_div_four : sin (pi / 4) = sqrt 2 / 2 :=
+by { transitivity sin (pi / 2 ^ 2), congr, norm_num, simp }
+
+lemma cos_pi_div_eight : cos (pi / 8) = sqrt (2 + sqrt 2) / 2 :=
+by { transitivity cos (pi / 2 ^ 3), congr, norm_num, simp }
+
+lemma sin_pi_div_eight : sin (pi / 8) = sqrt (2 - sqrt 2) / 2 :=
+by { transitivity sin (pi / 2 ^ 3), congr, norm_num, simp }
+
+lemma cos_pi_div_sixteen : cos (pi / 16) = sqrt (2 + sqrt (2 + sqrt 2)) / 2 :=
+by { transitivity cos (pi / 2 ^ 4), congr, norm_num, simp }
+
+lemma sin_pi_div_sixteen : sin (pi / 16) = sqrt (2 - sqrt (2 + sqrt 2)) / 2 :=
+by { transitivity sin (pi / 2 ^ 4), congr, norm_num, simp }
+
+lemma cos_pi_div_thirty_two : cos (pi / 32) = sqrt (2 + sqrt (2 + sqrt (2 + sqrt 2))) / 2 :=
+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 }
+
+end cos_div_pow_two
+
 /-- The type of angles -/
 def angle : Type :=
 quotient_add_group.quotient (gmultiples (2 * π))
@@ -1068,6 +1188,13 @@ lemma div_sqrt_one_add_lt_one (x : ℝ) : x / sqrt (1 + x ^ 2) < 1 :=
 lemma neg_one_lt_div_sqrt_one_add (x : ℝ) : -1 < x / sqrt (1 + x ^ 2) :=
 (abs_lt.1 (abs_div_sqrt_one_add_lt _)).1
 
+@[simp] lemma tan_pi_div_four : tan (π / 4) = 1 :=
+begin
+  rw [tan_eq_sin_div_cos, cos_pi_div_four, sin_pi_div_four],
+  have h : (sqrt 2) / 2 > 0 := by cancel_denoms,
+  exact div_self (ne_of_gt h),
+end
+
 lemma tan_pos_of_pos_of_lt_pi_div_two {x : ℝ} (h0x : 0 < x) (hxp : x < π / 2) : 0 < tan x :=
 by rw tan_eq_sin_div_cos; exact div_pos (sin_pos_of_pos_of_lt_pi h0x (by linarith))
   (cos_pos_of_neg_pi_div_two_lt_of_lt_pi_div_two (by linarith) hxp)
@@ -1168,6 +1295,12 @@ tan_inj_of_lt_of_lt_pi_div_two (neg_pi_div_two_lt_arctan _)
 @[simp] lemma arctan_zero : arctan 0 = 0 :=
 by simp [arctan]
 
+@[simp] lemma arctan_one : arctan 1 = π / 4 :=
+begin
+  refine tan_inj_of_lt_of_lt_pi_div_two (neg_pi_div_two_lt_arctan 1) (arctan_lt_pi_div_two 1) _ _ _;
+  linarith [pi_pos, tan_arctan 1, tan_pi_div_four],
+end
+
 @[simp] lemma arctan_neg (x : ℝ) : arctan (-x) = - arctan x :=
 by simp [arctan, neg_div]
 

src/data/real/pi.lean

@@ -6,121 +6,6 @@ Authors: Floris van Doorn
 import analysis.special_functions.trigonometric
 
 namespace real
-variable (x : ℝ)
-
-/-- the series `sqrt_two_add_series x n` is `sqrt(2 + sqrt(2 + ... ))` with `n` square roots,
-  starting with `x`. We define it here because `cos (pi / 2 ^ (n+1)) = sqrt_two_add_series 0 n / 2`
--/
-@[simp] noncomputable def sqrt_two_add_series (x : ℝ) : ℕ → ℝ
-| 0     := x
-| (n+1) := sqrt (2 + sqrt_two_add_series n)
-
-lemma sqrt_two_add_series_zero : sqrt_two_add_series x 0 = x := by simp
-lemma sqrt_two_add_series_one : sqrt_two_add_series 0 1 = sqrt 2 := by simp
-lemma sqrt_two_add_series_two : sqrt_two_add_series 0 2 = sqrt (2 + sqrt 2) := by simp
-
-lemma sqrt_two_add_series_zero_nonneg : ∀(n : ℕ), 0 ≤ sqrt_two_add_series 0 n
-| 0     := le_refl 0
-| (n+1) := sqrt_nonneg _
-
-lemma sqrt_two_add_series_nonneg {x : ℝ} (h : 0 ≤ x) : ∀(n : ℕ), 0 ≤ sqrt_two_add_series x n
-| 0     := h
-| (n+1) := sqrt_nonneg _
-
-lemma sqrt_two_add_series_lt_two : ∀(n : ℕ), sqrt_two_add_series 0 n < 2
-| 0     := by norm_num
-| (n+1) :=
-  begin
-    refine lt_of_lt_of_le _ (le_of_eq $ sqrt_sqr $ le_of_lt two_pos),
-    rw [sqrt_two_add_series, sqrt_lt],
-    apply add_lt_of_lt_sub_left,
-    apply lt_of_lt_of_le (sqrt_two_add_series_lt_two n),
-    norm_num, apply add_nonneg, norm_num, apply sqrt_two_add_series_zero_nonneg, norm_num
-  end
-
-lemma sqrt_two_add_series_succ (x : ℝ) :
-  ∀(n : ℕ), sqrt_two_add_series x (n+1) = sqrt_two_add_series (sqrt (2 + x)) n
-| 0     := rfl
-| (n+1) := by rw [sqrt_two_add_series, sqrt_two_add_series_succ, sqrt_two_add_series]
-
-lemma sqrt_two_add_series_monotone_left {x y : ℝ} (h : x ≤ y) :
-  ∀(n : ℕ), sqrt_two_add_series x n ≤ sqrt_two_add_series y n
-| 0     := h
-| (n+1) :=
-  begin
-    rw [sqrt_two_add_series, sqrt_two_add_series],
-    apply sqrt_le_sqrt, apply add_le_add_left, apply sqrt_two_add_series_monotone_left
-  end
-
-@[simp] lemma cos_pi_over_two_pow : ∀(n : ℕ), cos (pi / 2 ^ (n+1)) = sqrt_two_add_series 0 n / 2
-| 0     := by simp
-| (n+1) :=
-  begin
-    symmetry, rw [div_eq_iff_mul_eq], symmetry,
-    rw [sqrt_two_add_series, sqrt_eq_iff_sqr_eq, mul_pow, cos_square, ←mul_div_assoc,
-      nat.add_succ, pow_succ, mul_div_mul_left, cos_pi_over_two_pow, add_mul],
-    congr, norm_num,
-    rw [mul_comm, pow_two, mul_assoc, ←mul_div_assoc, mul_div_cancel_left, ←mul_div_assoc,
-        mul_div_cancel_left],
-    norm_num, norm_num, norm_num,
-    apply add_nonneg, norm_num, apply sqrt_two_add_series_zero_nonneg, norm_num,
-    apply le_of_lt, apply cos_pos_of_neg_pi_div_two_lt_of_lt_pi_div_two,
-    { transitivity (0 : ℝ), rw neg_lt_zero, apply pi_div_two_pos,
-      apply div_pos pi_pos, apply pow_pos, norm_num },
-    apply div_lt_div' (le_refl pi) _ pi_pos _,
-    refine lt_of_le_of_lt (le_of_eq (pow_one _).symm) _,
-    apply pow_lt_pow, norm_num, apply nat.succ_lt_succ, apply nat.succ_pos, all_goals {norm_num}
-  end
-
-lemma sin_square_pi_over_two_pow (n : ℕ) :
-  sin (pi / 2 ^ (n+1)) ^ 2 = 1 - (sqrt_two_add_series 0 n / 2) ^ 2 :=
-by rw [sin_square, cos_pi_over_two_pow]
-
-lemma sin_square_pi_over_two_pow_succ (n : ℕ) :
-  sin (pi / 2 ^ (n+2)) ^ 2 = 1 / 2 - sqrt_two_add_series 0 n / 4 :=
-begin
-  rw [sin_square_pi_over_two_pow, sqrt_two_add_series, div_pow, sqr_sqrt, add_div, ←sub_sub],
-  congr, norm_num, norm_num, apply add_nonneg, norm_num, apply sqrt_two_add_series_zero_nonneg,
-end
-
-@[simp] lemma sin_pi_over_two_pow_succ (n : ℕ) :
-  sin (pi / 2 ^ (n+2)) = sqrt (2 - sqrt_two_add_series 0 n) / 2 :=
-begin
-  symmetry, rw [div_eq_iff_mul_eq], symmetry,
-  rw [sqrt_eq_iff_sqr_eq, mul_pow, sin_square_pi_over_two_pow_succ, sub_mul],
-  { congr, norm_num, rw [mul_comm], convert mul_div_cancel' _ _, norm_num, norm_num },
-  { rw [sub_nonneg], apply le_of_lt, apply sqrt_two_add_series_lt_two },
-  apply le_of_lt, apply mul_pos, apply sin_pos_of_pos_of_lt_pi,
-  { apply div_pos pi_pos, apply pow_pos, norm_num },
-  refine lt_of_lt_of_le _ (le_of_eq (div_one _)), rw [div_lt_div_left],
-  refine lt_of_le_of_lt (le_of_eq (pow_zero 2).symm) _,
-  apply pow_lt_pow, norm_num, apply nat.succ_pos, apply pi_pos,
-  apply pow_pos, all_goals {norm_num}
-end
-
-lemma cos_pi_div_four : cos (pi / 4) = sqrt 2 / 2 :=
-by { transitivity cos (pi / 2 ^ 2), congr, norm_num, simp }
-
-lemma sin_pi_div_four : sin (pi / 4) = sqrt 2 / 2 :=
-by { transitivity sin (pi / 2 ^ 2), congr, norm_num, simp }
-
-lemma cos_pi_div_eight : cos (pi / 8) = sqrt (2 + sqrt 2) / 2 :=
-by { transitivity cos (pi / 2 ^ 3), congr, norm_num, simp }
-
-lemma sin_pi_div_eight : sin (pi / 8) = sqrt (2 - sqrt 2) / 2 :=
-by { transitivity sin (pi / 2 ^ 3), congr, norm_num, simp }
-
-lemma cos_pi_div_sixteen : cos (pi / 16) = sqrt (2 + sqrt (2 + sqrt 2)) / 2 :=
-by { transitivity cos (pi / 2 ^ 4), congr, norm_num, simp }
-
-lemma sin_pi_div_sixteen : sin (pi / 16) = sqrt (2 - sqrt (2 + sqrt 2)) / 2 :=
-by { transitivity sin (pi / 2 ^ 4), congr, norm_num, simp }
-
-lemma cos_pi_div_thirty_two : cos (pi / 32) = sqrt (2 + sqrt (2 + sqrt (2 + sqrt 2))) / 2 :=
-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 }
 
 lemma pi_gt_sqrt_two_add_series (n : ℕ) : 2 ^ (n+1) * sqrt (2 - sqrt_two_add_series 0 n) < pi :=
 begin
@@ -160,7 +45,7 @@ begin
   apply pow_ne_zero, norm_num, norm_num
 end
 
-/-- From an upper bound on `sqrt_two_add_series 0 n = 2 cos (pi / 2 ^ (n+1))` of the form 
+/-- From an upper bound on `sqrt_two_add_series 0 n = 2 cos (pi / 2 ^ (n+1))` of the form
 `sqrt_two_add_series 0 n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2)`, one can deduce the lower bound `a < pi`
 thanks to basic trigonometric inequalities as expressed in `pi_gt_sqrt_two_add_series`. -/
 theorem pi_lower_bound_start (n : ℕ) {a}