English
Under a mild exclusion of negative integers, the reciprocal relation holds: (Γℝ(1−s))^{-1} = Γℂ(s) cos(π s/2) (Γℝ(s))^{-1}.
Русский
При всеми подходящими условиями выполняется: (Γℝ(1−s))^{-1} = Γℂ(s) cos(π s/2) (Γℝ(s))^{-1}.
LaTeX
$$$$ (\Gamma_{\mathbb{R}}(1 - s))^{-1} = \Gamma_{\mathbb{C}}(s) \cos\left(\frac{\pi s}{2}\right) \big( \Gamma_{\mathbb{R}}(s) \big)^{-1}, \quad s \notin \{ -n : n \in \mathbb{N} \}. $$$$
Lean4
/-- Formulation of reflection formula tailored to functional equations of L-functions of even
Dirichlet characters (including Riemann zeta). -/
theorem inv_Gammaℝ_one_sub {s : ℂ} (hs : ∀ (n : ℕ), s ≠ -n) :
(Gammaℝ (1 - s))⁻¹ = Gammaℂ s * cos (π * s / 2) * (Gammaℝ s)⁻¹ :=
by
have h1 : Gammaℝ s ≠ 0 := by
rw [Ne, Gammaℝ_eq_zero_iff, not_exists]
intro n h
specialize hs (2 * n)
simp_all
have h2 : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1) := by
intro n h
specialize hs (2 * n + 1)
simp_all
rw [← Gammaℝ_div_Gammaℝ_one_sub h2, ← div_eq_mul_inv, div_right_comm, div_self h1, one_div]
