Unscaled Polynomial Vanishes at Projected Roots

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.PolynomialProperties

Statement

Theorem Unscaled Polynomial Vanishes at Projected Roots
[blueprint]

For $0 \leq k < N$, $P_N(\cos(\theta + 2\pi k/N);\theta) = 0$. This is immediate from the definition of $P_N$ as $\prod_{k=0}^{N-1}(x - r_k(\theta))$.

theorem unscaledPolynomial_eval_at_projection (N : ℕ) (θ : ℝ) (k : ℕ) (hk : k < N) :
    (unscaledPolynomial N θ).eval (Real.cos (θ + 2 * π * k / N)) = 0 := by
Proof ▼ 


  unfold unscaledPolynomial
  apply polynomialFromRealRoots_eval_mem
  exact realProjection_mem_list N θ k hk

Dependencies (uses)

Dependents (used by)

Neighborhood

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