Documentation

CompPoly.Bivariate.ToPoly

Equivalence with Mathlib Bivariate Polynomials #

This file establishes the conversion from CBivariate R to Mathlib's R[X][Y] (Polynomial (Polynomial R)).

Main definitions:

Main results:

Core conversion lemmas between CBivariate R and R[X][Y].

source
noncomputable def CompPoly.CBivariate.toPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Semiring R] (p : CBivariate R) :
Polynomial (Polynomial R)

Convert CBivariate R to Mathlib's bivariate polynomial R[X][Y].

Maps each Y-coefficient through CPolynomial.toPoly, then builds Polynomial (Polynomial R) as the sum of monomials.

Instances For
    source
    def CompPoly.CBivariate.ofPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] [Semiring (Polynomial R)] (p : Polynomial (Polynomial R)) :
    CBivariate R

    Convert Mathlib's R[X][Y] to CBivariate R (inverse of toPoly).

    Extracts each Y-coefficient via p.coeff, converts to CPolynomial R via toImpl and trimming, then builds the canonical bivariate sum.

    Instances For
      source
      theorem CompPoly.CBivariate.toPoly_add {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (p q : CBivariate R) :
      (p + q).toPoly = p.toPoly + q.toPoly

      toPoly preserves addition.

      source
      theorem CompPoly.CBivariate.toPoly_monomial {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (n : ℕ) (c : CPolynomial R) :
      toPoly (CPolynomial.monomial n c) = (Polynomial.monomial n) c.toPoly

      toPoly sends a Y-monomial to the corresponding monomial in R[X][Y].

      source
      theorem CompPoly.CBivariate.ofPoly_monomial {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (n : ℕ) (c : Polynomial R) :
      ofPoly ((Polynomial.monomial n) c) = CPolynomial.monomial n ⟨c.toImpl, ⋯⟩

      ofPoly sends a Y-monomial in R[X][Y] to a bivariate monomial.

      source
      theorem CompPoly.CBivariate.toImpl_add {R : Type u_1} [BEq R] [LawfulBEq R] [Semiring R] (p q : Polynomial R) :
      p.toImpl + q.toImpl = (p + q).toImpl

      Polynomial.toImpl preserves addition, accounting for trimming in the raw representation.

      source
      theorem CompPoly.CBivariate.ofPoly_add {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (p q : Polynomial (Polynomial R)) :
      ofPoly (p + q) = ofPoly p + ofPoly q

      ofPoly preserves addition in R[X][Y].

      source
      theorem CompPoly.CBivariate.ofPoly_coeff {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (p : Polynomial (Polynomial R)) (n : ℕ) :
      (CPolynomial.coeff (ofPoly p) n).toPoly = p.coeff n

      The outer coefficient of ofPoly p converts back to the corresponding R[X] coefficient.

      source
      theorem CompPoly.CBivariate.toPoly_coeff {R : Type u_1} [BEq R] [LawfulBEq R] [Semiring R] (p : CBivariate R) (n : ℕ) :
      p.toPoly.coeff n = (CPolynomial.coeff p n).toPoly

      The outer coefficient of toPoly p is CPolynomial.coeff p n converted to R[X].

      source
      theorem CompPoly.CBivariate.toPoly_eq_map {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (p : CBivariate R) :
      p.toPoly = Polynomial.map (↑CPolynomial.ringEquiv) (CPolynomial.toPoly p)

      toPoly is the map of the outer polynomial via CPolynomial.ringEquiv.

      source
      theorem CompPoly.CBivariate.toPoly_mul {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (p q : CBivariate R) :
      (p * q).toPoly = p.toPoly * q.toPoly

      toPoly preserves multiplication.

      Ring equivalence between bivariate representations.

      source
      theorem CompPoly.CBivariate.ofPoly_toPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (p : Polynomial (Polynomial R)) :
      (ofPoly p).toPoly = p

      Round-trip from Mathlib: converting a polynomial to CBivariate and back is the identity.

      source
      theorem CompPoly.CBivariate.toPoly_ofPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (p : CBivariate R) :
      ofPoly p.toPoly = p

      Round-trip from CBivariate: converting to Mathlib and back is the identity.

      source
      noncomputable def CompPoly.CBivariate.ringEquiv {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] :
      CBivariate R ≃+* Polynomial (Polynomial R)

      Ring equivalence between CBivariate R and Mathlib's R[X][Y].

      Instances For
        source
        theorem CompPoly.CBivariate.toPoly_one {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] :
        toPoly 1 = 1

        toPoly preserves 1.

        source
        theorem CompPoly.CBivariate.ofPoly_one {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] :
        ofPoly 1 = 1

        ofPoly preserves 1.

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

        toPoly maps the zero bivariate polynomial to 0.

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

        ofPoly maps 0 in R[X][Y] to the zero bivariate polynomial.

        source
        noncomputable def CompPoly.CBivariate.toPolyRingHom {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] :
        CBivariate R →+* Polynomial (Polynomial R)

        Ring hom from computable bivariates to Mathlib bivariates.

        Instances For
          source
          noncomputable def CompPoly.CBivariate.ofPolyRingHom {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] :
          Polynomial (Polynomial R) →+* CBivariate R

          Ring hom from Mathlib bivariates to computable bivariates.

          Instances For
            source
            theorem CompPoly.CBivariate.ofPoly_mul {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (p q : Polynomial (Polynomial R)) :
            ofPoly (p * q) = ofPoly p * ofPoly q

            ofPoly preserves multiplication.

            Shared helper: deferred-trim Horner foldr commutes with toPoly #

            evalY and (transitively) evalEval fold the Y-coefficients of f : CBivariate R with a raw Horner pattern (smulRight a then addRaw) and trim once at the end. The helper below bridges that raw fold's toPoly image with the Finset.sum form of the polynomial evaluation.

            Correctness lemmas for evaluation, coefficients, support, and degrees.

            source
            theorem CompPoly.CBivariate.evalY_toPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (a : R) (f : CBivariate R) :
            (evalY a f).toPoly = Polynomial.eval (Polynomial.C a) f.toPoly

            evalY a corresponds to outer evaluation at Polynomial.C a.

            source
            theorem CompPoly.CBivariate.eval_y_horner_eq_eval_y {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (a : R) (p : CBivariate R) :
            evalYHorner a p = evalY a p

            Horner evaluation in Y agrees with the deferred-trim sum-of-powers evaluator.

            Both evalYHorner and the new evalY reduce to the same Polynomial under toPoly, and toPoly is injective on canonical polynomials, so the two canonical results coincide.

            source
            theorem CompPoly.CBivariate.eval_eval_horner_y_then_x_eq_eval_eval {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (x y : R) (p : CBivariate R) :
            evalEvalHornerYThenX x y p = evalEval x y p

            Y-then-X Horner full evaluation agrees with the existing evaluator.

            source
            theorem CompPoly.CBivariate.evalEval_toPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (x y : R) (f : CBivariate R) :
            evalEval x y f = Polynomial.evalEval x y f.toPoly

            toPoly preserves full evaluation: evalEval x y f = (toPoly f).evalEval x y.

            source
            theorem CompPoly.CBivariate.coeff_toPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (f : CBivariate R) (i j : ℕ) :
            (f.toPoly.coeff j).coeff i = f.coeff i j

            toPoly preserves coefficients: coefficient of X^i Y^j matches.

            source
            theorem CompPoly.CBivariate.support_toPoly_outer {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (f : CBivariate R) :
            f.toPoly.support = f.supportY

            The outer support of toPoly f equals the Y-support of f.

            source
            theorem CompPoly.CBivariate.natDegreeY_toPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (f : CBivariate R) :
            f.toPoly.natDegree = f.natDegreeY

            toPoly preserves Y-degree.

            source
            theorem CompPoly.CBivariate.coeff_toPoly_Y {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (f : CBivariate R) (j : ℕ) :
            f.toPoly.coeff j = ((↑f).coeff j).toPoly

            The outer Y-coefficient formula used for X-degree transport.

            source
            theorem CompPoly.CBivariate.natDegreeX_toPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (f : CBivariate R) :
            (f.toPoly.support.sup fun (j : ℕ) => (f.toPoly.coeff j).natDegree) = f.natDegreeX

            toPoly preserves X-degree (max over Y-coefficients of their degree in X).

            source
            theorem CompPoly.CBivariate.CC_toPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (r : R) :
            (CC r).toPoly = Polynomial.C (Polynomial.C r)

            CC corresponds to the nested constant polynomial in R[X][Y].

            source
            theorem CompPoly.CBivariate.X_toPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] :
            X.toPoly = Polynomial.C Polynomial.X

            X (inner variable) corresponds to Polynomial.C Polynomial.X in R[X][Y].

            source
            theorem CompPoly.CBivariate.Y_toPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] :
            Y.toPoly = Polynomial.X

            Y (outer variable) corresponds to Polynomial.X in R[X][Y].

            source
            theorem CompPoly.CBivariate.monomialXY_toPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (n m : ℕ) (c : R) :
            (monomialXY n m c).toPoly = (Polynomial.monomial m) ((Polynomial.monomial n) c)

            monomialXY n m c corresponds to Y^m with inner coefficient X^n * c.

            source
            theorem CompPoly.CBivariate.supportX_toPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (f : CBivariate R) :
            f.supportX = f.toPoly.support.biUnion fun (j : ℕ) => (f.toPoly.coeff j).support

            supportX corresponds to the union of inner supports of outer coefficients.

            source
            theorem CompPoly.CBivariate.totalDegree_toPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (f : CBivariate R) :
            f.totalDegree = f.toPoly.support.sup fun (j : ℕ) => (f.toPoly.coeff j).natDegree + j

            totalDegree corresponds to the supremum over j of natDegree ((toPoly f).coeff j) + j.

            source
            theorem CompPoly.CBivariate.evalX_toPoly_coeff {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (a : R) (f : CBivariate R) (j : ℕ) :
            (evalX a f).toPoly.coeff j = Polynomial.eval a (f.toPoly.coeff j)

            evalX a evaluates each inner coefficient at a.

            source
            theorem CompPoly.CBivariate.evalX_toPoly_eval_commute {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (a y : R) (hc : Commute a y) (f : CBivariate R) :
            CPolynomial.eval y (evalX a f) = Polynomial.evalEval a y f.toPoly

            evalX is compatible with full bivariate evaluation when a and y commute.

            source
            theorem CompPoly.CBivariate.evalX_toPoly_eval {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [CommSemiring R] [DecidableEq R] (a y : R) (f : CBivariate R) :
            CPolynomial.eval y (evalX a f) = Polynomial.evalEval a y f.toPoly

            evalX_toPoly_eval_commute specialized to commutative rings.

            source
            theorem CompPoly.CBivariate.eval_eval_horner_x_then_y_eq_eval_eval {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [CommSemiring R] [DecidableEq R] (x y : R) (p : CBivariate R) :
            evalEvalHornerXThenY x y p = evalEval x y p

            X-then-Y Horner full evaluation agrees with the existing evaluator over commutative coefficient semirings.

            source
            theorem CompPoly.CBivariate.evalX_toPoly_eval_commute_converse {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (a y : R) (h : ∀ (f : CBivariate R), CPolynomial.eval y (evalX a f) = Polynomial.evalEval a y f.toPoly) :
            Commute a y

            The Commute hypothesis in evalX_toPoly_eval_commute is necessary: if the identity holds for every bivariate polynomial then a and y commute.

            source
            theorem CompPoly.CBivariate.eval_comm {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [CommSemiring R] [DecidableEq R] (a x : R) (f : CBivariate R) :
            CPolynomial.eval x (evalY a f) = CPolynomial.eval a (evalX x f)

            Computable analogue of Polynomial.Bivariate.eval_comm: evaluating Y at a and then X at x agrees with first applying the X = x evaluation through the inner coefficients and then evaluating Y at a.

            source
            theorem CompPoly.CBivariate.leadingCoeffY_toPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (f : CBivariate R) :
            f.leadingCoeffY.toPoly = f.toPoly.leadingCoeff

            leadingCoeffY corresponds to the leading coefficient in the outer variable.

            source
            theorem CompPoly.CBivariate.swap_toPoly_coeff {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (f : CBivariate R) (i j : ℕ) :
            (f.swap.toPoly.coeff j).coeff i = (f.toPoly.coeff i).coeff j

            swap exchanges X- and Y-exponents.

            source
            theorem CompPoly.CBivariate.leadingCoeffX_toPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (f : CBivariate R) :
            f.leadingCoeffX.toPoly = f.swap.toPoly.leadingCoeff

            leadingCoeffX is the Y-leading coefficient of the swapped polynomial.