-
Notifications
You must be signed in to change notification settings - Fork 251
/
Chebyshev.lean
133 lines (105 loc) · 4.65 KB
/
Chebyshev.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
/-
Copyright (c) 2020 Johan Commelin. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johan Commelin
-/
import Mathlib.Algebra.Polynomial.AlgebraMap
import Mathlib.Data.Complex.Exponential
import Mathlib.Data.Complex.Module
import Mathlib.RingTheory.Polynomial.Chebyshev
#align_import analysis.special_functions.trigonometric.chebyshev from "leanprover-community/mathlib"@"2c1d8ca2812b64f88992a5294ea3dba144755cd1"
/-!
# Multiple angle formulas in terms of Chebyshev polynomials
This file gives the trigonometric characterizations of Chebyshev polynomials, for both the real
(`Real.cos`) and complex (`Complex.cos`) cosine.
-/
set_option linter.uppercaseLean3 false
namespace Polynomial.Chebyshev
open Polynomial
variable {R A : Type*} [CommRing R] [CommRing A] [Algebra R A]
@[simp]
theorem aeval_T (x : A) (n : ℤ) : aeval x (T R n) = (T A n).eval x := by
rw [aeval_def, eval₂_eq_eval_map, map_T]
#align polynomial.chebyshev.aeval_T Polynomial.Chebyshev.aeval_T
@[simp]
theorem aeval_U (x : A) (n : ℤ) : aeval x (U R n) = (U A n).eval x := by
rw [aeval_def, eval₂_eq_eval_map, map_U]
#align polynomial.chebyshev.aeval_U Polynomial.Chebyshev.aeval_U
@[simp]
theorem algebraMap_eval_T (x : R) (n : ℤ) :
algebraMap R A ((T R n).eval x) = (T A n).eval (algebraMap R A x) := by
rw [← aeval_algebraMap_apply_eq_algebraMap_eval, aeval_T]
#align polynomial.chebyshev.algebra_map_eval_T Polynomial.Chebyshev.algebraMap_eval_T
@[simp]
theorem algebraMap_eval_U (x : R) (n : ℤ) :
algebraMap R A ((U R n).eval x) = (U A n).eval (algebraMap R A x) := by
rw [← aeval_algebraMap_apply_eq_algebraMap_eval, aeval_U]
#align polynomial.chebyshev.algebra_map_eval_U Polynomial.Chebyshev.algebraMap_eval_U
-- Porting note: added type ascriptions to the statement
@[simp, norm_cast]
theorem complex_ofReal_eval_T : ∀ (x : ℝ) n, (((T ℝ n).eval x : ℝ) : ℂ) = (T ℂ n).eval (x : ℂ) :=
@algebraMap_eval_T ℝ ℂ _ _ _
#align polynomial.chebyshev.complex_of_real_eval_T Polynomial.Chebyshev.complex_ofReal_eval_T
-- Porting note: added type ascriptions to the statement
@[simp, norm_cast]
theorem complex_ofReal_eval_U : ∀ (x : ℝ) n, (((U ℝ n).eval x : ℝ) : ℂ) = (U ℂ n).eval (x : ℂ) :=
@algebraMap_eval_U ℝ ℂ _ _ _
#align polynomial.chebyshev.complex_of_real_eval_U Polynomial.Chebyshev.complex_ofReal_eval_U
/-! ### Complex versions -/
section Complex
open Complex
variable (θ : ℂ)
/-- The `n`-th Chebyshev polynomial of the first kind evaluates on `cos θ` to the
value `cos (n * θ)`. -/
@[simp]
theorem T_complex_cos (n : ℤ) : (T ℂ n).eval (cos θ) = cos (n * θ) := by
induction n using Polynomial.Chebyshev.induct with
| zero => simp
| one => simp
| add_two n ih1 ih2 =>
simp only [T_add_two, eval_sub, eval_mul, eval_X, eval_ofNat, ih1, ih2, sub_eq_iff_eq_add,
cos_add_cos]
push_cast
ring_nf
| neg_add_one n ih1 ih2 =>
simp only [T_sub_one, eval_sub, eval_mul, eval_X, eval_ofNat, ih1, ih2, sub_eq_iff_eq_add',
cos_add_cos]
push_cast
ring_nf
#align polynomial.chebyshev.T_complex_cos Polynomial.Chebyshev.T_complex_cos
/-- The `n`-th Chebyshev polynomial of the second kind evaluates on `cos θ` to the
value `sin ((n + 1) * θ) / sin θ`. -/
@[simp]
theorem U_complex_cos (n : ℤ) : (U ℂ n).eval (cos θ) * sin θ = sin ((n + 1) * θ) := by
induction n using Polynomial.Chebyshev.induct with
| zero => simp
| one => simp [one_add_one_eq_two, sin_two_mul]; ring
| add_two n ih1 ih2 =>
simp only [U_add_two, add_sub_cancel_right, eval_sub, eval_mul, eval_X, eval_ofNat, sub_mul,
mul_assoc, ih1, ih2, sub_eq_iff_eq_add, sin_add_sin]
push_cast
ring_nf
| neg_add_one n ih1 ih2 =>
simp only [U_sub_one, add_sub_cancel_right, eval_sub, eval_mul, eval_X, eval_ofNat, sub_mul,
mul_assoc, ih1, ih2, sub_eq_iff_eq_add', sin_add_sin]
push_cast
ring_nf
#align polynomial.chebyshev.U_complex_cos Polynomial.Chebyshev.U_complex_cos
end Complex
/-! ### Real versions -/
section Real
open Real
variable (θ : ℝ) (n : ℤ)
/-- The `n`-th Chebyshev polynomial of the first kind evaluates on `cos θ` to the
value `cos (n * θ)`. -/
@[simp]
theorem T_real_cos : (T ℝ n).eval (cos θ) = cos (n * θ) := mod_cast T_complex_cos θ n
#align polynomial.chebyshev.T_real_cos Polynomial.Chebyshev.T_real_cos
/-- The `n`-th Chebyshev polynomial of the second kind evaluates on `cos θ` to the
value `sin ((n + 1) * θ) / sin θ`. -/
@[simp]
theorem U_real_cos : (U ℝ n).eval (cos θ) * sin θ = sin ((n + 1) * θ) :=
mod_cast U_complex_cos θ n
#align polynomial.chebyshev.U_real_cos Polynomial.Chebyshev.U_real_cos
end Real
end Polynomial.Chebyshev