Chebyshev Circles: Rotated Roots of Unity and Chebyshev Polynomials
Progress
0 not ready
0 work in progress
0 sorry
0 proven
83 fully proven
0 axiom
0 mathlib ready
83 declarations
Completion
83 proven
0 sorry
0 other
Attention
0 blocked
0 issues
0 tech debt
Checks
Graph is disconnectedNo circular dependencies
Kernel Verification
Blueprint Coverage: 83/83 (100%)
Axioms: 3 standard, 0 custom
Soundness ChecksNot implemented
Key Declarations
Rotated Roots of Unity
Definition 1.1
When the $N$-th roots of unity are rotated by an angle $\theta$
(equivalently, multiplied by $e^{i\theta}$), we obtain the $N$ complex numbers
$e^{i(\theta + 2\pi k/N)}$ for $k = 0, 1, \ldots, N-1$.
The rotation angle $\theta$ controls the orientation of the $N$-gon.
def rotatedRootsOfUnityList (N : ℕ) (θ : ℝ) : List ℂ :=
List.range N |>.map (fun k => exp (I * (θ + 2 * π * k / N)))
Real Projections List
Definition def-realProjectionsList
The real projections of the rotated $N$-th roots of unity are the $N$
real numbers
$$r_k(\theta) = \cos\!\left(\theta + \frac{2\pi k}{N}\right), \quad k = 0, 1, \ldots, N-1.$$
def realProjectionsList (N : ℕ) (θ : ℝ) : List ℝ :=
(List.range N).map (fun (k : ℕ) => Real.cos (θ + 2 * π * k / N))
Scaled Polynomial
Definition 1.3
The scaled polynomial is defined as
$$S_N(x;\theta) = 2^{N-1} \cdot P_N(x;\theta).$$
It inherits the degree and roots from $P_N$, with leading coefficient $2^{N-1}$.
def scaledPolynomial (N : ℕ) (θ : ℝ) : Polynomial ℝ :=
C (2 ^ (N - 1)) * unscaledPolynomial N θ
Sum of Cosines at Equally-Spaced Angles
Theorem lem-sum_cos_phi_vanishes
For $N \ge 2$ and any $\theta \in \mathbb{R}$,
$\sum_{k=0}^{N-1} \cos\bigl(\theta + \frac{2\pi k}{N}\bigr) = 0.$
theorem sum_cos_roots_of_unity (N : ℕ) (θ : ℝ) (hN : 2 ≤ N) :
∑ k ∈ Finset.range N, Real.cos (θ + 2 * π * k / N) = 0 := by
Cosine Sum at Integer Multiples Vanishes
Theorem lem-sum_cos_m_phi_vanishes
For $N \ge 1$, $0 < m < N$, and any $\theta \in \mathbb{R}$,
$\sum_{k=0}^{N-1} \cos\bigl(m\bigl(\theta + \frac{2\pi k}{N}\bigr)\bigr) = 0.$
theorem sum_cos_multiple_rotated_roots (N : ℕ) (m : ℕ) (θ : ℝ)
(hN : 0 < N) (hm : 0 < m) (hm' : m < N) :
∑ k ∈ Finset.range N, Real.cos (m * (θ + 2 * π * k / N)) = 0 := by
Constant Term Varies with Theta
Theorem lem-scaledPolynomial-constantTerm-varies
For $N > 0$, there exist $\theta_1, \theta_2 \in \mathbb{R}$ such that the
constant term of $S_N(x;\theta_1)$ differs from that of $S_N(x;\theta_2)$.
theorem scaledPolynomial_constantTerm_varies (N : ℕ) (hN_pos : 0 < N) :
∃ θ₁ θ₂ : ℝ, scaledPolynomial_coeff N θ₁ 0 ≠ scaledPolynomial_coeff N θ₂ 0 := by
Power Sum Invariance
Theorem 4.3.1
For any integers $N \ge 1$, $j$ with $1 \le j < N$, and any $\theta \in \mathbb{R}$,
$\sum_{k=0}^{N-1} \cos^j\!\bigl(\theta + \frac{2\pi k}{N}\bigr)$
is independent of $\theta$.
theorem powerSumCos_invariant (N : ℕ) (j : ℕ) (θ₁ θ₂ : ℝ)
(hN : 0 < N) (hj : 0 < j) (hj' : j < N) :
∑ k ∈ Finset.range N, (Real.cos (θ₁ + 2 * π * k / N)) ^ j =
∑ k ∈ Finset.range N, (Real.cos (θ₂ + 2 * π * k / N)) ^ j := by
Newton's Identities for Multisets
Theorem thm-newton_identities
For a multiset $s$ and $m > 0$,
$m \cdot e_m(s) = (-1)^{m+1} \sum_{\substack{(a,b) \\ a+b = m,\; a < m}}
(-1)^a\, e_a(s)\, p_b(s).$
theorem multiset_newton_identity (s : Multiset ℝ) (m : ℕ) (_ : 0 < m) :
(m : ℝ) * s.esymm m = (-1)^(m + 1) *
(Finset.antidiagonal m).sum (fun a =>
if a.1 < m then (-1)^a.1 * s.esymm a.1 * (s.map (fun x => x ^ a.2)).sum
else 0) := by
Elementary Symmetric Functions of Rotated Roots Are Invariant
Theorem lem-esymm_invariant
For $0 < m < N$, the elementary symmetric polynomial
$e_m\bigl(r_0(\theta), \ldots, r_{N-1}(\theta)\bigr)$
is independent of $\theta$.
theorem esymm_rotated_roots_invariant (N : ℕ) (m : ℕ) (θ₁ θ₂ : ℝ)
(hN : 0 < N) (hm : 0 < m) (hm' : m < N) :
let l1 :=
Coefficient Independence Theorem
Theorem 5.1.1
For any $N \geq 1$ and any $k \geq 1$, the coefficient $[x^k] S_N(x;\theta_1) = [x^k] S_N(x;\theta_2)$
for all $\theta_1, \theta_2 \in \mathbb{R}$.
theorem constant_term_only_varies (N : ℕ) (θ₁ θ₂ : ℝ) (k : ℕ) (hN : 0 < N)
(hk : 0 < k) : (scaledPolynomial N θ₁).coeff k = (scaledPolynomial N θ₂).coeff k := by
Full Root Characterization of Chebyshev Polynomials
Theorem lem-chebyshev-T-eval-eq-zero-iff
For $N \geq 1$ and $x \in \mathbb{R}$,
$T_N(x) = 0 \iff \exists\, k < N,\; x = \cos\!\left(\frac{(2k+1)\pi}{2N}\right)$.
theorem chebyshev_T_eval_eq_zero_iff (N : ℕ) (hN : 0 < N) (x : ℝ) :
(Polynomial.Chebyshev.T ℝ N).eval x = 0 ↔ ∃ k < N, x = chebyshevRoot N k := by
Power Sum Equality
Theorem 6.2.2
For $1 \leq j < N$,
$\sum_{k=0}^{N-1} \cos^j\!\left(\theta + \frac{2\pi k}{N}\right) =
\sum_{k=0}^{N-1} \cos^j\!\left(\frac{(2k+1)\pi}{2N}\right)$.
theorem general_powersum_equality (N j : ℕ) (hN : 0 < N) (hj : 0 < j) (hj' : j < N) :
∑ k ∈ Finset.range N, (Real.cos (2 * π * k / N)) ^ j =
∑ k ∈ Finset.range N, (Real.cos ((2 * k + 1 : ℝ) * π / (2 * N))) ^ j := by
Coefficient Matching at theta = 0
Theorem lem-scaledPolynomial-matches-chebyshev-at-zero
For $N \geq 1$ and $k \geq 1$,
$[x^k]\, S_N(x; 0) = [x^k]\, T_N(x)$.
The proof proceeds by case analysis: $N = 1, 2, 3$ are verified by explicit computation,
and $N \geq 4$ uses the power sum equality and Newton's identities to match elementary
symmetric polynomials.
theorem scaledPolynomial_matches_chebyshev_at_zero (N : ℕ) (k : ℕ) (hN : 0 < N) (hk : 0 < k) :
(scaledPolynomial N 0).coeff k = (Polynomial.Chebyshev.T ℝ N).coeff k := by
Main Theorem Statement
Definition thm-main-statement
For any positive integer $N \geq 1$ and any angle $\theta \in \mathbb{R}$,
$$S_N(x;\theta) = T_N(x) + c(N,\theta),$$
where the constant $c(N,\theta)$ is given explicitly by
$$c(N,\theta) = 2^{N-1} \cdot (-1)^N \cdot \prod_{k=0}^{N-1}
\cos\!\left(\theta + \frac{2\pi k}{N}\right) - T_N(0).$$
Moreover, all coefficients of $S_N(x;\theta)$ of degree $k \geq 1$ are independent
of $\theta$ and equal the corresponding coefficients of $T_N(x)$.
def StatementOfTheorem : Prop :=
∀ (N : ℕ) (θ : ℝ), 0 < N →
scaledPolynomial N θ = Polynomial.Chebyshev.T ℝ N + C (explicitConstant N θ)
Proof of Main Theorem
Theorem 1.4
For any $N \geq 1$ and $\theta \in \mathbb{R}$,
$S_N(x;\theta) = T_N(x) + c(N,\theta)$.
theorem mainTheorem : StatementOfTheorem := by
Project Notes
No project notes