English
Provided s is not of the form 1−n (n natural), the shifted cosZeta satisfies cosZeta(a)(1−s) = 2 (2π)^{−s} Γ(s) cos(π s/2) cosZeta(a)(s).
Русский
При условии, что s не равно 1−n (n∈ℕ), имеет место равенство: cosZeta(a)(1−s) = 2 (2π)^{−s} Γ(s) cos(π s/2) cosZeta(a)(s).
LaTeX
$$$$\\cosZeta(a)(1-s) = 2\\cdot (2\\pi)^{-s} \\Gamma(s) \\cos\\left(\\tfrac{\\pi s}{2}\\right) \\cosZeta(a)(s), \\quad \\forall s\\text{ with } \\forall n\\in\\mathbb{N},\\ s\\neq 1-n.$$$$
Lean4
/-- If `s` is not of the form `1 - n` for `n ∈ ℕ`, then `cosZeta a (1 - s)` is an explicit
multiple of `hurwitzZetaEven s`. -/
theorem cosZeta_one_sub (a : UnitAddCircle) {s : ℂ} (hs : ∀ (n : ℕ), s ≠ 1 - n) :
cosZeta a (1 - s) = 2 * (2 * π) ^ (-s) * Gamma s * cos (π * s / 2) * hurwitzZetaEven a s :=
by
rw [← Gammaℂ]
have : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (Gammaℝ (1 - s))⁻¹ :=
by
rw [cosZeta, Function.update_of_ne, div_eq_mul_inv]
simpa [sub_eq_zero] using (hs 0).symm
rw [this, completedCosZeta_one_sub, inv_Gammaℝ_one_sub (fun n ↦ by simpa using hs (n + 1)),
hurwitzZetaEven_def_of_ne_or_ne (Or.inr (by simpa using hs 1))]
generalize Gammaℂ s * cos (π * s / 2) = A
ring_nf
