def Hex.DensePoly.reverseSeries {R : Type u} [Zero R] [DecidableEq R] (f : DensePoly R) (n : Nat) : TSeries R n

Reverse a dense polynomial from its leading end into an exactly n-term truncated series, padding with zeros when n exceeds the polynomial size.

Equations

• f.reverseSeries n = Hex.TSeries.ofFn fun (i : Nat) => if i < f.size then f.coeff (f.size - 1 - i) else 0

theorem Hex.DensePoly.coeff_reverseSeries {R : Type u} [Zero R] [DecidableEq R] (f : DensePoly R) (n i : Nat) (hi : i < n) : (f.reverseSeries n).coeff i = if i < f.size then f.coeff (f.size - 1 - i) else 0

Coefficient law for zero-extending polynomial reversal.

theorem Hex.DensePoly.coeff_reverseSeries_of_lt {R : Type u} [Zero R] [DecidableEq R] (f : DensePoly R) (n i : Nat) (hi : i < n) (hf : i < f.size) : (f.reverseSeries n).coeff i = f.coeff (f.size - 1 - i)

Inside the polynomial support, reversal reads down from the leading coefficient.

theorem Hex.DensePoly.coeff_reverseSeries_of_size_le {R : Type u} [Zero R] [DecidableEq R] (f : DensePoly R) (n i : Nat) (hi : i < n) (hf : f.size ≤ i) : (f.reverseSeries n).coeff i = 0

Outside the polynomial support, reversal is zero rather than the constant coefficient selected by saturated Nat subtraction.

def Hex.DensePoly.polyOfSeries {R : Type u} [Zero R] [DecidableEq R] {n : Nat} (a : TSeries R n) : DensePoly R

Convert all represented coefficients of a truncated series to a normalized dense polynomial.

Equations

• Hex.DensePoly.polyOfSeries a = Hex.DensePoly.ofList (List.map a.coeff (List.range n))

theorem Hex.DensePoly.coeff_polyOfSeries {R : Type u} [Zero R] [DecidableEq R] {n : Nat} (a : TSeries R n) (i : Nat) : (polyOfSeries a).coeff i = if i < n then a.coeff i else 0

Coefficient law for conversion from a fixed series prefix.

theorem Hex.DensePoly.coeff_polyOfSeries_of_lt {R : Type u} [Zero R] [DecidableEq R] {n : Nat} (a : TSeries R n) (i : Nat) (hi : i < n) : (polyOfSeries a).coeff i = a.coeff i

Converting a series to a polynomial and reading a represented coefficient returns the original coefficient.

theorem Hex.DensePoly.coeff_polyOf_reverseSeries {R : Type u} [Zero R] [DecidableEq R] (f : DensePoly R) (n i : Nat) : (polyOfSeries (f.reverseSeries n)).coeff i = if i < n then if i < f.size then f.coeff (f.size - 1 - i) else 0 else 0

Converting a reversed polynomial prefix back to a polynomial exposes the same guarded reversal coefficient law.