Scaled Polynomial Degree

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.PolynomialConstruction

Statement

Theorem Scaled Polynomial Degree
[blueprint]

For $N > 0$, $\deg S_N(x;\theta) = N.$

theorem scaledPolynomial_degree (N : ℕ) (θ : ℝ) (_hN : 0 < N) :
    (scaledPolynomial N θ).degree = N := by
Proof ▼ 


  unfold scaledPolynomial
  rw [degree_C_mul, unscaledPolynomial_degree N θ]
  exact pow_ne_zero (N - 1) two_ne_zero

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