Documentation

CompPoly.Univariate.Linear

Linear Algebra API for Computable Univariate Polynomials #

This file contains linear maps and instance-stable bounded-degree predicates for CPolynomial.

source
def CompPoly.CPolynomial.lcoeff {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (n : ℕ) :
CPolynomial R →ₗ[R] R

This is an R-linear function that returns the coefficient of X^n.

Instances For
    source
    @[simp]
    theorem CompPoly.CPolynomial.lcoeff_apply {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (n : ℕ) (p : CPolynomial R) :
    (lcoeff n) p = p.coeff n

    Applying lcoeff n returns the coefficient of degree n.

    source
    def CompPoly.CPolynomial.degreeLE {R : Type u_1} [Zero R] (n : WithBot ℕ) :
    Set (CPolynomial R)

    The set of CPolynomial R consisting of polynomials of degree ≤ n.

    Instances For
      source
      def CompPoly.CPolynomial.degreeLT {R : Type u_1} [Zero R] (n : ℕ) :
      Set (CPolynomial R)

      The set of CPolynomial R consisting of polynomials of degree < n.

      Instances For
        source
        theorem CompPoly.CPolynomial.mem_degreeLE {R : Type u_1} [Zero R] {n : WithBot ℕ} {p : CPolynomial R} :
        p ∈ degreeLE n ↔ p.degree ≤ n

        Membership in degreeLE is the corresponding degree bound.

        source
        theorem CompPoly.CPolynomial.mem_degreeLT {R : Type u_1} [Zero R] {n : ℕ} {p : CPolynomial R} :
        p ∈ degreeLT n ↔ p.degree < ↑n

        Membership in degreeLT is the corresponding strict degree bound.

        source
        theorem CompPoly.CPolynomial.mem_degreeLT_iff_size_le {R : Type u_1} [Zero R] {n : ℕ} {p : CPolynomial R} :
        p ∈ degreeLT n ↔ Array.size ↑p ≤ n

        degreeLT n is exactly the bounded-size carrier storing at most n coefficients.

        source
        theorem CompPoly.CPolynomial.zero_mem_degreeLT {R : Type u_1} [Zero R] (n : ℕ) :
        0 ∈ degreeLT n

        The zero polynomial has bounded degree for every cutoff.

        source
        theorem CompPoly.CPolynomial.add_mem_degreeLT {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] {n : ℕ} {p q : CPolynomial R} (hp : p ∈ degreeLT n) (hq : q ∈ degreeLT n) :
        p + q ∈ degreeLT n

        degreeLT n is closed under addition.

        source
        theorem CompPoly.CPolynomial.nsmul_mem_degreeLT {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] {n m : ℕ} {p : CPolynomial R} (hp : p ∈ degreeLT n) :
        m • p ∈ degreeLT n

        degreeLT n is closed under additive scalar multiplication.

        source
        theorem CompPoly.CPolynomial.smul_mem_degreeLT {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] {n : ℕ} (r : R) {p : CPolynomial R} (hp : p ∈ degreeLT n) :
        r • p ∈ degreeLT n

        degreeLT n is closed under semiring scalar multiplication.

        source
        @[instance_reducible]
        instance CompPoly.CPolynomial.instZeroElemDegreeLT {R : Type u_1} [Semiring R] (n : ℕ) :
        Zero ↑(degreeLT n)
        source
        @[instance_reducible]
        instance CompPoly.CPolynomial.instAddElemDegreeLT {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (n : ℕ) :
        Add ↑(degreeLT n)
        source
        @[instance_reducible]
        instance CompPoly.CPolynomial.instSMulNatElemDegreeLT {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (n : ℕ) :
        SMul ℕ ↑(degreeLT n)
        source
        @[instance_reducible]
        instance CompPoly.CPolynomial.instSMulElemDegreeLT {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (n : ℕ) :
        SMul R ↑(degreeLT n)
        source
        @[instance_reducible]
        instance CompPoly.CPolynomial.instAddCommMonoidElemDegreeLT {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (n : ℕ) :
        AddCommMonoid ↑(degreeLT n)
        source
        @[instance_reducible]
        instance CompPoly.CPolynomial.instModuleElemDegreeLT {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (n : ℕ) :
        Module R ↑(degreeLT n)
        source
        def CompPoly.CPolynomial.degreeLTCoeffs {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (n : ℕ) :
        ↑(degreeLT n) →ₗ[R] Fin n → R

        The first n coefficients on degreeLT n form a computable linear map to Fin n → R.

        Instances For
          source
          @[simp]
          theorem CompPoly.CPolynomial.degreeLTCoeffs_apply {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (n : ℕ) (p : ↑(degreeLT n)) (i : Fin n) :
          (degreeLTCoeffs n) p i = (↑p).coeff ↑i

          Applying degreeLTCoeffs returns the corresponding bounded coefficient.