English
The Riemann zeta functional equation holds: ζ(1−s) = 2(2π)^(−s) Γ(s) cos(πs/2) ζ(s), provided s avoids certain exceptional values.
Русский
Функциональное уравнение дзеты Римана: ζ(1−s) = 2(2π)^(−s) Γ(s) cos(πs/2) ζ(s), при исключённых значениях s.
LaTeX
$$$\\\\riemannZeta(1-s) = 2 \\\\left( 2 \\\\pi \\right)^{-s} Γ(s) cos( π s / 2) \\\\riemannZeta(s)$, при подходящих условиях на s$$
Lean4
/-- Riemann zeta functional equation, formulated for `ζ`: if `1 - s ∉ ℕ`, then we have
`ζ (1 - s) = 2 ^ (1 - s) * π ^ (-s) * Γ s * sin (π * (1 - s) / 2) * ζ s`. -/
theorem riemannZeta_one_sub {s : ℂ} (hs : ∀ n : ℕ, s ≠ -n) (hs' : s ≠ 1) :
riemannZeta (1 - s) = 2 * (2 * π) ^ (-s) * Gamma s * cos (π * s / 2) * riemannZeta s := by
rw [riemannZeta, hurwitzZetaEven_one_sub 0 hs (Or.inr hs'), cosZeta_zero, hurwitzZetaEven_zero]
