English
For all x ∈ ℝ and n ∈ ℕ, logGammaSeq(x+1,n) = logGammaSeq(x,n+1) + log x − (x+1)(log(n+1) − log n).
Русский
Для всех x ∈ ℝ и n ∈ ℕ выполняется logGammaSeq(x+1,n) = logGammaSeq(x,n+1) + log x − (x+1)(log(n+1) − log n).
LaTeX
$$$$ \logGammaSeq(x+1,n) = \logGammaSeq(x,n+1) + \log x - (x+1)(\log(n+1) - \log n). $$$$
Lean4
theorem logGammaSeq_add_one (x : ℝ) (n : ℕ) :
logGammaSeq (x + 1) n = logGammaSeq x (n + 1) + log x - (x + 1) * (log (n + 1) - log n) :=
by
dsimp only [Nat.factorial_succ, logGammaSeq]
conv_rhs => rw [Finset.sum_range_succ', Nat.cast_zero, add_zero]
rw [Nat.cast_mul, log_mul]; rotate_left
· rw [Nat.cast_ne_zero]; exact Nat.succ_ne_zero n
· rw [Nat.cast_ne_zero]; exact Nat.factorial_ne_zero n
have : ∑ m ∈ Finset.range (n + 1), log (x + 1 + ↑m) = ∑ k ∈ Finset.range (n + 1), log (x + ↑(k + 1)) :=
by
congr! 2 with m
push_cast
abel
rw [← this, Nat.cast_add_one n]
ring
