English
The reflection-type relation: Γℝ(1−s) Γℝ(1+s) = (cos(π s/2))^{-1}.
Русский
Отражательная формула: Γℝ(1−s) Γℝ(1+s) = (cos(π s/2))^{-1}.
LaTeX
$$$$ \Gamma_{\mathbb{R}}(1 - s) \; \Gamma_{\mathbb{R}}(1 + s) = \left( \cos\left( \frac{\pi s}{2} \right) \right)^{-1}. $$$$
Lean4
/-- Reformulation of the reflection formula in terms of `Gammaℝ`. -/
theorem Gammaℝ_one_sub_mul_Gammaℝ_one_add (s : ℂ) : Gammaℝ (1 - s) * Gammaℝ (1 + s) = (cos (π * s / 2))⁻¹ :=
calc
Gammaℝ (1 - s) * Gammaℝ (1 + s)
_ = (π ^ ((s - 1) / 2) * π ^ ((-1 - s) / 2)) * (Gamma ((1 - s) / 2) * Gamma (1 - (1 - s) / 2)) :=
by
simp only [Gammaℝ_def]
ring_nf
_ = (π ^ ((s - 1) / 2) * π ^ ((-1 - s) / 2) * π ^ (1 : ℂ)) / sin (π / 2 - π * s / 2) :=
by
rw [Complex.Gamma_mul_Gamma_one_sub, cpow_one]
ring_nf
_ = _ := by
simp_rw [← cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero), Complex.sin_pi_div_two_sub]
ring_nf
rw [cpow_zero, one_mul]
