Scaled Polynomial Leading Coefficient

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.PolynomialConstruction

Statement

Theorem Scaled Polynomial Leading Coefficient
[blueprint]

The leading coefficient of $S_N(x;\theta)$ is $2^{N-1}$.

theorem scaledPolynomial_leadingCoeff (N : ℕ) (θ : ℝ) :
    (scaledPolynomial N θ).leadingCoeff = 2 ^ (N - 1) := by
Proof ▼ 


  unfold scaledPolynomial
  rw [leadingCoeff_mul, leadingCoeff_C, unscaledPolynomial_monic, mul_one]

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