English
For real a and s with Re(s) > 1, the Dirichlet series HasSum for completedHurwitzZetaEven a s holds with terms depending on n+a.
Русский
Для вещественного a и s с Re(s) > 1 выполняется рядовая представление completedHurwitzZetaEven a s через сумму по n ∈ ℤ с членами, зависящими от n+a.
LaTeX
$$$\\forall a\\in\\mathbb{R},\\ {s\\in\\mathbb{C}}\\ (\\Re s>1)\\Rightarrow HasSum\\Bigl(n\\mapsto \\Gamma(s)\\,/\\,(|n+a|)^{s}\\,/2\\Bigr)\\ (\\mathrm{completedHurwitzZetaEven}(a,s)).$$$
Lean4
/-- Formula for `completedCosZeta` as a Dirichlet series in the convergence range
(second version, with sum over `ℕ`). -/
theorem hasSum_nat_completedCosZeta (a : ℝ) {s : ℂ} (hs : 1 < re s) :
HasSum (fun n : ℕ ↦ if n = 0 then 0 else Gammaℝ s * Real.cos (2 * π * a * n) / (n : ℂ) ^ s)
(completedCosZeta a s) :=
by
have aux : ((|0| : ℤ) : ℂ) ^ s = 0 := by rw [abs_zero, Int.cast_zero, zero_cpow (ne_zero_of_one_lt_re hs)]
have hint := (hasSum_int_completedCosZeta a hs).nat_add_neg
rw [aux, div_zero, zero_div, add_zero] at hint
refine hint.congr_fun fun n ↦ ?_
split_ifs with h
· simp only [h, Nat.cast_zero, aux, div_zero, zero_div, neg_zero, zero_add]
·
simp only [ofReal_cos, ofReal_mul, ofReal_ofNat, ofReal_natCast, Complex.cos,
show 2 * π * a * n * I = 2 * π * I * a * n by ring, neg_mul, mul_div_assoc, div_right_comm _ (2 : ℂ),
Int.cast_natCast, Nat.abs_cast, Int.cast_neg, mul_neg, abs_neg, ← mul_add, ← add_div]
