English
For a nonnegative-valued ℂ-valued arithmetic function a, the iterated derivatives of its L-series satisfy a similar alternating sign bound on a horizontal region to the right of the abscissa of absolute convergence.
Русский
Для вещественно неотрицательной ℂ-значной арифметической функции a итеративные производные L-рядa удовлетворяют аналогичному неравенству по знаку на правой полуплоскости.
LaTeX
$$$0 \le (-1)^n \cdot \mathrm{iteratedDeriv}_n (\mathrm{LSeries}(a; \cdot))(x) \quad (x > \mathrm{abscissaOfAbsConv}(a))$$$
Lean4
/-- If all values of `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 positive {a : ℕ → ℂ} (ha₀ : 0 ≤ a) (ha₁ : 0 < a 1) {x : ℝ} (hx : abscissaOfAbsConv a < x) : 0 < LSeries a x :=
by
rw [LSeries]
refine Summable.tsum_pos ?_ (fun n ↦ term_nonneg (ha₀ n) x) 1 <| term_pos one_ne_zero ha₁ x
exact LSeriesSummable_of_abscissaOfAbsConv_lt_re <| by simpa only [ofReal_re] using hx
