English
ExpZeta satisfies a functional equation relating s and 1 − s, involving Gamma and HurwitzZeta at a and −a.
Русский
ExpZeta удовлетворяет функциональному равенству, связывающему s и 1 − s, с участием Γ и HurwitzZeta в точках a и −a.
LaTeX
$$$$\\expZeta(a,1-s) = (2\\pi)^{-s} \\Gamma(s) \\left( e^{\\pi i s/2} \\expZeta(a,s) + e^{-\\pi i s/2} \\expZeta(-a,s)\\right).$$$$
Lean4
/-- Functional equation for the exponential zeta function. -/
theorem expZeta_one_sub (a : UnitAddCircle) {s : ℂ} (hs : ∀ (n : ℕ), s ≠ 1 - n) :
expZeta a (1 - s) =
(2 * π) ^ (-s) * Gamma s * (exp (π * I * s / 2) * hurwitzZeta a s + exp (-π * I * s / 2) * hurwitzZeta (-a) s) :=
by
have hs' (n : ℕ) : s ≠ -↑n := by
convert hs (n + 1) using 1
push_cast
ring
rw [expZeta, cosZeta_one_sub a hs, sinZeta_one_sub a hs', hurwitzZeta, hurwitzZeta, hurwitzZetaEven_neg,
hurwitzZetaOdd_neg, Complex.cos, Complex.sin]
rw [show ↑π * I * s / 2 = ↑π * s / 2 * I by ring, show -↑π * I * s / 2 = -(↑π * s / 2) * I by ring]
-- these `generalize` commands are not strictly needed for the `ring_nf` call to succeed, but
-- make it run faster:
generalize (2 * π : ℂ) ^ (-s) = x
generalize (↑π * s / 2 * I).exp = y
generalize (-(↑π * s / 2) * I).exp = z
ring_nf
rw [I_sq]
ring_nf
