Documentation

CompPoly.LinearAlgebra.PolynomialMatrix.Approximant.PMBasis

Recursive PM-Basis #

Umbrella module for the divide-and-conquer PM-basis: executable definitions, correctness development, and the production PMBasisContext instances backed by the recursive driver with scalar dense-kernel leaves.

source
def CompPoly.PolynomialMatrix.Approximant.kernelLeafPMBasisContextWithLowAndCompose {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (lowCtx : MulLowContext F) (leafCutoff composeLeafCutoff : ℕ) :
PMBasisContext F

PM-basis context backed by the recursive driver, scalar dense-kernel leaves, and an independently tuned basis-composition cutoff.

Instances For
    source
    def CompPoly.PolynomialMatrix.Approximant.kernelLeafPMBasisContextWithLow {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (lowCtx : MulLowContext F) (leafCutoff : ℕ) :
    PMBasisContext F

    PM-basis context backed by the recursive driver and scalar dense-kernel leaves.

    Instances For
      source
      def CompPoly.PolynomialMatrix.Approximant.kernelLeafPMBasisContext {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (leafCutoff : ℕ) :
      PMBasisContext F

      PM-basis context whose low products are obtained by truncating full products.

      Instances For