English
The L-function TrivChar₁ is the updated trivial L-function obtained by removing the simple pole at s = 1 via a finite modification.
Русский
LFunctionTrivChar₁ — это обновлённая тривиальная L-функция, полученная удалением простого полюса в s = 1 путём конечного модифицирования.
LaTeX
$$$\text{LFunctionTrivChar}_{1}(n) = \text{update}(\text{LFunctionTrivChar}(n), 1, \prod_{p \in n.primeFactors} (1 - p^{−1}))$$$
Lean4
/-- Global root number of `χ` (for `χ` primitive; junk otherwise). Defined as
`gaussSum χ stdAddChar / I ^ a / N ^ (1 / 2)`, where `a = 0` if even, `a = 1` if odd. (The factor
`1 / I ^ a` is the Archimedean root number.) This is a complex number of absolute value 1.
-/
noncomputable def rootNumber (χ : DirichletCharacter ℂ N) : ℂ :=
gaussSum χ stdAddChar / I ^ (if χ.Even then 0 else 1) / N ^ (1 / 2 : ℂ)
