Scaled Polynomial Coefficient Accessor

StatusFully Proven

TypeAbbrev

ModuleChebyshevCircles.Definitions.Core

Statement

Abbrev Scaled Polynomial Coefficient Accessor

Extracts the $k$-th coefficient of $S_N(x;\theta)$. In particular, the constant term is \texttt{scaledPolynomial\_coeff N θ 0} and the leading coefficient is \texttt{scaledPolynomial\_coeff N θ N} $= 2^{N-1}$.

abbrev scaledPolynomial_coeff (N : ℕ) (θ : ℝ) (k : ℕ) : ℝ :=
  (scaledPolynomial N θ).coeff k

Dependencies (uses)

Scaled Polynomial

Dependents (used by)

Constant Term Varies with Theta

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