doublingGamma_add_one — Mathlib

English

For all real s with s ≠ 0, doublingGamma(s+1) = s · doublingGamma(s).

Русский

Для любого действительного s ≠ 0 выполняется doublingGamma(s+1) = s · doublingGamma(s).

LaTeX

$$$ \mathrm{doublingGamma}(s+1) = s \cdot \mathrm{doublingGamma}(s) \quad (s \ne 0) $$$

Lean4

theorem doublingGamma_add_one (s : ℝ) (hs : s ≠ 0) : doublingGamma (s + 1) = s * doublingGamma s :=
  by
  rw [doublingGamma, doublingGamma, (by abel : s + 1 - 1 = s - 1 + 1), add_div, add_assoc, add_halves (1 : ℝ),
    Gamma_add_one (div_ne_zero hs two_ne_zero), rpow_add two_pos, rpow_one]
  ring

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