Scaled Polynomial Degree Equals Chebyshev Degree

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.PolynomialProperties

Statement

Theorem Scaled Polynomial Degree Equals Chebyshev Degree
[blueprint]

For $N \geq 1$, $\deg(S_N(x;\theta)) = \deg(T_N(x)) = N$. This follows directly from the degree of the scaled polynomial and the Chebyshev degree lemma.

theorem scaledPolynomial_degree_eq_chebyshev (N : ℕ) (θ : ℝ) (hN : 0 < N) :
    (scaledPolynomial N θ).degree = (Polynomial.Chebyshev.T ℝ N).degree := by
Proof ▼ 


  rw [chebyshev_T_degree N hN]
  exact scaledPolynomial_degree N θ hN

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