Gamma_mul_Gamma_add_half — Mathlib

English

The real gamma function satisfies the same half-argument relation as the complex one: Γ(s) Γ(s+1/2) = Γ(2s) 2^{1−2s} √π.

Русский

Реальная Гамма-функция удовлетворяет аналогичному отношению с половинным шагом: Γ(s) Γ(s+1/2) = Γ(2s) 2^{1−2s} √π.

LaTeX

$$$$ \Gamma(s) \Gamma\left(s + \tfrac{1}{2}\right) = \Gamma(2s) \; 2^{1-2s} \; \sqrt{\pi}. $$$$

Lean4

theorem Gamma_mul_Gamma_add_half (s : ℝ) : Gamma s * Gamma (s + 1 / 2) = Gamma (2 * s) * (2 : ℝ) ^ (1 - 2 * s) * √π :=
  by
  rw [← ofReal_inj]
  simpa only [← Gamma_ofReal, ofReal_cpow zero_le_two, ofReal_mul, ofReal_add, ofReal_div, ofReal_sub] using
    Complex.Gamma_mul_Gamma_add_half ↑s

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