English
If a is a nonnegative ℂ-valued arithmetic function and a(1) > 0, then L(a; x) is strictly positive for all x greater than the abscissa of absolute convergence.
Русский
Если a≥0 и a(1)>0, то LSeries(a; x) положительна для всех x больше абсциссы абсолютной сходимости.
LaTeX
$$$LSeries(a; x) > 0 \quad \text{for } x > \mathrm{abscissaOfAbsConv}(a)$$$
Lean4
/-- 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 positive_of_differentiable_of_eqOn {a : ℕ → ℂ} (ha₀ : 0 ≤ a) (ha₁ : 0 < a 1) {f : ℂ → ℂ}
(hf : Differentiable ℂ f) {x : ℝ} (hx : abscissaOfAbsConv a ≤ x) (hf' : {s | x < s.re}.EqOn f (LSeries a)) (y : ℝ) :
0 < f y := by
have hxy : x < max x y + 1 := (le_max_left x y).trans_lt (lt_add_one _)
have hxy' : abscissaOfAbsConv a < max x y + 1 := hx.trans_lt <| mod_cast hxy
have hys : (max x y + 1 : ℂ) ∈ {s | x < s.re} := by simp only [Set.mem_setOf_eq, add_re, ofReal_re, one_re, hxy]
have hfx : 0 < f (max x y + 1) := by simpa only [hf' hys, ofReal_add, ofReal_one] using positive ha₀ ha₁ hxy'
refine (hfx.trans_le <| hf.apply_le_of_iteratedDeriv_alternating (fun n _ ↦ ?_) ?_)
· have hs : IsOpen {s : ℂ | x < s.re} := continuous_re.isOpen_preimage _ isOpen_Ioi
simpa only [hf'.iteratedDeriv_of_isOpen hs n hys, ofReal_add, ofReal_one] using iteratedDeriv_alternating ha₀ hxy' n
· exact_mod_cast (le_max_right x y).trans (lt_add_one _).le
