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

One bounded Newton reversion update.

Equations

• One or more equations did not get rendered due to their size.

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

Revert through coefficient m - 1, zeroing all later coefficients.

Equations

• One or more equations did not get rendered due to their size.

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

The compositional inverse of b, given an inverse of its linear coefficient.

Equations

• b.revOfUnit v = Hex.TSeries.revUpTo n b v

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

Check the constant coefficient and look up the linear inverse when that coefficient is represented.

Equations

• b.rev? = if b.coeff 0 ≠ 0 then none else if n ≤ 1 then some 0 else match Hex.TSeries.UnitOps.inv? (b.coeff 1) with | some v => some (b.revOfUnit v) | none => none

def Hex.TSeries.revLagrange {R : Type u} {n : Nat} [Lean.Grind.CommRing R] [NatInverses R (n - 1)] (b : TSeries R n) (v : R) : TSeries R n

Direct Lagrange inversion. This deliberately performs the explicit division by k and therefore carries NatInverses R (n-1). Consecutive powers are carried through the fold, so the schoolbook route performs n full multiplications and costs O(n³) rather than recomputing each power by square-and-multiply. When b.coeff 0 = 0, b = X * shiftQuotient b exactly; the unavailable top coefficient of the quotient is harmless because truncated multiplication is lower triangular.

Equations

• b.revLagrange v = (Hex.TSeries.lagrangeState✝ ((Hex.TSeries.shiftQuotient✝ b).invOfUnit v) n).snd

theorem Hex.TSeries.revUpTo_agree {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (m : Nat) (b : TSeries R n) (v : R) (h0 : b.coeff 0 = 0) (hv : b.coeff 1 * v = 1) : Agree m (revUpTo m b v) (b.revOfUnit v)

Bounded Newton reversion agrees with the full compositional inverse throughout the requested prefix.

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

Newton reversion is both a left and right compositional inverse.

theorem Hex.TSeries.revOfUnit_coeff_zero {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (b : TSeries R n) (v : R) (h0 : b.coeff 0 = 0) (hv : b.coeff 1 * v = 1) : (b.revOfUnit v).coeff 0 = 0

A Newton reversion has zero constant coefficient.

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

Direct Lagrange inversion agrees with Newton reversion whenever its explicit natural-number divisions are available.

theorem Hex.TSeries.revOfUnit_coeff_one {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (b : TSeries R n) (v : R) (h0 : b.coeff 0 = 0) (hv : b.coeff 1 * v = 1) (h : 1 < n) : (b.revOfUnit v).coeff 1 = v

The compositional inverse retains the supplied inverse linear coefficient.

theorem Hex.TSeries.rev_le_one {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (b : TSeries R n) (hn : n ≤ 1) (h0 : b.coeff 0 = 0) : b.comp 0 = X ∧ comp 0 b = X

At precision at most one, every zero-constant series reverts to zero.

theorem Hex.TSeries.revOfUnit_le_one {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (b : TSeries R n) (v : R) (hn : n ≤ 1) : b.revOfUnit v = 0

The bounded Newton implementation itself returns zero when no linear coefficient is represented.

theorem Hex.TSeries.rev_numerator_valuation {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (b : TSeries R n) (v : R) (h0 : b.coeff 0 = 0) (hv : b.coeff 1 * v = 1) (j i : Nat) (hi : i < min n (2 ^ j)) : (b.comp (newton (b.revStep v) (mulUpTo n (C v) X) j) - X).coeff i = 0

The Newton numerator vanishes throughout the precision already established by an iterate.

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

Optional reversion keeps the constant test at precision one while dropping the nonexistent linear test.