Unscaled Polynomial

StatusFully Proven
TypeDefinition
ModuleChebyshevCircles.Definitions.Core

Statement

Definition Unscaled Polynomial

Let $P_N(x;\theta)$ denote the monic polynomial having the rotated root projections as roots: $$P_N(x;\theta) = \prod_{k=0}^{N-1}\!\left(x - \cos\!\left(\theta + \frac{2\pi k}{N}\right)\right).$$ Since the roots are real and lie in $[-1,1]$, this polynomial has real coefficients and degree $N$.

def unscaledPolynomial (N : ) (θ : ) : Polynomial  :=
  polynomialFromRealRoots (realProjectionsList N θ)

Neighborhood

Legend
Not Ready
Work in Progress
Sorry (theorems only)
Proven/Defined
Fully Proven (theorems only)
Axiom
Mathlib Ready
Theorems/Lemmas
Definitions
Axioms