hurwitzZetaOdd — Mathlib

English

hurwitzZetaOdd(a, s) is the odd part of Hurwitz zeta: hurwitzZetaOdd(a,s) = completedHurwitzZetaOdd(a,s) / Gamma(s+1).

Русский

hurwitzZetaOdd(a,s) является нечетной частью Хёрвитца ζ-функции: hurwitzZetaOdd(a,s) = completedHurwitzZetaOdd(a,s) / Γ(s+1).

LaTeX

$$$$ \operatorname{hurwitzZetaOdd}(a,s) = \frac{\operatorname{completedHurwitzZetaOdd}(a,s)}{\Gamma(s+1)}. $$$$

Lean4

/-- The odd part of the Hurwitz zeta function, i.e. the meromorphic function of `s` which agrees
with `1 / 2 * ∑' (n : ℤ), sign (n + a) / |n + a| ^ s` for `1 < re s` -/
noncomputable def hurwitzZetaOdd (a : UnitAddCircle) (s : ℂ) :=
  completedHurwitzZetaOdd a s / Gammaℝ (s + 1)

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