LSeries_sum — Mathlib

English

If each f i is summable, then the L-series of the finite sum equals the finite sum of L-series values.

Русский

Если каждый f i суммируем, то L-ряд от конечной суммы равен сумме значений L-рядов.

LaTeX

$$$\forall i:\, i\in S,\ LSeries (S\!\sum i=> f i) s = S\!\sum i=> LSeries (f i) s$$$

Lean4

@[simp]
theorem LSeries_sum (hf : ∀ i ∈ S, LSeriesSummable (f i) s) : LSeries (∑ i ∈ S, f i) s = ∑ i ∈ S, LSeries (f i) s := by
  simpa [LSeries, term_sum] using Summable.tsum_finsetSum hf

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