Gamma_one_half_eq — Mathlib

English

The complex gamma at 1/2 equals sqrt(pi) in the complex sense.

Русский

Гамма в комплексной области в точке 1/2 равна sqrt(pi).

LaTeX

$$$$\\Gamma\\left(\\tfrac{1}{2}\\right) = (\\pi)^{1/2}.$$$$

Lean4

/-- The special-value formula `Γ(1/2) = √π`, which is equivalent to the Gaussian integral. -/
theorem Gamma_one_half_eq : Complex.Gamma (1 / 2) = (π : ℂ) ^ (1 / 2 : ℂ) :=
  by
  convert congr_arg ((↑) : ℝ → ℂ) Real.Gamma_one_half_eq
  · simpa only [one_div, ofReal_inv, ofReal_ofNat] using Gamma_ofReal (1 / 2)
  · rw [sqrt_eq_rpow, ofReal_cpow pi_pos.le, ofReal_div, ofReal_ofNat, ofReal_one]

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