Gamma_add_one — Mathlib

English

For any real s ≠ 0, the Gamma function satisfies the recurrence Γ(s+1) = s Γ(s).

Русский

Для любого действительного s ≠ 0 гамма-функция удовлетворяет рекуррентному отношению Γ(s+1) = s Γ(s).

LaTeX

$$$\Gamma(s+1) = s\,\Gamma(s) \quad (s \neq 0)$$$

Lean4

theorem Gamma_add_one {s : ℝ} (hs : s ≠ 0) : Gamma (s + 1) = s * Gamma s :=
  by
  simp_rw [Gamma]
  rw [Complex.ofReal_add, Complex.ofReal_one, Complex.Gamma_add_one, Complex.re_ofReal_mul]
  rwa [Complex.ofReal_ne_zero]

Похожие утверждения