Linear Algebra API for Computable Univariate Polynomials

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

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.

Equations

• CompPoly.CPolynomial.lcoeff n = { toFun := fun (p : CompPoly.CPolynomial R) => p.coeff n, map_add' := ⋯, map_smul' := ⋯ }

@[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.

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.

Equations

• CompPoly.CPolynomial.degreeLE n = {p : CompPoly.CPolynomial R | (↑p).degreeBound ≤ n}

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.

Equations

• CompPoly.CPolynomial.degreeLT n = {p : CompPoly.CPolynomial R | (↑p).degreeBound < ↑n}

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.

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.

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.

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.

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.

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.

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.

@[instance_reducible]

instance CompPoly.CPolynomial.instZeroElemDegreeLT {R : Type u_1} [Semiring R] (n : ℕ) : Zero ↑(degreeLT n)

Equations

• CompPoly.CPolynomial.instZeroElemDegreeLT n = { zero := ⟨0, ⋯⟩ }

@[instance_reducible]

instance CompPoly.CPolynomial.instAddElemDegreeLT {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (n : ℕ) : Add ↑(degreeLT n)

Equations

• CompPoly.CPolynomial.instAddElemDegreeLT n = { add := fun (p q : ↑(CompPoly.CPolynomial.degreeLT n)) => ⟨↑p + ↑q, ⋯⟩ }

@[instance_reducible]

instance CompPoly.CPolynomial.instSMulNatElemDegreeLT {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (n : ℕ) : SMul ℕ ↑(degreeLT n)

Equations

• CompPoly.CPolynomial.instSMulNatElemDegreeLT n = { smul := fun (m : ℕ) (p : ↑(CompPoly.CPolynomial.degreeLT n)) => ⟨m • ↑p, ⋯⟩ }

@[instance_reducible]

instance CompPoly.CPolynomial.instSMulElemDegreeLT {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (n : ℕ) : SMul R ↑(degreeLT n)

Equations

• CompPoly.CPolynomial.instSMulElemDegreeLT n = { smul := fun (r : R) (p : ↑(CompPoly.CPolynomial.degreeLT n)) => ⟨r • ↑p, ⋯⟩ }

@[instance_reducible]

instance CompPoly.CPolynomial.instAddCommMonoidElemDegreeLT {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (n : ℕ) : AddCommMonoid ↑(degreeLT n)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance CompPoly.CPolynomial.instModuleElemDegreeLT {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (n : ℕ) : Module R ↑(degreeLT n)

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• CompPoly.CPolynomial.degreeLTCoeffs n = { toFun := fun (p : ↑(CompPoly.CPolynomial.degreeLT n)) (i : Fin n) => (↑p).coeff ↑i, map_add' := ⋯, map_smul' := ⋯ }

@[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.