Gamma_nat_add_half — Mathlib

English

For a natural k, Γ(k+1/2) equals (2k-1)‼ times sqrt(pi) divided by 2^{k}.

Русский

Для натурального k, Γ(k+1/2) = (2k-1)‼ · √π / 2^{k}.

LaTeX

$$$$\\Gamma\\bigl(k+\\tfrac{1}{2}\\bigr) = (2k-1)‼ \\cdot \\frac{\\sqrt{\\pi}}{2^{k}}.$$$$

Lean4

/-- The special-value formula `Γ(k + 1/2) = (2 * k - 1)‼ * √π / (2 ^ k))` for half-integer
values of the gamma function in terms of `Nat.doubleFactorial`. -/
theorem Gamma_nat_add_half (k : ℕ) : Gamma (k + 1 / 2) = (2 * k - 1 : ℕ)‼ * √π / (2 ^ k) := by
  cases k with
  | zero => simp [-one_div, Gamma_one_half_eq]
  | succ k => simpa [-one_div, mul_add] using Gamma_nat_add_one_add_half k

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