Chu–Vandermonde identities for the ascending Pochhammer polynomial

Mathlib already records the falling-factorial Chu–Vandermonde identity as Ring.descPochhammer_smeval_add, and the binomial-ring form as Ring.add_choose_eq. The matching identities for the rising factorial ascPochhammer are not present.

This file is a temporary home. Intended Mathlib placement:

• ascPochhammer_smeval_add, ascPochhammer_eval_add → Mathlib.RingTheory.Binomial, immediately after Ring.descPochhammer_smeval_add
• ascPochhammer_eval_sum → the same file, after the binary identity

TODO: if those lemmas land in Mathlib, delete this file and switch uses to the upstream names.

theorem ascPochhammer_eval_add {R : Type u_1} [CommSemiring R] (r s : R) (k : ℕ) : Polynomial.eval (r + s) (ascPochhammer R k) = ∑ ij ∈ Finset.antidiagonal k, ↑(k.choose ij.1) * (Polynomial.eval r (ascPochhammer R ij.1) * Polynomial.eval s (ascPochhammer R ij.2))

Chu–Vandermonde identity for the rising factorial.

This is the ascending counterpart of Ring.descPochhammer_smeval_add. In Appell's notation it is ((r+s,k)=\sum_m \binom{k}{m}(r,m)(s,k-m)).

theorem ascPochhammer_smeval_add {R : Type u_1} [CommSemiring R] (r s : R) (k : ℕ) : (ascPochhammer ℕ k).smeval (r + s) = ∑ ij ∈ Finset.antidiagonal k, ↑(k.choose ij.1) * ((ascPochhammer ℕ ij.1).smeval r * (ascPochhammer ℕ ij.2).smeval s)

Smeval form of ascPochhammer_eval_add, matching the statement shape of Ring.descPochhammer_smeval_add.

theorem ascPochhammer_eval_add_sum_range {R : Type u_1} [CommSemiring R] (r s : R) (k : ℕ) : Polynomial.eval (r + s) (ascPochhammer R k) = ∑ m ∈ Finset.range (k + 1), ↑(k.choose m) * (Polynomial.eval r (ascPochhammer R m) * Polynomial.eval s (ascPochhammer R (k - m)))

Range form of ascPochhammer_eval_add.

theorem ascPochhammer_eval_sum {R : Type u_1} [CommSemiring R] {ι : Type u_2} [DecidableEq ι] (s : Finset ι) (b : ι → R) (n : ℕ) : Polynomial.eval (∑ i ∈ s, b i) (ascPochhammer R n) = ∑ m ∈ s.piAntidiag n, ↑(Nat.multinomial s m) * ∏ i ∈ s, Polynomial.eval (b i) (ascPochhammer R (m i))

Multinomial Chu–Vandermonde identity for the rising factorial.

In Appell's notation this is ((∑_i b_i,,n)=\sum \mathrm{multinomial}(m),∏_i (b_i,m_i)), summed over multi-indices with (|m|=n).