Proof of Main Theorem

StatusFully Proven

TypeTheorem

ModuleChebyshevCircles.ProofOfMainTheorem

Statement

We now assemble the pieces to prove the main theorem. By the power sum equality theorem, the rotated root projections $r_k(\theta)$ and the Chebyshev roots $\xi_k$ have matching power sums for $1 \leq j < N$. Newton's identities then imply that the elementary symmetric polynomials match, so the polynomial coefficients of degree $k \geq 1$ are identical.

Theorem 1.4

[blueprint]

For any $N \geq 1$ and $\theta \in \mathbb{R}$, $S_N(x;\theta) = T_N(x) + c(N,\theta)$.

theorem mainTheorem : StatementOfTheorem := by

Proof ▼

The proof proceeds by coefficient comparison via \texttt{ext n}. For $n \geq 1$: the $n$-th coefficient of $S_N$ is $\theta$-invariant (\texttt{constant\_term\_only\_varies}), so it equals the coefficient at $\theta = 0$, which matches $T_N$ by \texttt{scaledPolynomial\_matches\_chebyshev\_at\_zero}. For $n = 0$: the explicit constant $c(N,\theta)$ is chosen precisely so that the constant terms agree.


  intro N θ hN
  -- Prove equality coefficient by coefficient
  ext n
  simp only [coeff_add, coeff_C]
  by_cases hn : n = 0
  · -- Constant term: explicitConstant is chosen exactly to make this work
    simp [hn]
    rw [explicitConstant_correct N θ hN]
    ring
  · -- Non-constant terms: θ-invariance + match at θ=0
    simp [hn]
    have h_pos : 0 < n := Nat.pos_of_ne_zero hn
    calc (scaledPolynomial N θ).coeff n
        = (scaledPolynomial N 0).coeff n := constant_term_only_varies N θ 0 n hN h_pos
      _ = (Chebyshev.T ℝ N).coeff n := scaledPolynomial_matches_chebyshev_at_zero N n hN h_pos

This completes the proof that Chebyshev polynomials emerge from projections of rotated roots of unity. The only degree of freedom under rotation is the constant term, reflecting that the $N$-th power sum is the only one that can depend on $\theta$.

Dependencies (uses)

Dependents (used by)

None

Neighborhood

Depth: 1 / 1

Legend

Not Ready

Work in Progress

Sorry (theorems only)

Proven/Defined

Fully Proven (theorems only)

Axiom

Mathlib Ready

Theorems/Lemmas

Definitions

Axioms