2.2. Series and their coefficients🔗

Hex.TSeries.{u} (R : Type u) (n : ℕ) : Type u
Hex.TSeries.{u} (R : Type u) (n : ℕ) :
  Type u

Hex.TSeries.mk.{u}

coeffs : Vector R n

Hex.TSeries.coeff reads coefficients: a.coeff i is the coefficient of xⁱ, and is 0 when i ≥ n. That 0 is a convention which keeps statements about coefficients short. It does not say that the series being approximated has a zero coefficient there, only that a does not record it. Hex.TSeries.ofFn builds a series from a function giving its coefficients, Hex.TSeries.C makes a constant series, and Hex.TSeries.X is the series x. The usual notation +, -, *, ^ and numerals is available, and multiplication discards every term of degree n or more. Two series are equal when their n coefficients agree (Hex.TSeries.ext), and equality is decidable when it is decidable in R. For example, (1 - x)(1 + x + x² + ⋯) = 1:

Euler's product from the introduction has the coefficients of the pentagonal number theorem: apart from the constant coefficient 1, the nonzero ones sit at the pentagonal numbers k(3k - 1)/2 and k(3k + 1)/2 for k ≥ 1, that is 1, 2, 5, 7, 12, 15, 22, 26, …, and they are (-1)ᵏ:

#v[1, -1, -1, 0, 0, 1, 0, 1, 0, 0, 0, 0, -1, 0, 0, -1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0]

The operations below are total functions. Where an operation only makes sense under a hypothesis, such as a zero constant coefficient for exp, the function does not check it: it returns some series in every case, and the theorems about it carry the hypothesis. Where checking is possible, an Option-valued form such as inv? or comp? checks the hypothesis and returns none when it fails.

Precisions 0 and 1 are allowed. TSeries R 0 is the zero ring, in which every element is a unit and has a square root. The hypotheses of the theorems below are stated so that they remain true there: the theorems about the logarithm, for example, assume (a - 1).coeff 0 = 0 rather than a.coeff 0 = 1, which would be false at precision 0.