Scaled Polynomial Vanishes at Projected Roots

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.PolynomialProperties

Statement

Theorem Scaled Polynomial Vanishes at Projected Roots
[blueprint]

For $0 \leq k < N$, $S_N(\cos(\theta + 2\pi k/N);\theta) = 0$. Follows from the unscaled polynomial vanishing and the multiplicative scaling by $2^{N-1}$.

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


  unfold scaledPolynomial
  rw [eval_mul, unscaledPolynomial_eval_at_projection N θ k hk]
  simp

Dependencies (uses)

Dependents (used by)

None

Neighborhood

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