2.1. Introduction
A formal power series a₀ + a₁x + a₂x² + ⋯ over a commutative ring R has
infinitely many coefficients, and a program can hold only finitely many of
them. HexTruncatedSeries computes with the first n coefficients, for an
n fixed in the type: a value of type TSeries R n is a power series modulo
xⁿ. Besides the ring operations, it provides the classical operations on
power series: inverse, square root, exponential, logarithm, substitution of
one series into another, and the compositional inverse. Every coefficient it
returns is exact.
Generating functions are the most direct use. Euler showed that the number
p(k) of partitions of k is the coefficient of xᵏ in
1 / ((1 - x)(1 - x²)(1 - x³)⋯).
Modulo x³⁰ only the first 29 factors matter, and inverting their product
gives p(0), p(1), …, p(29). Here X is the indeterminate x, and
.coeffs is the vector of coefficients in increasing degree:
open Hex Hex.TSeries
namespace HexTruncatedSeriesChapter
/-- `(1 - x)(1 - x²)⋯(1 - xⁿ⁻¹)` at precision `n`. -/
def euler (n : Nat) : TSeries Int n :=
(List.range (n - 1)).foldl
(fun acc j => acc * (1 - X ^ (j + 1))) 1
def partitions : TSeries Int 30 :=
invOfUnit (euler 30) 1
#eval partitions.coeffs
Here invOfUnit a u inverts a, given an inverse u of its constant
coefficient; the constant coefficient of Euler's product is 1. The inverse
is computed by Newton's method, which doubles the number of correct
coefficients at each step, and needs no division in R beyond the one the
caller supplies. So it works over ℤ, and so does the compositional inverse.
The exponential and logarithm divide by 1, 2, …, n - 1, and their types say
so; see Exponential and logarithm.
HexTruncatedSeries depends only on HexBasic, and not on
Mathlib; import it to compute. Its coefficient rings are instances of
Lean.Grind.CommRing, which every Mathlib CommRing provides. The companion
HexTruncatedSeriesTheory, which imports Mathlib, proves that TSeries R n
is the quotient of Mathlib's PowerSeries R by the ideal (Xⁿ), and that
the operations with a Mathlib counterpart agree with it; import it to prove
theorems about Mathlib's power series. See
The Mathlib correspondence.