English
If the L-series agrees with an entire function on a half-plane of absolute convergence and is positive on a point, then the function remains positive on a real line beyond the abscissa, given differentiability and nonnegativity of the coefficients.
Русский
Если L-ряд согласуется с целой функцией на полуплоскости с абсолютной сходимостью и положителен на одной точке, то он остаётся положительным на вещественной прямой за абсциссой, при наличии дифференцируемости и неотрицательности коэффициентов.
LaTeX
$$$f(y) > 0 \quad \text{for } y \in \mathbb{R}, \ y > \mathrm{abscissaOfAbsConv}(a)$$$
Lean4
/-- If all values of a `ℂ`-valued arithmetic function are nonnegative reals and `x` is a
real number in the domain of absolute convergence, then the `n`th iterated derivative
of the associated L-series is nonnegative real when `n` is even and nonpositive real
when `n` is odd. -/
theorem iteratedDeriv_LSeries_alternating (a : ArithmeticFunction ℂ) (hn : ∀ n, 0 ≤ a n) {x : ℝ}
(h : LSeries.abscissaOfAbsConv a < x) (n : ℕ) : 0 ≤ (-1) ^ n * iteratedDeriv n (LSeries (a ·)) x :=
LSeries.iteratedDeriv_alternating hn h n
