hurwitzZeta — Mathlib

English

For χ and s with s ≠ 0 or N ≠ 1, L(χ,s) = completedLFunction(χ,s) / gammaFactor(χ,s).

Русский

Для χ и s с s ≠ 0 или N ≠ 1 имеет место тождество L(χ,s) = completedLFunction(χ,s) / gammaFactor(χ,s).

LaTeX

$$$L(\chi,s) = \dfrac{\text{completedLFunction}(\chi,s)}{\gamma\text{Factor}(\chi,s)}$$$

Lean4

/-- The Hurwitz zeta function, which is the meromorphic continuation of
`∑ (n : ℕ), 1 / (n + a) ^ s` if `0 ≤ a ≤ 1`. See `hasSum_hurwitzZeta_of_one_lt_re` for the relation
to the Dirichlet series in the convergence range. -/
noncomputable def hurwitzZeta (a : UnitAddCircle) (s : ℂ) :=
  hurwitzZetaEven a s + hurwitzZetaOdd a s

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