English
The isomorphism symmetry implies has sum structure is preserved under negation of a, i.e., hasSum structure is invariant under a → −a for the zero-pole-removed version.
Русский
Симметрия сохраняет структуру суммирования при замене a на −a для версии без полюсов.
LaTeX
$$$$ \\text{For all } a,\\ s, \\text{ } \\operatorname{completedHurwitzZetaEven}_0(-a,s) = \\operatorname{completedHurwitzZetaEven}_0(a,s). $$$$
Lean4
/-- The function `evenKernel a - L` has exponential decay at `+∞`, where `L = 1` if
`a = 0` and `L = 0` otherwise. -/
theorem isBigO_atTop_evenKernel_sub (a : UnitAddCircle) :
∃ p : ℝ, 0 < p ∧ (evenKernel a · - (if a = 0 then 1 else 0)) =O[atTop] (rexp <| -p * ·) := by
induction a using QuotientAddGroup.induction_on with
| H b =>
obtain ⟨p, hp, hp'⟩ := HurwitzKernelBounds.isBigO_atTop_F_int_zero_sub b
refine ⟨p, hp, (EventuallyEq.isBigO ?_).trans hp'⟩
filter_upwards [eventually_gt_atTop 0] with t h
simp [← (hasSum_int_evenKernel b h).tsum_eq, HurwitzKernelBounds.F_int, HurwitzKernelBounds.f_int]
