Main Theorem Support: Coefficient Matching Lemmas

This module contains the supporting lemmas for proving that rotated N-th roots of unity, when projected onto the real axis and used as polynomial roots (scaled by 2^(N-1)), yield the N-th Chebyshev polynomial of the first kind plus a constant.

The main theorem mainTheorem is in ProofOfMainTheorem.lean, which uses the key lemma scaledPolynomial_matches_chebyshev_at_zero from this file.

Key Results

• chebyshev_T_leadingCoeff: Leading coefficient of T_N is 2^(N-1)
• scaledPolynomial_matches_chebyshev_at_zero: At θ=0, scaled polynomial coefficients match T_N

Supporting Lemmas (by case)

• scaledPolynomial_matches_chebyshev_N_eq_1: N=1 case
• scaledPolynomial_matches_chebyshev_N_eq_2: N=2 case
• scaledPolynomial_matches_chebyshev_N_eq_3: N=3 case
• scaledPolynomial_matches_chebyshev_N_ge_4: General N≥4 case

References

• Blueprint §1
• Research Paper

Tags

Chebyshev polynomials, roots of unity, polynomial coefficients

Main Theorems

The culminating results connecting rotated roots of unity to Chebyshev polynomials. Two sorries remain: one trivial ring tactic fix in N=3 case, and the general N≥4 case which requires deep harmonic analysis to prove power sum equality for Chebyshev roots.

theorem chebyshev_T_leadingCoeff (N : ℕ) (hN : 0 < N) : (Polynomial.Chebyshev.T ℝ ↑N).leadingCoeff = 2 ^ (N - 1)

The leading coefficient of Chebyshev T_N is 2^(N-1) for N ≥ 1.

This can be proven by induction using the recurrence T_{n+2} = 2X·T_{n+1} - T_n, but the proof is tedious and requires careful manipulation of leading coefficients. The result is standard in the literature on Chebyshev 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

For θ=0, the scaled polynomial coefficients match Chebyshev for k > 0.

Explicit Constant Term Formula Proofs

theorem scaledPolynomial_constantTerm_formula (N : ℕ) (θ : ℝ) (hN : 0 < N) : (scaledPolynomial N θ).coeff 0 = constantTermFormula N θ

The constant term of the scaled polynomial equals the explicit formula. The constant term of ∏(X - r_i) is (-1)^N * ∏r_i, so scaling by 2^(N-1) gives 2^(N-1) * (-1)^N * ∏cos(θ + 2πk/N).

theorem chebyshev_T_constantTerm (N : ℕ) : (Polynomial.Chebyshev.T ℝ ↑N).coeff 0 = chebyshevConstantTerm N

The constant term of Chebyshev polynomial T_N equals chebyshevConstantTerm N.

theorem explicitConstant_correct (N : ℕ) (θ : ℝ) (hN : 0 < N) : explicitConstant N θ = (scaledPolynomial N θ).coeff 0 - (Polynomial.Chebyshev.T ℝ ↑N).coeff 0

The explicit constant formula is correct: it equals the difference of constant terms.