2.6. Exponential and logarithm🔗

For a series a with constant coefficient 0 at precision n, exp a = Σ_{k<n} aᵏ/k! (the terms with k ≥ n vanish), and for a series a with constant coefficient 1, log a is the integral of a′/a with constant coefficient 0. At precision n both need the inverses of 1, …, n - 1 in R, and nothing more, so both take an instance of NatInverses R (n - 1):

Hex.TSeries.exp.{u} {R : Type u} {n : ℕ} [Lean.Grind.CommRing R]
  [Hex.TSeries.NatInverses R (n - 1)] (a : Hex.TSeries R n) :
  Hex.TSeries R n
Hex.TSeries.exp.{u} {R : Type u} {n : ℕ}
  [Lean.Grind.CommRing R]
  [Hex.TSeries.NatInverses R (n - 1)]
  (a : Hex.TSeries R n) : Hex.TSeries R n

Hex.TSeries.log.{u} {R : Type u} {n : ℕ} [Lean.Grind.CommRing R]
  [Hex.TSeries.NatInverses R (n - 1)] (a : Hex.TSeries R n) :
  Hex.TSeries R n
Hex.TSeries.log.{u} {R : Type u} {n : ℕ}
  [Lean.Grind.CommRing R]
  [Hex.TSeries.NatInverses R (n - 1)]
  (a : Hex.TSeries R n) : Hex.TSeries R n

Every ring has NatInverses R 0 and NatInverses R 1, Rat has NatInverses Rat m for every m, and HexTruncatedSeriesTheory provides an instance for every ℚ-algebra. Over ℤ, then, exp and log exist at precision at most 2, and exp (X : TSeries Int 3) does not typecheck, since exp x = 1 + x + x²/2 + ⋯. Over ℤ/pℤ with p prime, the inverses of 1, …, n - 1 exist exactly when n ≤ p, so exp and log make sense up to precision p, where Mathlib's exponential, which needs a ℚ-algebra, does not exist. This library does not depend on a type of integers modulo p, so an instance for one has to come from the code that uses it.

The exponential generating function of the Bell numbers, which count the partitions of a set of k elements, is exp(eˣ - 1):

[1, 1, 2, 5, 15, 52, 203, 877, 4140, 21147]

Taking the logarithm of Euler's generating function for partitions,

log ∏ⱼ 1/(1 - xʲ) = Σⱼ Σₘ xʲᵐ/m,

so for k ≥ 1, k times the coefficient of xᵏ is the sum σ(k) of the divisors of k (the first entry printed is the constant coefficient, 0):

[0, 1, 3, 4, 7, 6, 12, 8, 15, 13, 18, 12, 28, 14, 24, 24, 31, 18, 39, 20, 42, 32, 36, 24, 60, 31, 42, 40, 56, 30]

The logarithm is computed directly from its definition, with one inverse, one derivative, one product and one integral. The exponential is computed by Newton's method applied to log y = a, with the step y ↦ y(1 + a - log y), taking one logarithm at each step. The library proves the functional equations:

Hex.TSeries.log_exp.{u} {R : Type u} {n : ℕ} [Lean.Grind.CommRing R]
  [Hex.TSeries.NatInverses R (n - 1)] (a : Hex.TSeries R n)
  (h : a.coeff 0 = 0) : a.exp.log = a
Hex.TSeries.log_exp.{u} {R : Type u}
  {n : ℕ} [Lean.Grind.CommRing R]
  [Hex.TSeries.NatInverses R (n - 1)]
  (a : Hex.TSeries R n)
  (h : a.coeff 0 = 0) : a.exp.log = a

Hex.TSeries.exp_log.{u} {R : Type u} {n : ℕ} [Lean.Grind.CommRing R]
  [Hex.TSeries.NatInverses R (n - 1)] (a : Hex.TSeries R n)
  (h : (a - 1).coeff 0 = 0) : a.log.exp = a
Hex.TSeries.exp_log.{u} {R : Type u}
  {n : ℕ} [Lean.Grind.CommRing R]
  [Hex.TSeries.NatInverses R (n - 1)]
  (a : Hex.TSeries R n)
  (h : (a - 1).coeff 0 = 0) :
  a.log.exp = a

Hex.TSeries.exp_add.{u} {R : Type u} {n : ℕ} [Lean.Grind.CommRing R]
  [Hex.TSeries.NatInverses R (n - 1)] (a b : Hex.TSeries R n)
  (ha : a.coeff 0 = 0) (hb : b.coeff 0 = 0) :
  (a + b).exp = a.exp * b.exp
Hex.TSeries.exp_add.{u} {R : Type u}
  {n : ℕ} [Lean.Grind.CommRing R]
  [Hex.TSeries.NatInverses R (n - 1)]
  (a b : Hex.TSeries R n)
  (ha : a.coeff 0 = 0)
  (hb : b.coeff 0 = 0) :
  (a + b).exp = a.exp * b.exp