LSeries_eq_zero_of_abscissaOfAbsConv_eq_top

English

If the abscissa of absolute convergence of f is infinite (top), then LSeries f equals zero.

Русский

Если абсцисса абсолютной сходимости f равна бесконечности (верхний предел), тогда LSeries f = 0.

LaTeX

$$$$ \operatorname{abscissaOfAbsConv}(f) = \top \quad\Rightarrow\quad LSeries f = 0. $$$$

Lean4

theorem LSeries_eq_zero_of_abscissaOfAbsConv_eq_top {f : ℕ → ℂ} (h : abscissaOfAbsConv f = ⊤) : LSeries f = 0 :=
  by
  ext1 s
  exact
    LSeries.eq_zero_of_not_LSeriesSummable f s <|
      mt LSeriesSummable.abscissaOfAbsConv_le <| h ▸ fun H ↦ (H.trans_lt <| EReal.coe_lt_top _).false

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