Documentation

CompPoly.Bivariate.Deriv

Partial Derivatives and Multiplicity of Computable Bivariate Polynomials #

This file defines partial derivatives (partialDerivX, partialDerivY, iterated and mixed partials) and the multiplicity condition hasMultiplicity used in the Guruswami–Sudan interpolation step.

Multiplicity of a root at (a, b) is defined through the Taylor shift shiftC a b Q = Q(X + a, Y + b). Q has multiplicity at least r at (a, b) when every coefficient of the shifted polynomial of total degree less than r is zero. This is the Hasse-derivative criterion for root multiplicity over a field of any characteristic: the coefficient of Xⁱ Yʲ in shiftC a b Q is the order-(i, j) Hasse derivative of Q evaluated at (a, b). The zero polynomial has infinite multiplicity. As an aside, ordinary partial derivatives fail to capture this in positive characteristic. The integer factor introduced by differentiation can vanish, so its product with a nonzero coefficient may become zero.

shiftC_toPoly identifies the computable shift with Mathlib's Polynomial.Bivariate.shift, and hasMultiplicity_iff_rootMultiplicity proves that hasMultiplicity agrees with the reference Polynomial.Bivariate.rootMultiplicity.

source
def CompPoly.CBivariate.partialDerivX {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (f : CBivariate R) :
CBivariate R

Partial derivative with respect to X: differentiate each Y-coefficient in X.

Instances For
    source
    def CompPoly.CBivariate.partialDerivY {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (f : CBivariate R) :
    CBivariate R

    Partial derivative with respect to Y: differentiate in the outer variable.

    Instances For
      source
      theorem CompPoly.CBivariate.outerCoeff_support_monomial {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (f : CBivariate R) (g : CPolynomial R → CPolynomial R) (hg : g 0 = 0) (j : ℕ) :
      (∑ k ∈ CPolynomial.support f, CPolynomial.monomial k (g ((↑f).coeff k))).coeff j = g (CPolynomial.coeff f j)

      Outer coefficient of a support-sum of monomials whose Y-coefficients are mapped by a zero-preserving g: the j-th coefficient is g applied to the j-th Y-coefficient.

      source
      theorem CompPoly.CBivariate.outerCoeff_partialDerivX {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (f : CBivariate R) (j : ℕ) :
      CPolynomial.coeff f.partialDerivX j = (CPolynomial.coeff f j).derivative

      Outer coefficient of the X-partial derivative: differentiate the j-th Y-coefficient.

      source
      theorem CompPoly.CBivariate.coeff_partialDerivX {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (f : CBivariate R) (i j : ℕ) :
      f.partialDerivX.coeff i j = f.coeff (i + 1) j * ↑(i + 1)

      Coefficient formula for the X-partial derivative.

      source
      theorem CompPoly.CBivariate.coeff_partialDerivY {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (f : CBivariate R) (i j : ℕ) :
      f.partialDerivY.coeff i j = f.coeff i (j + 1) * ↑(j + 1)

      Coefficient formula for the Y-partial derivative.

      source
      theorem CompPoly.CBivariate.partialDerivX_zero {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] :
      partialDerivX 0 = 0

      The X-partial derivative of zero is zero.

      source
      theorem CompPoly.CBivariate.partialDerivY_zero {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] :
      partialDerivY 0 = 0

      The Y-partial derivative of zero is zero.

      source
      theorem CompPoly.CBivariate.partialDerivX_add {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (f g : CBivariate R) :
      (f + g).partialDerivX = f.partialDerivX + g.partialDerivX

      The X-partial derivative distributes over addition.

      source
      theorem CompPoly.CBivariate.partialDerivY_add {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (f g : CBivariate R) :
      (f + g).partialDerivY = f.partialDerivY + g.partialDerivY

      The Y-partial derivative distributes over addition.

      source
      theorem CompPoly.CBivariate.partialDerivX_toPoly {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (f : CBivariate R) (j : ℕ) :
      f.partialDerivX.toPoly.coeff j = Polynomial.derivative (f.toPoly.coeff j)

      The X-partial derivative differentiates each Y-coefficient under toPoly.

      source
      theorem CompPoly.CBivariate.partialDerivY_toPoly {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (f : CBivariate R) :
      f.partialDerivY.toPoly = Polynomial.derivative f.toPoly

      The Y-partial derivative corresponds to Polynomial.derivative under toPoly.

      source
      theorem CompPoly.CBivariate.partialDerivY_mul {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (f g : CBivariate R) :
      (f * g).partialDerivY = f.partialDerivY * g + f * g.partialDerivY

      The Y-partial derivative satisfies the Leibniz product rule.

      source
      theorem CompPoly.CBivariate.partialDerivX_mul {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (f g : CBivariate R) :
      (f * g).partialDerivX = f.partialDerivX * g + f * g.partialDerivX

      The X-partial derivative satisfies the Leibniz product rule.

      source
      def CompPoly.CBivariate.iterPartialDerivX {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (n : ℕ) (f : CBivariate R) :
      CBivariate R

      Iterated partial derivative with respect to X.

      Instances For
        source
        def CompPoly.CBivariate.iterPartialDerivY {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (n : ℕ) (f : CBivariate R) :
        CBivariate R

        Iterated partial derivative with respect to Y.

        Instances For
          source
          theorem CompPoly.CBivariate.iterPartialDerivX_toPoly {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (n : ℕ) (f : CBivariate R) (j : ℕ) :
          (iterPartialDerivX n f).toPoly.coeff j = (⇑Polynomial.derivative)^[n] (f.toPoly.coeff j)

          Iterated X-partial derivative differentiates each Y-coefficient under toPoly.

          source
          theorem CompPoly.CBivariate.iterPartialDerivY_toPoly {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (n : ℕ) (f : CBivariate R) :
          (iterPartialDerivY n f).toPoly = (⇑Polynomial.derivative)^[n] f.toPoly

          Iterated Y-partial derivative corresponds to Polynomial.derivative^[n] under toPoly.

          source
          def CompPoly.CBivariate.mixedPartialDeriv {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (i j : ℕ) (f : CBivariate R) :
          CBivariate R

          Mixed partial derivative: i-fold in X, then j-fold in Y.

          Instances For
            source
            theorem CompPoly.CBivariate.partialDerivX_partialDerivY_comm {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (f : CBivariate R) :
            f.partialDerivY.partialDerivX = f.partialDerivX.partialDerivY

            X and Y partial derivatives commute.

            source
            theorem CompPoly.CBivariate.mixedPartials_comm {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (i j : ℕ) (f : CBivariate R) :
            iterPartialDerivX i (iterPartialDerivY j f) = iterPartialDerivY j (iterPartialDerivX i f)

            Mixed partial derivatives commute.

            source
            def CompPoly.CBivariate.shiftY {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (b : R) (Q : CBivariate R) :
            CBivariate R

            Shift the outer Y variable: Q(X, Y + b).

            Instances For
              source
              def CompPoly.CBivariate.shiftX {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (a : R) (Q : CBivariate R) :
              CBivariate R

              Shift the inner X variable: Q(X + a, Y), Taylor-shifting each Y-coefficient.

              Instances For
                source
                def CompPoly.CBivariate.shiftC {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (a b : R) (Q : CBivariate R) :
                CBivariate R

                The full shift Q(X + a, Y + b).

                Instances For
                  source
                  def CompPoly.CBivariate.hasMultiplicity {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (Q : CBivariate R) (r : ℕ) (a b : R) :
                  Prop

                  Q has multiplicity at least r at (a, b): every coefficient of the shifted polynomial Q(X + a, Y + b) of total degree < r vanishes.

                  Instances For
                    source
                    def CompPoly.CBivariate.checkMultiplicity {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (Q : CBivariate R) (r : ℕ) (a b : R) :
                    Bool

                    Decidable check for multiplicity.

                    Instances For
                      source
                      theorem CompPoly.CBivariate.shiftY_toPoly {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (b : R) (Q : CBivariate R) :
                      (shiftY b Q).toPoly = Q.toPoly.comp (Polynomial.X + Polynomial.C (Polynomial.C b))

                      The outer (Y) shift corresponds to Y ↦ Y + b under toPoly.

                      source
                      theorem CompPoly.CBivariate.outerCoeff_shiftX {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (a : R) (P : CBivariate R) (j : ℕ) :
                      CPolynomial.coeff (shiftX a P) j = CPolynomial.taylor a (CPolynomial.coeff P j)

                      Outer coefficient of the X-shift: Taylor-shift the j-th Y-coefficient.

                      source
                      theorem CompPoly.CBivariate.shiftX_toPoly {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (a : R) (P : CBivariate R) :
                      (shiftX a P).toPoly = Polynomial.map (Polynomial.X + Polynomial.C a).compRingHom P.toPoly

                      The inner (X) shift corresponds to X ↦ X + a under toPoly.

                      source
                      theorem CompPoly.CBivariate.shiftC_toPoly {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (a b : R) (Q : CBivariate R) :
                      (shiftC a b Q).toPoly = Polynomial.Bivariate.shift Q.toPoly a b

                      The computable shift agrees with Polynomial.Bivariate.shift under toPoly.

                      source
                      theorem CompPoly.CBivariate.eval_C_eq_evalY {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (b : R) (Q : CBivariate R) :
                      CPolynomial.eval (CPolynomial.C b) Q = evalY b Q

                      Evaluating the outer variable at the constant C b agrees with the Horner evaluator evalY.

                      source
                      theorem CompPoly.CBivariate.coeff_shiftC_zero_zero {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (a b : R) (Q : CBivariate R) :
                      (shiftC a b Q).coeff 0 0 = evalEval a b Q

                      The (0,0) coefficient of the shift is evaluation at the point.

                      source
                      theorem CompPoly.CBivariate.hasMultiplicity_one_iff {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (Q : CBivariate R) (a b : R) :
                      Q.hasMultiplicity 1 a b ↔ evalEval a b Q = 0

                      Multiplicity at least 1 is equivalent to vanishing at the point.

                      source
                      theorem CompPoly.CBivariate.hasMultiplicity_iff_rootMultiplicity {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (Q : CBivariate R) (r : ℕ) (a b : R) :
                      Q.hasMultiplicity r a b ↔ ∀ m ∈ Polynomial.Bivariate.rootMultiplicity Q.toPoly a b, r ≤ m

                      hasMultiplicity agrees with the reference Polynomial.Bivariate.rootMultiplicity, where none denotes infinite multiplicity (the zero polynomial).

                      source
                      theorem CompPoly.CBivariate.hasMultiplicity_zero {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (Q : CBivariate R) (a b : R) :
                      Q.hasMultiplicity 0 a b

                      Every polynomial has multiplicity at least 0 at any point.

                      source
                      theorem CompPoly.CBivariate.hasMultiplicity_succ {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (Q : CBivariate R) (r : ℕ) (a b : R) :
                      Q.hasMultiplicity (r + 1) a b → Q.hasMultiplicity r a b

                      Multiplicity is monotone: higher multiplicity implies lower.

                      source
                      theorem CompPoly.CBivariate.toPoly_injective {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] {P Q : CBivariate R} (h : P.toPoly = Q.toPoly) :
                      P = Q

                      toPoly is injective on canonical bivariate polynomials.

                      source
                      theorem CompPoly.CBivariate.shiftC_add {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (a b : R) (P Q : CBivariate R) :
                      shiftC a b (P + Q) = shiftC a b P + shiftC a b Q

                      The generic Taylor shift is additive.

                      source
                      theorem CompPoly.CBivariate.shiftC_mul {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (a b : R) (P Q : CBivariate R) :
                      shiftC a b (P * Q) = shiftC a b P * shiftC a b Q

                      The generic Taylor shift is multiplicative.

                      source
                      theorem CompPoly.CBivariate.hasMultiplicity_iff_check {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (Q : CBivariate R) (r : ℕ) (a b : R) :
                      Q.hasMultiplicity r a b ↔ Q.checkMultiplicity r a b = true

                      The decidable check agrees with the propositional multiplicity.