The derivative of Laurent polynomials

Over a ring R, the formal derivative d/dT of Laurent polynomials sends a Tⁿ to n a Tⁿ⁻¹ for every integer n, so the coefficient of Tⁿ in f' is n + 1 times the coefficient of Tⁿ⁺¹ in f. It satisfies the product rule, extends Polynomial.derivative along Polynomial.toLaurent, and kills the constants; without additive torsion its kernel is exactly the constants. For commutative R it is bundled as a derivation LaurentPolynomial.derivative', following Polynomial.derivative'.

The residue of the form f dT is the coefficient of T⁻¹ in f. Since n Tⁿ⁻¹ has residue zero for every n, every derivative has residue zero, and the product rule gives integration by parts Res(f dg) = -Res((df) g). These are the Laurent-polynomial counterparts of the derivative and residue of Laurent series: the embedding of Laurent polynomials into Laurent series commutes with the derivatives (LaurentPolynomial.toLaurentSeries_derivative) and carries the residue Res(f dg) of Laurent polynomials to the Laurent-series residue pairing (LaurentSeries.residuePairing_toLaurentSeries).

Main definitions

• LaurentPolynomial.derivative: the formal derivative of Laurent polynomials.
• LaurentPolynomial.derivative': the formal derivative as a derivation, for commutative R.

Main results

• LaurentPolynomial.derivative_C_mul_T: the derivative of a Tⁿ is n a Tⁿ⁻¹.
• LaurentPolynomial.coeff_derivative: the coefficient formula for the derivative.
• LaurentPolynomial.derivative_mul: the product rule.
• LaurentPolynomial.derivative_toLaurent: compatibility with Polynomial.derivative.
• LaurentPolynomial.derivative_eq_zero_iff_exists_C: without additive torsion, the kernel of the derivative consists of the constants.
• LaurentPolynomial.coeff_neg_one_derivative: a derivative has residue zero.
• LaurentPolynomial.coeff_neg_one_mul_derivative: integration by parts for residues.

noncomputable def LaurentPolynomial.derivative {R : Type u_1} [Ring R] : LaurentPolynomial R →ₗ[R] LaurentPolynomial R

The formal derivative d/dT of Laurent polynomials, sending a Tⁿ to n a Tⁿ⁻¹ for every integer n.

theorem LaurentPolynomial.derivative_single {R : Type u_1} [Ring R] (n : ℤ) (a : R) : derivative (AddMonoidAlgebra.single n a) = AddMonoidAlgebra.single (n - 1) (a * ↑n)

The derivative of the monomial a Tⁿ, written with AddMonoidAlgebra.single. The simp normal form of a Laurent monomial is C a * T n, handled by LaurentPolynomial.derivative_C_mul_T.

@[simp]

theorem LaurentPolynomial.derivative_C_mul_T {R : Type u_1} [Ring R] (a : R) (n : ℤ) : derivative (C a * T n) = C (a * ↑n) * T (n - 1)

The derivative of a Tⁿ is n a Tⁿ⁻¹, for every integer n.

@[simp]

theorem LaurentPolynomial.derivative_T {R : Type u_1} [Ring R] (n : ℤ) : derivative (T n) = ↑n * T (n - 1)

The derivative of Tⁿ is n Tⁿ⁻¹, for every integer n.

@[simp]

theorem LaurentPolynomial.derivative_C {R : Type u_1} [Ring R] (a : R) : derivative (C a) = 0

The derivative of a constant is zero.

@[simp]

theorem LaurentPolynomial.derivative_one {R : Type u_1} [Ring R] : derivative 1 = 0

The derivative of 1 is zero.

@[simp]

theorem LaurentPolynomial.coeff_derivative {R : Type u_1} [Ring R] (f : LaurentPolynomial R) (n : ℤ) : (derivative f).coeff n = f.coeff (n + 1) * (↑n + 1)

The coefficient of Tⁿ in f' is n + 1 times the coefficient of Tⁿ⁺¹ in f.

theorem LaurentPolynomial.coeff_derivative_sub_one {R : Type u_1} [Ring R] (f : LaurentPolynomial R) (n : ℤ) : (derivative f).coeff (n - 1) = f.coeff n * ↑n

The coefficient of Tⁿ⁻¹ in f' is n times the coefficient of Tⁿ in f.

theorem LaurentPolynomial.coeff_neg_one_derivative {R : Type u_1} [Ring R] (f : LaurentPolynomial R) : (derivative f).coeff (-1) = 0

A derivative has residue zero: the coefficient of T⁻¹ in f' vanishes.

theorem LaurentPolynomial.derivative_mul {R : Type u_1} [Ring R] (f g : LaurentPolynomial R) : derivative (f * g) = derivative f * g + f * derivative g

The product rule for the derivative of Laurent polynomials.

@[simp]

theorem LaurentPolynomial.derivative_toLaurent {R : Type u_1} [Ring R] (p : Polynomial R) : derivative (Polynomial.toLaurent p) = Polynomial.toLaurent (Polynomial.derivative p)

The derivative of Laurent polynomials extends the derivative of polynomials along Polynomial.toLaurent.

theorem LaurentPolynomial.derivative_eq_zero_iff_exists_C {R : Type u_1} [Ring R] [IsAddTorsionFree R] {f : LaurentPolynomial R} : derivative f = 0 ↔ ∃ (c : R), C c = f

The kernel of the derivative. Without additive torsion in R, a Laurent polynomial has derivative zero exactly when it is a constant.

theorem LaurentPolynomial.coeff_neg_one_mul_derivative {R : Type u_1} [Ring R] (f g : LaurentPolynomial R) : (f * derivative g).coeff (-1) = -(derivative f * g).coeff (-1)

Integration by parts for residues of Laurent polynomials: Res(f dg) = -Res((df) g), where the residue is the coefficient of T⁻¹. The factor order is kept, since R need not be commutative.

noncomputable def LaurentPolynomial.derivative' (R : Type u_1) [CommRing R] : Derivation R (LaurentPolynomial R) (LaurentPolynomial R)

The formal derivative of Laurent polynomials over a commutative ring, as a derivation.

@[simp]

theorem LaurentPolynomial.derivative'_apply {R : Type u_1} [CommRing R] (f : LaurentPolynomial R) : (derivative' R) f = derivative f

The derivation LaurentPolynomial.derivative' R evaluates as the formal derivative.