LSeriesSummable_logMul_of_lt_re — Mathlib

English

If abscissaOfAbsConv f < s.re, then LSeriesSummable (logMul f) s.

Русский

Если abscissaOfAbsConv f < s.re, то LSeriesSummable (logMul f) s.

LaTeX

$$abscissaOfAbsConv f < s.re \Rightarrow LSeriesSummable (logMul f) s$$

Lean4

/-- If the L-series of `f` is summable at `s` and `re s < re s'`, then the L-series of the
point-wise product of `log` with `f` is summable at `s'`. -/
theorem LSeriesSummable_logMul_of_lt_re {f : ℕ → ℂ} {s : ℂ} (h : abscissaOfAbsConv f < s.re) :
    LSeriesSummable (logMul f) s :=
  (LSeriesSummable_logMul_and_hasDerivAt h).1

Похожие утверждения