Scaled Polynomial

StatusFully Proven

TypeDefinition

ModuleChebyshevCircles.Definitions.Core

Statement

To match the normalization of Chebyshev polynomials, which have leading coefficient $2^{N-1}$ for $N \geq 1$, we scale the monic polynomial $P_N$ by this factor.

Definition 1.3

[blueprint]

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 θ

The main theorem establishes that $S_N(x;\theta) = T_N(x) + c(\theta)$, so only the constant term varies with $\theta$. All higher-degree coefficients are $\theta$-independent and match those of $T_N$.

Dependencies (uses)

Unscaled Polynomial

Dependents (used by)

Scaled Polynomial Coefficient Accessor
Scaled Polynomial Degree
Scaled Polynomial Leading Coefficient
Coefficient Independence Theorem
Scaled Polynomial Vanishes at Projected Roots
Scaled Polynomial Constant Term Formula
Main Theorem Statement

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