English
The complex gamma function at 1/2 equals the square root of pi.
Русский
Комплексная гамма-функция в точке 1/2 равна корню из пи.
LaTeX
$$$$\\Gamma\\left(\\tfrac{1}{2}\\right) = \\sqrt{\\pi}.$$$$
Lean4
/-- The special-value formula `Γ(1/2) = √π`, which is equivalent to the Gaussian integral. -/
theorem Gamma_one_half_eq : Real.Gamma (1 / 2) = √π :=
by
rw [Gamma_eq_integral one_half_pos, ← integral_comp_rpow_Ioi_of_pos zero_lt_two]
convert congr_arg (fun x : ℝ => 2 * x) (integral_gaussian_Ioi 1) using 1
· rw [← integral_const_mul]
refine setIntegral_congr_fun measurableSet_Ioi fun x hx => ?_
dsimp only
have : (x ^ (2 : ℝ)) ^ (1 / (2 : ℝ) - 1) = x⁻¹ :=
by
rw [← rpow_mul (le_of_lt hx)]
norm_num
rw [rpow_neg (le_of_lt hx), rpow_one]
rw [smul_eq_mul, this]
simp [field, (ne_of_lt (show 0 < x from hx)).symm]
norm_num
· rw [div_one, ← mul_div_assoc, mul_comm, mul_div_cancel_right₀ _ (two_ne_zero' ℝ)]
