Documentation

CompPoly.Univariate.CoefficientInterpolation

Coefficient-Form Interpolation from a Vanishing Polynomial #

Build the coefficient polynomial interpolating packed points from the node vanishing polynomial G = ∏ᵢ (X - xᵢ) using the formula R = ∑ᵢ yᵢ / G'(xᵢ) * G / (X - xᵢ).

source
def CompPoly.CPolynomial.divByLinearFactor {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (p : CPolynomial F) (x : F) :
CPolynomial F

Synthetic quotient by the monic linear factor X - x.

This is the quotient part of division by X - x, computed in one high-to-low coefficient pass. When x is a root of p, it is exactly p / (X - x).

Instances For
    source
    theorem CompPoly.CPolynomial.divByLinearFactor_eq_divByMonic {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (p : CPolynomial F) (x : F) :
    p.divByLinearFactor x = p.divByMonic (linearFactor x)

    Synthetic division by X - x agrees with generic monic division.

    source
    def CompPoly.CPolynomial.interpolationTermWithVanishing {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (G : CPolynomial F) (point : F × F) (derivativeValue : F) :
    CPolynomial F

    One coefficient-form interpolation term from a packed point and G'(xᵢ).

    Instances For
      source
      def CompPoly.CPolynomial.interpolateCoefficientFormWithVanishing {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (E : BatchEvalContext F) (G : CPolynomial F) (points : Array (F × F)) :
      CPolynomial F

      Coefficient-form interpolation from packed points and an already-built node vanishing polynomial. The supplied batch evaluator is used only for the G' evaluations at the interpolation nodes.

      Instances For
        source
        def CompPoly.CPolynomial.interpolateCoefficientForm {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (V : VanishingPolynomialContext F) (E : BatchEvalContext F) (points : Array (F × F)) :
        CPolynomial F

        Coefficient-form interpolation from packed points using a vanishing-polynomial context and a batch-evaluation context.

        Instances For
          source
          theorem CompPoly.CPolynomial.interpolateCoefficientForm_eval_point {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (V : VanishingPolynomialContext F) (E : BatchEvalContext F) {points : Array (F × F)} (hdistinct : (List.map (fun (point : F × F) => point.1) points.toList).Nodup) {point : F × F} (hpoint : point ∈ points.toList) :
          eval point.1 (interpolateCoefficientForm V E points) = point.2

          Coefficient-form interpolation evaluates to the packed values at distinct nodes.