Pochhammer

Stream: maths

[Johan Commelin]

I just discussed with @Yaël Dillies about the Pochhammer polynomial. In mathlib we now have two variants, the ascending Pochhammer polynomial and the descending Pochhammer polynomial. I think it is possible to unify them.

We can have pochhammer (n : A) : R[X] where:

• R is a semiring
• A is a locally finite linearly ordered additive monoid
• there is a coercion from A to R

Then pochhammer n can be defined as the product of X + (i:R) where i ranges over (Finset.uIcc 0 n).erase n.
For n : \Z negative, this recovers the descending version, and for n : \N this recovers the ascending version. I think \N and \Z are the only values of A that we care about, but who knows... we've been surprised before.

Interested to hear feedback about this proposed refactor. cc @Moritz Firsching

[Yaël Dillies]

I think you only need:

• R is a semiring
• A is a locally finite lattice with a 0
• there is a coercion from A to R

But I doubt it widens the applications.

[Johan Commelin]

A needs a 0, but yes, I guess you're right that we don't need the addition.

[Moritz Firsching]

I guess this can be done. I'm not entirely sure what the benefit over the status quo. At least it would probably be convenient to keep some names for both variants, since some other theorems might involve one or the other, or one could just get used to pochhammer n for negative n. Should this be in sync with Nat.ascFactorial and Nat.descFactorial?

In any case, no matter what the definition is, we should add the relations

$${(x)}_n = {(x-n+1)}^{(n)} = (-1)^n (-x)^{(n)}$$

and

$$x^{(n)} = {(x+n-1)}_{n} = (-1)^n (-x)_n$$

[Johan Commelin]

One benefit is that some lemmas get deduplicated.

[Moritz Firsching]

makes sense

[Yaël Dillies]

I doubt Nat.descFactorial can fit in this picture because of the lack of map ℤ → ℕ. However, we could generalise pochhammer away from Polynomial so that the current pochhammer k becomes pochhammer X k and Nat.ascFactorial n k becomes pochhammer n k.

[Johan Commelin]

Which, I guess also generalises the pochEval that @Scott Carnahan introduces in his PR on binomial rings.

[Yaël Dillies]

(#6934)

[Moritz Firsching]

Thanks for the pointer, I didn't even see that one

[Scott Carnahan]

I would be very happy with a generalization of pochhammer that didn't require me to deal with evaluation of polynomials. This was one reason I introduced pochEval. The other reason was because Nat.ascFactorial has an annoying shift by one, e.g., Nat.ascFactorial n 1 = n+1 instead of n. I wanted something that would generalize to semirings without occasionally needing to subtract one.