Positivity of values of L-series

The main results of this file are as follows.

• If a : ℕ → ℂ takes nonnegative real values and a 1 > 0, then L a x > 0 when x : ℝ is in the open half-plane of absolute convergence; see LSeries.positive and ArithmeticFunction.LSeries_positive.

• If in addition the L_series of a agrees on some open right half-plane where it converges with an entire function f, then f is positive on the real axis; see LSeries.positive_of_eq_differentiable and ArithmeticFunction.LSeries_positive_of_eq_differentiable.

theorem LSeries.iteratedDeriv_alternating {a : ℕ → ℂ} (hn : 0 ≤ a) {x : ℝ} (h : 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.

theorem LSeries.positive {a : ℕ → ℂ} (ha₀ : 0 ≤ a) (ha₁ : 0 < a 1) {x : ℝ} (hx : LSeries.abscissaOfAbsConv a < ↑x) : 0 < LSeries a ↑x

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 LSeries.positive_of_differentiable_of_eqOn {a : ℕ → ℂ} (ha₀ : 0 ≤ a) (ha₁ : 0 < a 1) {f : ℂ → ℂ} (hf : Differentiable ℂ f) {x : ℝ} (hx : LSeries.abscissaOfAbsConv a ≤ ↑x) (hf' : Set.EqOn f (LSeries a) {s : ℂ | x < s.re}) (y : ℝ) : 0 < f ↑y

If all values of a : ℕ → ℂ are nonnegative reals and a 1 is positive, and the L-series of a agrees with an entire function f on some open right half-plane where it converges, then f is real and positive on ℝ.

theorem ArithmeticFunction.iteratedDeriv_LSeries_alternating (a : ArithmeticFunction ℂ) (hn : ∀ (n : ℕ), 0 ≤ a n) {x : ℝ} (h : LSeries.abscissaOfAbsConv ⇑a < ↑x) (n : ℕ) : 0 ≤ (-1) ^ n * iteratedDeriv n (LSeries fun (x : ℕ) => a x) ↑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.

theorem ArithmeticFunction.LSeries_positive {a : ℕ → ℂ} (ha₀ : 0 ≤ a) (ha₁ : 0 < a 1) {x : ℝ} (hx : LSeries.abscissaOfAbsConv a < ↑x) : 0 < LSeries a ↑x

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 ArithmeticFunction.LSeries_positive_of_differentiable_of_eqOn {a : ArithmeticFunction ℂ} (ha₀ : 0 ≤ fun (x : ℕ) => a x) (ha₁ : 0 < a 1) {f : ℂ → ℂ} (hf : Differentiable ℂ f) {x : ℝ} (hx : LSeries.abscissaOfAbsConv ⇑a ≤ ↑x) (hf' : Set.EqOn f (LSeries ⇑a) {s : ℂ | x < s.re}) (y : ℝ) : 0 < f ↑y

If all values of a ℂ-valued arithmetic function a are nonnegative reals and a 1 is positive, and the L-series of a agrees with an entire function f on some open right half-plane where it converges, then f is real and positive on ℝ.