chore(polynomial/chebyshev): changes names of chebyshev₁ to chebyshev.T and chebyshev₂ to chebyshev.U (#6519)

Still have to write here what was changed (will be a long list). More or less this is just search and replace `chebyshev₁` for `chebyshev.T` and `chebyshev₂` for `chebyshev.U`.

* `polynomial.chebyshev₁` is now `polynomial.chebyshev.T`
* `polynomial.chebyshev₁_zero` is now `polynomial.chebyshev.T_zero`
* `polynomial.chebyshev₁_one` is now `polynomial.chebyshev.T_one`
* `polynomial.chebyshev₁_two` is now `polynomial.chebyshev.T_two`
* `polynomial.chebyshev₁_add_two` is now `polynomial.chebyshev.T_add_two`
* `polynomial.chebyshev₁_of_two_le` is now `polynomial.chebyshev.T_of_two_le`
* `polynomial.map_chebyshev₁` is now `polynomial.chebyshev.map_T`
* `polynomial.chebyshev₂` is now `polynomial.chebyshev.U`
* `polynomial.chebyshev₂_zero` is now `polynomial.chebyshev.U_zero`
* `polynomial.chebyshev₂_one` is now `polynomial.chebyshev.U_one`
* `polynomial.chebyshev₂_two` is now `polynomial.chebyshev.U_two`
* `polynomial.chebyshev₂_add_two` is now `polynomial.chebyshev.U_add_two`
* `polynomial.chebyshev₂_of_two_le` is now `polynomial.chebyshev.U_of_two_le`
* `polynomial.chebyshev₂_eq_X_mul_chebyshev₂_add_chebyshev₁` is now `polynomial.chebyshev.U_eq_X_mul_U_add_T`
* `polynomial.chebyshev₁_eq_chebyshev₂_sub_X_mul_chebyshev₂` is now `polynomial.chebyshev.T_eq_U_sub_X_mul_U`
* `polynomial.chebyshev₁_eq_X_mul_chebyshev₁_sub_pol_chebyshev₂` is now `polynomial.chebyshev.T_eq_X_mul_T_sub_pol_U`
* `polynomial.one_sub_X_pow_two_mul_chebyshev₂_eq_pol_in_chebyshev₁` is now `polynomial.chebyshev.one_sub_X_pow_two_mul_U_eq_pol_in_T`
* `polynomial.map_chebyshev₂` is now `polynomial.chebyshev.map_U`
* `polynomial.chebyshev₁_derivative_eq_chebyshev₂` is now `polynomial.chebyshev.T_derivative_eq_U`
* `polynomial.one_sub_X_pow_two_mul_derivative_chebyshev₁_eq_poly_in_chebyshev₁` is now `polynomial.chebyshev.one_sub_X_pow_two_mul_derivative_T_eq_poly_in_T`
* `polynomial.add_one_mul_chebyshev₁_eq_poly_in_chebyshev₂` is now `polynomial.chebyshev.add_one_mul_T_eq_poly_in_U`
* `polynomial.mul_chebyshev₁` is now `polynomial.chebyshev.mul_T`
* `polynomial.chebyshev₁_mul` is now `polynomial.chebyshev.T_mul`
* `polynomial.dickson_one_one_eq_chebyshev₁` is now `polynomial.dickson_one_one_eq_chebyshev_T`
* `polynomial.chebyshev₁_eq_dickson_one_one` is now `polynomial.chebyshev_T_eq_dickson_one_one`
* `chebyshev₁_complex_cos` is now `polynomial.chebyshev.T_complex_cos`
* `cos_nat_mul` is now `polynomial.chebyshev.cos_nat_mul`
* `chebyshev₂_complex_cos` is now `polynomial.chebyshev.U_complex_cos`
* `sin_nat_succ_mul` is now `polynomial.chebyshev.sin_nat_succ_mul`




Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>

Author: Julian-Kuelshammer

src/analysis/special_functions/trigonometric.lean

@@ -26,7 +26,7 @@ Many basic inequalities on trigonometric functions are established.
 The continuity and differentiability of the usual trigonometric functions are proved, and their
 derivatives are computed.
 
-* `polynomial.chebyshev₁_complex_cos`: the `n`-th Chebyshev polynomial evaluates on `complex.cos θ`
+* `polynomial.chebyshev.T_complex_cos`: the `n`-th Chebyshev polynomial evaluates on `complex.cos θ`
   to the value `n * complex.cos θ`.
 
 ## Tags
@@ -2864,20 +2864,20 @@ lemma differentiable.clog {f : E → ℂ} (h₁ : differentiable ℂ f)
 
 end log_deriv
 
-section chebyshev₁
+namespace polynomial.chebyshev
 
 open polynomial complex
 
 /-- The `n`-th Chebyshev polynomial of the first kind evaluates on `cos θ` to the
 value `cos (n * θ)`. -/
-lemma chebyshev₁_complex_cos (θ : ℂ) :
-  ∀ n, (chebyshev₁ ℂ n).eval (cos θ) = cos (n * θ)
-| 0       := by simp only [chebyshev₁_zero, eval_one, nat.cast_zero, zero_mul, cos_zero]
-| 1       := by simp only [eval_X, one_mul, chebyshev₁_one, nat.cast_one]
+lemma T_complex_cos (θ : ℂ) :
+  ∀ n, (T ℂ n).eval (cos θ) = cos (n * θ)
+| 0       := by simp only [T_zero, eval_one, nat.cast_zero, zero_mul, cos_zero]
+| 1       := by simp only [eval_X, one_mul, T_one, nat.cast_one]
 | (n + 2) :=
 begin
-  simp only [eval_X, eval_one, chebyshev₁_add_two, eval_sub, eval_bit0, nat.cast_succ, eval_mul],
-  rw [chebyshev₁_complex_cos (n + 1), chebyshev₁_complex_cos n],
+  simp only [eval_X, eval_one, T_add_two, eval_sub, eval_bit0, nat.cast_succ, eval_mul],
+  rw [T_complex_cos (n + 1), T_complex_cos n],
   have aux : sin θ * sin θ = 1 - cos θ * cos θ,
   { rw ← sin_sq_add_cos_sq θ, ring, },
   simp only [nat.cast_add, nat.cast_one, add_mul, cos_add, one_mul, sin_add, mul_assoc, aux],
@@ -2887,24 +2887,18 @@ end
 /-- `cos (n * θ)` is equal to the `n`-th Chebyshev polynomial of the first kind evaluated
 on `cos θ`. -/
 lemma cos_nat_mul (n : ℕ) (θ : ℂ) :
-  cos (n * θ) = (chebyshev₁ ℂ n).eval (cos θ) :=
-(chebyshev₁_complex_cos θ n).symm
-
-end chebyshev₁
-
-section chebyshev₂
-
-open polynomial complex
+  cos (n * θ) = (T ℂ n).eval (cos θ) :=
+(T_complex_cos θ n).symm
 
 /-- The `n`-th Chebyshev polynomial of the second kind evaluates on `cos θ` to the
 value `sin ((n+1) * θ) / sin θ`. -/
-lemma chebyshev₂_complex_cos (θ : ℂ) (n : ℕ) :
-  (chebyshev₂ ℂ n).eval (cos θ) * sin θ = sin ((n+1) * θ) :=
+lemma U_complex_cos (θ : ℂ) (n : ℕ) :
+  (U ℂ n).eval (cos θ) * sin θ = sin ((n+1) * θ) :=
 begin
   induction n with d hd,
-  { simp only [chebyshev₂_zero, nat.cast_zero, eval_one, mul_one, zero_add, one_mul] },
-  { rw chebyshev₂_eq_X_mul_chebyshev₂_add_chebyshev₁,
-    simp only [eval_add, eval_mul, eval_X, chebyshev₁_complex_cos, add_mul, mul_assoc, hd, one_mul],
+  { simp only [U_zero, nat.cast_zero, eval_one, mul_one, zero_add, one_mul] },
+  { rw U_eq_X_mul_U_add_T,
+    simp only [eval_add, eval_mul, eval_X, T_complex_cos, add_mul, mul_assoc, hd, one_mul],
     conv_rhs { rw [sin_add, mul_comm] },
     push_cast,
     simp only [add_mul, one_mul] }
@@ -2913,10 +2907,10 @@ end
 /-- `sin ((n + 1) * θ)` is equal to `sin θ` multiplied with the `n`-th Chebyshev polynomial of the
 second kind evaluated on `cos θ`. -/
 lemma sin_nat_succ_mul (n : ℕ) (θ : ℂ) :
-  sin ((n + 1) * θ) = (chebyshev₂ ℂ n).eval (cos θ) * sin θ :=
-(chebyshev₂_complex_cos θ n).symm
+  sin ((n + 1) * θ) = (U ℂ n).eval (cos θ) * sin θ :=
+(U_complex_cos θ n).symm
 
-end chebyshev₂
+end polynomial.chebyshev
 
 namespace real
 open_locale real