def Hex.TSeries.invStep {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a b : TSeries R n) (m : Nat) : TSeries R n

One bounded Newton inverse update.

Equations

• a.invStep b m = Hex.TSeries.mulUpTo m b (Hex.TSeries.C (1 + 1) - Hex.TSeries.mulUpTo m a b)

def Hex.TSeries.invUpTo {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (m : Nat) (a : TSeries R n) (u : R) : TSeries R n

Invert through coefficient m - 1, zeroing all later stored coefficients.

Equations

• Hex.TSeries.invUpTo m a u = Hex.TSeries.ofFn fun (i : Nat) => if i < m then (Hex.TSeries.newton a.invStep (Hex.TSeries.C u) (Hex.TSeries.steps (min m n))).coeff i else 0

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

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

Equations

• a.invOfUnit u = Hex.TSeries.invUpTo n a u

def Hex.TSeries.inv? {R : Type u} {n : Nat} [Lean.Grind.CommRing R] [UnitOps R] (a : TSeries R n) : Option (TSeries R n)

Look up a constant-coefficient inverse and invert the series.

Equations

• a.inv? = if n = 0 then some 0 else match Hex.TSeries.UnitOps.inv? (a.coeff 0) with | some u => some (a.invOfUnit u) | none => none

theorem Hex.TSeries.coeff_invUpTo {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (m : Nat) (a : TSeries R n) (u : R) (hu : a.coeff 0 * u = 1) (i : Nat) (hi : i < n) : (invUpTo m a u).coeff i = if i < m then (a.invOfUnit u).coeff i else 0

Bounded inversion agrees with full inversion below its requested bound.

theorem Hex.TSeries.invOfUnit_mul {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a : 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 {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a b : 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.

theorem Hex.TSeries.inv?_isSome_iff {R : Type u} {n : Nat} [Lean.Grind.CommRing R] [UnitOps R] [LawfulUnitOps R] (a : TSeries R n) : a.inv?.isSome = true ↔ n = 0 ∨ ∃ (u : R), a.coeff 0 * u = 1

Optional inversion succeeds exactly for units of the truncated-series ring, including the unconditional precision-zero case.