X-Adic Approximant Problems

Basic data structures for approximant-basis computations over polynomial matrices.

References

• [Beckermann, B., and Labahn, G., A uniform approach for the fast computation of matrix-type Pade approximants][BL94]
• [Giorgi, P., Jeannerod, C.-P., and Villard, G., On the complexity of polynomial matrix computations][GJV03]

structure CompPoly.PolynomialMatrix.Approximant.XAdicProblem (F : Type u_2) [Zero F] : Type u_2

A row approximant problem p * matrix = 0 mod X^orders.

• orders : Array ℕ
• matrix : PolynomialMatrix F

def CompPoly.PolynomialMatrix.Approximant.maxOrder {F : Type u_1} [Zero F] (problem : XAdicProblem F) : ℕ

Maximum X-adic order in a problem.

def CompPoly.PolynomialMatrix.Approximant.totalOrder {F : Type u_1} [Zero F] (problem : XAdicProblem F) : ℕ

Sum of X-adic orders.

def CompPoly.PolynomialMatrix.Approximant.lowerOrders {F : Type u_1} [Zero F] (problem : XAdicProblem F) (d : ℕ) : Array ℕ

Truncate every problem order to at most d.

def CompPoly.PolynomialMatrix.Approximant.residualOrders {F : Type u_1} [Zero F] (problem : XAdicProblem F) (d : ℕ) : Array ℕ

Remaining orders after the first d coefficients have been consumed.

def CompPoly.PolynomialMatrix.Approximant.updateShiftByRows {F : Type u_1} [Zero F] [BEq F] (basis : PolynomialMatrix F) (shift : Array ℕ) : Array ℕ

Shift update used by the second recursive PM-basis call.

def CompPoly.PolynomialMatrix.Approximant.residualMatrixWithProduct {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (productKernel : Array ℕ → PolynomialMatrix F → PolynomialMatrix F → PolynomialMatrix F) (basis matrix : PolynomialMatrix F) (d : ℕ) (orders : Array ℕ) : PolynomialMatrix F

Residual matrix (P * A) div X^d, using an explicit product kernel and truncating to the requested residual orders columnwise.

def CompPoly.PolynomialMatrix.Approximant.residualMatrix {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (lowCtx : MulLowContext F) (basis matrix : PolynomialMatrix F) (d : ℕ) (orders : Array ℕ) : PolynomialMatrix F

Residual matrix (P * A) div X^d, truncated to the requested residual orders columnwise, using the direct low-product row-column kernel.