English
If a≥0 componentwise and x is to the right of the abscissa of absolute convergence, then the nth iterated derivative of the L-series is nonnegative after multiplication by (−1)^n, i.e., the sign alternates with n.
Русский
Если компонентa(n) неотрицателен и x находится справа от абсциссы абсолютной сходимости, то n-ая итеративная производная L-рядa умноженная на (−1)^n неотрицательна, знак чередуется по n.
LaTeX
$$$0 \le (-1)^n \cdot \mathrm{iteratedDeriv}_n \ \mathrm{LSeries}(a; x) \quad (n\in\mathbb{N})$$$
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_alternating {a : ℕ → ℂ} (hn : 0 ≤ a) {x : ℝ} (h : LSeries.abscissaOfAbsConv a < x) (n : ℕ) :
0 ≤ (-1) ^ n * iteratedDeriv n (LSeries a) x :=
by
rw [LSeries_iteratedDeriv _ h, LSeries, ← mul_assoc, ← pow_add, Even.neg_one_pow ⟨n, rfl⟩, one_mul]
refine tsum_nonneg fun k ↦ ?_
rw [LSeries.term_def]
split
· exact le_rfl
· refine mul_nonneg ?_ <| (inv_natCast_cpow_ofReal_pos (by assumption) x).le
induction n with
| zero => simpa only [Function.iterate_zero, id_eq] using hn k
| succ n IH =>
rw [Function.iterate_succ_apply']
refine mul_nonneg ?_ IH
simp only [← natCast_log, zero_le_real, Real.log_natCast_nonneg]
