English
For all s and under mild exclusion, (Γℝ(2−s))^{-1} = Γℂ(s) sin(π s/2) (Γℝ(s+1))^{-1}.
Русский
Для всех допустимых s выполняется: (Γℝ(2−s))^{-1} = Γℂ(s) sin(π s/2) (Γℝ(s+1))^{-1}.
LaTeX
$$$$ (\Gamma_{\mathbb{R}}(2 - s))^{-1} = \Gamma_{\mathbb{C}}(s) \sin\left(\frac{\pi s}{2}\right) \big( \Gamma_{\mathbb{R}}(s + 1)\big)^{-1}. $$$$
Lean4
/-- Formulation of reflection formula tailored to functional equations of L-functions of odd
Dirichlet characters. -/
theorem inv_Gammaℝ_two_sub {s : ℂ} (hs : ∀ (n : ℕ), s ≠ -n) :
(Gammaℝ (2 - s))⁻¹ = Gammaℂ s * sin (π * s / 2) * (Gammaℝ (s + 1))⁻¹ :=
by
by_cases h : s = 1
·
rw [h, (by ring : 2 - 1 = (1 : ℂ)), Gammaℝ_one, Gammaℝ, neg_div, (by simp : (1 + 1) / 2 = (1 : ℂ)),
Complex.Gamma_one, Gammaℂ_one, mul_one, Complex.sin_pi_div_two, mul_one, cpow_neg_one, mul_one, inv_inv,
div_mul_cancel₀ _ (ofReal_ne_zero.mpr pi_ne_zero), inv_one]
rw [← Ne, ← sub_ne_zero] at h
have h' (n : ℕ) : s - 1 ≠ -n := by
rcases n with - | m
· rwa [Nat.cast_zero, neg_zero]
· rw [Ne, sub_eq_iff_eq_add]
convert hs m using 2
push_cast
ring
rw [(by ring : 2 - s = 1 - (s - 1)), inv_Gammaℝ_one_sub h', (by rw [sub_add_cancel] : Gammaℂ s = Gammaℂ (s - 1 + 1)),
Gammaℂ_add_one h, (by ring : s + 1 = (s - 1) + 2), Gammaℝ_add_two h, mul_sub, sub_div, mul_one,
Complex.cos_sub_pi_div_two]
simp_rw [mul_div_assoc, mul_inv]
generalize (Gammaℝ (s - 1))⁻¹ = A
field_simp
