completedSinZeta_one_sub — Mathlib

English

For every a, there exists p>0 such that oddKernel(a) decays at least as fast as exp(-p x) as x→+∞.

Русский

Для каждого a существует p>0, такой что oddKernel(a) затухает не медленнее exp(-p x) при x→+∞.

LaTeX

$$$$ \exists p>0,\; \operatorname{IsBigO}_{atTop}(\text{oddKernel}(a), x \mapsto e^{-p x}). $$$$

Lean4

/-- Functional equation for the odd Hurwitz zeta function (alternative form). -/
theorem completedSinZeta_one_sub (a : UnitAddCircle) (s : ℂ) :
    completedSinZeta a (1 - s) = completedHurwitzZetaOdd a s := by simp [← completedHurwitzZetaOdd_one_sub]

Похожие утверждения