English
Let r and n be nonnegative integers. The ascending Pochhammer polynomial with parameter r, evaluated at n, satisfies a forward recurrence: n times its value at n+1 equals (n + r) times its value at n.
Русский
Пусть r и n — неотрицательные целые числа. Возрастающий полином Поххаммера с параметром r, вычисляемый в точке n, удовлетворяет переходному правилу: n умножить на значение в точке n+1 равно (n + r) умножить на значение в точке n.
LaTeX
$$$n\cdot (\operatorname{ascPochhammer}_{\mathbb{N}}(r)).eval(n+1) = (n+r)\cdot (\operatorname{ascPochhammer}_{\mathbb{N}}(r)).eval(n)$$$
Lean4
theorem ascPochhammer_nat_eval_succ (r : ℕ) :
∀ n : ℕ, n * (ascPochhammer ℕ r).eval (n + 1) = (n + r) * (ascPochhammer ℕ r).eval n
| 0 => by
by_cases h : r = 0
· simp only [h, zero_mul, zero_add]
· simp only [ascPochhammer_eval_zero, zero_mul, if_neg h, mul_zero]
| k + 1 => by simp only [ascPochhammer_nat_eq_ascFactorial, Nat.succ_ascFactorial, add_right_comm]
