def Hex.TSeries.truncate {R : Type u} {n : Nat} [Zero R] (a : TSeries R n) (m : Nat) (_h : m ≤ n) : TSeries R m

Discard coefficients at index m and above.

Equations

• a.truncate m _h = Hex.TSeries.ofFn a.coeff

def Hex.TSeries.extend {R : Type u} {n : Nat} [Zero R] (a : TSeries R n) (m : Nat) (_h : n ≤ m) : TSeries R m

Pad a series with zero coefficients to a larger precision.

Equations

• a.extend m _h = Hex.TSeries.ofFn a.coeff

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

Multiply by x^k, discarding coefficients shifted beyond the precision.

Equations

• a.mulXPow k = Hex.TSeries.ofFn fun (i : Nat) => if k ≤ i then a.coeff (i - k) else 0

def Hex.TSeries.allZeroBelow {R : Type u} {n : Nat} [Zero R] [DecidableEq R] (a : TSeries R n) (m : Nat) : Bool

Whether every coefficient below m is zero.

Equations

• a.allZeroBelow m = (List.range m).all fun (i : Nat) => decide (a.coeff i = 0)

def Hex.TSeries.divXPow? {R : Type u} {n : Nat} [Zero R] [DecidableEq R] (a : TSeries R n) (k : Nat) : Option (TSeries R (n - k))

Divide by x^k when every discarded low coefficient is zero.

Equations

• a.divXPow? k = if a.allZeroBelow (min k n) = true then some (Hex.TSeries.ofFn fun (i : Nat) => a.coeff (i + k)) else none

def Hex.TSeries.valuation? {R : Type u} {n : Nat} [Zero R] [DecidableEq R] (a : TSeries R n) : Option Nat

The first represented nonzero coefficient, if one exists.

Equations

• a.valuation? = List.find? (fun (i : Nat) => decide (a.coeff i ≠ 0)) (List.range n)

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

The formal derivative, losing one coefficient of precision.

Equations

• a.deriv = Hex.TSeries.ofFn fun (i : Nat) => ↑(i + 1) * a.coeff (i + 1)

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

The derivative retained at the input precision, with the unavailable top coefficient set to zero.

Equations

• a.derivPad = Hex.TSeries.ofFn fun (i : Nat) => if i + 1 < n then ↑(i + 1) * a.coeff (i + 1) else 0

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

Formal integration with zero constant coefficient.

Equations

• a.integrate = Hex.TSeries.ofFn fun (i : Nat) => if i = 0 then 0 else Hex.TSeries.NatInverses.invNat n i * a.coeff (i - 1)

@[simp]

theorem Hex.TSeries.coeff_truncate {R : Type u} {n m : Nat} [Lean.Grind.CommRing R] (a : TSeries R n) (h : m ≤ n) (i : Nat) (hi : i < m) : (a.truncate m h).coeff i = a.coeff i

Truncation preserves every coefficient in the retained prefix.

@[simp]

theorem Hex.TSeries.coeff_extend {R : Type u} {n m : Nat} [Lean.Grind.CommRing R] (a : TSeries R n) (h : n ≤ m) (i : Nat) (hi : i < m) : (a.extend m h).coeff i = a.coeff i

Zero extension preserves represented coefficients and reads zero above the source precision through total coefficient access.

@[simp]

theorem Hex.TSeries.truncate_extend {R : Type u} {n m : Nat} [Lean.Grind.CommRing R] (a : TSeries R n) (h : n ≤ m) : (a.extend m h).truncate n h = a

Truncating a zero extension back to its source precision is the identity.

@[simp]

theorem Hex.TSeries.truncate_zero {R : Type u} {n m : Nat} [Lean.Grind.CommRing R] (h : m ≤ n) : truncate 0 m h = 0

Truncation preserves zero.

@[simp]

theorem Hex.TSeries.truncate_one {R : Type u} {n m : Nat} [Lean.Grind.CommRing R] (h : m ≤ n) : truncate 1 m h = 1

Truncation preserves one.

@[simp]

theorem Hex.TSeries.truncate_add {R : Type u} {n m : Nat} [Lean.Grind.CommRing R] (a b : TSeries R n) (h : m ≤ n) : (a + b).truncate m h = a.truncate m h + b.truncate m h

Truncation preserves addition.

@[simp]

theorem Hex.TSeries.truncate_neg {R : Type u} {n m : Nat} [Lean.Grind.CommRing R] (a : TSeries R n) (h : m ≤ n) : (-a).truncate m h = -a.truncate m h

Truncation preserves negation.

@[simp]

theorem Hex.TSeries.truncate_sub {R : Type u} {n m : Nat} [Lean.Grind.CommRing R] (a b : TSeries R n) (h : m ≤ n) : (a - b).truncate m h = a.truncate m h - b.truncate m h

Truncation preserves subtraction.

@[simp]

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

Multiplication by x^k shifts coefficients upward by k.

theorem Hex.TSeries.allZeroBelow_eq_true {R : Type u} {n : Nat} [Lean.Grind.CommRing R] [DecidableEq R] (a : TSeries R n) (m : Nat) : a.allZeroBelow m = true ↔ ∀ (i : Nat), i < m → a.coeff i = 0

The zero-prefix test succeeds exactly when every tested coefficient vanishes.

theorem Hex.TSeries.allZeroBelow_eq_false {R : Type u} {n : Nat} [Lean.Grind.CommRing R] [DecidableEq R] (a : TSeries R n) (m : Nat) : a.allZeroBelow m = false ↔ ∃ (i : Nat), i < m ∧ a.coeff i ≠ 0

The zero-prefix test fails exactly when it encounters a nonzero coefficient.

theorem Hex.TSeries.divXPow?_isSome_iff {R : Type u} {n : Nat} [Lean.Grind.CommRing R] [DecidableEq R] (a : TSeries R n) (k : Nat) : (a.divXPow? k).isSome = true ↔ ∀ (i : Nat), i < min k n → a.coeff i = 0

Division by x^k succeeds exactly when every discarded represented coefficient is zero.

theorem Hex.TSeries.divXPow?_eq_none_iff {R : Type u} {n : Nat} [Lean.Grind.CommRing R] [DecidableEq R] (a : TSeries R n) (k : Nat) : a.divXPow? k = none ↔ ∃ (i : Nat), i < min k n ∧ a.coeff i ≠ 0

Division by x^k fails exactly when a discarded represented coefficient is nonzero.

theorem Hex.TSeries.coeff_divXPow?_eq_some {R : Type u} {n : Nat} [Lean.Grind.CommRing R] [DecidableEq R] (a : TSeries R n) (k : Nat) {b : TSeries R (n - k)} (h : a.divXPow? k = some b) (i : Nat) (hi : i < n - k) : b.coeff i = a.coeff (i + k)

A successful division by x^k exposes the shifted coefficients.

theorem Hex.TSeries.divXPow?_eq_some_iff {R : Type u} {n : Nat} [Lean.Grind.CommRing R] [DecidableEq R] (a : TSeries R n) (k : Nat) (b : TSeries R (n - k)) : a.divXPow? k = some b ↔ (∀ (i : Nat), i < min k n → a.coeff i = 0) ∧ ∀ (i : Nat), i < n - k → b.coeff i = a.coeff (i + k)

The complete characterization of a successful division by x^k.

@[simp]

theorem Hex.TSeries.divXPow?_mulXPow {R : Type u} {n : Nat} [Lean.Grind.CommRing R] [DecidableEq R] (a : TSeries R n) (k : Nat) : (a.mulXPow k).divXPow? k = some (a.truncate (n - k) ⋯)

Multiplying by x^k and then dividing recovers the represented prefix of the input.

theorem Hex.TSeries.mulXPow_extend_divXPow?_eq {R : Type u} {n : Nat} [Lean.Grind.CommRing R] [DecidableEq R] (a : TSeries R n) (k : Nat) (b : TSeries R (n - k)) (h : a.divXPow? k = some b) : (b.extend n ⋯).mulXPow k = a

Extending a successful quotient and multiplying back by x^k recovers the dividend.

theorem Hex.TSeries.valuation?_eq_some_iff {R : Type u} {n : Nat} [Lean.Grind.CommRing R] [DecidableEq R] (a : TSeries R n) (k : Nat) : a.valuation? = some k ↔ k < n ∧ a.coeff k ≠ 0 ∧ ∀ (i : Nat), i < k → a.coeff i = 0

A successful valuation search identifies a represented nonzero coefficient and proves every earlier coefficient zero.

theorem Hex.TSeries.valuation?_eq_none_iff {R : Type u} {n : Nat} [Lean.Grind.CommRing R] [DecidableEq R] (a : TSeries R n) : a.valuation? = none ↔ ∀ (i : Nat), i < n → a.coeff i = 0

A failed valuation search means that every represented coefficient is zero.

@[simp]

theorem Hex.TSeries.valuation?_eq_none_iff_eq_zero {R : Type u} {n : Nat} [Lean.Grind.CommRing R] [DecidableEq R] (a : TSeries R n) : a.valuation? = none ↔ a = 0

The valuation search fails exactly on the zero truncated series.

theorem Hex.TSeries.coeff_ne_zero_of_valuation?_eq_some {R : Type u} {n : Nat} [Lean.Grind.CommRing R] [DecidableEq R] (a : TSeries R n) (k : Nat) (h : a.valuation? = some k) : a.coeff k ≠ 0

The coefficient selected by a successful valuation search is nonzero.

theorem Hex.TSeries.coeff_eq_zero_of_lt_valuation {R : Type u} {n : Nat} [Lean.Grind.CommRing R] [DecidableEq R] (a : TSeries R n) (k i : Nat) (h : a.valuation? = some k) (hi : i < k) : a.coeff i = 0

Every coefficient below a successful valuation is zero.

@[simp]

theorem Hex.TSeries.coeff_deriv {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a : TSeries R n) (i : Nat) (hi : i < n - 1) : a.deriv.coeff i = ↑(i + 1) * a.coeff (i + 1)

Coefficients of the precision-losing formal derivative.

@[simp]

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

Coefficients of the precision-preserving padded derivative.

@[simp]

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

Coefficients of zero-constant formal integration.

theorem Hex.TSeries.integrate_congr {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a : TSeries R n) (h₁ h₂ : NatInverses R n) : a.integrate = a.integrate

Integration is independent of which lawful natural-inverse dictionary is in scope.

@[simp]

theorem Hex.TSeries.deriv_integrate {R : Type u} {n : Nat} [Lean.Grind.CommRing R] [NatInverses R n] (a : TSeries R n) : a.integrate.deriv = a

Differentiation cancels zero-constant integration at every represented coefficient.

theorem Hex.TSeries.deriv_mul {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a b : TSeries R n) : (a * b).deriv = a.deriv * b.truncate (n - 1) ⋯ + a.truncate (n - 1) ⋯ * b.deriv

Formal differentiation obeys the product rule after both undifferentiated factors are truncated to the derivative's precision.

@[simp]

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

The precision-preserving derivative is additive.

@[simp]

theorem Hex.TSeries.derivPad_C {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (c : R) : (C c).derivPad = 0

The precision-preserving derivative kills constant series.

@[simp]

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

The precision-preserving derivative kills zero.

@[simp]

theorem Hex.TSeries.derivPad_one {R : Type u} {n : Nat} [Lean.Grind.CommRing R] : derivPad 1 = 0

The precision-preserving derivative kills one.

@[simp]

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

A constant scalar factors through the precision-preserving derivative.

theorem Hex.TSeries.derivPad_foldl_add {R : Type u} {n : Nat} [Lean.Grind.CommRing R] {α : Type} (xs : List α) (f : α → TSeries R n) (z : TSeries R n) : (List.foldl (fun (acc : TSeries R n) (x : α) => acc + f x) z xs).derivPad = List.foldl (fun (acc : TSeries R n) (x : α) => acc + (f x).derivPad) z.derivPad xs

The precision-preserving derivative commutes with an additive fold.

theorem Hex.TSeries.eq_of_deriv {R : Type u} {n : Nat} [Lean.Grind.CommRing R] [NatInverses R (n - 1)] {a b : TSeries R n} (h0 : a.coeff 0 = b.coeff 0) (hderiv : a.deriv = b.deriv) : a = b

Two truncated series with the same constant coefficient and derivative are equal when all represented positive naturals are invertible.

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

Truncation preserves multiplication.

def Hex.TSeries.Agree {R : Type u} {n : Nat} [Zero R] (p : Nat) (a b : TSeries R n) : Prop

Two series have the same represented coefficients below p.

Equations

• Hex.TSeries.Agree p a b = ∀ (i : Nat), i < n → i < p → a.coeff i = b.coeff i

theorem Hex.TSeries.derivPad_mul_agree {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a b : TSeries R n) : Agree (n - 1) (a * b).derivPad (a.derivPad * b + a * b.derivPad)

The product rule for derivPad holds through the last coefficient whose successor is represented.

theorem Hex.TSeries.derivPad_X_agree {R : Type u} {n : Nat} [Lean.Grind.CommRing R] : Agree (n - 1) X.derivPad 1

The padded derivative of X is one throughout the honest derivative prefix.

theorem Hex.TSeries.Agree.refl {R : Type u} {n : Nat} [Zero R] (p : Nat) (a : TSeries R n) : Agree p a a

Every series agrees with itself at every precision.

theorem Hex.TSeries.Agree.symm {R : Type u} {n : Nat} [Zero R] {p : Nat} {a b : TSeries R n} (h : Agree p a b) : Agree p b a

Prefix agreement is symmetric.

theorem Hex.TSeries.Agree.trans {R : Type u} {n : Nat} [Zero R] {p : Nat} {a b c : TSeries R n} (hab : Agree p a b) (hbc : Agree p b c) : Agree p a c

Prefix agreement is transitive.

theorem Hex.TSeries.Agree.mono {R : Type u} {n : Nat} [Zero R] {p q : Nat} {a b : TSeries R n} (h : Agree p a b) (hpq : q ≤ p) : Agree q a b

Agreement through a precision implies agreement through every smaller precision.

theorem Hex.TSeries.Agree.full {R : Type u} {n : Nat} [Zero R] {p : Nat} {a b : TSeries R n} (h : Agree p a b) (hnp : n ≤ p) : a = b

Agreement through the represented precision implies series equality.

theorem Hex.TSeries.Agree.add {R : Type u} {n : Nat} [Lean.Grind.CommRing R] {p : Nat} {a a' b b' : TSeries R n} (ha : Agree p a a') (hb : Agree p b b') : Agree p (a + b) (a' + b')

Prefix agreement is preserved by addition.

theorem Hex.TSeries.Agree.foldl_add {R : Type u} {n : Nat} [Lean.Grind.CommRing R] {α : Type} {p : Nat} (xs : List α) (f g : α → TSeries R n) (h : ∀ (x : α), x ∈ xs → Agree p (f x) (g x)) : Agree p (List.foldl (fun (acc : TSeries R n) (x : α) => acc + f x) 0 xs) (List.foldl (fun (acc : TSeries R n) (x : α) => acc + g x) 0 xs)

Pointwise agreement of summands is preserved by an additive fold.

theorem Hex.TSeries.Agree.neg {R : Type u} {n : Nat} [Lean.Grind.CommRing R] {p : Nat} {a a' : TSeries R n} (ha : Agree p a a') : Agree p (-a) (-a')

Prefix agreement is preserved by negation.

theorem Hex.TSeries.Agree.sub {R : Type u} {n : Nat} [Lean.Grind.CommRing R] {p : Nat} {a a' b b' : TSeries R n} (ha : Agree p a a') (hb : Agree p b b') : Agree p (a - b) (a' - b')

Prefix agreement is preserved by subtraction.

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

If a difference vanishes through a prefix, its terms agree there.

theorem Hex.TSeries.Agree.mul {R : Type u} {n : Nat} [Lean.Grind.CommRing R] {p : Nat} {a a' b b' : TSeries R n} (ha : Agree p a a') (hb : Agree p b b') : Agree p (a * b) (a' * b')

Prefix agreement is preserved by multiplication.

theorem Hex.TSeries.Agree.pow {R : Type u} {n : Nat} [Lean.Grind.CommRing R] {p : Nat} {a b : TSeries R n} (h : Agree p a b) (k : Nat) : Agree p (a ^ k) (b ^ k)

Prefix agreement is preserved by natural powers.

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

A bounded product agrees with the ordinary product throughout its work prefix.

@[simp]

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

Multiplication bounded at the represented precision is ordinary multiplication.

theorem Hex.TSeries.Agree.zeroMul {R : Type u} {n : Nat} [Lean.Grind.CommRing R] {p q : Nat} {a b : TSeries R n} (ha : Agree p a 0) (hb : Agree q b 0) : Agree (p + q) (a * b) 0

Orders add under multiplication: a product of two vanishing prefixes vanishes through the sum of their lengths.

theorem Hex.TSeries.derivPad_pow_agree {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a : TSeries R n) (k : Nat) : Agree (n - 1) (a ^ k).derivPad (C ↑k * a ^ (k - 1) * a.derivPad)

The power rule for derivPad holds throughout its honest prefix.