Theorems · Theorem · number theory

LSeries.positive_of_differentiable_of_eqOn

∀ {a : ℕ → ℂ},
  0 ≤ a →
    0 < a 1 →
      ∀ {f : ℂ → ℂ},
        Differentiable ℂ f →
          ∀ {x : ℝ}, LSeries.abscissaOfAbsConv a ≤ ↑x → 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 ℝ.

Defined in

Mathlib.NumberTheory.LSeries.Positivity

Cited by

1 results in Mathlib

Foundations

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