English
For a complex s and a positive integer n ≠ 0, the GammaSeq satisfies a left-recurrence relation: GammaSeq(s+1, n) divided by s equals (n/(n+1+s)) times GammaSeq(s, n).
Русский
Для комплексного s и натурального n ≠ 0 выполняется левосторонняя рекуррентная формула GammaSeq: GammaSeq(s+1, n)/s = (n/(n+1+s)) · GammaSeq(s, n).
LaTeX
$$$$ \\frac{\\GammaSeq(s+1, n)}{s} = \\frac{n}{n+1+s} \\; \\GammaSeq(s, n), \\quad n \\neq 0. $$$$
Lean4
theorem GammaSeq_add_one_left (s : ℂ) {n : ℕ} (hn : n ≠ 0) : GammaSeq (s + 1) n / s = n / (n + 1 + s) * GammaSeq s n :=
by
conv_lhs => rw [GammaSeq, Finset.prod_range_succ, div_div]
conv_rhs =>
rw [GammaSeq, Finset.prod_range_succ', Nat.cast_zero, add_zero, div_mul_div_comm, ← mul_assoc, ← mul_assoc,
mul_comm _ (Finset.prod _ _)]
congr 3
· rw [cpow_add _ _ (Nat.cast_ne_zero.mpr hn), cpow_one, mul_comm]
· refine Finset.prod_congr (by rfl) fun x _ => ?_
push_cast; ring
· abel
