Theorems · Theorem · number theory

LSeries.iteratedDeriv_alternating

∀ {a : ℕ → ℂ},
  0 ≤ a → ∀ {x : ℝ}, LSeries.abscissaOfAbsConv a < ↑x → ∀ (n : ℕ), 0 ≤ (-1) ^ n * iteratedDeriv n (LSeries a) ↑x

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 nth iterated derivative of the associated L-series is nonnegative real when n is even and nonpositive real when n is odd.

Defined in

Mathlib.NumberTheory.LSeries.Positivity

Cited by

2 results in Mathlib

Foundations

Depth 298 from the axioms · uses propext, Classical.choice, Quot.sound