def Hex.TSeries.convCoeff {R : Type u} [Zero R] [Add R] [Mul R] (f g : Nat → R) (i : Nat) : R

The coefficient of degree i in the product of two coefficient functions.

Equations

• Hex.TSeries.convCoeff f g i = List.foldl (fun (acc : R) (j : Nat) => acc + f j * g (i - j)) 0 (List.range (i + 1))

def Hex.TSeries.zero {R : Type u} {n : Nat} [Zero R] : TSeries R n

The zero truncated series.

Equations

• Hex.TSeries.zero = Hex.TSeries.ofFn fun (x : Nat) => 0

def Hex.TSeries.one {R : Type u} {n : Nat} [Zero R] [One R] : TSeries R n

The constant-one truncated series.

Equations

• Hex.TSeries.one = Hex.TSeries.ofFn fun (i : Nat) => if i = 0 then 1 else 0

def Hex.TSeries.add {R : Type u} {n : Nat} [Zero R] [Add R] (a b : TSeries R n) : TSeries R n

Coefficientwise addition of truncated series.

Equations

• a.add b = Hex.TSeries.ofFn fun (i : Nat) => a.coeff i + b.coeff i

def Hex.TSeries.neg {R : Type u} {n : Nat} [Zero R] [Neg R] (a : TSeries R n) : TSeries R n

Coefficientwise negation of a truncated series.

Equations

• a.neg = Hex.TSeries.ofFn fun (i : Nat) => -a.coeff i

def Hex.TSeries.sub {R : Type u} {n : Nat} [Zero R] [Sub R] (a b : TSeries R n) : TSeries R n

Coefficientwise subtraction of truncated series.

Equations

• a.sub b = Hex.TSeries.ofFn fun (i : Nat) => a.coeff i - b.coeff i

def Hex.TSeries.mul {R : Type u} {n : Nat} [Zero R] [Add R] [Mul R] (a b : TSeries R n) : TSeries R n

Schoolbook truncated convolution.

Equations

• a.mul b = Hex.TSeries.ofFn fun (i : Nat) => Hex.TSeries.convCoeff a.coeff b.coeff i

@[instance_reducible]

instance Hex.TSeries.instZero {R : Type u} {n : Nat} [Zero R] : Zero (TSeries R n)

Equations

• Hex.TSeries.instZero = { zero := Hex.TSeries.zero }

@[instance_reducible]

instance Hex.TSeries.instOneOfZero {R : Type u} {n : Nat} [Zero R] [One R] : One (TSeries R n)

Equations

• Hex.TSeries.instOneOfZero = { one := Hex.TSeries.one }

@[instance_reducible]

instance Hex.TSeries.instAddOfZero {R : Type u} {n : Nat} [Zero R] [Add R] : Add (TSeries R n)

Equations

• Hex.TSeries.instAddOfZero = { add := Hex.TSeries.add }

@[instance_reducible]

instance Hex.TSeries.instNegOfZero {R : Type u} {n : Nat} [Zero R] [Neg R] : Neg (TSeries R n)

Equations

• Hex.TSeries.instNegOfZero = { neg := Hex.TSeries.neg }

@[instance_reducible]

instance Hex.TSeries.instSubOfZero {R : Type u} {n : Nat} [Zero R] [Sub R] : Sub (TSeries R n)

Equations

• Hex.TSeries.instSubOfZero = { sub := Hex.TSeries.sub }

@[instance_reducible]

instance Hex.TSeries.instMulOfZeroOfAdd {R : Type u} {n : Nat} [Zero R] [Add R] [Mul R] : Mul (TSeries R n)

Equations

• Hex.TSeries.instMulOfZeroOfAdd = { mul := Hex.TSeries.mul }

def Hex.TSeries.C {R : Type u} {n : Nat} [Zero R] (c : R) : TSeries R n

The constant truncated series.

Equations

• Hex.TSeries.C c = Hex.TSeries.ofFn fun (i : Nat) => if i = 0 then c else 0

def Hex.TSeries.X {R : Type u} {n : Nat} [Zero R] [One R] : TSeries R n

The indeterminate x, which is zero at precisions zero and one.

Equations

• Hex.TSeries.X = Hex.TSeries.ofFn fun (i : Nat) => if i = 1 then 1 else 0

@[irreducible]

def Hex.TSeries.powLoop {R : Type u} {n : Nat} [Zero R] [One R] [Add R] [Mul R] (acc base : TSeries R n) (e : Nat) : TSeries R n

Tail-recursive square-and-multiply worker with an explicit accumulator.

Equations

• acc.powLoop base e = if he : e = 0 then acc else have acc' := if e % 2 = 1 then acc * base else acc; acc'.powLoop (base * base) (e / 2)

def Hex.TSeries.pow {R : Type u} {n : Nat} [Zero R] [One R] [Add R] [Mul R] (a : TSeries R n) (k : Nat) : TSeries R n

Truncated-series exponentiation by square-and-multiply.

Equations

• a.pow k = Hex.TSeries.powLoop 1 a k

@[instance_reducible]

instance Hex.TSeries.instPowNatOfZeroOfOneOfAddOfMul {R : Type u} {n : Nat} [Zero R] [One R] [Add R] [Mul R] : Pow (TSeries R n) Nat

Equations

• Hex.TSeries.instPowNatOfZeroOfOneOfAddOfMul = { pow := Hex.TSeries.pow }

def Hex.TSeries.mulUpTo {R : Type u} {n : Nat} [Zero R] [Add R] [Mul R] (m : Nat) (a b : TSeries R n) : TSeries R n

Multiply only through degree m - 1, zeroing the remaining stored coefficients.

Equations

• Hex.TSeries.mulUpTo m a b = Hex.TSeries.ofFn fun (i : Nat) => if i < m then Hex.TSeries.convCoeff a.coeff b.coeff i else 0

def Hex.TSeries.mulUpToImpl {R : Type u} {n : Nat} [Zero R] [Add R] [Mul R] (m : Nat) (a b : TSeries R n) : TSeries R n

Allocation-conscious implementation of mulUpTo. It writes only the requested prefix into one uniquely owned zero buffer.

Equations

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

theorem Hex.TSeries.coeff_modify {R : Type u} {n : Nat} [Zero R] (a : TSeries R n) (k i : Nat) (c : R) (hi : i < n) : { coeffs := a.coeffs.modify k fun (x : R) => c }.coeff i = if k = i then c else a.coeff i

Reading a represented coefficient after an in-place vector update sees the replacement exactly at the updated index.

@[csimp]

theorem Hex.TSeries.mulUpTo_eq_impl : @mulUpTo = @mulUpToImpl

Compiled bounded multiplication uses the single-buffer implementation.

@[simp]

theorem Hex.TSeries.coeff_zero {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (i : Nat) : coeff 0 i = 0

Every coefficient of the zero series is zero.

@[simp]

theorem Hex.TSeries.coeff_one {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (i : Nat) (hi : i < n) : coeff 1 i = if i = 0 then 1 else 0

The constant and higher coefficients of the one series.

@[simp]

theorem Hex.TSeries.coeff_add {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a b : TSeries R n) (i : Nat) (hi : i < n) : (a + b).coeff i = a.coeff i + b.coeff i

Coefficient extraction commutes with addition.

theorem Hex.TSeries.coeff_foldl_add {R : Type u} {n : Nat} [Lean.Grind.CommRing R] {α : Type} (xs : List α) (f : α → TSeries R n) (z : TSeries R n) (i : Nat) (hi : i < n) : (List.foldl (fun (acc : TSeries R n) (k : α) => acc + f k) z xs).coeff i = List.foldl (fun (acc : R) (k : α) => acc + (f k).coeff i) (z.coeff i) xs

Coefficient extraction commutes with a left fold of series addition.

@[simp]

theorem Hex.TSeries.coeff_neg {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a : TSeries R n) (i : Nat) (hi : i < n) : (-a).coeff i = -a.coeff i

Coefficient extraction commutes with negation.

@[simp]

theorem Hex.TSeries.coeff_sub {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a b : TSeries R n) (i : Nat) (hi : i < n) : (a - b).coeff i = a.coeff i - b.coeff i

Coefficient extraction commutes with subtraction.

theorem Hex.TSeries.coeff_mul {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a b : TSeries R n) (i : Nat) (hi : i < n) : (a * b).coeff i = convCoeff a.coeff b.coeff i

Product coefficients are the truncated convolution of the operands.

@[simp]

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

The constant coefficient of a product is the product of the constants.

@[simp]

theorem Hex.TSeries.coeff_C {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (c : R) (i : Nat) (hi : i < n) : (C c).coeff i = if i = 0 then c else 0

Coefficients of a constant series.

@[simp]

theorem Hex.TSeries.coeff_X {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (i : Nat) (hi : i < n) : X.coeff i = if i = 1 then 1 else 0

Coefficients of the indeterminate.

@[simp]

theorem Hex.TSeries.X_coeff_zero {R : Type u} {n : Nat} [Lean.Grind.CommRing R] : X.coeff 0 = 0

The indeterminate has zero constant coefficient at every precision.

@[simp]

theorem Hex.TSeries.C_one {R : Type u} {n : Nat} [Lean.Grind.CommRing R] : C 1 = 1

Embedding one as a constant series agrees with the series one.

@[simp]

theorem Hex.TSeries.C_zero {R : Type u} {n : Nat} [Lean.Grind.CommRing R] : C 0 = 0

Embedding zero as a constant series agrees with the series zero.

@[simp]

theorem Hex.TSeries.C_add {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a b : R) : C (a + b) = C a + C b

Constant-series embedding preserves addition.

@[simp]

theorem Hex.TSeries.C_mul {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a b : R) : C (a * b) = C a * C b

Constant-series embedding preserves multiplication.

@[simp]

theorem Hex.TSeries.coeff_C_mul {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (c : R) (a : TSeries R n) (i : Nat) (hi : i < n) : (C c * a).coeff i = c * a.coeff i

Left multiplication by a constant series scales every coefficient.

@[simp]

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

Bounded multiplication agrees with multiplication below its work bound and is zero above it.

@[instance_reducible]

instance Hex.TSeries.instNatCast {R : Type u} {n : Nat} [Lean.Grind.CommRing R] : NatCast (TSeries R n)

Natural casts are constant series.

Equations

• Hex.TSeries.instNatCast = { natCast := fun (k : Nat) => match k with | 0 => 0 | 1 => 1 | k.succ.succ => Hex.TSeries.C ↑(k + 2) }

@[instance_reducible]

instance Hex.TSeries.instOfNat {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (k : Nat) : OfNat (TSeries R n) k

Natural numerals are constant series.

Equations

• Hex.TSeries.instOfNat 0 = { ofNat := 0 }
• Hex.TSeries.instOfNat 1 = { ofNat := 1 }
• Hex.TSeries.instOfNat k_2.succ.succ = { ofNat := Hex.TSeries.C (OfNat.ofNat (k_2 + 2)) }

@[instance_reducible]

instance Hex.TSeries.instNSMul {R : Type u} {n : Nat} [Lean.Grind.CommRing R] : SMul Nat (TSeries R n)

Natural scalar multiplication is multiplication by a constant series.

Equations

• Hex.TSeries.instNSMul = { smul := fun (k : Nat) (a : Hex.TSeries R n) => ↑k * a }

@[instance_reducible]

instance Hex.TSeries.instIntCast {R : Type u} {n : Nat} [Lean.Grind.CommRing R] : IntCast (TSeries R n)

Integer casts are constant series.

Equations

• Hex.TSeries.instIntCast = { intCast := fun (i : Int) => match i with | Int.ofNat k => ↑k | Int.negSucc k => -↑(k + 1) }

@[instance_reducible]

instance Hex.TSeries.instZSMul {R : Type u} {n : Nat} [Lean.Grind.CommRing R] : SMul Int (TSeries R n)

Integer scalar multiplication uses the standard signed natural action.

Equations

• Hex.TSeries.instZSMul = { smul := fun (i : Int) (a : Hex.TSeries R n) => match i with | Int.ofNat k => k • a | Int.negSucc k => -((k + 1) • a) }

theorem Hex.TSeries.add_zero {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a : TSeries R n) : a + 0 = a

Zero is a right identity for truncated-series addition.

theorem Hex.TSeries.add_comm {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a b : TSeries R n) : a + b = b + a

Truncated-series addition is commutative.

theorem Hex.TSeries.add_assoc {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a b c : TSeries R n) : a + b + c = a + (b + c)

Truncated-series addition is associative.

theorem Hex.TSeries.mul_assoc {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a b c : TSeries R n) : a * b * c = a * (b * c)

Truncated-series multiplication is associative.

theorem Hex.TSeries.mul_one {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a : TSeries R n) : a * 1 = a

One is a right identity for truncated-series multiplication.

theorem Hex.TSeries.one_mul {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a : TSeries R n) : 1 * a = a

One is a left identity for truncated-series multiplication.

theorem Hex.TSeries.left_distrib {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a b c : TSeries R n) : a * (b + c) = a * b + a * c

Multiplication distributes over addition on the left.

theorem Hex.TSeries.right_distrib {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a b c : TSeries R n) : (a + b) * c = a * c + b * c

Multiplication distributes over addition on the right.

theorem Hex.TSeries.zero_mul {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a : TSeries R n) : 0 * a = 0

Zero annihilates truncated-series multiplication on the left.

theorem Hex.TSeries.mul_zero {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a : TSeries R n) : a * 0 = 0

Zero annihilates truncated-series multiplication on the right.

theorem Hex.TSeries.pow_zero {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a : TSeries R n) : a ^ 0 = 1

The zeroth power of a truncated series is one.

theorem Hex.TSeries.pow_succ {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a : TSeries R n) (k : Nat) : a ^ (k + 1) = a ^ k * a

Successor powers multiply the preceding power by the base.

theorem Hex.TSeries.pow_zero' {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a : TSeries R n) : a.pow 0 = 1

Direct-definition form of pow_zero, for bridges that also install a second lawful power operation.

theorem Hex.TSeries.pow_succ' {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a : TSeries R n) (k : Nat) : a.pow (k + 1) = a.pow k * a

Direct-definition form of pow_succ, for bridges that also install a second lawful power operation.

@[simp]

theorem Hex.TSeries.pow_one {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a : TSeries R n) : a ^ 1 = a

The first power of a truncated series is the series itself.

theorem Hex.TSeries.pow_add {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a : TSeries R n) (j k : Nat) : a ^ (j + k) = a ^ j * a ^ k

Powers at a sum of exponents split as a product.

theorem Hex.TSeries.pow_mul {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a : TSeries R n) (j k : Nat) : (a ^ j) ^ k = a ^ (j * k)

Iterated powers multiply their exponents.

theorem Hex.TSeries.ofNat_succ {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (k : Nat) : OfNat.ofNat (k + 1) = OfNat.ofNat k + 1

Successor numerals in truncated series agree with addition by one.

theorem Hex.TSeries.ofNat_eq_natCast {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (k : Nat) : OfNat.ofNat k = ↑k

Natural numerals agree with the natural-cast operation.

theorem Hex.TSeries.nsmul_eq_natCast_mul {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (k : Nat) (a : TSeries R n) : k • a = ↑k * a

Natural scalar multiplication is multiplication by the corresponding constant series.

theorem Hex.TSeries.neg_add_cancel {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a : TSeries R n) : -a + a = 0

Additive negation cancels a truncated series.

theorem Hex.TSeries.sub_eq_add_neg {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a b : TSeries R n) : a - b = a + -b

Subtraction agrees with addition of the negation.

theorem Hex.TSeries.neg_zsmul {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (i : Int) (a : TSeries R n) : -i • a = -(i • a)

Negating an integer scalar negates its scalar action.

theorem Hex.TSeries.intCast_neg {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (i : Int) : ↑(-i) = -↑i

Integer casts commute with negation.

theorem Hex.TSeries.mul_comm {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a b : TSeries R n) : a * b = b * a

Truncated-series multiplication is commutative.

@[simp]

theorem Hex.TSeries.coeff_mul_X {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a : TSeries R n) (i : Nat) (hi : i < n) : (a * X).coeff i = if i = 0 then 0 else a.coeff (i - 1)

Multiplication by X shifts coefficients upward by one.

@[simp]

theorem Hex.TSeries.coeff_X_pow {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (k i : Nat) (hi : i < n) : (X ^ k).coeff i = if i = k then 1 else 0

The coefficient of X ^ k is one in degree k and zero elsewhere.

@[simp]

theorem Hex.TSeries.coeff_X_pow_mul {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a : TSeries R n) (k i : Nat) (hi : i < n) : (X ^ k * a).coeff i = if k ≤ i then a.coeff (i - k) else 0

Multiplication by X ^ k shifts coefficients upward by k, with coefficients below that degree equal to zero.

theorem Hex.TSeries.coeff_C_mul_X_pow {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (c : R) (k i : Nat) (hi : i < n) : (C c * X ^ k).coeff i = if i = k then c else 0

A scalar monomial has its scalar coefficient in exactly one degree.

@[instance_reducible]

instance Hex.TSeries.instSemiringOfCommRing {R : Type u} {n : Nat} [Lean.Grind.CommRing R] : Lean.Grind.Semiring (TSeries R n)

Fixed-precision truncated series form a lightweight commutative ring.

Equations

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

@[instance_reducible]

instance Hex.TSeries.instRingOfCommRing {R : Type u} {n : Nat} [Lean.Grind.CommRing R] : Lean.Grind.Ring (TSeries R n)

Equations

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

@[instance_reducible]

instance Hex.TSeries.instCommRing {R : Type u} {n : Nat} [Lean.Grind.CommRing R] : Lean.Grind.CommRing (TSeries R n)

Equations

• Hex.TSeries.instCommRing = { toRing := Hex.TSeries.instRingOfCommRing, mul_comm := ⋯ }