feat(ring_theory/polynomial/chebyshev/defs): Chebyshev polynomials of…

… the second kind (#5793)

This will define Chebyshev polynomials of the second kind and introduce some basic properties:

- [x] Define Chebyshev polynomials of the second kind.
- [x] Relate Chebyshev polynomials of the first and second kind through recursive formulae
- [x] Prove trigonometric identity regarding Chebyshev polynomials of the second kind
- [x] Compute the derivative of the Chebyshev polynomials of the first kind in terms of the Chebyshev polynomials of the second kind. 
- [x] Compute the derivative of the Chebyshev polynomials of the second kind in terms of the Chebyshev polynomials of the first kind.



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

docs/references.bib

@@ -523,3 +523,12 @@ @misc{scholze2011perfectoid
       archivePrefix={arXiv},
       primaryClass={math.AG}
 }
+
+@misc{ponton2020chebyshev,
+      title={Roots of {C}hebyshev polynomials: a purely algebraic approach},
+      author={Lionel Ponton},
+      year={2020}
+      eprint={2008.03575}
+      archivePrefix={arXiv},
+      primaryClass={math.NT}
+}

src/analysis/special_functions/trigonometric.lean

@@ -2561,7 +2561,8 @@ section chebyshev₁
 
 open polynomial complex
 
-/-- the `n`-th Chebyshev polynomial evaluates on `cos θ` to the value `cos (n * θ)`. -/
+/-- 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]
@@ -2576,13 +2577,40 @@ begin
   ring,
 end
 
-/-- `cos (n * θ)` is equal to the `n`-th Chebyshev polynomial evaluated on `cos θ`. -/
+/-- `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
+
+/-- 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) * θ) :=
+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],
+    conv_rhs { rw [sin_add, mul_comm] },
+    push_cast,
+    simp only [add_mul, one_mul] }
+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
+
+end chebyshev₂
+
 namespace real
 open_locale real
 

src/ring_theory/polynomial/chebyshev/defs.lean

@@ -4,32 +4,52 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
 
-import data.polynomial.eval
+import data.polynomial.derivative
+import tactic.ring
 
 /-!
 # Chebyshev polynomials
 
 The Chebyshev polynomials are two families of polynomials indexed by `ℕ`,
 with integral coefficients.
-In this file, we only consider Chebyshev polynomials of the first kind.
 
 See the file `ring_theory.polynomial.chebyshev.basic` for more properties.
 
-## Main declarations
+## Main definitions
 
 * `polynomial.chebyshev₁`: the Chebyshev polynomials of the first kind.
+* `polynomial.chebyshev₂`: the Chebyshev polynomials of the second kind.
 * `polynomial.lambdashev`: a variant on the Chebyshev polynomials that define a Lambda structure
   on `polynomial ℤ`.
 
+## Main statements
+
+* The formal derivative of the Chebyshev polynomials of the first kind is a scalar multiple of the
+  Chebyshev polynomials of the second kind.
+
 ## Implementation details
 
 In this file we only give definitions and some very elementary simp-lemmas.
 This way, we can import this file in `analysis.special_functions.trigonometric`,
 and import that file in turn, in `ring_theory.polynomial.chebyshev.basic`.
 
+## References
+
+[Lionel Ponton, _Roots of the Chebyshev polynomials: A purely algebraic approach_]
+[ponton2020chebyshev]
+
 ## TODO
 
-Add Chebyshev polynomials of the second kind.
+* Redefine and/or relate the definition of Chebyshev polynomials to `linear_recurrence`.
+* Add explicit formula involving square roots for Chebyshev polynomials
+  `ring_theory.polynomial.chebyshev.basic`.
+* Compute zeroes and extrema of Chebyshev polynomials.
+* Prove that the roots of the Chebyshev polynomials (except 0) are irrational.
+* Prove minimax properties of Chebyshev polynomials.
+* Define a variant of Chebyshev polynomials of the second kind removing the 2
+  (sometimes Dickson polynomials of the second kind) or even more general Dickson polynomials.
+* Prove that the adjacency matrices of simply laced Dynkin diagrams are precisely the adjacency
+  matrices of simple connected graphs which annihilate the Dickson polynomials.
 -/
 
 
@@ -112,4 +132,162 @@ begin
 end
 
 
+end polynomial
+
+namespace polynomial
+
+variables (R S : Type*) [comm_ring R] [comm_ring S]
+
+/-- `chebyshev₂ n` is the `n`-th Chebyshev polynomial of the second kind -/
+noncomputable def chebyshev₂ : ℕ → polynomial R
+| 0       := 1
+| 1       := 2 * X
+| (n + 2) := 2 * X * chebyshev₂ (n + 1) - chebyshev₂ n
+
+@[simp] lemma chebyshev₂_zero : chebyshev₂ R 0 = 1 := rfl
+@[simp] lemma chebyshev₂_one : chebyshev₂ R 1 = 2 * X := rfl
+lemma chebyshev₂_two : chebyshev₂ R 2 = 4 * X ^ 2 - 1 :=
+by { simp only [chebyshev₂], ring, }
+
+@[simp] lemma chebyshev₂_add_two (n : ℕ) :
+  chebyshev₂ R (n + 2) = 2 * X * chebyshev₂ R (n + 1) - chebyshev₂ R n :=
+by rw chebyshev₂
+
+lemma chebyshev₂_of_two_le (n : ℕ) (h : 2 ≤ n) :
+  chebyshev₂ R n = 2 * X * chebyshev₂ R (n - 1) - chebyshev₂ R (n - 2) :=
+begin
+  obtain ⟨n, rfl⟩ := nat.exists_eq_add_of_le h,
+  rw add_comm,
+  exact chebyshev₂_add_two R n
+end
+
+lemma chebyshev₂_eq_X_mul_chebyshev₂_add_chebyshev₁ :
+  ∀ (n : ℕ), chebyshev₂ R (n+1) = X * chebyshev₂ R n + chebyshev₁ R (n+1)
+| 0        := by { simp only [chebyshev₂_zero, chebyshev₂_one, chebyshev₁_one], ring }
+| 1        := by { simp only [chebyshev₂_one, chebyshev₁_two, chebyshev₂_two], ring }
+| (n + 2)  :=
+  calc chebyshev₂ R (n + 2 + 1) = 2 * X * (X * chebyshev₂ R (n + 1) + chebyshev₁ R (n + 2))
+                                          - (X * chebyshev₂ R n + chebyshev₁ R (n + 1)) :
+            by simp only [chebyshev₂_add_two, chebyshev₂_eq_X_mul_chebyshev₂_add_chebyshev₁ n,
+                                chebyshev₂_eq_X_mul_chebyshev₂_add_chebyshev₁ (n + 1)]
+  ... = X * (2 * X * chebyshev₂ R (n + 1) - chebyshev₂ R n)
+          + (2 * X * chebyshev₁ R (n + 2) - chebyshev₁ R (n + 1)) :
+            by ring
+  ... = X * chebyshev₂ R (n + 2) + chebyshev₁ R (n + 2 + 1) :
+            by simp only [chebyshev₂_add_two, chebyshev₁_add_two]
+
+lemma chebyshev₁_eq_chebyshev₂_sub_X_mul_chebyshev₂ (n : ℕ) :
+  chebyshev₁ R (n+1) = chebyshev₂ R (n+1) - X * chebyshev₂ R n :=
+by rw [chebyshev₂_eq_X_mul_chebyshev₂_add_chebyshev₁, add_comm (X * chebyshev₂ R n), add_sub_cancel]
+
+
+lemma chebyshev₁_eq_X_mul_chebyshev₁_sub_pol_chebyshev₂ :
+  ∀ (n : ℕ), chebyshev₁ R (n+2) = X * chebyshev₁ R (n+1) - (1 - X ^ 2) * chebyshev₂ R n
+| 0        := by { simp only [chebyshev₁_one, chebyshev₁_two, chebyshev₂_zero], ring }
+| 1        := by { simp only [chebyshev₁_add_two, chebyshev₁_zero, chebyshev₁_add_two,
+                              chebyshev₂_one, chebyshev₁_one], ring }
+| (n + 2)  :=
+calc chebyshev₁ R (n + 2 + 2)
+    = 2 * X * chebyshev₁ R (n + 2 + 1) - chebyshev₁ R (n + 2) : chebyshev₁_add_two _ _
+... = 2 * X * (X * chebyshev₁ R (n + 2) - (1 - X ^ 2) * chebyshev₂ R (n + 1))
+      - (X * chebyshev₁ R (n + 1) - (1 - X ^ 2) * chebyshev₂ R n) :
+            by simp only [chebyshev₁_eq_X_mul_chebyshev₁_sub_pol_chebyshev₂]
+... = X * (2 * X * chebyshev₁ R (n + 2) -  chebyshev₁ R (n + 1))
+      - (1 - X ^ 2) * (2 * X * chebyshev₂ R (n + 1) - chebyshev₂ R n) :
+            by ring
+... = X * chebyshev₁ R (n + 2 + 1) - (1 - X ^ 2) * chebyshev₂ R (n + 2) :
+            by rw [chebyshev₁_add_two _ (n + 1), chebyshev₂_add_two]
+
+lemma one_sub_X_pow_two_mul_chebyshev₂_eq_pol_in_chebyshev₁ (n : ℕ) :
+  (1 - X ^ 2) * chebyshev₂ R n = X * chebyshev₁ R (n + 1) - chebyshev₁ R (n + 2) :=
+by rw [chebyshev₁_eq_X_mul_chebyshev₁_sub_pol_chebyshev₂, ←sub_add, sub_self, zero_add]
+
+variables {R S}
+
+@[simp] lemma map_chebyshev₂ (f : R →+* S) :
+  ∀ (n : ℕ), map f (chebyshev₂ R n) = chebyshev₂ S n
+| 0       := by simp only [chebyshev₂_zero, map_one]
+| 1       :=
+begin
+  simp only [chebyshev₂_one, map_X, map_mul, map_add, map_one],
+  change map f (1+1) * X = 2 * X,
+  simpa only [map_add, map_one]
+end
+| (n + 2) :=
+begin
+  simp only [chebyshev₂_add_two, map_mul, map_sub, map_X, bit0, map_add, map_one],
+  rw [map_chebyshev₂ (n + 1), map_chebyshev₂ n],
+end
+
+lemma chebyshev₁_derivative_eq_chebyshev₂ :
+  ∀ (n : ℕ), derivative (chebyshev₁ R (n + 1)) = (n + 1) * chebyshev₂ R n
+| 0        := by simp only [chebyshev₁_one, chebyshev₂_zero, derivative_X, nat.cast_zero, zero_add,
+                           mul_one]
+| 1        := by { simp only [chebyshev₁_two, chebyshev₂_one, derivative_sub, derivative_one,
+                              derivative_mul, derivative_X_pow, nat.cast_one,
+                              nat.cast_two],
+                    norm_num }
+| (n + 2)  :=
+  calc derivative (chebyshev₁ R (n + 2 + 1))
+      = 2 * chebyshev₁ R (n + 2) + 2 * X * derivative (chebyshev₁ R (n + 1 + 1))
+                                 - derivative (chebyshev₁ R (n + 1)) :
+              by simp only [chebyshev₁_add_two _ (n + 1), derivative_sub, derivative_mul,
+                                      derivative_X, derivative_bit0, derivative_one, bit0_zero,
+                                      zero_mul, zero_add, mul_one]
+  ... = 2 * (chebyshev₂ R (n + 1 + 1) - X * chebyshev₂ R (n + 1))
+        + 2 * X * ((n + 1 + 1) * chebyshev₂ R (n + 1)) - (n + 1) * chebyshev₂ R n :
+              by rw_mod_cast [chebyshev₁_derivative_eq_chebyshev₂,
+                chebyshev₁_derivative_eq_chebyshev₂, chebyshev₁_eq_chebyshev₂_sub_X_mul_chebyshev₂]
+  ... = (n + 1) * (2 * X * chebyshev₂ R (n + 1) - chebyshev₂ R n) + 2 * chebyshev₂ R (n + 2) :
+              by ring
+  ... = (n + 1) * chebyshev₂ R (n + 2) + 2 * chebyshev₂ R (n + 2) :
+              by rw chebyshev₂_add_two
+  ... = (n + 2 + 1) * chebyshev₂ R (n + 2) :
+              by ring
+  ... = (↑(n + 2) + 1) * chebyshev₂ R (n + 2) :
+              by norm_cast
+
+lemma one_sub_X_pow_two_mul_derivative_chebyshev₁_eq_poly_in_chebyshev₁ (n : ℕ) :
+  (1 - X ^ 2)  * (derivative (chebyshev₁ R (n+1))) =
+    (n + 1) * (chebyshev₁ R n - X * chebyshev₁ R (n+1)) :=
+  calc
+  (1 - X ^ 2)  * (derivative (chebyshev₁ R (n+1)))
+  = (1 - X ^ 2 ) * ((n + 1) * chebyshev₂ R n) :
+            by rw chebyshev₁_derivative_eq_chebyshev₂
+  ... = (n + 1) * ((1 - X ^ 2) * chebyshev₂ R n) :
+            by ring
+  ... = (n + 1) * (X * chebyshev₁ R (n + 1) - (2 * X * chebyshev₁ R (n + 1) - chebyshev₁ R n)) :
+            by rw [one_sub_X_pow_two_mul_chebyshev₂_eq_pol_in_chebyshev₁, chebyshev₁_add_two]
+  ... = (n + 1) * (chebyshev₁ R n - X * chebyshev₁ R (n+1)) :
+            by ring
+
+lemma add_one_mul_chebyshev₁_eq_poly_in_chebyshev₂ (n : ℕ) :
+  ((n : polynomial R) + 1) * chebyshev₁ R (n+1) =
+    X * chebyshev₂ R n - (1 - X ^ 2) * derivative ( chebyshev₂ R n) :=
+begin
+  have h : derivative (chebyshev₁ R (n + 2)) = (chebyshev₂ R (n + 1) - X * chebyshev₂ R n)
+    + X * derivative (chebyshev₁ R (n + 1)) + 2 * X * chebyshev₂ R n
+    - (1 - X ^ 2) * derivative (chebyshev₂ R n),
+  { conv_lhs { rw chebyshev₁_eq_X_mul_chebyshev₁_sub_pol_chebyshev₂ },
+  simp only [derivative_sub, derivative_mul, derivative_X, derivative_one, derivative_X_pow,
+  one_mul, chebyshev₁_derivative_eq_chebyshev₂],
+  rw [chebyshev₁_eq_chebyshev₂_sub_X_mul_chebyshev₂, nat.cast_bit0, nat.cast_one],
+  ring },
+  calc ((n : polynomial R) + 1) * chebyshev₁ R (n + 1)
+      = ((n : polynomial R) + 1 + 1) * (X * chebyshev₂ R n + chebyshev₁ R (n + 1))
+        - X * ((n + 1) * chebyshev₂ R n) - (X * chebyshev₂ R n + chebyshev₁ R (n + 1)) :
+            by ring
+  ... = derivative (chebyshev₁ R (n + 2)) - X * derivative (chebyshev₁ R (n + 1))
+                                          - chebyshev₂ R (n + 1) :
+            by rw [←chebyshev₂_eq_X_mul_chebyshev₂_add_chebyshev₁,
+                  ←chebyshev₁_derivative_eq_chebyshev₂, ←nat.cast_one, ←nat.cast_add,
+                  nat.cast_one, ←chebyshev₁_derivative_eq_chebyshev₂ (n + 1)]
+  ... = (chebyshev₂ R (n + 1) - X * chebyshev₂ R n) + X * derivative (chebyshev₁ R (n + 1))
+        + 2 * X * chebyshev₂ R n - (1 - X ^ 2) * derivative (chebyshev₂ R n)
+        - X * derivative (chebyshev₁ R (n + 1)) - chebyshev₂ R (n + 1) :
+            by rw h
+  ... = X * chebyshev₂ R n - (1 - X ^ 2) * derivative (chebyshev₂ R n) :
+            by ring,
+end
+
 end polynomial