hex

2.3. Changing the precision🔗

Hex.TSeries.truncate keeps the coefficients below a smaller precision m. It is a ring homomorphism, so a computation at precision n also gives the answer at every smaller precision:

🔗theorem
Hex.TSeries.truncate_mul.{u} {R : Type u} {n m : ℕ}
  [Lean.Grind.CommRing R] (a b : Hex.TSeries R n) (h : m ≤ n) :
  (a * b).truncate m h = a.truncate m h * b.truncate m h
Hex.TSeries.truncate_mul.{u} {R : Type u}
  {n m : ℕ} [Lean.Grind.CommRing R]
  (a b : Hex.TSeries R n) (h : m ≤ n) :
  (a * b).truncate m h =
    a.truncate m h * b.truncate m h

Truncation preserves multiplication.

Hex.TSeries.extend goes the other way, padding with zeros to a larger precision. It is not a ring homomorphism, because it asserts that the coefficients it does not know are zero. At precision 2 the product x · x is 0, while after extending to precision 3 it is x²:

def x2 : TSeries Int 2 := X def x3 : TSeries Int 3 := x2.extend 3 (⊢ 2 ≤ 3 All goals completed! 🐙) #guard x2 * x2 = 0 #guard x3 * x3 ≠ (x2 * x2).extend 3 (⊢ 2 ≤ 3 All goals completed! 🐙)

So extend gives the right answer when the missing coefficients are known to vanish, for example for a polynomial of degree less than n. Hex.TSeries.mulXPow multiplies by xᵏ, discarding the top k coefficients. Hex.TSeries.divXPow? divides by xᵏ, and returns none unless the bottom k coefficients are zero; its result has precision n - k, since the top k coefficients of the quotient are unknown. Hex.TSeries.valuation? finds the first nonzero coefficient, and returns none for the zero series:

def shifted : TSeries Int 6 := X ^ 2 * (3 + X) (some 2, some #v[3, 1, 0, 0], none)#eval (shifted.valuation?, (shifted.divXPow? 2).map (·.coeffs), (shifted.divXPow? 3).map (·.coeffs)) 
(some 2, some #v[3, 1, 0, 0], none)

The derivative Hex.TSeries.deriv also loses precision: the coefficient of xⁿ⁻¹ in the derivative is n aₙ, and aₙ is not known, so the derivative of a series of precision n has precision n - 1. Hex.TSeries.integrate gains one, returning the integral with constant coefficient 0 at precision n + 1. It divides the coefficient of xᵏ⁻¹ by k for k = 1, …, n, and so needs those inverses in R, which are supplied by an instance of Hex.TSeries.NatInverses:

🔗type class
Hex.TSeries.NatInverses.{u} (R : Type u) [Lean.Grind.CommRing R]
  (m : ℕ) : Type u
Hex.TSeries.NatInverses.{u} (R : Type u)
  [Lean.Grind.CommRing R] (m : ℕ) : Type u

Inverses of the natural numbers 1 through m in R.

Instance Constructor

Hex.TSeries.NatInverses.mk.{u}

Methods

invNat : ℕ → R

A total lookup whose values are constrained on 1, ..., m.

invNat_eq : ∀ (k : ℕ), 1 ≤ k → k ≤ m → ↑k * Hex.TSeries.NatInverses.invNat m k = 1

The lookup inverts every required natural number.

In each case the loss or gain of precision is part of the type. A caller who needs n coefficients of a derivative computes at precision n + 1.