2.4. Inverses and Newton's method🔗

For n ≥ 1, a series is a unit of TSeries R n exactly when its constant coefficient is a unit of R.

def

Hex.TSeries.invOfUnit.{u} {R : Type u} {n : ℕ} [Lean.Grind.CommRing R]
  (a : Hex.TSeries R n) (u : R) : Hex.TSeries R n
Hex.TSeries.invOfUnit.{u} {R : Type u}
  {n : ℕ} [Lean.Grind.CommRing R]
  (a : Hex.TSeries R n) (u : R) :
  Hex.TSeries R n

The inverse of a, given an inverse of its constant coefficient.

If b inverts a modulo xᵏ, then b(2 - ab) inverts a modulo x²ᵏ. invOfUnit a u starts from the constant u and applies this step ⌈log₂ n⌉ times. The step that reaches precision 2k computes its products only below x²ᵏ, using Hex.TSeries.mulUpTo. Each step then costs about a quarter of the step after it, and the whole inverse costs a constant multiple of a single multiplication at precision n. The library proves that the result is an inverse, and that it is the only one:

theorem

Hex.TSeries.invOfUnit_mul.{u} {R : Type u} {n : ℕ}
  [Lean.Grind.CommRing R] (a : Hex.TSeries R n) (u : R)
  (hu : a.coeff 0 * u = 1) : a * a.invOfUnit u = 1
Hex.TSeries.invOfUnit_mul.{u} {R : Type u}
  {n : ℕ} [Lean.Grind.CommRing R]
  (a : Hex.TSeries R n) (u : R)
  (hu : a.coeff 0 * u = 1) :
  a * a.invOfUnit u = 1

Newton inversion satisfies the defining multiplicative equation.

theorem

Hex.TSeries.invOfUnit_unique.{u} {R : Type u} {n : ℕ}
  [Lean.Grind.CommRing R] (a b : Hex.TSeries R n) (u : R)
  (hu : a.coeff 0 * u = 1) (hb : a * b = 1) : b = a.invOfUnit u
Hex.TSeries.invOfUnit_unique.{u}
  {R : Type u} {n : ℕ}
  [Lean.Grind.CommRing R]
  (a b : Hex.TSeries R n) (u : R)
  (hu : a.coeff 0 * u = 1)
  (hb : a * b = 1) : b = a.invOfUnit u

A multiplicative inverse with the supplied constant witness is unique.

invOfUnit does not check its witness. Given a u that does not invert the constant coefficient it returns some series, and the theorems above say nothing about it. Hex.TSeries.inv? finds the witness itself, using a Hex.TSeries.UnitOps instance on R. When the lookup is also lawful, that is, it finds an inverse exactly for the units of R (Hex.TSeries.LawfulUnitOps), inv? returns none exactly when the series is not a unit (Hex.TSeries.inv?_isSome_iff). The library provides lawful instances for Int and Rat. The series 2 - x is not a unit over ℤ, and over ℚ its inverse is 1/2 + x/4 + x²/8 + ⋯:

def twoMinusX : TSeries Int 5 := 2 - X
def twoMinusXQ : TSeries Rat 5 := 2 - X

(none, some #v[(1 : Rat)/2, (1 : Rat)/4, (1 : Rat)/8, (1 : Rat)/16, (1 : Rat)/32])#eval ((inv? twoMinusX).map (·.coeffs),
  (inv? twoMinusXQ).map (·.coeffs))

(none, some #v[(1 : Rat)/2, (1 : Rat)/4, (1 : Rat)/8, (1 : Rat)/16, (1 : Rat)/32])

The square root, exponential and compositional inverse below are computed by Newton's method in the same way, with the same bounded steps.