English
CosZeta(a,s) equals the average of expZeta(a,s) and expZeta(-a,s): cosZeta(a,s) = (expZeta(a,s) + expZeta(-a,s))/2.
Русский
CosZeta(a,s) равно среднему значения ExpZeta(a,s) и ExpZeta(-a,s): cosZeta(a,s) = (expZeta(a,s) + expZeta(-a,s))/2.
LaTeX
$$$$\\cosZeta(a,s) = \\frac{\\expZeta(a,s) + \\expZeta(-a,s)}{2}.$$$$
Lean4
theorem hurwitzZeta_one_sub (a : UnitAddCircle) {s : ℂ} (hs : ∀ (n : ℕ), s ≠ -n) (hs' : a ≠ 0 ∨ s ≠ 1) :
hurwitzZeta a (1 - s) =
(2 * π) ^ (-s) * Gamma s * (exp (-π * I * s / 2) * expZeta a s + exp (π * I * s / 2) * expZeta (-a) s) :=
by
rw [hurwitzZeta, hurwitzZetaEven_one_sub a hs hs', hurwitzZetaOdd_one_sub a hs, expZeta, expZeta, Complex.cos,
Complex.sin, sinZeta_neg, cosZeta_neg]
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
