Explicit Constant Formula Correctness

StatusFully Proven

TypeTheorem

ModuleChebyshevCircles.Proofs.MainTheoremSupport

Statement

Theorem Explicit Constant Formula Correctness

For $N \geq 1$, $c(\theta) = [x^0]\, S_N(x;\theta) - [x^0]\, T_N(x) = 2^{N-1} \cdot (-1)^N \cdot \prod_{k=0}^{N-1}\cos(\theta + 2\pi k/N) - T_N(0)$.

theorem explicitConstant_correct (N : ℕ) (θ : ℝ) (hN : 0 < N) :
    explicitConstant N θ = (scaledPolynomial N θ).coeff 0 - (Polynomial.Chebyshev.T ℝ N).coeff 0 := by

Proof ▼


  unfold explicitConstant constantTermFormula chebyshevConstantTerm
  rw [scaledPolynomial_constantTerm_formula N θ hN, chebyshev_T_constantTerm]
  -- Both sides are: constantTermFormula N θ - chebyshevConstantTerm N
  rfl

Dependencies (uses)

Explicit Constant c(N, θ)
Chebyshev Constant Term
Scaled Polynomial Constant Term Formula

Dependents (used by)

Proof of Main Theorem

Neighborhood

Depth: 1 / 1

Legend

Not Ready

Work in Progress

Sorry (theorems only)

Proven/Defined

Fully Proven (theorems only)

Axiom

Mathlib Ready

Theorems/Lemmas

Definitions

Axioms