English
The iterated derivatives of the L-series in the alternating sense preserve nonnegativity under suitable assumptions, extending the positivity phenomenon to higher-order derivatives.
Русский
Итерированные производные L-рядa в чередующемся виде сохраняют неотрицательность при корректных предположениях, распространяя положительное свойство на производные более высокого порядка.
LaTeX
$$$0 \le (-1)^n \cdot \mathrm{iteratedDeriv}_n (\mathrm{LSeries}(a))(x) \quad (n\ge 0)$$$
Lean4
/-- If all values of a `ℂ`-valued arithmetic function `a` are nonnegative reals and `a 1` is
positive, then `L a x` is positive real for all real `x` larger than `abscissaOfAbsConv a`. -/
theorem LSeries_positive {a : ℕ → ℂ} (ha₀ : 0 ≤ a) (ha₁ : 0 < a 1) {x : ℝ} (hx : LSeries.abscissaOfAbsConv a < x) :
0 < LSeries a x :=
LSeries.positive ha₀ ha₁ hx
