English
The generalization of choose to negative first argument: choose (−r) n equals (−1)^n times choose (r+n−1) n.
Русский
Обобщение choose для отрицательного аргумента: choose(−r) n = (−1)^n · choose (r+n−1) n.
LaTeX
$$$ \forall R\ [NonAssocRing\ R]\ [Pow\ R\ Nat]\ [BinomialRing\ R]\ (r: R)\ (n: \mathbb{N}),\ choose(-r) n = (-1)^n \cdot choose (r+n-1) n$$$
Lean4
/-- Pochhammer version of Chu-Vandermonde identity -/
theorem descPochhammer_smeval_add [Ring R] {r s : R} (k : ℕ) (h : Commute r s) :
(descPochhammer ℤ k).smeval (r + s) =
∑ ij ∈ antidiagonal k,
Nat.choose k ij.1 * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s) :=
by
induction k with
| zero => simp
| succ k
ih =>
rw [descPochhammer_succ_right, mul_comm, smeval_mul,
sum_antidiagonal_choose_succ_mul fun i j => ((descPochhammer ℤ i).smeval r * (descPochhammer ℤ j).smeval s), ←
sum_add_distrib, smeval_sub, smeval_X, smeval_natCast, pow_zero, pow_one, ih, mul_sum]
refine sum_congr rfl ?_
intro ij hij
have hdx :
(descPochhammer ℤ ij.1).smeval r * (X - (ij.2 : ℤ[X])).smeval s =
(X - (ij.2 : ℤ[X])).smeval s * (descPochhammer ℤ ij.1).smeval r :=
by
refine (commute_iff_eq ((descPochhammer ℤ ij.1).smeval r) ((X - (ij.2 : ℤ[X])).smeval s)).mp ?_
exact smeval_commute ℤ (descPochhammer ℤ ij.1) (X - (ij.2 : ℤ[X])) h
rw [descPochhammer_succ_right, mul_comm, smeval_mul, descPochhammer_succ_right, mul_comm, smeval_mul, ←
mul_assoc ((descPochhammer ℤ ij.1).smeval r), hdx]
simp only [mul_assoc _ ((descPochhammer ℤ ij.1).smeval r) _,
← mul_assoc _ _ (((descPochhammer ℤ ij.1).smeval r) * _)]
have hl :
(r + s - k • 1) * (k.choose ij.1) =
(k.choose ij.1) * (X - (ij.2 : ℤ[X])).smeval s + ↑(k.choose ij.2) * (X - (ij.1 : ℤ[X])).smeval r :=
by
simp only [smeval_sub, smeval_X, pow_one, smeval_natCast, pow_zero]
rw [← Nat.choose_symm_of_eq_add (List.Nat.mem_antidiagonal.mp hij).symm, (List.Nat.mem_antidiagonal.mp hij).symm,
← mul_add, Nat.cast_comm, add_smul]
abel_nf
rw [hl, ← add_mul]
