structure Hex.TSeries (R : Type u) (n : Nat) : Type u

A power series over R truncated at precision n, represented by its coefficients in ascending degree order.

• coeffs : Vector R n

  The coefficients of x^0 through x^(n-1).

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

The coefficient of x^i, read as zero when i is beyond the precision.

Equations

• a.coeff i = if h : i < n then a.coeffs[i] else 0

def Hex.TSeries.ofFn {R : Type u} {n : Nat} (f : Nat → R) : TSeries R n

Tabulate a truncated series from a total coefficient function.

Equations

• Hex.TSeries.ofFn f = { coeffs := Hex.Vector.ofFn' fun (i : Fin n) => f ↑i }

@[simp]

theorem Hex.TSeries.coeff_ofFn {R : Type u} {n : Nat} [Zero R] (f : Nat → R) (i : Nat) (hi : i < n) : (ofFn f).coeff i = f i

Tabulation stores the requested coefficient at every represented index.

theorem Hex.TSeries.ext {R : Type u} {n : Nat} [Zero R] {a b : TSeries R n} (h : ∀ (i : Nat), i < n → a.coeff i = b.coeff i) : a = b

Two truncated series are equal when all represented coefficients agree.

theorem Hex.TSeries.ext_iff {R : Type u} {n : Nat} [Zero R] {a b : TSeries R n} : a = b ↔ ∀ (i : Nat), i < n → a.coeff i = b.coeff i

@[instance_reducible]

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

Kernel-reducible equality, routed through HexBasic's vector equality.

Equations

• a.instDecidableEq b = match h : decEq a.coeffs b.coeffs with | { decide := true, reflects_decide := ht } => isTrue ⋯ | { decide := false, reflects_decide := hf } => isFalse ⋯