English
For s ∈ ℂ and n ∈ ℕ with -Re(s) < n, ΓAux(n,s) = ΓAux(n+1,s).
Русский
При -Re(s) < n выполняется ΓAux(n,s) = ΓAux(n+1,s).
LaTeX
$$$$ \GammaAux(n,s) = \GammaAux(n+1, s), \quad -\operatorname{Re}(s) < n. $$$$
Lean4
theorem GammaAux_recurrence1 (s : ℂ) (n : ℕ) (h1 : -s.re < ↑n) : GammaAux n s = GammaAux n (s + 1) / s := by
induction n generalizing s with
| zero =>
simp only [CharP.cast_eq_zero, Left.neg_neg_iff] at h1
dsimp only [GammaAux]; rw [GammaIntegral_add_one h1]
rw [mul_comm, mul_div_cancel_right₀]; contrapose! h1; rw [h1]
simp
| succ n hn =>
dsimp only [GammaAux]
have hh1 : -(s + 1).re < n := by
rw [Nat.cast_add, Nat.cast_one] at h1
rw [add_re, one_re]; linarith
rw [← hn (s + 1) hh1]