English
The division version: Γℝ(s) / Γℝ(1−s) = Γℂ(s) cos(π s/2).
Русский
Формула деления: Γℝ(s) / Γℝ(1−s) = Γℂ(s) cos(π s/2).
LaTeX
$$$$ \frac{\Gamma_{\mathbb{R}}(s)}{\Gamma_{\mathbb{R}}(1 - s)} = \Gamma_{\mathbb{C}}(s) \cos\left(\frac{\pi s}{2}\right). $$$$
Lean4
/-- Another formulation of the reflection formula in terms of `Gammaℝ`. -/
theorem Gammaℝ_div_Gammaℝ_one_sub {s : ℂ} (hs : ∀ (n : ℕ), s ≠ -(2 * n + 1)) :
Gammaℝ s / Gammaℝ (1 - s) = Gammaℂ s * cos (π * s / 2) :=
by
have : Gammaℝ (s + 1) ≠ 0 := by
simpa only [Ne, Gammaℝ_eq_zero_iff, not_exists, ← eq_sub_iff_add_eq, sub_eq_add_neg, ← neg_add]
calc
Gammaℝ s / Gammaℝ (1 - s)
_ = (Gammaℝ s * Gammaℝ (s + 1)) / (Gammaℝ (1 - s) * Gammaℝ (1 + s)) := by
rw [add_comm 1 s, mul_comm (Gammaℝ (1 - s)) (Gammaℝ (s + 1)), ← div_div, mul_div_cancel_right₀ _ this]
_ = (2 * (2 * π) ^ (-s) * Gamma s) / ((cos (π * s / 2))⁻¹) := by
rw [Gammaℝ_one_sub_mul_Gammaℝ_one_add, Gammaℝ_mul_Gammaℝ_add_one, Gammaℂ_def]
_ = _ := by rw [Gammaℂ_def, div_eq_mul_inv, inv_inv]
