Unscaled Polynomial
StatusFully Proven
TypeDefinition
ModuleChebyshevCircles.Definitions.Core
Statement
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 θ)
Dependencies (uses)
Neighborhood
Legend
Not Ready
Work in Progress
Sorry (theorems only)
Proven/Defined
Fully Proven (theorems only)
Axiom
Mathlib Ready
Theorems/Lemmas
Definitions
Axioms