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 Algebra.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_intCast 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) : p.smeval x = p.sum (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) : p.smeval x = p.sum (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.C r).smeval 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.monomial n) r).smeval x = r • x ^ n

theorem Polynomial.eval_eq_smeval {R : Type u_1} [Semiring R] (r : R) (p : Polynomial R) : Polynomial.eval r p = p.smeval 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 = p.smeval 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.X.smeval 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.X ^ n).smeval 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) : (p + q).smeval x = p.smeval x + q.smeval x

theorem Polynomial.smeval_natCast (R : Type u_1) [Semiring R] {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] [Module R S] (x : S) (n : ℕ) : (↑n).smeval 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) : (r • p).smeval x = r • p.smeval 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 = { toFun := fun (f : Polynomial R) => f.smeval 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 = p.smeval x

theorem Polynomial.leval_coe_eq_smeval {R : Type u_3} [Semiring R] (r : R) : ⇑(Polynomial.leval r) = fun (p : Polynomial R) => p.smeval 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_natCast {S : Type u_2} [NonAssocSemiring S] [Pow S ℕ] [NatPowAssoc S] (q : Polynomial ℕ) (n : ℕ) : q.smeval ↑n = ↑(q.smeval 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] : p.smeval 0 = p.coeff 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) : (p * Polynomial.X).smeval x = p.smeval 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.X * p).smeval x = x * p.smeval 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 : ℕ) : p.smeval x * x ^ m * x ^ n = p.smeval 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 : ℕ) : (p * Polynomial.X ^ n).smeval x = p.smeval 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 * p.smeval x = x ^ m * (x ^ n * p.smeval 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.X ^ n * p).smeval x = x ^ n * p.smeval 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.C r * p).smeval x = r • p.smeval 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.monomial n) r * p).smeval x = r • (x ^ n * p.smeval 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) : (p * q).smeval x = p.smeval x * q.smeval 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 : ℕ) : (p ^ n).smeval x = p.smeval 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) : (p.comp q).smeval x = p.smeval (q.smeval 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 = p.smeval 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) => p.smeval x