English
The family residueClass for a fixed modulus q decomposes into a Dirichlet-twisted sum, yielding a linear combination of twists of vonMangoldt; this makes summability arguments workable via characters.
Русский
Семейство residueClass по модулю q распадается на линейную комбинацию twists (скручиваний) функции vonMangoldt по дуги Дирихле; это упрощает суммируемость через символы.
LaTeX
$$$\operatorname{residueClass}(a;n) = \frac{1}{q\varphi(q)} \sum_{\chi} χ(a)^{-1} χ(n) \Lambda(n)$$$
Lean4
/-- If all values of a `ℂ`-valued arithmetic function `a` are nonnegative reals and `a 1`
is positive, and the L-series of `a` agrees with an entire function `f` on some open
right half-plane where it converges, then `f` is real and positive on `ℝ`. -/
theorem LSeries_positive_of_differentiable_of_eqOn {a : ArithmeticFunction ℂ} (ha₀ : 0 ≤ (a ·)) (ha₁ : 0 < a 1)
{f : ℂ → ℂ} (hf : Differentiable ℂ f) {x : ℝ} (hx : LSeries.abscissaOfAbsConv a ≤ x)
(hf' : {s | x < s.re}.EqOn f (LSeries a)) (y : ℝ) : 0 < f y :=
LSeries.positive_of_differentiable_of_eqOn ha₀ ha₁ hf hx hf' y
