Gamma_mul_Gamma_add_half_of_pos — Mathlib

English

Legendre's duplication formula: for s > 0, Γ(s) Γ(s+1/2) = Γ(2s) 2^{1-2s} √π.

Русский

Формула удвоения Лежандра: для s > 0, Γ(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} \quad (s>0) $$$

Lean4

/-- Legendre's doubling formula for the Gamma function, for positive real arguments. Note that
we shall later prove this for all `s` as `Real.Gamma_mul_Gamma_add_half` (superseding this result)
but this result is needed as an intermediate step. -/
theorem Gamma_mul_Gamma_add_half_of_pos {s : ℝ} (hs : 0 < s) :
    Gamma s * Gamma (s + 1 / 2) = Gamma (2 * s) * 2 ^ (1 - 2 * s) * √π :=
  by
  rw [← doublingGamma_eq_Gamma (mul_pos two_pos hs), doublingGamma, mul_div_cancel_left₀ _ (two_ne_zero' ℝ),
    (by abel : 1 - 2 * s = -(2 * s - 1)), rpow_neg zero_le_two]
  field_simp

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