The ascending Pochhammer polynomial transform

This file defines the linear transformation on univariate polynomials that sends the standard monomial X ^ n to the ascending Pochhammer polynomial ascPochhammer R n that is $X (X+1) \cdots (X+n-1)$. The inverse transformation is also defined and some identities are proven.

Mathematical preliminaries

The transformation is expressed using Stirling numbers, for which different notations are in use. Here the Stirling numbers are taken as stirlingFirst and stirlingSecond from Mathlib.Combinatorics.Enumerative.Stirling.

In the NIST Handbook [DLMF], Section 26.8, the Stirling numbers are defined using the notation s and S. The concordance is given by $s(n,k)=(−1)^{n−k}{stirlingFirst}(n,k)$ and $S(n,k)={stirlingSecond}(n,k)$. The Mathlib functions {stirlingFirst} and {stirlingSecond} are nonnegative and are called the unsigned Stirling numbers of the first and second kind. The s of [DLMF] is called the signed Stirling number of the first kind.

DLMF 26.8.7 gives the expansion in terms of the signed Stirling numbers of the first kind: $$ \sum_{k=0}^{n} s(n,k) x^k = (x-n+1)_n . $$

DLMF 26.8.10 gives the inverse expansion in terms of the Stirling numbers of the second kind: $$ \sum_{k=1}^{n} S(n,k) (x-k+1)_k = x^n . $$

Finally, DLMF 26.8.39 gives the two Stirling inversion identities: $$ \sum_{j=k}^{n} s(j,k) S(n,j) = \sum_{j=k}^{n} s(n,j) S(j,k) = \delta_{n,k} . $$ These DLMF formulas use falling factorials. In this file the rising factorials of ascPochhammer are used and this entails a replacement of x by -x.

The resulting transformations define a linear equivalence of Polynomial R. It preserves the leading coefficient and natural degree. The file also proves its interaction with multiplication by X.

Main definitions and results

• ascPochhammerTransform: the linear map sending X ^ n to ascPochhammer R n.
• ascPochhammerInverseTransform: its inverse, expressed using Stirling numbers of the second kind.
• ascPochhammerLinearEquiv: the resulting linear equivalence of Polynomial R.
• coeff_ascPochhammerTransform: the coefficient formula in terms of Stirling numbers of the first kind.
• ascPochhammerTransform_X_mul: the relation between multiplication by X and the shift X ↦ X + 1.

References

[DLMF] NIST Digital Library of Mathematical Functions. https://dlmf.nist.gov/, Release 1.2.7 of 2026-06-15. F. W. J. Olver, A. B. Olde Daalhuis, D. W. Lozier, B. I. Schneider, R. F. Boisvert, C. W. Clark, B. R. Miller, B. V. Saunders, H. S. Cohl, and M. A. McClain, eds.

@[simp]

theorem coeff_ascPochhammer (R : Type u_1) [CommRing R] (n k : ℕ) : (ascPochhammer R n).coeff k = ↑(n.stirlingFirst k)

The $k$-th coefficient of the $n$-th ascending Pochhammer polynomial is the unsigned Stirling number of the first kind.

theorem ascPochhammer_eq_sum_stirlingFirst (R : Type u_1) [CommRing R] (n : ℕ) : ascPochhammer R n = ∑ k ∈ Finset.range (n + 1), (Polynomial.monomial k) ↑(n.stirlingFirst k)

Expansion of the ascending Pochhammer polynomial in the standard monomial basis, with coefficients given by the unsigned Stirling numbers of the first kind.

noncomputable def inverseAscPochhammerBasis (R : Type u_1) [CommRing R] (n : ℕ) : Polynomial R

The image of X ^ n under the inverse ascending Pochhammer transform, expressed in the standard monomial basis using signed Stirling numbers of the second kind.

Equations

• inverseAscPochhammerBasis R n = ∑ k ∈ Finset.range (n + 1), (Polynomial.monomial k) ((-1) ^ (n - k) * ↑(n.stirlingSecond k))

theorem sum_stirlingSecond_mul_ascPochhammer (R : Type u_1) [CommRing R] (n : ℕ) : ∑ k ∈ Finset.range (n + 1), ((-1) ^ (n - k) * ↑(n.stirlingSecond k)) • ascPochhammer R k = Polynomial.X ^ n

Expansion of the standard monomial X ^ n in the ascending Pochhammer basis, with coefficients given by signed Stirling numbers of the second kind.

noncomputable def ascPochhammerTransform (R : Type u_1) [CommRing R] : Polynomial R →ₗ[R] Polynomial R

The R-linear transformation of Polynomial R sending the standard monomial X ^ n to the ascending Pochhammer polynomial ascPochhammer R n.

Equations

• ascPochhammerTransform R = Polynomial.lsum fun (n : ℕ) => LinearMap.id.smulRight (ascPochhammer R n)

@[simp]

theorem ascPochhammerTransform_monomial (R : Type u_1) [CommRing R] (n : ℕ) (a : R) : (ascPochhammerTransform R) ((Polynomial.monomial n) a) = a • ascPochhammer R n

The ascending Pochhammer transform sends the monomial a * X ^ n to a • ascPochhammer R n.

@[simp]

theorem ascPochhammerTransform_X_pow (R : Type u_1) [CommRing R] (n : ℕ) : (ascPochhammerTransform R) (Polynomial.X ^ n) = ascPochhammer R n

The ascending Pochhammer transform sends the standard monomial X ^ n to the ascending Pochhammer polynomial ascPochhammer R n.

noncomputable def ascPochhammerInverseTransform (R : Type u_1) [CommRing R] : Polynomial R →ₗ[R] Polynomial R

The inverse ascending Pochhammer transform, defined by sending X ^ n to inverseAscPochhammerBasis R n and extending linearly.

Equations

• ascPochhammerInverseTransform R = Polynomial.lsum fun (n : ℕ) => LinearMap.id.smulRight (inverseAscPochhammerBasis R n)

@[simp]

theorem ascPochhammerInverseTransform_monomial (R : Type u_1) [CommRing R] (n : ℕ) (a : R) : (ascPochhammerInverseTransform R) ((Polynomial.monomial n) a) = a • inverseAscPochhammerBasis R n

The inverse ascending Pochhammer transform applied to a monomial.

@[simp]

theorem ascPochhammerInverseTransform_X_pow (R : Type u_1) [CommRing R] (n : ℕ) : (ascPochhammerInverseTransform R) (Polynomial.X ^ n) = inverseAscPochhammerBasis R n

The inverse ascending Pochhammer transform sends X ^ n to inverseAscPochhammerBasis R n.

theorem ascPochhammerTransform_inverseAscPochhammerBasis (R : Type u_1) [CommRing R] (n : ℕ) : (ascPochhammerTransform R) (inverseAscPochhammerBasis R n) = Polynomial.X ^ n

Applying the ascending Pochhammer transform to the inverse basis polynomials recovers the standard monomials $X^n$.

theorem ascPochhammerTransform_inverseTransform (R : Type u_1) [CommRing R] (p : Polynomial R) : (ascPochhammerTransform R) ((ascPochhammerInverseTransform R) p) = p

Applying the ascending Pochhammer transform after the inverse transform is the identity on polynomials.

theorem ascPochhammerTransform_comp_inverse (R : Type u_1) [CommRing R] : ascPochhammerTransform R ∘ₗ ascPochhammerInverseTransform R = LinearMap.id

The composition of the ascending Pochhammer transform and its inverse is the identity linear map.

theorem ascPochhammerTransform_apply (R : Type u_1) [CommRing R] (p : Polynomial R) : (ascPochhammerTransform R) p = p.sum fun (n : ℕ) (a : R) => a • ascPochhammer R n

Expands the ascending Pochhammer transform of p by replacing each standard monomial X ^ n by ascPochhammer R n, with the same coefficient.

theorem coeff_ascPochhammerTransform (R : Type u_1) [CommRing R] (p : Polynomial R) (k : ℕ) : ((ascPochhammerTransform R) p).coeff k = p.sum fun (n : ℕ) (a : R) => a * ↑(n.stirlingFirst k)

The k-th coefficient of the transformed polynomial, expressed as a sum over the coefficients of the original polynomial.

theorem coeff_ascPochhammerTransform_eq_sum_range (R : Type u_1) [CommRing R] (p : Polynomial R) (k : ℕ) : ((ascPochhammerTransform R) p).coeff k = ∑ n ∈ Finset.range (p.natDegree + 1), p.coeff n * ↑(n.stirlingFirst k)

The k-th coefficient of the transformed polynomial, expressed as a finite sum over degrees 0, ..., p.natDegree.

theorem coeff_natDegree_ascPochhammerTransform (R : Type u_1) [CommRing R] (p : Polynomial R) : ((ascPochhammerTransform R) p).coeff p.natDegree = p.coeff p.natDegree

The leading coefficient of the polynomial is preserved under the ascending Pochhammer transform.

theorem natDegree_ascPochhammerTransform (R : Type u_1) [CommRing R] (p : Polynomial R) : ((ascPochhammerTransform R) p).natDegree = p.natDegree

The natural degree of a polynomial is preserved under the ascending Pochhammer transform.

theorem ascPochhammerTransform_injective (R : Type u_1) [CommRing R] : Function.Injective ⇑(ascPochhammerTransform R)

The ascending Pochhammer transform is injective.

noncomputable def ascPochhammerLinearEquiv (R : Type u_1) [CommRing R] : Polynomial R ≃ₗ[R] Polynomial R

The linear equivalence of Polynomial R that sends X ^ n to the ascending Pochhammer polynomial ascPochhammer R n.

Equations

• ascPochhammerLinearEquiv R = { toLinearMap := ascPochhammerTransform R, invFun := ⇑(ascPochhammerInverseTransform R), left_inv := ⋯, right_inv := ⋯ }

theorem ascPochhammerTransform_X_mul (R : Type u_1) [CommRing R] (p : Polynomial R) : (ascPochhammerTransform R) (Polynomial.X * p) = Polynomial.X * ((ascPochhammerTransform R) p).comp (Polynomial.X + 1)

The ascending Pochhammer transform intertwines multiplication by X with multiplication by X followed by the shift X ↦ X + 1: T (X * p) = X * (T p).comp (X + 1).