English
The real-argument gamma values satisfy a doubling relation with the complex gamma: Γℝ(s) Γℝ(s+1) = Γℂ(s).
Русский
Формула удвоения: Γℝ(с) Γℝ(с+1) = Γℂ(с).
LaTeX
$$$$ \Gamma_{\mathbb{R}}(s) \; \Gamma_{\mathbb{R}}(s+1) = \Gamma_{\mathbb{C}}(s). $$$$
Lean4
/-- Reformulation of the doubling formula in terms of `Gammaℝ`. -/
theorem Gammaℝ_mul_Gammaℝ_add_one (s : ℂ) : Gammaℝ s * Gammaℝ (s + 1) = Gammaℂ s :=
by
simp only [Gammaℝ_def, Gammaℂ_def]
calc
_ = (π ^ (-s / 2) * π ^ (-(s + 1) / 2)) * (Gamma (s / 2) * Gamma (s / 2 + 1 / 2)) := by ring_nf
_ = 2 ^ (1 - s) * (π ^ (-1 / 2 - s) * π ^ (1 / 2 : ℂ)) * Gamma s :=
by
rw [← cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero), Complex.Gamma_mul_Gamma_add_half, sqrt_eq_rpow,
ofReal_cpow pi_pos.le, ofReal_div, ofReal_one, ofReal_ofNat]
ring_nf
_ = 2 * ((2 : ℝ) ^ (-s) * π ^ (-s)) * Gamma s :=
by
rw [sub_eq_add_neg, cpow_add _ _ two_ne_zero, cpow_one, ← cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero),
ofReal_ofNat]
ring_nf
_ = 2 * (2 * π) ^ (-s) * Gamma s := by rw [← mul_cpow_ofReal_nonneg two_pos.le pi_pos.le, ofReal_ofNat]
