English
For real a and s with Re(s) > 1, there is a Dirichlet series expansion of completedHurwitzZetaEven a s as a sum over ℤ 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 `completedHurwitzZetaEven` as a Dirichlet series in the convergence range. -/
theorem hasSum_int_completedHurwitzZetaEven (a : ℝ) {s : ℂ} (hs : 1 < re s) :
HasSum (fun n : ℤ ↦ Gammaℝ s / (↑|n + a| : ℂ) ^ s / 2) (completedHurwitzZetaEven a s) :=
by
have hF (t : ℝ) (ht : 0 < t) :
HasSum (fun n : ℤ ↦ if n + a = 0 then 0 else (1 / 2 : ℂ) * rexp (-π * (n + a) ^ 2 * t))
((evenKernel a t - (if (a : UnitAddCircle) = 0 then 1 else 0 : ℝ)) / 2) :=
by
refine (ofReal_sub .. ▸ (hasSum_ofReal.mpr (hasSum_int_evenKernel₀ a ht)).div_const 2).congr_fun fun n ↦ ?_
split_ifs
· rw [ofReal_zero, zero_div]
· rw [mul_comm, mul_one_div]
rw [show
completedHurwitzZetaEven a s =
mellin (fun t ↦ ((evenKernel (↑a) t : ℂ) - ↑(if (a : UnitAddCircle) = 0 then 1 else 0 : ℝ)) / 2) (s / 2)
by
simp_rw [mellin_div_const, apply_ite ofReal, ofReal_one, ofReal_zero]
refine congr_arg (· / 2) ((hurwitzEvenFEPair a).hasMellin (?_ : 1 / 2 < (s / 2).re)).2.symm
rwa [div_ofNat_re, div_lt_div_iff_of_pos_right two_pos]]
refine (hasSum_mellin_pi_mul_sq (zero_lt_one.trans hs) hF ?_).congr_fun fun n ↦ ?_
· simp_rw [← mul_one_div ‖_‖]
apply Summable.mul_left
rwa [summable_one_div_int_add_rpow]
· rw [mul_one_div, div_right_comm]
