Gamma_nat_add_one_add_half — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- The special-value formula `Γ(k + 1 + 1/2) = (2 * k + 1)‼ * √π / (2 ^ (k + 1))` for half-integer
values of the gamma function in terms of `Nat.doubleFactorial`. -/
theorem Gamma_nat_add_one_add_half (k : ℕ) : Gamma (k + 1 + 1 / 2) = (2 * k + 1 : ℕ)‼ * √π / (2 ^ (k + 1)) := by
  induction k with
  | zero => simp [-one_div, add_comm (1 : ℝ), Gamma_add_one, Gamma_one_half_eq]; ring
  | succ k
    ih =>
    rw [add_right_comm, Gamma_add_one (by positivity), Nat.cast_add, Nat.cast_one, ih, Nat.mul_add]
    simp
    ring

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