2.7. Composition and reversion🔗

Hex.TSeries.comp substitutes one series into another. When b has constant coefficient 0, comp a b = a(b(x)) = Σₖ aₖ bᵏ, where only k < n matters because bᵏ is divisible by xᵏ. When b has a nonzero constant coefficient c, the constant coefficient of a(b(x)) would be the infinite sum Σ aₖ cᵏ, which has no meaning in a general ring.

Hex.TSeries.comp_spec.{u} {R : Type u} {n : ℕ} [Lean.Grind.CommRing R]
  (a b : Hex.TSeries R n) (h : b.coeff 0 = 0) :
  a.comp b =
    List.foldl (fun acc k => acc + Hex.TSeries.C (a.coeff k) * b.pow k)
      0 (List.range n)
Hex.TSeries.comp_spec.{u} {R : Type u}
  {n : ℕ} [Lean.Grind.CommRing R]
  (a b : Hex.TSeries R n)
  (h : b.coeff 0 = 0) :
  a.comp b =
    List.foldl
      (fun acc k =>
        acc +
          Hex.TSeries.C (a.coeff k) *
            b.pow k)
      0 (List.range n)

The sum is evaluated by the algorithm of Brent and Kung. With s about √n, it splits a into blocks of s coefficients, computes the powers b⁰, b¹, …, bˢ once, evaluates each block as a linear combination of those powers, and combines the blocks by Horner's rule in bˢ. This takes about 2√n multiplications of series, and n² multiplications of coefficients to form the blocks. Horner's rule in b itself, available as Hex.TSeries.compHorner, takes n multiplications of series. The exponential generating function of the Bell numbers is a composition:

When b has constant coefficient 0 and linear coefficient a unit, it has a compositional inverse: a series y with b(y(x)) = x, and then also y(b(x)) = x. Hex.TSeries.revOfUnit computes it, given an inverse of the linear coefficient:

Hex.TSeries.revOfUnit.{u} {R : Type u} {n : ℕ} [Lean.Grind.CommRing R]
  (b : Hex.TSeries R n) (v : R) : Hex.TSeries R n
Hex.TSeries.revOfUnit.{u} {R : Type u}
  {n : ℕ} [Lean.Grind.CommRing R]
  (b : Hex.TSeries R n) (v : R) :
  Hex.TSeries R n

Hex.TSeries.revOfUnit_comp.{u} {R : Type u} {n : ℕ}
  [Lean.Grind.CommRing R] (b : Hex.TSeries R n) (v : R)
  (h0 : b.coeff 0 = 0) (hv : b.coeff 1 * v = 1) :
  b.comp (b.revOfUnit v) = Hex.TSeries.X ∧
    (b.revOfUnit v).comp b = Hex.TSeries.X
Hex.TSeries.revOfUnit_comp.{u}
  {R : Type u} {n : ℕ}
  [Lean.Grind.CommRing R]
  (b : Hex.TSeries R n) (v : R)
  (h0 : b.coeff 0 = 0)
  (hv : b.coeff 1 * v = 1) :
  b.comp (b.revOfUnit v) = Hex.TSeries.X ∧
    (b.revOfUnit v).comp b = Hex.TSeries.X

It uses Newton's method for the equation b(y) = x, with the step y ↦ y - (b(y) - x)/b′(y). The only division is by b′(y), whose constant coefficient is the linear coefficient of b, so no other division is needed and reversion works over ℤ. The Catalan series y = x c(x) satisfies y = x + y², so it is the compositional inverse of x - x²:

#v[0, 1, 1, 2, 5, 14, 42, 132, 429, 1430]

Lagrange's inversion formula gives the coefficients of the compositional inverse directly: for 1 ≤ k < n, [xᵏ] y = (1/k) [xᵏ⁻¹] (x/b)ᵏ, where x/b is the inverse of the unit series b/x. Evaluated as written, it divides by k, so Hex.TSeries.revLagrange, which evaluates it, needs NatInverses R (n - 1). The library proves that the two agree whenever both apply:

Hex.TSeries.revLagrange_eq.{u} {R : Type u} {n : ℕ}
  [Lean.Grind.CommRing R] [Hex.TSeries.NatInverses R (n - 1)]
  (b : Hex.TSeries R n) (v : R) (h0 : b.coeff 0 = 0)
  (hv : b.coeff 1 * v = 1) : b.revLagrange v = b.revOfUnit v
Hex.TSeries.revLagrange_eq.{u}
  {R : Type u} {n : ℕ}
  [Lean.Grind.CommRing R]
  [Hex.TSeries.NatInverses R (n - 1)]
  (b : Hex.TSeries R n) (v : R)
  (h0 : b.coeff 0 = 0)
  (hv : b.coeff 1 * v = 1) :
  b.revLagrange v = b.revOfUnit v

A rooted tree whose k vertices are labelled 1, …, k is a root together with a set of rooted trees on the other labels, so the exponential generating function T of such trees satisfies T = x eᵀ. So T is the compositional inverse of x e⁻ˣ, and for k ≥ 1 its coefficients recover Cayley's formula kᵏ⁻¹:

[0, 1, 2, 9, 64, 625, 7776, 117649, 2097152, 43046721]