Scalar-multiple polynomial evaluation

This file defines polynomial evaluation via scalar multiplication. Our polynomials have coefficients in a semiring R, and we evaluate at a weak form of R-algebra, namely an additive commutative monoid with an action of R and a notion of natural number power. This is a generalization of Data.Polynomial.Eval.

Main definitions

• Polynomial.smeval: function for evaluating a polynomial with coefficients in a Semiring R at an element x of an AddCommMonoid S that has natural number powers and an R-action.
• smeval.linearMap: the smeval function as an R-linear map, when S is an R-module.
• smeval.algebraMap: the smeval function as an R-algebra map, when S is an R-algebra.

Main results

• smeval_monomial: monomials evaluate as we expect.
• smeval_add, smeval_smul: linearity of evaluation, given an R-module.
• smeval_mul, smeval_comp: multiplicativity of evaluation, given power-associativity.
• eval₂_eq_smeval, leval_eq_smeval.linearMap, aeval = smeval.algebraMap, etc.: comparisons

To do

• smeval_neg and smeval_int_cast for R a ring and S an AddCommGroup.
• Nonunital evaluation for polynomials with vanishing constant term for Pow S ℕ+ (different file?)

def Polynomial.smul_pow {R : Type u_1} [Semiring R] {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] [MulActionWithZero R S] (x : S) : ℕ → R → S

Scalar multiplication together with taking a natural number power.

Equations

• Polynomial.smul_pow x n r = r • x ^ n

@[irreducible]

def Polynomial.smeval {R : Type u_3} [Semiring R] (p : Polynomial R) {S : Type u_4} [AddCommMonoid S] [Pow S ℕ] [MulActionWithZero R S] (x : S) : S

Evaluate a polynomial p in the scalar semiring R at an element x in the target S using scalar multiple R-action.

Equations

• @Polynomial.smeval = Polynomial.wrapped✝.1

theorem Polynomial.smeval_def {R : Type u_3} [Semiring R] (p : Polynomial R) {S : Type u_4} [AddCommMonoid S] [Pow S ℕ] [MulActionWithZero R S] (x : S) : Polynomial.smeval p x = Polynomial.sum p (Polynomial.smul_pow x)

theorem Polynomial.smeval_eq_sum {R : Type u_1} [Semiring R] (p : Polynomial R) {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] [MulActionWithZero R S] (x : S) : Polynomial.smeval p x = Polynomial.sum p (Polynomial.smul_pow x)

@[simp]

theorem Polynomial.smeval_C {R : Type u_1} [Semiring R] (r : R) {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] [MulActionWithZero R S] (x : S) : Polynomial.smeval (Polynomial.C r) x = r • x ^ 0

@[simp]

theorem Polynomial.smeval_monomial {R : Type u_1} [Semiring R] (r : R) {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] [MulActionWithZero R S] (x : S) (n : ℕ) : Polynomial.smeval ((Polynomial.monomial n) r) x = r • x ^ n

theorem Polynomial.eval_eq_smeval {R : Type u_1} [Semiring R] (r : R) (p : Polynomial R) : Polynomial.eval r p = Polynomial.smeval p r

theorem Polynomial.eval₂_eq_smeval (R : Type u_3) [Semiring R] {S : Type u_4} [Semiring S] (f : R →+* S) (p : Polynomial R) (x : S) : Polynomial.eval₂ f x p = Polynomial.smeval p x

@[simp]

theorem Polynomial.smeval_zero (R : Type u_1) [Semiring R] {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] [MulActionWithZero R S] (x : S) : Polynomial.smeval 0 x = 0

@[simp]

theorem Polynomial.smeval_one (R : Type u_1) [Semiring R] {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] [MulActionWithZero R S] (x : S) : Polynomial.smeval 1 x = 1 • x ^ 0

@[simp]

theorem Polynomial.smeval_X (R : Type u_1) [Semiring R] {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] [MulActionWithZero R S] (x : S) : Polynomial.smeval Polynomial.X x = x ^ 1

@[simp]

theorem Polynomial.smeval_X_pow (R : Type u_1) [Semiring R] {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] [MulActionWithZero R S] (x : S) {n : ℕ} : Polynomial.smeval (Polynomial.X ^ n) x = x ^ n

@[simp]

theorem Polynomial.smeval_add (R : Type u_1) [Semiring R] (p : Polynomial R) (q : Polynomial R) {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] [Module R S] (x : S) : Polynomial.smeval (p + q) x = Polynomial.smeval p x + Polynomial.smeval q x

theorem Polynomial.smeval_nat_cast (R : Type u_1) [Semiring R] {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] [Module R S] (x : S) (n : ℕ) : Polynomial.smeval (↑n) x = n • x ^ 0

@[simp]

theorem Polynomial.smeval_smul (R : Type u_1) [Semiring R] (p : Polynomial R) {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] [Module R S] (x : S) (r : R) : Polynomial.smeval (r • p) x = r • Polynomial.smeval p x

def Polynomial.smeval.linearMap (R : Type u_1) [Semiring R] {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] [Module R S] (x : S) : Polynomial R →ₗ[R] S

Polynomial.smeval as a linear map.

Equations

• Polynomial.smeval.linearMap R x = { toAddHom := { toFun := fun (f : Polynomial R) => Polynomial.smeval f x, map_add' := ⋯ }, map_smul' := ⋯ }

@[simp]

theorem Polynomial.smeval.linearMap_apply (R : Type u_1) [Semiring R] (p : Polynomial R) {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] [Module R S] (x : S) : (Polynomial.smeval.linearMap R x) p = Polynomial.smeval p x

theorem Polynomial.leval_coe_eq_smeval {R : Type u_3} [Semiring R] (r : R) : ⇑(Polynomial.leval r) = fun (p : Polynomial R) => Polynomial.smeval p r

theorem Polynomial.leval_eq_smeval.linearMap {R : Type u_3} [Semiring R] (r : R) : Polynomial.leval r = Polynomial.smeval.linearMap R r

In the module docstring for algebras at Mathlib.Algebra.Algebra.Basic, we see that [CommSemiring R] [Semiring S] [Module R S] [IsScalarTower R S S] [SMulCommClass R S S] is an equivalent way to express [CommSemiring R] [Semiring S] [Algebra R S] that allows one to relax the defining structures independently. For non-associative power-associative algebras (e.g., octonions), we replace the [Semiring S] with [NonAssocSemiring S] [Pow S ℕ] [NatPowAssoc S].

theorem Polynomial.smeval_at_nat_cast {S : Type u_2} [NonAssocSemiring S] [Pow S ℕ] [NatPowAssoc S] (q : Polynomial ℕ) (n : ℕ) : Polynomial.smeval q ↑n = ↑(Polynomial.smeval q n)

theorem Polynomial.smeval_at_zero (R : Type u_1) [CommSemiring R] (p : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [Pow S ℕ] [NatPowAssoc S] : Polynomial.smeval p 0 = Polynomial.coeff p 0 • 1

theorem Polynomial.smeval_mul_X (R : Type u_1) [CommSemiring R] (p : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [IsScalarTower R S S] [Pow S ℕ] [NatPowAssoc S] (x : S) : Polynomial.smeval (p * Polynomial.X) x = Polynomial.smeval p x * x

theorem Polynomial.smeval_X_mul (R : Type u_1) [CommSemiring R] (p : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [SMulCommClass R S S] [Pow S ℕ] [NatPowAssoc S] (x : S) : Polynomial.smeval (Polynomial.X * p) x = x * Polynomial.smeval p x

theorem Polynomial.smeval_assoc_X_pow (R : Type u_1) [CommSemiring R] (p : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [IsScalarTower R S S] [Pow S ℕ] [NatPowAssoc S] (x : S) (m : ℕ) (n : ℕ) : Polynomial.smeval p x * x ^ m * x ^ n = Polynomial.smeval p x * (x ^ m * x ^ n)

theorem Polynomial.smeval_mul_X_pow (R : Type u_1) [CommSemiring R] (p : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [IsScalarTower R S S] [Pow S ℕ] [NatPowAssoc S] (x : S) (n : ℕ) : Polynomial.smeval (p * Polynomial.X ^ n) x = Polynomial.smeval p x * x ^ n

theorem Polynomial.smeval_X_pow_assoc (R : Type u_1) [CommSemiring R] (p : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [SMulCommClass R S S] [Pow S ℕ] [NatPowAssoc S] (x : S) (m : ℕ) (n : ℕ) : x ^ m * x ^ n * Polynomial.smeval p x = x ^ m * (x ^ n * Polynomial.smeval p x)

theorem Polynomial.smeval_X_pow_mul (R : Type u_1) [CommSemiring R] (p : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [SMulCommClass R S S] [Pow S ℕ] [NatPowAssoc S] (x : S) (n : ℕ) : Polynomial.smeval (Polynomial.X ^ n * p) x = x ^ n * Polynomial.smeval p x

theorem Polynomial.smeval_C_mul (R : Type u_1) [CommSemiring R] (r : R) (p : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [Pow S ℕ] (x : S) : Polynomial.smeval (Polynomial.C r * p) x = r • Polynomial.smeval p x

theorem Polynomial.smeval_monomial_mul (R : Type u_1) [CommSemiring R] (r : R) (p : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [SMulCommClass R S S] [Pow S ℕ] [NatPowAssoc S] (x : S) (n : ℕ) : Polynomial.smeval ((Polynomial.monomial n) r * p) x = r • (x ^ n * Polynomial.smeval p x)

theorem Polynomial.smeval_mul (R : Type u_1) [CommSemiring R] (p : Polynomial R) (q : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [IsScalarTower R S S] [SMulCommClass R S S] [Pow S ℕ] [NatPowAssoc S] (x : S) : Polynomial.smeval (p * q) x = Polynomial.smeval p x * Polynomial.smeval q x

theorem Polynomial.smeval_pow (R : Type u_1) [CommSemiring R] (p : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [IsScalarTower R S S] [SMulCommClass R S S] [Pow S ℕ] [NatPowAssoc S] (x : S) (n : ℕ) : Polynomial.smeval (p ^ n) x = Polynomial.smeval p x ^ n

theorem Polynomial.smeval_comp (R : Type u_1) [CommSemiring R] (p : Polynomial R) (q : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [IsScalarTower R S S] [SMulCommClass R S S] [Pow S ℕ] [NatPowAssoc S] (x : S) : Polynomial.smeval (Polynomial.comp p q) x = Polynomial.smeval p (Polynomial.smeval q x)

theorem Polynomial.aeval_eq_smeval {R : Type u_1} [CommSemiring R] {S : Type u_2} [Semiring S] [Algebra R S] (x : S) (p : Polynomial R) : (Polynomial.aeval x) p = Polynomial.smeval p x

theorem Polynomial.aeval_coe_eq_smeval {R : Type u_1} [CommSemiring R] {S : Type u_2} [Semiring S] [Algebra R S] (x : S) : ⇑(Polynomial.aeval x) = fun (p : Polynomial R) => Polynomial.smeval p x