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

The reference Horner composition.

Equations

• a.compHorner b = Hex.TSeries.compHornerUpTo✝ n a b

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

Brent--Kung composition computed only below precision m.

Equations

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

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

Full-precision Brent--Kung composition.

Equations

• a.compBrentKung b = Hex.TSeries.compBrentKungUpTo n a b

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

Bounded composition used by Newton reversion.

Equations

• Hex.TSeries.compUpTo m a b = Hex.TSeries.compBrentKungUpTo m a b

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

Substitute b into a, using Brent--Kung composition.

Equations

• a.comp b = Hex.TSeries.compUpTo n a b

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

Check the zero-constant sufficient condition before composing.

Equations

• a.comp? b = if b.coeff 0 = 0 then some (a.comp b) else none

theorem Hex.TSeries.pow_vanish {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (b : TSeries R n) (h : b.coeff 0 = 0) (k : Nat) : Agree k (b ^ k) 0

A power of a series with zero constant coefficient vanishes below its exponent.

theorem Hex.TSeries.compHorner_spec {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a b : TSeries R n) : a.compHorner b = List.foldl (fun (acc : TSeries R n) (k : Nat) => acc + C (a.coeff k) * b.pow k) 0 (List.range n)

Horner composition is the finite coefficient-scaled power sum.

theorem Hex.TSeries.comp_eq_horner {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a b : TSeries R n) (h : b.coeff 0 = 0) : a.comp b = a.compHorner b

Brent--Kung and Horner agree under the zero-constant substitution condition.

theorem Hex.TSeries.coeff_compUpTo {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (m : Nat) (a b : TSeries R n) (h : b.coeff 0 = 0) (i : Nat) (hi : i < n) : (compUpTo m a b).coeff i = if i < m then (a.comp b).coeff i else 0

Bounded composition agrees with full composition below its bound.

theorem Hex.TSeries.comp_spec {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a b : TSeries R n) (h : b.coeff 0 = 0) : a.comp b = List.foldl (fun (acc : TSeries R n) (k : Nat) => acc + C (a.coeff k) * b.pow k) 0 (List.range n)

Composition is the finite truncated sum of coefficient-scaled powers.

@[simp]

theorem Hex.TSeries.comp_X_right {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a : TSeries R n) : a.comp X = a

Substituting x leaves a series unchanged.

@[simp]

theorem Hex.TSeries.comp_X_left {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (b : TSeries R n) (h : b.coeff 0 = 0) : X.comp b = b

Substituting a zero-constant series into x returns that series.

theorem Hex.TSeries.comp_mul {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a a' b : TSeries R n) (h : b.coeff 0 = 0) : (a * a').comp b = a.comp b * a'.comp b

Composition preserves multiplication under the zero-constant condition.

theorem Hex.TSeries.comp_add {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a a' b : TSeries R n) (h : b.coeff 0 = 0) : (a + a').comp b = a.comp b + a'.comp b

Substitution preserves addition when the inner series has zero constant coefficient.

@[simp]

theorem Hex.TSeries.comp_zero {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (b : TSeries R n) (h : b.coeff 0 = 0) : comp 0 b = 0

Substituting into the zero series gives zero.

@[simp]

theorem Hex.TSeries.comp_C {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (c : R) (b : TSeries R n) (h : b.coeff 0 = 0) : (C c).comp b = C c

Substitution leaves a constant series unchanged.

@[simp]

theorem Hex.TSeries.comp_zero_right {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a : TSeries R n) : a.comp 0 = C (a.coeff 0)

Substitution of zero extracts the outer constant coefficient.

@[simp]

theorem Hex.TSeries.comp_one {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (b : TSeries R n) (h : b.coeff 0 = 0) : comp 1 b = 1

Substituting into the one series gives one.

theorem Hex.TSeries.comp_pow {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a b : TSeries R n) (h : b.coeff 0 = 0) (k : Nat) : (a ^ k).comp b = a.comp b ^ k

Substitution preserves natural powers.

theorem Hex.TSeries.coeff_comp_zero {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a b : TSeries R n) (h : b.coeff 0 = 0) : (a.comp b).coeff 0 = a.coeff 0

Substitution by a zero-constant series preserves the outer constant coefficient.

theorem Hex.TSeries.comp_assoc {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a b c : TSeries R n) (hb : b.coeff 0 = 0) (hc : c.coeff 0 = 0) : (a.comp b).comp c = a.comp (b.comp c)

Substitution is associative when both inner series have zero constant coefficient.

theorem Hex.TSeries.Agree.comp_inner {R : Type u} {n : Nat} [Lean.Grind.CommRing R] {p : Nat} (a b b' : TSeries R n) (hb : Agree p b b') (h0 : b.coeff 0 = 0) (h0' : b'.coeff 0 = 0) : Agree p (a.comp b) (a.comp b')

Substitution by prefix-agreeing zero-constant inner series produces prefix-agreeing results.

theorem Hex.TSeries.Agree.compUpTo {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (p : Nat) (a b : TSeries R n) (h : b.coeff 0 = 0) : Agree p (TSeries.compUpTo p a b) (a.comp b)

Bounded substitution agrees with full substitution throughout its work prefix.