Gamma_add_one — Mathlib

English

Recurrence: Γ(s+1) = s Γ(s) for all s ≠ 0.

Русский

Рекуррентность: Γ(s+1) = s Γ(s) для любого s ≠ 0.

LaTeX

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

Lean4

/-- The recurrence relation for the `Γ` function. -/
theorem Gamma_add_one (s : ℂ) (h2 : s ≠ 0) : Gamma (s + 1) = s * Gamma s :=
  by
  let n := ⌊1 - s.re⌋₊
  have t1 : -s.re < n := by simpa only [sub_sub_cancel_left] using Nat.sub_one_lt_floor (1 - s.re)
  have t2 : -(s + 1).re < n := by rw [add_re, one_re]; linarith
  rw [Gamma_eq_GammaAux s n t1, Gamma_eq_GammaAux (s + 1) n t2, GammaAux_recurrence1 s n t1]
  field_simp

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