English
For r in a suitable semiring, the recurrence for ascPochhammer smeval with successor arguments follows the standard combinatorial pattern; i.e., smeval of ascPochhammer at (k+1) relates to previous terms via a binomial-type recurrence.
Русский
Для pразмещения ascPochhammer smeval с переходом к следующему аргументу следует стандартная комбинаторная рекуррентность.
LaTeX
$$$\mathrm{smeval}(\mathrm{ascPochhammer} (\ℕ) (k+1))\; (r+1) = \mathrm{multichoose}(r, k+1) \ + \ \mathrm{smeval}(\mathrm{ascPochhammer} (\ℕ) (k+1))\; r$$$
Lean4
theorem ascPochhammer_smeval_neg_eq_descPochhammer (r : R) (k : ℕ) :
(ascPochhammer ℕ k).smeval (-r) = Int.negOnePow k • (descPochhammer ℤ k).smeval r := by
induction k with
| zero => simp
| succ k
ih =>
simp only [ascPochhammer_succ_right, smeval_mul, ih, descPochhammer_succ_right, sub_eq_add_neg]
have h : (X + (k : ℕ[X])).smeval (-r) = -(X + (-k : ℤ[X])).smeval r := by simp [smeval_natCast, add_comm]
rw [h, ← neg_mul_comm, Int.natCast_add, Int.natCast_one, Int.negOnePow_succ, Units.neg_smul, Units.smul_def,
Units.smul_def, ← smul_mul_assoc, neg_mul]
